diff --git a/Makefile b/Makefile index 445e361..3d98689 100644 --- a/Makefile +++ b/Makefile @@ -44,3 +44,6 @@ profile: .PHONY rm isolate* build/*; node --prof newt.js -o newt2.js src/Main.newt node --prof-process isolate* > profile.txt +clean: + rm newt*.js iife.js min.js min.js.gz + diff --git a/TODO.md b/TODO.md index 2f6fcd5..fa1d6dc 100644 --- a/TODO.md +++ b/TODO.md @@ -10,12 +10,13 @@ - POper added to physical syntax types, but not implemented - [x] Remove erased fields from constructor data - [ ] Teach magic nat / magic enum about erased args -- [ ] Update LiftLambda.newt for arg removal changes +- [x] Update LiftLambda.newt for arg removal changes - [ ] Add error for non-linear names in pattern matching (currently it picks one) - We probably should handle forced values. Idris requires them to have the same name. - [ ] Functions with erased-only arguments still get called with `()` - do we want this or should they be constants? - [x] Take the parens off of FC to make vscode happy - [x] Magic to make Bool a boolean +- [ ] Lifted closures could elide unused arguments (LiftWhere / LiftLambda) - [ ] Look into using holes for errors (https://types.pl/@AndrasKovacs/115401455046442009) - This would let us hit more cases in a function when we hit an error. - I've been wanting to try holes for parse errors too. diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt index 0880d7b..eded0ca 100644 --- a/src/Lib/Compile.newt +++ b/src/Lib/Compile.newt @@ -11,7 +11,7 @@ import Lib.Prettier import Lib.CompileExp import Lib.TopContext import Lib.LiftWhere --- import Lib.LiftLambda -- NOW needs update for arg erasure +import Lib.LiftLambda import Lib.TCO import Lib.Ref2 import Lib.Erasure diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 24e1b55..5e1d100 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -119,7 +119,6 @@ compileTerm t@(Ref fc nm@(QN _ tag)) = do arity <- arityForName fc nm defs <- getRef Defs case arity of - -- we don't need to curry functions that take one argument Nil => case the (Maybe Def) $ lookupMap' nm defs of Just (DCon ix EnumCon _ _) => pure $ CLit $ LInt $ cast ix diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 9ac100f..3a22776 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1186,9 +1186,7 @@ buildLitCases ctx prob fc scnm scty = do Nothing => True -- can this happen? _ => False --- TODO - figure out if these need to be in Prelude or have a special namespace --- If we lookupRaw "String", we could get different answers in different contexts. --- maybe Hardwire this one +-- Names of builtin primitive types, declared in Main.newt stringType intType charType boolType : QName stringType = QN primNS "String" intType = QN primNS "Int" diff --git a/src/Lib/LiftLambda.newt b/src/Lib/LiftLambda.newt index 2b32020..b300202 100644 --- a/src/Lib/LiftLambda.newt +++ b/src/Lib/LiftLambda.newt @@ -11,22 +11,22 @@ import Data.SnocList import Data.IORef import Monad.State - ExpMap : U ExpMap = SortedMap QName CExp -liftLambdaTm : QName → SnocList Name → CExp → State ExpMap CExp +liftLambdaTm : QName → SnocList (Quant × Name) → CExp → State ExpMap CExp -- CBnd liftLambdaTm name env (CFun nms t) = CFun nms <$> liftLambdaTm name (env <>< nms) t liftLambdaTm name env (CApp t u) = CApp <$> liftLambdaTm name env t <*> liftLambdaTm name env u liftLambdaTm name env (CLet nm v sc) = do v <- liftLambdaTm name env v - sc <- liftLambdaTm name (env :< nm) sc + sc <- liftLambdaTm name (env :< (Many, nm)) sc pure $ CLet nm v sc liftLambdaTm name env (CLetRec nm v sc) = do - v <- liftLambdaTm name (env :< nm) v - sc <- liftLambdaTm name (env :< nm) sc + -- references should be removed by liftWhere + v <- liftLambdaTm name (env :< (Zero, nm)) v + sc <- liftLambdaTm name (env :< (Zero, nm)) sc pure $ CLetRec nm v sc liftLambdaTm name env tm@(CCase t alts) = do @@ -39,14 +39,15 @@ liftLambdaTm name env tm@(CCase t alts) = do liftLambdaAlt (CDefAlt tm) = CDefAlt <$> liftLambdaTm name env tm liftLambdaAlt (CLitAlt l tm) = CLitAlt l <$> liftLambdaTm name env tm liftLambdaAlt (CConAlt ix nm info args tm) = - CConAlt ix nm info args <$> liftLambdaTm name (env <>< args) tm + CConAlt ix nm info args <$> liftLambdaTm name (env <>< map (_,_ Many) args) tm liftLambdaTm name@(QN ns nm) env tm@(CLam nm t) = do let (nms, t) = splitLam tm Lin t' <- liftLambdaTm name (env <>< nms) t + let env' = env <>> nms -- TODO - maybe a better name here? qn <- getName name "lifted" - modify $ updateMap qn (CFun (env <>> nms) t') - pure $ CAppRef qn (makeApp (snoclen env)) (length' nms) + modify $ updateMap qn (CFun env' t') + pure $ CAppRef qn (makeApp (snoclen env)) (map fst env') where getName : QName → String → State ExpMap QName getName qn@(QN ns nm) ext = do @@ -55,8 +56,8 @@ liftLambdaTm name@(QN ns nm) env tm@(CLam nm t) = do let (Just _) = lookupMap qn' top | _ => pure qn' getName qn (ext ++ "'") - splitLam : CExp → SnocList Name → List Name × CExp - splitLam (CLam nm t) acc = splitLam t (acc :< nm) + splitLam : CExp → SnocList (Quant × Name) → List (Quant × Name) × CExp + splitLam (CLam nm t) acc = splitLam t (acc :< (Many, nm)) splitLam t acc = (acc <>> Nil, t) wrapLam : Nat → CExp → CExp