-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathErase.hs
121 lines (109 loc) · 4.54 KB
/
Erase.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
module Erase where
import NbE
import Term
data UntypedTerm =
UVar Int
| ULam UntypedTerm
| UApp UntypedTerm UntypedTerm
deriving Show
uIdentity :: UntypedTerm
uIdentity = ULam $ UVar 0
finalSort :: Value -> Either String (Maybe Level)
finalSort (VAbort x) = finalSort x
finalSort (VAddProof t _ _) = finalSort t
finalSort (VPi a f) = do
s <- finalSort a
case s of
Just k | k > LevelN 0 -> Left $ "Erasing pi over large sort " ++ show s
_ -> finalSort $ inst f [Reflect a (NVar 1000)]
finalSort (VRelevantBottom) = return $ Just $ LevelN 0
finalSort (VBottom) = return Nothing -- $ Just $ LevelN 0
finalSort (VTop) = return $ Just $ LevelN 0
finalSort (VNat) = return $ Just $ LevelN 0
finalSort (VRefine t _) = finalSort t
finalSort (VSigma a f) = do
s <- finalSort a
case s of
Just k | k > LevelN 0 -> Left $ "Erasing sigma over large sort " ++ show s
_ -> finalSort $ inst f [Reflect a (NVar 1000)]
finalSort (VSquash x) = return $ Just $ LevelN 0
finalSort (VSort k) = return $ Just k
finalSort (Reflect t _) = return Nothing
finalSortN :: Neutral -> Either String (Maybe Level)
finalSortN (NVar k) = return Nothing
finalSortN (NApp x y) = finalSortN x
finalSortN (NNatRec n t x y) = finalSort $ inst t [Reflect VNat $ NVar 1000]
finalSortN (NUseProof e tx tp ty y) = finalSort $
inst ty [Reflect tp $ NVar 1000, Reflect tx $ NVar 1000]
-- probably not entirely correct but idc
finalSortN (NProj1 x) = finalSortN x
finalSortN (NProj2 x) = finalSortN x
eraseTypedValue :: Value -> Value -> Int -> Either String UntypedTerm
eraseTypedValue (VAddProof t _ _) x n = eraseTypedValue t x n
eraseTypedValue (VPi a f) x n = do
end <- finalSort a
case end of
Just (LevelN 0) -> eraseTypedValue (inst f [irrel]) (vApp x irrel) n
Just k -> Left $ "Erasing pi over large sort " ++ show k
Nothing -> ULam <$> eraseTypedValue (inst f [fresh]) (vApp x fresh) (n + 1)
where
irrel = Reflect a (NVar 10000)
fresh = Reflect a (NVar n)
eraseTypedValue (VBottom) x n =
eraseTypedValue VRelevantBottom (vElimAbort x) n
eraseTypedValue (VRelevantBottom) (VAddProof x _ _) n =
eraseTypedValue VRelevantBottom x n
eraseTypedValue (VRelevantBottom) (VAbort x) n =
eraseTypedValue VRelevantBottom x n
eraseTypedValue (VRelevantBottom) (Reflect _ e) n = eraseNeutral e n
-- I'm not entirely sure about this one
eraseTypedValue (VTop) t n = return $ UVar 0
eraseTypedValue (VNat) t n = Left "Erasing Nats is unimplemented"
eraseTypedValue (VRefine t _) x n = eraseTypedValue t x n
eraseTypedValue (VSigma a f) p n = do
let (p1, p2) = vProjs p
p1' <- eraseTypedValue a p1 n
p2' <- eraseTypedValue (inst f [p1]) p2 n
return $ ULam $ UApp (UApp (UVar 0) p1') p2'
eraseTypedValue (VSort k) t n = Left "Erasing a sort"
eraseTypedValue t@(Reflect _ _) (VAddProof x _ _) n = eraseTypedValue t x n
eraseTypedValue (Reflect _ _) (Reflect _ e) n = eraseNeutral e n
eraseTypedValue a b c = Left $ "Something something " ++ show a ++ " " ++ show b ++ " " ++ show c
eraseNormal :: Normal -> Int -> Either String UntypedTerm
eraseNormal (Normal t x) = eraseTypedValue t x
eraseNeutral :: Neutral -> Int -> Either String UntypedTerm
eraseNeutral (NVar k) n = return $ UVar $ n - (k + 1)
eraseNeutral (NApp x (Normal y z)) n = do
end <- finalSort y
case end of
Just (LevelN 0) -> eraseNeutral x n
Just k -> Left $ "Erasing pi over large sort " ++ show k
Nothing -> UApp <$> (eraseNeutral x n) <*> (eraseTypedValue y z n)
eraseNeutral (NNatRec _ _ _ _) n = Left "Erasing NatRecs is unimplemented"
eraseNeutral (NUseProof e tx tp ty y) n = Left "Erasing UseProofs is unimplemented"
eraseNeutral (NProj1 e) n = do
e' <- eraseNeutral e n
return $ UApp e' $ ULam $ ULam $ UVar 1
eraseNeutral (NProj2 e) n = do
e' <- eraseNeutral e n
return $ UApp e' $ ULam $ ULam $ UVar 0
eraseNeutral (NUseSquash e ty y) n = Left "Erasing UseSquashes is unimplemented"
deleteVar :: UntypedTerm -> Int -> Maybe UntypedTerm
deleteVar (UVar n) m
| n == m = Nothing
| n > m = Just $ UVar $ n - 1
| otherwise = Just $ UVar n
deleteVar (ULam x) m = ULam <$> deleteVar x (m + 1)
deleteVar (UApp x y) m = UApp <$> deleteVar x m <*> deleteVar y m
etaReduce :: UntypedTerm -> UntypedTerm
etaReduce (UVar n) = UVar n
etaReduce (ULam x)
| UApp x' (UVar 0) <- etaReduce x, Just x' <- deleteVar x' 0 = x'
| otherwise = ULam $ etaReduce x
etaReduce (UApp x y) = UApp (etaReduce x) (etaReduce y)
toBLC :: UntypedTerm -> String
toBLC (UVar n) = replicate (n + 1) '1' ++ "0"
toBLC (ULam x) = "00" ++ toBLC x
toBLC (UApp x y) = "01" ++ toBLC x ++ toBLC y
-- toBLC :: UntypedTerm -> String
-- toBLC = show