dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

the "mode" argument to eval was unused and not fully propagated

Browse Source
This commit is contained in:
Steve Dunham
2025-09-02 21:10:32 -07:00
parent a3801b8ba0
commit 97c50a254a
4 changed files with 75 additions and 97 deletions
Download Patch File Download Diff File Expand all files Collapse all files

56
src/Lib/Elab.newt
View File

@@ -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)

91
src/Lib/Eval.newt
View File

@@ -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}"

23
src/Lib/ProcessDecl.newt
View File

@@ -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.

2
src/Lib/Types.newt
View File

@@ -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