From 49623896f65489138cb427d7bfc6df05b0ab8c4b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 7 Jul 2026 07:39:48 +0200 Subject: [PATCH] feat: named ring/field instances for `ring`/`field` structure selection A carrier type can carry several ring/field structures; the tactics silently used the first registered one with no way to disambiguate. Give instances an optional name at declaration (`instance ring [foo] with T ...`) and let the tactic target it (`ring [foo]` / `field [foo]`). Bare `ring`/`field` are unchanged: with no name, the first matching instance is used, so the single-structure case behaves identically. --- src/ecDecl.ml | 1 + src/ecDecl.mli | 1 + src/ecHiGoal.ml | 14 +++++--- src/ecHiGoal.mli | 2 +- src/ecHiTacticals.ml | 4 +-- src/ecParser.mly | 14 ++++---- src/ecParsetree.ml | 5 +-- src/ecScope.ml | 13 +++---- src/ecSubst.ml | 3 +- src/ecTheoryReplay.ml | 3 +- src/ecTyping.ml | 16 ++++++--- src/ecTyping.mli | 4 +-- tests/field-multi-instance.ec | 65 +++++++++++++++++++++++++++++++++++ tests/ring-multi-instance.ec | 63 +++++++++++++++++++++++++++++++++ 14 files changed, 178 insertions(+), 30 deletions(-) create mode 100644 tests/field-multi-instance.ec create mode 100644 tests/ring-multi-instance.ec diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 365253413..c2d52cdff 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -336,6 +336,7 @@ type rkind = [ ] type ring = { + r_name : EcSymbols.symbol option; r_type : EcTypes.ty; r_zero : EcPath.path; r_one : EcPath.path; diff --git a/src/ecDecl.mli b/src/ecDecl.mli index 98e366a6c..e1253bfb2 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -199,6 +199,7 @@ type rkind = [ ] type ring = { + r_name : EcSymbols.symbol option; r_type : EcTypes.ty; r_zero : EcPath.path; r_one : EcPath.path; diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index c3f8e89f6..c2ce31e9a 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -181,7 +181,7 @@ let process_clear (info : clear_info) tc = t_clears ~leniant:true clear_list tc (* -------------------------------------------------------------------- *) -let process_algebra mode kind eqs (tc : tcenv1) = +let process_algebra mode kind ?name eqs (tc : tcenv1) = let (env, hyps, concl) = FApi.tc1_eflat tc in if not (EcAlgTactic.is_module_loaded env) then @@ -210,6 +210,10 @@ let process_algebra mode kind eqs (tc : tcenv1) = let tparams = (LDecl.tohyps hyps).h_tvar in + let named = omap unloc name in + let named_suffix = + match named with None -> "" | Some n -> Printf.sprintf " named `%s'" n in + let tactic = match match mode, kind with @@ -220,14 +224,14 @@ let process_algebra mode kind eqs (tc : tcenv1) = with | `Ring t -> let r = - match TT.get_ring (tparams, ty) env with - | None -> tacuerror "cannot find a ring structure" + match TT.get_ring ?name:named (tparams, ty) env with + | None -> tacuerror "cannot find a ring structure%s" named_suffix | Some r -> r in t r eqs (f1, f2) | `Field t -> let r = - match TT.get_field (tparams, ty) env with - | None -> tacuerror "cannot find a field structure" + match TT.get_field ?name:named (tparams, ty) env with + | None -> tacuerror "cannot find a field structure%s" named_suffix | Some r -> r in t r eqs (f1, f2) in diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index ddc361c41..7e871e956 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -104,7 +104,7 @@ val process_wlog : suff:bool -> psymbol list -> pformula -> backward val process_genhave : ttenv -> pgenhave -> backward (* -------------------------------------------------------------------- *) -val process_algebra : [`Solve] -> [`Ring|`Field] -> psymbol list -> backward +val process_algebra : [`Solve] -> [`Ring|`Field] -> ?name:psymbol -> psymbol list -> backward (* -------------------------------------------------------------------- *) val process_crushmode : crushmode -> bool * backward option diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 610f20db0..c44c58c5b 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -138,8 +138,8 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) = | Psplit (`Default i) -> process_split ?i | Psplit (`All `Maybe)-> process_split_all ~must:false | Psplit (`All `One) -> process_split_all ~must:true - | Pfield st -> process_algebra `Solve `Field st - | Pring st -> process_algebra `Solve `Ring st + | Pfield (nm, st) -> process_algebra `Solve `Field ?name:nm st + | Pring (nm, st) -> process_algebra `Solve `Ring ?name:nm st | Palg_norm -> EcStrongRing.t_alg_eq | Pexists fs -> process_exists fs | Pleft -> process_left diff --git a/src/ecParser.mly b/src/ecParser.mly index 9a24157bd..8b75ec9a5 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -1732,10 +1732,11 @@ subtype_rename: (* -------------------------------------------------------------------- *) (* Type classes (instances) *) tycinstance: -| loca=is_local INSTANCE x=qident +| loca=is_local INSTANCE x=qident nm=bracket(ident)? WITH typ=tyvars_decl? ty=loc(type_exp) ops=tyci_op* axs=tyci_ax* { { pti_name = x; + pti_as = nm; pti_type = (odfl [] typ, ty); pti_ops = ops; pti_axs = axs; @@ -1744,10 +1745,11 @@ tycinstance: } } -| loca=is_local INSTANCE x=qident c=uoption(UINT) p=uoption(UINT) +| loca=is_local INSTANCE x=qident nm=bracket(ident)? c=uoption(UINT) p=uoption(UINT) WITH typ=tyvars_decl? ty=loc(type_exp) ops=tyci_op* axs=tyci_ax* { { pti_name = x; + pti_as = nm; pti_type = (odfl [] typ, ty); pti_ops = ops; pti_axs = axs; @@ -2868,11 +2870,11 @@ logtactic: | SPLIT PLUS { Psplit (`All `One) } -| FIELD eqs=ident* - { Pfield eqs } +| FIELD nm=bracket(ident)? eqs=ident* + { Pfield (nm, eqs) } -| RING eqs=ident* - { Pring eqs } +| RING nm=bracket(ident)? eqs=ident* + { Pring (nm, eqs) } | ALGNORM { Palg_norm } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 18f4acccf..0f1354f5e 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1108,8 +1108,8 @@ type logtactic = | Passumption | Psmt of pprover_infos | Psplit of [ `Default of int option | `All of [ `Maybe | `One ] ] - | Pfield of psymbol list - | Pring of psymbol list + | Pfield of psymbol option * psymbol list + | Pring of psymbol option * psymbol list | Palg_norm | Pexists of ppt_arg located list | Pleft @@ -1212,6 +1212,7 @@ type prealize = { (* -------------------------------------------------------------------- *) type ptycinstance = { pti_name : pqsymbol; + pti_as : psymbol option; pti_type : ptyparams * pty; pti_ops : (psymbol * (pty list * pqsymbol)) list; pti_axs : (psymbol * ptactic_core) list; diff --git a/src/ecScope.ml b/src/ecScope.ml index 19cddec23..67fd16c24 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2509,8 +2509,9 @@ module Ty = struct let p_field = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field" ], "field" ) (* ------------------------------------------------------------------ *) - let ring_of_symmap env ty kind symbols = - { r_type = ty; + let ring_of_symmap ?name env ty kind symbols = + { r_name = name; + r_type = ty; r_zero = oget (Mstr.find_opt "rzero" symbols); r_one = oget (Mstr.find_opt "rone" symbols); r_add = oget (Mstr.find_opt "add" symbols); @@ -2541,7 +2542,7 @@ module Ty = struct let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in let symbols = check_tci_operators env ty tci.pti_ops symbols in - let cr = ring_of_symmap env (snd ty) kind symbols in + let cr = ring_of_symmap ?name:(omap unloc tci.pti_as) env (snd ty) kind symbols in let axioms = EcAlgTactic.ring_axioms env cr in let lc = (tci.pti_loca :> locality) in let inter = check_tci_axioms scope mode tci.pti_axs axioms lc in @@ -2562,8 +2563,8 @@ module Ty = struct in Ax.add_defer scope inter (* ------------------------------------------------------------------ *) - let field_of_symmap env ty symbols = - { f_ring = ring_of_symmap env ty `Integer symbols; + let field_of_symmap ?name env ty symbols = + { f_ring = ring_of_symmap ?name env ty `Integer symbols; f_inv = oget (Mstr.find_opt "inv" symbols); f_div = Mstr.find_opt "div" symbols; } @@ -2583,7 +2584,7 @@ module Ty = struct hierror "field instances cannot be polymorphic"; let symbols = EcAlgTactic.field_symbols env (snd ty) in let symbols = check_tci_operators env ty tci.pti_ops symbols in - let cr = field_of_symmap env (snd ty) symbols in + let cr = field_of_symmap ?name:(omap unloc tci.pti_as) env (snd ty) symbols in let axioms = EcAlgTactic.field_axioms env cr in let lc = (tci.pti_loca :> locality) in let inter = check_tci_axioms scope mode tci.pti_axs axioms lc; in diff --git a/src/ecSubst.ml b/src/ecSubst.ml index a94a4738a..b2fa2836c 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -994,7 +994,8 @@ let fresh_scparams (s : subst) (xtys : (EcIdent.t * ty) list) = (* -------------------------------------------------------------------- *) let subst_ring (s : subst) cr = - { r_type = subst_ty s cr.r_type; + { r_name = cr.r_name; + r_type = subst_ty s cr.r_type; r_zero = subst_path s cr.r_zero; r_one = subst_path s cr.r_one; r_add = subst_path s cr.r_add; diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index d85b49c23..916a2aafc 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -1040,7 +1040,8 @@ and replay_instance let (typ, ty) = EcSubst.subst_genty subst (typ, ty) in let tc = let rec doring cr = - { r_type = EcSubst.subst_ty subst cr.r_type; + { r_name = cr.r_name; + r_type = EcSubst.subst_ty subst cr.r_type; r_zero = forpath cr.r_zero; r_one = forpath cr.r_one; r_add = forpath cr.r_add; diff --git a/src/ecTyping.ml b/src/ecTyping.ml index cd32c69e5..1be5f098c 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3911,25 +3911,33 @@ let get_instances (tvi, bty) env = with EcUnify.UnificationFailure _ -> None) inst -let get_ring (typ, ty) env = +(* When [name] is given, only the instance registered under that name is + selected; otherwise the first matching instance (registration order) is + used, preserving the single-structure behaviour. *) +let name_selects name iname = + match name with None -> true | Some _ -> name = iname + +let get_ring ?name (typ, ty) env = let module E = struct exception Found of ring end in try List.iter (fun (_, _, cr) -> match cr with - | `Ring cr -> raise (E.Found cr) + | `Ring cr when name_selects name cr.EcDecl.r_name -> + raise (E.Found cr) | _ -> ()) (get_instances (typ, ty) env); None with E.Found cr -> Some cr -let get_field (typ, ty) env = +let get_field ?name (typ, ty) env = let module E = struct exception Found of field end in try List.iter (fun (_, _, cr) -> match cr with - | `Field cr -> raise (E.Found cr) + | `Field cr when name_selects name cr.EcDecl.f_ring.EcDecl.r_name -> + raise (E.Found cr) | _ -> ()) (get_instances (typ, ty) env); None diff --git a/src/ecTyping.mli b/src/ecTyping.mli index 1080fdb6d..624432c2d 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -320,5 +320,5 @@ val check_modtype : env -> mpath -> module_sig -> mty_mr -> unit (* -------------------------------------------------------------------- *) -val get_ring : (ty_params * ty) -> env -> EcDecl.ring option -val get_field : (ty_params * ty) -> env -> EcDecl.field option +val get_ring : ?name:symbol -> (ty_params * ty) -> env -> EcDecl.ring option +val get_field : ?name:symbol -> (ty_params * ty) -> env -> EcDecl.field option diff --git a/tests/field-multi-instance.ec b/tests/field-multi-instance.ec new file mode 100644 index 000000000..42735d5d4 --- /dev/null +++ b/tests/field-multi-instance.ec @@ -0,0 +1,65 @@ +(* Selecting a named `field` structure when a carrier has several instances. + Mirrors ring-multi-instance.ec for the `field` tactic: two field structures + are registered on `real', each named at declaration and picked with + `field []'. *) +require import Real. + +(* ------------------------------------------------------------------ *) +(* Structure A, registered under the name `A'. *) +op zeroA : real = 0%r. +op oneA : real = 1%r. +op addA (x y : real) : real = x + y. +op oppA (x : real) : real = -x. +op mulA (x y : real) : real = x * y. +op invA (x : real) : real = inv x. +op exprA (x : real) (n : int) : real = RField.exp x n. +op ofintA (n : int) : real = n%r. + +instance field [A] with real + op rzero = zeroA op rone = oneA op add = addA op opp = oppA + op mul = mulA op expr = exprA op ofint = ofintA op inv = invA + + proof oner_neq0 by smt() proof addr0 by smt() proof addrA by smt() + proof addrC by smt() proof addrN by smt() proof mulr1 by smt() + proof mulrA by smt() proof mulrC by smt() proof mulrDl by smt() + proof mulrV by smt() + proof expr0 by smt(RField.expr0 RField.exprS RField.exprN) + proof exprS by smt(RField.expr0 RField.exprS RField.exprN) + proof exprN by smt(RField.expr0 RField.exprS RField.exprN) + proof ofint0 by smt() proof ofint1 by smt() + proof ofintS by smt() proof ofintN by smt(). + +(* ------------------------------------------------------------------ *) +(* Structure B, registered under the name `B'. *) +op zeroB : real = 0%r. +op oneB : real = 1%r. +op addB (x y : real) : real = x + y. +op oppB (x : real) : real = -x. +op mulB (x y : real) : real = x * y. +op invB (x : real) : real = inv x. +op exprB (x : real) (n : int) : real = RField.exp x n. +op ofintB (n : int) : real = n%r. + +instance field [B] with real + op rzero = zeroB op rone = oneB op add = addB op opp = oppB + op mul = mulB op expr = exprB op ofint = ofintB op inv = invB + + proof oner_neq0 by smt() proof addr0 by smt() proof addrA by smt() + proof addrC by smt() proof addrN by smt() proof mulr1 by smt() + proof mulrA by smt() proof mulrC by smt() proof mulrDl by smt() + proof mulrV by smt() + proof expr0 by smt(RField.expr0 RField.exprS RField.exprN) + proof exprS by smt(RField.expr0 RField.exprS RField.exprN) + proof exprN by smt(RField.expr0 RField.exprS RField.exprN) + proof ofint0 by smt() proof ofint1 by smt() + proof ofintS by smt() proof ofintN by smt(). + +(* Each selector routes to its own structure. The trailing `smt()' discharges + the `x <> 0' side condition that `field' emits for the inverse. *) +lemma fA (x : real) : + x <> zeroA => mulA (addA x oneA) (invA x) = addA oneA (invA x). +proof. move=> h; field [A]; smt(). qed. + +lemma fB (x : real) : + x <> zeroB => mulB (addB x oneB) (invB x) = addB oneB (invB x). +proof. move=> h; field [B]; smt(). qed. diff --git a/tests/ring-multi-instance.ec b/tests/ring-multi-instance.ec new file mode 100644 index 000000000..e7239341f --- /dev/null +++ b/tests/ring-multi-instance.ec @@ -0,0 +1,63 @@ +(* Selecting a named `ring` structure when a carrier has several instances. + Two ring structures are registered on `int`; each is given a name at + declaration, and the `ring` tactic is directed at one of them with + `ring []`. Bare `ring` keeps resolving the sole/first instance. *) +require import Int. +require (*--*) Ring. + +(* ------------------------------------------------------------------ *) +(* Structure A, registered under the name `A'. *) +op zeroA : int = 0. +op oneA : int = 1. +op addA (x y : int) : int = x + y. +op oppA (x : int) : int = -x. +op mulA (x y : int) : int = x * y. +op exprA (x : int) (n : int) : int = Ring.IntID.exp x n. + +instance ring [A] with int + op rzero = zeroA op rone = oneA op add = addA + op opp = oppA op mul = mulA op expr = exprA + + proof oner_neq0 by smt() proof addr0 by smt() proof addrA by smt() + proof addrC by smt() proof addrN by smt() proof mulr1 by smt() + proof mulrA by smt() proof mulrC by smt() proof mulrDl by smt() + proof expr0 by smt(Ring.IntID.expr0) proof exprS by smt(Ring.IntID.exprS). + +(* Only one instance exists here, so bare `ring` resolves it (this is the + backwards-compatible, single-structure case). *) +lemma bare (x y : int) : addA x (mulA y oneA) = addA (mulA oneA y) x. +proof. ring. qed. + +lemma useA1 (x y : int) : addA x (mulA y oneA) = addA (mulA oneA y) x. +proof. ring [A]. qed. + +(* ------------------------------------------------------------------ *) +(* Structure B, registered under the name `B'. Same underlying maths, but + distinct operator paths, so it is a genuinely separate instance on the + same carrier `int'. *) +op zeroB : int = 0. +op oneB : int = 1. +op addB (x y : int) : int = x + y. +op oppB (x : int) : int = -x. +op mulB (x y : int) : int = x * y. +op exprB (x : int) (n : int) : int = Ring.IntID.exp x n. + +instance ring [B] with int + op rzero = zeroB op rone = oneB op add = addB + op opp = oppB op mul = mulB op expr = exprB + + proof oner_neq0 by smt() proof addr0 by smt() proof addrA by smt() + proof addrC by smt() proof addrN by smt() proof mulr1 by smt() + proof mulrA by smt() proof mulrC by smt() proof mulrDl by smt() + proof expr0 by smt(Ring.IntID.expr0) proof exprS by smt(Ring.IntID.exprS). + +(* Two instances are now registered on `int'. Each selector routes to its own + structure: the operators of the other structure are opaque to it, so a goal + phrased with A's operators is a ring identity only for structure A (and dually + for B). These lemmas being accepted is exactly what shows the selector picks + the intended structure rather than the first-registered one. *) +lemma useA2 (x y : int) : addA x (mulA y oneA) = addA (mulA oneA y) x. +proof. ring [A]. qed. + +lemma useB (x y : int) : addB x (mulB y oneB) = addB (mulB oneB y) x. +proof. ring [B]. qed.