From 97c50a254a5dcdd99078cc3c3155bd813b271fff Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 2 Sep 2025 21:10:32 -0700 Subject: [PATCH] the "mode" argument to eval was unused and not fully propagated --- src/Lib/Elab.newt | 56 ++++++++++++------------- src/Lib/Eval.newt | 91 +++++++++++++++++----------------------- src/Lib/ProcessDecl.newt | 23 ++++------ src/Lib/Types.newt | 2 - 4 files changed, 75 insertions(+), 97 deletions(-) diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index b8e9960..7338c7a 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -183,13 +183,13 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do debug $ \ _ => "TRYAUTO solving \{show k} : \{show ty}" -- fill in solved metas in type x <- quote ctx.lvl ty - ty <- eval ctx.env CBN x + ty <- eval ctx.env x debug $ \ _ => "AUTO ---> \{show ty}" -- we want the context here too. top <- getTop Nil <- contextMatches ctx ty | ((tm, vty) :: Nil) => do - val <- eval ctx.env CBN tm + val <- eval ctx.env tm debug $ \ _ => "LOCAL SOLUTION \{rpprint Nil tm} evaled to \{show val}" let sp = makeSpine ctx.lvl ctx.bds solve ctx.env k sp val @@ -212,7 +212,7 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do pure False -- The `check` fills in implicits tm <- check ctx (RVar fc nm) ty - val <- eval ctx.env CBN tm + val <- eval ctx.env tm debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}" debug $ \ _ => "GLOBAL SOLUTION \{show val}" let sp = makeSpine ctx.lvl ctx.bds @@ -395,13 +395,13 @@ solve env m sp t = do ren <- invert l sp -- force unlet hack <- quote l t - t <- eval env CBN hack + t <- eval env hack catchError (do tm <- rename m ren l t let tm = lams (snoclen sp) (reverse ctx_.boundNames) tm top <- getTop - soln <- eval Nil CBN tm + soln <- eval Nil tm updateMeta m $ \case (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln @@ -507,7 +507,7 @@ unify env mode t u = do top <- getTop case lookup k' top of Just (MkEntry _ name ty (Fn tm) _) => do - vtm <- eval Nil CBN tm + vtm <- eval Nil tm appvtm <- vappSpine vtm sp' unify env mode t appvtm _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]\n env is \{show env}" @@ -517,7 +517,7 @@ unify env mode t u = do top <- getTop case lookup k top of Just (MkEntry _ name ty (Fn tm) _) => do - vtm <- eval Nil CBN tm + vtm <- eval Nil tm tmsp <- vappSpine vtm sp unify env mode tmsp u _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}\n env is \{show env}" @@ -639,14 +639,14 @@ insert ctx tm ty = do m <- freshMeta ctx (getFC tm) a AutoSolve debug $ \ _ => "INSERT Auto \{rpprint (names ctx) m} : \{show a}" debug $ \ _ => "TM \{rpprint (names ctx) tm}" - mv <- eval ctx.env CBN m + mv <- eval ctx.env m bapp <- b $$ mv insert ctx (App (getFC tm) tm m) bapp VPi fc x Implicit rig a b => do m <- freshMeta ctx (getFC tm) a Normal debug $ \ _ => "INSERT \{rpprint (names ctx) m} : \{show a}" debug $ \ _ => "TM \{rpprint (names ctx) tm}" - mv <- eval ctx.env CBN m + mv <- eval ctx.env m bapp <- b $$ mv insert ctx (App (getFC tm) tm m) bapp va => pure (tm, va) @@ -791,7 +791,7 @@ updateContext ctx ((k, val) :: cs) = checkCase : Context → Problem → String → Val → (QName × Int × Tm) → M Bool checkCase ctx prob scnm scty (dcName, arity, ty) = do - vty <- eval Nil CBN ty + vty <- eval Nil ty (ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin (Just res) <- catchError (Just <$> unify ctx'.env UPattern ty' scty) (\err => do @@ -813,7 +813,7 @@ checkCase ctx prob scnm scty (dcName, arity, ty) = do buildCase : Context -> Problem -> String -> Val -> (QName × Int × Tm) -> M (Maybe CaseAlt) buildCase ctx prob scnm scty (dcName, arity, ty) = do debug $ \ _ => "CASE \{scnm} match \{show dcName} ty \{rpprint (names ctx) ty}" - vty <- eval Nil CBN ty + vty <- eval Nil ty (ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin -- TODO I think we need to figure out what is dotted, maybe @@ -1031,7 +1031,7 @@ checkWhere ctx decls body ty = do -- REVIEW is this right, cribbed from my top level code top <- getTop clauses' <- traverse makeClause clauses - vty <- eval ctx.env CBN funTy + vty <- eval ctx.env funTy debug $ \ _ => "\{name} vty is \{show vty}" let ctx' = extend ctx name vty @@ -1041,7 +1041,7 @@ checkWhere ctx decls body ty = do -- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...) -- But I'll attempt letrec first tm <- buildTree (withPos ctx' defFC) (MkProb clauses' vty) - vtm <- eval ctx'.env CBN tm + vtm <- eval ctx'.env tm -- Should we run the rest with the definition in place? -- I'm wondering if switching from bind to define will mess with metas -- let ctx' = define ctx name vtm vty @@ -1059,11 +1059,11 @@ checkDone ctx Nil body ty = do env' <- for ctx.env $ \ val => do ty <- quote (length' ctx.env) val -- This is not getting vars under lambdas - eval ctx.env CBV ty + eval ctx.env ty types' <- for ctx.types $ \case (nm,ty) => do nty <- quote (length' env') ty - ty' <- eval env' CBV nty + ty' <- eval env' nty pure (nm, ty') let ctx = MkCtx ctx.lvl env' types' ctx.bds ctx.ctxFC debug $ \ _ => "AFTER" @@ -1073,7 +1073,7 @@ checkDone ctx Nil body ty = do -- The case eval code only works in the Tm -> Val case at the moment. -- we don't have anything like `vapp` for case ty <- quote (length' ctx.env) ty - ty <- eval ctx.env CBN ty + ty <- eval ctx.env ty debug $ \ _ => "check at \{show ty}" got <- check ctx body ty @@ -1428,9 +1428,9 @@ check ctx tm ty = do (RLet fc nm ty v sc, rty) => do ty' <- check ctx ty (VU emptyFC) - vty <- eval ctx.env CBN ty' + vty <- eval ctx.env ty' v' <- check ctx v vty - vv <- eval ctx.env CBN v' + vv <- eval ctx.env v' let ctx' = define ctx nm vv vty sc' <- check ctx' sc rty pure $ Let fc nm v' sc' @@ -1475,7 +1475,7 @@ check ctx tm ty = do infer ctx tm@(RUpdateRec fc _ _) = do error fc "I can't infer record updates" -- mvar <- freshMeta ctx fc (VU emptyFC) Normal - -- a <- eval ctx.env CBN mvar + -- a <- eval ctx.env mvar -- let ty = VPi fc ":ins" Explicit Many a (MkClosure ctx.env mvar) -- tm <- check ctx tm ty -- pure (tm, ty) @@ -1488,7 +1488,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types case lookupRaw nm top of Just (MkEntry _ name ty def _) => do debug $ \ _ => "lookup \{show name} as \{show def}" - vty <- eval Nil CBN ty + vty <- eval Nil ty pure (Ref fc name, vty) Nothing => error fc "\{show nm} not in scope" go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty) @@ -1518,40 +1518,40 @@ infer ctx (RApp fc t u icit) = do -- TODO test case to cover this. tty => do debug $ \ _ => "unify PI for \{show tty}" - a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN + a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal -- FIXME - I had to guess Many here. What are the side effects? unifyCatch fc ctx tty (VPi fc ":ins" icit Many a b) pure (a,b) u <- check ctx u a - u' <- eval ctx.env CBN u + u' <- eval ctx.env u bappu <- b $$ u' pure (App fc t u, bappu) infer ctx (RU fc) = pure (UU fc, VU fc) -- YOLO infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do ty' <- check ctx ty (VU fc) - vty' <- eval ctx.env CBN ty' + vty' <- eval ctx.env ty' ty2' <- check (extend ctx nm vty') ty2 (VU fc) pure (Pi fc nm icit quant ty' ty2', (VU fc)) infer ctx (RLet fc nm ty v sc) = do ty' <- check ctx ty (VU emptyFC) - vty <- eval ctx.env CBN ty' + vty <- eval ctx.env ty' v' <- check ctx v vty - vv <- eval ctx.env CBN v' + vv <- eval ctx.env v' let ctx' = define ctx nm vv vty (sc',scty) <- infer ctx' sc pure $ (Let fc nm v' sc', scty) infer ctx (RAnn fc tm rty) = do ty <- check ctx rty (VU fc) - vty <- eval ctx.env CBN ty + vty <- eval ctx.env ty tm <- check ctx tm vty pure (tm, vty) infer ctx (RLam _ (BI fc nm icit quant) tm) = do - a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN + a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env let ctx' = extend ctx nm a (tm', b) <- infer ctx' tm debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}" @@ -1560,7 +1560,7 @@ infer ctx (RLam _ (BI fc nm icit quant) tm) = do infer ctx (RImplicit fc) = do ty <- freshMeta ctx fc (VU emptyFC) Normal - vty <- eval ctx.env CBN ty + vty <- eval ctx.env ty tm <- freshMeta ctx fc vty Normal pure (tm, vty) diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt index cdf4128..628e7ec 100644 --- a/src/Lib/Eval.newt +++ b/src/Lib/Eval.newt @@ -10,22 +10,17 @@ import Data.IORef import Data.SnocList import Data.SortedMap - -eval : Env -> Mode -> Tm -> M Val +eval : Env -> Tm -> M Val -- REVIEW everything is evalutated whether it's needed or not -- It would be nice if the environment were lazy. -- e.g. case is getting evaluated when passed to a function because -- of dependencies in pi-types, even if the dependency isn't used - infixl 8 _$$_ - _$$_ : Closure -> Val -> M Val -_$$_ (MkClosure env tm) u = eval (u :: env) CBN tm - - +_$$_ (MkClosure env tm) u = eval (u :: env) tm vapp : Val -> Val -> M Val vapp (VLam _ _ _ _ t) u = t $$ u @@ -34,15 +29,12 @@ vapp (VRef fc nm sp) u = pure $ VRef fc nm (sp :< u) vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u) vapp t u = error' "impossible in vapp \{show t} to \{show u}\n" - vappSpine : Val -> SnocList Val -> M Val vappSpine t Lin = pure t vappSpine t (xs :< x) = do rest <- vappSpine t xs vapp rest x - - lookupVar : Env -> Int -> Maybe Val lookupVar env k = let l = cast $ length env in if k > l @@ -74,7 +66,7 @@ tryEval env (VRef fc k sp) = do catchError ( do debug $ \ _ => "app \{show name} to \{show sp}" - vtm <- eval env CBN tm + vtm <- eval env tm debug $ \ _ => "tm is \{render 90 $ pprint Nil tm}" val <- vappSpine vtm sp case val of @@ -92,7 +84,6 @@ tryEval env (VRef fc k sp) = do pure Nothing tryEval _ _ = pure Nothing - -- Force far enough to compare types forceType : Env -> Val -> M Val @@ -107,41 +98,41 @@ forceType env x = do | _ => pure x forceType env x' -evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val) -evalCase env mode sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do +evalCase : Env -> Val -> List CaseAlt -> M (Maybe Val) +evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do top <- getTop if nm == name then 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 sc xs -- bail for a stuck function _ => pure Nothing where go : Env -> List Val -> List String -> M (Maybe Val) go env (arg :: args) (nm :: nms) = go (arg :: env) args nms go env args Nil = do - t' <- eval env mode t + t' <- eval env t Just <$> vappSpine t' (Lin <>< args) go env Nil rest = pure Nothing -- REVIEW - this is handled in the caller already -evalCase env mode sc@(VVar fc k sp) alts = case lookupVar env k of +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 mode val alts + evalCase env val alts Just t => do val <- vappSpine t sp - evalCase env mode val alts + evalCase env val alts Nothing => do debug $ \ _ => "lookup \{show k} is Nothing in env \{show env}" pure Nothing -evalCase env mode sc (CaseDefault u :: xs) = Just <$> eval (sc :: env) mode u -evalCase env mode sc cc = do +evalCase env sc (CaseDefault u :: xs) = Just <$> eval (sc :: env) u +evalCase env sc cc = do debug $ \ _ => "CASE BAIL sc \{show sc} vs " -- \{show cc}" debug $ \ _ => "env is \{show env}" pure Nothing @@ -155,52 +146,51 @@ evalCase env mode sc cc = do -- TODO maybe add glueing -eval env mode (Ref fc x) = pure $ VRef fc x Lin -eval env mode (App _ t u) = do - t' <- eval env mode t - u' <- eval env mode u + +eval env (Ref fc x) = pure $ VRef fc x Lin +eval env (App _ t u) = do + t' <- eval env t + u' <- eval env u vapp t' u' -eval env mode (UU fc) = pure (VU fc) -eval env mode (Erased fc) = pure (VErased fc) -eval env mode (Meta fc i) = do +eval env (UU fc) = pure (VU fc) +eval env (Erased fc) = pure (VErased fc) +eval env (Meta fc i) = do meta <- lookupMeta i case meta of (Solved _ k t) => pure $ t _ => pure $ VMeta fc i Lin -eval env mode (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t) -eval env mode (Pi fc x icit rig a b) = do - a' <- eval env mode a +eval env (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t) +eval env (Pi fc x icit rig a b) = do + a' <- eval env a pure $ VPi fc x icit rig a' (MkClosure env b) -eval env mode (Let fc nm t u) = do - t' <- eval env mode t - u' <- eval (VVar fc (cast $ length env) Lin :: env) mode u +eval env (Let fc nm t u) = do + t' <- eval env t + u' <- eval (VVar fc (cast $ length env) Lin :: env) u pure $ VLet fc nm t' u' -eval env mode (LetRec fc nm ty t u) = do - ty' <- eval env mode ty - t' <- eval (VVar fc (length' env) Lin :: env) mode t - u' <- eval (VVar fc (length' env) Lin :: env) mode 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' -- 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 -eval env mode (Bnd fc i) = case getAt' i env of +eval env (Bnd fc i) = case getAt' i env of Just rval => pure rval Nothing => error fc "Bad deBruin index \{show i}" -eval env mode (Lit fc lit) = pure $ VLit fc lit +eval env (Lit fc lit) = pure $ VLit fc lit -eval env mode tm@(Case fc sc alts) = do +eval env tm@(Case fc sc alts) = do -- TODO we need to be able to tell eval to expand aggressively here. - sc' <- eval env mode sc + sc' <- eval env sc sc' <- unlet env sc' -- try to expand lets from pattern matching sc' <- forceType env sc' - vsc <- eval env mode sc - vcase <- evalCase env mode sc' alts + vsc <- eval env sc + vcase <- evalCase env sc' alts pure $ fromMaybe (VCase fc vsc alts) vcase - quote : (lvl : Int) -> Val -> M Tm - quoteSp : (lvl : Int) -> Tm -> SnocList Val -> M Tm quoteSp lvl t Lin = pure t quoteSp lvl t (xs :< x) = do @@ -246,12 +236,7 @@ quote l (VErased fc) = pure $ Erased fc -- ezoo only seems to use it at Nil, but essentially does this: nf : Env -> Tm -> M Tm -nf env t = eval env CBN t >>= quote (length' env) - - -nfv : Env -> Tm -> M Tm -nfv env t = eval env CBV t >>= quote (length' env) - +nf env t = eval env t >>= quote (length' env) prvalCtx : {{ctx : Context}} -> Val -> M String prvalCtx {{ctx}} v = do @@ -310,7 +295,7 @@ zonkApp top l env t@(Meta fc k) sp = do meta <- lookupMeta k case meta of (Solved _ j v) => do - sp' <- traverse (eval env CBN) sp + sp' <- traverse (eval env) sp debug $ \ _ => "zonk \{show k} -> \{show v} spine \{show sp'}" foo <- vappSpine v (Lin <>< sp') debug $ \ _ => "-> result is \{show foo}" diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 228e223..c6447be 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -59,7 +59,7 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do sols <- case kind of AutoSolve => do x <- quote ctx.lvl ty - ty <- eval ctx.env CBN x + ty <- eval ctx.env x debug $ \ _ => "AUTO ---> \{show ty}" -- we want the context here too. top <- getTop @@ -150,11 +150,10 @@ processDef ns fc nm clauses = do | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}" log 1 $ \ _ => "check \{nm} at \{render 90 $ pprint Nil ty}" - vty <- eval Nil CBN ty + vty <- eval Nil ty debug $ \ _ => "\{nm} vty is \{show vty}" - -- I can take LHS apart syntactically or elaborate it with an infer clauses' <- traverse makeClause clauses tm <- buildTree (mkCtx fc) (MkProb clauses' vty) @@ -165,9 +164,6 @@ processDef ns fc nm clauses = do -- NOW - might not need this if we do it at compile time tm' <- zonk top 0 Nil tm debug $ \ _ => "NF\n\{render 80 $ pprint Nil tm'}" - -- This is done in Compile.newt now, we can't store the result because we need the real thing at compile time - -- tm'' <- erase Nil tm' Nil - -- debug $ \ _ => "ERASED\n\{render 80 $ pprint Nil tm''}" debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm'} : \{render 90 $ pprint Nil ty}" updateDef (QN ns nm) fc ty (Fn tm') @@ -179,13 +175,11 @@ processCheck ns fc tm ty = do info fc "check \{show tm} at \{show ty}" ty' <- check (mkCtx fc) ty (VU fc) putStrLn " got type \{render 90 $ pprint Nil ty'}" - vty <- eval Nil CBN ty' + vty <- eval Nil ty' res <- check (mkCtx fc) tm vty putStrLn " got \{render 90 $ pprint Nil res}" norm <- nf Nil res putStrLn " NF \{render 90 $ pprint Nil norm}" - norm <- nfv Nil res - putStrLn " NFV \{render 90 $ pprint Nil norm}" processClass : List String → FC → String → Telescope → List Decl → M Unit @@ -220,6 +214,7 @@ processClass ns classFC nm tele decls = do log 1 $ \ _ => "\{render 90 $ pretty decl}" processDecl ns $ TypeSig fc (name :: Nil) funType processDecl ns decl + setFlag (QN ns name) fc Inline where makeLHS : Raw → Telescope → Raw makeLHS acc ((BI fc' nm icit quant, _) :: tele) = RApp fc' (makeLHS acc tele) (RVar fc' nm) Implicit @@ -278,7 +273,7 @@ processInstance ns instfc ty decls = do | _ => error tyFC "\{show tconName} has multiple constructors \{show cons}" 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 + 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 @@ -286,7 +281,7 @@ processInstance ns instfc ty decls = do debug $ \ _ => "traverse \{show $ map showTm args}" -- This is a little painful because we're reverse engineering the -- individual types back out from the composite type - args' <- traverse (eval env CBN) args + args' <- traverse (eval env) args debug $ \ _ => "args' is \{show args'}" appty <- apply vdcty args' conTele <- getFields appty env Nil @@ -416,8 +411,8 @@ processData ns fc nm ty cons = do tyty <- check (mkCtx fc) ty (VU fc) case lookupRaw nm top of Just (MkEntry _ name type Axiom _) => do - tyty' <- eval Nil CBN tyty - type' <- eval Nil CBN type + tyty' <- eval Nil tyty + type' <- eval Nil type unifyCatch fc (mkCtx fc) tyty' type' Just _ => error fc "\{show nm} already declared" Nothing => setDef (QN ns nm) fc tyty Axiom Nil @@ -449,7 +444,6 @@ processData ns fc nm ty cons = do let arity = cast $ piArity tyty updateDef (QN ns nm) fc tyty (TCon arity cnames) where - binderName : Binder → Name binderName (MkBinder _ nm _ _ _) = nm @@ -493,6 +487,7 @@ processRecord ns recordFC nm tele cname decls = do log 1 $ \ _ => "\{render 90 $ pretty pdecl}" processDecl ns $ TypeSig fc (pname :: Nil) funType processDecl ns pdecl + setFlag (QN ns pname) fc Inline -- currently mixfix registration is handled in the parser -- since we now run a decl at a time we could do it here. diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 0f8d230..2829e47 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -233,8 +233,6 @@ data Val : U where Env : U Env = List Val -data Mode = CBN | CBV - data Closure = MkClosure Env Tm getValFC : Val -> FC