Modules live in separate contexts, only imported modules are in scope

TODO.md

@@ -1,13 +1,14 @@
 
 ## TODO
 
+- [ ] `Def` is shadowed between Types and Syntax (TCon vs DCon), detect this
 - [ ] review pattern matching. goal is to have a sane context on the other end. secondary goal - bring it closer to the paper.
 
 - [x] redo code to determine base path
 - [ ] save/load results of processing a module
-  - [ ] keep each module separate in context
+  - [x] keep each module separate in context
-    - search would include imported modules, collect ops into and from modules
+    - [x] search would include imported modules, collect ops into and from modules
-    - should I allow the idris assignment hack?
+    - should I allow the idris cross module assignment hack?
     - >>> sort out metas (maybe push them up to the main list)
     - eventually we may want to support resuming halfway through a file
 

port/Lib/Common.newt

@@ -1,5 +1,6 @@
 module Lib.Common
 
+import Prelude
 import Data.String
 import Data.Int
 import Data.SortedMap

port/Lib/Compile.newt

@@ -1,12 +1,15 @@
 -- TODO Audit how much "outside" stuff could pile up in the continuation.
 module Lib.Compile
 
+import Prelude
+import Lib.Common
 import Lib.Types
 import Lib.Prettier
 import Lib.CompileExp
 import Lib.TopContext
 import Data.String
 import Data.Int
+import Data.SortedMap
 
 data StKind = Plain | Return | Assign String
 

port/Lib/CompileExp.newt

@@ -7,6 +7,8 @@
 -- I could make names unique (e.q. on lambdas), but I might want that to vary per backend?
 module Lib.CompileExp
 
+import Prelude
+import Lib.Common
 import Lib.Types -- Name / Tm
 import Lib.TopContext
 import Lib.Prettier

port/Lib/Elab.newt

@@ -1,14 +1,19 @@
 module Lib.Elab
 
+import Prelude
+import Lib.Common
 import Lib.Parser.Impl
 import Lib.Prettier
 import Data.String
+import Data.SnocList
 import Data.IORef
-import Lib.Types
+import Data.SortedMap
 import Lib.Eval
 import Lib.Util
 import Lib.TopContext
+-- FIXME Def is shadowing...
 import Lib.Syntax
+import Lib.Types
 
 
 vprint : Context -> Val -> M String
@@ -223,7 +228,11 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
           | res => do
               debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
               pure False
-      (nm :: Nil) <- findMatches ctx ty $ map snd $ toList top.defs
+      let te = listValues top.defs
+      let rest = map {List} (\ x => listValues x.modDefs) $
+            mapMaybe (flip lookupMap' top.modules) top.imported
+
+      (nm :: Nil) <- findMatches ctx ty $ join (te :: rest)
         | res => do
           debug $ \ _ => "FAILED to solve \{show ty}, matches: \{show res}"
           pure False
@@ -307,7 +316,7 @@ addConstraint env ix sp tm = do
     (Unsolved pos k a b c cons) => do
       debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
       pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
-    (Solved _ k tm) => error' "Meta \{show k} already solved (addConstraint :: Nil)"
+    (Solved _ k tm) => error' "Meta \{show k} already solved [addConstraint]"
     (OutOfScope) => error' "Meta \{show ix} out of scope"
   mc <- readIORef top.metaCtx
   checkAutos ix (listValues mc.metas)
@@ -417,7 +426,7 @@ maybeCheck action = do
 
 solve env m sp t = do
   meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m
-    | _ => error (getFC t) "Meta \{show m} already solved! (solve :: Nil)"
+    | _ => error (getFC t) "Meta \{show m} already solved! [solve]"
   debug $ \ _ => "SOLVE \{show m} \{show kind} lvl \{show $ length' env} sp \{show sp} is \{show t}"
   let size = length $ filter (\x => x == Bound) ctx_.bds
   debug $ \ _ => "\{show m} size is \{show size} sps \{show $ snoclen sp}"
@@ -442,7 +451,7 @@ solve env m sp t = do
 
     updateMeta m $ \case
       (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
-      (Solved _ k x) => error' "Meta \{show ix} already solved! (solve2 :: Nil)"
+      (Solved _ k x) => error' "Meta \{show ix} already solved! [solve2]"
       OutOfScope => error' "Meta \{show ix} out of scope"
     maybeCheck $ for_ cons $ \case
       MkMc fc env sp rhs => do
@@ -645,7 +654,7 @@ freshMeta ctx fc ty kind = do
   debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
   -- need the ns here
   -- we were fudging this for v1
-  let qn = QN ("$meta" :: Nil) (show mc.next)
+  let qn = QN top.ns "$m\{show mc.next}"
   let newmeta = Unsolved fc qn ctx ty kind Nil
   writeIORef top.metaCtx $ MC (updateMap qn newmeta mc.metas) (1 + mc.next) mc.mcmode
   -- infinite loop - keeps trying Ord a => Ord (a \x a)
@@ -1445,8 +1454,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types
         Nothing => error fc "\{show nm} not in scope"
     go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty)
       else go (i + 1) xs
--- FIXME tightens up output but hardcodes a name
+
--- infer ctx (RApp fc (RVar _ "_$_") u icit) = infer ctx u
 infer ctx (RApp fc t u icit) = do
   -- If the app is explicit, add any necessary metas
   (icit, t, tty) <- case the Icit icit of

port/Lib/Erasure.newt

@@ -1,5 +1,7 @@
 module Lib.Erasure
 
+import Prelude
+import Lib.Common
 import Lib.Types
 import Data.SnocList
 import Lib.TopContext

port/Lib/Eval.newt

@@ -1,5 +1,8 @@
 module Lib.Eval
 
+import Prelude
+import Lib.Common
+import Lib.Prettier
 import Lib.Types
 import Lib.TopContext
 

port/Lib/Parser.newt

@@ -2,6 +2,9 @@ module Lib.Parser
 
 -- NOW Still working on this.
 
+import Prelude
+import Lib.Common
+import Data.SortedMap
 import Data.String
 import Lib.Parser.Impl
 import Lib.Syntax

port/Lib/Parser/Impl.newt

@@ -1,5 +1,6 @@
 module Lib.Parser.Impl
 
+import Prelude
 import Lib.Token
 import Lib.Common
 import Data.String

port/Lib/Prettier.newt

@@ -1,7 +1,7 @@
 -- A prettier printer, Philip Wadler
 -- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
 module Lib.Prettier
-
+import Prelude
 import Data.Int
 
 -- `Doc` is a pretty printing document.  Constructors are private, use

port/Lib/ProcessDecl.newt

@@ -1,13 +1,17 @@
 module Lib.ProcessDecl
 
+import Prelude
 import Data.IORef
 import Data.String
 
+import Lib.Common
 import Lib.Elab
 import Lib.Parser
 import Lib.Syntax
+import Data.SortedMap
 import Lib.TopContext
 import Lib.Eval
+import Lib.Prettier
 import Lib.Types
 import Lib.Util
 import Lib.Erasure

port/Lib/Syntax.newt

@@ -1,5 +1,7 @@
 module Lib.Syntax
 
+import Prelude
+import Lib.Common
 import Data.String
 import Lib.Parser.Impl
 import Lib.Prettier

port/Lib/Tokenizer.newt

@@ -7,7 +7,7 @@ module Lib.Tokenizer
 
 -- Newt is having a rough time dealing with do blocks for Either in here
 --
-
+import Prelude
 import Lib.Token
 import Lib.Common
 import Data.String

port/Lib/TopContext.newt

@@ -3,6 +3,8 @@ module Lib.TopContext
 import Data.IORef
 import Data.SortedMap
 import Data.String
+import Prelude
+import Lib.Common
 import Lib.Types
 
 -- I want unique ids, to be able to lookup, update, and a Ref so
@@ -10,29 +12,39 @@ import Lib.Types
 
 
 lookup : QName -> TopContext -> Maybe TopEntry
-lookup nm top = lookupMap' nm top.defs
+lookup qn@(QN ns nm) top =
+  case lookupMap' qn top.defs of
+    Just entry => Just entry
+    Nothing => case lookupMap' ns top.modules of
+      Just mod => lookupMap' qn mod.modDefs
+      Nothing => Nothing
 
 -- TODO - look at imported namespaces, and either have a map of imported names or search imported namespaces..
 
 lookupRaw : String -> TopContext -> Maybe TopEntry
-lookupRaw raw top = go $ toList top.defs
+lookupRaw raw top =
+  case lookupMap' (QN top.ns raw) top.defs of
+    Just entry => Just entry
+    Nothing => go top.imported
   where
-    go : List (QName × TopEntry) -> Maybe TopEntry
+    go : List (List String) → Maybe TopEntry
     go Nil = Nothing
-    go (((QN ns nm), entry) :: rest) = if nm == raw then Just entry else go rest
+    go (ns :: nss) = case lookupMap' ns top.modules of
-
+      Nothing => go nss
--- Maybe pretty print?
+      Just mod => case lookupMap' (QN ns raw) mod.modDefs of
+        Just entry => Just entry
+        Nothing => go nss
 
 
 instance Show TopContext where
-  show (MkTop defs metas _ _ _ _) = "\nContext:\n (\{ joinBy "\n" $ map (show ∘ snd) $ toList defs} :: Nil)"
+  show (MkTop _ _ _ defs metas _ _ _) = "\nContext:\n (\{ joinBy "\n" $ map (show ∘ snd) $ toList defs} :: Nil)"
 
 -- TODO need to get class dependencies working
 emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
 emptyTop = do
   mcctx <- newIORef (MC EmptyMap 0 CheckAll)
   errs <- newIORef $ the (List Error) Nil
-  pure $ MkTop EmptyMap mcctx False errs Nil EmptyMap
+  pure $ MkTop EmptyMap Nil Nil EmptyMap mcctx False errs EmptyMap
 
 
 setDef : QName -> FC -> Tm -> Def -> M Unit
@@ -41,9 +53,9 @@ setDef name fc ty def = do
   let (Nothing) = lookupMap' name top.defs
     | Just (MkEntry fc' nm' ty' def') => error fc "\{show name} is already defined at \{show fc'}"
   modify $ \case
-    MkTop defs metaCtx verbose errors loaded ops =>
+    MkTop mods imp ns defs metaCtx verbose errors ops =>
       let defs = (updateMap name (MkEntry fc name ty def) top.defs) in
-      MkTop defs metaCtx verbose errors loaded ops
+      MkTop mods imp ns defs metaCtx verbose errors ops
 
 
 updateDef : QName -> FC -> Tm -> Def -> M Unit
@@ -52,9 +64,9 @@ updateDef name fc ty def = do
   let (Just (MkEntry fc' nm' ty' def')) = lookupMap' name top.defs
     | Nothing => error fc "\{show name} not declared"
   modify $ \case
-    MkTop defs metaCtx verbose errors loaded ops =>
+    MkTop mods imp ns defs metaCtx verbose errors ops =>
       let defs = (updateMap name (MkEntry fc' name ty def) defs) in
-      MkTop defs metaCtx verbose errors loaded ops
+      MkTop mods imp ns defs metaCtx verbose errors ops
 
 addError : Error -> M Unit
 addError err = do

port/Lib/Types.newt

@@ -1,6 +1,6 @@
 module Lib.Types
 
--- For FC, Error
+import Prelude
 import Lib.Common
 import Lib.Prettier
 
@@ -332,6 +332,14 @@ record TopEntry where
 instance Show TopEntry where
   show (MkEntry fc name type def) = "\{show name} : \{show type} := \{show def}"
 
+record ModContext where
+  constructor MkModCtx
+  modDefs : SortedMap QName TopEntry
+  -- Do we need this if everything solved is zonked?
+  modMetaCtx : MetaContext
+  -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import
+  ctxOps : Operators
+
 -- Top level context.
 -- Most of the reason this is separate is to have a different type
 -- `Def` for the entries.
@@ -339,15 +347,26 @@ instance Show TopEntry where
 -- The price is that we have names in addition to levels. Do we want to
 -- expand these during normalization?
 
+-- A placeholder while walking through dependencies of a module
+emptyModCtx : ModContext
+emptyModCtx = MkModCtx EmptyMap (MC EmptyMap 0 NoCheck) EmptyMap
+
 record TopContext where
   constructor MkTop
-  -- We'll add a map later?
+  -- maybe we use a String instead of List String for the left of QN
+  -- I'm putting a dummy entry in
+  modules : SortedMap (List String) ModContext
+  imported : List (List String)
+
+  -- current module
+  ns : List String
   defs : SortedMap QName TopEntry
   metaCtx : IORef MetaContext
+
+  -- Global values
   verbose : Bool -- command line flag
   errors : IORef (List Error)
-  -- loaded modules
+  -- what do we do here? we can accumulate for now, but we'll want to respect import
-  loaded : List String
   ops : Operators
 
 -- we'll use this for typechecking, but need to keep a TopContext around too.
@@ -482,12 +501,18 @@ error' : ∀ a. String -> M a
 error' msg = throwError $ E emptyFC msg
 
 lookupMeta : QName -> M MetaEntry
-lookupMeta ix = do
+lookupMeta ix@(QN ns nm) = do
   top <- get
   mc <- readIORef {M} top.metaCtx
   case lookupMap' ix mc.metas of
     Just meta => pure meta
-    Nothing => pure OutOfScope
+    Nothing => case lookupMap' ns top.modules of
+      Nothing => 
+          error emptyFC "missing module: \{show ns}"
+      Just mod => case lookupMap' ix mod.modMetaCtx.metas of
+        Nothing => 
+          error emptyFC "missing meta: \{show ix}"
+        Just entry => pure entry 
 
 mkCtx : FC -> Context
 mkCtx fc = MkCtx 0 Nil Nil Nil fc

port/Lib/Util.newt

@@ -1,5 +1,7 @@
 module Lib.Util
 
+import Prelude
+import Lib.Common
 import Lib.Types
 import Data.List1
 

port/Main.newt

@@ -1,8 +1,10 @@
 module Main
 
+import Prelude
 import Data.List1
 import Data.String
 import Data.IORef
+import Data.SortedMap
 import Lib.Common
 import Lib.Compile
 import Lib.Parser
@@ -18,6 +20,9 @@ import Lib.Syntax
 import Lib.Syntax
 import Node
 
+primNS : List String
+primNS = ("Prim" :: Nil)
+
 jsonTopContext : M Json
 jsonTopContext = do
   top <- get
@@ -77,9 +82,10 @@ processModule : FC -> String -> List String -> QName -> M String
 processModule importFC base stk qn@(QN ns nm) = do
   top <- get
   -- TODO make top.loaded a List QName
-  let name = joinBy "." (snoc ns nm)
+  let modns = (snoc ns nm)
-  let (False) = elem name top.loaded | _ => pure ""
+  let name = joinBy "." modns
-  modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors (name :: top.loaded)top.ops)
+  let (Nothing) = lookupMap modns top.modules | _ => pure ""
+  modify (\ top => MkTop (updateMap modns emptyModCtx top.modules) top.imported top.ns top.defs top.metaCtx top.verbose top.errors top.ops)
   let fn = (joinBy "/" (base :: ns)) ++ "/" ++ nm ++ ".newt"
   (Right src) <- liftIO {M} $ readFile fn
     | Left err => exitFailure "ERROR at \{show importFC}: error reading \{fn}: \{show err}"
@@ -99,7 +105,7 @@ processModule importFC base stk qn@(QN ns nm) = do
   let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks
     | Left (err, toks) => exitFailure (showError src err)
 
-  for imports $ \case
+  imported <- for imports $ \case
     MkImport fc name' => do
       let (a,b) = unsnoc $ split1 name' "."
       let qname = QN a b
@@ -107,16 +113,30 @@ processModule importFC base stk qn@(QN ns nm) = do
       when (elem name' stk) $ \ _ => error emptyFC "import loop \{show name} -> \{show name'}"
 
       processModule fc base (name :: stk) qname
+      pure $ split name' "."
+
+  let imported = snoc imported primNS
+
+  -- I guess we should empty defs now instead of at the end?
+
+  putStrLn $ "MODNS " ++ show modns
+  top <- get
+  (decls, ops) <- parseDecls fn top.ops toks Lin
 
   top <- get
-  mc <- readIORef top.metaCtx
+  freshMC <- newIORef (MC EmptyMap 0 CheckAll)
-
+  -- set imported, mod, freshMC, ops  before processing
-  (decls, ops) <- parseDecls fn top.ops toks Lin
+  modify (\ top => MkTop top.modules imported modns EmptyMap freshMC top.verbose top.errors ops)
-  modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors top.loaded ops)
   putStrLn "process Decls"
-
   traverse (tryProcessDecl ns) (collectDecl decls)
 
+  -- update modules with result
+  top <- get
+  mc <- readIORef top.metaCtx
+  let modules = updateMap modns (MkModCtx top.defs mc top.ops) top.modules
+  freshMC <- newIORef (MC EmptyMap 0 CheckAll)
+  modify (\ top => MkTop modules Nil Nil EmptyMap freshMC top.verbose top.errors top.ops)
+
   (Nil) <- liftIO {M} $ readIORef top.errors
     | errors => do
         for_ errors $ \err =>
@@ -179,9 +199,15 @@ processFile fn = do
   -- let base = if base == "" then "." else base
 
   -- declare internal primitives
-  processDecl ("Prim" :: Nil) (PType emptyFC "Int" Nothing)
+
-  processDecl ("Prim" :: Nil) (PType emptyFC "String" Nothing)
+  processDecl primNS (PType emptyFC "Int" Nothing)
-  processDecl ("Prim" :: Nil) (PType emptyFC "Char" Nothing)
+  processDecl primNS (PType emptyFC "String" Nothing)
+  processDecl primNS (PType emptyFC "Char" Nothing)
+
+  top <- get
+  let modules = updateMap primNS (MkModCtx top.defs (MC EmptyMap 0 CheckAll) top.ops) top.modules
+  modify (\ top => MkTop modules (primNS :: Nil) Nil EmptyMap top.metaCtx top.verbose top.errors top.ops)
+
 
   src <- processModule emptyFC base Nil qn
   top <- get
@@ -200,7 +226,7 @@ cmdLine : List String -> M (Maybe String × List String)
 cmdLine Nil = pure (Nothing, Nil)
 cmdLine ("--top" :: args) = cmdLine args -- handled later
 cmdLine ("-v" :: args) = do
-  modify (\ top => MkTop top.defs top.metaCtx True top.errors top.loaded top.ops)
+  modify (\ top => MkTop top.modules top.imported top.ns top.defs top.metaCtx True top.errors top.ops)
   cmdLine args
 cmdLine ("-o" :: fn :: args) = do
   (out, files) <- cmdLine args

src/Lib/Parser/Impl.idr

@@ -1,10 +1,12 @@
 module Lib.Parser.Impl
 
+import Prelude
 import Lib.Token
 import Lib.Common
 import Data.String
 import Data.Nat
 import Data.List1
+import Data.SortedMap
 
 public export
 TokenList : Type