From ea583d9f0f5e4a1a687b70f0e04e875969462157 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 15 Dec 2023 17:20:30 +0100 Subject: Make good progress on updating SymbolicToPure --- compiler/PrintPure.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 2fe5843e..3a5ce513 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -592,6 +592,14 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) in "[ " ^ String.concat ", " fields ^ " ]" | _ -> raise (Failure "Unexpected")) + | Lambda _ -> + let pats, e = destruct_lambdas e in + let vars = + String.concat " " (List.map (typed_pattern_to_string env) pats) + in + let e = texpression_to_string env false indent indent_incr e in + let s = "λ " ^ vars ^ " => " ^ e in + if inside then "(" ^ s ^ ")" else s | Meta (meta, e) -> ( let meta_s = emeta_to_string env meta in let e = texpression_to_string env inside indent indent_incr e in -- cgit v1.3.1 From 955fdab55304979ba2d61432ea654241f20abaa4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 15 Dec 2023 18:14:12 +0100 Subject: Make progress on propagating the changes --- compiler/Extract.ml | 8 ++-- compiler/PrintPure.ml | 16 ++----- compiler/Pure.ml | 3 +- compiler/PureMicroPasses.ml | 110 ++++++++++++++++++++++---------------------- compiler/PureTypeCheck.ml | 8 +--- compiler/PureUtils.ml | 24 +++------- 6 files changed, 72 insertions(+), 97 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1ea26d79..7e2efd8a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -285,9 +285,9 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) | App _ -> let app, args = destruct_apps e in extract_App ctx fmt inside app args - | Abs _ -> - let xl, e = destruct_abs_list e in - extract_Abs ctx fmt inside xl e + | Lambda _ -> + let xl, e = destruct_lambdas e in + extract_Lambda ctx fmt inside xl e | Qualif _ -> (* We use the app case *) extract_App ctx fmt inside e [] @@ -574,7 +574,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) (* No argument: shouldn't happen *) raise (Failure "Unreachable") -and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) +and extract_Lambda (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (xl : typed_pattern list) (e : texpression) : unit = (* Open a box for the abs expression *) F.pp_open_hovbox fmt ctx.indent_incr; diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 3a5ce513..79506c04 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -543,9 +543,9 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) let app, args = destruct_apps e in (* Convert to string *) app_to_string env inside indent indent_incr app args - | Abs _ -> - let xl, e = destruct_abs_list e in - let e = abs_to_string env indent indent_incr xl e in + | Lambda _ -> + let xl, e = destruct_lambdas e in + let e = lambda_to_string env indent indent_incr xl e in if inside then "(" ^ e ^ ")" else e | Qualif _ -> (* Qualifier without arguments *) @@ -592,14 +592,6 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) in "[ " ^ String.concat ", " fields ^ " ]" | _ -> raise (Failure "Unexpected")) - | Lambda _ -> - let pats, e = destruct_lambdas e in - let vars = - String.concat " " (List.map (typed_pattern_to_string env) pats) - in - let e = texpression_to_string env false indent indent_incr e in - let s = "λ " ^ vars ^ " => " ^ e in - if inside then "(" ^ s ^ ")" else s | Meta (meta, e) -> ( let meta_s = emeta_to_string env meta in let e = texpression_to_string env inside indent indent_incr e in @@ -668,7 +660,7 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) (* Add parentheses *) if all_args <> [] && inside then "(" ^ e ^ ")" else e -and abs_to_string (env : fmt_env) (indent : string) (indent_incr : string) +and lambda_to_string (env : fmt_env) (indent : string) (indent_incr : string) (xl : typed_pattern list) (e : texpression) : string = let xl = List.map (typed_pattern_to_string env) xl in let e = texpression_to_string env false indent indent_incr e in diff --git a/compiler/Pure.ml b/compiler/Pure.ml index eb6b00c8..ddacf0c4 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -684,7 +684,7 @@ type expression = field accesses with calls to projectors over fields (when there are clashes of field names, some provers like F* get pretty bad...) *) - | Abs of typed_pattern * texpression (** Lambda abstraction: [fun x -> e] *) + | Lambda of typed_pattern * texpression (** Lambda abstraction: [λ x => e] *) | Qualif of qualif (** A top-level qualifier *) | Let of bool * typed_pattern * texpression * texpression (** Let binding. @@ -728,7 +728,6 @@ type expression = | Switch of texpression * switch_body | Loop of loop (** See the comments for {!loop} *) | StructUpdate of struct_update (** See the comments for {!struct_update} *) - | Lambda of typed_pattern * texpression (** [λ x => e] *) | Meta of (emeta[@opaque]) * texpression (** Meta-information *) and switch_body = If of texpression * texpression | Match of match_branch list diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index d92b3de0..0102b13e 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -385,17 +385,17 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let ctx, arg = update_texpression arg ctx in let e = App (app, arg) in (ctx, e) - | Abs (x, e) -> update_abs x e ctx | Qualif _ -> (* nothing to do *) (ctx, e.e) | Let (monadic, lb, re, e) -> update_let monadic lb re e ctx | Switch (scrut, body) -> update_switch_body scrut body ctx | Loop loop -> update_loop loop ctx | StructUpdate supd -> update_struct_update supd ctx + | Lambda (lb, e) -> update_lambda lb e ctx | Meta (meta, e) -> update_emeta meta e ctx in (ctx, { e; ty }) (* *) - and update_abs (x : typed_pattern) (e : texpression) (ctx : pn_ctx) : + and update_lambda (x : typed_pattern) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = (* We first add the left-constraint *) let ctx = add_left_constraint x ctx in @@ -404,7 +404,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* Update the abstracted value *) let x = update_typed_pattern ctx x in (* Put together *) - (ctx, Abs (x, e)) + (ctx, Lambda (x, e)) (* *) and update_let (monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = @@ -890,12 +890,12 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) let call_is_child = check_call func1 generics1 args1 in if call_is_child then fun () -> true else fun () -> self#visit_texpression env e ()) + | Lambda (_, e) -> self#visit_texpression env e | App _ -> ( fun () -> match opt_destruct_function_call e with | Some (func1, tys1, args1) -> check_call func1 tys1 args1 | None -> false) - | Abs (_, e) -> self#visit_texpression env e | Qualif _ -> (* Note that this case includes functions without arguments *) fun () -> false @@ -975,7 +975,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx) | Var _ | CVar _ | Const _ | App _ | Qualif _ | Switch (_, _) | Meta (_, _) - | StructUpdate _ | Abs _ -> + | StructUpdate _ | Lambda _ -> super#visit_expression env e | Let (monadic, lv, re, e) -> (* Compute the set of values used in the next expression *) @@ -1323,28 +1323,20 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = method! visit_Loop env loop = let fun_sig = def.signature in - let fun_sig_info = fun_sig.info in - let fun_effect_info = fun_sig_info.effect_info in + let fwd_info = fun_sig.fwd_info in + let fwd_effect_info = fwd_info.effect_info in (* TODO: *) assert (not !Config.return_back_funs); (* Generate the loop definition *) - let loop_effect_info = - { - stateful_group = fun_effect_info.stateful_group; - stateful = fun_effect_info.stateful; - can_fail = fun_effect_info.can_fail; - can_diverge = fun_effect_info.can_diverge; - is_rec = fun_effect_info.is_rec; - } - in + let loop_fwd_effect_info = fwd_effect_info in - let loop_sig_info = + let loop_fwd_sig_info : fun_sig_info = let fuel = if !Config.use_fuel then 1 else 0 in let num_inputs = List.length loop.inputs in let fwd_info : inputs_info = - let info = fun_sig_info.fwd_info in + let info = fwd_info.fwd_info in let fwd_state = info.num_inputs_with_fuel_with_state - info.num_inputs_with_fuel_no_state @@ -1358,48 +1350,48 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = } in - { fwd_info; effect_info = loop_effect_info } + { fwd_info; effect_info = loop_fwd_effect_info } in - assert (fun_sig_info_is_wf loop_sig_info); + assert (fun_sig_info_is_wf loop_fwd_sig_info); let inputs_tys = - (* TODO: *) - assert (not !Config.return_back_funs); - let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in let fwd_inputs = List.map (fun (v : var) -> v.ty) loop.inputs in - let info = fun_sig_info.fwd_info in - let state = + let info = fwd_info.fwd_info in + let fwd_state = Collections.List.subslice fun_sig.inputs info.num_inputs_with_fuel_no_state info.num_inputs_with_fuel_with_state in - let _, back_inputs = - Collections.List.split_at fun_sig.inputs - info.num_inputs_with_fuel_with_state + let back_inputs = + if !Config.return_back_funs then [] + else + snd + (Collections.List.split_at fun_sig.inputs + info.num_inputs_with_fuel_with_state) in - List.concat [ fuel; fwd_inputs; state; back_inputs ] + List.concat [ fuel; fwd_inputs; fwd_state; back_inputs ] in - let output, doutputs = + let output = match loop.back_output_tys with | None -> (* Forward function: the return type is the same as the parent function *) - (fun_sig.output, fun_sig.doutputs) + fun_sig.output | Some doutputs -> (* Backward function: custom return type *) let output = mk_simpl_tuple_ty doutputs in let output = - if loop_effect_info.stateful then + if loop_fwd_effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ] else output in let output = - if loop_effect_info.can_fail then mk_result_ty output + if loop_fwd_effect_info.can_fail then mk_result_ty output else output in - (output, doutputs) + output in let loop_sig = @@ -1409,8 +1401,8 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = preds = fun_sig.preds; inputs = inputs_tys; output; - doutputs; - info = loop_sig_info; + fwd_info = loop_fwd_sig_info; + back_effect_info = fun_sig.back_effect_info; } in @@ -1427,7 +1419,8 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = (* Introduce the forward input state *) let fwd_state_var, fwd_state_lvs = assert ( - loop_effect_info.stateful = Option.is_some loop.input_state); + loop_fwd_effect_info.stateful + = Option.is_some loop.input_state); match loop.input_state with | None -> ([], []) | Some input_state -> @@ -1436,11 +1429,9 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = ([ state_var ], [ state_lvs ]) in - (* Introduce the additional backward inputs *) - (* TODO: *) - assert (not !Config.return_back_funs); + (* Introduce the additional backward inputs, if necessary *) let fun_body = Option.get def.body in - let info = fun_sig_info.fwd_info in + let info = fwd_info.fwd_info in let _, back_inputs = Collections.List.split_at fun_body.inputs info.num_inputs_with_fuel_with_state @@ -2063,14 +2054,12 @@ let filter_loop_inputs (transl : pure_fun_translation list) : (* We start by computing the filtering information, for each function *) let compute_one_filter_info (decl : fun_decl) = - (* TODO: *) - assert (not !Config.return_back_funs); (* There should be a body *) let body = Option.get decl.body in (* We only look at the forward inputs, without the state *) let inputs_prefix, _ = Collections.List.split_at body.inputs - decl.signature.info.fwd_info.num_inputs_with_fuel_no_state + decl.signature.fwd_info.fwd_info.num_inputs_with_fuel_no_state in let used = ref (List.map (fun v -> (var_get_id v, false)) inputs_prefix) in let inputs_prefix_length = List.length inputs_prefix in @@ -2089,9 +2078,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) : in (* Set the fuel as used *) - let sg_info = decl.signature.info in - (* TODO: *) - assert (not !Config.return_back_funs); + let sg_info = decl.signature.fwd_info in if sg_info.fwd_info.has_fuel then set_used (fst (Collections.List.nth inputs 0)); @@ -2177,13 +2164,18 @@ let filter_loop_inputs (transl : pure_fun_translation list) : let num_filtered = List.length (List.filter (fun b -> not b) used_info) in - let { generics; llbc_generics; preds; inputs; output; doutputs; info } - = + let { + generics; + llbc_generics; + preds; + inputs; + output; + fwd_info; + back_effect_info; + } = decl.signature in - (* TODO: *) - assert (not !Config.return_back_funs); - let { fwd_info; effect_info } = info in + let { fwd_info; effect_info } = fwd_info in let { has_fuel; @@ -2208,10 +2200,18 @@ let filter_loop_inputs (transl : pure_fun_translation list) : } in - let info = { fwd_info; effect_info } in - assert (fun_sig_info_is_wf info); + let fwd_info = { fwd_info; effect_info } in + assert (fun_sig_info_is_wf fwd_info); let signature = - { generics; llbc_generics; preds; inputs; output; doutputs; info } + { + generics; + llbc_generics; + preds; + inputs; + output; + fwd_info; + back_effect_info; + } in { decl with signature } diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index 3c1800a8..d60d6a05 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -120,7 +120,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = assert (output_ty = e.ty); check_texpression ctx app; check_texpression ctx arg - | Abs (pat, body) -> + | Lambda (pat, body) -> let pat_ty, body_ty = destruct_arrow e.ty in assert (pat.ty = pat_ty); assert (body.ty = body_ty); @@ -229,12 +229,6 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = check_texpression ctx fe) supd.updates | _ -> raise (Failure "Unexpected")) - | Lambda (pat, e_next) -> - assert (e.ty = e_next.ty); - (* Check the pattern and register the introduced variables at the same time *) - let ctx = check_typed_pattern ctx pat in - (* Check the next expression *) - check_texpression ctx e_next | Meta (_, e_next) -> assert (e_next.ty = e.ty); check_texpression ctx e_next diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 80b25641..6e86578c 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -215,8 +215,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig = *) let rec let_group_requires_parentheses (e : texpression) : bool = match e.e with - | Var _ | CVar _ | Const _ | App _ | Abs _ | Qualif _ | StructUpdate _ -> - false + | Var _ | CVar _ | Const _ | App _ | Qualif _ | StructUpdate _ -> false | Let (monadic, _, _, next_e) -> if monadic then true else let_group_requires_parentheses next_e | Switch (_, _) -> false @@ -374,18 +373,6 @@ let opt_destruct_tuple (ty : ty) : ty list option = Some generics.types | _ -> None -let mk_abs (x : typed_pattern) (e : texpression) : texpression = - let ty = TArrow (x.ty, e.ty) in - let e = Abs (x, e) in - { e; ty } - -let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression = - match e.e with - | Abs (x, e') -> - let xl, e'' = destruct_abs_list e' in - (x :: xl, e'') - | _ -> ([], e) - let destruct_arrow (ty : ty) : ty * ty = match ty with | TArrow (ty0, ty1) -> (ty0, ty1) @@ -717,13 +704,16 @@ let type_decl_from_type_id_is_tuple_struct (ctx : TypesAnalysis.type_infos) info.is_tuple_struct | TAssumed _ -> false +let mk_lambda (x : typed_pattern) (e : texpression) : texpression = + let ty = TArrow (x.ty, e.ty) in + let e = Lambda (x, e) in + { e; ty } + let mk_lambda_from_var (var : var) (mp : mplace option) (e : texpression) : texpression = - let ty = TArrow (var.ty, e.ty) in let pat = PatVar (var, mp) in let pat = { value = pat; ty = var.ty } in - let e = Lambda (pat, e) in - { e; ty } + mk_lambda pat e let mk_lambdas_from_vars (vars : var list) (mps : mplace option list) (e : texpression) : texpression = -- cgit v1.3.1 From 999f48d032107722aa6ca714da828ab2788ca412 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Dec 2023 12:06:07 +0100 Subject: Fix a minor mistake in SymbolicToPure --- compiler/PrintPure.ml | 12 +++++++----- compiler/PureMicroPasses.ml | 9 +++++++-- compiler/SymbolicToPure.ml | 5 +---- 3 files changed, 15 insertions(+), 11 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 79506c04..1ce146a4 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -103,10 +103,13 @@ let adt_field_names (env : fmt_env) = Print.Types.adt_field_names (fmt_env_to_llbc_fmt_env env) let option_to_string = Print.option_to_string -let type_var_to_string = Print.Types.type_var_to_string -let const_generic_var_to_string = Print.Types.const_generic_var_to_string -let integer_type_to_string = Print.Values.integer_type_to_string let literal_type_to_string = Print.Values.literal_type_to_string +let type_var_to_string (v : type_var) = "(" ^ v.name ^ ": Type)" + +let const_generic_var_to_string (v : const_generic_var) = + "(" ^ v.name ^ " : " ^ literal_type_to_string v.ty ^ ")" + +let integer_type_to_string = Print.Values.integer_type_to_string let scalar_value_to_string = Print.Values.scalar_value_to_string let literal_to_string = Print.Values.literal_to_string @@ -203,13 +206,12 @@ and trait_instance_id_to_string (env : fmt_env) (inside : bool) | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")" let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string = - let clause_id = trait_clause_id_to_string env clause.clause_id in let trait_id = trait_decl_id_to_string env clause.trait_id in let generics = generic_args_to_strings env true clause.generics in let generics = if generics = [] then "" else " " ^ String.concat " " generics in - "[" ^ clause_id ^ "]: " ^ trait_id ^ generics + trait_id ^ generics let generic_params_to_strings (env : fmt_env) (generics : generic_params) : string list = diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index a7c2f154..34597d32 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -11,6 +11,10 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let fmt = trans_ctx_to_pure_fmt_env ctx in PrintPure.fun_decl_to_string fmt def +let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = + let fmt = trans_ctx_to_pure_fmt_env ctx in + PrintPure.fun_sig_to_string fmt sg + (** Small utility. We sometimes have to insert new fresh variables in a function body, in which @@ -1303,7 +1307,8 @@ let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option = those function bodies into independent definitions while removing occurrences of the {!Pure.Loop} node. *) -let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = +let decompose_loops (_ctx : trans_ctx) (def : fun_decl) : + fun_decl * fun_decl list = match def.body with | None -> (def, []) | Some body -> @@ -1982,7 +1987,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n")); (* Extract the loop definitions by removing the {!Loop} node *) - let def, loops = decompose_loops def in + let def, loops = decompose_loops ctx def in (* Apply the remaining passes *) let f = apply_end_passes_to_def ctx def in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index a79340b6..7359f68a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -950,7 +950,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) let fwd_info = (* *) let has_fuel = fwd_fuel <> [] in - let num_inputs_no_fuel_no_state = List.length fwd_inputs in + let num_inputs_no_fuel_no_state = List.length fwd_inputs_no_fuel_no_state in let num_inputs_with_fuel_no_state = (* We use the fact that [fuel] has length 1 if we use some fuel, 0 otherwise *) List.length fwd_fuel + num_inputs_no_fuel_no_state @@ -2620,9 +2620,6 @@ and translate_forward_end (ectx : C.eval_ctx) (loop_input_values : V.typed_value S.symbolic_value_id_map option) (fwd_e : S.expression) (back_e : S.expression S.region_group_id_map) (ctx : bs_ctx) : texpression = - (* TODO: *) - assert (not !Config.return_back_funs); - let translate_one_end ctx (bid : RegionGroupId.id option) = let ctx = { ctx with bid } in (* Update the current state with the additional state received by the backward -- cgit v1.3.1 From eae740d644f5ccd1ad2a7e853a9cdf303c8df61e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 21 Dec 2023 22:45:47 +0100 Subject: Fix issues when extracting stateful functions --- compiler/PrintPure.ml | 51 +++++++++++++++++++++++----------------------- compiler/SymbolicToPure.ml | 30 +++++++++++++-------------- 2 files changed, 40 insertions(+), 41 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 1ce146a4..315dd512 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -611,35 +611,36 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) * expression *) let app, generics = match app.e with - | Qualif qualif -> + | Qualif qualif -> ( (* Qualifier case *) - (* Convert the qualifier identifier *) - let qualif_s = - match qualif.id with - | FunOrOp fun_id -> fun_or_op_id_to_string env fun_id - | Global global_id -> global_decl_id_to_string env global_id - | AdtCons adt_cons_id -> - let variant_s = - adt_variant_to_string env adt_cons_id.adt_id - adt_cons_id.variant_id - in - ConstStrings.constructor_prefix ^ variant_s - | Proj { adt_id; field_id } -> - let adt_s = adt_variant_to_string env adt_id None in - let field_s = adt_field_to_string env adt_id field_id in - (* Adopting an F*-like syntax *) - ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s - | TraitConst (trait_ref, generics, const_name) -> - let trait_ref = trait_ref_to_string env true trait_ref in - let generics_s = generic_args_to_string env generics in + match qualif.id with + | FunOrOp fun_id -> + let generics = generic_args_to_strings env true qualif.generics in + let qualif_s = fun_or_op_id_to_string env fun_id in + (qualif_s, generics) + | Global global_id -> + let generics = generic_args_to_strings env true qualif.generics in + (global_decl_id_to_string env global_id, generics) + | AdtCons adt_cons_id -> + let variant_s = + adt_variant_to_string env adt_cons_id.adt_id + adt_cons_id.variant_id + in + (ConstStrings.constructor_prefix ^ variant_s, []) + | Proj { adt_id; field_id } -> + let adt_s = adt_variant_to_string env adt_id None in + let field_s = adt_field_to_string env adt_id field_id in + (* Adopting an F*-like syntax *) + (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) + | TraitConst (trait_ref, generics, const_name) -> + let trait_ref = trait_ref_to_string env true trait_ref in + let generics_s = generic_args_to_string env generics in + let qualif = if generics <> empty_generic_args then "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name else trait_ref ^ "." ^ const_name - in - (* Convert the type instantiation *) - let generics = generic_args_to_strings env true qualif.generics in - (* *) - (qualif_s, generics) + in + (qualif, [])) | _ -> (* "Regular" expression case *) let inside = args <> [] || (args = [] && inside) in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 37f621e4..7eb75584 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2782,7 +2782,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) ^ pure_ty_to_string ctx true_e.ty ^ "\n\nfalse_e.ty: " ^ pure_ty_to_string ctx false_e.ty)); - assert (ty = false_e.ty); + if !Config.fail_hard then assert (ty = false_e.ty); { e; ty } | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : @@ -3005,7 +3005,7 @@ and translate_forward_end (ectx : C.eval_ctx) fresh_vars back_sg.inputs_no_state ctx in let ctx, backward_inputs_with_state = - if (ctx_get_effect_info ctx).stateful then + if back_sg.effect_info.stateful then let ctx, var, _ = bs_ctx_fresh_state_var ctx in (ctx, backward_inputs_no_state @ [ var ]) else (ctx, backward_inputs_no_state) @@ -3061,18 +3061,7 @@ and translate_forward_end (ectx : C.eval_ctx) if !Config.return_back_funs then (* Compute the output of the forward function *) let fwd_effect_info = ctx.sg.fwd_info.effect_info in - let output_ty = - let ty = ctx.sg.fwd_output in - if fwd_effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; ty ] - else ty - in - let ctx, fwd_var = fresh_var None output_ty ctx in - let ctx, state_var, state_pat = - if fwd_effect_info.stateful then - let ctx, var, pat = bs_ctx_fresh_state_var ctx in - (ctx, [ var ], [ pat ]) - else (ctx, [], []) - in + let ctx, pure_fwd_var = fresh_var None ctx.sg.fwd_output ctx in let fwd_e = translate_one_end ctx None in (* Introduce the backward functions. *) @@ -3105,10 +3094,19 @@ and translate_forward_end (ectx : C.eval_ctx) let vars = let back_vars = List.filter_map (fun x -> x) back_vars in if ctx.sg.fwd_info.ignore_output then back_vars - else fwd_var :: back_vars + else pure_fwd_var :: back_vars in let vars = List.map mk_texpression_from_var vars in let ret = mk_simpl_tuple_texpression vars in + + (* Introduce a fresh input state variable for the forward expression *) + let _ctx, state_var, state_pat = + if fwd_effect_info.stateful then + let ctx, var, pat = bs_ctx_fresh_state_var ctx in + (ctx, [ var ], [ pat ]) + else (ctx, [], []) + in + let state_var = List.map mk_texpression_from_var state_var in let ret = mk_simpl_tuple_texpression (state_var @ [ ret ]) in let ret = mk_result_return_texpression ret in @@ -3135,7 +3133,7 @@ and translate_forward_end (ectx : C.eval_ctx) back_vars_els ret in (* Bind the expression for the forward output *) - let fwd_var = mk_typed_pattern_from_var fwd_var None in + let fwd_var = mk_typed_pattern_from_var pure_fwd_var None in let pat = mk_simpl_tuple_pattern (state_pat @ [ fwd_var ]) in mk_let fwd_effect_info.can_fail pat fwd_e e else translate_one_end ctx ctx.bid -- cgit v1.3.1 From 70d506d148e5ae1a3e4115034161f449aff666ed Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 22 Dec 2023 21:03:17 +0100 Subject: Fix the output type of the loops backward functions --- compiler/PrintPure.ml | 11 ++------ compiler/Pure.ml | 4 +-- compiler/PureMicroPasses.ml | 25 +++-------------- compiler/PureTypeCheck.ml | 6 ----- compiler/SymbolicToPure.ml | 65 ++++++++++++++++++++++++++++++++++++++++----- 5 files changed, 65 insertions(+), 46 deletions(-) (limited to 'compiler/PrintPure.ml') diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 315dd512..66475d02 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -711,21 +711,14 @@ and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string) ^ String.concat "; " (List.map (var_to_string env) loop.inputs) ^ "]" in - let back_output_tys = - let tys = - match loop.back_output_tys with - | None -> "" - | Some tys -> String.concat "; " (List.map (ty_to_string env false) tys) - in - "back_output_tys: [" ^ tys ^ "]" - in + let output_ty = "output_ty: " ^ ty_to_string env false loop.output_ty in let fun_end = texpression_to_string env false indent2 indent_incr loop.fun_end in let loop_body = texpression_to_string env false indent2 indent_incr loop.loop_body in - "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ back_output_tys ^ "\n" + "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ output_ty ^ "\n" ^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}" diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 71531688..a879ba37 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -754,9 +754,7 @@ and loop = { inputs : var list; inputs_lvs : typed_pattern list; (** The inputs seen as patterns. See {!fun_body}. *) - back_output_tys : ty list option; - (** The types of the given back values, if we ar esynthesizing a backward - function *) + output_ty : ty; (** The output type of the loop *) loop_body : texpression; } diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 67495ab5..e7e9d5e1 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -459,7 +459,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = input_state; inputs; inputs_lvs; - back_output_tys; + output_ty; loop_body; } = loop @@ -478,7 +478,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = input_state; inputs; inputs_lvs; - back_output_tys; + output_ty; loop_body; } in @@ -1498,26 +1498,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) : List.concat [ fuel; fwd_inputs; fwd_state; back_inputs ] in - let output = - match loop.back_output_tys with - | None -> - (* Forward function: the return type is the same as the - parent function *) - fun_sig.output - | Some doutputs -> - (* Backward function: custom return type *) - let output = mk_simpl_tuple_ty doutputs in - let output = - if loop_fwd_effect_info.stateful then - mk_simpl_tuple_ty [ mk_state_ty; output ] - else output - in - let output = - if loop_fwd_effect_info.can_fail then mk_result_ty output - else output - in - output - in + let output = loop.output_ty in let loop_sig = { diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index d60d6a05..a989fd3b 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -188,12 +188,6 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = List.iter check_branch branches) | Loop loop -> assert (loop.fun_end.ty = e.ty); - (* If we translate forward functions, the type of the loop is the same - as the type of the parent expression - in case of backward functions, - the loop doesn't necessarily give back the same values as the parent - function - *) - assert (Option.is_some loop.back_output_tys || loop.loop_body.ty = e.ty); check_texpression ctx loop.fun_end; check_texpression ctx loop.loop_body | StructUpdate supd -> ( diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index cd367d83..bf92482a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3368,7 +3368,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Compute the backward outputs *) let ctx = ref ctx in let rg_to_given_back_tys = - T.RegionGroupId.Map.map + RegionGroupId.Map.map (fun (_, tys) -> (* The types shouldn't contain borrows - we can translate them as forward types *) List.map @@ -3380,10 +3380,63 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = in let ctx = !ctx in - let back_output_tys = - match ctx.bid with - | None -> None - | Some rg_id -> Some (T.RegionGroupId.Map.find rg_id rg_to_given_back_tys) + (* The output type of the loop function *) + let output_ty = + if !Config.return_back_funs then + (* The loop backward functions consume the same additional inputs as the parent + function, but have custom outputs *) + let back_sgs = RegionGroupId.Map.values ctx.sg.back_sg in + let given_back_tys = RegionGroupId.Map.values rg_to_given_back_tys in + let back_tys = + List.filter_map + (fun ((back_sg, given_back) : back_sg_info * ty list) -> + let effect_info = back_sg.effect_info in + (* Compute the input/output types *) + let inputs = List.map snd back_sg.inputs in + let outputs = given_back in + (* Filter if necessary *) + if !Config.simplify_merged_fwd_backs && inputs = [] && outputs = [] + then None + else + let output = mk_simpl_tuple_ty outputs in + let output = + mk_back_output_ty_from_effect_info effect_info inputs output + in + let ty = mk_arrows inputs output in + Some ty) + (List.combine back_sgs given_back_tys) + in + let output = + if ctx.sg.fwd_info.ignore_output then back_tys + else ctx.sg.fwd_output :: back_tys + in + let output = mk_simpl_tuple_ty output in + let effect_info = ctx.sg.fwd_info.effect_info in + let output = + if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ] + else output + in + if effect_info.can_fail && inputs <> [] then mk_result_ty output + else output + else + match ctx.bid with + | None -> + (* Forward function: same type as the parent function *) + (translate_fun_sig_from_decomposed ctx.sg None).output + | Some rg_id -> + (* Backward function: custom return type *) + let doutputs = T.RegionGroupId.Map.find rg_id rg_to_given_back_tys in + let output = mk_simpl_tuple_ty doutputs in + let fwd_effect_info = ctx.sg.fwd_info.effect_info in + let output = + if fwd_effect_info.stateful then + mk_simpl_tuple_ty [ mk_state_ty; output ] + else output + in + let output = + if fwd_effect_info.can_fail then mk_result_ty output else output + in + output in (* Add the loop information in the context *) @@ -3460,7 +3513,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = input_state; inputs; inputs_lvs; - back_output_tys; + output_ty; loop_body; } in -- cgit v1.3.1