Start working on ExtractAst

3 files changed, 63 insertions, 7 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;
+}
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.