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

prep for self-hosting

Browse Source
This commit is contained in:
Steve Dunham
2024-12-29 21:17:06 -08:00
parent 6397cac18a
commit 57a8fe9609
9 changed files with 44 additions and 62 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Lib/Common.idr
View File

@@ -135,7 +135,7 @@ Show Fixity where
public export
record OpDef where
constructor MkOp
name : String
opname : String
prec : Int
fix : Fixity
isPrefix : Bool

4
src/Lib/CompileExp.idr
View File

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

4
src/Lib/Elab.idr
View File

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

4
src/Lib/Erasure.idr
View File

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

8
src/Lib/Eval.idr
View File

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

2
src/Lib/ProcessDecl.idr
View File

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

75
src/Lib/Types.idr
View File

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