From a96c9e10cec6b8af30dd1c70214ec9b6db66645f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 11:20:47 +0100
Subject: Change the type of [Pure.call.args] to [expression list] rather than
 [typed_rvalue list]

---
 src/PrintPure.ml       | 24 +++++++++++++----------
 src/Pure.ml            | 52 +++++++++++++++-----------------------------------
 src/PureMicroPasses.ml | 13 +++++--------
 src/SymbolicToPure.ml  | 12 ++++++++++--
 4 files changed, 44 insertions(+), 57 deletions(-)

(limited to 'src')

diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 9d28c959..98c832a1 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -353,22 +353,13 @@ let meta_to_string (fmt : ast_formatter) (meta : meta) : string =
   in
   "@meta[" ^ meta ^ "]"
 
-let call_to_string (fmt : ast_formatter) (call : call) : string =
-  let val_fmt = ast_to_value_formatter fmt in
-  let ty_fmt = ast_to_type_formatter fmt in
-  let tys = List.map (ty_to_string ty_fmt) call.type_params in
-  let args = List.map (typed_rvalue_to_string fmt) call.args in
-  let all_args = List.append tys args in
-  let fun_id = fun_id_to_string fmt call.func in
-  if all_args = [] then fun_id else fun_id ^ " " ^ String.concat " " all_args
-
 let rec expression_to_string (fmt : ast_formatter) (indent : string)
     (indent_incr : string) (e : expression) : string =
   match e with
   | Return v -> "return " ^ typed_rvalue_to_string fmt v
   | Fail -> "fail"
   | Value (v, _) -> typed_rvalue_to_string fmt v
-  | Call call -> call_to_string fmt call
+  | Call call -> call_to_string fmt indent indent_incr call
   | Let (lv, re, e) -> let_to_string fmt indent indent_incr lv re e
   | Switch (scrutinee, _, body) ->
       switch_to_string fmt indent indent_incr scrutinee body
@@ -377,6 +368,19 @@ let rec expression_to_string (fmt : ast_formatter) (indent : string)
       let e = expression_to_string fmt indent indent_incr e in
       indent ^ meta ^ "\n" ^ e
 
+and call_to_string (fmt : ast_formatter) (indent : string)
+    (indent_incr : string) (call : call) : string =
+  let val_fmt = ast_to_value_formatter fmt in
+  let ty_fmt = ast_to_type_formatter fmt in
+  let tys = List.map (ty_to_string ty_fmt) call.type_params in
+  (* The arguments are expressions, so this may not be perfect... (though
+   * those expressions will in most cases be values) *)
+  let indent1 = indent ^ indent_incr in
+  let args = List.map (expression_to_string fmt indent indent_incr) call.args in
+  let all_args = List.append tys args in
+  let fun_id = fun_id_to_string fmt call.func in
+  if all_args = [] then fun_id else fun_id ^ " " ^ String.concat " " all_args
+
 and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
     (lv : typed_lvalue) (re : expression) (e : expression) : string =
   let indent1 = indent ^ indent_incr in
diff --git a/src/Pure.ml b/src/Pure.ml
index 64851449..cba0a1f4 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -307,40 +307,6 @@ class ['self] map_expression_base =
     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.
@@ -394,6 +360,19 @@ type expression =
   | Switch of typed_rvalue * mplace option * switch_body
   | Meta of meta * expression  (** Meta-information *)
 
+and call = {
+  func : fun_id;
+  type_params : ty list;
+  args : expression 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.
+       *)
+}
+
 and switch_body =
   | If of expression * expression
   | SwitchInt of T.integer_type * (scalar_value * expression) list * expression
@@ -405,7 +384,7 @@ and match_branch = { pat : typed_lvalue; branch : expression }
     {
       name = "iter_expression";
       variety = "iter";
-      ancestors = [ "iter_call" ];
+      ancestors = [ "iter_expression_base" ];
       nude = true (* Don't inherit [VisitorsRuntime.iter] *);
       concrete = true;
     },
@@ -413,11 +392,10 @@ and match_branch = { pat : typed_lvalue; branch : expression }
       {
         name = "map_expression";
         variety = "map";
-        ancestors = [ "map_call" ];
+        ancestors = [ "map_expression_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
       }]
-(** "Regular" typed value (we map variables to typed values) *)
 
 type fun_sig = {
   type_params : type_var list;
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 4ee67011..80d4e8bf 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -133,11 +133,6 @@ let compute_pretty_names (def : fun_def) : fun_def =
       (ctx : pn_ctx) : pn_ctx =
     match mp with None -> ctx | Some mp -> add_right_constraint mp rv ctx
   in
-  let add_opt_right_constraint_list ctx rvs =
-    List.fold_left
-      (fun ctx (mp, rv) -> add_opt_right_constraint mp rv ctx)
-      ctx rvs
-  in
   let add_left_constraint (lv : typed_lvalue) (ctx : pn_ctx) : pn_ctx =
     let obj =
       object (self)
@@ -171,10 +166,12 @@ let compute_pretty_names (def : fun_def) : fun_def =
     (ctx, Value (v, mp))
   (* *)
   and update_call (call : call) (ctx : pn_ctx) : pn_ctx * expression =
-    let ctx =
-      add_opt_right_constraint_list ctx
-        (List.combine call.args_mplaces call.args)
+    let ctx, args =
+      List.fold_left_map
+        (fun ctx arg -> update_expression arg ctx)
+        ctx call.args
     in
+    let call = { call with args } in
     (ctx, Call call)
   (* *)
   and update_let (lv : typed_lvalue) (re : expression) (e : expression)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index f4b92dff..5c0250f7 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -954,7 +954,10 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             (ctx, Binop (binop, int_ty0))
         | _ -> failwith "Unreachable")
   in
-  let call = { func; type_params; args; args_mplaces } in
+  let args =
+    List.map (fun (arg, mp) -> Value (arg, mp)) (List.combine args args_mplaces)
+  in
+  let call = { func; type_params; args } in
   let call = Call call in
   (* Translate the next expression *)
   let e = translate_expression e ctx in
@@ -1069,7 +1072,12 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       let e = translate_expression e ctx in
       (* Put everything together *)
       let args_mplaces = List.map (fun _ -> None) inputs in
-      let call = { func; type_params; args = inputs; args_mplaces } in
+      let args =
+        List.map
+          (fun (arg, mp) -> Value (arg, mp))
+          (List.combine inputs args_mplaces)
+      in
+      let call = { func; type_params; args } in
       Let (output, Call call, e)
   | V.SynthRet ->
       (* If we end the abstraction which consumed the return value of the function
-- 
cgit v1.2.3