blob: 08354b466f77acbe1686b63c9a3171c55d2f5d77 (
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
|
module Obs.NormalForm
import Data.Fin
import Obs.Sort
import Obs.Substitution
import Text.PrettyPrint.Prettyprinter
%default total
-- Definition ------------------------------------------------------------------
data Constructor : Nat -> Type
data Neutral : Nat -> Type
data NormalForm : Nat -> Type
public export
data Constructor : Nat -> Type where
Sort : Sort -> Constructor n
Top : Constructor n
Bottom : Constructor n
public export
data Neutral : Nat -> Type where
Var : Fin n -> Neutral n
Absurd : Neutral n
public export
data NormalForm : Nat -> Type where
Ntrl : Neutral n -> NormalForm n
Cnstr : Constructor n -> NormalForm n
Irrel : NormalForm n
public export
record Definition (n : Nat) where
constructor MkDefinition
name : Maybe String
sort : Sort
ty : NormalForm n
tm : NormalForm n
public export
data Context : Nat -> Type where
Nil : Context 0
(:<) : Context n -> Definition n -> Context (S n)
-- Interfaces ------------------------------------------------------------------
-- Naive equality tests
eqCnstr : Constructor n -> Constructor n -> Bool
eqNtrl : Neutral n -> Neutral n -> Bool
eqWhnf : NormalForm n -> NormalForm n -> Bool
eqCnstr (Sort s) (Sort s') = s == s'
eqCnstr Top Top = True
eqCnstr Bottom Bottom = True
eqCnstr _ _ = False
eqNtrl (Var i) (Var j) = i == j
eqNtrl Absurd Absurd = True
eqNtrl _ _ = False
eqWhnf (Ntrl t) (Ntrl u) = eqNtrl t u
eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
eqWhnf Irrel Irrel = True
eqWhnf _ _ = False
export
Eq (Constructor n) where
t == u = eqCnstr t u
export
Eq (Neutral n) where
t == u = eqNtrl t u
export
Eq (NormalForm n) where
t == u = eqWhnf t u
-- Pretty Print ----------------------------------------------------------------
prettyPrecCnstr : Prec -> Constructor n -> Doc ann
prettyPrecNtrl : Prec -> Neutral n -> Doc ann
prettyPrecWhnf : Prec -> NormalForm n -> Doc ann
prettyPrecCnstr d (Sort s) = prettyPrec d s
prettyPrecCnstr d Top = pretty "()"
prettyPrecCnstr d Bottom = pretty "Void"
prettyPrecNtrl d (Var i) = pretty "$\{show i}"
prettyPrecNtrl d Absurd = pretty "absurd"
prettyPrecWhnf d (Ntrl t) = prettyPrecNtrl d t
prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
prettyPrecWhnf d Irrel = pretty "_"
export
Pretty (Constructor n) where
prettyPrec = prettyPrecCnstr
export
Pretty (Neutral n) where
prettyPrec = prettyPrecNtrl
export
Pretty (NormalForm n) where
prettyPrec = prettyPrecWhnf
export
Pretty (Definition n) where
pretty def = group $
pretty def.name <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
pretty def.name <++> equals <+> softline <+> pretty def.tm
export
Pretty (Context n) where
pretty [] = neutral
pretty ([] :< def) = pretty def
pretty (ctx :< def) = pretty ctx <+> hardline <+> hardline <+> pretty def
-- Operations ------------------------------------------------------------------
-- Renaming
renameCnstr : Constructor n -> (Fin n -> Fin m) -> Constructor m
renameNtrl : Neutral n -> (Fin n -> Fin m) -> Neutral m
renameWhnf : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
renameCnstr (Sort s) f = Sort s
renameCnstr Top f = Top
renameCnstr Bottom f = Bottom
renameNtrl (Var i) f = Var (f i)
renameNtrl Absurd f = Absurd
renameWhnf (Ntrl t) f = Ntrl $ renameNtrl t f
renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
renameWhnf Irrel f = Irrel
export
Rename Constructor where
rename = renameCnstr
export
Rename Neutral where
rename = renameNtrl
export
Rename NormalForm where
rename = renameWhnf
-- Substitution
substCnstr : Constructor n -> (Fin n -> NormalForm m) -> Constructor m
substNtrl : Neutral n -> (Fin n -> NormalForm m) -> NormalForm m
substWhnf : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m
substCnstr (Sort s) f = Sort s
substCnstr Top f = Top
substCnstr Bottom f = Bottom
substNtrl (Var i) f = f i
substNtrl Absurd f = Ntrl Absurd
substWhnf (Ntrl t) f = substNtrl t f
substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
substWhnf Irrel f = Irrel
export
Subst Constructor NormalForm Constructor where
subst = substCnstr
export
Subst Neutral NormalForm NormalForm where
subst = substNtrl
export
Subst NormalForm NormalForm NormalForm where
subst = substWhnf
|
