rachel/pi
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

changed some case orders to maybe optimize code a bit (maybe?)

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-07-25 00:35:20 +02:00
parent 48e9a474ff
commit cd8ee29281
3 changed files with 29 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/Core/Check.idr
View File

@ -65,8 +65,13 @@ mutual
-- terms types term
infer : Ctx n -> Ctx n -> Term n -> PI Value
infer trs tys (TVar i) = pure (index i tys)
infer trs tys TType = pure VType
infer trs tys TTop = pure VType
infer trs tys TBot = pure VType
infer trs tys TNat = pure VType
infer trs tys TStar = pure VTop
infer trs tys TZero = pure VNat
infer trs tys (TVar i) = pure (index i tys)
infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
\case
VClos env (TPi a b) => do
@ -76,24 +81,10 @@ mutual
_ => oops "expected infer pi"
infer trs tys TTop = pure VType
infer trs tys TBot = pure VType
infer trs tys TNat = pure VType
infer trs tys TStar = pure VTop
infer trs tys TZero = pure VNat
infer trs tys (TSuc n) = do
guardS "suc n" =<< check trs tys VNat n
pure VNat
infer trs tys (TTopInd c st) = do
guardS "⊤ C" =<< check trs tys (VClos trs (TPi TTop TType)) c
guardS "⊤ ★" =<< check trs tys (VApp (VClos trs c) VStar) st
pure (VClos trs (TPi TTop (TApp (weakTr c) (TVar 0))))
infer trs tys (TBotInd c) = do
guardS "⊥ C" =<< check trs tys (VClos trs (TPi TBot TType)) c
pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
infer trs tys (TNatInd c z s) = do
guardS "ℕ C" =<< check trs tys (VClos trs (TPi TNat TType)) c
guardS "ℕ z" =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
@ -116,6 +107,15 @@ mutual
guardS "let infer" =<< check trs tys (VClos trs ty) tr
infer !(extT trs trs tr) !(extT tys trs ty) tri
infer trs tys (TTopInd c st) = do
guardS "⊤ C" =<< check trs tys (VClos trs (TPi TTop TType)) c
guardS "⊤ ★" =<< check trs tys (VApp (VClos trs c) VStar) st
pure (VClos trs (TPi TTop (TApp (weakTr c) (TVar 0))))
infer trs tys (TBotInd c) = do
guardS "⊥ C" =<< check trs tys (VClos trs (TPi TBot TType)) c
pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
infer trs tys x = oops ("cannot infer type" ++ show x)
public export

15
src/Core/Convert.idr
View File

@ -23,13 +23,15 @@ convert u1 u2 = do
logS ("with value representations '" ++ show u1' ++ "' and '" ++ show u2' ++ "'.")
assert_total $ -- :(
case (u1', u2') of
(VGen k1, VGen k2) => pure (k1 == k2)
(VType, VType) => pure True
(VTop, VTop) => pure True
(VStar, VStar) => pure True
(VBot, VBot) => pure True
(VNat, VNat) => pure True
(VGen k1, VGen k2) => pure (k1 == k2)
(VNatTr n, VNatTr m) => pure (n == m)
(VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
(VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
@ -41,14 +43,8 @@ convert u1 u2 = do
guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2)
convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
(VNatTr n, VNatTr m) => pure (n == m)
(VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2
(VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
termGuard env1 env2 c1 c2
termConv env1 env2 st1 st2
(VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
(VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
@ -75,6 +71,11 @@ convert u1 u2 = do
v <- VGen <$> fresh
convert vsc (VClos (v :: env) sc)
(VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
termGuard env1 env2 c1 c2
termConv env1 env2 st1 st2
_ => pure False
where
termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool

12
src/Core/Normalize.idr
View File

@ -50,16 +50,16 @@ mutual
public export
eval : Ctx n -> Term n -> PI Value
eval env (TVar i) = pure (index i env)
eval env (TApp f x) = do
f' <- eval env f
x' <- eval env x
assert_total (app f' x') -- :(
eval env TType = pure VType
eval env TTop = pure VTop
eval env TStar = pure VStar
eval env TBot = pure VBot
eval env TNat = pure VNat
eval env TZero = pure (VNatTr 0)
eval env (TApp f x) = do
f' <- eval env f
x' <- eval env x
assert_total (app f' x') -- :(
eval env (TSuc n) = do
n' <- eval env n
@ -77,10 +77,11 @@ mutual
tr' <- eval env tr
eval (tr' :: env) tri
eval env tr = pure (VClos env tr)
eval env tr = pure (VClos env tr)
public export
whnf : Value -> PI Value
whnf (VClos env tr) = eval env tr
whnf (VApp f x) = do
f' <- whnf f
x' <- whnf x
@ -89,5 +90,4 @@ whnf (VPair a b) = do
a' <- whnf a
b' <- whnf b
pure (VPair a' b')
whnf (VClos env tr) = eval env tr
whnf v = pure v