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
208
209
210
211
212
213
|
module Obs.Typing.Conversion
import Control.Monad.Identity
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 ------------------------------------------------------------------
convertUntyped : (rel : Relevance) -> (left, right : NormalForm rel ctx) -> Identity Bool
export
convert : (rel : Relevance)
-> (type : TypeNormalForm ctx)
-> (left, right : NormalForm rel ctx)
-> Identity Bool
convert rel type left right = convertUntyped rel left right
convertCnstr : (left, right : Constructor ctx) -> Identity Bool
convertCnstr (Universe {s}) (Universe {s = s'}) = pure (s == s')
convertCnstr
(Pi {domainSort, codomainSort, domain, codomain})
(Pi
{ domainSort = domainSort'
, codomainSort = codomainSort'
, domain = domain'
, codomain = codomain'
}) = do
let Yes Refl = decEq (domainSort, codomainSort) (domainSort', codomainSort')
| No _ => pure False
convertDomain <- convert
{ rel = Relevant
, type = cast domainSort
, left = assert_smaller domain domain.type
, right = assert_smaller domain' domain'.type
}
convertCodomain <- convert
{ rel = Relevant
, type = cast codomainSort
, left = codomain
, right = codomain'
}
pure (convertDomain && convertCodomain)
convertCnstr
(Lambda {domainRel, var = _, body})
(Lambda {domainRel = domainRel', var = _, body = body'}) = do
let Yes Refl = decEq domainRel domainRel'
| No _ => pure False
convertUntyped {rel = Relevant, left = body, right = body'}
convertCnstr
(Sigma {indexSort, elementSort, index, element})
(Sigma
{ indexSort = indexSort'
, elementSort = elementSort'
, index = index'
, element = element'
}) = do
let Yes Refl = decEq (indexSort, elementSort) (indexSort', elementSort')
| No _ => pure False
convertIndex <- convert
{ rel = Relevant
, type = cast indexSort
, left = assert_smaller index index.type
, right = assert_smaller index' index'.type
}
convertElement <- convert
{ rel = Relevant
, type = cast elementSort
, left = element
, right = element'
}
pure (convertIndex && convertElement)
convertCnstr
(Pair {indexRel, elementRel, prf = _, first, second})
(Pair
{ indexRel = indexRel'
, elementRel = elementRel'
, prf = _
, first = first'
, second = second'
}) = do
let Yes Refl = decEq (indexRel, elementRel) (indexRel', elementRel')
| No _ => pure False
convertFirst <- convertUntyped {rel = indexRel, left = first, right = first'}
convertSecond <- convertUntyped {rel = elementRel, left = second, right = second'}
pure (convertFirst && convertSecond)
convertCnstr Bool Bool = pure True
convertCnstr True True = pure True
convertCnstr False False = pure True
convertCnstr (Box {prop}) (Box {prop = prop'}) =
convert {rel = Relevant, type = cast Prop, left = prop, right = prop'}
convertCnstr MkBox MkBox = pure True
convertCnstr Top Top = pure True
convertCnstr Bottom Bottom = pure True
convertCnstr left right = pure False
convertNtrl : (left, right : Neutral ctx) -> Identity Bool
convertNtrl (Var {var = _, i}) (Var {var = _, i = j}) = pure (elemToNat i == elemToNat j)
convertNtrl (App {argRel, fun, arg}) (App {argRel = argRel', fun = fun', arg = arg'}) = do
let Yes Refl = decEq argRel argRel'
| No _ => pure False
convertFun <- convertNtrl {left = fun, right = fun'}
convertArg <- convertUntyped {rel = argRel, left = arg, right = arg'}
pure (convertFun && convertArg)
convertNtrl (First {secondRel = _, arg}) (First {secondRel = _, arg = arg'}) =
convertNtrl arg arg'
convertNtrl (Second {firstRel = _, arg}) (Second {firstRel = _, arg = arg'}) =
convertNtrl arg arg'
convertNtrl
(If {discriminant, true, false})
(If {discriminant = discriminant', true = true', false = false'}) =
do
convertDiscriminant <- convertNtrl {left = discriminant, right = discriminant}
convertTrue <- convertUntyped {rel = Relevant, left = true, right = true'}
convertFalse <- convertUntyped {rel = Relevant, left = false, right = false'}
pure (convertDiscriminant && convertTrue && convertFalse)
convertNtrl Absurd Absurd = pure True
convertNtrl
(Equal {type, left, right})
(Equal {type = type', left = left', right = right'}) =
do
convertType <- convertNtrl {left = type, right = type'}
convertLeft <- convertUntyped {rel = Relevant, left = left, right = left'}
convertRight <- convertUntyped {rel = Relevant, left = right, right = right'}
pure (convertType && convertLeft && convertRight)
-- We don't need to check, e.g. EqualL and EqualR
-- Assume (EqualL left right) ~~ (EqualR left' right')
-- Then (Ntrl left) ~~ (Cnstr left')
-- This means left' is either Lambda or Pair
-- Lamda and Pair are not type constructors.
-- Hence we have a contradiction, so we are done.
convertNtrl (EqualL {left, right}) (EqualL {left = left', right = right'}) = do
convertLeft <- convertNtrl {left = left, right = left'}
convertRight <- convertUntyped {rel = Relevant, left = right, right = right'}
pure (convertLeft && convertRight)
convertNtrl (EqualR {left, right}) (EqualR {left = left', right = right'}) = do
convertLeft <- convertCnstr {left = left, right = left'}
convertRight <- convertNtrl {left = right, right = right'}
pure (convertLeft && convertRight)
convertNtrl (EqualStuck {left, right}) (EqualStuck {left = left', right = right'}) = do
convertLeft <- convertCnstr {left = left, right = left'}
convertRight <- convertCnstr {left = right, right = right'}
pure (convertLeft && convertRight)
convertNtrl
(CastL {oldType, newType, value})
(CastL {oldType = oldType', newType = newType', value = value'}) =
do
convertOldType <- convertNtrl {left = oldType, right = oldType'}
convertNewType <- convertUntyped {rel = Relevant, left = newType, right = newType'}
convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
pure (convertOldType && convertNewType && convertValue)
convertNtrl
(CastR {oldType, newType, value})
(CastR {oldType = oldType', newType = newType', value = value'}) =
do
convertOldType <- convertCnstr {left = oldType, right = oldType'}
convertNewType <- convertNtrl {left = newType, right = newType'}
convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
pure (convertOldType && convertNewType && convertValue)
convertNtrl
(CastStuck {oldType, newType, value})
(CastStuck {oldType = oldType', newType = newType', value = value'}) =
do
convertOldType <- convertCnstr {left = oldType, right = oldType'}
convertNewType <- convertCnstr {left = newType, right = newType'}
convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
pure (convertOldType && convertNewType && convertValue)
convertNtrl left right = pure False
convertEta : (left : Constructor ctx) -> (right : Neutral ctx) -> Identity Bool
convertEta (Lambda {domainRel, var, body}) right = do
let right = weaken [domainRel] right
let rightBody = App {argRel = domainRel, fun = right, arg = point Nothing Here}
convertUntyped {rel = Relevant, left = body, right = Ntrl rightBody}
convertEta (Pair {indexRel = Relevant, elementRel = Relevant, prf, first, second}) right = do
let rightFirst = First {secondRel = Relevant, arg = right}
let rightSecond = Second {firstRel = Relevant, arg = right}
convertFirst <- convertUntyped {rel = Relevant, left = first, right = Ntrl rightFirst}
convertSecond <- convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
pure (convertFirst && convertSecond)
convertEta (Pair {indexRel = Relevant, elementRel = Irrelevant, prf, first, second}) right = do
let rightFirst = First {secondRel = Relevant, arg = right}
convertUntyped {rel = Relevant, left = first, right = Ntrl rightFirst}
convertEta (Pair {indexRel = Irrelevant, elementRel = Relevant, prf, first, second}) right = do
let rightSecond = Second {firstRel = Relevant, arg = right}
convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
convertEta MkBox right = pure True
convertEta left right = pure False
convertUntyped Irrelevant left right = pure True
convertUntyped Relevant (Ntrl left) (Ntrl right) = convertNtrl left right
convertUntyped Relevant (Ntrl left) (Cnstr right) = assert_total (convertEta right left)
convertUntyped Relevant (Cnstr left) (Ntrl right) = convertEta left right
convertUntyped Relevant (Cnstr left) (Cnstr right) = convertCnstr left right
|
