diff options
author | Son Ho | 2022-01-28 23:02:12 +0100 |
---|---|---|
committer | Son Ho | 2022-01-28 23:02:12 +0100 |
commit | 34805f522e3c6d5ba9776738dd539dcd4b6d121d (patch) | |
tree | 87c50f36ad86e5caea2184c721dd233e5ae439e9 /src/ExtractAst.ml | |
parent | 04b05665f70ebb45b8d29adbd0529df197d8d5f3 (diff) |
Start working on ExtractAst
Diffstat (limited to 'src/ExtractAst.ml')
-rw-r--r-- | src/ExtractAst.ml | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/ExtractAst.ml b/src/ExtractAst.ml new file mode 100644 index 00000000..a80d3d08 --- /dev/null +++ b/src/ExtractAst.ml @@ -0,0 +1,55 @@ +(** 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. + *) + +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_def = { + 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; +} |