Skip to content

Commit eeb3470

Browse files
strubstrub
committed
Rework stdlib clones
1 parent fdd7813 commit eeb3470

File tree

8 files changed

+46
-89
lines changed

8 files changed

+46
-89
lines changed

‎src/ecScope.ml

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1971,10 +1971,10 @@ module Theory = struct
19711971
exception TopScope
19721972

19731973
(* ------------------------------------------------------------------ *)
1974-
let bind (scope : scope) (cth : thloaded) =
1974+
let bind ?(import = true) (scope : scope) (cth : thloaded) =
19751975
assert (scope.sc_pr_uc = None);
19761976
{ scope with
1977-
sc_env = EcSection.add_th ~import:true cth scope.sc_env }
1977+
sc_env = EcSection.add_th ~import cth scope.sc_env }
19781978

19791979
(* ------------------------------------------------------------------ *)
19801980
let required (scope : scope) (name : required_info) =
@@ -2052,13 +2052,13 @@ module Theory = struct
20522052
((cth, required), scope.sc_name, sup)
20532053

20542054
(* ------------------------------------------------------------------ *)
2055-
let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
2055+
let exit ?import ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
20562056
assert (scope.sc_pr_uc = None);
20572057

20582058
let cth = exit_r ~pempty (add_clears clears scope) in
20592059
let ((cth, required), (name, _), scope) = cth in
20602060
let scope = List.fold_right require_loaded required scope in
2061-
let scope = ofold (fun cth scope -> bind scope cth) scope cth in
2061+
let scope = ofold (fun cth scope -> bind ?import scope cth) scope cth in
20622062
(name, scope)
20632063

20642064
(* ------------------------------------------------------------------ *)
@@ -2209,7 +2209,8 @@ module Cloning = struct
22092209

22102210
(* ------------------------------------------------------------------ *)
22112211
let hooks : scope R.ovrhooks =
2212-
let thexit sc pempty = snd (Theory.exit ?clears:None ~pempty sc) in
2212+
let thexit sc ~import pempty =
2213+
snd (Theory.exit ~import ?clears:None ~pempty sc) in
22132214
let add_item scope ~import item =
22142215
let item = EcTheory.mkitem ~import item in
22152216
{ scope with sc_env = EcSection.add_item item scope.sc_env } in

‎src/ecScope.mli

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,8 @@ module Theory : sig
151151
(* [exit scope] close and finalize the top-most theory and returns
152152
* its name. Raises [TopScope] if [scope] has not super scope. *)
153153
val exit :
154-
?pempty:[`ClearOnly | `Full | `No]
154+
?import:bool
155+
-> ?pempty:[`ClearOnly | `Full | `No]
155156
-> ?clears:(pqsymbol option) list
156157
-> scope -> symbol * scope
157158

‎src/ecThCloning.ml

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ type evclone = {
6262
evc_modexprs : (me_override located) Msym.t;
6363
evc_modtypes : (mt_override located) Msym.t;
6464
evc_lemmas : evlemma;
65-
evc_ths : evclone Msym.t;
65+
evc_ths : (evclone * bool) Msym.t;
6666
}
6767

6868
and evlemma = {
@@ -91,7 +91,9 @@ let rec evc_update (upt : evclone -> evclone) (nm : symbol list) (evc : evclone)
9191
| x :: nm ->
9292
let ths =
9393
Msym.change
94-
(fun sub -> Some (evc_update upt nm (odfl evc_empty sub)))
94+
(fun sub ->
95+
let subevc, clear = odfl (evc_empty, false) sub in
96+
Some (evc_update upt nm subevc, clear))
9597
x evc.evc_ths
9698
in
9799
{ evc with evc_ths = ths }
@@ -101,8 +103,8 @@ let rec evc_get (nm : symbol list) (evc : evclone) =
101103
| [] -> Some evc
102104
| x :: nm ->
103105
match Msym.find_opt x evc.evc_ths with
104-
| None -> None
105-
| Some evc -> evc_get nm evc
106+
| None -> None
107+
| Some (evc, _) -> evc_get nm evc
106108

107109
(* -------------------------------------------------------------------- *)
108110
let find_mc =
@@ -390,6 +392,13 @@ end = struct
390392
let thd = let thd = EcPath.toqsymbol sp in (fst thd @ [snd thd]) in
391393
let xdth = nm @ [x] in
392394

395+
assert (not (Msym.mem x evc.evc_ths));
396+
397+
let evc = { evc with
398+
evc_ths = Msym.change (fun sub ->
399+
let sub, clear = odfl (evc_empty, false) sub in
400+
Some (sub, clear || (mode <> `Alias))) x evc.evc_ths } in
401+
393402
let rec doit_r prefix (proofs, evc) dth =
394403
match dth with
395404
| Th_type (x, _) ->

‎src/ecThCloning.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ type evclone = {
4848
evc_modexprs : (me_override located) Msym.t;
4949
evc_modtypes : (mt_override located) Msym.t;
5050
evc_lemmas : evlemma;
51-
evc_ths : evclone Msym.t;
51+
evc_ths : (evclone * bool) Msym.t;
5252
}
5353

5454
and evlemma = {

‎src/ecTheoryReplay.ml

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ and 'a ovrhooks = {
3636
henv : 'a -> EcSection.scenv;
3737
hadd_item : 'a -> import:bool -> EcTheory.theory_item_r -> 'a;
3838
hthenter : 'a -> thmode -> symbol -> is_local -> 'a;
39-
hthexit : 'a -> [`Full | `ClearOnly | `No] -> 'a;
39+
hthexit : 'a -> import:bool -> [`Full | `ClearOnly | `No] -> 'a;
4040
herr : 'b . ?loc:EcLocation.t -> string -> 'b;
4141
}
4242

@@ -989,7 +989,9 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) =
989989
let thmode = cth.cth_mode in
990990
let (subst, x) = rename ove subst (`Theory, ox) in
991991
let subovrds = Msym.find_opt ox ove.ovre_ovrd.evc_ths in
992-
let subovrds = EcUtils.odfl evc_empty subovrds in
992+
let subovrds = EcUtils.odfl (evc_empty, false) subovrds in
993+
let subovrds, clear = subovrds in
994+
let hidden = hidden || clear in
993995
let subove = { ove with
994996
ovre_ovrd = subovrds;
995997
ovre_abstract = ove.ovre_abstract || (thmode = `Abstract);
@@ -1006,7 +1008,7 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) =
10061008
List.fold_left
10071009
(fun state item -> replay1 subove state (hidden, item))
10081010
(subst, ops, proofs, subscope) cth.cth_items in
1009-
let scope = ove.ovre_hooks.hthexit subscope `Full in
1011+
let scope = ove.ovre_hooks.hthexit ~import:(not hidden) subscope `Full in
10101012
(subst, ops, proofs, scope)
10111013

10121014
in (subst, ops, proofs, subscope)
@@ -1038,7 +1040,7 @@ let replay (hooks : 'a ovrhooks)
10381040
List.fold_left
10391041
(fun state item -> replay1 ove state (hidden, item))
10401042
(subst, Mp.empty, [], scope) items in
1041-
let scope = if incl then scope else hooks.hthexit scope `No in
1043+
let scope = if incl then scope else hooks.hthexit scope ~import:true `No in
10421044
(List.rev proofs, scope)
10431045

10441046
with EcEnv.DuplicatedBinding x ->

‎src/ecTheoryReplay.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ and 'a ovrhooks = {
2727
henv : 'a -> EcSection.scenv;
2828
hadd_item : 'a -> import:bool -> EcTheory.theory_item_r -> 'a;
2929
hthenter : 'a -> thmode -> symbol -> EcTypes.is_local -> 'a;
30-
hthexit : 'a -> [`Full | `ClearOnly | `No] -> 'a;
30+
hthexit : 'a -> import:bool -> [`Full | `ClearOnly | `No] -> 'a;
3131
herr : 'b . ?loc:EcLocation.t -> string -> 'b;
3232
}
3333

‎theories/algebra/Poly.ec

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -504,7 +504,7 @@ qed.
504504
lemma onep_neq0 : poly1 <> poly0.
505505
proof. by apply/negP => /poly_eqP /(_ 0); rewrite !polyCE /= oner_neq0. qed.
506506

507-
clone import Ring.ComRing as PolyComRing with
507+
clone export Ring.ComRing as PolyComRing with
508508
type t <= poly ,
509509
op zeror <= poly0,
510510
op oner <= poly1,

‎theories/algebra/PolyReduce.ec

Lines changed: 16 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -8,46 +8,22 @@ require import Ring StdOrder IntDiv ZModP Ideal Poly.
88

99
(* ==================================================================== *)
1010
abstract theory PolyReduce.
11+
type coeff.
1112

12-
clone import PolyComRing as BasePoly with
13-
(* We currently don't care about inverting polynomials *)
14-
pred PolyComRing.unit <= fun p => exists q, polyM q p = oner,
15-
op PolyComRing.invr <= fun p => choiceb (fun q => polyM q p = oner) p
16-
proof PolyComRing.mulVr, PolyComRing.unitP, PolyComRing.unitout.
17-
realize PolyComRing.mulVr by smt(choicebP).
18-
realize PolyComRing.unitP by smt().
19-
realize PolyComRing.unitout by smt(choiceb_dfl).
13+
clone import ComRing as Coeff with type t <= coeff.
2014

21-
(*-*) import Coeff PolyComRing BigPoly BigCf.
15+
clone export PolyComRing as BasePoly
16+
with type coeff <- coeff,
17+
theory Coeff <- Coeff.
18+
19+
import Coeff BigPoly BigCf.
2220

2321
(* -------------------------------------------------------------------- *)
2422
clone import IdealComRing as PIdeal with
25-
type t <- BasePoly.poly,
26-
op IComRing.zeror <- BasePoly.poly0,
27-
op IComRing.oner <- BasePoly.poly1,
28-
op IComRing.( + ) <- BasePoly.PolyComRing.( + ),
29-
op IComRing.([-]) <- BasePoly.PolyComRing.([-]),
30-
op IComRing.( * ) <- BasePoly.PolyComRing.( * ),
31-
op IComRing.invr <- BasePoly.PolyComRing.invr,
32-
pred IComRing.unit <- BasePoly.PolyComRing.unit,
33-
op BigDom.BAdd.big <- BasePoly.BigPoly.PCA.big<:'a>,
34-
op BigDom.BMul.big <- BasePoly.BigPoly.PCM.big<:'a>
35-
36-
proof IComRing.addrA by exact: BasePoly.PolyComRing.addrA ,
37-
IComRing.addrC by exact: BasePoly.PolyComRing.addrC ,
38-
IComRing.add0r by exact: BasePoly.PolyComRing.add0r ,
39-
IComRing.addNr by exact: BasePoly.PolyComRing.addNr ,
40-
IComRing.oner_neq0 by exact: BasePoly.PolyComRing.oner_neq0,
41-
IComRing.mulrA by exact: BasePoly.PolyComRing.mulrA ,
42-
IComRing.mulrC by exact: BasePoly.PolyComRing.mulrC ,
43-
IComRing.mul1r by exact: BasePoly.PolyComRing.mul1r ,
44-
IComRing.mulrDl by exact: BasePoly.PolyComRing.mulrDl ,
45-
IComRing.mulVr by exact: BasePoly.PolyComRing.mulVr ,
46-
IComRing.unitP by exact: BasePoly.PolyComRing.unitP ,
47-
IComRing.unitout by exact: BasePoly.PolyComRing.unitout
48-
49-
remove abbrev IComRing.(-)
50-
remove abbrev IComRing.(/)
23+
type t <- BasePoly.poly,
24+
theory IComRing <- BasePoly.PolyComRing,
25+
op BigDom.BAdd.big <- BasePoly.BigPoly.PCA.big<:'a>,
26+
op BigDom.BMul.big <- BasePoly.BigPoly.PCM.big<:'a>
5127

5228
remove abbrev BigDom.BAdd.bigi
5329
remove abbrev BigDom.BMul.bigi.
@@ -484,56 +460,24 @@ end PolyReduce.
484460

485461
(* ==================================================================== *)
486462
abstract theory PolyReduceZp.
463+
type coeff.
487464

488465
op p : { int | 2 <= p } as ge2_p.
489466

490467
clone import ZModRing as Zp with
491468
op p <= p
492469
proof ge2_p by exact/ge2_p.
493470

494-
type Zp = zmod.
495-
496-
clone include PolyReduce with
497-
type BasePoly.coeff <- Zp,
498-
pred BasePoly.Coeff.unit <- Zp.unit,
499-
op BasePoly.Coeff.zeror <- Zp.zero,
500-
op BasePoly.Coeff.oner <- Zp.one,
501-
op BasePoly.Coeff.( + ) <- Zp.( + ),
502-
op BasePoly.Coeff.([-]) <- Zp.([-]),
503-
op BasePoly.Coeff.( * ) <- Zp.( * ),
504-
op BasePoly.Coeff.invr <- Zp.inv,
505-
op BasePoly.Coeff.ofint <- Zp.ZModpRing.ofint,
506-
op BasePoly.Coeff.exp <- Zp.ZModpRing.exp,
507-
op BasePoly.Coeff.intmul <- Zp.ZModpRing.intmul,
508-
op BasePoly.Coeff.lreg <- Zp.ZModpRing.lreg
509-
proof BasePoly.Coeff.addrA by exact Zp.ZModpRing.addrA
510-
proof BasePoly.Coeff.addrC by exact Zp.ZModpRing.addrC
511-
proof BasePoly.Coeff.add0r by exact Zp.ZModpRing.add0r
512-
proof BasePoly.Coeff.addNr by exact Zp.ZModpRing.addNr
513-
proof BasePoly.Coeff.oner_neq0 by exact Zp.ZModpRing.oner_neq0
514-
proof BasePoly.Coeff.mulrA by exact Zp.ZModpRing.mulrA
515-
proof BasePoly.Coeff.mulrC by exact Zp.ZModpRing.mulrC
516-
proof BasePoly.Coeff.mul1r by exact Zp.ZModpRing.mul1r
517-
proof BasePoly.Coeff.mulrDl by exact Zp.ZModpRing.mulrDl
518-
proof BasePoly.Coeff.mulVr by exact Zp.ZModpRing.mulVr
519-
proof BasePoly.Coeff.unitP by exact Zp.ZModpRing.unitP
520-
proof BasePoly.Coeff.unitout by exact Zp.ZModpRing.unitout
521-
remove abbrev BasePoly.Coeff.(-)
522-
remove abbrev BasePoly.Coeff.(/).
523-
524-
clear [BasePoly.Coeff.*].
525-
clear [BasePoly.Coeff.AddMonoid.*].
526-
clear [BasePoly.Coeff.MulMonoid.*].
527-
528-
(* -------------------------------------------------------------------- *)
529-
import BasePoly.
471+
clone import PolyReduce with
472+
type coeff <- Zp.zmod,
473+
theory Coeff <- ZModpRing.
530474

531475
(* ==================================================================== *)
532476
(* We already know that polyXnD1 is finite. However, we prove here that *)
533477
(* we can build the full-uniform distribution over polyXnD1 by sampling *)
534478
(* uniformly each coefficient in the reduced form representation. *)
535479

536-
op dpolyX (dcoeff : Zp distr) : polyXnD1 distr =
480+
op dpolyX (dcoeff : zmod distr) : polyXnD1 distr =
537481
dmap (dpoly n dcoeff) pinject.
538482

539483
lemma dpolyX_ll d : is_lossless d => is_lossless (dpolyX d).

0 commit comments

Comments
 (0)