Skip to content

[Internal] Make |- and -| compose in different orders #885

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
oskgo merged 2 commits into from
Feb 5, 2026
Merged

[Internal] Make |- and -| compose in different orders #885

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
059ad5b
make `|-` and `-|` different
oskgo Feb 4, 2026
447f7ae
fix precedence
oskgo Feb 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/ecCoreGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down
6 changes: 3 additions & 3 deletions src/ecCoreModules.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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) =
Expand Down
10 changes: 5 additions & 5 deletions src/ecEnv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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) ->
Expand Down Expand Up @@ -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

Expand Down
12 changes: 6 additions & 6 deletions src/ecHiGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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

(* -------------------------------------------------------------------- *)
Expand Down
6 changes: 3 additions & 3 deletions src/ecHiInductive.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/ecHiNotations.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/ecLexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/ecLoader.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
18 changes: 9 additions & 9 deletions src/ecLowGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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 =
Expand All @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/ecParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1759,15 +1759,15 @@ 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;
po_aliases = List.tl x;
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; } }

Expand Down
6 changes: 3 additions & 3 deletions src/ecPrinting.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/ecScope.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions src/ecSection.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) =
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 =
Expand All @@ -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

Expand Down
2 changes: 1 addition & 1 deletion src/ecSmt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
Loading