blob: 37bdf67e54f4073f77ad47280cf426b002396ce0 (
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
|
module Obs.Typing.Conversion
import Data.Fin
import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
import Obs.Sort
import Obs.Substitution
-- Conversion ------------------------------------------------------------------
-- invariant: all definitions fully expanded
-- invariant: m |- t, u <- a : s
partial export
convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
partial
convertSet : (t, u : NormalForm n) -> Logging ann Bool
partial
convertSum : (t, u : NormalForm n) -> (s, s' : Sort) -> (a, b : NormalForm n) -> Logging ann Bool
-- In sort Prop
convert Irrel Irrel a Prop = pure True
-- In unknown type in set
convert t u (Ntrl _) (Set k) = pure $ t == u
-- In type Set
convert t u (Cnstr (Sort _)) (Set _) = convertSet t u
-- In type Pi
convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
convert t u b s'
-- In type Sigma
convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
t1 <- doFst t
u1 <- doFst t
True <- convert t1 u1 a s
| False => pure False
b <- subst1 t1 b
t2 <- doSnd t
u2 <- doSnd t
convert t2 u2 b s'
-- In type Sum (manually expanding definition of doCase)
convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b
-- In type Container
convert t u (Cnstr (Container s a s' s'')) (Set l) = do
t <- expandContainer t
u <- expandContainer u
convert (Cnstr t) (Cnstr u) (Cnstr (expandContainerTy s a s' s'')) (Set l)
-- Default
convert t u a s =
inScope "invalid conversion" $ fatal $
fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
convertSet (Cnstr (Sort s')) (Cnstr (Sort s'')) = pure $ s' == s''
convertSet (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) =
pure $
s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) =
pure $
s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) =
pure $
s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
convertSet (Cnstr (Container s a s' s'')) (Cnstr (Container l a' l' l'')) =
pure $
s == l && s' == l' && s'' == l'' && !(convertSet a a')
convertSet (Cnstr Top) (Cnstr Top) = pure True
convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True
convertSet (Ntrl t) u = pure (Ntrl t == u)
convertSet t (Ntrl u) = pure (t == Ntrl u)
convertSet t u = pure $ False
convertSum (Cnstr (Left t)) (Cnstr (Left u)) s s' a b = convert t u a s
convertSum (Cnstr (Right t)) (Cnstr (Right u)) s s' a b = convert t u b s'
convertSum (Ntrl t) u s s' a b = pure (Ntrl t == u)
convertSum t (Ntrl u) s s' a b = pure (t == Ntrl u)
convertSum t u s s' a b = pure False
|
