From f006fa875d2d7408ca2a9a638cde75e2422e8aa0 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 31 Mar 2025 21:21:37 -0700 Subject: [PATCH] Classify constructors, only dump modules if they successfully compile --- Makefile | 3 ++ TODO.md | 33 ++++++++++++----- newt-vscode/syntaxes/newt.tmLanguage.json | 13 ++++--- src/Lib/CompileExp.newt | 14 ++++---- src/Lib/Elab.newt | 6 ++-- src/Lib/Eval.newt | 2 +- src/Lib/ProcessDecl.newt | 44 ++++++++++++++++++----- src/Lib/Types.newt | 12 +++++-- src/Main.newt | 3 +- 9 files changed, 94 insertions(+), 36 deletions(-) diff --git a/Makefile b/Makefile index 91ef200..6658ad6 100644 --- a/Makefile +++ b/Makefile @@ -16,6 +16,7 @@ build/exec/newt: ${OSRCS} idris2 --build newt.ipkg build/exec/newt.js: ${OSRCS} + rm build/* idris2 --cg node -o newt.js -p contrib -c orig/Main.idr build/exec/newt.min.js: ${OSRCS} @@ -33,9 +34,11 @@ newt.js: ${SRCS} $(RUNJS) bootstrap/newt.js src/Main.newt -o newt.js newt2.js: newt.js + rm build/* $(RUNJS) newt.js src/Main.newt -o newt2.js newt3.js: newt2.js + rm -f build/* $(RUNJS) newt2.js src/Main.newt -o newt3.js cmp newt2.js newt3.js diff --git a/TODO.md b/TODO.md index 855dbb7..8244707 100644 --- a/TODO.md +++ b/TODO.md @@ -3,29 +3,44 @@ Syntax -> Parser.Impl ? -- [ ] implement tail call optimization +- [x] fix string highlighting +- [x] implement tail call optimization +- [ ] implement magic nat (need primitive `+`, '-', and `==` in `CompileExp`) +- [ ] drop erased args on types and top level functions +- [ ] can I do some inlining without blowing up code size? +- [ ] implement string enum (or number, but I'm using strings for tags at the moment) +- [ ] use monaco input method instead of lean's - [ ] `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. + - Two issues + - I'm rewriting stuff in the context, leaving it in a bad state (forward references). I think I can avoid this. + - The variables at the end of pattern matching have types with references in the wrong order. I think we can reorder them on dependencies. +- Improve `auto` + - [ ] Improve cases where the auto isn't solved because of a type error + - [ ] Handle `Foo Blah`, `Foo a => Bar a` vs `Bar Blah` +- [ ] Add some optimizations + - [ ] see if we can make the typeclass stuff a little leaner, e.g. inline a projection of a static record. + - It would be nice if IO looked like imperative JS, but that might be a bit of a stretch. -- [ ] rename for top level functions (and maybe stuff in scope, probably need LSP first) +- [ ] LSP and/or more editor support + - [ ] Probably need ranges for FC + - [ ] leave an interactive process running + - [ ] collect metadata or run through the serialization data + - [ ] rename in editor 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 +- [x] save/load results of processing a module - [x] keep each module separate in context - [x] search would include imported modules, collect ops into and from modules - [x] serialize modules - - [ ] deserialize modules if up to date - - should I allow the idris cross module assignment hack? - - >>> sort out metas (maybe push them up to the main list) + - [x] deserialize modules if up to date + - We use a hash of the source and all of its import hashes to check - eventually we may want to support resuming halfway through a file - [x] get port to run - [x] something goes terribly wrong with traverse_ and for_ (related to erasure, I think) -- [ ] sort through issues that came up during port - [x] ~~don't use `take` - it's not stack safe~~ The newt version is stack safe -- [ ] move idris version into a bootstrap directory - - (Need Idris/chez or newt-in-newt to bootstrap!) More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff. diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index c6bcac6..730a8d7 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -24,13 +24,16 @@ "end": "`", "patterns": [{ "include": "source.js" }] }, - { - "name": "string.single.newt", - "match": "'(.|\\\\.)'" - }, { "name": "string.double.newt", - "match": "\"(.|\\\\.)\"" + "begin": "\"", + "end": "\"", + "patterns": [ + { + "name": "constant.character.escape.newt", + "match": "\\\\[^{]" + } + ] } ] } diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 1b8530e..9e06e5f 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -62,7 +62,7 @@ arityForName fc nm = do Nothing => error fc "Name \{show nm} not in scope" (Just Axiom) => pure Z (Just (TCon arity strs)) => pure $ cast arity - (Just (DCon k str)) => pure $ cast k + (Just (DCon _ k str)) => pure $ cast k (Just (Fn t)) => pure $ lamArity t (Just (PrimTCon arity)) => pure $ cast arity (Just (PrimFn t arity used)) => pure arity @@ -148,17 +148,17 @@ compileFun tm = go tm Lin go tm args = CFun (args <>> Nil) <$> compileTerm tm -- What are the Defs used for above? (Arity for name) -compileDCon : QName → Int → CExp -compileDCon (QN _ nm) 0 = CConstr nm Nil -compileDCon (QN _ nm) arity = +compileDCon : QName → ConInfo → Int → CExp +compileDCon (QN _ nm) info 0 = CConstr nm Nil +compileDCon (QN _ nm) info arity = let args = map (\k => "h\{show k}") (range 0 arity) in CFun args $ CConstr nm $ map (\k => CBnd $ arity - k - 1) (range 0 arity) -- probably want to drop the Ref2 when we can defToCExp : {{Ref2 Defs St}} → (QName × Def) -> M (QName × CExp) defToCExp (qn, Axiom) = pure $ (qn, CErased) -defToCExp (qn, DCon arity _) = pure $ (qn, compileDCon qn arity) -defToCExp (qn, TCon arity _) = pure $ (qn, compileDCon qn arity) -defToCExp (qn, PrimTCon arity) = pure $ (qn, compileDCon qn arity) +defToCExp (qn, DCon info arity _) = pure $ (qn, compileDCon qn info arity) +defToCExp (qn, TCon arity _) = pure $ (qn, compileDCon qn NormalCon arity) +defToCExp (qn, PrimTCon arity) = pure $ (qn, compileDCon qn NormalCon arity) defToCExp (qn, PrimFn src _ deps) = pure $ (qn, CRaw src deps) defToCExp (qn, Fn tm) = (_,_ qn) <$> compileFun tm diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 2a37373..63fcc3d 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -694,7 +694,7 @@ getConstructors ctx scfc (VRef fc nm _) = do lookupDCon nm = do top <- getTop case lookup nm top of - (Just (MkEntry _ name type (DCon k str))) => pure (name, k, type) + (Just (MkEntry _ name type (DCon _ k str))) => pure (name, k, type) Just _ => error fc "Internal Error: \{show nm} is not a DCon" Nothing => error fc "Internal Error: DCon \{show nm} not found" getConstructors ctx scfc tm = do @@ -946,7 +946,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do -- TODO can we check this when we make the PatCon? top <- getTop case lookup nm top of - (Just (MkEntry _ name type (DCon k tcname))) => + (Just (MkEntry _ name type (DCon _ k tcname))) => if (tcname /= sctynm) then error fc "Constructor is \{show tcname} expected \{show sctynm}" else pure Nothing @@ -974,7 +974,7 @@ mkPat (tm, icit) = do top <- getTop case splitArgs tm Nil of ((RVar fc nm), b) => case lookupRaw nm top of - (Just (MkEntry _ name type (DCon k str))) => do + (Just (MkEntry _ name type (DCon _ k str))) => do -- TODO check arity, also figure out why we need reverse bpat <- traverse (mkPat) b pure $ PatCon fc icit name bpat Nothing diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt index 87b8472..3a8e50b 100644 --- a/src/Lib/Eval.newt +++ b/src/Lib/Eval.newt @@ -112,7 +112,7 @@ evalCase env mode sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do debug $ \ _ => "ECase \{show nm} \{show sp} \{show nms} \{showTm t}" go env (sp <>> Nil) nms else case lookup nm top of - (Just (MkEntry _ str type (DCon k str1))) => evalCase env mode sc xs + (Just (MkEntry _ str type (DCon _ k str1))) => evalCase env mode sc xs -- bail for a stuck function _ => pure Nothing where diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 6435532..d992c8e 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -274,7 +274,7 @@ processInstance ns instfc ty decls = do | _ => error tyFC "\{show tconName} is not a type constructor" let (con :: Nil) = cons | _ => error tyFC "\{show tconName} has multiple constructors \{show cons}" - let (Just (MkEntry _ _ dcty (DCon _ _))) = lookup con top + let (Just (MkEntry _ _ dcty (DCon _ _ _))) = lookup con top | _ => error tyFC "can't find constructor \{show con}" vdcty@(VPi _ nm icit rig a b) <- eval Nil CBN dcty | x => error (getFC x) "dcty not Pi" @@ -377,6 +377,32 @@ processShortData ns fc lhs sigs = do mkDecl args acc (RApp fc' t u icit) = mkDecl args (u :: acc) t mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}" +-- Identify Nat-like, enum-like, etc +populateConInfo : List TopEntry → List TopEntry +populateConInfo entries = + let (Nothing) = traverse checkEnum entries + | Just entries => entries in + let (a :: b :: Nil) = entries | _ => entries in + let (Just succ) = find isSucc entries | _ => entries in + let (Just zero) = find isZero entries | _ => entries in + setInfo zero ZeroCon :: setInfo succ SuccCon :: Nil + where + setInfo : TopEntry → ConInfo → TopEntry + setInfo (MkEntry fc nm dty (DCon _ arity hn)) info = MkEntry fc nm dty (DCon info arity hn) + setInfo x _ = x + + checkEnum : TopEntry → Maybe TopEntry + checkEnum (MkEntry fc nm dty (DCon _ 0 hn)) = Just $ MkEntry fc nm dty (DCon EnumCon 0 hn) + checkEnum _ = Nothing + + isZero : TopEntry → Bool + isZero (MkEntry fc nm dty (DCon _ 0 hn)) = True + isZero _ = False + + -- TODO - handle indexes, etc + isSucc : TopEntry → Bool + isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ 1 hn)) = a == b + isSucc _ = False processData : List String → FC → String → Raw → List Decl → M Unit processData ns fc nm ty cons = do @@ -392,7 +418,7 @@ processData ns fc nm ty cons = do unifyCatch fc (mkCtx fc) tyty' type' Just (MkEntry _ name type _) => error fc "\{show nm} already declared" Nothing => setDef (QN ns nm) fc tyty Axiom - cnames <- for cons $ \x => case x of + entries <- join <$> (for cons $ \x => case x of (TypeSig fc names tm) => do debug $ \ _ => "check dcon \{show names} \{show tm}" dty <- check (mkCtx fc) tm (VU fc) @@ -407,15 +433,17 @@ processData ns fc nm ty cons = do | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}" when (hn /= QN ns nm) $ \ _ => error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}" + pure $ map (\ nm' => (MkEntry fc (QN ns nm') dty (DCon NormalCon (getArity dty) hn))) names + decl => throwError $ E (getFC decl) "expected constructor declaration") + for entries $ \case (MkEntry name fc dty def) => setDef fc name dty def + let entries = populateConInfo entries + let cnames = map (\x => x.name) entries - for names $ \ nm' => do - setDef (QN ns nm') fc dty (DCon (getArity dty) hn) - pure $ map (QN ns) names - decl => throwError $ E (getFC decl) "expected constructor declaration" - log 1 $ \ _ => "setDef \{nm} TCon \{show $ join cnames}" + log 1 $ \ _ => "setDef \{nm} TCon \{show cnames}" let arity = cast $ piArity tyty - updateDef (QN ns nm) fc tyty (TCon arity (join cnames)) + updateDef (QN ns nm) fc tyty (TCon arity cnames) where + binderName : Binder → Name binderName (MkBinder _ nm _ _ _) = nm diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index a23038a..23d23df 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -307,13 +307,21 @@ record MetaContext where next : Int mcmode : MetaMode -data Def = Axiom | TCon Int (List QName) | DCon Int QName | Fn Tm | PrimTCon Int +data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon + +instance Show ConInfo where + show NormalCon = "" + show SuccCon = "[S]" + show ZeroCon = "[Z]" + show EnumCon = "[E]" + +data Def = Axiom | TCon Int (List QName) | DCon ConInfo Int QName | Fn Tm | PrimTCon Int | PrimFn String Nat (List QName) instance Show Def where show Axiom = "axiom" show (TCon _ strs) = "TCon \{show strs}" - show (DCon k tyname) = "DCon \{show k} \{show tyname}" + show (DCon ci k tyname) = "DCon \{show k} \{show tyname} \{show ci}" show (Fn t) = "Fn \{show t}" show (PrimTCon _) = "PrimTCon" show (PrimFn src arity used) = "PrimFn \{show src} \{show arity} \{show used}" diff --git a/src/Main.newt b/src/Main.newt index ad115de..3e2351a 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -161,7 +161,8 @@ processModule importFC base stk qn@(QN ns nm) = do mc <- readIORef top.metaCtx let mod = MkModCtx csum top.defs mc top.ops - if stk == Nil then pure MkUnit else dumpModule qn src mod + errors <- liftIO {M} $ readIORef top.errors + if stk == Nil || length' errors == 0 then pure MkUnit else dumpModule qn src mod let modules = updateMap modns mod top.modules modifyTop (\ top => MkTop modules top.imported top.ns top.defs top.metaCtx top.verbose top.errors top.ops)