add syntax for inline examples

marklemay · Apr 8, 2024 · a9ba280 · a9ba280
1 parent 4751b13
commit a9ba280
Show file tree

Hide file tree

Showing 3 changed files with 327 additions and 320 deletions.
diff --git a/src/Env.hs b/src/Env.hs
@@ -38,6 +38,9 @@ type DefCtx = Map RefName (Term, Ty)
 
 type Module = (Map TCName DataDef, DefCtx)
 
+-- we can have some internal stuff in a module that should not be exposed (examples for instnace)
+type OpenModule = (Module, [Term])
+
 -- TODO clean up the notion of module, undermodule
 
 -- | rempaps all the unbound vars that match dataconstructors and typeconstructors 

diff --git a/src/Ffi/Ffi.hs b/src/Ffi/Ffi.hs
@@ -131,7 +131,7 @@ loadString s =
 
   case parseModule webPath s of
     Left ls -> parseError ls
-    Right m@(ddefs,trmdefs) -> 
+    Right (m@(ddefs,trmdefs), examples) -> 
       -- loggg $ lfullshow  m
       let em = runExcept $ runFreshMT $ C.elabmodule (empTyEnv{dataCtx=ddefs,defCtx=trmdefs}) sr in
 
@@ -151,7 +151,7 @@ loadString s =
 
 
 
-parseModule :: Path -> String -> Either ParseError Module
+parseModule :: Path -> String -> Either ParseError Env.OpenModule
 parseModule path s = prettyParse path s $ token modulep