/
calculus_def.ml
136 lines (99 loc) · 3.2 KB
/
calculus_def.ml
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
open Libpprinter
open Libparser
(*********************************)
(* Definitions of data structure *)
(*********************************)
type name = string
module NameMap = Map.Make(
struct
type t = string
let compare x y = compare x y
end
);;
module NameSet = Set.Make(
struct
type t = string
let compare x y = compare x y
end
);;
type index = int
module IndexSet = Set.Make(
struct
type t = int
let compare x y = compare x y
end
);;
module IndexMap = Map.Make(
struct
type t = int
let compare x y = compare x y
end
);;
type nature = Explicit
| Implicit
| NJoker (* used for unification *)
type uType = Type | Set | Prop
type uLevel = UName of name | USucc of uLevel | UMax of uLevel list
type uLevel_constraints = UEq of uLevel * uLevel
| ULt of uLevel * uLevel
type position = NoPosition
| Position of ((int * int) * (int * int)) * name list
type reduced = bool
type term = Universe of uType * uLevel * position
(* constante *)
| Cste of name * typeannotation * position * reduced
(* Free Var (index < 0) and Bounded Var (index > 0) *)
| Var of index * typeannotation * position
(* these constructors are only valide after parsing, and removed by typechecking *)
| AVar of typeannotation * position (* _ *)
| TName of name * typeannotation * position
(* quantifiers *)
| Lambda of (name * term * nature * position) * term * typeannotation * position * reduced
| Forall of (name * term * nature * position) * term * typeannotation * position * reduced
| Let of (name * term * position) * term * typeannotation * position * reduced
(* application *)
| App of term * (term * nature) list * typeannotation * position * reduced
(* destruction *)
| Match of term * (pattern list * term) list * typeannotation * position * reduced
and pattern = PAvar | PName of string
| PCstor of name * (pattern * nature) list
and typeannotation = NoAnnotation
| Annotation of term
| TypedAnnotation of term
| Typed of term
and substitution = term IndexMap.t
and var_frame = {
name: name;
ty: term;
nature: nature;
pos: position;
}
(* context *)
and context = {
bvs: var_frame list; (* size = n *)
fvs: (index * term * term option * name option) list list; (* size = n+1 *)
conversion_hyps: (term * term) list list; (* size = n *)
lvl_cste: uLevel_constraints list; (* size = ??? *)
}
(* for notation *)
type op = Nofix
| Prefix of int
| Infix of int * associativity
| Postfix of int
(* values contains in module *)
type value = Inductive of name list * term
| Axiom of term
| Definition of term
| Constructor of term
and defs = (name, value) Hashtbl.t;;
type poussin_error = FreeError of string
| Unshiftable_term of term * int * int
| UnknownCste of name
| NoUnification of context * term * term
| NoNatureUnification of context * term * term
| UnknownUnification of context * term * term
| NegativeIndexBVar of int
| UnknownBVar of context * int
| UnknownFVar of context * int
| NotInductiveDestruction of context * term
exception PoussinException of poussin_error