Skip to content

Commit 141ddfd

Browse files
strubstrub
committed
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.
1 parent 3800968 commit 141ddfd

14 files changed

Lines changed: 178 additions & 30 deletions

‎src/ecDecl.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -336,6 +336,7 @@ type rkind = [
336336
]
337337

338338
type ring = {
339+
r_name : EcSymbols.symbol option;
339340
r_type : EcTypes.ty;
340341
r_zero : EcPath.path;
341342
r_one : EcPath.path;

‎src/ecDecl.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -199,6 +199,7 @@ type rkind = [
199199
]
200200

201201
type ring = {
202+
r_name : EcSymbols.symbol option;
202203
r_type : EcTypes.ty;
203204
r_zero : EcPath.path;
204205
r_one : EcPath.path;

‎src/ecHiGoal.ml‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ let process_clear (info : clear_info) tc =
181181
t_clears ~leniant:true clear_list tc
182182

183183
(* -------------------------------------------------------------------- *)
184-
let process_algebra mode kind eqs (tc : tcenv1) =
184+
let process_algebra mode kind ?name eqs (tc : tcenv1) =
185185
let (env, hyps, concl) = FApi.tc1_eflat tc in
186186

187187
if not (EcAlgTactic.is_module_loaded env) then
@@ -210,6 +210,10 @@ let process_algebra mode kind eqs (tc : tcenv1) =
210210

211211
let tparams = (LDecl.tohyps hyps).h_tvar in
212212

213+
let named = omap unloc name in
214+
let named_suffix =
215+
match named with None -> "" | Some n -> Printf.sprintf " named `%s'" n in
216+
213217
let tactic =
214218
match
215219
match mode, kind with
@@ -220,14 +224,14 @@ let process_algebra mode kind eqs (tc : tcenv1) =
220224
with
221225
| `Ring t ->
222226
let r =
223-
match TT.get_ring (tparams, ty) env with
224-
| None -> tacuerror "cannot find a ring structure"
227+
match TT.get_ring ?name:named (tparams, ty) env with
228+
| None -> tacuerror "cannot find a ring structure%s" named_suffix
225229
| Some r -> r
226230
in t r eqs (f1, f2)
227231
| `Field t ->
228232
let r =
229-
match TT.get_field (tparams, ty) env with
230-
| None -> tacuerror "cannot find a field structure"
233+
match TT.get_field ?name:named (tparams, ty) env with
234+
| None -> tacuerror "cannot find a field structure%s" named_suffix
231235
| Some r -> r
232236
in t r eqs (f1, f2)
233237
in

‎src/ecHiGoal.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ val process_wlog : suff:bool -> psymbol list -> pformula -> backward
104104
val process_genhave : ttenv -> pgenhave -> backward
105105

106106
(* -------------------------------------------------------------------- *)
107-
val process_algebra : [`Solve] -> [`Ring|`Field] -> psymbol list -> backward
107+
val process_algebra : [`Solve] -> [`Ring|`Field] -> ?name:psymbol -> psymbol list -> backward
108108

109109
(* -------------------------------------------------------------------- *)
110110
val process_crushmode : crushmode -> bool * backward option

‎src/ecHiTacticals.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -138,8 +138,8 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) =
138138
| Psplit (`Default i) -> process_split ?i
139139
| Psplit (`All `Maybe)-> process_split_all ~must:false
140140
| Psplit (`All `One) -> process_split_all ~must:true
141-
| Pfield st -> process_algebra `Solve `Field st
142-
| Pring st -> process_algebra `Solve `Ring st
141+
| Pfield (nm, st) -> process_algebra `Solve `Field ?name:nm st
142+
| Pring (nm, st) -> process_algebra `Solve `Ring ?name:nm st
143143
| Palg_norm -> EcStrongRing.t_alg_eq
144144
| Pexists fs -> process_exists fs
145145
| Pleft -> process_left

‎src/ecParser.mly‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1732,10 +1732,11 @@ subtype_rename:
17321732
(* -------------------------------------------------------------------- *)
17331733
(* Type classes (instances) *)
17341734
tycinstance:
1735-
| loca=is_local INSTANCE x=qident
1735+
| loca=is_local INSTANCE x=qident nm=bracket(ident)?
17361736
WITH typ=tyvars_decl? ty=loc(type_exp) ops=tyci_op* axs=tyci_ax*
17371737
{
17381738
{ pti_name = x;
1739+
pti_as = nm;
17391740
pti_type = (odfl [] typ, ty);
17401741
pti_ops = ops;
17411742
pti_axs = axs;
@@ -1744,10 +1745,11 @@ tycinstance:
17441745
}
17451746
}
17461747

1747-
| loca=is_local INSTANCE x=qident c=uoption(UINT) p=uoption(UINT)
1748+
| loca=is_local INSTANCE x=qident nm=bracket(ident)? c=uoption(UINT) p=uoption(UINT)
17481749
WITH typ=tyvars_decl? ty=loc(type_exp) ops=tyci_op* axs=tyci_ax*
17491750
{
17501751
{ pti_name = x;
1752+
pti_as = nm;
17511753
pti_type = (odfl [] typ, ty);
17521754
pti_ops = ops;
17531755
pti_axs = axs;
@@ -2868,11 +2870,11 @@ logtactic:
28682870
| SPLIT PLUS
28692871
{ Psplit (`All `One) }
28702872

2871-
| FIELD eqs=ident*
2872-
{ Pfield eqs }
2873+
| FIELD nm=bracket(ident)? eqs=ident*
2874+
{ Pfield (nm, eqs) }
28732875

2874-
| RING eqs=ident*
2875-
{ Pring eqs }
2876+
| RING nm=bracket(ident)? eqs=ident*
2877+
{ Pring (nm, eqs) }
28762878

28772879
| ALGNORM
28782880
{ Palg_norm }

‎src/ecParsetree.ml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1108,8 +1108,8 @@ type logtactic =
11081108
| Passumption
11091109
| Psmt of pprover_infos
11101110
| Psplit of [ `Default of int option | `All of [ `Maybe | `One ] ]
1111-
| Pfield of psymbol list
1112-
| Pring of psymbol list
1111+
| Pfield of psymbol option * psymbol list
1112+
| Pring of psymbol option * psymbol list
11131113
| Palg_norm
11141114
| Pexists of ppt_arg located list
11151115
| Pleft
@@ -1212,6 +1212,7 @@ type prealize = {
12121212
(* -------------------------------------------------------------------- *)
12131213
type ptycinstance = {
12141214
pti_name : pqsymbol;
1215+
pti_as : psymbol option;
12151216
pti_type : ptyparams * pty;
12161217
pti_ops : (psymbol * (pty list * pqsymbol)) list;
12171218
pti_axs : (psymbol * ptactic_core) list;

‎src/ecScope.ml‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2509,8 +2509,9 @@ module Ty = struct
25092509
let p_field = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field" ], "field" )
25102510

25112511
(* ------------------------------------------------------------------ *)
2512-
let ring_of_symmap env ty kind symbols =
2513-
{ r_type = ty;
2512+
let ring_of_symmap ?name env ty kind symbols =
2513+
{ r_name = name;
2514+
r_type = ty;
25142515
r_zero = oget (Mstr.find_opt "rzero" symbols);
25152516
r_one = oget (Mstr.find_opt "rone" symbols);
25162517
r_add = oget (Mstr.find_opt "add" symbols);
@@ -2541,7 +2542,7 @@ module Ty = struct
25412542

25422543
let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in
25432544
let symbols = check_tci_operators env ty tci.pti_ops symbols in
2544-
let cr = ring_of_symmap env (snd ty) kind symbols in
2545+
let cr = ring_of_symmap ?name:(omap unloc tci.pti_as) env (snd ty) kind symbols in
25452546
let axioms = EcAlgTactic.ring_axioms env cr in
25462547
let lc = (tci.pti_loca :> locality) in
25472548
let inter = check_tci_axioms scope mode tci.pti_axs axioms lc in
@@ -2562,8 +2563,8 @@ module Ty = struct
25622563
in Ax.add_defer scope inter
25632564

25642565
(* ------------------------------------------------------------------ *)
2565-
let field_of_symmap env ty symbols =
2566-
{ f_ring = ring_of_symmap env ty `Integer symbols;
2566+
let field_of_symmap ?name env ty symbols =
2567+
{ f_ring = ring_of_symmap ?name env ty `Integer symbols;
25672568
f_inv = oget (Mstr.find_opt "inv" symbols);
25682569
f_div = Mstr.find_opt "div" symbols; }
25692570

@@ -2583,7 +2584,7 @@ module Ty = struct
25832584
hierror "field instances cannot be polymorphic";
25842585
let symbols = EcAlgTactic.field_symbols env (snd ty) in
25852586
let symbols = check_tci_operators env ty tci.pti_ops symbols in
2586-
let cr = field_of_symmap env (snd ty) symbols in
2587+
let cr = field_of_symmap ?name:(omap unloc tci.pti_as) env (snd ty) symbols in
25872588
let axioms = EcAlgTactic.field_axioms env cr in
25882589
let lc = (tci.pti_loca :> locality) in
25892590
let inter = check_tci_axioms scope mode tci.pti_axs axioms lc; in

‎src/ecSubst.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -994,7 +994,8 @@ let fresh_scparams (s : subst) (xtys : (EcIdent.t * ty) list) =
994994

995995
(* -------------------------------------------------------------------- *)
996996
let subst_ring (s : subst) cr =
997-
{ r_type = subst_ty s cr.r_type;
997+
{ r_name = cr.r_name;
998+
r_type = subst_ty s cr.r_type;
998999
r_zero = subst_path s cr.r_zero;
9991000
r_one = subst_path s cr.r_one;
10001001
r_add = subst_path s cr.r_add;

‎src/ecTheoryReplay.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1040,7 +1040,8 @@ and replay_instance
10401040
let (typ, ty) = EcSubst.subst_genty subst (typ, ty) in
10411041
let tc =
10421042
let rec doring cr =
1043-
{ r_type = EcSubst.subst_ty subst cr.r_type;
1043+
{ r_name = cr.r_name;
1044+
r_type = EcSubst.subst_ty subst cr.r_type;
10441045
r_zero = forpath cr.r_zero;
10451046
r_one = forpath cr.r_one;
10461047
r_add = forpath cr.r_add;

0 commit comments

Comments
 (0)