rename top/put/modify on M to avoid collisions

TODO.md

@@ -1,10 +1,14 @@
 
 ## TODO
 
+Syntax -> Parser.Impl ?
+
 - [ ] implement tail call optimization
 - [ ] `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.
 
+- [ ] rename for top level functions (and maybe stuff in scope, probably need LSP first)
+- [ ] warn on unused imports?
 - [x] redo code to determine base path
 - [x] emit only one branch for default case when splitting inductives
 - [ ] save/load results of processing a module

port/Lib/Compile.newt

@@ -311,7 +311,7 @@ getNames _ acc = acc
 -- This will be what we work on for optimization passes
 getEntries : SortedMap QName Def → QName → M (SortedMap QName Def)
 getEntries acc name = do
-  top <- get
+  top <- getTop
   case lookup name top of
     Nothing => do
       putStrLn "bad name \{show name}"
@@ -355,7 +355,7 @@ process name = do
 
 compile : M (List Doc)
 compile = do
-  top <- get
+  top <- getTop
   case lookupRaw "main" top of
     Just (MkEntry fc name type def) => do
       tmp <- process name

port/Lib/CompileExp.newt

@@ -54,7 +54,7 @@ lamArity _ = Z
 -- TODO - figure out how this will work with erasure
 arityForName : FC -> QName -> M Nat
 arityForName fc nm = do
-  top <- get
+  top <- getTop
   case lookup nm top of
   -- let the magic hole through for now (will generate bad JS)
     Nothing => error fc "Name \{show nm} not in scope"
@@ -90,7 +90,7 @@ apply t ts acc Z ty = go (CApp t (acc <>> Nil) 0) ts
 compileTerm (Bnd _ k) = pure $ CBnd k
 -- need to eta expand to arity
 compileTerm t@(Ref fc nm) = do
-  top <- get
+  top <- getTop
   let (Just (MkEntry _ _ type _)) = lookup nm top
           | Nothing => error fc "Undefined name \{show nm}"
   arity <- arityForName fc nm
@@ -108,7 +108,7 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
   (t@(Ref fc nm), args) => do
         args' <- traverse compileTerm args
         arity <- arityForName fc nm
-        top <- get
+        top <- getTop
         let (Just (MkEntry _ _ type _)) = lookup nm top
           | Nothing => error fc "Undefined name \{show nm}"
         apply (CRef (show nm)) args' Lin arity type

port/Lib/Elab.newt

@@ -118,7 +118,7 @@ findMatches : Context -> Val -> List TopEntry -> M (List String)
 findMatches ctx ty Nil = pure Nil
 findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
   let (True) = isCandidate ty type | False => findMatches ctx ty xs
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   catchError (do
       -- TODO sort out the FC here
@@ -145,7 +145,7 @@ contextMatches ctx ty = go (zip ctx.env ctx.types)
     go ((tm, nm, vty) :: xs) = do
       type <- quote ctx.lvl vty
       let (True) = isCandidate ty type | False => go xs
-      top <- get
+      top <- getTop
       mc <- readIORef top.metaCtx
       catchError(do
           debug $ \ _ => "TRY context \{nm} : \{rpprint (names ctx) type} for \{show ty}"
@@ -180,7 +180,7 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
       ty <- eval ctx.env CBN x
       debug $ \ _ => "AUTO ---> \{show ty}"
       -- we want the context here too.
-      top <- get
+      top <- getTop
       Nil <- contextMatches ctx ty
           | ((tm, vty) :: Nil) => do
               unifyCatch (getFC ty) ctx ty vty
@@ -210,7 +210,7 @@ trySolveAuto _ = pure False
 
 solveAutos : M Unit
 solveAutos = do
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   res <- run $ filter isAuto (listValues mc.metas)
   if res then solveAutos else pure MkUnit
@@ -229,7 +229,7 @@ solveAutos = do
 
 updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit
 updateMeta ix f = do
-  top <- get
+  top <- getTop
   mc <- readIORef {M} top.metaCtx
   let (Just me) = lookupMap' ix mc.metas | Nothing => pure MkUnit
   me <- f me
@@ -250,7 +250,7 @@ checkAutos ix (_ :: rest) = checkAutos ix rest
 
 addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit
 addConstraint env ix sp tm = do
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   let (CheckAll) = mc.mcmode | _ => pure MkUnit
   updateMeta ix $ \case
@@ -345,7 +345,7 @@ ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst
 
 maybeCheck : M Unit -> M Unit
 maybeCheck action = do
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   case mc.mcmode of
     CheckAll => action
@@ -377,7 +377,7 @@ solve env m sp t = do
     tm <- rename m ren l t
 
     let tm = lams (snoclen sp) (reverse ctx_.boundNames) tm
-    top <- get
+    top <- getTop
     soln <- eval Nil CBN tm
 
     updateMeta m $ \case
@@ -471,7 +471,7 @@ unify env mode t u = do
     -- We _could_ look up the ref, eval against Nil and vappSpine...
     unifyRef t         u@(VRef fc' k' sp') = do
       debug $ \ _ => "expand \{show t} =?= %ref \{show k'}"
-      top <- get
+      top <- getTop
       case lookup k' top of
         Just (MkEntry _ name ty (Fn tm)) => do
           vtm <- eval Nil CBN tm
@@ -481,7 +481,7 @@ unify env mode t u = do
 
     unifyRef t@(VRef fc k sp) u = do
       debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
-      top <- get
+      top <- getTop
       case lookup k top of
         Just (MkEntry _ name ty (Fn tm)) => do
           vtm <- eval Nil CBN tm
@@ -577,7 +577,7 @@ unifyCatch fc ctx ty' ty = do
 
 freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
 freshMeta ctx fc ty kind = do
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
   -- need the ns here
@@ -618,7 +618,7 @@ insert ctx tm ty = do
 
 primType : FC -> QName -> M Val
 primType fc nm = do
-  top <- get
+  top <- getTop
   case lookup nm top of
       Just (MkEntry _ name ty (PrimTCon _)) => pure $ VRef fc name Lin
       _ => error fc "Primitive type \{show nm} not in scope"
@@ -686,13 +686,13 @@ getConstructors ctx scfc (VRef fc nm _) = do
   where
     lookupTCon : QName -> M (List QName)
     lookupTCon str = do
-      top <- get
+      top <- getTop
       case lookup nm top of
         (Just (MkEntry _ name type (TCon _ names))) => pure names
         _ => error scfc "Not a type constructor \{show nm}"
     lookupDCon : QName -> M (QName × Int × Tm)
     lookupDCon nm = do
-      top <- get
+      top <- getTop
       case lookup nm top of
         (Just (MkEntry _ name type (DCon k str))) => pure (name, k, type)
         Just _ => error fc "Internal Error: \{show nm} is not a DCon"
@@ -944,7 +944,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
                 pure $ Just $ (scnm, (PatVar fc icit nm')) :: rest ++ xs ++ acc
             else do
               -- TODO can we check this when we make the PatCon?
-              top <- get
+              top <- getTop
               case lookup nm top of
                   (Just (MkEntry _ name type (DCon k tcname))) =>
                     if (tcname /= sctynm)
@@ -971,7 +971,7 @@ mkPat (RAs fc as tm, icit) = do
     (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}"
     t => error fc "Can't put as on non-constructor \{show tm}"
 mkPat (tm, icit) = do
-  top <- get
+  top <- getTop
   case splitArgs tm Nil of
     ((RVar fc nm), b) => case lookupRaw nm top of
                 (Just (MkEntry _ name type (DCon k str))) => do
@@ -1011,7 +1011,7 @@ checkWhere ctx decls body ty = do
     | _ => error sigFC "expected function definition after this signature"
   unless (name == name') $ \ _ => error defFC "Expected def for \{name}"
   -- REVIEW is this right, cribbed from my top level code
-  top <- get
+  top <- getTop
   clauses' <- traverse makeClause clauses
   vty <- eval ctx.env CBN funTy
   debug $ \ _ => "\{name} vty is \{show vty}"
@@ -1222,7 +1222,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
       case meta of
         (Solved _ k t) => forceType ctx.env scty'
         (Unsolved _ k xs _ _ _) => do
-          top <- get
+          top <- getTop
           mc <- readIORef top.metaCtx
           -- TODO - only hit the relevant ones
           solveAutos
@@ -1292,7 +1292,7 @@ undo prev ((DoExpr fc tm) :: xs) = do
   pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit
 undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs
 undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
-  top <- get
+  top <- getTop
   case lookupRaw nm top of
     Just _ => do
       let nm = "$sc"
@@ -1328,7 +1328,7 @@ check ctx tm ty = do
       debug $ \ _ => "SCTY \{show scty}"
 
       let scnm = fresh "sc"
-      top <- get
+      top <- getTop
       clauses <- for alts $ \case
         (MkAlt pat rawRHS) => do
           pat' <- mkPat (pat, Explicit)
@@ -1408,7 +1408,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types
   where
     go : Int -> List (String × Val)  -> M (Tm × Val)
     go i Nil = do
-      top <- get
+      top <- getTop
       case lookupRaw nm top of
         Just (MkEntry _ name ty def) => do
           debug $ \ _ => "lookup \{show name} as \{show def}"

port/Lib/Erasure.newt

@@ -16,7 +16,7 @@ EEnv = List (String × Quant × Maybe Tm)
 
 getType : Tm -> M (Maybe Tm)
 getType (Ref fc nm) = do
-  top <- get
+  top <- getTop
   case lookup nm top of
     Nothing => error fc "\{show nm} not in scope"
     (Just (MkEntry _ name type def)) => pure $ Just type
@@ -45,7 +45,7 @@ doAlt : EEnv -> CaseAlt -> M CaseAlt
 -- REVIEW do we extend env?
 doAlt env (CaseDefault t) = CaseDefault <$> erase env t Nil
 doAlt env (CaseCons name args t) = do
-  top <- get
+  top <- getTop
   let (Just (MkEntry _ str type def)) = lookup name top
     | _ => error emptyFC "\{show name} dcon missing from context"
   let env' = piEnv env type args
@@ -64,7 +64,7 @@ doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t Nil
 erase env t sp = case t of
   (App fc u v) => erase env u ((fc,v) :: sp)
   (Ref fc nm) => do
-    top <- get
+    top <- getTop
     case lookup nm top of
       Nothing => error fc "\{show nm} not in scope"
       (Just (MkEntry _ name type def)) => eraseSpine env t sp (Just type)

port/Lib/Eval.newt

@@ -68,7 +68,7 @@ unlet env x = pure x
 -- Try applying VRef to spine, back out if it is stuck
 tryEval : Env -> Val -> M (Maybe Val)
 tryEval env (VRef fc k sp) = do
-  top <- get
+  top <- getTop
   case lookup k top of
       Just (MkEntry _ name ty (Fn tm)) =>
         catchError (
@@ -106,7 +106,7 @@ forceType env x = do
 
 evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
 evalCase env mode sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
-  top <- get
+  top <- getTop
   if nm == name
     then do
       debug $ \ _ =>  "ECase \{show nm} \{show sp} \{show nms} \{showTm t}"

port/Lib/ProcessDecl.newt

@@ -64,7 +64,7 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
           ty <- eval ctx.env CBN x
           debug $ \ _ => "AUTO ---> \{show ty}"
           -- we want the context here too.
-          top <- get
+          top <- getTop
           -- matches <- case !(contextMatches ctx ty) of
           --   Nil => findMatches ctx ty $ toList top.defs
           --   xs => pure xs
@@ -105,7 +105,7 @@ processDecl ns  (PMixFix _ _ _ _)  = pure MkUnit
 processDecl ns  (TypeSig fc names tm) = do
   log 1 $ \ _ => "-----"
 
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   -- let mstart = length' mc.metas
   for names $ \nm => do
@@ -118,13 +118,13 @@ processDecl ns  (TypeSig fc names tm) = do
   ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom
 
 processDecl ns (PType fc nm ty) = do
-  top <- get
+  top <- getTop
   ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc)
   let arity = cast $ piArity ty'
   setDef (QN ns nm) fc ty' (PrimTCon arity)
 
 processDecl ns  (PFunc fc nm used ty src) = do
-  top <- get
+  top <- getTop
   ty <- check (mkCtx fc) ty (VU fc)
   ty' <- nf Nil ty
   log 1 $ \ _ => "pfunc \{nm} : \{render 90 $ pprint Nil ty'} = \{show src}"
@@ -137,7 +137,7 @@ processDecl ns  (PFunc fc nm used ty src) = do
 processDecl ns (Def fc nm clauses) = do
   log 1 $ \ _ => "-----"
   log 1 $ \ _ => "Def \{show nm}"
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   let (Just entry) = lookupRaw nm top
     | Nothing => throwError $ E fc "No declaration for \{nm}"
@@ -173,7 +173,7 @@ processDecl ns (Def fc nm clauses) = do
 
 processDecl ns (DCheck fc tm ty) = do
   log 1 $ \ _ => "----- DCheck"
-  top <- get
+  top <- getTop
 
   info fc "check \{show tm} at \{show ty}"
   ty' <- check (mkCtx fc) ty (VU fc)
@@ -237,7 +237,7 @@ processDecl ns (Instance instfc ty decls) = do
 
   log 1 $ \ _ => "-----"
   log 1 $ \ _ => "Instance \{render 90 $ pretty ty}"
-  top <- get
+  top <- getTop
   let tyFC = getFC ty
 
   vty <- check (mkCtx instfc) ty (VU instfc)
@@ -374,7 +374,7 @@ processDecl ns (ShortData fc lhs sigs) = do
 processDecl ns (Data fc nm ty cons) = do
   log 1 $ \ _ => "-----"
   log 1 $ \ _ => "Data \{nm}"
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
   tyty <- check (mkCtx fc) ty (VU fc)
   case lookupRaw nm top of

port/Lib/Syntax.newt

@@ -3,7 +3,6 @@ module Lib.Syntax
 import Prelude
 import Lib.Common
 import Data.String
-import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.Types
 

port/Lib/TopContext.newt

@@ -49,10 +49,10 @@ emptyTop = do
 
 setDef : QName -> FC -> Tm -> Def -> M Unit
 setDef name fc ty def = do
-  top <- get
+  top <- getTop
   let (Nothing) = lookupMap' name top.defs
     | Just (MkEntry fc' nm' ty' def') => error fc "\{show name} is already defined at \{show fc'}"
-  modify $ \case
+  modifyTop $ \case
     MkTop mods imp ns defs metaCtx verbose errors ops =>
       let defs = (updateMap name (MkEntry fc name ty def) top.defs) in
       MkTop mods imp ns defs metaCtx verbose errors ops
@@ -60,15 +60,15 @@ setDef name fc ty def = do
 
 updateDef : QName -> FC -> Tm -> Def -> M Unit
 updateDef name fc ty def = do
-  top <- get
+  top <- getTop
   let (Just (MkEntry fc' nm' ty' def')) = lookupMap' name top.defs
     | Nothing => error fc "\{show name} not declared"
-  modify $ \case
+  modifyTop $ \case
     MkTop mods imp ns defs metaCtx verbose errors ops =>
       let defs = (updateMap name (MkEntry fc' name ty def) defs) in
       MkTop mods imp ns defs metaCtx verbose errors ops
 
 addError : Error -> M Unit
 addError err = do
-  top <- get
+  top <- getTop
   modifyIORef top.errors (_::_ err)

port/Lib/Types.newt

@@ -460,27 +460,27 @@ filterM pred (x :: xs) = do
   if check then _::_ x <$> filterM pred xs else filterM pred xs
 
 
-get : M TopContext
-get = MkM $ \ tc => pure $ Right (tc, tc)
+getTop : M TopContext
+getTop = MkM $ \ tc => pure $ Right (tc, tc)
 
-put : TopContext -> M Unit
-put tc = MkM $ \_ => pure $ Right (tc, MkUnit)
+putTop : TopContext -> M Unit
+putTop tc = MkM $ \_ => pure $ Right (tc, MkUnit)
 
-modify : (TopContext -> TopContext) -> M Unit
-modify f = do
-  tc <- get
-  put (f tc)
+modifyTop : (TopContext -> TopContext) -> M Unit
+modifyTop f = do
+  tc <- getTop
+  putTop (f tc)
 
 -- Force argument and print if verbose is true
 
 log : Int -> Lazy String -> M Unit
 log lvl x = do
-  top <- get
+  top <- getTop
   when (lvl <= top.verbose) $ \ _ => putStrLn $ force x
 
 logM : Int → M String -> M Unit
 logM lvl x = do
-  top <- get
+  top <- getTop
   when (lvl <= top.verbose) $ \ _ => do
     msg <- x
     putStrLn msg
@@ -516,7 +516,7 @@ error' msg = throwError $ E emptyFC msg
 
 lookupMeta : QName -> M MetaEntry
 lookupMeta ix@(QN ns nm) = do
-  top <- get
+  top <- getTop
   mc <- readIORef {M} top.metaCtx
   case lookupMap' ix mc.metas of
     Just meta => pure meta

port/Main.newt

@@ -27,7 +27,7 @@ primNS = ("Prim" :: Nil)
 
 jsonTopContext : M Json
 jsonTopContext = do
-  top <- get
+  top <- getTop
   pure $ JsonObj (("context", JsonArray (map jsonDef $ listValues top.defs)) :: Nil)
   where
     jsonDef : TopEntry -> Json
@@ -82,12 +82,12 @@ parseDecls fn ops toks@(first :: _) acc =
 -- New style loader, one def at a time
 processModule : FC -> String -> List String -> QName -> M String
 processModule importFC base stk qn@(QN ns nm) = do
-  top <- get
+  top <- getTop
   -- TODO make top.loaded a List QName
   let modns = (snoc ns nm)
   let name = joinBy "." modns
   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)
+  modifyTop (\ 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}"
@@ -121,18 +121,18 @@ processModule importFC base stk qn@(QN ns nm) = do
 
   putStrLn "module \{modName}"
   log 1 $ \ _ => "MODNS " ++ show modns
-  top <- get
+  top <- getTop
   (decls, ops) <- parseDecls fn top.ops toks Lin
 
-  top <- get
+  top <- getTop
   freshMC <- newIORef (MC EmptyMap 0 CheckAll)
   -- set imported, mod, freshMC, ops  before processing
-  modify (\ top => MkTop top.modules imported modns EmptyMap freshMC top.verbose top.errors ops)
+  modifyTop (\ top => MkTop top.modules imported modns EmptyMap freshMC top.verbose top.errors ops)
   log 1 $ \ _ => "process Decls"
   traverse (tryProcessDecl ns) (collectDecl decls)
 
   -- update modules with result, leave the rest of context in case this is top file
-  top <- get
+  top <- getTop
   mc <- readIORef top.metaCtx
 
   let mod = MkModCtx top.defs mc top.ops
@@ -140,7 +140,7 @@ processModule importFC base stk qn@(QN ns nm) = do
 
   let modules = updateMap modns mod top.modules
   freshMC <- newIORef (MC EmptyMap 0 CheckAll)
-  modify (\ top => MkTop modules top.imported top.ns top.defs top.metaCtx top.verbose top.errors top.ops)
+  modifyTop (\ top => MkTop modules top.imported top.ns top.defs top.metaCtx top.verbose top.errors top.ops)
 
   (Nil) <- liftIO {M} $ readIORef top.errors
     | errors => do
@@ -165,7 +165,7 @@ baseDir Lin _ = Left "module path doesn't match directory"
 
 showErrors : String -> String -> M Unit
 showErrors fn src = do
-  top <- get
+  top <- getTop
   (Nil) <- liftIO {M} $ readIORef top.errors
     | errors => do
         for_ errors $ \err =>
@@ -201,12 +201,12 @@ processFile fn = do
   processDecl primNS (PType emptyFC "String" Nothing)
   processDecl primNS (PType emptyFC "Char" Nothing)
 
-  top <- get
+  top <- getTop
   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)
+  modifyTop (\ top => MkTop modules (primNS :: Nil) Nil EmptyMap top.metaCtx top.verbose top.errors top.ops)
 
   src <- processModule emptyFC base Nil qn
-  top <- get
+  top <- getTop
 
   showErrors fn src
   pure MkUnit
@@ -216,7 +216,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.modules top.imported top.ns top.defs top.metaCtx (top.verbose + 1) top.errors top.ops)
+  modifyTop (\ top => MkTop top.modules top.imported top.ns top.defs top.metaCtx (top.verbose + 1) top.errors top.ops)
   cmdLine args
 cmdLine ("-o" :: fn :: args) = do
   (out, files) <- cmdLine args

src/Lib/Syntax.idr

@@ -2,7 +2,6 @@ module Lib.Syntax
 
 import Data.String
 import Data.Maybe
-import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.Types