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
[@@@ocaml.warning "-33"]
open Options
type constant =
| ConstBitv of string
| ConstInt of string
| ConstReal of Num.num
| ConstTrue
| ConstFalse
| ConstVoid
type pp_infix =
| PPand | PPor | PPxor | PPimplies | PPiff
| PPlt | PPle | PPgt | PPge | PPeq | PPneq
| PPadd | PPsub | PPmul | PPdiv | PPmod
| PPpow_int | PPpow_real
type pp_prefix =
| PPneg | PPnot
type ppure_type =
| PPTint
| PPTbool
| PPTreal
| PPTunit
| PPTbitv of int
| PPTvarid of string * Loc.t
| PPTexternal of ppure_type list * string * Loc.t
type pattern =
{ pat_loc : Loc.t; pat_desc : string * string list }
type lexpr =
{ pp_loc : Loc.t; pp_desc : pp_desc }
and pp_desc =
| PPvar of string
| PPapp of string * lexpr list
| PPmapsTo of string * lexpr
| PPinInterval of lexpr * bool * lexpr * lexpr * bool
| PPdistinct of lexpr list
| PPconst of constant
| PPinfix of lexpr * pp_infix * lexpr
| PPprefix of pp_prefix * lexpr
| PPget of lexpr * lexpr
| PPset of lexpr * lexpr * lexpr
| PPdot of lexpr * string
| PPrecord of (string * lexpr) list
| PPwith of lexpr * (string * lexpr) list
| PPconcat of lexpr * lexpr
| PPif of lexpr * lexpr * lexpr
| PPforall of
(string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPexists of
(string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPforall_named of
(string * string * ppure_type) list * (lexpr list * bool) list *
lexpr list * lexpr
| PPexists_named of
(string * string * ppure_type) list * (lexpr list * bool) list *
lexpr list * lexpr
| PPnamed of string * lexpr
| PPlet of (string * lexpr) list * lexpr
| PPcheck of lexpr
| PPcut of lexpr
| PPcast of lexpr * ppure_type
| PPmatch of lexpr * (pattern * lexpr) list
| PPisConstr of lexpr * string
| PPproject of bool * lexpr * string
type plogic_type =
| PPredicate of ppure_type list
| PFunction of ppure_type list * ppure_type
type body_type_decl =
| Record of string * (string * ppure_type) list
| Enum of string list
| Algebraic of (string * (string * ppure_type) list) list
| Abstract
type type_decl = Loc.t * string list * string * body_type_decl
type decl =
| Theory of Loc.t * string * string * decl list
| Axiom of Loc.t * string * Util.axiom_kind * lexpr
| Rewriting of Loc.t * string * lexpr list
| Goal of Loc.t * string * lexpr
| Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type
| Predicate_def of
Loc.t * (string * string) *
(Loc.t * string * ppure_type) list * lexpr
| Function_def of
Loc.t * (string * string) *
(Loc.t * string * ppure_type) list * ppure_type * lexpr
| TypeDecl of type_decl list
| Push of Loc.t * int
| Pop of Loc.t * int
type file = decl list