From 059ad5b6a509baa68a05b0927f8587f01b537263 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 4 Feb 2026 17:03:16 +0100 Subject: [PATCH 1/2] make `|-` and `-|` different --- src/ecCoreGoal.ml | 2 +- src/ecCoreModules.ml | 6 +++--- src/ecEnv.ml | 10 +++++----- src/ecHiGoal.ml | 12 ++++++------ src/ecHiInductive.ml | 6 +++--- src/ecHiNotations.ml | 2 +- src/ecLexer.mll | 2 +- src/ecLoader.ml | 2 +- src/ecLowGoal.ml | 18 +++++++++--------- src/ecParser.mly | 4 ++-- src/ecPrinting.ml | 6 +++--- src/ecScope.ml | 2 +- src/ecSection.ml | 10 +++++----- src/ecSmt.ml | 2 +- src/ecTyping.ml | 18 +++++++++--------- src/ecUFind.ml | 6 +++--- src/ecUnify.ml | 2 +- src/ecUtils.ml | 2 +- src/ecUtils.mli | 2 +- src/phl/ecPhlCodeTx.ml | 2 +- src/phl/ecPhlLoopTx.ml | 2 +- src/phl/ecPhlRwEquiv.ml | 2 +- src/phl/ecPhlSp.ml | 4 ++-- 23 files changed, 62 insertions(+), 62 deletions(-) diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 74ff095f5..4b75e5b0c 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -867,7 +867,7 @@ module FApi = struct (* ------------------------------------------------------------------ *) let t_ors_map (totc : 'a -> backward) (xs : 'a list) (tc : tcenv1) = - t_ors_pmap (some |- totc) xs tc + t_ors_pmap (some -| totc) xs tc (* ------------------------------------------------------------------ *) let t_ors (tts : backward list) (tc : tcenv1) = diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml index a07f9ab2a..11b15caa6 100644 --- a/src/ecCoreModules.ml +++ b/src/ecCoreModules.ml @@ -21,7 +21,7 @@ let symbol_of_lv = function EcTypes.symbol_of_pv pv | LvTuple pvs -> - String.concat "" (List.map (EcTypes.symbol_of_pv |- fst) pvs) + String.concat "" (List.map (EcTypes.symbol_of_pv -| fst) pvs) let ty_of_lv = function | LvVar (_, ty) -> ty @@ -45,7 +45,7 @@ let name_of_lv lv = | LvVar (pv, _) -> EcTypes.name_of_pvar pv | LvTuple pvs -> - String.concat "_" (List.map (EcTypes.name_of_pvar |- fst) pvs) + String.concat "_" (List.map (EcTypes.name_of_pvar -| fst) pvs) let lv_of_expr e = match e.e_node with @@ -184,7 +184,7 @@ let rec lv_get_uninit_read (w : Ssym.t) (lv : lvalue) = Ssym.union (sx_of_pv x) w | LvTuple xs -> - let w' = List.map (sx_of_pv |- fst) xs in + let w' = List.map (sx_of_pv -| fst) xs in Ssym.big_union (w :: w') and s_get_uninit_read (w : Ssym.t) (s : stmt) = diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 6950cfc3b..c19bbe60c 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -1875,7 +1875,7 @@ module Mod = struct let me_params = clearparams (List.length args) me.me_params in let me_oinfos = - let keep = List.map (EcPath.mident |- fst) me_params in + let keep = List.map (EcPath.mident -| fst) me_params in let keep = Sm.of_list keep in Msym.map (OI.filter (fun f -> Sm.mem (f.x_top) keep)) me.me_oinfos in @@ -2136,7 +2136,7 @@ module ModTy = struct let ois = EcSubst.subst_oracle_infos subst sig_.mis_oinfos in let params = mt.mt_params in - let keep = List.map (EcPath.mident |- fst) params in + let keep = List.map (EcPath.mident -| fst) params in let keep = Sm.of_list keep in let ois = Msym.map (OI.filter (fun f -> Sm.mem (f.x_top) keep)) ois in @@ -3115,7 +3115,7 @@ module Theory = struct Some (Th_axiom (x, { ax with ax_kind = `Axiom (tags, true) })) | Th_addrw (p, ps, lc) -> - let ps = List.filter ((not) |- inclear |- oget |- EcPath.prefix) ps in + let ps = List.filter ((not) -| inclear -| oget -| EcPath.prefix) ps in if List.is_empty ps then None else Some (Th_addrw (p, ps,lc)) | Th_auto ({ axioms } as auto_rl) -> @@ -3328,12 +3328,12 @@ module LDecl = struct (* ------------------------------------------------------------------ *) let by_name s hyps = - match List.ofind ((=) s |- EcIdent.name |- fst) hyps.h_local with + match List.ofind ((=) s -| EcIdent.name -| fst) hyps.h_local with | None -> error (LookupError (`Symbol s)) | Some h -> h let by_id id hyps = - match List.ofind (EcIdent.id_equal id |- fst) hyps.h_local with + match List.ofind (EcIdent.id_equal id -| fst) hyps.h_local with | None -> error (LookupError (`Ident id)) | Some x -> snd x diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 8a5ebb0a7..aa2dc1af1 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -758,14 +758,14 @@ let process_rewrite1_r ttenv ?target ri tc = match simpl with | Some logic -> let hyps = FApi.tc1_hyps tc in - let target = target |> omap (fst |- LDecl.hyp_by_name^~ hyps |- unloc) in + let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) | None -> t_id in FApi.t_seq tt process_trivial tc | RWSimpl logic -> let hyps = FApi.tc1_hyps tc in - let target = target |> omap (fst |- LDecl.hyp_by_name^~ hyps |- unloc) in + let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) tc | RWDelta ((s, r, o, px), p) -> begin @@ -782,7 +782,7 @@ let process_rewrite1_r ttenv ?target ri tc = | RWRw (((s : rwside), r, o, p), pts) -> begin let do1 (mode : [`Full | `Light]) ((subs : rwside), pt) tc = let hyps = FApi.tc1_hyps tc in - let target = target |> omap (fst |- LDecl.hyp_by_name^~ hyps |- unloc) in + let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in let hyps = FApi.tc1_hyps ?target tc in let ptenv, prw = @@ -916,7 +916,7 @@ let process_rewrite ttenv ?target ri tc = else process_rewrite1 ttenv ri tc in - match fc |> omap ((process_tfocus tc) |- unloc) with + match fc |> omap ((process_tfocus tc) -| unloc) with | None -> FApi.t_onalli dorw tc | Some fc -> FApi.t_onselecti fc dorw tc @@ -1160,7 +1160,7 @@ let process_view1 pe tc = in let discharge tc = - let intros = List.map (EcIdent.name |- fst |- snd) ids in + let intros = List.map (EcIdent.name -| fst -| snd) ids in let intros = LDecl.fresh_ids hyps intros in let for1 evm (x, idty) id = @@ -1217,7 +1217,7 @@ let process_view1 pe tc = (* -------------------------------------------------------------------- *) let process_view pes tc = - let views = List.map (t_last |- process_view1) pes in + let views = List.map (t_last -| process_view1) pes in List.fold_left (fun tc tt -> tt tc) (FApi.tcenv_of_tcenv1 tc) views (* -------------------------------------------------------------------- *) diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml index 45edcdcc7..c3c32645c 100644 --- a/src/ecHiInductive.ml +++ b/src/ecHiInductive.ml @@ -141,14 +141,14 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) = isempty_1 [ tyinst ty ] | Record (_, fields) -> - isempty_1 (List.map (tyinst |- snd) fields) + isempty_1 (List.map (tyinst -| snd) fields) | Datatype dt -> (* FIXME: Inspecting all constructors recursively causes non-termination in some cases. One can have the same limitation as is done for positivity in order to limit this unfolding to well-behaved cases. *) - isempty_n (List.map (List.map tyinst |- snd) dt.tydt_ctors) + isempty_n (List.map (List.map tyinst -| snd) dt.tydt_ctors) in @@ -327,7 +327,7 @@ let trans_matchfix let create o = EcIdent.create (omap_dfl unloc "_" o) in - let pvars = List.map (create |- unloc) cargs in + let pvars = List.map (create -| unloc) cargs in let pvars = List.combine pvars ctorty in (pb, (indp, ind, (ctorsym, ctoridx)), pvars, xpos) diff --git a/src/ecHiNotations.ml b/src/ecHiNotations.ml index ea8959d97..3d742857c 100644 --- a/src/ecHiNotations.ml +++ b/src/ecHiNotations.ml @@ -55,7 +55,7 @@ let trans_notation_r (env : env) (nt : pnotation located) = (List.map getident xbd, arg)) nt.nt_args) in let xs = List.map2 (fun xty (aid, aty) -> - (aid, toarrow (List.map (snd |- snd) xty) aty)) + (aid, toarrow (List.map (snd -| snd) xty) aty)) abd (snd (TT.trans_binding env ue xs)) in let benv = EcEnv.Var.bind_locals xs env in diff --git a/src/ecLexer.mll b/src/ecLexer.mll index b05cfe095..a163d3c2f 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -285,7 +285,7 @@ List.iter (curry (Hashtbl.add table)) _operators; table let opre = - let ops = List.map fst (List.filter (snd |- snd) _operators) in + let ops = List.map fst (List.filter (snd -| snd) _operators) in let ops = List.ksort ~key:(String.length) ~cmp:compare ~rev:true ops in let ops = String.join "|" (List.map EcRegexp.quote ops) in let ops = Printf.sprintf "(%s)" ops in diff --git a/src/ecLoader.ml b/src/ecLoader.ml index b9bfb4770..25378c19e 100644 --- a/src/ecLoader.ml +++ b/src/ecLoader.ml @@ -74,7 +74,7 @@ let rec addidir ?namespace ?(recursive = false) (idir : string) (ecl : ecloader) ecl.ecl_idirs <- ((namespace, idir), idx) :: ecl.ecl_idirs | _ -> - if not (List.exists ((=) idx |- snd) idirs) then + if not (List.exists ((=) idx -| snd) idirs) then ecl.ecl_idirs <- ((namespace, idir), idx) :: ecl.ecl_idirs end diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 2e2690156..6aac3f573 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -621,7 +621,7 @@ let t_intro_s (id : iname) (tc : tcenv1) = (* -------------------------------------------------------------------- *) let t_intros_i_x (ids : EcIdent.t list) (tc : tcenv1) = - t_intros_x (List.map (notag |- some) ids) tc + t_intros_x (List.map (notag -| some) ids) tc (* -------------------------------------------------------------------- *) let t_intros_i (ids : EcIdent.t list) (tc : tcenv1) = @@ -1110,8 +1110,8 @@ let gen_tuple_intro tys = ((x, fx), (y, fy), f_eq fx fy) in let eqs = List.mapi eq tys in - let concl = f_eq (f_tuple (List.map (snd |- proj3_1) eqs)) - (f_tuple (List.map (snd |- proj3_2) eqs)) in + let concl = f_eq (f_tuple (List.map (snd -| proj3_1) eqs)) + (f_tuple (List.map (snd -| proj3_2) eqs)) in let concl = f_imps (List.map proj3_3 eqs) concl in let concl = let bindings = @@ -1249,8 +1249,8 @@ let gen_tuple_eq_elim (tys : ty list) : form = ((x, fx), (y, fy), f_eq fx fy) in let eqs = List.mapi eq tys in - let concl = f_eq (f_tuple (List.map (snd |- proj3_1) eqs)) - (f_tuple (List.map (snd |- proj3_2) eqs)) in + let concl = f_eq (f_tuple (List.map (snd -| proj3_1) eqs)) + (f_tuple (List.map (snd -| proj3_2) eqs)) in let concl = f_imps [f_imps (List.map proj3_3 eqs) fp; concl] fp in let concl = let bindings = @@ -1275,7 +1275,7 @@ let t_elim_eq_tuple_r_n ((_, sf) : form * sform) concl tc = let tc = RApi.rtcenv_of_tcenv1 tc in let hyps = RApi.tc_hyps tc in let fs = List.combine (destr_tuple a1) (destr_tuple a2) in - let tys = List.map (f_ty |- fst) fs in + let tys = List.map (f_ty -| fst) fs in let hd = RApi.bwd_of_fwd (pf_gen_tuple_eq_elim tys hyps) tc in let args = List.flatten (List.map (fun (x, y) -> [x; y]) fs) in let args = concl :: args in @@ -2019,7 +2019,7 @@ let t_subst_x ?(exn = InvalidGoalShape) ?kind ?(except = Sid.empty) ?(clear = SC y, f_local y f.f_ty in let subst, check = LowSubst.build_subst env var fy in let post, (id', _), pre = - try List.find_pivot (id_equal id |- fst) (LDecl.tohyps hyps).h_local + try List.find_pivot (id_equal id -| fst) (LDecl.tohyps hyps).h_local with Not_found -> assert false in @@ -2246,7 +2246,7 @@ let t_progress ?options ?ti (tt : FApi.backward) (tc : tcenv1) = match sform_of_form concl with | SFquant (Lforall, _, _) -> let bd = fst (destr_forall concl) in - let ids = List.map (EcIdent.name |- fst) bd in + let ids = List.map (EcIdent.name -| fst) bd in let ids = LDecl.fresh_ids hyps ids in FApi.t_seq (t_intros_i ids) aux0 tc @@ -2326,7 +2326,7 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) = match sform_of_form concl with | SFquant (Lforall, _, _) -> let bd = fst (destr_forall concl) in - let ids = List.map (EcIdent.name |- fst) bd in + let ids = List.map (EcIdent.name -| fst) bd in let ids = LDecl.fresh_ids hyps ids in let st = { st with cs_undosubst = Sid.of_list (List.map fst (LDecl.tohyps hyps).h_local) } in FApi.t_seqs diff --git a/src/ecParser.mly b/src/ecParser.mly index 06f464f93..cda6b5afa 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -1759,7 +1759,7 @@ operator: { let gloc = EcLocation.make $startpos $endpos in let sty = sty |> ofdfl (fun () -> - mk_loc (b |> omap (loc |- fst) |> odfl gloc) PTunivar) in + mk_loc (b |> omap (loc -| fst) |> odfl gloc) PTunivar) in { po_kind = k; po_name = List.hd x; @@ -1767,7 +1767,7 @@ operator: po_tags = odfl [] tags; po_tyvars = tyvars; po_args = odfl ([], None) args; - po_def = opdef_of_opbody sty (omap (unloc |- fst) b); + po_def = opdef_of_opbody sty (omap (unloc -| fst) b); po_ax = obind snd b; po_locality = locality; } } diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 4c100ca9c..5d805325a 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1663,7 +1663,7 @@ and try_pp_chained_orderings match match_pp_notations ~filter:(fun (p, _) -> is_ordering_op p) ppe f with | Some ((op, (tvi, _)), ue, ev, ov, [i1; i2]) -> begin let ti = Tvar.subst ov in - let tvi = List.map (ti |- tvar) tvi in + let tvi = List.map (ti -| tvar) tvi in let sb = EcMatching.MEV.assubst ue ev ppe.ppe_env in let i1 = Fsubst.f_subst sb i1 in let i2 = Fsubst.f_subst sb i2 in @@ -1802,8 +1802,8 @@ and try_pp_notations | Some ((p, (tv, nt)), ue, ev, ov, eargs) -> let ti = Tvar.subst ov in let rty = ti nt.ont_resty in - let tv = List.map (ti |- tvar) tv in - let args = List.map (curry f_local |- snd_map ti) nt.ont_args in + let tv = List.map (ti -| tvar) tv in + let args = List.map (curry f_local -| snd_map ti) nt.ont_args in let f = f_op p tv (toarrow tv rty) in let f = f_app f args rty in let f = Fsubst.f_subst (EcMatching.MEV.assubst ue ev ppe.ppe_env) f in diff --git a/src/ecScope.ml b/src/ecScope.ml index 77e85a23e..4b0220e1a 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1370,7 +1370,7 @@ module Op = struct | OB_oper (Some (OP_Plain bd)) -> let path = EcPath.pqname (path scope) (unloc op.po_name) in let axop = - let nargs = List.sum (List.map (List.length |- fst) args) in + let nargs = List.sum (List.map (List.length -| fst) args) in EcDecl.axiomatized_op ~nargs path (tyop.op_tparams, bd) lc in let tyop = { tyop with op_opaque = { reduction = true; smt = false; }} in let scope = bind scope (unloc op.po_name, tyop) in diff --git a/src/ecSection.ml b/src/ecSection.ml index 97ef2ea33..95da81897 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -141,7 +141,7 @@ and on_lp (aenv : aenv) (lp : lpattern) = match lp with | LSymbol (_, ty) -> on_ty aenv ty | LTuple xs -> List.iter (fun (_, ty) -> on_ty aenv ty) xs - | LRecord (_, xs) -> List.iter (on_ty aenv |- snd) xs + | LRecord (_, xs) -> List.iter (on_ty aenv -| snd) xs (* -------------------------------------------------------------------- *) and on_binding (aenv : aenv) ((_, ty) : (EcIdent.t * ty)) = @@ -236,7 +236,7 @@ and on_instr (aenv : aenv) (i : instr)= | Smatch (e, b) -> let forb (bs, s) = - List.iter (on_ty aenv |- snd) bs; + List.iter (on_ty aenv -| snd) bs; on_stmt aenv s in on_expr aenv e; List.iter forb b @@ -438,9 +438,9 @@ and on_tydecl (aenv : aenv) (tyd : tydecl) = | Abstract -> () | Record (f, fds) -> on_form aenv f; - List.iter (on_ty aenv |- snd) fds + List.iter (on_ty aenv -| snd) fds | Datatype dt -> - List.iter (List.iter (on_ty aenv) |- snd) dt.tydt_ctors; + List.iter (List.iter (on_ty aenv) -| snd) dt.tydt_ctors; List.iter (on_form aenv) [dt.tydt_schelim; dt.tydt_schcase] and on_typeclass (aenv : aenv) tc = @@ -466,7 +466,7 @@ and on_opdecl (aenv : aenv) (opdecl : operator) = pri.pri_ctors | OB_nott nott -> - List.iter (on_ty aenv |- snd) nott.ont_args; + List.iter (on_ty aenv -| snd) nott.ont_args; on_ty aenv nott.ont_resty; on_expr aenv nott.ont_body diff --git a/src/ecSmt.ml b/src/ecSmt.ml index fdc3d18f6..b0230936a 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -287,7 +287,7 @@ let instantiate tparams ~textra targs tres tys = (fun mtv tv ty -> WTy.Mtv.add tv ty mtv) WTy.Mtv.empty tparams tys in let textra = List.map (WTy.ty_inst mtv) textra in - let targs = List.map (some |- WTy.ty_inst mtv) targs in + let targs = List.map (some -| WTy.ty_inst mtv) targs in let tres = tres |> omap (WTy.ty_inst mtv) in (textra, targs, tres) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 593b78b72..8b84ff175 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -278,7 +278,7 @@ let (_i_inuse, s_inuse, se_inuse) = | Smatch (e, bs) -> let map = se_inuse map e in - let map = List.fold_left (fun map -> s_inuse map |- snd) map bs in + let map = List.fold_left (fun map -> s_inuse map -| snd) map bs in map | Sassert e -> @@ -1056,7 +1056,7 @@ let transpattern1 env ue (p : EcParsetree.plpattern) = (LTuple (List.combine xs subtys), ttuple subtys) | LPRecord fields -> - let xs = List.map (unloc |- snd) fields in + let xs = List.map (unloc -| snd) fields in if not (List.is_unique xs) then tyerror p.pl_loc env NonLinearPattern; @@ -1077,7 +1077,7 @@ let transpattern1 env ue (p : EcParsetree.plpattern) = in List.map for1 fields in - let recp = Sp.of_list (List.map (fst |- proj3_1) fields) in + let recp = Sp.of_list (List.map (fst -| proj3_1) fields) in let recp = match Sp.elements recp with | [] -> assert false @@ -1217,7 +1217,7 @@ let trans_record env ue (subtt, proj) (loc, b, fields) = in List.map for1 fields in - let recp = Sp.of_list (List.map (fst |- proj3_1) fields) in + let recp = Sp.of_list (List.map (fst -| proj3_1) fields) in let recp = match Sp.elements recp with | [] -> assert false @@ -1334,7 +1334,7 @@ let trans_branch ~loc env ue gindty ((pb, body) : ppattern * _) = unify_or_fail env ue loc ~expct:pty gindty; let create o = EcIdent.create (omap_dfl unloc "_" o) in - let pvars = List.map (create |- unloc) cargs in + let pvars = List.map (create -| unloc) cargs in let pvars = List.combine pvars ctorty in (ctorsym, (pvars, body)) @@ -2292,7 +2292,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = (* Module parameters must have been added to the environment *) and get_oi_calls env (params, items) = let mparams = - let mparams = List.map (mident |- fst) params in + let mparams = List.map (mident -| fst) params in Sm.of_list mparams in let comp_oi oi it = match it with @@ -2458,7 +2458,7 @@ and transstruct1 (env : EcEnv.env) (st : pstructure_item located) = [], [transstruct1_alias env name f] | Pst_import ms -> - (List.map (fst |- trans_msymbol env) ms), [] + (List.map (fst -| trans_msymbol env) ms), [] | Pst_include (m, imp, procs) -> begin let (mo, ms) = trans_msymbol env m in @@ -2969,7 +2969,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = | PFMatchBuild (deep, xs, ptg, ppt) -> let f = f_ands (flatten deep f) in - let xs = List.map (EcIdent.create |- unloc) xs in + let xs = List.map (EcIdent.create -| unloc) xs in let xst = List.map (fun x -> (x, tbool)) xs in let lenv = EcEnv.Var.bind_locals xst env in let tg = trans_prop lenv ue ptg in @@ -3160,7 +3160,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = | None -> x | Some qs -> let (nm, name) = x.pl_desc in - { x with pl_desc = ((List.map (unloc |- fst) qs)@nm, name) } + { x with pl_desc = ((List.map (unloc -| fst) qs)@nm, name) } in let do1 = function diff --git a/src/ecUFind.ml b/src/ecUFind.ml index 3fe12071d..db4bf8a2e 100644 --- a/src/ecUFind.ml +++ b/src/ecUFind.ml @@ -95,7 +95,7 @@ module Make (I : Item) (D : Data) = struct let (item, w, olddata) = xfind item uf in { forest = M.add item (Root (w, data)) uf.forest; nvoids = uf.nvoids - - (odfl 0 (olddata |> omap (int_of_bool |- D.isvoid))) + - (odfl 0 (olddata |> omap (int_of_bool -| D.isvoid))) + (int_of_bool (D.isvoid data)); } (* ------------------------------------------------------------------ *) @@ -121,8 +121,8 @@ module Make (I : Item) (D : Data) = struct let uf = { forest = M.add item1 link1 (M.add item2 link2 uf.forest); nvoids = uf.nvoids - - (odfl 0 (data1 |> omap (int_of_bool |- D.isvoid)) + - odfl 0 (data2 |> omap (int_of_bool |- D.isvoid))) + - (odfl 0 (data1 |> omap (int_of_bool -| D.isvoid)) + + odfl 0 (data2 |> omap (int_of_bool -| D.isvoid))) + (int_of_bool (D.isvoid data)); } in (uf, effects) diff --git a/src/ecUnify.ml b/src/ecUnify.ml index 0fff10aa6..45cc66753 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -127,7 +127,7 @@ let unify_core (env : EcEnv.env) (uf : UF.t) pb = match t1.ty_node, t2.ty_node with | Tunivar id1, Tunivar id2 -> begin if not (uid_equal id1 id2) then - let effects = reffold (swap |- UF.union id1 id2) uf in + let effects = reffold (swap -| UF.union id1 id2) uf in List.iter (Queue.push^~ pb) effects end diff --git a/src/ecUtils.ml b/src/ecUtils.ml index e852ce0c0..10218dc67 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -57,7 +57,7 @@ let predT (_ : 'a) = true let (^~) f = fun x y -> f y x let (-|) f g = fun x -> f (g x) -let (|-) g f = fun x -> g (f x) +let (|-) g f = fun x -> f (g x) let (|>) x f = f x let (<|) f x = f x diff --git a/src/ecUtils.mli b/src/ecUtils.mli index 7d0a4c3c8..87bea947a 100644 --- a/src/ecUtils.mli +++ b/src/ecUtils.mli @@ -29,7 +29,7 @@ val predT: 'a -> bool val (^~) : ('a -> 'b -> 'c) -> ('b -> 'a -> 'c) val (-|) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b -val (|-) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b +val (|-) : ('c -> 'a) -> ('a -> 'b) -> 'c -> 'b val (|>) : 'a -> ('a -> 'b) -> 'b val (<|) : ('a -> 'b) -> 'a -> 'b diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index f3ec2c513..4f2bb1469 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -295,7 +295,7 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) ( if not (List.for_all is_const_expression es) then tc_error pf "right-values are not closed expressions"; - if not (List.for_all (is_loc |- fst) lv) then + if not (List.for_all (is_loc -| fst) lv) then tc_error pf "left-values must be made of local variables only"; let subst = diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 0844ab2f2..2ede919f8 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -65,7 +65,7 @@ let check_dslc pf = List.iter doit_s [c1; c2] | Smatch (_, bs) -> - List.iter (doit_s |- snd) bs + List.iter (doit_s -| snd) bs | Srnd _ | Scall _ | Swhile _ | Sassert _ | Sabstract _ -> error () diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml index 100d49e72..a568172e8 100644 --- a/src/phl/ecPhlRwEquiv.ml +++ b/src/phl/ecPhlRwEquiv.ml @@ -145,7 +145,7 @@ let process_rewrite_equiv info tc = let args, ret_ty = EcTyping.trans_args subenv ue (loc pargs) proc.f_sig (unloc pargs) in let res = omap (fun v -> EcTyping.transexpcast subenv `InProc ue ret_ty v) pres in let es = e_subst (Tuni.subst (EcUnify.UniEnv.close ue)) in - Some (List.map es args, omap (EcModules.lv_of_expr |- es) res) + Some (List.map es args, omap (EcModules.lv_of_expr -| es) res) with EcUnify.UninstantiateUni -> EcTyping.tyerror (loc pargs) env EcTyping.FreeTypeVariables end diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml index ec3b2eb36..025ff6d59 100644 --- a/src/phl/ecPhlSp.ml +++ b/src/phl/ecPhlSp.ml @@ -65,7 +65,7 @@ module LowInternal = struct | LvTuple vs, _ -> begin let aux = List.map2 (fun x y -> (fst x, fst y)) vs new_ids in try - let new_id = snd (List.find (NormMp.pv_equal env pv' |- fst) aux) in + let new_id = snd (List.find (NormMp.pv_equal env pv' -| fst) aux) in ALocal (new_id, ty) with Not_found -> var end @@ -96,7 +96,7 @@ module LowInternal = struct let subst = EcFol.Fsubst.f_subst_id in let subst = EcFol.Fsubst.f_bind_local subst id f in (List.map (snd_map (EcFol.Fsubst.f_subst subst)) assoc, - List.filter ((<>) id |- fst) bds, + List.filter ((<>) id -| fst) bds, EcFol.Fsubst.f_subst subst pre) | _ -> ((a, f) :: assoc, bds, pre) From 447f7aeb76c3efd1bd81dad85e0b74c73dacb702 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 4 Feb 2026 17:52:19 +0100 Subject: [PATCH 2/2] fix precedence --- src/ecHiGoal.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index aa2dc1af1..d34ba4aa7 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -758,14 +758,14 @@ let process_rewrite1_r ttenv ?target ri tc = match simpl with | Some logic -> let hyps = FApi.tc1_hyps tc in - let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in + let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) | None -> t_id in FApi.t_seq tt process_trivial tc | RWSimpl logic -> let hyps = FApi.tc1_hyps tc in - let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in + let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) tc | RWDelta ((s, r, o, px), p) -> begin @@ -782,7 +782,7 @@ let process_rewrite1_r ttenv ?target ri tc = | RWRw (((s : rwside), r, o, p), pts) -> begin let do1 (mode : [`Full | `Light]) ((subs : rwside), pt) tc = let hyps = FApi.tc1_hyps tc in - let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in + let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in let hyps = FApi.tc1_hyps ?target tc in let ptenv, prw =