From c7af01d1a0375f6addd5c56b54891e5d1cc95c42 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 10 Apr 2026 06:27:08 +0200 Subject: [PATCH 1/5] add tactic 'simplify if' performing if conversion --- src/ecHiTacticals.ml | 5 +- src/ecMatching.ml | 85 ++++++++++---------- src/ecMatching.mli | 6 +- src/ecParser.mly | 7 +- src/ecParsetree.ml | 3 +- src/ecPrinting.ml | 15 ++-- src/phl/ecPhlCodeTx.ml | 171 +++++++++++++++++++++++++++++++++------- src/phl/ecPhlCodeTx.mli | 2 +- 8 files changed, 206 insertions(+), 88 deletions(-) diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 7c6da7e2e..d7fb5eaa4 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -194,6 +194,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Pinterleave info -> EcPhlSwap.process_interleave info | Pcfold info -> EcPhlCodeTx.process_cfold info | Pkill info -> EcPhlCodeTx.process_kill info + | PsimplifyIf info -> EcPhlCodeTx.process_transform_if info | Pasgncase info -> EcPhlCodeTx.process_case info | Palias info -> EcPhlCodeTx.process_alias info | Pset info -> EcPhlCodeTx.process_set info @@ -231,7 +232,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Prepl_stmt infos -> EcPhlTrans.process_equiv_trans infos | Pprocrewrite (s, p, f) -> EcPhlRewrite.process_rewrite s p f | Pprocrewriteat (x, f) -> EcPhlRewrite.process_rewrite_at x f - | Pchangestmt (s, b, p, c) -> EcPhlRewrite.process_change_stmt s b p c + | Pchangestmt (s, b, p, c) -> EcPhlRewrite.process_change_stmt s b p c | Prwprgm infos -> EcPhlRwPrgm.process_rw_prgm infos | Phoaresplit -> EcPhlHoare.process_hoaresplit in @@ -246,7 +247,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | `Gap gap -> Format.fprintf fmt "%a" EcPrinting.(pp_codegap1 ppe) gap | `Instr i -> Format.fprintf fmt "%a" EcPrinting.(pp_codepos1 ppe) i ) is) - + (* -------------------------------------------------------------------- *) and process_sub (ttenv : ttenv) tts tc = diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 66b8d9062..71db06302 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -68,7 +68,7 @@ module Position = struct *) (* Branch selection *) - type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] + type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int] type nm_codepos_brsel = [`Cond of bool | `Match of int] (* Linear code position inside a block *) @@ -141,12 +141,12 @@ module Position = struct let gap_after_pos (cp : codepos1) : codegap1 = GapAfter cp (* Gap -> instr *) - let instr_before_gap (cg : codegap1) : codepos1 = + let instr_before_gap (cg : codegap1) : codepos1 = match cg with | GapAfter cp -> cp | GapBefore cp -> shift1 ~offset:(-1) cp - let instr_after_gap (cg : codegap1) : codepos1 = + let instr_after_gap (cg : codegap1) : codepos1 = match cg with | GapAfter cp -> shift1 ~offset:1 cp | GapBefore cp -> cp @@ -184,7 +184,7 @@ module Position = struct let codegap1_range_of_codepos1 (cp1: codepos1) : codegap1_range = (gap_before_pos cp1, gap_after_pos cp1) - let codegap_range_of_codepos ((cpath, cp1): codepos) : codegap_range = + let codegap_range_of_codepos ((cpath, cp1): codepos) : codegap_range = (cpath, codegap1_range_of_codepos1 cp1) let nm_codegap1_range_of_nm_codepos1 (cp1: nm_codepos1) : nm_codegap1_range = @@ -193,7 +193,7 @@ module Position = struct let nm_codegap_range_of_nm_codepos ((cpath, cp1): nm_codepos) : nm_codegap_range = (cpath, nm_codegap1_range_of_nm_codepos1 cp1) - let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = + let codepos1_of_nm_codepos1 (nm: nm_codepos1) : codepos1 = (0, `ByPos nm) let cpos1_after_last : codepos1 = @@ -209,7 +209,7 @@ module Position = struct let cpos_last : codepos = cpos1_to_top cpos1_last - (* + (* Check that the ranges are valid and then: if either is empty -> true otherwise possibilities are: @@ -218,13 +218,13 @@ module Position = struct 3. s2 <= s1 <= min(e1, e2) => false 4. s2 <= e2 <= s1 <= e1 => true *) - + let disjoint ((s1, e1): nm_codegap1_range) ((s2, e2): nm_codegap1_range) : bool = if s1 > e1 || s2 > e2 then raise InvalidCPos; (s1 = e1) || (s2 = e2) || (* Degenerate case where one of the reanges is empty *) (max s1 s2 >= min e1 e2) (* Otherwise, intersection of (a, b) /\ (c, d) *) (* = (max a c, min b d) *) - (* and this is empty if lower_lim >= upper_lim *) + (* and this is empty if lower_lim >= upper_lim *) let nm_codepos1_in_nm_codegap1_range (cp: nm_codepos1) ((start, fin): nm_codegap1_range) : bool = (start <= cp && cp < fin) @@ -303,7 +303,7 @@ module Position = struct | true -> (List.rev s2, ir, List.rev s1) let exists_match (env: env) (cpm: cp_match) (s: stmt) : bool = - try + try ignore (find_by_cp_match env (None, cpm) s); true with InvalidCPos -> false @@ -331,12 +331,12 @@ module Position = struct if check then check_nm_cpos1 nm s; nm - let normalize_cpos1 ?(check = true) (env: EcEnv.env) ((off, cb): codepos1) (s: stmt) : nm_codepos1 = + let normalize_cpos1 ?(check = true) (env: EcEnv.env) ((off, cb): codepos1) (s: stmt) : nm_codepos1 = let nm = off + normalize_cp_base ~check:false env cb s in (* Make sure the position we are pointing to is valid in the context *) (* List.length points to the position "after the last" and has special meaning depending on the context *) - if check then check_nm_cpos1 nm s; + if check then check_nm_cpos1 nm s; nm let find_and_normalize_cpos1 ?(rev = true) (env : EcEnv.env) (cp1 : codepos1) (s : stmt) = @@ -352,7 +352,13 @@ module Position = struct let indt = oget (EcDecl.tydecl_as_datatype indt) in let cnames = List.fst indt.tydt_ctors in try List.findi (fun _ n -> EcSymbols.sym_equal sel n) cnames |> fst - with Not_found -> raise InvalidCPos + with Not_found -> raise InvalidCPos + + let select_match_arm on_error env e (br:codepos_brsel) = + match br with + | `Match ms -> select_match_arm_idx env e ms + | `MatchByPos ix -> ix + | _ -> on_error () (* Get the block pointed to by brsel for a given instruction *) let normalize_brsel (env: env) (i: instr) (br: codepos_brsel) : (env * stmt) * nm_codepos_brsel = @@ -360,18 +366,14 @@ module Position = struct | (Sif (_, t, _), `Cond true) -> (env, t), `Cond true | (Sif (_, _, f), `Cond false) -> (env, f), `Cond false | (Swhile (_, s), `Cond true) -> (env, s), `Cond true - | (Smatch (e, ss), `Match ms) -> - let ix = select_match_arm_idx env e ms in + | (Smatch (e, ss), _) -> + let ix = select_match_arm (fun _ -> assert false) env e br in let (locals, s) = List.at ss ix in let env = EcEnv.Var.bind_locals locals env in - begin try - (env, s), `Match ix - with Invalid_argument _ -> - raise InvalidCPos - end + (env, s), `Match ix | _ -> assert false - let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt = + let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt = normalize_brsel env i br |> fst |> snd (* Normalizes a code position step and returns the block it points to *) @@ -387,10 +389,10 @@ module Position = struct let (env, s), npath = normalize_cpos_path env cpath s in (env, s), (npath, normalize_cpos1 env cp1 s) - let resolve_offset1_from_cpos1 env (base: nm_codepos1) (off: codeoffset1) (s: stmt) : nm_codepos1 = + let resolve_offset1_from_cpos1 env (base: nm_codepos1) (off: codeoffset1) (s: stmt) : nm_codepos1 = match off with - | `Absolute off -> normalize_cpos1 env off s - | `Relative i -> + | `Absolute off -> normalize_cpos1 env off s + | `Relative i -> let nm = (base + i) in check_nm_cpos1 nm s; nm @@ -572,24 +574,23 @@ module Zipper = struct | Sif (e, ifs1, ifs2), `Cond false -> (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env - | Smatch (e, bs), `Match cn -> - let ix = select_match_arm_idx env e cn in + | Smatch (e, bs), _ -> + let ix = select_match_arm (fun () -> raise InvalidCPos) env e sub in let prebr, (locals, body), postbr = List.pivot_at ix bs in let env = EcEnv.Var.bind_locals locals env in (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env - | _ -> raise InvalidCPos in zpr, ((List.length s1), step), env let pre_zipper_of_codepos_path (env : EcEnv.env) (cpath: codepos_path) (s: stmt) = List.fold_left_map - (fun ((zpr, s), env) cps -> + (fun ((zpr, s), env) cps -> let (zpr, s), step, env = zipper_step_into_block env cps s zpr in ((zpr, s), env), step) - ((ZTop, s), env) cpath + ((ZTop, s), env) cpath let zipper_of_cgap_r (env : EcEnv.env) ((cpath, cp1) : codegap) (s : stmt) = let ((zpr, s), env), nmcp = pre_zipper_of_codepos_path env cpath s in - + let nm = normalize_cgap1 env cp1 s in let s1, s2 = split_at_nmcgap1 nm s in let zpr = zipper ~env (List.rev s1) s2 zpr in @@ -604,12 +605,12 @@ module Zipper = struct let zipper_of_cgap (env : EcEnv.env) (cp : codegap) (s : stmt) = fst (zipper_of_cgap_r env cp s) - (* + (* * Returns: * - A zipper pointing to the start of the range - * - A split of the block according to the range + * - A split of the block according to the range * - The normalized cpos range - *) + *) let zipper_and_split_of_cgap_range (env: env) (path, (start, fin) : codegap_range) (s: stmt) : zipper * _ * nm_codegap_range = let (zpr, ((cpath, _), s)) = zipper_of_cgap_r env (path, start) s in let start = normalize_cgap1 env start s in @@ -1026,9 +1027,9 @@ let f_match_core opts hyps (ue, ev) f1 f2 = if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then failure (); let subst = - if id_equal hf1.hf_m hf2.hf_m then + if id_equal hf1.hf_m hf2.hf_m then subst - else + else Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs)); let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in @@ -1052,9 +1053,9 @@ let f_match_core opts hyps (ue, ev) f1 f2 = if hf1.bhf_cmp <> hf2.bhf_cmp then failure (); let subst = - if id_equal hf1.bhf_m hf2.bhf_m then + if id_equal hf1.bhf_m hf2.bhf_m then subst - else + else Fsubst.f_bind_mem subst hf1.bhf_m hf2.bhf_m in assert (not (Mid.mem hf1.bhf_m mxs) && not (Mid.mem hf2.bhf_m mxs)); let mxs = Mid.add hf1.bhf_m hf2.bhf_m mxs in @@ -1069,16 +1070,16 @@ let f_match_core opts hyps (ue, ev) f1 f2 = if not (EcReduction.EqTest.for_xp env hf1.ef_fr hf2.ef_fr) then failure(); let subst = - if id_equal hf1.ef_ml hf2.ef_ml then + if id_equal hf1.ef_ml hf2.ef_ml then subst - else + else Fsubst.f_bind_mem subst hf1.ef_ml hf2.ef_ml in assert (not (Mid.mem hf1.ef_ml mxs) && not (Mid.mem hf2.ef_ml mxs)); let mxs = Mid.add hf1.ef_ml hf2.ef_ml mxs in let subst = - if id_equal hf1.ef_mr hf2.ef_mr then + if id_equal hf1.ef_mr hf2.ef_mr then subst - else + else Fsubst.f_bind_mem subst hf1.ef_mr hf2.ef_mr in assert (not (Mid.mem hf1.ef_mr mxs) && not (Mid.mem hf2.ef_mr mxs)); let mxs = Mid.add hf1.ef_mr hf2.ef_mr mxs in @@ -1094,9 +1095,9 @@ let f_match_core opts hyps (ue, ev) f1 f2 = doit env (subst, mxs) pr1.pr_args pr2.pr_args; let ev1, ev2 = pr1.pr_event, pr2.pr_event in let subst = - if id_equal ev1.m ev2.m then + if id_equal ev1.m ev2.m then subst - else + else Fsubst.f_bind_mem subst ev1.m ev2.m in assert (not (Mid.mem ev1.m mxs) && not (Mid.mem ev2.m mxs)); let mxs = Mid.add ev1.m ev2.m mxs in diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 6a912ffb7..1f9e8a64d 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -31,7 +31,7 @@ module Position : sig ] (* Branch selection *) - type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol] + type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int] type nm_codepos_brsel = [`Cond of bool | `Match of int] (* Linear code position inside a block *) @@ -58,7 +58,7 @@ module Position : sig (* Top-level first and last position *) val cpos_first : codepos val cpos_last : codepos - + (* Block-level first and last position *) val cpos1_first : codepos1 val cpos1_last : codepos1 @@ -94,7 +94,7 @@ module Position : sig val normalize_cpos1 : ?check:bool -> env -> codepos1 -> stmt -> nm_codepos1 - val resolve_offset1_from_cpos1 : env -> nm_codepos1 -> codeoffset1 -> stmt -> nm_codepos1 + val resolve_offset1_from_cpos1 : env -> nm_codepos1 -> codeoffset1 -> stmt -> nm_codepos1 val find_by_cpos1 : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list diff --git a/src/ecParser.mly b/src/ecParser.mly index 6d6b1f9ac..db998b5df 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2635,11 +2635,11 @@ s_codegap1_before_(I): | LBRACKET cps=codepos1 DOTDOT cpe=codepos1 RBRACKET { (GapBefore cps, GapAfter cpe) } -| LBRACKET cps=codepos1 PLUSGT cpo=loc(mparen(sword)) RBRACKET { +| LBRACKET cps=codepos1 PLUSGT cpo=loc(mparen(sword)) RBRACKET { if unloc cpo > 0 then begin let (offset, base) = cps in (GapBefore cps, GapAfter (offset + unloc cpo, base)) - end else + end else parse_error (loc cpo) (Some "cannot give negative offset for codepos range end") } @@ -3112,6 +3112,9 @@ direction: | ALIAS s=side? x=lident CEQ p=sform_h AT o=codepos { Psetmatch (s, o, x, p) } +| SIMPLIFY IF s=side? o=codepos? + { PsimplifyIf (s, o) } + | WEAKMEM s=side? h=loc(ipcore_name) p=param_decl { Pweakmem(s, h, p) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index ce01073ca..306489973 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -60,7 +60,7 @@ type pcp_base = [ type pbranch_select = [`Cond of bool | `Match of psymbol] type pcodepos1 = int * pcp_base type pcodepos_step = (pcodepos1 * pbranch_select) -type pcodepos_path = pcodepos_step list +type pcodepos_path = pcodepos_step list type pcodepos = pcodepos_path * pcodepos1 type pdocodepos1 = pcodepos1 doption option @@ -802,6 +802,7 @@ type phltactic = | Poutline of outline_info | Pinterleave of interleave_info located | Pkill of (oside * pcodepos * int option) + | PsimplifyIf of (oside * pcodepos option) | Pasgncase of (oside * pcodepos) | Prnd of oside * psemrndpos option * rnd_tac_info_f | Prndsem of bool * oside * pcodegap1 diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index cbe75ad3f..1278e9a04 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2465,14 +2465,15 @@ let pp_codeoffset1 (ppe : PPEnv.t) (fmt : Format.formatter) (offset : CP.codeoff | `Absolute p -> Format.fprintf fmt "%a" (pp_codepos1 ppe) p | `Relative o -> Format.fprintf fmt "%d" o -let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) = +let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) = Format.fprintf fmt "%s" (match br with | `Cond true -> "." | `Cond false -> "?" - | `Match cp -> Format.sprintf "#%s." cp) + | `Match cp -> Format.sprintf "#%s." cp + | `MatchByPos ix -> Format.sprintf "#%i" ix) -let pp_codepos_step (ppe: PPEnv.t) (fmt: Format.formatter) ((cp, br): CP.codepos_step) = +let pp_codepos_step (ppe: PPEnv.t) (fmt: Format.formatter) ((cp, br): CP.codepos_step) = Format.fprintf fmt "%a%a" (pp_codepos1 ppe) cp pp_codepos_brsel br let pp_codepos_path ppe = @@ -2491,16 +2492,16 @@ let pp_codegap1 (ppe : PPEnv.t) (fmt : Format.formatter) (g : CP.codegap1) = let pp_codegap (ppe : PPEnv.t) (fmt : Format.formatter) ((cpath, g1) : CP.codegap) = Format.fprintf fmt "%a%a" (pp_codepos_path ppe) cpath (pp_codegap1 ppe) g1 -let symbol_and_codepos1_of_codegap1_range_edge (cg: CP.codegap1) : symbol * CP.codepos1 = +let symbol_and_codepos1_of_codegap1_range_edge (cg: CP.codegap1) : symbol * CP.codepos1 = match cg with | GapBefore cp -> "[", cp | GapAfter cp -> "]", cp (* -------------------------------------------------------------------- *) let pp_codegap1_range (ppe: PPEnv.t) (fmt: Format.formatter) ((start, fin) : CP.codegap1_range) = - let s, cps = symbol_and_codepos1_of_codegap1_range_edge start in - let e, cpe = symbol_and_codepos1_of_codegap1_range_edge fin in - Format.fprintf fmt "%s%a;%a%s" s (pp_codepos1 ppe) cps (pp_codepos1 ppe) cpe e + let s, cps = symbol_and_codepos1_of_codegap1_range_edge start in + let e, cpe = symbol_and_codepos1_of_codegap1_range_edge fin in + Format.fprintf fmt "%s%a;%a%s" s (pp_codepos1 ppe) cps (pp_codepos1 ppe) cpe e (* FIXME: change when we can change the syntax *) let pp_codegap_range (ppe: PPEnv.t) (fmt: Format.formatter) ((cpath, cp1r) : CP.codegap_range) = diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index 5d49a34fc..0e1d49fee 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -255,7 +255,7 @@ let cfold_stmt promoted into the propagated substitution. *) let for_instruction (subst, preserve: (expr, unit) Mpv.t * (PV.t Mnpv.t)) (i : instr) = - let esubst subst e = + let esubst subst e = EcPV.Mpv.esubst env subst e |> e_simplify in let isubst subst i = @@ -275,9 +275,9 @@ let cfold_stmt (* are automatically preserved by construction *) let update_preserved preserve subst pv e = let rd = EcPV.e_read env e in - let rd = List.fold_left (fun rd pv -> - EcPV.PV.remove env pv rd - ) rd (propagated_pvs subst) + let rd = List.fold_left (fun rd pv -> + EcPV.PV.remove env pv rd + ) rd (propagated_pvs subst) in Mnpv.add pv rd preserve in @@ -291,55 +291,55 @@ let cfold_stmt in match i.i_node with - | Sasgn (lv, e) -> + | Sasgn (lv, e) -> let asgns = explode_assgn lv e in let exception Abort in - begin try + begin try let (subst, preserve), asgns = List.fold_left_map (fun (subst, preserve) ((pv, t), e) -> (* 1. When hitting an assignment to a preserved var *) - if is_preserved preserve pv then + if is_preserved preserve pv then if eager (* 1.1 Promote to propagated on eager *) - then + then let e = esubst subst e in promote_preserved_to_propagated subst preserve pv e, None else raise Abort (* 1.2 Fail on non-eager *) - else + else (* 2. When not preserved and not propagated, do nothing *) - if not (is_propagated subst pv) then + if not (is_propagated subst pv) then (subst, preserve), Some ((pv, t), esubst subst e) (* 3. When propagated, propagate *) - else + else let e = esubst subst e in let preserve = update_preserved preserve subst pv e in let subst = Mpv.add env pv e subst in (subst, preserve), None ) (subst, preserve) asgns - in + in let asgns = List.filter_map identity asgns in `Continue ((subst, preserve), Option.to_list (i_asgn_of_pve asgns)) with Abort -> `Interrupt end - | Srnd _ - | Scall _ - | Swhile _ - | Sif _ - | Smatch _ -> + | Srnd _ + | Scall _ + | Swhile _ + | Sif _ + | Smatch _ -> let wr = EcPV.i_write env i in let spvs = Mnpv.keys (Mpv.pvs subst) in let ppvs = Mnpv.keys preserve in - if - let check = List.for_all (fun pv -> + if + let check = List.for_all (fun pv -> not @@ EcPV.PV.mem_pv env pv wr) in check spvs && check ppvs then `Continue ((subst, preserve), [isubst subst i]) - else + else `Interrupt | Sraise _ -> `Interrupt - | Sabstract id -> + | Sabstract id -> let aus = EcEnv.AbsStmt.byid id env in begin match aus with | { aus_calls = []; aus_reads; aus_writes } -> @@ -367,22 +367,22 @@ let cfold_stmt | { i_node = Sasgn (lv, e) } :: is -> let asgns = explode_assgn lv e in let lv = List.fst asgns in - + if not (List.for_all (is_loc -| fst) lv) then tc_error pf "left-values must be made of local variables only"; - (* Variables in the domain of substs + (* Variables in the domain of substs are variables to be propagated *) let subst = List.fold_left (fun subst ((pv, _), e) -> Mpv.add env pv e subst) Mpv.empty asgns in - let preserve = - List.fold_left - (fun preserve ((pv, _), e) -> - Mnpv.add - pv + let preserve = + List.fold_left + (fun preserve ((pv, _), e) -> + Mnpv.add + pv EcPV.(PV.remove env pv (e_read env e)) preserve) Mnpv.empty @@ -398,7 +398,7 @@ let cfold_stmt tc_error pf "cannot find a left-value assignment at given position" in - let asgns = Mnpv.bindings (Mpv.pvs subst) in + let asgns = Mnpv.bindings (Mpv.pvs subst) in let lv, es = List.map (fun (pv, e) -> (pv, e_ty e), e) asgns |> List.split @@ -424,7 +424,7 @@ let t_cfold = let tr = fun side -> `Fold (side, cpos, olen) in let cb = fun cenv _ me zpr -> cfold_stmt ~eager cenv me olen zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) tc + t_code_transform side ~bdhoare:true cpos tr (t_zip cb) tc (* -------------------------------------------------------------------- *) let t_kill = FApi.t_low3 "code-tx-kill" t_kill_r @@ -556,3 +556,114 @@ let process_case ((side, pos) : side option * pcodepos) (tc : tcenv1) = let concl = EcLowPhlGoal.hl_set_stmt side concl s in FApi.xmutate1 tc `ProcCase (goals @ [concl]) + + + +(* ---------------------------------------------------------------------- *) + +let transform_if (env:EcEnv.env) (e : expr) (s1 : stmt) (s2 : stmt) = + let mod1 = s_write env s1 in + let mod2 = s_write env s2 in + let modv, modg = PV.elements (PV.union mod1 mod2) in + assert (modg = []); + if modv = [] then [] + else + let upd (m : (expr, unit) Mpv.t) (x:prog_var) (e:expr) = + Mpv.add env x e (Mpv.remove env x m) in + let init = + List.fold_left (fun m (x,ty) -> Mpv.add env x (e_var x ty) m) Mpv.empty modv in + + let transform_v m (x, ty) = + let x' = EcIdent.create (symbol_of_pv x) in + upd m x (e_local x' ty), (x', ty) in + + let transform_lv m lv = + match lv with + | LvVar (x, ty) -> + let m, (x', ty) = transform_v m (x, ty) in + m, LSymbol (x', ty) + | LvTuple xs -> + let m, xs' = List.map_fold transform_v m xs in + m, LTuple xs' in + + let transform_i m i = + let lv, e = destr_asgn i in + let e = Mpv.esubst env m e in + let m, lp = transform_lv m lv in + m, (lp, e) in + + let transform_s (s:stmt) = List.map_fold transform_i init s.s_node in + + let m1, bd1 = transform_s s1 in + let m2, bd2 = transform_s s2 in + let es = + let e_if (x,ty) = + let ex = e_var x ty in + e_if e (Mpv.esubst env m1 ex) (Mpv.esubst env m2 ex) in + e_tuple (List.map e_if modv) in + let add_binding bd es = + List.fold_right (fun (lp,e) es -> e_let lp e es) bd es in + let es = add_binding bd1 (add_binding bd2 es) in + [i_asgn (oget (lv_of_list modv), es)] + +let transform_if_stmt env (pf, _) me i = + match i.i_node with + | Sif (e, s1, s2) -> + if not (List.for_all is_asgn s1.s_node) then + tc_error pf "the then branch contains intruction that are not assignments"; + if not (List.for_all is_asgn s2.s_node) then + tc_error pf "the else branch contains intruction that are not assignments"; + (me, transform_if env e s1 s2) + | _ -> tc_error pf "the given position does not correspond to an if instruction" + +let t_transform_if_r side cpos g = + let env = FApi.tc1_env g in + let tr = fun side -> `TransformIf (side, cpos) in + t_code_transform side ~bdhoare:true cpos tr (t_fold (transform_if_stmt env)) g + +let t_transform_if = FApi.t_low2 "code-tx-transform_if" t_transform_if_r + +let find_pos (test : instr -> bool) (s:stmt) = + let exception Found of Position.codepos in + let rec find_pos rpath n (s:instr list) = + match s with + | [] -> () + | i :: s -> + if test i then raise (Found (List.rev rpath, Position.cpos1 n)); + find_pos_sub rpath n i; + find_pos rpath (n+1) s + + and find_pos_sub rpath n i = + match i.i_node with + | Sif (_, s1, s2) -> + find_pos ((Position.cpos1 n,`Cond true)::rpath) 0 s1.s_node; + find_pos ((Position.cpos1 n,`Cond false)::rpath) 0 s2.s_node + | Swhile (_, s) -> + find_pos ((Position.cpos1 n,`Cond true)::rpath) 0 s.s_node; + | Smatch(_, bs) -> + List.iteri (fun i (_, s) -> + find_pos ((Position.cpos1 n,`MatchByPos i)::rpath) 0 s.s_node) bs + | _ -> () in + try find_pos [] 0 s.s_node; None + with Found r -> Some r + +let t_transform_if_rec1 side g = + let (_, s) = tc1_get_stmt side g in + let test i = + match i.i_node with + | Sif (_, s1, s2) -> + List.for_all is_asgn s1.s_node && List.for_all is_asgn s2.s_node + | _ -> false in + match find_pos test s with + | Some cpos -> t_transform_if side cpos g + | None -> tc_error (!!g) "no more transformation" + +let t_transform_if_rec side g = + FApi.t_repeat (t_transform_if_rec1 side) g + +let process_transform_if (side, cpos) tc = + match cpos with + | None -> t_transform_if_rec side tc + | Some cpos -> + let cpos = EcLowPhlGoal.tc1_process_codepos tc (side, cpos) in + t_transform_if side cpos tc diff --git a/src/phl/ecPhlCodeTx.mli b/src/phl/ecPhlCodeTx.mli index 468b4b056..3bbd6e1cf 100644 --- a/src/phl/ecPhlCodeTx.mli +++ b/src/phl/ecPhlCodeTx.mli @@ -21,6 +21,6 @@ val process_set : oside * pcodepos * bool * psymbol * pexpr -> backward val process_set_match : oside * pcodepos * psymbol * pformula -> backward val process_cfold : pcfold -> backward val process_case : oside * pcodepos -> backward - +val process_transform_if : oside * pcodepos option -> backward (* -------------------------------------------------------------------- *) val process_weakmem : (oside * psymbol * fun_params) -> backward From 2fe90eead0345465e49581ebee734f6b88aa5d1e Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 10 Apr 2026 09:12:18 +0200 Subject: [PATCH 2/5] add documentation --- doc/tactics/simplify-if.rst | 134 ++++++++++++++++++++++++++++++++ examples/tactics/simplify_if.ec | 62 +++++++++++++++ 2 files changed, 196 insertions(+) create mode 100644 doc/tactics/simplify-if.rst create mode 100644 examples/tactics/simplify_if.ec diff --git a/doc/tactics/simplify-if.rst b/doc/tactics/simplify-if.rst new file mode 100644 index 000000000..8415ab8fb --- /dev/null +++ b/doc/tactics/simplify-if.rst @@ -0,0 +1,134 @@ +======================================================================== +Tactic: `simplify if` +======================================================================== + +The `simplify if` performs an if-conversion on program statement, +i.e it transform if statement into if expression. This transformation preserves the semantics. +This allows to obtain a statement where the weakest precondition does not grow +exponentially in the number of if. + +To illustrate the problem here is an example that show how grow the weakest pre-condition: +.. ecproof:: + :title: Weakest pre-condition grow exponentially. + + require import AllCore. + + module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } + }. + + hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). + proof. + proc. + unroll for ^while. + (*$*) time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *) + skip. + move => />. + smt(). + qed. + +.. admonition:: Syntax + + Since the tactic preserves the semantic it applies to all program logics. + + `simplify if side? codepos?` + + The `side` argument is required when the goal is a `equiv` judgment, it allows to select + on which side you want to apply the program transformation. The `codepos` argument allows + to specify on which `if` instruction you want to apply the transformation. + + +.. contents:: + :local: + +------------------------------------------------------------------------ +Variant: Transform at a given code possition +------------------------------------------------------------------------ +The tactic applies only if the branches of selected the `if` instruction are only composed of +assignment. + +.. exproof:: + : title: Hoare logic example selecting where to apply the transformation + require import AllCore. + + module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } + }. + + hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). + proof. + proc. + unroll for ^while. + (* You can select a particular occurence of if using codepos *) + (*$*) simplify if ^if. (* Apply the transformation on the first if *) + simplify if ^if{2}. (* Apply the transformation on the second if *) + simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *) + time wp. + skip. + move => />. + smt(). + qed. + +------------------------------------------------------------------------ +Variant: Transform as much as possible +------------------------------------------------------------------------ + +.. admonition:: Syntax + + `simplify if` + +This variant try to find a position where the transformation is possible and applies it. +This is repeated until no position is found. + +.. ecproof:: + :title: Hoare logic example + + require import AllCore. + + module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } + }. + + hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). + proof. + proc. + unroll for ^while. + (*$*)simplify if. (* if instruction are transformed into single assignment *) + time wp. (* The size of the wp is now linear in the number of instruction *) + skip. + move => />. + smt(). + qed. diff --git a/examples/tactics/simplify_if.ec b/examples/tactics/simplify_if.ec new file mode 100644 index 000000000..f187901a5 --- /dev/null +++ b/examples/tactics/simplify_if.ec @@ -0,0 +1,62 @@ +require import AllCore. + +module M = { + proc f (j:int) : int * int = { + var i, x, y; + x <- 0; + y <- 0; + i <- 0; + while (i < 6) { + if (i = j) x <- i; + else y <- y + i; + i <- i + 1; + } + return (x, y); + } +}. + +hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). +proof. + proc. + unroll for ^while. + time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *) + skip. + move => />. + smt(). +qed. + +hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). +proof. + proc. + unroll for ^while. + simplify if. (* if instruction are transformed into single assignment *) + time wp. (* The size of the wp is now linear in the number of instruction *) + skip. + move => />. + smt(). +qed. + +hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15). +proof. + proc. + unroll for ^while. + (* You can select a particular occurence of if using codepos *) + simplify if ^if. (* Apply the transformation on the first if *) + simplify if ^if{2}. (* Apply the transformation on the second if *) + simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *) + time wp. + skip. + move => />. + smt(). +qed. + + + + + + + + + + + From 00518af088739bd8f4f0c39346b93ec83ab0d668 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 10 Apr 2026 15:26:14 +0200 Subject: [PATCH 3/5] improve doc --- doc/tactics/simplify-if.rst | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/doc/tactics/simplify-if.rst b/doc/tactics/simplify-if.rst index 8415ab8fb..86275a8df 100644 --- a/doc/tactics/simplify-if.rst +++ b/doc/tactics/simplify-if.rst @@ -2,15 +2,18 @@ Tactic: `simplify if` ======================================================================== -The `simplify if` performs an if-conversion on program statement, -i.e it transform if statement into if expression. This transformation preserves the semantics. -This allows to obtain a statement where the weakest precondition does not grow -exponentially in the number of if. +The `simplify if` transformation performs an if-conversion on program statements, +i.e., it rewrites `if` statements into conditional expressions. This transformation +preserves the program semantics. -To illustrate the problem here is an example that show how grow the weakest pre-condition: -.. ecproof:: - :title: Weakest pre-condition grow exponentially. +This conversion helps prevent the weakest precondition from growing exponentially +with the number of `if` statements. + +To illustrate this issue, consider the following example, which shows how the +weakest precondition can grow exponentially: +.. ecproof:: + :title: Weakest precondition grows exponentially. require import AllCore. module M = { @@ -39,15 +42,14 @@ To illustrate the problem here is an example that show how grow the weakest pre- qed. .. admonition:: Syntax - - Since the tactic preserves the semantic it applies to all program logics. + Since the tactic preserves semantics, it can be applied to all program logics. `simplify if side? codepos?` - The `side` argument is required when the goal is a `equiv` judgment, it allows to select - on which side you want to apply the program transformation. The `codepos` argument allows - to specify on which `if` instruction you want to apply the transformation. - + The `side` argument is required when the goal is an `equiv` judgment; it specifies +on which side the transformation should be applied. + The `codepos` argument allows you to indicate which `if` statement the transformation +should target. .. contents:: :local: @@ -55,9 +57,8 @@ To illustrate the problem here is an example that show how grow the weakest pre- ------------------------------------------------------------------------ Variant: Transform at a given code possition ------------------------------------------------------------------------ -The tactic applies only if the branches of selected the `if` instruction are only composed of -assignment. - +The tactic applies only if the branches of the selected `if` statement consist solely of +assignments. .. exproof:: : title: Hoare logic example selecting where to apply the transformation require import AllCore. @@ -99,8 +100,8 @@ Variant: Transform as much as possible `simplify if` -This variant try to find a position where the transformation is possible and applies it. -This is repeated until no position is found. +This variant attempts to find a position where the transformation can be applied and +applies it. The process is repeated until no applicable position remains. .. ecproof:: :title: Hoare logic example From c7dc1ec4e7aff1fe6ef4e95bf7c3b77ec34e74b0 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 10 Apr 2026 17:23:47 +0200 Subject: [PATCH 4/5] fix documentation --- doc/tactics/simplify-if.rst | 18 +++++++++++------- flake.nix | 2 +- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/doc/tactics/simplify-if.rst b/doc/tactics/simplify-if.rst index 86275a8df..890f9e396 100644 --- a/doc/tactics/simplify-if.rst +++ b/doc/tactics/simplify-if.rst @@ -14,6 +14,7 @@ weakest precondition can grow exponentially: .. ecproof:: :title: Weakest precondition grows exponentially. + require import AllCore. module M = { @@ -41,14 +42,15 @@ weakest precondition can grow exponentially: smt(). qed. +Since the tactic preserves semantics, it can be applied to all program logics. + .. admonition:: Syntax - Since the tactic preserves semantics, it can be applied to all program logics. - `simplify if side? codepos?` + `simplify if side? codepos?` - The `side` argument is required when the goal is an `equiv` judgment; it specifies +The `side` argument is required when the goal is an `equiv` judgment; it specifies on which side the transformation should be applied. - The `codepos` argument allows you to indicate which `if` statement the transformation +The `codepos` argument allows you to indicate which `if` statement the transformation should target. .. contents:: @@ -59,8 +61,10 @@ Variant: Transform at a given code possition ------------------------------------------------------------------------ The tactic applies only if the branches of the selected `if` statement consist solely of assignments. -.. exproof:: - : title: Hoare logic example selecting where to apply the transformation + +.. ecproof:: + :title: Hoare logic example selecting where to apply the transformation. + require import AllCore. module M = { @@ -104,7 +108,7 @@ This variant attempts to find a position where the transformation can be applied applies it. The process is repeated until no applicable position remains. .. ecproof:: - :title: Hoare logic example + :title: Hoare logic example. require import AllCore. diff --git a/flake.nix b/flake.nix index 77d38a85f..7af701ad4 100644 --- a/flake.nix +++ b/flake.nix @@ -107,7 +107,7 @@ buildInputs = devPackages ++ [ pkgs.git scope'.why3 packages.provers ] - ++ (with pkgs.python3Packages; [ pyyaml ]); + ++ (with pkgs.python3Packages; [ pyyaml pip ]); }; }); } From 660bf07734fe961e173ad1ab1c88084b481a07fe Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 10 Apr 2026 17:24:22 +0200 Subject: [PATCH 5/5] remove unused argument extend t_code_transform to ehoare --- src/ecLowPhlGoal.ml | 21 +++++++++++++-------- src/phl/ecPhlCodeTx.ml | 12 ++++++------ src/phl/ecPhlLoopTx.ml | 8 ++++---- 3 files changed, 23 insertions(+), 18 deletions(-) diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 63da6bf64..416bb1562 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -789,7 +789,7 @@ let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) ((me, Zpr.zip zpr, gs) : memenv * _ * form list) with InvalidCPos -> tc_error (fst cenv) "invalid code position" -let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc = +let t_code_transform (side : oside) cpos tr tx tc = let pf = FApi.tc1_penv tc in match side with @@ -799,27 +799,32 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc = match concl.f_node with | FhoareS hs -> let pr, po = hs_pr hs, hs_po hs in + (* FIXME: This is very suspicious why only main is provided ? *) let po = po.hsi_inv.main in let (me, stmt, cs) = tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in let concl = - f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs) + f_hoareS (snd me) pr stmt (hs_po hs) in FApi.xmutate1 tc (tr None) (cs @ [concl]) - | FbdHoareS bhs when bdhoare -> + | FbdHoareS bhs -> let pr, po = bhs_pr bhs, bhs_po bhs in let (me, stmt, cs) = tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in - let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs) - bhs.bhs_cmp (bhs_bd bhs) in + let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in + FApi.xmutate1 tc (tr None) (cs @ [concl]) + + | FeHoareS ehs -> + let pr, po = ehs_pr ehs, ehs_po ehs in + let (me, stmt, cs) = + tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in + let concl = f_eHoareS (snd me) pr stmt po in FApi.xmutate1 tc (tr None) (cs @ [concl]) | _ -> let kinds = - (if bdhoare then [`PHoare `Stmt] else []) - @ [`Hoare `Stmt] in - + [`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in tc_error_noXhl ~kinds:kinds pf end diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index 0e1d49fee..2fee2797e 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -78,7 +78,7 @@ let t_kill_r side cpos olen tc = in let tr = fun side -> `Kill (side, cpos, olen) in - t_code_transform side ~bdhoare:true cpos tr (t_zip kill_stmt) tc + t_code_transform side cpos tr (t_zip kill_stmt) tc (* -------------------------------------------------------------------- *) let alias_stmt env id (pf, _) me i = @@ -109,7 +109,7 @@ let alias_stmt env id (pf, _) me i = let t_alias_r side cpos id g = let env = FApi.tc1_env g in let tr = fun side -> `Alias (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold (alias_stmt env id)) g + t_code_transform side cpos tr (t_fold (alias_stmt env id)) g (* -------------------------------------------------------------------- *) let set_stmt (fresh, id) e = @@ -136,7 +136,7 @@ let set_stmt (fresh, id) e = let t_set_r side cpos (fresh, id) e tc = let tr = fun side -> `Set (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_zip (set_stmt (fresh, id) e)) tc + t_code_transform side cpos tr (t_zip (set_stmt (fresh, id) e)) tc (* -------------------------------------------------------------------- *) let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) = @@ -181,7 +181,7 @@ let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) = let t_set_match_r (side : oside) (cpos : Position.codepos) (id : symbol) pattern tc = let tr = fun side -> `SetMatch (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr + t_code_transform side cpos tr (t_zip (set_match_stmt id pattern)) tc (* -------------------------------------------------------------------- *) @@ -424,7 +424,7 @@ let t_cfold = let tr = fun side -> `Fold (side, cpos, olen) in let cb = fun cenv _ me zpr -> cfold_stmt ~eager cenv me olen zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) tc + t_code_transform side cpos tr (t_zip cb) tc (* -------------------------------------------------------------------- *) let t_kill = FApi.t_low3 "code-tx-kill" t_kill_r @@ -619,7 +619,7 @@ let transform_if_stmt env (pf, _) me i = let t_transform_if_r side cpos g = let env = FApi.tc1_env g in let tr = fun side -> `TransformIf (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold (transform_if_stmt env)) g + t_code_transform side cpos tr (t_fold (transform_if_stmt env)) g let t_transform_if = FApi.t_low2 "code-tx-transform_if" t_transform_if_r diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index b8bf396d5..453b9ccdc 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -115,7 +115,7 @@ let fission_stmt (il, (d1, d2)) (pf, hyps) me zpr = let t_fission_r side cpos infos g = let tr = fun side -> `LoopFission (side, cpos, infos) in let cb = fun cenv _ me zpr -> fission_stmt infos cenv me zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g + t_code_transform side cpos tr (t_zip cb) g let t_fission = FApi.t_low3 "loop-fission" t_fission_r @@ -170,7 +170,7 @@ let fusion_stmt (il, (d1, d2)) (pf, hyps) me zpr = let t_fusion_r side cpos infos g = let tr = fun side -> `LoopFusion (side, cpos, infos) in let cb = fun cenv _ me zpr -> fusion_stmt infos cenv me zpr in - t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g + t_code_transform side cpos tr (t_zip cb) g let t_fusion = FApi.t_low3 "loop-fusion" t_fusion_r @@ -182,7 +182,7 @@ let unroll_stmt (pf, _) me i = let t_unroll_r side cpos g = let tr = fun side -> `LoopUnraoll (side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold unroll_stmt) g + t_code_transform side cpos tr (t_fold unroll_stmt) g let t_unroll = FApi.t_low2 "loop-unroll" t_unroll_r @@ -199,7 +199,7 @@ let splitwhile_stmt b (pf, _) me i = let t_splitwhile_r b side cpos g = let tr = fun side -> `SplitWhile (b, side, cpos) in - t_code_transform side ~bdhoare:true cpos tr (t_fold (splitwhile_stmt b)) g + t_code_transform side cpos tr (t_fold (splitwhile_stmt b)) g let t_splitwhile = FApi.t_low3 "split-while" t_splitwhile_r