diff options
Diffstat (limited to '')
| -rw-r--r-- | src/PrintPure.ml | 24 | ||||
| -rw-r--r-- | src/Pure.ml | 52 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 13 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 12 |
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 |