@@ -185,14 +185,13 @@ nameMatcher xs =
185
185
186
186
-- Initialize ------------------------------------------------------------------
187
187
188
- -- | initCryptolEnv - Create initial CryptolEnv, this involves loading the built-in modules
189
- -- (preludeName, arrayName, preludeReferenceName) and translating them into SAWCore, and
188
+ -- | initCryptolEnv - Create initial CryptolEnv, this involves loading
189
+ -- the built-in modules (preludeName, arrayName,
190
+ -- preludeReferenceName) and translating them into SAWCore, and
190
191
-- putting them into scope.
191
192
--
192
- -- NOTE: submodules in these built-in modules would be suppported here .
193
+ -- NOTE: submodules in these built-in modules are supported in this code .
193
194
--
194
- -- FIXME: There is some code duplication between this and `loadCryptolModule` and `importModule`.
195
-
196
195
initCryptolEnv ::
197
196
(? fileReader :: FilePath -> IO ByteString ) =>
198
197
SharedContext -> IO CryptolEnv
@@ -230,7 +229,6 @@ initCryptolEnv sc = do
230
229
let refMod = T. tcTopEntityToModule refTop
231
230
232
231
-- Set up reference implementation redirections
233
- -- FIXME: Unclear, add some documentation here.
234
232
let refDecls = T. mDecls refMod
235
233
let nms = Set. toList (MI. ifsPublic (TIface. genIfaceNames refMod))
236
234
@@ -434,9 +432,7 @@ checkNotParameterized m =
434
432
-- FIXME: Code duplication, these two functions are highly similar:
435
433
-- - loadCryptolModule
436
434
-- - importModule
437
- --
438
- -- TODO:
439
- -- - common up the common code
435
+ -- - TODO: "common up" the common code per #2569.
440
436
441
437
-- | loadCryptolModule - load a cryptol module and return a handle to
442
438
-- the `CryptolModule`. The contents of the module are not imported.
@@ -585,7 +581,10 @@ updateFFITypes m eTermEnv' eFFITypes' =
585
581
-- FIXME:
586
582
-- - submodules are not handled correctly below.
587
583
-- - the code is duplicating functionality that we have with `importModule`
588
- --
584
+ -- TODO:
585
+ -- - new design in PR#2569 should replace this function such that the
586
+ -- fundamental work is done via `importModule`.
587
+
589
588
bindCryptolModule :: (P. ModName , CryptolModule ) -> CryptolEnv -> CryptolEnv
590
589
bindCryptolModule (modName, CryptolModule sm tm) env =
591
590
env { eExtraNames = flip (foldr addName) (Map. keys tm') $
@@ -604,7 +603,6 @@ bindCryptolModule (modName, CryptolModule sm tm) env =
604
603
f _ = Nothing
605
604
606
605
addName name = MN. shadowing (MN. singletonNS C. NSValue (P. mkQual modName (MN. nameIdent name)) name)
607
- -- FIXME: suspicious. (Do we need to do any C.NSModule?)
608
606
609
607
addSubModule name = MN. shadowing (MN. singletonNS C. NSModule (P. mkQual modName (MN. nameIdent name)) name)
610
608
@@ -628,8 +626,9 @@ extractDefFromCryptolModule (CryptolModule _ tm) name =
628
626
-- environment with a module. Closely mirrors the sawscript command "import".
629
627
--
630
628
-- NOTE:
631
- -- - the module can be qualified or not (per 'as' argument).
632
- -- - per 'vis' we can import public definitions or *all* (i.e., kinternal and public) definitions.
629
+ -- - the module can be qualified or not (per 'as' argument). per
630
+ -- - 'vis' we can import public definitions or *all* (i.e., internal
631
+ -- and public) definitions.
633
632
634
633
importModule ::
635
634
(? fileReader :: FilePath -> IO ByteString ) =>
0 commit comments