diff --git a/.gitignore b/.gitignore index 80b1e7e..9aee438 100644 --- a/.gitignore +++ b/.gitignore @@ -6,7 +6,7 @@ build/ *.bak *.agda *.agdai -/*.js +/newt*.js input.txt node_modules mkday.py diff --git a/Makefile b/Makefile index 337dca9..a91089f 100644 --- a/Makefile +++ b/Makefile @@ -29,7 +29,7 @@ newt.so: newt.ss prim.ss chez --script scripts/compile-chez.ss newt2.ss: newt.so - chez --program newt.ss src/Main.newt -o newt2.ss + time chez --program newt.so src/Main.newt -o newt2.ss test: newt.js scripts/test diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 46fb3df..b32fb41 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -138,7 +138,6 @@ findMatches ctx ty ((name, type) :: xs) = do debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}" -- This check is solving metas, so we save mc below in case we want this solution let (QN ns nm) = name - let (cod, tele) = splitTele type setMetaMode CheckFirst tm <- check ctx (RVar fc nm) ty debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}" @@ -344,19 +343,9 @@ rename meta ren lvl (VPi fc n icit rig ty tm) = do pure (Pi fc n icit rig ty' scope') rename meta ren lvl (VU fc) = pure (UU fc) rename meta ren lvl (VErased fc) = pure (Erased fc) --- for now, we don't do solutions with case in them. -rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution" -rename meta ren lvl (VLit fc lit) = pure (Lit fc lit) -rename meta ren lvl (VLet fc name val body) = do - val' <- rename meta ren lvl val - body' <- rename meta (lvl :: ren) (1 + lvl) body - pure $ Let fc name val' body' --- these probably shouldn't show up in solutions... -rename meta ren lvl (VLetRec fc name ty val body) = do - ty' <- rename meta ren lvl ty - val' <- rename meta (lvl :: ren) (1 + lvl) val - body' <- rename meta (lvl :: ren) (1 + lvl) body - pure $ LetRec fc name ty' val' body' +-- for now, we don't do solutions with case, let, letrec in them +-- If we we need this, follow the model of VLam +rename meta ren lvl tm = error (getFC tm) "Unhandled term in `rename`: \{show tm}" lams : Nat -> List String -> Tm -> Tm lams Z _ tm = tm @@ -749,7 +738,6 @@ substVal k v tm = go tm where go : Val -> Val go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp)) - go (VLet fc nm a b) = VLet fc nm (go a) b go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b go (VMeta fc ix sp) = VMeta fc ix (map go sp) go (VRef fc nm sp) = VRef fc nm (map go sp) diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt index fa2e08f..f94a272 100644 --- a/src/Lib/Eval.newt +++ b/src/Lib/Eval.newt @@ -9,6 +9,7 @@ import Lib.TopContext import Data.IORef import Data.SnocList import Data.SortedMap +import Lib.Error eval : Env -> Tm -> M Val @@ -27,6 +28,7 @@ vapp (VLam _ _ _ _ t) u = t $$ u vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u) vapp (VRef fc nm sp) u = pure $ VRef fc nm (sp :< u) vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u) +-- not really impossible, could be a stuck VCase. vapp t u = error' "impossible in vapp \{show t} to \{show u}\n" vappSpine : Val -> SnocList Val -> M Val @@ -69,8 +71,9 @@ tryEval env (VRef fc k sp) = do vtm <- eval env tm debug $ \ _ => "tm is \{render 90 $ pprint Nil tm}" val <- vappSpine vtm sp + -- These are considered "stuck" and we back out to the nearest name application case val of - VCase _ _ _ => pure Nothing + VCase _ _ _ _ => pure Nothing VLam _ _ _ _ _ => pure Nothing -- For now? There is a spot in Compile.newt that has -- two applications of fresh that is getting unfolded even @@ -78,7 +81,7 @@ tryEval env (VRef fc k sp) = do -- coming out of a let and is instantly applied VLetRec _ _ _ _ _ => pure Nothing v => pure $ Just v) - (\ _ => pure Nothing) + (const $ pure Nothing) _ => do debug $ \ _ => "tryEval blocked on undefined \{show k}" pure Nothing @@ -98,7 +101,7 @@ forceType env x = do | _ => pure x forceType env x' --- for cases applied to a value +-- Handles cases applied to a value, return Nothing if stuck -- TODO this does not handle CaseLit evalCase : Env -> Val -> List CaseAlt -> M (Maybe Val) evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do @@ -112,40 +115,19 @@ evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do -- bail for a stuck function _ => pure Nothing where + -- put constructor args into scope pushArgs : Env -> List Val -> List String -> M (Maybe Val) pushArgs env (arg :: args) (nm :: nms) = pushArgs (arg :: env) args nms - pushArgs env args Nil = do - t' <- eval env t - Just <$> vappSpine t' (Lin <>< args) + pushArgs env Nil Nil = Just <$> eval env t + pushArgs env args Nil = fatalError "Extra args \{show args}" pushArgs env Nil rest = pure Nothing --- REVIEW - this is handled in the caller already -evalCase env sc@(VVar fc k sp) alts = case lookupVar env k of - Just tt@(VVar fc' k' sp') => do - debug $ \ _ => "lookup \{show k} is \{show tt}" - if k' == k - then pure Nothing - else do - val <- vappSpine (VVar fc' k' sp') sp - evalCase env val alts - Just t => do - val <- vappSpine t sp - evalCase env val alts - Nothing => do - debug $ \ _ => "lookup \{show k} is Nothing in env \{show env}" - pure Nothing + evalCase env sc (CaseDefault u :: xs) = Just <$> eval env u evalCase env sc cc = do debug $ \ _ => "CASE BAIL sc \{show sc} vs " -- \{show cc}" debug $ \ _ => "env is \{show env}" pure Nothing --- neutral alts -evalAlt : Env → CaseAlt → M VCaseAlt -evalAlt env (CaseDefault tm) = VCaseDefault <$> eval env tm -evalAlt env (CaseLit lit tm) = VCaseLit lit <$> eval env tm --- in the cons case, we're binding args -evalAlt env (CaseCons nm args tm) = pure $ VCaseCons nm args env tm - -- So smalltt says: -- Smalltt has the following approach: -- - Top-level and local definitions are lazy. @@ -173,13 +155,19 @@ eval env (Pi fc x icit rig a b) = do pure $ VPi fc x icit rig a' (MkClosure env b) eval env (Let fc nm t u) = do t' <- eval env t - u' <- eval (VVar fc (length' env) Lin :: env) u - pure $ VLet fc nm t' u' + -- + if True + then pure $ VLet fc nm t' (MkClosure env u) + else eval (t' :: env) u eval env (LetRec fc nm ty t u) = do - ty' <- eval env ty - t' <- eval (VVar fc (length' env) Lin :: env) t - u' <- eval (VVar fc (length' env) Lin :: env) u - pure $ VLetRec fc nm ty' t' u' + -- Used for `where`, we'd probably need to treat this like Lam. + error fc "eval letrec" + -- I think we need to handle this like lam/let, disabled for now. + -- It should be gone by the time we hit inlining, we'll see if it arises in other cases + -- ty' <- eval env ty + -- t' <- eval (VVar fc (length' env) Lin :: env) t + -- u' <- eval (VVar fc (length' env) Lin :: env) u + -- pure $ VLetRec fc nm ty' t' u' -- Here, we assume env has everything. We push levels onto it during type checking. -- I think we could pass in an l and assume everything outside env is free and -- translate to a level @@ -191,15 +179,13 @@ eval env (Lit fc lit) = pure $ VLit fc lit eval env tm@(Case fc sc alts) = do -- TODO we need to be able to tell eval to expand aggressively here. sc' <- eval env sc - sc' <- unlet env sc' -- try to expand lets from pattern matching - -- possibly too aggressive? + -- inline metas and do beta reduction at head sc' <- forceType env sc' Nothing <- evalCase env sc' alts | Just v => pure v vsc <- eval env sc - alts' <- traverse (evalAlt env) alts - pure $ VCase fc vsc alts' + pure $ VCase fc vsc env alts quote : (lvl : Int) -> Val -> M Tm @@ -210,10 +196,14 @@ quoteSp lvl t (xs :< x) = do x' <- quote lvl x pure $ App emptyFC t' x' -quoteAlt : Int → VCaseAlt → M CaseAlt -quoteAlt l (VCaseDefault val) = CaseDefault <$> quote l val -quoteAlt l (VCaseLit lit val) = CaseLit lit <$> quote l val -quoteAlt l (VCaseCons nm args env tm) = do +normAlt : Env → Int → CaseAlt → M CaseAlt +normAlt env l (CaseDefault tm) = do + val <- eval env tm + CaseDefault <$> quote l val +normAlt env l (CaseLit lit tm) = do + val <- eval env tm + CaseLit lit <$> quote l val +normAlt env l (CaseCons nm args tm) = do val <- eval (mkenv l env args) tm tm <- quote (length' args + l) val pure $ CaseCons nm args tm @@ -224,7 +214,7 @@ quoteAlt l (VCaseCons nm args env tm) = do quote l (VVar fc k sp) = if k < l then quoteSp l (Bnd fc (lvl2ix l k )) sp -- level to index - else error fc "Bad index in quote \{show k} depth \{show l}" + else error fc "Bad level in quote \{show k} depth \{show l}" quote l (VMeta fc i sp) = do meta <- lookupMeta i case meta of @@ -241,6 +231,7 @@ quote l (VPi fc x icit rig a b) = do pure $ Pi fc x icit rig a' tm quote l (VLet fc nm t u) = do t' <- quote l t + u <- u $$ VVar fc l Lin u' <- quote (1 + l) u pure $ Let fc nm t' u' quote l (VLetRec fc nm ty t u) = do @@ -250,10 +241,11 @@ quote l (VLetRec fc nm ty t u) = do pure $ LetRec fc nm ty' t' u' quote l (VU fc) = pure (UU fc) quote l (VRef fc n sp) = quoteSp l (Ref fc n) sp -quote l (VCase fc sc valts) = do +quote l (VCase fc sc env alts) = do sc' <- quote l sc - alts <- traverse (quoteAlt l) valts - pure $ Case fc sc' alts + alts' <- traverse (normAlt env l) alts + pure $ Case fc sc' alts' + quote l (VLit fc lit) = pure $ Lit fc lit quote l (VErased fc) = pure $ Erased fc @@ -268,7 +260,6 @@ prvalCtx {{ctx}} v = do tm <- quote ctx.lvl v pure $ render 90 $ pprint (map fst ctx.types) tm - -- 'zonk' is substituting metas _and_ doing inlining -- It is a flavor of eval, maybe we could combine them with some flags @@ -309,23 +300,37 @@ zonkApp top l env t@(Meta fc k) sp = do meta <- lookupMeta k case meta of (Solved _ j v) => do + debug $ \ _ => "zonk for \{show k} env \{show env}" + debug $ \ _ => "spine \{show sp}" sp' <- traverse (eval env) sp - debug $ \ _ => "zonk \{show k} -> \{show v} spine \{show sp'}" + debug $ \ _ => "zonk meta \{show k} -> \{show v} spine \{show sp'}" foo <- vappSpine v (Lin <>< sp') debug $ \ _ => "-> result is \{show foo}" - tweakFC fc <$> quote l foo + if length' env /= l + then fatalError "MM2 \{show l} /= \{show $ length' env}" + else pure MkUnit + res <- tweakFC fc <$> quote l foo + debug $ \ _ => "quoted \{show res}" + pure res _ => pure $ appSpine t sp zonkApp top l env t sp = do + debug $ \ _ => "zonk2 for \{show t} env \{show env}" + debug $ \ _ => "spine \{show sp}" t' <- zonk top l env t -- inlining let (Just tm) = inlineDef t' | _ => pure $ appSpine t' sp sp' <- traverse (eval env) sp vtm <- eval env tm catchError (do - foo <- vappSpine vtm (Lin <>< sp') - t' <- quote l foo - zonk top l env t') - (\_ => pure $ appSpine t' sp) + debug $ \ _ => "zonk will app \{show t'} @ \{show sp} ~> \{show vtm} @ \{show sp'}" + res <- vappSpine vtm (Lin <>< sp') + debug $ \_ => "result is \{show res}" + t' <- quote l res + x <- zonk top l env t' + pure x) + (\err => do + debug $ \_ => "result err \{showError "" err}" + pure $ appSpine t' sp) where -- lookup name and return Def if flagged inline inlineDef : Tm → Maybe Tm diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index be674ae..d8ff3e8 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -310,6 +310,7 @@ processInstance ns instfc ty decls = do vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty | x => error (getFC x) "dcty not Pi" debug $ \ _ => "dcty \{render 90 $ pprint Nil dcty}" + -- let (_,args) = funArgs codomain debug $ \ _ => "traverse \{show $ map show args}" -- This is a little painful because we're reverse engineering the @@ -546,9 +547,6 @@ processRecord ns recordFC (nameFC, nm) tele cname decls = do processFields : Raw → Raw → List (String × Raw) → List (FC × String × Raw) → M Unit processFields _ _ _ Nil = pure MkUnit processFields autoPat tail deps ((fc,name,ty) :: rest) = do - -- TODO dependency isn't handled yet - -- we'll need to replace stuff like `len` with `len self`. - let funType = substRaw deps $ teleToPi (impTele tele) $ RPi fc (BI fc "$self" Explicit Many) tail ty -- `.fieldName` diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index d3b6d37..19ded78 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -23,7 +23,10 @@ derive Show BD data Quant = Zero | Many derive Eq Quant -derive Show Quant + +instance Show Quant where + show Zero = "0 " + show Many = "" -- We could make this polymorphic and use for environment... @@ -169,20 +172,15 @@ Val : U Closure : U Env : U -data VCaseAlt : U where - -- Like a Closure, but with a lot of args - VCaseCons : (name : QName) -> (args : List String) -> Env -> Tm -> VCaseAlt - VCaseLit : Literal -> Val -> VCaseAlt - VCaseDefault : Val -> VCaseAlt - data Val : U where VVar : FC -> (k : Int) -> (sp : SnocList Val) -> Val VRef : FC -> (nm : QName) -> (sp : SnocList Val) -> Val - VCase : FC -> (sc : Val) -> List VCaseAlt -> Val + VCase : FC -> (sc : Val) -> Env -> List CaseAlt -> Val VMeta : FC -> QName -> (sp : SnocList Val) -> Val VLam : FC -> Name -> Icit -> Quant -> Closure -> Val VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val - VLet : FC -> Name -> Val -> Val -> Val + -- not substing let, like idris + VLet : FC -> Name -> Val -> Closure -> Val VLetRec : FC -> Name -> Val -> Val -> Val -> Val VU : FC -> Val VErased : FC -> Val @@ -196,7 +194,7 @@ data Closure = MkClosure Env Tm getValFC : Val -> FC getValFC (VVar fc _ _) = fc getValFC (VRef fc _ _) = fc -getValFC (VCase fc _ _) = fc +getValFC (VCase fc _ _ _) = fc getValFC (VMeta fc _ _) = fc getValFC (VLam fc _ _ _ _) = fc getValFC (VPi fc _ _ _ a b) = fc @@ -220,15 +218,10 @@ instance Show Val where show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{showClosure y})" show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{showClosure y})" show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show x}}}. \{showClosure y})" - show (VCase fc sc alts) = "(%case \{show sc} \{unwords $ map showAlt alts})" - where - showAlt : VCaseAlt → String - showAlt (VCaseDefault v) = "(%cdef \{show v})" - showAlt (VCaseLit lit v) = "(%clit \{show v})" - showAlt (VCaseCons nm args env v) = "(%ccon \{show nm} \{unwords $ map show args} [\{show $ length env} env] \{show v}" + show (VCase fc sc env alts) = "(%case \{show sc} \{unwords $ map show alts})" show (VU _) = "U" show (VLit _ lit) = show lit - show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}" + show (VLet _ nm a (MkClosure env b)) = "(%let \{show nm} = \{show a} in \{show b}" show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}" show (VErased _) = "ERASED" @@ -269,7 +262,10 @@ record MetaContext where derive Eq MetaMode -data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon | TrueCon | FalseCon | NilCon | ConsCon +data ConInfo = NormalCon + | SuccCon | ZeroCon + | EnumCon | TrueCon | FalseCon + | NilCon | ConsCon derive Eq ConInfo