@@ -260,6 +260,20 @@ initCryptolEnv sc = do
260
260
, eFFITypes = Map. empty
261
261
}
262
262
263
+ -- | Translate all declarations in all loaded modules to SAWCore terms
264
+ -- NOTE: used only for initialization code.
265
+
266
+ genTermEnv :: SharedContext -> ME. ModuleEnv -> C. Env -> IO (Map T. Name Term )
267
+ genTermEnv sc modEnv cryEnv0 = do
268
+ let declGroups = concatMap T. mDecls
269
+ $ filter (not . T. isParametrizedModule)
270
+ $ ME. loadedModules modEnv
271
+ nominals = ME. loadedNominalTypes modEnv
272
+ cryEnv1 <- C. genCodeForNominalTypes sc nominals cryEnv0
273
+ cryEnv2 <- C. importTopLevelDeclGroups sc C. defaultPrimitiveOptions cryEnv1 declGroups
274
+ return (C. envE cryEnv2)
275
+
276
+
263
277
-- Parse -----------------------------------------------------------------------
264
278
265
279
ioParseExpr :: InputText -> IO (P. Expr P. PName )
@@ -400,17 +414,6 @@ translateDeclGroups sc env dgs =
400
414
, eTermEnv = C. envE cryEnv'
401
415
}
402
416
403
- -- | Translate all declarations in all loaded modules to SAWCore terms
404
- genTermEnv :: SharedContext -> ME. ModuleEnv -> C. Env -> IO (Map T. Name Term )
405
- genTermEnv sc modEnv cryEnv0 = do
406
- let declGroups = concatMap T. mDecls
407
- $ filter (not . T. isParametrizedModule)
408
- $ ME. loadedModules modEnv
409
- nominals = ME. loadedNominalTypes modEnv
410
- cryEnv1 <- C. genCodeForNominalTypes sc nominals cryEnv0
411
- cryEnv2 <- C. importTopLevelDeclGroups sc C. defaultPrimitiveOptions cryEnv1 declGroups
412
- return (C. envE cryEnv2)
413
-
414
417
--------------------------------------------------------------------------------
415
418
416
419
@@ -669,7 +672,7 @@ importModule sc env src as vis imps = do
669
672
do oldCryEnv <- mkCryEnv env
670
673
cEnv <- C. genCodeForNominalTypes sc newNominal oldCryEnv
671
674
newCryEnv <- C. importTopLevelDeclGroups
672
- sc C. defaultPrimitiveOptions cEnv newDeclGroups
675
+ sc C. defaultPrimitiveOptions cEnv newDeclGroups
673
676
return (C. envE newCryEnv)
674
677
675
678
let newImport = (vis, P. Import { T. iModule= locate $ T. mName m
0 commit comments