From 58802bdaeef6c4c73cb82427eb0f2c6ca9d9a43a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 13:49:40 +0100
Subject: Start working on to_monadic and make the expression visitors an
 extension of the typed_lvalue visitors

---
 src/Pure.ml            | 96 ++++++++++++++++++++++++++++++++++++--------------
 src/PureMicroPasses.ml | 52 +++++++++++++++++++++++----
 src/SymbolicToPure.ml  |  7 ++++
 3 files changed, 121 insertions(+), 34 deletions(-)

diff --git a/src/Pure.ml b/src/Pure.ml
index 375cdb0f..201ffd74 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -146,13 +146,17 @@ type mplace = { name : string option; projection : projection }
 
 type place = { var : VarId.id; projection : projection }
 
-(** Ancestor for [iter_var_or_dummy] iter visitor *)
+(** Ancestor for [iter_var_or_dummy] visitor *)
 class ['self] iter_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
+    method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
+
     method visit_var : 'env -> var -> unit = fun _ _ -> ()
 
+    method visit_place : 'env -> place -> unit = fun _ _ -> ()
+
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
 
     method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
@@ -163,8 +167,13 @@ class ['self] map_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
+    method visit_constant_value : 'env -> constant_value -> constant_value =
+      fun _ x -> x
+
     method visit_var : 'env -> var -> var = fun _ x -> x
 
+    method visit_place : 'env -> place -> place = fun _ x -> x
+
     method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x
 
     method visit_ty : 'env -> ty -> ty = fun _ x -> x
@@ -175,8 +184,13 @@ class virtual ['self] reduce_value_base =
   object (self : 'self)
     inherit [_] VisitorsRuntime.reduce
 
+    method visit_constant_value : 'env -> constant_value -> 'a =
+      fun _ _ -> self#zero
+
     method visit_var : 'env -> var -> 'a = fun _ _ -> self#zero
 
+    method visit_place : 'env -> place -> 'a = fun _ _ -> self#zero
+
     method visit_mplace : 'env -> mplace -> 'a = fun _ _ -> self#zero
 
     method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero
@@ -261,10 +275,33 @@ and adt_rvalue = {
 }
 
 and typed_rvalue = { value : rvalue; ty : ty }
-(** In most situations we won't use the type in [typed_rvalue].
-    Note that it is still necessary to have some useful informations
-    about ADTs, though.
- *)
+[@@deriving
+  visitors
+    {
+      name = "iter_typed_rvalue";
+      variety = "iter";
+      ancestors = [ "iter_typed_lvalue" ];
+      nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+      concrete = true;
+      polymorphic = false;
+    },
+    visitors
+      {
+        name = "map_typed_rvalue";
+        variety = "map";
+        ancestors = [ "map_typed_lvalue" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        concrete = true;
+        polymorphic = false;
+      },
+    visitors
+      {
+        name = "reduce_typed_rvalue";
+        variety = "reduce";
+        ancestors = [ "reduce_typed_lvalue" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        polymorphic = false;
+      }]
 
 type unop = Not | Neg of T.integer_type
 
@@ -278,18 +315,10 @@ type fun_id =
 (** Meta-information stored in the AST *)
 type meta = Assignment of mplace * typed_rvalue
 
-(** Ancestor for [iter_expression] iter visitor *)
+(** Ancestor for [iter_expression] visitor *)
 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_mplace : 'env -> mplace -> unit = fun _ _ -> ()
+    inherit [_] iter_typed_rvalue
 
     method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
 
@@ -302,20 +331,10 @@ class ['self] iter_expression_base =
     method visit_fun_id : 'env -> fun_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for [map_expression] map visitor *)
+(** Ancestor for [map_expression] visitor *)
 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_mplace : 'env -> mplace -> mplace = fun _ x -> x
+    inherit [_] map_typed_rvalue
 
     method visit_meta : 'env -> meta -> meta = fun _ x -> x
 
@@ -330,6 +349,22 @@ class ['self] map_expression_base =
     method visit_fun_id : 'env -> fun_id -> fun_id = fun _ x -> x
   end
 
+(** Ancestor for [reduce_expression] visitor *)
+class virtual ['self] reduce_expression_base =
+  object (_self : 'self)
+    inherit [_] reduce_typed_rvalue
+
+    method visit_meta : 'env -> meta -> 'a = fun _ _ -> ()
+
+    method visit_integer_type : 'env -> T.integer_type -> 'a = fun _ _ -> ()
+
+    method visit_scalar_value : 'env -> scalar_value -> 'a = fun _ _ -> ()
+
+    method visit_id : 'env -> VariantId.id -> 'a = fun _ _ -> ()
+
+    method visit_fun_id : 'env -> fun_id -> 'a = fun _ _ -> ()
+  end
+
 (** **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.
@@ -416,6 +451,13 @@ and match_branch = { pat : typed_lvalue; branch : expression }
         ancestors = [ "map_expression_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
+      },
+    visitors
+      {
+        name = "reduce_expression";
+        variety = "reduce";
+        ancestors = [ "reduce_expression_base" ];
+        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
       }]
 
 type fun_sig = {
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 9f261386..cb7f5b23 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -7,6 +7,17 @@ open TranslateCore
 (** The local logger *)
 let log = L.pure_micro_passes_log
 
+(** Small utility.
+
+    We sometimes have to insert new fresh variables in a function body, in which
+    case we need to make their indices greater than the indices of all the variables
+    in the body.
+    TODO: things would be simpler if we used a better representation of the
+    variables indices...
+ *)
+let get_expression_min_var_counter (e : expression) : VarId.generator =
+  raise Unimplemented
+
 type pn_ctx = string VarId.Map.t
 (** "pretty-name context": see [compute_pretty_names] *)
 
@@ -266,8 +277,34 @@ let filter_unused_assignments (def : fun_def) : fun_def =
 
 (** Add unit arguments for functions with no arguments, and change their return type. *)
 let to_monadic (def : fun_def) : fun_def =
-  (* TODO *)
-  def
+  (* Update the body *)
+  let obj =
+    object
+      inherit [_] map_expression as super
+
+      method! visit_call env call =
+        (* If no arguments, introduce unit *)
+        if call.args = [] then
+          let args = [ Value (SymbolicToPure.unit_rvalue, None) ] in
+          { call with args } (* Otherwise: nothing to do *)
+        else super#visit_call env call
+    end
+  in
+  let body = obj#visit_expression () def.body in
+  let def = { def with body } in
+
+  (* Update the signature *)
+  if def.inputs = [] then (
+    assert (def.signature.inputs = []);
+    let signature =
+      { def.signature with inputs = [ SymbolicToPure.unit_ty ] }
+    in
+    let var_cnt = get_expression_min_var_counter def.body in
+    let id, _ = VarId.fresh var_cnt in
+    let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in
+    let inputs = [ var ] in
+    { def with signature; inputs })
+  else def
 
 (** Apply all the micro-passes to a function.
 
@@ -296,6 +333,12 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
   let def = remove_meta def in
   log#ldebug (lazy ("remove_meta:\n" ^ fun_def_to_string ctx def));
 
+  (* Add unit arguments for functions with no arguments, and change their return type.
+   * **Rk.**: from now onwards, the types in the AST are correct (until now,
+   * functions had return type `t` where they should have return type `result t`) *)
+  (* let def = to_monadic def in
+     log#ldebug (lazy ("to_monadic:\n" ^ fun_def_to_string ctx def));*)
+
   (* Inline the useless variable reassignments *)
   let def = inline_useless_var_reassignments def in
   log#ldebug
@@ -308,11 +351,6 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
 
   (* TODO: deconstruct the monadic bindings into matches *)
 
-  (* Add unit arguments for functions with no arguments, and change their return type.
-   * TODO: move that at the beginning? *)
-  let def = to_monadic def in
-  log#ldebug (lazy ("to_monadic:\n" ^ fun_def_to_string ctx def));
-
   (* We are done *)
   def
 
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 2279dd06..30142639 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -27,6 +27,13 @@ let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
 
 let mk_tuple_ty (tys : ty list) : ty = Adt (Tuple, tys)
 
+let unit_ty : ty = Adt (Tuple, [])
+
+let unit_rvalue : typed_rvalue =
+  let value = RvAdt { variant_id = None; field_values = [] } in
+  let ty = unit_ty in
+  { value; ty }
+
 let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
   let value = RvPlace (mk_place_from_var v) in
   let ty = v.ty in
-- 
cgit v1.2.3