summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-28 11:20:47 +0100
committerSon Ho2022-01-28 11:20:47 +0100
commita96c9e10cec6b8af30dd1c70214ec9b6db66645f (patch)
treedc2cba2fc51e8b8ba50cbabc05f852e8dffe000b
parent4211b52f1dc9dd55512192ff3519d4f58c897963 (diff)
Change the type of [Pure.call.args] to [expression list] rather than
[typed_rvalue list]
-rw-r--r--src/PrintPure.ml24
-rw-r--r--src/Pure.ml52
-rw-r--r--src/PureMicroPasses.ml13
-rw-r--r--src/SymbolicToPure.ml12
4 files changed, 44 insertions, 57 deletions
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