Skip to content

Commit 06da2d3

Browse files
tabareautabareau
authored
Merge pull request #905 from JasonGross/coq-8.16+pre-refactor-quotation-mfsets
Populate some early MSets and FSets modules
2 parents 2dba386 + b486251 commit 06da2d3

File tree

7 files changed

+61
-4
lines changed

7 files changed

+61
-4
lines changed

‎common/theories/Kernames.v‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11

22
(* Distributed under the terms of the MIT license. *)
33
From Coq Require Import Lia MSetList OrderedTypeAlt OrderedTypeEx FMapAVL FMapFacts MSetAVL MSetFacts MSetProperties.
4-
From MetaCoq.Utils Require Import utils.
4+
From MetaCoq.Utils Require Import utils MCMSets MCFSets.
55
From Coq Require Import ssreflect.
66
From Equations Require Import Equations.
77

@@ -296,6 +296,8 @@ End Kername.
296296

297297
Module KernameMap := FMapAVL.Make Kername.OT.
298298
Module KernameMapFact := FMapFacts.WProperties KernameMap.
299+
Module KernameMapExtraFact := FSets.WFactsExtra_fun Kername.OT KernameMap KernameMapFact.F.
300+
Module KernameMapDecide := FMapAVL.Decide Kername.OT KernameMap.
299301

300302
Notation eq_kername := (eqb (A:=kername)) (only parsing).
301303

@@ -313,6 +315,9 @@ Module KernameSet := MSetAVL.Make Kername.
313315
Module KernameSetFact := MSetFacts.WFactsOn Kername KernameSet.
314316
Module KernameSetOrdProp := MSetProperties.OrdProperties KernameSet.
315317
Module KernameSetProp := KernameSetOrdProp.P.
318+
Module KernameSetDecide := KernameSetProp.Dec.
319+
Module KernameSetExtraOrdProp := MSets.ExtraOrdProperties KernameSet KernameSetOrdProp.
320+
Module KernameSetExtraDecide := MSetAVL.Decide Kername KernameSet.
316321

317322
Lemma knset_in_fold_left {A} kn f (l : list A) acc :
318323
KernameSet.In kn (fold_left (fun acc x => KernameSet.union (f x) acc) l acc) <->

‎common/theories/Universes.v‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
From Coq Require Import OrdersAlt MSetList MSetAVL MSetFacts MSetProperties MSetDecide FMapAVL.
22
From Equations Require Import Equations.
3-
From MetaCoq.Utils Require Import utils.
3+
From MetaCoq.Utils Require Import utils MCMSets MCFSets.
44
From MetaCoq.Common Require Import BasicAst config.
55
Require Import ssreflect.
66

@@ -165,6 +165,8 @@ Module LevelSetFact := WFactsOn Level LevelSet.
165165
Module LevelSetOrdProp := MSetProperties.OrdProperties LevelSet.
166166
Module LevelSetProp := LevelSetOrdProp.P.
167167
Module LevelSetDecide := LevelSetProp.Dec.
168+
Module LevelSetExtraOrdProp := MSets.ExtraOrdProperties LevelSet LevelSetOrdProp.
169+
Module LevelSetExtraDecide := MSetAVL.Decide Level LevelSet.
168170
Module LS := LevelSet.
169171

170172
Ltac lsets := LevelSetDecide.fsetdec.
@@ -342,6 +344,7 @@ Module LevelExprSetFact := WFactsOn LevelExpr LevelExprSet.
342344
Module LevelExprSetOrdProp := MSetProperties.OrdProperties LevelExprSet.
343345
Module LevelExprSetProp := LevelExprSetOrdProp.P.
344346
Module LevelExprSetDecide := LevelExprSetProp.Dec.
347+
Module LevelExprSetExtraOrdProp := MSets.ExtraOrdProperties LevelExprSet LevelExprSetOrdProp.
345348

346349
(* We have decidable equality w.r.t leibniz equality for sets of levels.
347350
This means concreteUniverses also have a decidable equality. *)
@@ -1215,6 +1218,8 @@ End Universe.
12151218

12161219
Module UniverseMap := FMapAVL.Make Universe.OTOrig.
12171220
Module UniverseMapFact := FMapFacts.WProperties UniverseMap.
1221+
Module UniverseMapExtraFact := FSets.WFactsExtra_fun Universe.OTOrig UniverseMap UniverseMapFact.F.
1222+
Module UniverseMapDecide := FMapAVL.Decide Universe.OTOrig UniverseMap.
12181223

12191224
Definition is_propositional u :=
12201225
Universe.is_prop u || Universe.is_sprop u.
@@ -1485,6 +1490,8 @@ Module ConstraintSetOrdProp := MSetProperties.OrdProperties ConstraintSet.
14851490
Module ConstraintSetProp := ConstraintSetOrdProp.P.
14861491
Module CS := ConstraintSet.
14871492
Module ConstraintSetDecide := ConstraintSetProp.Dec.
1493+
Module ConstraintSetExtraOrdProp := MSets.ExtraOrdProperties ConstraintSet ConstraintSetOrdProp.
1494+
Module ConstraintSetExtraDecide := MSetAVL.Decide UnivConstraint ConstraintSet.
14881495
Ltac csets := ConstraintSetDecide.fsetdec.
14891496

14901497
Notation "(=_cset)" := ConstraintSet.Equal (at level 0).

‎template-coq/_PluginProject‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,8 +123,12 @@ gen-src/logic2.ml
123123
gen-src/logic2.mli
124124
gen-src/mCCompare.ml
125125
gen-src/mCCompare.mli
126+
gen-src/mCFSets.ml
127+
gen-src/mCFSets.mli
126128
gen-src/mCList.ml
127129
gen-src/mCList.mli
130+
gen-src/mCMSets.ml
131+
gen-src/mCMSets.mli
128132
gen-src/mCOption.ml
129133
gen-src/mCOption.mli
130134
gen-src/mCPrelude.ml
@@ -232,6 +236,22 @@ gen-src/zeven.ml
232236
gen-src/zeven.mli
233237
gen-src/zpower.ml
234238
gen-src/zpower.mli
239+
# gen-src/carryType.ml
240+
# gen-src/carryType.mli
241+
# gen-src/coreTactics.ml
242+
# gen-src/coreTactics.mli
243+
# gen-src/depElim.ml
244+
# gen-src/depElim.mli
245+
# gen-src/floatClass.ml
246+
# gen-src/floatClass.mli
247+
# gen-src/init.ml
248+
# gen-src/init.mli
249+
# gen-src/mCUint63.ml
250+
# gen-src/mCUint63.mli
251+
# gen-src/noConfusion.ml
252+
# gen-src/noConfusion.mli
253+
# gen-src/wf.ml
254+
# gen-src/wf.mli
235255

236256
gen-src/metacoq_template_plugin.mlpack
237257

‎template-coq/_PluginProject.in‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,8 +121,12 @@ gen-src/logic2.ml
121121
gen-src/logic2.mli
122122
gen-src/mCCompare.ml
123123
gen-src/mCCompare.mli
124+
gen-src/mCFSets.ml
125+
gen-src/mCFSets.mli
124126
gen-src/mCList.ml
125127
gen-src/mCList.mli
128+
gen-src/mCMSets.ml
129+
gen-src/mCMSets.mli
126130
gen-src/mCOption.ml
127131
gen-src/mCOption.mli
128132
gen-src/mCPrelude.ml
@@ -230,6 +234,22 @@ gen-src/zeven.ml
230234
gen-src/zeven.mli
231235
gen-src/zpower.ml
232236
gen-src/zpower.mli
237+
# gen-src/carryType.ml
238+
# gen-src/carryType.mli
239+
# gen-src/coreTactics.ml
240+
# gen-src/coreTactics.mli
241+
# gen-src/depElim.ml
242+
# gen-src/depElim.mli
243+
# gen-src/floatClass.ml
244+
# gen-src/floatClass.mli
245+
# gen-src/init.ml
246+
# gen-src/init.mli
247+
# gen-src/mCUint63.ml
248+
# gen-src/mCUint63.mli
249+
# gen-src/noConfusion.ml
250+
# gen-src/noConfusion.mli
251+
# gen-src/wf.ml
252+
# gen-src/wf.mli
233253

234254
gen-src/metacoq_template_plugin.mlpack
235255

‎template-coq/gen-src/metacoq_template_plugin.mlpack‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,8 @@ MCString
7878
MCUtils
7979
Signature
8080
All_Forall
81+
MCFSets
82+
MCMSets
8183
Config0
8284
Kernames
8385
Primitive

‎utils/theories/MCFSets.v‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ From MetaCoq.Utils Require Import MCReflect MCUtils.
44
From MetaCoq.Utils.MCTactics Require Import SpecializeUnderBindersBy DestructHead SplitInContext.
55
From Equations.Prop Require Import Classes.
66

7-
Module FSets.
7+
Module Export FSets.
88
Module Type WFacts_funSig (E : DecidableTypeOrig) (M : WSfun E) := Nop <+ WFacts_fun E M.
99

1010
Module WFactsExtra_fun (E : DecidableTypeOrig) (Import W : WSfun E) (Import WFacts : WFacts_funSig E W).
@@ -70,7 +70,7 @@ End FMapList.
7070
Module FMapAVL.
7171
Module Type MakeSig (T : OrderedTypeOrig) := Nop <+ FMapAVL.Make T.
7272

73-
Module Decide (T : OrderedTypeOrig) (M : FMapAVL.MakeSig T). (* (Import WFacts : WFacts_funSig T M) (qT : QuotationOfOrderedTypeOrig T) (qM : FMapAVL.QuotationOfMake T M) (qWFacts : QuotationOfWFacts_fun T M WFacts).*)
73+
Module Decide (T : OrderedTypeOrig) (M : FMapAVL.MakeSig T).
7474
Module Raw.
7575
Scheme Induction for M.Raw.tree Sort Type.
7676
Scheme Induction for M.Raw.tree Sort Set.
@@ -145,4 +145,6 @@ Module FMapAVL.
145145
End with_t.
146146
End Raw.
147147
End Decide.
148+
149+
Module Type DecideSig (T : OrderedTypeOrig) (M : FMapAVL.MakeSig T) := Nop <+ Decide T M.
148150
End FMapAVL.

‎utils/theories/MCMSets.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ Module Export MSets.
7979
Module Type WExtraPropertiesOnSig (E : DecidableType) (W : WSetsOn E) (WProperties : WPropertiesOnSig E W) := Nop <+ WExtraPropertiesOn E W WProperties.
8080

8181
Module ExtraOrdProperties (Import M : Sets) (Import MOrdProperties : OrdPropertiesSig M).
82+
Module P := WExtraPropertiesOn M.E M MOrdProperties.P.
8283

8384
Definition above x s : bool := for_all (fun y => if ME.lt_dec y x then true else false) s.
8485
Definition below x s : bool := for_all (fun y => if ME.lt_dec x y then true else false) s.

0 commit comments

Comments
 (0)