feat: named ring/field instances for ring/field structure selection

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;

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;

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

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

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

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 }

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;

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

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;

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;

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

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

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 [<name>]'. *)
+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.

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 [<name>]`. 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.