Simplify the let-bindings in the pure AST

1 files changed, 94 insertions, 61 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 61d2d130..64851449 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -18,6 +18,20 @@ module SynthPhaseId = IdGen ()
 module VarId = IdGen ()
 (** Pay attention to the fact that we also define a [VarId] module in Values *)
 
+(* TODO
+   (** The assumed types for the pure AST.
+
+       In comparison with CFIM:
+       - we removed `Box` (because it is translated as the identity: `Box T == T`)
+       - we added `Result`, which is the type used in the error monad. This allows
+         us to have a unified treatment of expressions.
+     *)
+   type assumed_ty = unit
+
+   type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty
+   [@@deriving show, ord]
+*)
+
 type ty =
   | Adt of T.type_id * ty list
       (** [Adt] encodes ADTs and tuples and assumed types.
@@ -238,55 +252,6 @@ type fun_id =
   | Unop of unop
   | Binop of E.binop * T.integer_type
 
-type call = {
-  func : fun_id;
-  type_params : ty list;
-  args : typed_rvalue list;
-      (** Note that at this point, some functions have no arguments. For instance:
-          ```
-          fn f();
-          ```
-
-          In the extracted code, we add a unit argument. This is unit argument is
-          added later, when going from the "pure" AST to the "extracted" AST.
-       *)
-  args_mplaces : mplace option list;  (** Meta data *)
-}
-
-(* TODO: we might want to merge Call and Assign *)
-type let_bindings =
-  | Call of typed_lvalue * call
-      (** The called function and the tuple of returned values. *)
-  | Assign of typed_lvalue * typed_rvalue * mplace option
-      (** Variable assignment: the introduced pattern and the place we read.
-      
-          We are quite general for the left-value on purpose; this is used
-          in several situations:
-
-          1. When deconstructing a tuple:
-          ```
-          let (x, y) = p in ...
-          ```
-          (not all languages have syntax like `p.0`, `p.1`... and it is more
-          readable anyway).
-          
-          2. When expanding an enumeration with one variant.
-          
-          In this case, [Deconstruct] has to be understood as:
-          ```
-          let Cons x tl = ls in
-          ...
-          ```
-          
-          Note that later, depending on the language we extract to, we can
-          eventually update it to something like this (for F*, for instance):
-          ```
-          let x = Cons?.v ls in
-          let tl = Cons?.tl ls in
-          ...
-          ```
-       *)
-
 (** Meta-information stored in the AST *)
 type meta = Assignment of mplace * typed_rvalue
 
@@ -295,12 +260,12 @@ class ['self] iter_expression_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
+    method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
+
     method visit_typed_rvalue : 'env -> typed_rvalue -> unit = fun _ _ -> ()
 
     method visit_typed_lvalue : 'env -> typed_lvalue -> unit = fun _ _ -> ()
 
-    method visit_let_bindings : 'env -> let_bindings -> unit = fun _ _ -> ()
-
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
 
     method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
@@ -311,7 +276,7 @@ class ['self] iter_expression_base =
 
     method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
 
-    method visit_var_or_dummy : 'env -> var_or_dummy -> unit = fun _ _ -> ()
+    method visit_fun_id : 'env -> fun_id -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for [map_expression] map visitor *)
@@ -319,15 +284,14 @@ class ['self] map_expression_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
+    method visit_ty : 'env -> ty -> ty = fun _ x -> x
+
     method visit_typed_rvalue : 'env -> typed_rvalue -> typed_rvalue =
       fun _ x -> x
 
     method visit_typed_lvalue : 'env -> typed_lvalue -> typed_lvalue =
       fun _ x -> x
 
-    method visit_let_bindings : 'env -> let_bindings -> let_bindings =
-      fun _ x -> x
-
     method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x
 
     method visit_meta : 'env -> meta -> meta = fun _ x -> x
@@ -340,10 +304,43 @@ class ['self] map_expression_base =
 
     method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
 
-    method visit_var_or_dummy : 'env -> var_or_dummy -> var_or_dummy =
-      fun _ x -> x
+    method visit_fun_id : 'env -> fun_id -> fun_id = fun _ x -> x
   end
 
+type call = {
+  func : fun_id;
+  type_params : ty list;
+  args : typed_rvalue list;
+      (** Note that immediately after we converted the symbolic AST to a pure AST,
+          some functions may have no arguments. For instance:
+          ```
+          fn f();
+          ```
+          We later add a unit argument.
+          
+          TODO: we should use expressions...
+       *)
+  args_mplaces : mplace option list;  (** Meta data *)
+}
+[@@deriving
+  visitors
+    {
+      name = "iter_call";
+      variety = "iter";
+      ancestors = [ "iter_expression_base" ];
+      nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+      concrete = true;
+    },
+    visitors
+      {
+        name = "map_call";
+        variety = "map";
+        ancestors = [ "map_expression_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        concrete = true;
+      }]
+(** "Regular" typed value (we map variables to typed values) *)
+
 (** **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.
@@ -352,12 +349,48 @@ class ['self] map_expression_base =
     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 =
   | Return of typed_rvalue
   | Fail
-  | Let of let_bindings * expression
-      (** Let bindings include the let-bindings introduced because of function calls *)
+  | Value of typed_rvalue * mplace option
+  | Call of call
+  | Let of typed_lvalue * expression * expression
+      (** Let binding.
+      
+          TODO: add a boolean to control whether the let is monadic or not.
+          For instance, in F*:
+          - non-monadic: `let x = ... in ...`
+          - monadic:     `x <-- ...; ...`
+
+          Note that we are quite general for the left-value on purpose; this
+          is used in several situations:
+
+          1. When deconstructing a tuple:
+          ```
+          let (x, y) = p in ...
+          ```
+          (not all languages have syntax like `p.0`, `p.1`... and it is more
+          readable anyway).
+          
+          2. When expanding an enumeration with one variant.
+          
+          In this case, [Deconstruct] has to be understood as:
+          ```
+          let Cons x tl = ls in
+          ...
+          ```
+          
+          Note that later, depending on the language we extract to, we can
+          eventually update it to something like this (for F*, for instance):
+          ```
+          let x = Cons?.v ls in
+          let tl = Cons?.tl ls in
+          ...
+          ```
+       *)
   | Switch of typed_rvalue * mplace option * switch_body
   | Meta of meta * expression  (** Meta-information *)
 
@@ -372,7 +405,7 @@ and match_branch = { pat : typed_lvalue; branch : expression }
     {
       name = "iter_expression";
       variety = "iter";
-      ancestors = [ "iter_expression_base" ];
+      ancestors = [ "iter_call" ];
       nude = true (* Don't inherit [VisitorsRuntime.iter] *);
       concrete = true;
     },
@@ -380,7 +413,7 @@ and match_branch = { pat : typed_lvalue; branch : expression }
       {
         name = "map_expression";
         variety = "map";
-        ancestors = [ "map_expression_base" ];
+        ancestors = [ "map_call" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
       }]