blob: 766c21e3e9572426c2b46a6fbc2ad75f466b2b1b (
plain)
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
|
module Obs.Typing.Conversion
import Control.Monad.Maybe
import Control.Monad.Trans
import Data.Bool
import Data.Nat
import Decidable.Equality
import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
import Obs.Substitution
import Obs.Universe
%default total
-- Conversion ------------------------------------------------------------------
export
convert : (s : Universe)
-> (a : TypeNormalForm ctx)
-> (t, u : NormalForm (relevance s) ctx)
-> MaybeT (Logging ann) (NormalForm (relevance s) ctx)
untypedConvert : (t, u : NormalForm Relevant ctx) -> MaybeT (Logging ann) (NormalForm Relevant ctx)
-- Diagonals
untypedConvert (Cnstr (Universe s)) (Cnstr (Universe s')) =
if s == s' then pure (Cnstr (Universe s)) else nothing
untypedConvert (Cnstr (Pi s s' var a b)) (Cnstr (Pi l l' _ a' b')) = do
let Yes Refl = decEq s l
| No _ => nothing
lift $ trace "going back to type-directed conversion"
a <- assert_total (convert (succ s) (cast s) a a')
b <- assert_total (convert (succ s') (cast s') b b')
pure (Cnstr $ Pi s s' var a b)
untypedConvert (Cnstr (Lambda s var t)) (Cnstr (Lambda s' _ u)) = do
let Yes Refl = decEq s s'
| No _ => nothing
lift $ trace "converting under lambda"
t <- untypedConvert t u
pure (Cnstr $ Lambda s var t)
untypedConvert (Cnstr (Sigma s s' var a b)) (Cnstr (Sigma l l' _ a' b')) = do
let Yes Refl = decEq s l
| No _ => nothing
lift $ trace "going back to type-directed conversion"
a <- assert_total (convert (succ s) (cast s) a a')
b <- assert_total (convert (succ s') (cast s') b b')
pure (Cnstr $ Sigma s s' var a b)
untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf' t' u')) = do
let Yes Refl = decEq (s, s') (l, l')
| No _ => nothing
lift $ trace "converting pair pointwise"
t <- untypedConvert t t'
u <- untypedConvert u u'
pure (Cnstr $ Pair l l' Set t u)
untypedConvert (Cnstr (Pair s@(Set _) Prop prf t u)) (Cnstr (Pair l Prop prf' t' u')) = do
let Yes Refl = decEq s l
| No _ => nothing
lift $ trace "converting pair pointwise"
t <- untypedConvert t t'
pure (Cnstr $ Pair l Prop Set t Irrel)
untypedConvert (Cnstr (Pair Prop s'@(Set _) prf t u)) (Cnstr (Pair Prop l' prf' t' u')) = do
let Yes Refl = decEq s' l'
| No _ => nothing
lift $ trace "converting pair pointwise"
u <- untypedConvert u u'
pure (Cnstr $ Pair Prop l' Set Irrel u)
untypedConvert (Cnstr Bool) (Cnstr Bool) = pure (Cnstr Bool)
untypedConvert (Cnstr True) (Cnstr True) = pure (Cnstr True)
untypedConvert (Cnstr False) (Cnstr False) = pure (Cnstr False)
untypedConvert (Cnstr Top) (Cnstr Top) = pure (Cnstr Top)
untypedConvert (Cnstr Bottom) (Cnstr Bottom) = pure (Cnstr Bottom)
untypedConvert t@(Ntrl (Var _ _ _ i)) (Ntrl (Var _ _ _ j)) =
if elemToNat i == elemToNat j then pure t else nothing
untypedConvert lhs@(Ntrl (App r t u)) rhs@(Ntrl (App r' t' u')) = do
let Yes Refl = decEq r r'
| No _ => nothing
lift $ trace "checking parts of a spine"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
let Relevant = r'
| Irrelevant => lift $ doApp t Irrel
u <- untypedConvert u u'
lift $ doApp t u
untypedConvert lhs@(Ntrl (Fst r t)) rhs@(Ntrl (Fst r' t')) = do
lift $ trace "checking full pair for fst"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
lift $ doFst Relevant r t
untypedConvert lhs@(Ntrl (Snd r t)) rhs@(Ntrl (Snd r' t')) = do
lift $ trace "checking full pair for snd"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
lift $ doSnd r Relevant (rewrite pairRelevantRight r in t)
untypedConvert lhs@(Ntrl (If t f g)) rhs@(Ntrl (If t' f' g')) = do
lift $ trace "checking all branches of if"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
f <- untypedConvert f f'
g <- untypedConvert g g'
lift $ doIf t f g
untypedConvert (Ntrl Absurd) (Ntrl Absurd) = pure (Ntrl Absurd)
untypedConvert lhs@(Ntrl (Equal a t u)) rhs@(Ntrl (Equal a' t' u')) = do
lift $ trace "checking equal (stuck on type)"
a <- untypedConvert (assert_smaller lhs (Ntrl a)) (assert_smaller rhs (Ntrl a'))
t <- untypedConvert t t'
u <- untypedConvert u u'
lift $ doEqual _ a t u
untypedConvert lhs@(Ntrl (EqualL t u)) rhs@(Ntrl (EqualL t' u')) = do
lift $ trace "checking equal (stuck on left)"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
u <- untypedConvert u u'
lift $ doEqualSet t u
untypedConvert lhs@(Ntrl (EqualR t u)) rhs@(Ntrl (EqualR t' u')) = do
lift $ trace "checking equal (stuck on right)"
t <- untypedConvert (assert_smaller lhs (Cnstr t)) (assert_smaller rhs (Cnstr t'))
u <- untypedConvert (assert_smaller lhs (Ntrl u)) (assert_smaller rhs (Ntrl u'))
lift $ doEqualSet t u
untypedConvert lhs@(Ntrl (EqualStuck t u)) rhs@(Ntrl (EqualStuck t' u')) = do
lift $ trace "checking equal (head mismatch)"
t <- untypedConvert (assert_smaller lhs (Cnstr t)) (assert_smaller rhs (Cnstr t'))
u <- untypedConvert (assert_smaller lhs (Cnstr u)) (assert_smaller rhs (Cnstr u'))
lift $ doEqualSet t u
untypedConvert lhs@(Ntrl (CastL a b t)) rhs@(Ntrl (CastL a' b' t')) = do
lift $ trace "checking cast (stuck on left)"
a <- untypedConvert (assert_smaller lhs (Ntrl a)) (assert_smaller rhs (Ntrl a'))
b <- untypedConvert b b'
t <- untypedConvert t t'
lift $ doCast _ a b t
untypedConvert lhs@(Ntrl (CastR a b t)) rhs@(Ntrl (CastR a' b' t')) = do
lift $ trace "checking cast (stuck on right)"
a <- untypedConvert (assert_smaller lhs (Cnstr a)) (assert_smaller rhs (Cnstr a'))
b <- untypedConvert (assert_smaller lhs (Ntrl b)) (assert_smaller rhs (Ntrl b'))
t <- untypedConvert t t'
lift $ doCast _ a b t
untypedConvert lhs@(Ntrl (CastStuck a b t)) rhs@(Ntrl (CastStuck a' b' t')) = do
lift $ trace "checking cast (stuck on left)"
a <- untypedConvert (assert_smaller lhs (Cnstr a)) (assert_smaller rhs (Cnstr a'))
b <- untypedConvert (assert_smaller lhs (Cnstr b)) (assert_smaller rhs (Cnstr b'))
t <- untypedConvert t t'
lift $ doCast _ a b t
-- Pi types
untypedConvert t@(Cnstr (Lambda s var _)) (Ntrl u) = do
u <- lift $ doApp (Ntrl $ weaken [relevance s] u) (point (var, (s ** Refl)) Here)
assert_total (untypedConvert t (Cnstr (Lambda s var u)))
untypedConvert (Ntrl t) u@(Cnstr (Lambda s var _)) = do
t <- lift $ doApp (Ntrl $ weaken [relevance s] t) (point (var, (s ** Refl)) Here)
assert_total (untypedConvert (Cnstr (Lambda s var t)) u)
-- Sigma types
untypedConvert t@(Cnstr (Pair s s' prf _ _)) t'@(Ntrl _) =
let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t'
in do
t' <- lift $ doFst (relevance s) (relevance s') t''
u' <- lift $ doSnd (relevance s) (relevance s') t''
assert_total (untypedConvert t (Cnstr (Pair s s' prf t' u')))
untypedConvert t@(Ntrl _) t'@(Cnstr (Pair s s' prf _ _)) =
let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t
in do
t <- lift $ doFst (relevance s) (relevance s') t''
u <- lift $ doSnd (relevance s) (relevance s') t''
assert_total (untypedConvert (Cnstr (Pair s s' prf t u)) t')
-- Bools
-- no cases because diagonals complete
-- Fallback
untypedConvert _ _ = nothing
convert Prop a Irrel Irrel = pure Irrel
convert (Set k) (Ntrl a) t u = do
lift $ trace $ pretty {ann} "cannot do type-directed conversion on" <++> pretty a
untypedConvert t u
convert (Set k) (Cnstr (Universe s)) t u = do
lift $ trace $ pretty {ann} "converting in type" <++> pretty s
untypedConvert t u
convert (Set k) (Cnstr (Pi s s'@(Set _) var a b)) t u = do
-- s' must be Set, otherwise ty is in Prop
lift $ trace "converting pi type"
t' <- lift $ doApp (Sorted.weaken [relevance s] t) (point (var, (s ** Refl)) Here)
u' <- lift $ doApp (Sorted.weaken [relevance s] u) (point (var, (s ** Refl)) Here)
t <- convert s' b t' u'
pure (Cnstr $ Lambda s var t)
convert (Set k) ty@(Cnstr (Sigma s@(Set j) s' var a b)) t u = do
lift $ trace "converting sigma type"
t1 <- lift $ doFst Relevant (relevance s') t
u1 <- lift $ doFst Relevant (relevance s') u
t1 <- convert s a t1 u1
t2 <- lift $ doSnd Relevant (relevance s') t
u2 <- lift $ doSnd Relevant (relevance s') u
b <- lift $ subst1 t1 b
t2 <- convert s' (assert_smaller ty b) t2 u2
pure (Cnstr $ Pair s s' Set t1 t2)
convert (Set k) ty@(Cnstr (Sigma Prop s'@(Set _) var a b)) t u = do
lift $ trace "converting sigma type (snd only)"
t2 <- lift $ doSnd Irrelevant Relevant t
u2 <- lift $ doSnd Irrelevant Relevant u
b <- lift $ subst1 Irrel b
t2 <- convert s' (assert_smaller ty b) t2 u2
pure (Cnstr $ Pair Prop s' Set Irrel t2)
convert (Set 0) (Cnstr Bool) (Cnstr True) (Cnstr True) = do
lift $ trace "converting bool (true)"
pure (Cnstr True)
convert (Set 0) (Cnstr Bool) (Cnstr False) (Cnstr False) = do
lift $ trace "converting bool (false)"
pure (Cnstr False)
convert (Set k) (Cnstr Bool) t@(Ntrl _) u@(Ntrl _) = do
lift $ trace "converting bool (neutral)"
untypedConvert t u
convert (Set k) (Cnstr a) t u = lift $ inScope "bad type constructor" $ fatal a
|
