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

Remove unneeded implicities

Browse Source
This commit is contained in:
Steve Dunham
2024-07-14 16:04:26 -07:00
parent 76fae34bcf
commit 127a1e7f00
3 changed files with 23 additions and 26 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
src/Lib/Check.idr
View File

@@ -57,13 +57,13 @@ rename meta ren lvl v = go ren lvl v
go ren lvl (VMeta ix sp) = if ix == meta
then throwError $ E (0,0) "meta occurs check"
else goSpine ren lvl (Meta ix) sp
go ren lvl (VLam n icit t) = pure (Lam n icit !(go (lvl :: ren) (S lvl) !(t $$ VVar lvl [<])))
go ren lvl (VLam n t) = pure (Lam n !(go (lvl :: ren) (S lvl) !(t $$ VVar lvl [<])))
go ren lvl (VPi n icit ty tm) = pure (Pi n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar lvl [<])))
go ren lvl VU = pure U
lams : Nat -> Tm -> Tm
lams 0 tm = tm
lams (S k) tm = Lam "arg:\{show k}" Explicit (lams k tm)
lams (S k) tm = Lam "arg:\{show k}" (lams k tm)
solve : Nat -> Nat -> SnocList Val -> Val -> M ()
solve l m sp t = do
@@ -91,9 +91,9 @@ parameters (ctx: Context)
t' <- forceMeta t
u' <- forceMeta u
case (t',u') of
(VLam _ _ t, VLam _ _ t' ) => unify (l + 1) !(t $$ VVar l [<]) !(t' $$ VVar l [<])
(t, VLam _ _ t' ) => unify (l + 1) !(t `vapp` VVar l [<]) !(t' $$ VVar l [<])
(VLam _ _ t, t' ) => unify (l + 1) !(t $$ VVar l [<]) !(t' `vapp` VVar l [<])
(VLam _ t, VLam _ t') => unify (l + 1) !(t $$ VVar l [<]) !(t' $$ VVar l [<])
(t, VLam _ t') => unify (l + 1) !(t `vapp` VVar l [<]) !(t' $$ VVar l [<])
(VLam _ t, t' ) => unify (l + 1) !(t $$ VVar l [<]) !(t' `vapp` VVar l [<])
(VPi _ _ a b, VPi _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar l [<]) !(b' $$ VVar l [<])
(VVar k sp, VVar k' sp' ) =>
if k == k' then unifySpine l (k == k') sp sp'
@@ -133,12 +133,12 @@ check ctx tm ty with (force ty)
let var = VVar (length ctx.env) [<]
let ctx' = extend ctx nm a
tm' <- check ctx' tm !(b $$ var)
pure $ Lam nm icit tm'
pure $ Lam nm tm'
else if icit' == Implicit then do
let var = VVar (length ctx.env) [<]
ty' <- b $$ var
sc <- check (extend ctx nm' a) t ty'
pure $ Lam nm' icit' sc
pure $ Lam nm' sc
else
error [(DS "Icity issue checking \{show t} at \{show ty}")]
other => error [(DS "Expected pi type, got \{show !(quote 0 ty)}")]
@@ -147,7 +147,7 @@ check ctx tm ty with (force ty)
let var = VVar (length ctx.env) [<]
ty' <- b $$ var
sc <- check (extend ctx nm' a) tm ty'
pure $ Lam nm' Implicit sc
pure $ Lam nm' sc
check ctx tm _ | ty = do
-- We need to insert if it's not a Lam
-- TODO figure out why the exception is here (cribbed from kovacs)
@@ -216,7 +216,7 @@ infer ctx (RLam nm icit tm) = do
let ctx' = extend ctx nm a
(tm', b) <- infer ctx' tm
putStrLn "make lam for \{show nm} scope \{show tm'} : \{show b}"
pure $ (Lam nm icit tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
pure $ (Lam nm tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
-- error {ctx} [DS "can't infer lambda"]
infer ctx RHole = do

8
src/Lib/TT.idr
View File

@@ -132,7 +132,7 @@ infixl 8 $$
export
vapp : Val -> Val -> M Val
vapp (VLam _ icit t) u = t $$ u
vapp (VLam _ t) u = t $$ u
vapp (VVar k sp) u = pure $ VVar k (sp :< u)
vapp (VRef nm sp) u = pure $ VRef nm (sp :< u)
vapp (VMeta k sp) u = pure $ VMeta k (sp :< u)
@@ -157,9 +157,9 @@ eval env mode (Meta i) =
case !(lookupMeta i) of
(Unsolved _ k xs) => pure $ VMeta i [<]
(Solved k t) => pure $ t
eval env mode (Lam x icit t) = pure $ VLam x icit (MkClosure env t)
eval env mode (Lam x t) = pure $ VLam x (MkClosure env t)
eval env mode (Pi x icit a b) = pure $ VPi x icit !(eval env mode a) (MkClosure env b)
eval env mode (Let x icit ty t u) = eval (!(eval env mode t) :: env) mode u
eval env mode (Let x ty t u) = eval (!(eval env mode t) :: env) mode u
eval env mode (Bnd i) = case getAt i env of
Just rval => pure rval
Nothing => error' "Bad deBruin index \{show i}"
@@ -177,7 +177,7 @@ quote l (VVar k sp) = if k < l
then quoteSp l (Bnd ((l `minus` k) `minus` 1)) sp -- level to index
else ?borken
quote l (VMeta i sp) = quoteSp l (Meta i) sp
quote l (VLam x icit t) = pure $ Lam x icit !(quote (S l) !(t $$ VVar l [<]))
quote l (VLam x t) = pure $ Lam x !(quote (S l) !(t $$ VVar l [<]))
quote l (VPi x icit a b) = pure $ Pi x icit !(quote l a) !(quote (S l) !(b $$ VVar l [<]))
quote l VU = pure U
quote l (VRef n sp) = quoteSp l (Ref n Nothing) sp

23
src/Lib/Types.idr
View File

@@ -45,12 +45,11 @@ data Tm : Type where
Meta : Nat -> Tm
-- kovacs optimization, I think we can App out meta instead
-- InsMeta : Nat -> List BD -> Tm
Lam : Name -> Icit -> Tm -> Tm
-- Do we need to remember Icit here?
Lam : Name -> Tm -> Tm
App : Tm -> Tm -> Tm
U : Tm
Pi : Name -> Icit -> Tm -> Tm -> Tm
Let : Name -> Icit -> Tm -> Tm -> Tm -> Tm
Let : Name -> Tm -> Tm -> Tm -> Tm
%name Tm t, u, v
@@ -58,14 +57,13 @@ public export
Show Tm where
show (Bnd k) = "(Bnd \{show k})"
show (Ref str _) = "(Ref \{show str})"
show (Lam nm Implicit t) = "(\\ {\{nm}} => \{show t})"
show (Lam nm Explicit t) = "(\\ \{nm} => \{show t})"
show (Lam nm t) = "(\\ \{nm} => \{show t})"
show (App t u) = "(\{show t} \{show u})"
show (Meta i) = "(Meta \{show i})"
show U = "U"
show (Pi str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
show (Pi str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
show (Let str icit t u v) = "let \{str} : \{show t} = \{show u} in \{show v}"
show (Let str t u v) = "let \{str} : \{show t} = \{show u} in \{show v}"
-- I can't really show val because it's HOAS...
@@ -82,11 +80,11 @@ Eq (Tm) where
-- (Local x) == (Local y) = x == y
(Bnd x) == (Bnd y) = x == y
(Ref x _) == (Ref y _) = x == y
(Lam n icit t) == (Lam n' icit' t') = icit == icit' && t == t'
(Lam n t) == (Lam n' t') = t == t'
(App t u) == App t' u' = t == t' && u == u'
U == U = True
(Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
(Let n icit t u v) == (Let n' icit' t' u' v') = t == t' && u == u' && v == v'
(Let n t u v) == (Let n' t' u' v') = t == t' && u == u' && v == v'
_ == _ = False
public export
@@ -94,12 +92,11 @@ Pretty Tm where
pretty (Bnd k) = ?rhs_0
pretty (Ref str mt) = text str
pretty (Meta k) = text "?m\{show k}"
pretty (Lam str Implicit t) = text "(\\ {\{str}} => " <+> pretty t <+> ")"
pretty (Lam str Explicit t) = text "(\\ \{str} => " <+> pretty t <+> ")"
pretty (Lam str t) = text "(\\ \{str} => " <+> pretty t <+> ")"
pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
pretty U = "U"
pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> "=>" <+> pretty u <+> ")"
pretty (Let str icit t u v) = text "let" <+> text str <+> ":" <+> pretty t <+> "=" <+> pretty u
pretty (Let str t u v) = text "let" <+> text str <+> ":" <+> pretty t <+> "=" <+> pretty u
-- public export
-- data Closure : Nat -> Type
@@ -129,7 +126,7 @@ data Val : Type where
VRef : (nm : String) -> (sp : SnocList Val) -> Val
-- we'll need to look this up in ctx with IO
VMeta : (ix : Nat) -> (sp : SnocList Val) -> Val
VLam : Name -> Icit -> Closure -> Val
VLam : Name -> Closure -> Val
VPi : Name -> Icit -> Lazy Val -> Closure -> Val
VU : Val
@@ -141,7 +138,7 @@ Show Val where
show (VVar k sp) = "(%var \{show k} \{show sp})"
show (VRef nm sp) = "(%ref \{nm} \{show sp})"
show (VMeta ix sp) = "(%meta \{show ix} \{show sp})"
show (VLam str icit x) = "(%lam \{str} \{show icit} \{show x})"
show (VLam str x) = "(%lam \{str} \{show x})"
show (VPi str Implicit x y) = "(%pi {\{str} : \{show x}}. \{show y})"
show (VPi str Explicit x y) = "(%pi (\{str} : \{show x}). \{show y})"
show VU = "U"