From 5cce1a465e333dfb3cbff1c83a4f4a52a70f49b3 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 12 Jan 2025 08:57:01 -0800 Subject: [PATCH] Modules live in separate contexts, only imported modules are in scope --- TODO.md | 7 +++--- port/Lib/Common.newt | 1 + port/Lib/Compile.newt | 3 +++ port/Lib/CompileExp.newt | 2 ++ port/Lib/Elab.newt | 24 ++++++++++++------ port/Lib/Erasure.newt | 2 ++ port/Lib/Eval.newt | 3 +++ port/Lib/Parser.newt | 3 +++ port/Lib/Parser/Impl.newt | 1 + port/Lib/Prettier.newt | 2 +- port/Lib/ProcessDecl.newt | 4 +++ port/Lib/Syntax.newt | 2 ++ port/Lib/Tokenizer.newt | 2 +- port/Lib/TopContext.newt | 36 ++++++++++++++++++--------- port/Lib/Types.newt | 37 +++++++++++++++++++++++----- port/Lib/Util.newt | 2 ++ port/Main.newt | 52 +++++++++++++++++++++++++++++---------- src/Lib/Parser/Impl.idr | 2 ++ 18 files changed, 141 insertions(+), 44 deletions(-) diff --git a/TODO.md b/TODO.md index 6303a86..d68323d 100644 --- a/TODO.md +++ b/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 - - search would include imported modules, collect ops into and from modules - - should I allow the idris assignment hack? + - [x] keep each module separate in context + - [x] search would include imported modules, collect ops into and from modules + - 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 diff --git a/port/Lib/Common.newt b/port/Lib/Common.newt index a0ffc5b..3eba6d1 100644 --- a/port/Lib/Common.newt +++ b/port/Lib/Common.newt @@ -1,5 +1,6 @@ module Lib.Common +import Prelude import Data.String import Data.Int import Data.SortedMap diff --git a/port/Lib/Compile.newt b/port/Lib/Compile.newt index fa90232..2b4f83b 100644 --- a/port/Lib/Compile.newt +++ b/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 diff --git a/port/Lib/CompileExp.newt b/port/Lib/CompileExp.newt index af18403..f26f585 100644 --- a/port/Lib/CompileExp.newt +++ b/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 diff --git a/port/Lib/Elab.newt b/port/Lib/Elab.newt index 360477a..fe96af7 100644 --- a/port/Lib/Elab.newt +++ b/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 diff --git a/port/Lib/Erasure.newt b/port/Lib/Erasure.newt index be5fd06..d680b32 100644 --- a/port/Lib/Erasure.newt +++ b/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 diff --git a/port/Lib/Eval.newt b/port/Lib/Eval.newt index e4ccdf3..0e068ca 100644 --- a/port/Lib/Eval.newt +++ b/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 diff --git a/port/Lib/Parser.newt b/port/Lib/Parser.newt index c69de78..7dcddd5 100644 --- a/port/Lib/Parser.newt +++ b/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 diff --git a/port/Lib/Parser/Impl.newt b/port/Lib/Parser/Impl.newt index 7cbecee..42e428b 100644 --- a/port/Lib/Parser/Impl.newt +++ b/port/Lib/Parser/Impl.newt @@ -1,5 +1,6 @@ module Lib.Parser.Impl +import Prelude import Lib.Token import Lib.Common import Data.String diff --git a/port/Lib/Prettier.newt b/port/Lib/Prettier.newt index 6da0bb9..a95ce1d 100644 --- a/port/Lib/Prettier.newt +++ b/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 diff --git a/port/Lib/ProcessDecl.newt b/port/Lib/ProcessDecl.newt index e0a3b17..d7e0dae 100644 --- a/port/Lib/ProcessDecl.newt +++ b/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 diff --git a/port/Lib/Syntax.newt b/port/Lib/Syntax.newt index d8f2b8d..2af01b5 100644 --- a/port/Lib/Syntax.newt +++ b/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 diff --git a/port/Lib/Tokenizer.newt b/port/Lib/Tokenizer.newt index 78fe8d2..472908e 100644 --- a/port/Lib/Tokenizer.newt +++ b/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 diff --git a/port/Lib/TopContext.newt b/port/Lib/TopContext.newt index e738438..af94d64 100644 --- a/port/Lib/TopContext.newt +++ b/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 - --- Maybe pretty print? + go (ns :: nss) = case lookupMap' ns top.modules of + Nothing => go nss + 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 diff --git a/port/Lib/Types.newt b/port/Lib/Types.newt index ca40590..e6c7360 100644 --- a/port/Lib/Types.newt +++ b/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 - loaded : List String + -- what do we do here? we can accumulate for now, but we'll want to respect import 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 diff --git a/port/Lib/Util.newt b/port/Lib/Util.newt index ef99172..de4ebbf 100644 --- a/port/Lib/Util.newt +++ b/port/Lib/Util.newt @@ -1,5 +1,7 @@ module Lib.Util +import Prelude +import Lib.Common import Lib.Types import Data.List1 diff --git a/port/Main.newt b/port/Main.newt index 393e3c7..e707cb6 100644 --- a/port/Main.newt +++ b/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 (False) = elem name top.loaded | _ => pure "" - modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors (name :: top.loaded)top.ops) + 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) 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 - - (decls, ops) <- parseDecls fn top.ops toks Lin - modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors top.loaded ops) + 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) 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 ("Prim" :: Nil) (PType emptyFC "Char" Nothing) + + processDecl primNS (PType emptyFC "Int" 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 diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 87e8bfb..cac7c58 100644 --- a/src/Lib/Parser/Impl.idr +++ b/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