diff --git a/Makefile b/Makefile index 91e4a1e..445e361 100644 --- a/Makefile +++ b/Makefile @@ -21,8 +21,10 @@ newt3.js: newt2.js time $(RUNJS) newt2.js src/Main.newt -o newt3.js cmp newt2.js newt3.js -min.js: newt3.js +min.js: newt3.js scripts/pack scripts/pack + gzip -kf min.js + ls -l min.js min.js.gz test: newt.js scripts/test diff --git a/TODO.md b/TODO.md index 1735503..c2e9d27 100644 --- a/TODO.md +++ b/TODO.md @@ -2,6 +2,12 @@ ## TODO - [ ] Remove erased args from primitive functions +- [ ] consider moving primitive functions to a support file + - Downside here is that we lose some dead code elimination, but it better supports bootstrapping when calling convention changes. +- [ ] allow declaration of primitive operators + - Removes assumptions of hack in Compile.newt, but might not support other backends + - Alternate solution would be to pull from Prelude and hard code for all backends + - 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 diff --git a/scripts/pack b/scripts/pack new file mode 100755 index 0000000..a8bf3b3 --- /dev/null +++ b/scripts/pack @@ -0,0 +1,7 @@ +#!/bin/sh +( + echo '(function(){' + cat newt3.js + echo '})()' +) > iife.js +esbuild --minify iife.js > min.js diff --git a/src/Lib/LiftWhere.newt b/src/Lib/LiftWhere.newt index f4d8b6b..585410c 100644 --- a/src/Lib/LiftWhere.newt +++ b/src/Lib/LiftWhere.newt @@ -8,22 +8,23 @@ import Lib.Ref2 import Data.SortedMap import Data.IORef --- track depth and whether we need to replace Bnd with a top level call +-- track quantity, depth, and whether we need to replace Bnd with a top level call. +-- We _could_ keep track of the support and elide that as well. LiftEnv : U -LiftEnv = List (Maybe (QName × Nat)) +LiftEnv = List (Quant × Maybe (QName × List Quant)) liftWhereTm : {{Ref2 Defs St}} → QName → LiftEnv → Tm → M Tm liftWhereTm name env (Lam fc nm icit quant t) = - Lam fc nm icit quant <$> liftWhereTm name (Nothing :: env) t + Lam fc nm icit quant <$> liftWhereTm name ((quant, Nothing) :: env) t liftWhereTm name env (App fc t u) = App fc <$> liftWhereTm name env t <*> liftWhereTm name env u liftWhereTm name env (Pi fc nm icit quant t u) = do t <- liftWhereTm name env t - u <- liftWhereTm name (Nothing :: env) u + u <- liftWhereTm name ((quant, Nothing) :: env) u pure $ Pi fc nm icit quant t u liftWhereTm name env (Let fc nm v sc) = do v <- liftWhereTm name env v - sc <- liftWhereTm name (Nothing :: env) sc + sc <- liftWhereTm name ((Many, Nothing) :: env) sc pure $ Let fc nm v sc liftWhereTm name env tm@(Case fc t alts) = do t <- liftWhereTm name env t @@ -35,16 +36,20 @@ liftWhereTm name env tm@(Case fc t alts) = do liftWhereAlt (CaseDefault tm) = CaseDefault <$> liftWhereTm name env tm liftWhereAlt (CaseLit l tm) = CaseLit l <$> liftWhereTm name env tm liftWhereAlt (CaseCons qn args tm) = - CaseCons qn args <$> liftWhereTm name (map (const Nothing) args ++ env) tm + -- TODO - can we pull quantities off of these arguments? + -- We should switch to SnocList first, the args are backwards here + CaseCons qn args <$> liftWhereTm name ((map (const (Many, Nothing)) args) ++ env) tm -- This is where the magic happens liftWhereTm name env (LetRec fc nm ty t u) = do - let l = length env + -- let l = length env qn <- getName name nm - let env' = (Just (qn, S l) :: env) + -- I'll erase this one, since we're replacing all of the usages + let qs = Zero :: map fst env + let env' = ((Zero, Just (qn, qs)) :: env) -- environment should subst this function (see next case) t' <- liftWhereTm qn env' t -- TODO we could have subst in this var and dropped the extra argument - modifyRef Defs (updateMap qn (Fn $ wrapLam (S l) t')) + modifyRef Defs (updateMap qn (Fn $ wrapLam qs t')) -- The rest u' <- liftWhereTm qn env' u @@ -58,19 +63,18 @@ liftWhereTm name env (LetRec fc nm ty t u) = do let (Just _) = lookupMap qn' top | _ => pure qn' getName qn (ext ++ "'") - wrapLam : Nat → Tm → Tm - wrapLam Z tm = tm - -- REVIEW We've already erased, hopefully we don't need quantity - wrapLam (S k) tm = Lam fc "_" Explicit Many $ wrapLam k tm + wrapLam : List Quant → Tm → Tm + wrapLam Nil tm = tm + wrapLam (q :: qs) tm = wrapLam qs $ Lam fc "_" Explicit q tm -- And where it lands liftWhereTm name env tm@(Bnd fc k) = case getAt (cast k) env of - Just (Just (qn, v)) => pure $ apply (length' env) (cast v) (Ref fc qn) + Just (_, Just (qn, v)) => pure $ apply (length' env) (length' v) (Ref fc qn) _ => pure tm where apply : Int → Int → Tm → Tm apply l 0 tm = tm - -- (l - k) is like lvl2ix, but witih k one bigger + -- (l - k) is like lvl2ix, but with k one bigger apply l k tm = App fc (apply l (k - 1) tm) (Bnd fc (l - k)) liftWhereTm name env tm = pure tm @@ -78,7 +82,6 @@ liftWhereFn : {{Ref2 Defs St}} → QName × Def → M Unit liftWhereFn (name, Fn tm) = do tm' <- liftWhereTm name Nil tm modifyRef Defs $ updateMap name (Fn tm') - -- updateDef name fc type (Fn tm') liftWhereFn _ = pure MkUnit liftWhere : {{Ref2 Defs St}} → M Unit