diff options
| -rw-r--r-- | TODO.md | 2 | ||||
| -rw-r--r-- | src/ExtractAst.ml | 55 | ||||
| -rw-r--r-- | src/Pure.ml | 14 | ||||
| -rw-r--r-- | src/main.ml | 1 |
4 files changed, 65 insertions, 7 deletions
@@ -1,5 +1,7 @@ # TODO +0. Rename Pure -> PureAst + 0. For variables pretty names: we could try to use the meta places used for the forward function input vars to compute pretty names for the backward functions output vars. 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; +} diff --git a/src/Pure.ml b/src/Pure.ml index bc655b63..8c416ed1 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -434,17 +434,16 @@ class virtual ['self] mapreduce_expression_base = (** **Rk.:** here, [expression] is not at all equivalent to the expressions used in CFIM. They are lambda-calculus expressions, and are thus actually more general than the CFIM statements, in a sense. - - TODO: actually when I defined [expression] I still had Rust in mind, so - it is not a "textbook" lambda calculus expression (still quite constrained). - As we want to do transformations on it, through micro-passes, it would be - good to update it and make it more "regular". - - TODO: remove `Return` and `Fail` (they should be "normal" values, I think) *) type expression = | Value of typed_rvalue * mplace option | Call of call + (** The function calls are still quite structured. + Change that?... We might want to have a "normal" lambda calculus + app (with head and argument): this would allow us to replace some + field accesses with calls to projectors over fields (when there + are clashes of field names, some provers like F* get pretty bad...) + *) | Let of bool * typed_lvalue * texpression * texpression (** Let binding. @@ -500,6 +499,7 @@ and switch_body = | SwitchInt of T.integer_type * (scalar_value * texpression) list * texpression | Match of match_branch list +(* TODO: we could (should?) merge SwitchInt and Match *) and match_branch = { pat : typed_lvalue; branch : texpression } diff --git a/src/main.ml b/src/main.ml index 7381c648..baa76b77 100644 --- a/src/main.ml +++ b/src/main.ml @@ -7,6 +7,7 @@ module I = Interpreter module EL = Easy_logging.Logging module TA = TypesAnalysis open PureToExtract +open ExtractAst (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. |