From f991ca0d52e1232c41d3ec2b1e18aa98d680a1bb Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 18 Jan 2025 15:21:15 -0800 Subject: [PATCH] Remove unused argument that was blowing up serialization. --- port/Lib/Compile.newt | 2 +- port/Lib/CompileExp.newt | 4 ++-- port/Lib/Elab.newt | 26 +++++++++++++------------- port/Lib/Erasure.newt | 4 ++-- port/Lib/Eval.newt | 14 +++++++------- port/Lib/ProcessDecl.newt | 4 ++-- port/Lib/Types.newt | 24 ++++++++++++------------ port/Main.newt | 12 ------------ 8 files changed, 39 insertions(+), 51 deletions(-) diff --git a/port/Lib/Compile.newt b/port/Lib/Compile.newt index d2d8930..0321e4c 100644 --- a/port/Lib/Compile.newt +++ b/port/Lib/Compile.newt @@ -300,7 +300,7 @@ walkAlt acc (CaseCons name args t) = walkTm t acc walkAlt acc (CaseLit lit t) = walkTm t acc -walkTm (Ref x nm y) acc = process acc nm +walkTm (Ref x nm) acc = process acc nm walkTm (Lam x str _ _ t) acc = walkTm t acc walkTm (App x t u) acc = walkTm u acc >>= walkTm t walkTm (Pi x str icit y t u) acc = walkTm u acc >>= walkTm t diff --git a/port/Lib/CompileExp.newt b/port/Lib/CompileExp.newt index f26f585..915ecd7 100644 --- a/port/Lib/CompileExp.newt +++ b/port/Lib/CompileExp.newt @@ -106,7 +106,7 @@ apply t ts acc Z ty = go (CApp t (acc <>> Nil) 0) ts compileTerm (Bnd _ k) = pure $ CBnd k -- need to eta expand to arity -compileTerm t@(Ref fc nm _) = do +compileTerm t@(Ref fc nm) = do top <- get let (Just (MkEntry _ _ type _)) = lookup nm top | Nothing => error fc "Undefined name \{show nm}" @@ -119,7 +119,7 @@ compileTerm tm@(App _ _ _) = case funArgs tm of (Meta _ k, args) => do info (getFC tm) "Compiling an unsolved meta \{show tm}" pure $ CApp (CRef "Meta\{show k}") Nil 0 - (t@(Ref fc nm _), args) => do + (t@(Ref fc nm), args) => do args' <- traverse compileTerm args arity <- arityForName fc nm top <- get diff --git a/port/Lib/Elab.newt b/port/Lib/Elab.newt index fe96af7..ab55d9f 100644 --- a/port/Lib/Elab.newt +++ b/port/Lib/Elab.newt @@ -128,7 +128,7 @@ unifyCatch : FC -> Context -> Val -> Val -> M Unit isCandidate : Val -> Tm -> Bool isCandidate ty (Pi fc nm Explicit rig t u) = False isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u -isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm' +isCandidate (VRef _ nm _) (Ref fc nm') = nm == nm' isCandidate ty (App fc t u) = isCandidate ty t isCandidate _ _ = False @@ -358,7 +358,7 @@ renameSpine meta ren lvl tm (xs :< x) = do rename meta ren lvl (VVar fc k sp) = case findIndex' (_==_ k) ren of Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" Just x => renameSpine meta ren lvl (Bnd fc x) sp -rename meta ren lvl (VRef fc nm def sp) = renameSpine meta ren lvl (Ref fc nm def) sp +rename meta ren lvl (VRef fc nm sp) = renameSpine meta ren lvl (Ref fc nm) sp rename meta ren lvl (VMeta fc ix sp) = do -- So sometimes we have an unsolved meta in here which reference vars out of scope. debug $ \ _ => "rename Meta \{show ix} spine \{show sp}" @@ -523,7 +523,7 @@ unify env mode t u = do unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" unifyRef : Val -> Val -> M UnifyResult - unifyRef t'@(VRef fc k def sp) u'@(VRef fc' k' def' sp') = + unifyRef t'@(VRef fc k sp) u'@(VRef fc' k' sp') = -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y do -- catchError(unifySpine env mode (k == k') sp sp') $ \ err => do @@ -539,7 +539,7 @@ unify env mode t u = do -- Lennart.newt cursed type references itself -- We _could_ look up the ref, eval against Nil and vappSpine... - unifyRef t u@(VRef fc' k' def sp') = do + unifyRef t u@(VRef fc' k' sp') = do debug $ \ _ => "expand \{show t} =?= %ref \{show k'}" top <- get case lookup k' top of @@ -549,7 +549,7 @@ unify env mode t u = do unify env mode t appvtm _ => error fc' "unify failed \{show t} =?= \{show u} (no Fn :: Nil)\n env is \{show env}" - unifyRef t@(VRef fc k def sp) u = do + unifyRef t@(VRef fc k sp) u = do debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}" top <- get case lookup k top of @@ -692,7 +692,7 @@ primType : FC -> QName -> M Val primType fc nm = do top <- get case lookup nm top of - Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name PrimTCon Lin + Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name Lin _ => error fc "Primitive type \{show nm} not in scope" @@ -757,7 +757,7 @@ findSplit (x :: xs) = findSplit xs -- TODO, we may need to filter these against the type to rule out -- impossible cases getConstructors : Context -> FC -> Val -> M (List (QName × Int × Tm)) -getConstructors ctx scfc (VRef fc nm _ _) = do +getConstructors ctx scfc (VRef fc nm _) = do names <- lookupTCon nm traverse lookupDCon names where @@ -801,7 +801,7 @@ substVal k v tm = go tm 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 y sp) = VRef fc nm y (map go sp) + go (VRef fc nm sp) = VRef fc nm (map go sp) go tm = tm -- FIXME - do I need a Val closure like idris? -- or env in unify... @@ -874,10 +874,10 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do -- if the value is already constrained to a different constructor, return Nothing debug $ \ _ => "scrut \{scnm} constrained to \{show $ lookupDef ctx scnm}" - let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}" + let (VRef _ sctynm _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}" case lookupDef ctx scnm of - Just val@(VRef fc nm y sp) => + Just val@(VRef fc nm sp) => if nm /= dcName then do debug $ \ _ => "SKIP \{show dcName} because \{scnm} forced to \{show val}" @@ -912,7 +912,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do let (Just x) = findIndex' ((_==_ scnm) ∘ fst) ctx'.types | Nothing => error ctx.ctxFC "\{scnm} not is scope?" let lvl = lvl2ix (length' ctx'.env) x - let scon = (lvl, VRef ctx.ctxFC dcName (DCon arity dcName) sc) + let scon = (lvl, VRef ctx.ctxFC dcName sc) -- (DCon arity dcName) debug $ \ _ => "scty \{show scty}" debug $ \ _ => "UNIFY results \{show res.constraints}" @@ -1298,7 +1298,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do PatLit fc v => do let tyname = litTyName v case scty' of - (VRef fc1 nm x sp) => when (nm /= tyname) $ \ _ => error fc "expected \{show scty} and got \{show tyname}" + (VRef fc1 nm sp) => when (nm /= tyname) $ \ _ => error fc "expected \{show scty} and got \{show tyname}" _ => error fc "expected \{show scty} and got \{show tyname}" -- need to run through all of the PatLits in this slot and then find a fallback -- walk the list of patterns, stop if we hit a PatVar / PatWild, fail if we don't @@ -1450,7 +1450,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types Just (MkEntry _ name ty def) => do debug $ \ _ => "lookup \{show name} as \{show def}" vty <- eval Nil CBN ty - pure (Ref fc name def, vty) + 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) else go (i + 1) xs diff --git a/port/Lib/Erasure.newt b/port/Lib/Erasure.newt index d680b32..4e4a1ad 100644 --- a/port/Lib/Erasure.newt +++ b/port/Lib/Erasure.newt @@ -15,7 +15,7 @@ EEnv = List (String × Quant × Maybe Tm) -- check App at type getType : Tm -> M (Maybe Tm) -getType (Ref fc nm x) = do +getType (Ref fc nm) = do top <- get case lookup nm top of Nothing => error fc "\{show nm} not in scope" @@ -63,7 +63,7 @@ doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t Nil -- This is a little fuzzy because we don't have all of the types. erase env t sp = case t of (App fc u v) => erase env u ((fc,v) :: sp) - (Ref fc nm x) => do + (Ref fc nm) => do top <- get case lookup nm top of Nothing => error fc "\{show nm} not in scope" diff --git a/port/Lib/Eval.newt b/port/Lib/Eval.newt index 0e068ca..067c00f 100644 --- a/port/Lib/Eval.newt +++ b/port/Lib/Eval.newt @@ -30,7 +30,7 @@ _$$_ (MkClosure env tm) u = eval (u :: env) CBN tm vapp : Val -> Val -> M Val vapp (VLam _ _ _ _ t) u = t $$ u vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u) -vapp (VRef fc nm def sp) u = pure $ VRef fc nm def (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) vapp t u = error' "impossible in vapp \{show t} to \{show u}\n" @@ -67,7 +67,7 @@ unlet env x = pure x tryEval : Env -> Val -> M (Maybe Val) -tryEval env (VRef fc k _ sp) = do +tryEval env (VRef fc k sp) = do top <- get case lookup k top of Just (MkEntry _ name ty (Fn tm)) => @@ -105,7 +105,7 @@ forceType env x = do 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 mode sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do top <- get if nm == name then do @@ -152,7 +152,7 @@ evalCase env mode sc cc = do -- TODO maybe add glueing -eval env mode (Ref fc x def) = pure $ VRef fc x def Lin +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 @@ -232,7 +232,7 @@ quote l (VLetRec fc nm ty t u) = do u' <- quote (1 + l) u pure $ LetRec fc nm ty' t' u' quote l (VU fc) = pure (UU fc) -quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp +quote l (VRef fc n sp) = quoteSp l (Ref fc n) sp quote l (VCase fc sc alts) = do sc' <- quote l sc pure $ Case fc sc' alts @@ -286,7 +286,7 @@ appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs -- For errors, I think we want to pretend the code has been typed in place tweakFC : FC -> Tm -> Tm tweakFC fc (Bnd fc1 k) = Bnd fc k -tweakFC fc (Ref fc1 nm x) = Ref fc nm x +tweakFC fc (Ref fc1 nm) = Ref fc nm tweakFC fc (UU fc1) = UU fc tweakFC fc (Meta fc1 k) = Meta fc k tweakFC fc (Lam fc1 nm icit rig t) = Lam fc nm icit rig t @@ -339,5 +339,5 @@ zonk top l env t = case t of UU fc => pure $ UU fc Lit fc lit => pure $ Lit fc lit Bnd fc ix => pure $ Bnd fc ix - Ref fc ix def => pure $ Ref fc ix def + Ref fc ix => pure $ Ref fc ix Erased fc => pure $ Erased fc diff --git a/port/Lib/ProcessDecl.newt b/port/Lib/ProcessDecl.newt index d7e0dae..55e50c7 100644 --- a/port/Lib/ProcessDecl.newt +++ b/port/Lib/ProcessDecl.newt @@ -263,7 +263,7 @@ processDecl ns (Instance instfc ty decls) = do | _ => do debug $ \ _ => "Forward declaration \{show sigDecl}" - let (Ref _ tconName _, args) = funArgs codomain + let (Ref _ tconName, args) = funArgs codomain | (tm, _) => error tyFC "\{render 90 $ pprint Nil codomain} doesn't appear to be a TCon application" let (Just (MkEntry _ name type (TCon cons))) = lookup tconName top | _ => error tyFC "\{show tconName} is not a type constructor" @@ -394,7 +394,7 @@ processDecl ns (Data fc nm ty cons) = do let (codomain, tele) = splitTele dty -- for printing let tnames = reverse $ map binderName tele - let (Ref _ hn _, args) = funArgs codomain + let (Ref _ hn, args) = funArgs codomain | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}" when (hn /= QN ns nm) $ \ _ => error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}" diff --git a/port/Lib/Types.newt b/port/Lib/Types.newt index e6c7360..d80b4a9 100644 --- a/port/Lib/Types.newt +++ b/port/Lib/Types.newt @@ -74,7 +74,7 @@ instance Eq Literal where data Tm : U where Bnd : FC -> Int -> Tm -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. - Ref : FC -> QName -> Def -> Tm + Ref : FC -> QName -> Tm Meta : FC -> QName -> Tm Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm App : FC -> Tm -> Tm -> Tm @@ -90,7 +90,7 @@ data Tm : U where instance HasFC Tm where getFC (Bnd fc k) = fc - getFC (Ref fc str x) = fc + getFC (Ref fc str) = fc getFC (Meta fc k) = fc getFC (Lam fc str _ _ t) = fc getFC (App fc t u) = fc @@ -106,7 +106,7 @@ showCaseAlt : CaseAlt → String instance Show Tm where show (Bnd _ k) = "(Bnd \{show k})" - show (Ref _ str _) = "(Ref \{show str})" + show (Ref _ str) = "(Ref \{show str})" show (Lam _ nm icit rig t) = "(\\ \{show rig}\{nm} => \{show t})" show (App _ t u) = "(\{show t} \{show u})" show (Meta _ i) = "(Meta \{show i})" @@ -147,7 +147,7 @@ instance Eq Icit where instance Eq (Tm) where -- (Local x) == (Local y) = x == y (Bnd _ x) == (Bnd _ y) = x == y - (Ref _ x _) == Ref _ y _ = x == y + (Ref _ x) == Ref _ y = x == y (Lam _ n _ _ t) == Lam _ n' _ _ t' = t == t' (App _ t u) == App _ t' u' = t == t' && u == u' (UU _) == (UU _) = True @@ -175,7 +175,7 @@ pprint' p names (Bnd _ k) = case getAt (cast k) names of -- Either a bug or we're printing without names Nothing => text "BND:\{show k}" Just nm => text "\{nm}:\{show k}" -pprint' p names (Ref _ str mt) = text (show str) +pprint' p names (Ref _ str) = text (show str) pprint' p names (Meta _ k) = text "?m:\{show k}" pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t pprint' p names (App _ t u) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names u @@ -217,7 +217,7 @@ Closure : U data Val : U where -- This will be local / flex with spine. VVar : FC -> (k : Int) -> (sp : SnocList Val) -> Val - VRef : FC -> (nm : QName) -> Def -> (sp : SnocList Val) -> Val + VRef : FC -> (nm : QName) -> (sp : SnocList Val) -> Val -- neutral case VCase : FC -> (sc : Val) -> List CaseAlt -> Val -- we'll need to look this up in ctx with IO @@ -239,7 +239,7 @@ data Closure = MkClosure Env Tm getValFC : Val -> FC getValFC (VVar fc _ _) = fc -getValFC (VRef fc _ _ _) = fc +getValFC (VRef fc _ _) = fc getValFC (VCase fc _ _) = fc getValFC (VMeta fc _ _) = fc getValFC (VLam fc _ _ _ _) = fc @@ -257,8 +257,8 @@ showClosure : Closure → String instance Show Val where show (VVar _ k Lin) = "%var\{show k}" show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})" - show (VRef _ nm _ Lin) = show nm - show (VRef _ nm _ sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})" + show (VRef _ nm Lin) = show nm + show (VRef _ nm sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})" show (VMeta _ ix sp) = "(%meta \{show ix} (\{show $ snoclen sp} sp :: Nil))" show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{showClosure x})" show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{showClosure y})" @@ -507,12 +507,12 @@ lookupMeta ix@(QN ns nm) = do case lookupMap' ix mc.metas of Just meta => pure meta Nothing => case lookupMap' ns top.modules of - Nothing => + Nothing => error emptyFC "missing module: \{show ns}" Just mod => case lookupMap' ix mod.modMetaCtx.metas of - Nothing => + Nothing => error emptyFC "missing meta: \{show ix}" - Just entry => pure entry + Just entry => pure entry mkCtx : FC -> Context mkCtx fc = MkCtx 0 Nil Nil Nil fc diff --git a/port/Main.newt b/port/Main.newt index 8128b69..1a34c39 100644 --- a/port/Main.newt +++ b/port/Main.newt @@ -21,16 +21,6 @@ import Lib.Syntax import Lib.Syntax import Node --- this was an experiment, prepping for dumping module information --- it ends up with out of memory dumping defs of some of the files. --- Prelude is 114MB pretty-printed... gzip to 1M -pfunc dumpObject uses (MkIORes MkUnit fs): ∀ a. String → a → IO Unit := `(_,fn,a) => (w) => { - console.log(a) - let data = JSON.stringify(a, null, ' ') - fs.writeFileSync(fn, data) - return MkIORes(undefined, MkUnit, w) -}` - primNS : List String primNS = ("Prim" :: Nil) @@ -128,8 +118,6 @@ processModule importFC base stk qn@(QN ns nm) = do let imported = snoc imported primNS - -- I guess we should empty defs now instead of at the end? - putStrLn $ "MODNS " ++ show modns top <- get (decls, ops) <- parseDecls fn top.ops toks Lin