From 57a8fe9609ec86836ee8d2f65f910d87fe905a9e Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 29 Dec 2024 21:17:06 -0800 Subject: [PATCH] prep for self-hosting --- TODO.md | 3 +- scripts/translate.sh | 4 +++ src/Lib/Common.idr | 2 +- src/Lib/CompileExp.idr | 4 +-- src/Lib/Elab.idr | 4 +-- src/Lib/Erasure.idr | 4 +-- src/Lib/Eval.idr | 8 ++--- src/Lib/ProcessDecl.idr | 2 +- src/Lib/Types.idr | 75 ++++++++++++++--------------------------- 9 files changed, 44 insertions(+), 62 deletions(-) diff --git a/TODO.md b/TODO.md index e997625..3c80422 100644 --- a/TODO.md +++ b/TODO.md @@ -5,6 +5,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] tokenizer that can be ported to newt - [ ] string interpolation? +- [ ] mutual recursion in where? - [x] Move on to next decl in case of error - [x] for parse error, seek to col 0 token and process next decl - [ ] record update sugar, syntax TBD @@ -25,7 +26,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [ ] default implementations (use them if nothing is defined, where do we store them?) e.g. Ord compare, <, etc in Idris - I may need to actually store some details on interfaces rather than reverse engineer from type. - [x] syntax for negative integers -- [ ] White box tests in `test` directory +- [ ] White box tests in `test` directory (I can't get this to work right with pack et al) - [x] Put worker in iframe on safari - [ ] Warnings or errors for missing definitions - [ ] Add the type name to dcon so confusion detection in case split is simpler diff --git a/scripts/translate.sh b/scripts/translate.sh index 312df64..26f86d9 100755 --- a/scripts/translate.sh +++ b/scripts/translate.sh @@ -15,6 +15,7 @@ find src -type f -name '*.idr' | while read -r file; do s/\bType\b/U/g; s/\binterface\b/class/g; s/import public/import/g; + s/^\s*covering//g; s/^export//g; s/^public export//g; s/\(([A-Z]\w+), ?([^)]+)\)/(\1 × \2)/g; @@ -23,10 +24,13 @@ find src -type f -name '*.idr' | while read -r file; do # patterns would be another option, but # we would need to handle overlapping ones s/\[\]/Nil/g; + s/\{-/\/-/g; + s/-\}/-\//g; s/\[<\]/Lin/g; s/\[<([^\],]+)\]/(Lin :< \1)/g; s/\[([^\],]+)\]/(\1 :: Nil)/g; s/^([A-Z].*where)/instance \1/g; + s/^data (.*:\s*\w+)$/\1/g; ' "$file" > "$output_file" fi done diff --git a/src/Lib/Common.idr b/src/Lib/Common.idr index c0b72c4..a7dbbf5 100644 --- a/src/Lib/Common.idr +++ b/src/Lib/Common.idr @@ -135,7 +135,7 @@ Show Fixity where public export record OpDef where constructor MkOp - name : String + opname : String prec : Int fix : Fixity isPrefix : Bool diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 44fbd72..f6e7334 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -129,9 +129,9 @@ compileTerm tm@(App _ _ _) with (funArgs tm) debug "apply other \{pprint [] t}" t' <- compileTerm t args' <- traverse compileTerm args - apply t' args' [<] 0 (U emptyFC) + apply t' args' [<] 0 (UU emptyFC) -- error (getFC t) "Don't know how to apply \{showTm t}" -compileTerm (U _) = pure $ CRef "U" +compileTerm (UU _) = pure $ CRef "U" compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] Z compileTerm (Case _ t alts) = do t' <- compileTerm t diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 64ffd0b..4c9fb22 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -168,7 +168,7 @@ rename meta ren lvl v = go ren lvl v catchError (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) go ren lvl (VLam fc n icit rig t) = pure (Lam fc n icit rig !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<]))) go ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) - go ren lvl (VU fc) = pure (U fc) + go ren lvl (VU fc) = pure (UU fc) go ren lvl (VErased fc) = pure (Erased fc) -- for now, we don't do solutions with case in them. go ren lvl (VCase fc sc alts) = error fc "Case in solution" @@ -1127,7 +1127,7 @@ infer ctx (RApp fc t u icit) = do u <- check ctx u a pure (App fc t u, !(b $$ !(eval ctx.env CBN u))) -infer ctx (RU fc) = pure (U fc, VU fc) -- YOLO +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' diff --git a/src/Lib/Erasure.idr b/src/Lib/Erasure.idr index 723da8d..51337bf 100644 --- a/src/Lib/Erasure.idr +++ b/src/Lib/Erasure.idr @@ -71,7 +71,7 @@ erase env t sp = case t of (Pi fc nm icit rig u v) => do u' <- erase env u [] v' <- erase ((nm, Many, Just u) :: env) v [] - eraseSpine env (Pi fc nm icit rig u' v') sp (Just $ U emptyFC) + eraseSpine env (Pi fc nm icit rig u' v') sp (Just $ UU emptyFC) -- leaving as-is for now, we don't know the quantity of the apps (Meta fc k) => pure t (Case fc u alts) => do @@ -93,7 +93,7 @@ erase env t sp = case t of -- This is working, but empty FC Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" Just (nm, Many, ty) => eraseSpine env t sp ty - (U fc) => eraseSpine env t sp (Just $ U fc) + (UU fc) => eraseSpine env t sp (Just $ UU fc) (Lit fc lit) => eraseSpine env t sp Nothing Erased fc => error fc "erased value in relevant context" -- eraseSpine env t sp Nothing diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index d9a1157..cc9aa05 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -136,7 +136,7 @@ bind v env = v :: env eval env mode (Ref fc x def) = pure $ VRef fc x def [<] eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u) -eval env mode (U fc) = pure (VU fc) +eval env mode (UU fc) = pure (VU fc) eval env mode (Erased fc) = pure (VErased fc) eval env mode (Meta fc i) = case !(lookupMeta i) of @@ -182,7 +182,7 @@ quote l (VLam fc x icit rig t) = pure $ Lam fc x icit rig !(quote (S l) !(t $$ V quote l (VPi fc x icit rig a b) = pure $ Pi fc x icit rig !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<])) quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) u) quote l (VLetRec fc nm ty t u) = pure $ LetRec fc nm !(quote l ty) !(quote (S l) t) !(quote (S l) u) -quote l (VU fc) = pure (U fc) +quote l (VU fc) = pure (UU fc) quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts quote l (VLit fc lit) = pure $ Lit fc lit @@ -234,7 +234,7 @@ appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs tweakFC : FC -> Tm -> Tm tweakFC fc (Bnd fc1 k) = Bnd fc k tweakFC fc (Ref fc1 nm x) = Ref fc nm x -tweakFC fc (U fc1) = U fc +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 tweakFC fc (App fc1 t u) = App fc t u @@ -276,7 +276,7 @@ zonk top l env t = case t of (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u (LetRec fc nm ty t u) => LetRec fc nm <$> zonk top l env ty <*> zonkBind top l env t <*> zonkBind top l env u (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts - U fc => pure $ U fc + 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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 23d8eb5..8c4622e 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -474,7 +474,7 @@ processDecl ns (Data fc nm ty cons) = do -- logMetas mstart where checkDeclType : Tm -> M () - checkDeclType (U _) = pure () + checkDeclType (UU _) = pure () checkDeclType (Pi _ str icit rig t u) = checkDeclType u checkDeclType _ = error fc "data type doesn't return U" diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 9f702eb..fb2c4b1 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -12,7 +12,6 @@ import Data.SortedMap import Data.String import Data.Vect - public export data QName : Type where QN : List String -> String -> QName @@ -127,7 +126,7 @@ data Tm : Type where -- InsMeta : Nat -> List BD -> Tm Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm App : FC -> Tm -> Tm -> Tm - U : FC -> Tm + UU : FC -> Tm Pi : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm Case : FC -> Tm -> List CaseAlt -> Tm -- need type? @@ -146,7 +145,7 @@ HasFC Tm where getFC (Meta fc k) = fc getFC (Lam fc str _ _ t) = fc getFC (App fc t u) = fc - getFC (U fc) = fc + getFC (UU fc) = fc getFC (Pi fc str icit quant t u) = fc getFC (Case fc t xs) = fc getFC (Lit fc _) = fc @@ -157,13 +156,15 @@ HasFC Tm where covering Show Tm -public export covering +public export +covering Show CaseAlt where show (CaseDefault tm) = "_ => \{show tm}" show (CaseCons nm args tm) = "\{nm} \{unwords args} => \{show tm}" show (CaseLit lit tm) = "\{show lit} => \{show tm}" -public export covering +public export +covering Show Tm where show (Bnd _ k) = "(Bnd \{show k})" show (Ref _ str _) = "(Ref \{show str})" @@ -171,7 +172,7 @@ Show Tm where show (App _ t u) = "(\{show t} \{show u})" show (Meta _ i) = "(Meta \{show i})" show (Lit _ l) = "(Lit \{show l})" - show (U _) = "U" + show (UU _) = "U" show (Pi _ str Explicit rig t u) = "(Pi (\{show rig}\{str} : \{show t}) => \{show u})" show (Pi _ str Implicit rig t u) = "(Pi {\{show rig}\{str} : \{show t}} => \{show u})" show (Pi _ str Auto rig t u) = "(Pi {{\{show rig}\{str} : \{show t}}} => \{show u})" @@ -202,7 +203,7 @@ Eq (Tm) where (Ref _ x _) == Ref _ y _ = x == y (Lam _ n _ _ t) == Lam _ n' _ _ t' = t == t' (App _ t u) == App _ t' u' = t == t' && u == u' - (U _) == (U _) = True + (UU _) == (UU _) = True (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u' _ == _ = False @@ -239,7 +240,7 @@ pprint names tm = go 0 names tm go p names (Meta _ k) = text "?m:\{show k}" go p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> go 0 (nm :: names) t go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u - go p names (U _) = "U" + go p names (UU _) = "U" go p names (Pi _ nm Auto rig t u) = parens 0 p $ text "{{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u go p names (Pi _ nm Implicit rig t u) = parens 0 p $ @@ -280,13 +281,23 @@ data Val : Type where -- we'll need to look this up in ctx with IO VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val VLam : FC -> Name -> Icit -> Quant -> Closure -> Val - VPi : FC -> Name -> Icit -> Quant -> (a : Lazy Val) -> (b : Closure) -> Val + VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val VLet : FC -> Name -> Val -> Val -> Val VLetRec : FC -> Name -> Val -> Val -> Val -> Val VU : FC -> Val VErased : FC -> Val VLit : FC -> Literal -> Val +public export +Env : Type +Env = List Val + +public export +data Mode = CBN | CBV + +public export +data Closure = MkClosure Env Tm + public export getValFC : Val -> FC getValFC (VVar fc _ _) = fc @@ -307,7 +318,8 @@ HasFC Val where getFC = getValFC Show Closure -covering export +covering +export Show Val where show (VVar _ k [<]) = "%var\{show k}" show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> [])})" @@ -317,6 +329,7 @@ Show Val where show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{show x})" show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{show y})" show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{show y})" + show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show x}}}. \{show y})" show (VCase fc sc alts) = "(%case \{show sc} ...)" show (VU _) = "U" show (VLit _ lit) = show lit @@ -324,46 +337,9 @@ Show Val where show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}" show (VErased _) = "ERASED" -public export -Env : Type -Env = List Val - -public export -data Mode = CBN | CBV - -public export -data Closure = MkClosure Env Tm - covering Show Closure where show (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})" -{- -smalltt - -smalltt gets into weird haskell weeds in eval - shifting top level to the left -and tagging meta vs top with a bit. - -I think something subtle is going on with laziness on Elaboration.hs:300 -yeah, and define is even inlined. - -So it has a top context, and clears out almost everything for processing a def in -a different kind of context. - -we very much need an idea of local context for metas. I don't want to abstract over -the entire program. - -So I guess we have top and local then? - -With haskell syntax. I think we can have Axiom for claims and rewrite to def later. - -Hmm, so given ezoo, if I'm going simple, I could keep BDs short, and use the normal -context. (Zoo4.lean:222) I'd probably still need an undefined/axiom marker as a value? - -ok, so with just one context, Env is List Val and we're getting Tm back from type checking. - -Can I get val back? Do we need to quote? What happens if we don't? - --} record Context @@ -403,7 +379,7 @@ Show Def where show (DCon k tyname) = "DCon \{show k} \{show tyname}" show (Fn t) = "Fn \{show t}" show (PrimTCon) = "PrimTCon" - show (PrimFn src uses) = "PrimFn \{show src} \{show uses}" + show (PrimFn src used) = "PrimFn \{show src} \{show used}" ||| entry in the top level context public export @@ -483,7 +459,8 @@ Show MetaEntry where show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}" show (Solved _ k x) = "Solved \{show k} \{show x}" -export withPos : Context -> FC -> Context +export +withPos : Context -> FC -> Context withPos ctx fc = { fc := fc } ctx export