blob: a15c3c132be04a1b2ec4c8b377046eac6b01a1a1 (
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
|
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
Pi : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
Lambda : String -> NormalForm (S n) -> Constructor n
Top : Constructor n
Bottom : Constructor n
public export
data Neutral : Nat -> Type where
Var : String -> Fin n -> Neutral n
App : Neutral n -> NormalForm 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 : 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 (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
eqCnstr Top Top = True
eqCnstr Bottom Bottom = True
eqCnstr _ _ = False
eqNtrl (Var _ i) (Var _ j) = i == j
eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
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
export
Cast Sort (Constructor n) where
cast = Sort
export
Cast Sort (NormalForm n) where
cast = Cnstr . cast
-- 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 (Pi _ _ var a b) =
parenthesise (d > Open) $
group $
parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
pretty "->" <+> softline <+>
prettyPrecWhnf Open b
prettyPrecCnstr d (Lambda var t) =
parenthesise (d > Open) $
group $
backslash <+> pretty var <++>
pretty "=>" <+> softline <+>
prettyPrecWhnf Open t
prettyPrecCnstr d Top = pretty "()"
prettyPrecCnstr d Bottom = pretty "Void"
prettyPrecNtrl d (Var var i) = pretty "\{show var}@\{show i}"
prettyPrecNtrl d (App t u) =
parenthesise (d >= App) $
group $
fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u]
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 (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
renameCnstr Top f = Top
renameCnstr Bottom f = Bottom
renameNtrl (Var var i) f = Var var (f i)
renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
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
export
PointedRename Neutral where
point = Var ""
export
PointedRename NormalForm where
point = Ntrl . point
|
