blob: dd793291c51dc793993e4a7333fba863080740fb (
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
|
(** This module defines the AST which is to be extracted to generate code.
This AST is voluntarily as simple as possible, so that the extraction
can focus on pretty-printing and on the syntax specific to the different
provers.
TODO: we don't use this...
*)
type constant_value = Pure.constant_value
type pattern =
| PatVar of string
| PatDummy
| PatEnum of string * pattern list
(** Enum: the constructor name (tuple if `None`) and the fields.
Note that we never use structures as patters: we access the fields one
by one.
*)
| PatTuple of pattern list
(** We want to keep terms a little bit structured, for pretty printing.
See the `FieldProj` and the `Record` cases, for instance.
*)
type term =
| Constant of constant_value
| Var of string
| FieldProj of term * term
(** `x.y`
Of course, we can always use projectors like `record_get_y x`:
this variant is for pretty-printing.
Note that `FieldProj` are generated when translating `place` from
the "pure" AST.
*)
| App of term * term
| Let of bool * pattern * term * term
| If of term * term * term
| Switch of term * (pattern * term) list
| Ascribed of term * term (** `x <: ty` *)
| Tuple of term list
| Record of (string * term) list
(** In case a record has named fields, we try to use them, to generate
code like: `{ x = 3; y = true; }`
Otherwise, we can use `App` (with the record constructor).
*)
type fun_decl = {
name : string;
inputs : pattern list;
(** We can match over the inputs, hence the use of [pattern]. In practice,
we use [PatVar] and [PatDummy].
*)
input_tys : term list;
output_ty : term;
body : term;
}
|
