blob: c11c1584f1bc38b0ea8dae909b361cb268679b8b (
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
|
module Obs.NormalForm
import Data.Fin
import Obs.Sort
import Obs.Substitution
import Text.PrettyPrint.Prettyprinter
-- Definition ------------------------------------------------------------------
data Constructor : Nat -> Type
data Neutral : Nat -> Type
data NormalForm : Nat -> Type
public export
data Constructor : Nat -> Type where
Sort : Sort -> Constructor n
public export
data Neutral : Nat -> Type where
Var : Fin n -> Neutral n
public export
data NormalForm : Nat -> Type where
Ntrl : Neutral n -> NormalForm n
Cnstr : Constructor n -> 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'
eqNtrl (Var i) (Var j) = i == j
eqWhnf (Ntrl t) (Ntrl u) = eqNtrl t u
eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
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
prettyPrecNtrl d (Var i) = pretty "$\{show i}"
prettyPrecWhnf d (Ntrl t) = prettyPrecNtrl d t
prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
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
renameNtrl (Var i) f = Var (f i)
renameWhnf (Ntrl t) f = Ntrl $ renameNtrl t f
renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
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
substNtrl (Var i) f = f i
substWhnf (Ntrl t) f = substNtrl t f
substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
export
Subst Constructor NormalForm Constructor where
subst = substCnstr
export
Subst Neutral NormalForm NormalForm where
subst = substNtrl
export
Subst NormalForm NormalForm NormalForm where
subst = substWhnf
|
