Skip to content

Commit 8bd85e5

Browse files
JasonGrossJasonGross
committed
Use a more systematic mangling of universe names
This should hopefully both speed things up and potentially avoid universe inconsistencies. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 27m56.55s | 1728408 ko | Total Time / Peak Mem | 35m28.28s | 1976000 ko || -7m31.72s || -247592 ko | -21.22% | -12.52% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 3m44.84s | 1368456 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 4m28.56s | 1347576 ko || -0m43.71s || 20880 ko | -16.27% | +1.54% 1m38.93s | 1412680 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 2m13.30s | 1674924 ko || -0m34.37s || -262244 ko | -25.78% | -15.65% 0m29.41s | 1116164 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m56.50s | 1261512 ko || -0m27.08s || -145348 ko | -47.94% | -11.52% 3m18.00s | 1722424 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 3m42.94s | 1976000 ko || -0m24.93s || -253576 ko | -11.18% | -12.83% 0m52.40s | 878548 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 1m16.86s | 1041496 ko || -0m24.46s || -162948 ko | -31.82% | -15.64% 0m50.59s | 872104 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 1m14.63s | 1028104 ko || -0m24.03s || -156000 ko | -32.21% | -15.17% 1m00.31s | 1284464 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 1m23.83s | 1355772 ko || -0m23.51s || -71308 ko | -28.05% | -5.25% 0m48.68s | 857164 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 1m10.88s | 997404 ko || -0m22.19s || -140240 ko | -31.32% | -14.06% 0m47.98s | 864128 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 1m10.28s | 1009492 ko || -0m22.30s || -145364 ko | -31.73% | -14.39% 1m29.10s | 1275632 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 1m49.82s | 1297876 ko || -0m20.71s || -22244 ko | -18.86% | -1.71% 1m21.35s | 1275952 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 1m40.69s | 1293716 ko || -0m19.34s || -17764 ko | -19.20% | -1.37% 1m22.80s | 1276260 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 1m41.41s | 1301716 ko || -0m18.60s || -25456 ko | -18.35% | -1.95% 0m29.22s | 909244 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m46.57s | 1017928 ko || -0m17.35s || -108684 ko | -37.25% | -10.67% 0m52.42s | 1086680 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 1m07.19s | 1140600 ko || -0m14.76s || -53920 ko | -21.98% | -4.72% 0m45.23s | 1003852 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m58.27s | 1188136 ko || -0m13.04s || -184284 ko | -22.37% | -15.51% 0m10.48s | 749904 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m21.82s | 876040 ko || -0m11.33s || -126136 ko | -51.97% | -14.39% 0m10.69s | 741580 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m20.21s | 840224 ko || -0m09.52s || -98644 ko | -47.10% | -11.74% 0m21.51s | 803672 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m29.88s | 846932 ko || -0m08.36s || -43260 ko | -28.01% | -5.10% 0m11.25s | 747288 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m19.67s | 833044 ko || -0m08.42s || -85756 ko | -42.80% | -10.29% 0m10.08s | 773444 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m18.07s | 819904 ko || -0m07.99s || -46460 ko | -44.21% | -5.66% 0m38.44s | 931460 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m45.20s | 1013316 ko || -0m06.76s || -81856 ko | -14.95% | -8.07% 0m08.30s | 727596 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m14.55s | 787268 ko || -0m06.25s || -59672 ko | -42.95% | -7.57% 0m08.17s | 796076 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m13.50s | 826120 ko || -0m05.33s || -30044 ko | -39.48% | -3.63% 0m07.35s | 717660 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m12.66s | 785100 ko || -0m05.31s || -67440 ko | -41.94% | -8.58% 0m06.84s | 697892 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m11.49s | 723484 ko || -0m04.65s || -25592 ko | -40.46% | -3.53% 1m38.20s | 1728408 ko | ToTemplate/Coq/MSets.vo | 1m41.31s | 1939012 ko || -0m03.10s || -210604 ko | -3.06% | -10.86% 0m04.03s | 703936 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m07.25s | 726368 ko || -0m03.21s || -22432 ko | -44.41% | -3.08% 0m04.04s | 698904 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m06.85s | 724692 ko || -0m02.80s || -25788 ko | -41.02% | -3.55% 0m03.94s | 747208 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m06.55s | 759832 ko || -0m02.60s || -12624 ko | -39.84% | -1.66% 0m02.47s | 698728 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m04.68s | 708696 ko || -0m02.20s || -9968 ko | -47.22% | -1.40% 0m03.70s | 769896 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m04.88s | 771648 ko || -0m01.17s || -1752 ko | -24.18% | -0.22% 0m02.64s | 921532 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m04.02s | 926344 ko || -0m01.37s || -4812 ko | -34.32% | -0.51% 0m02.63s | 700724 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m04.09s | 700076 ko || -0m01.46s || 648 ko | -35.69% | +0.09% 0m02.38s | 758748 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m04.17s | 759436 ko || -0m01.79s || -688 ko | -42.92% | -0.09% 0m02.04s | 701080 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m03.37s | 698344 ko || -0m01.33s || 2736 ko | -39.46% | +0.39% 0m01.94s | 701404 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m03.28s | 697440 ko || -0m01.33s || 3964 ko | -40.85% | +0.56% 0m01.69s | 700096 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m02.81s | 705736 ko || -0m01.12s || -5640 ko | -39.85% | -0.79% 1m01.47s | 1389880 ko | ToTemplate/Coq/FSets.vo | 1m01.73s | 1402124 ko || -0m00.25s || -12244 ko | -0.42% | -0.87% 0m26.12s | 1284060 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m26.92s | 1338856 ko || -0m00.80s || -54796 ko | -2.97% | -4.09% 0m20.82s | 1095908 ko | ToTemplate/Template/Typing.vo | 0m20.40s | 1099736 ko || +0m00.42s || -3828 ko | +2.05% | -0.34% 0m18.82s | 908440 ko | ToTemplate/Common/Universes.vo | 0m18.48s | 916460 ko || +0m00.33s || -8020 ko | +1.83% | -0.87% 0m15.43s | 868820 ko | ToTemplate/Common/Kernames.vo | 0m14.86s | 872484 ko || +0m00.57s || -3664 ko | +3.83% | -0.41% 0m06.58s | 998568 ko | ToTemplate/Template/TermEquality.vo | 0m07.01s | 1005820 ko || -0m00.42s || -7252 ko | -6.13% | -0.72% 0m06.30s | 995716 ko | ToTemplate/Template/WfAst.vo | 0m06.50s | 1002992 ko || -0m00.20s || -7276 ko | -3.07% | -0.72% 0m05.88s | 935032 ko | ToTemplate/Common/Environment.vo | 0m06.47s | 950944 ko || -0m00.58s || -15912 ko | -9.11% | -1.67% 0m03.62s | 699480 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m03.88s | 702452 ko || -0m00.25s || -2972 ko | -6.70% | -0.42% 0m03.10s | 711792 ko | ToTemplate/Coq/Init.vo | 0m02.70s | 705556 ko || +0m00.39s || 6236 ko | +14.81% | +0.88% 0m02.90s | 990412 ko | ToTemplate/Template/Ast.vo | 0m03.14s | 999436 ko || -0m00.24s || -9024 ko | -7.64% | -0.90% 0m02.35s | 696844 ko | ToTemplate/Init.vo | 0m02.30s | 699476 ko || +0m00.05s || -2632 ko | +2.17% | -0.37% 0m02.35s | 699696 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m03.12s | 700204 ko || -0m00.77s || -508 ko | -24.67% | -0.07% 0m02.01s | 1003068 ko | ToTemplate/All.vo | 0m01.89s | 1010272 ko || +0m00.11s || -7204 ko | +6.34% | -0.71% 0m01.96s | 696624 ko | ToTemplate/Utils/All_Forall.vo | 0m01.91s | 696852 ko || +0m00.05s || -228 ko | +2.61% | -0.03% 0m01.89s | 757188 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m02.02s | 756856 ko || -0m00.13s || 332 ko | -6.43% | +0.04% 0m01.84s | 705696 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m02.58s | 710328 ko || -0m00.74s || -4632 ko | -28.68% | -0.65% 0m01.76s | 697100 ko | CommonUtils.vo | 0m01.36s | 697944 ko || +0m00.39s || -844 ko | +29.41% | -0.12% 0m01.62s | 700016 ko | ToTemplate/Coq/Numbers.vo | 0m01.16s | 700136 ko || +0m00.46s || -120 ko | +39.65% | -0.01% 0m01.59s | 712640 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.97s | 712756 ko || -0m00.37s || -116 ko | -19.28% | -0.01% 0m01.54s | 694776 ko | ToTemplate/Utils/MCOption.vo | 0m01.99s | 696804 ko || -0m00.44s || -2028 ko | -22.61% | -0.29% 0m01.52s | 870516 ko | ToTemplate/Common/BasicAst.vo | 0m01.60s | 877576 ko || -0m00.08s || -7060 ko | -5.00% | -0.80% 0m01.51s | 694220 ko | ToTemplate/Utils/MCReflect.vo | 0m01.51s | 694328 ko || +0m00.00s || -108 ko | +0.00% | -0.01% 0m01.50s | 960280 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.55s | 968092 ko || -0m00.05s || -7812 ko | -3.22% | -0.80% 0m01.49s | 693456 ko | ToTemplate/Utils/MCProd.vo | 0m01.50s | 694308 ko || -0m00.01s || -852 ko | -0.66% | -0.12% 0m01.46s | 985456 ko | ToTemplate/Template/AstUtils.vo | 0m01.64s | 995224 ko || -0m00.17s || -9768 ko | -10.97% | -0.98% 0m01.45s | 704060 ko | ToTemplate/Coq/Floats.vo | 0m01.01s | 703292 ko || +0m00.43s || 768 ko | +43.56% | +0.10% 0m01.36s | 697084 ko | ToTemplate/Coq/Lists.vo | 0m01.36s | 698156 ko || +0m00.00s || -1072 ko | +0.00% | -0.15% 0m01.35s | 700116 ko | ToTemplate/Utils/utils.vo | 0m01.26s | 700996 ko || +0m00.09s || -880 ko | +7.14% | -0.12% 0m01.34s | 693840 ko | ToTemplate/Coq/ssr.vo | 0m01.14s | 694884 ko || +0m00.20s || -1044 ko | +17.54% | -0.15% 0m01.33s | 694508 ko | ToTemplate/Utils/MCUtils.vo | 0m01.16s | 694536 ko || +0m00.17s || -28 ko | +14.65% | -0.00% 0m01.32s | 710140 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.40s | 711564 ko || -0m00.07s || -1424 ko | -5.71% | -0.20% 0m01.29s | 754500 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.57s | 755212 ko || -0m00.28s || -712 ko | -17.83% | -0.09% 0m01.27s | 756972 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.17s | 756196 ko || +0m00.10s || 776 ko | +8.54% | +0.10% 0m01.24s | 694592 ko | ToTemplate/Coq/Bool.vo | 0m01.43s | 695096 ko || -0m00.18s || -504 ko | -13.28% | -0.07% 0m01.20s | 746972 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.06s | 754076 ko || +0m00.13s || -7104 ko | +13.20% | -0.94% 0m01.20s | 693144 ko | ToTemplate/Utils/bytestring.vo | 0m01.53s | 698048 ko || -0m00.33s || -4904 ko | -21.56% | -0.70% 0m01.19s | 765652 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.09s | 771052 ko || +0m00.09s || -5400 ko | +9.17% | -0.70% 0m01.18s | 704780 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.70s | 707492 ko || -0m00.52s || -2712 ko | -30.58% | -0.38% 0m01.11s | 692748 ko | ToTemplate/Common/Primitive.vo | 0m01.25s | 693068 ko || -0m00.13s || -320 ko | -11.19% | -0.04% 0m01.09s | 695940 ko | ToTemplate/Coq/Strings.vo | 0m01.01s | 694968 ko || +0m00.08s || 972 ko | +7.92% | +0.13% 0m01.08s | 694044 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.16s | 693864 ko || -0m00.07s || 180 ko | -6.89% | +0.02% 0m01.03s | 701348 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.07s | 700708 ko || -0m00.04s || 640 ko | -3.73% | +0.09% 0m01.02s | 698120 ko | ToTemplate/Utils/MCList.vo | 0m01.29s | 693604 ko || -0m00.27s || 4516 ko | -20.93% | +0.65% 0m01.01s | 693148 ko | ToTemplate/Common/config.vo | 0m01.23s | 694780 ko || -0m00.21s || -1632 ko | -17.88% | -0.23% 0m01.01s | 695988 ko | ToTemplate/Utils/MCArith.vo | 0m01.19s | 693928 ko || -0m00.17s || 2060 ko | -15.12% | +0.29% 0m00.07s | 63164 ko | ToTemplate/Utils/MCEquality.vo | 0m00.04s | 63060 ko || +0m00.03s || 104 ko | +75.00% | +0.16% 0m00.07s | 63300 ko | ToTemplate/Utils/MCPred.vo | 0m00.03s | 63976 ko || +0m00.04s || -676 ko | +133.33% | -1.05% 0m00.07s | 64460 ko | ToTemplate/Utils/MCString.vo | 0m00.05s | 64348 ko || +0m00.02s || 112 ko | +40.00% | +0.17% 0m00.07s | 64916 ko | ToTemplate/Utils/monad_utils.vo | 0m00.06s | 63088 ko || +0m00.01s || 1828 ko | +16.66% | +2.89% 0m00.06s | 63864 ko | ToTemplate/Utils/LibHypsNaming.vo | 0m00.04s | 64692 ko || +0m00.01s || -828 ko | +49.99% | -1.27% 0m00.06s | 64556 ko | ToTemplate/Utils/MCCompare.vo | 0m00.06s | 64992 ko || +0m00.00s || -436 ko | +0.00% | -0.67% 0m00.06s | 62916 ko | ToTemplate/Utils/MCPrelude.vo | 0m00.07s | 63064 ko || -0m00.01s || -148 ko | -14.28% | -0.23% 0m00.06s | 64596 ko | ToTemplate/Utils/MCRelations.vo | 0m00.07s | 64120 ko || -0m00.01s || 476 ko | -14.28% | +0.74% 0m00.06s | 66120 ko | ToTemplate/Utils/wGraph.vo | 0m00.06s | 64668 ko || +0m00.00s || 1452 ko | +0.00% | +2.24% 0m00.05s | 67780 ko | ToTemplate/Common/Reflect.vo | 0m00.07s | 63112 ko || -0m00.02s || 4668 ko | -28.57% | +7.39% 0m00.05s | 64504 ko | ToTemplate/Template/LiftSubst.vo | 0m00.05s | 63644 ko || +0m00.00s || 860 ko | +0.00% | +1.35% 0m00.05s | 64312 ko | ToTemplate/Utils/ByteCompare.vo | 0m00.05s | 63780 ko || +0m00.00s || 532 ko | +0.00% | +0.83% 0m00.05s | 63592 ko | ToTemplate/Utils/ByteCompareSpec.vo | 0m00.04s | 64228 ko || +0m00.01s || -636 ko | +25.00% | -0.99% 0m00.04s | 63060 ko | ToTemplate/Common/Transform.vo | 0m00.05s | 64720 ko || -0m00.01s || -1660 ko | -20.00% | -2.56% 0m00.04s | 63428 ko | ToTemplate/Template/ReflectAst.vo | 0m00.05s | 64352 ko || -0m00.01s || -924 ko | -20.00% | -1.43% 0m00.04s | 63860 ko | ToTemplate/Utils/MCSquash.vo | 0m00.06s | 63524 ko || -0m00.01s || 336 ko | -33.33% | +0.52% 0m00.03s | 64740 ko | ToTemplate/Template/Induction.vo | 0m00.05s | 64888 ko || -0m00.02s || -148 ko | -40.00% | -0.22% 0m00.03s | 64172 ko | ToTemplate/Template/UnivSubst.vo | 0m00.02s | 63464 ko || +0m00.00s || 708 ko | +49.99% | +1.11% 0m00.03s | 63548 ko | ToTemplate/Utils/ByteCompare_opt.vo | 0m00.05s | 64136 ko || -0m00.02s || -588 ko | -40.00% | -0.91% ``` </p> </details>
1 parent bd06ca1 commit 8bd85e5

File tree

2 files changed

+86
-135
lines changed

2 files changed

+86
-135
lines changed

‎quotation/theories/CommonUtils.v‎

Lines changed: 77 additions & 128 deletions
Original file line numberDiff line numberDiff line change
@@ -223,71 +223,6 @@ Module WithTemplate.
223223
end.
224224
End with_monad.
225225

226-
#[local] Definition CacheT T : Type := term * list term * UniverseMap.t term -> T * (term * list term * UniverseMap.t term).
227-
#[local] Instance CacheT_Monad : Monad CacheT
228-
:= {| ret A v := fun st => (v, st)
229-
; bind A B v f := fun st => let '(v, st) := v st in f v st |}.
230-
#[local] Definition init_cache_and_run (lProp_t lSProp_t lSet_t : term) (default_univ : term) (available_univs : list term) {T} : CacheT T -> T
231-
:= fun f
232-
=> fst
233-
(f (default_univ,
234-
available_univs,
235-
UniverseMap.add
236-
Universe.lProp lProp_t
237-
(UniverseMap.add
238-
Universe.lSProp lSProp_t
239-
(UniverseMap.add
240-
(Universe.of_levels (inr Level.lzero)) lSet_t
241-
(UniverseMap.empty _))))).
242-
#[local] Definition lookupU (u : Universe.t) : CacheT term
243-
:= fun '((default_univ, fresh_univs, map) as st)
244-
=> match UniverseMap.find u map, fresh_univs with
245-
| Some t, _ => (t, st)
246-
| None, nil => (default_univ, st)
247-
| None, t :: fresh_univs
248-
=> (t, (default_univ, fresh_univs, UniverseMap.add u t map))
249-
end.
250-
251-
#[local]
252-
Definition tmRelaxSortsCached (in_domain : bool) (do_replace_U : Universe.t -> bool) (lProp_t lSProp_t lSet_t : term) (default_univ : term) (available_univs : list term) (t : term) : term
253-
:= init_cache_and_run
254-
lProp_t lSProp_t lSet_t default_univ available_univs
255-
(tmRelaxSortsM
256-
in_domain
257-
(fun u => if do_replace_U u
258-
then lookupU u
259-
else ret (tSort u))
260-
t).
261-
262-
Polymorphic Inductive list_of_types@{u} : Type@{u+1} := nil | cons (x : Type@{u}) (xs : list_of_types).
263-
Declare Scope list_of_types_scope.
264-
Delimit Scope list_of_types_scope with list_of_types.
265-
Bind Scope list_of_types_scope with list_of_types.
266-
267-
Infix "::" := cons : list_of_types_scope.
268-
Notation "[ ]" := nil : list_of_types_scope.
269-
Notation "[ x ]" := (cons x nil) : list_of_types_scope.
270-
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_of_types_scope.
271-
272-
Polymorphic Definition types_monad_map@{l b a t u} {T} {M : Monad@{t u} T} {B : Type@{b}} (f : Type@{a} -> T B)
273-
:= fix types_monad_map (l : list_of_types@{l}) : T (list B)
274-
:= match l with
275-
| []%list_of_types => ret []%list
276-
| (x :: xs)%list_of_types
277-
=> fx <- f x;;
278-
fxs <- types_monad_map xs;;
279-
ret (fx :: fxs)%list
280-
end.
281-
282-
#[local] Polymorphic Definition tmRelaxSortsQuote@{uP uSP uS uD uL t u _high} (in_domain : bool) (do_replace_U : Universe.t -> bool) (available_univs : list_of_types@{uL}) (t : term) : TemplateMonad@{t u} term
283-
:= lProp_t <- @tmQuote Type@{_high} Type@{uP};;
284-
lSProp_t <- @tmQuote Type@{_high} Type@{uSP};;
285-
lSet_t <- @tmQuote Type@{_high} Type@{uS};;
286-
default_univ <- @tmQuote Type@{_high} Type@{uD};;
287-
available_univs <- types_monad_map@{uL _high _ _ _} tmQuote available_univs;;
288-
ret (tmRelaxSortsCached in_domain do_replace_U lProp_t lSProp_t lSet_t default_univ available_univs t).
289-
290-
291226
#[local] Definition is_set (s : Universe.t) : bool
292227
:= match option_map Level.is_set (Universe.get_is_level s) with
293228
| Some true => true
@@ -306,77 +241,91 @@ Module WithTemplate.
306241
| _ => false
307242
end.
308243

309-
Polymorphic Definition tmRetypeMagicRelaxSetInCodomain@{U a b t u _high} {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
244+
Definition tmRelaxSet (in_domain : bool) (prefix : string) (t : term) : term
245+
:= tmRelaxSortsM
246+
(M:=fun T => T) in_domain
247+
(fun u => tSort (if is_set u then Universe.of_levels (inr (Level.Level (prefix ++ "._Set.0")%bs)) else u))
248+
t.
249+
250+
Module Import PrefixUniverse.
251+
Module Level.
252+
Definition prefix_with (prefix : string) (l : Level.t) : Level.t
253+
:= match l with
254+
| Level.lzero | Level.Var _ => l
255+
| Level.Level u => Level.Level (prefix ++ "." ++ u)%bs
256+
end.
257+
End Level.
258+
259+
Module LevelExprSet.
260+
Module Raw.
261+
Definition prefix_with (prefix : string) (l : LevelExprSet.Raw.t) : LevelExprSet.Raw.t
262+
:= List.map (fun '(l, n) => (Level.prefix_with prefix l, n)) l.
263+
End Raw.
264+
Lemma prefix_with_Ok {prefix : string} {l : LevelExprSet.Raw.t} (pf : LevelExprSet.Raw.Ok l) : LevelExprSet.Raw.Ok (Raw.prefix_with prefix l).
265+
Proof.
266+
hnf in *; cbv [Raw.prefix_with] in *; cbn in *.
267+
induction l as [|[l n] ls IH]; cbn in *; [ reflexivity | ].
268+
apply Bool.andb_true_iff in pf; destruct pf as [pf1 pf2].
269+
rewrite IH, Bool.andb_true_r by assumption.
270+
clear IH pf2.
271+
destruct ls as [|[l' n'] ls]; cbn in *; [ reflexivity | ].
272+
destruct l, l'; cbn in *; try assumption.
273+
induction prefix as [|?? IH];
274+
cbn in *; try assumption.
275+
rewrite ByteCompareSpec.compare_eq_refl; assumption.
276+
Qed.
277+
Definition prefix_with (prefix : string) (l : LevelExprSet.t) : LevelExprSet.t
278+
:= @LevelExprSet.Mkt (Raw.prefix_with prefix (@LevelExprSet.this l)) (prefix_with_Ok (@LevelExprSet.is_ok l)).
279+
Lemma is_empty_prefix_with {prefix} {l} : LevelExprSet.is_empty (prefix_with prefix l) = LevelExprSet.is_empty l.
280+
Proof.
281+
destruct l as [l pf]; cbn.
282+
cbv [LevelExprSet.is_empty prefix_with LevelExprSet.Raw.is_empty]; cbn.
283+
destruct l; cbn; reflexivity.
284+
Qed.
285+
End LevelExprSet.
286+
287+
Module nonEmptyLevelExprSet.
288+
Definition prefix_with (prefix : string) (l : nonEmptyLevelExprSet) : nonEmptyLevelExprSet
289+
:= {| t_set := LevelExprSet.prefix_with prefix l.(t_set)
290+
; t_ne := eq_trans LevelExprSet.is_empty_prefix_with l.(t_ne) |}.
291+
End nonEmptyLevelExprSet.
292+
293+
Module LevelAlgExpr := nonEmptyLevelExprSet.
294+
295+
Module Universe.
296+
Definition prefix_with (prefix : string) (u : Universe.t) : Universe.t
297+
:= match u with
298+
| Universe.lProp | Universe.lSProp => u
299+
| Universe.lType u => Universe.lType (LevelAlgExpr.prefix_with prefix u)
300+
end.
301+
End Universe.
302+
End PrefixUniverse.
303+
304+
Definition tmRelaxOnlyType (in_domain : bool) (prefix : string) (t : term) : term
305+
:= tmRelaxSortsM
306+
(M:=fun T => T) in_domain
307+
(fun u => tSort (PrefixUniverse.Universe.prefix_with prefix u))
308+
t.
309+
310+
Polymorphic Definition tmRetypeMagicRelaxSetInCodomain@{a b t u} (prefix : string) {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
310311
:= qx <- tmQuote x;;
311-
qx <- tmRelaxSortsQuote@{U U U U _high t u _high} false is_set [] qx;;
312+
let qx := tmRelaxSet false prefix qx in
312313
tmUnquoteTyped B qx.
313-
Polymorphic Definition tmRetypeRelaxSetInCodomain@{U a t u _high} {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
314-
:= tmRetypeMagicRelaxSetInCodomain@{U a a t u _high} A x.
314+
Polymorphic Definition tmRetypeRelaxSetInCodomain@{a t u} (prefix : string) {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
315+
:= tmRetypeMagicRelaxSetInCodomain@{a a t u} prefix A x.
315316

316-
Local Notation many_Types_2 tail := (Type :: Type :: Type :: Type :: tail)%list_of_types (only parsing).
317-
Local Notation many_Types_3 tail := (many_Types_2 (many_Types_2 tail)) (only parsing).
318-
Local Notation many_Types_4 tail := (many_Types_3 (many_Types_3 tail)) (only parsing).
319-
Local Notation many_Types_5 tail := (many_Types_4 (many_Types_4 tail)) (only parsing).
320-
Local Notation many_Types := (many_Types_5 nil) (only parsing).
321-
322-
Polymorphic Definition tmRetypeMagicRelaxOnlyType0@{U a b t u _high} {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
317+
Polymorphic Definition tmRetypeMagicRelaxOnlyType@{a b t u} (prefix : string) {A : Type@{a}} (B : Type@{b}) (x : A) : TemplateMonad@{t u} B
323318
:= qx <- tmQuote x;;
324-
qx <- tmRelaxSortsQuote@{U U U U _high t u _high} true is_only_type [] qx;;
319+
let qx := tmRelaxOnlyType true prefix qx in
325320
tmUnquoteTyped B qx.
326-
Polymorphic Definition tmRetypeRelaxOnlyType0@{U a t u _high} {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
327-
:= tmRetypeMagicRelaxOnlyType0@{U a a t u _high} A x.
328-
329-
Polymorphic Definition tmRetypeMagicRelaxOnlyType {A : Type} (B : Type) (x : A) : TemplateMonad B
330-
:= qx <- tmQuote x;;
331-
qx <- tmRelaxSortsQuote true is_only_type many_Types qx;;
332-
tmUnquoteTyped B qx.
333-
Polymorphic Definition tmRetypeRelaxOnlyType {A} (x : A) : TemplateMonad A
334-
:= tmRetypeMagicRelaxOnlyType A x.
321+
Polymorphic Definition tmRetypeRelaxOnlyType@{a t u} (prefix : string) {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
322+
:= tmRetypeMagicRelaxOnlyType@{a a t u} prefix A x.
335323

336324
(* Hack around https://github.com/MetaCoq/metacoq/issues/853 *)
337-
Polymorphic Definition tmRetypeAroundMetaCoqBug853_0 (t : typed_term) : TemplateMonad typed_term
338-
:= let '{| my_projT1 := ty ; my_projT2 := v |} := t in
339-
ty <- tmRetypeRelaxOnlyType0 ty;;
340-
v <- tmRetypeMagicRelaxOnlyType0 ty v;;
341-
ret {| my_projT1 := ty ; my_projT2 := v |}.
342-
343-
Polymorphic Definition tmRetypeAroundMetaCoqBug853_gen (t : typed_term) : TemplateMonad typed_term
325+
Definition tmRetypeAroundMetaCoqBug853 (prefix : string) (t : typed_term) : TemplateMonad typed_term
344326
:= let '{| my_projT1 := ty ; my_projT2 := v |} := t in
345-
ty <- tmRetypeRelaxOnlyType ty;;
346-
v <- tmRetypeMagicRelaxOnlyType ty v;;
327+
ty <- tmRetypeRelaxOnlyType prefix ty;;
328+
v <- tmRetypeMagicRelaxOnlyType prefix ty v;;
347329
ret {| my_projT1 := ty ; my_projT2 := v |}.
348-
349-
(* Hack around https://github.com/MetaCoq/metacoq/pull/876#issuecomment-1487743822 *)
350-
Monomorphic Variant exn : Set := GenericError.
351-
352-
Polymorphic Variant option_try@{u} (A : Type@{u}) : Type@{max(Set, u)} := my_Value (val : A) | my_Error (err : exn).
353-
354-
Arguments my_Value {A} val.
355-
Arguments my_Error {A} _.
356-
Polymorphic Class tmCheckSuccessHelper@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) := tmCheckSuccess_ret : unit.
357-
#[global] Hint Extern 0 (tmCheckSuccessHelper ?run) => run_template_program run (fun v => exact tt) : typeclass_instances.
358-
Polymorphic Definition tmCheckSuccess@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) : TemplateMonad@{t u} bool
359-
:= tmBind (tmInferInstance None (tmCheckSuccessHelper run))
360-
(fun inst => match inst with
361-
| my_Some _ => tmReturn true
362-
| my_None => tmReturn false
363-
end).
364-
Polymorphic Definition tmTryWorseButNoAnomaly@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) : TemplateMonad@{t u} (option_try@{t} A)
365-
:= succeeds <- tmCheckSuccess run;;
366-
if succeeds:bool
367-
then v <- run;; ret (my_Value v)
368-
else ret (my_Error GenericError).
369-
370-
Definition tmRetypeAroundMetaCoqBug853 (t : typed_term) : TemplateMonad typed_term
371-
:= Eval cbv [List.fold_right] in
372-
List.fold_right
373-
(fun tmRetype acc
374-
=> res <- tmTryWorseButNoAnomaly (tmRetype t);;
375-
match res with
376-
| my_Value v => ret v
377-
| my_Error _ => acc
378-
end)
379-
(tmRetypeAroundMetaCoqBug853_gen t)
380-
[tmRetypeAroundMetaCoqBug853_0; tmRetypeAroundMetaCoqBug853_gen].
381330
End WithTemplate.
382331
Export WithTemplate (transparentify, tmQuoteToGlobalReference, tmRetypeRelaxSetInCodomain, tmRetypeRelaxOnlyType, tmRetypeMagicRelaxSetInCodomain, tmRetypeMagicRelaxOnlyType, tmObj_magic, tmRetype, tmExtractBaseModPathFromMod, tmRetypeAroundMetaCoqBug853).

‎quotation/theories/ToTemplate/Init.v‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -424,7 +424,9 @@ Ltac unfold_quotation_of _ :=
424424
| change (@quotation_of A (transparentify t)) ]
425425
end.
426426

427-
Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} {debug:debug_opt} (work_aronud_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (base : modpath) (cs : list global_reference) : TemplateMonad@{t u} (list (string * typed_term@{u'}))
427+
(* for universe adjustment with [tmDeclareQuotationOfModule], [tmMakeQuotationOfModule] *)
428+
#[export] Unset MetaCoq Strict Unquote Universe Mode.
429+
Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} {debug:debug_opt} (work_around_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (base : modpath) (cs : list global_reference) : TemplateMonad@{t u} (list (string * typed_term@{u'}))
428430
:= let warn_bad_ctx c ctx :=
429431
(_ <- tmMsg "tmPrepareMakeQuotationOfModule: cannot handle polymorphism";;
430432
_ <- tmPrint c;;
@@ -442,7 +444,7 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
442444
_ <- tmDebugPrint r;;
443445
tmReturn []) in
444446
let make_qname '(mp, name)
445-
(* ideally we'd replace _ with __ so that there can't be any collision, but the utility functions aren't written and we don't need it in practice *)
447+
(* ideally we'd replace _ with __ so that there can't be any collision, but the utility functions aren't written and we don't need it in practice *)
446448
:= option_map
447449
(fun n => "q" ++ n)%bs
448450
match split_common_prefix base mp with
@@ -488,7 +490,7 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
488490
_ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote";;
489491
'{| my_projT1 := cty ; my_projT2 := cv |} <- tmUnquote c;;
490492
_ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote done";;
491-
tmReturn [(qname, if work_aronud_coq_bug_17303
493+
tmReturn [(qname, if work_around_coq_bug_17303
492494
then {| my_projT1 := term ; my_projT2 := c |}
493495
else {| my_projT1 := @quotation_of cty cv ; my_projT2 := c |})]
494496
end
@@ -507,7 +509,7 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
507509
_ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote";;
508510
'{| my_projT1 := cty ; my_projT2 := cv |} <- tmUnquote c;;
509511
_ <- tmDebugMsg "tmPrepareMakeQuotationOfConstants: tmUnquote done";;
510-
let tmcty := tmRetypeRelaxSetInCodomain@{U t t u _above_u} cty in
512+
let tmcty := tmRetypeRelaxSetInCodomain@{t t u} qname cty in
511513
_ <- tmDebugPrint tmcty;;
512514
cty <- tmcty;;
513515
let tmcv := tmObj_magic (B:=cty) cv in
@@ -524,19 +526,19 @@ Polymorphic Definition tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _
524526
ret ps.
525527

526528
(* N.B. We need to kludge around COQBUG(https://github.com/coq/coq/issues/17303) in Kernames :-( *)
527-
Polymorphic Definition tmMakeQuotationOfConstants_gen@{U d t u u' _T _above_u _above_u' _above_gr} {debug:debug_opt} (work_aronud_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (existing_instance : option hint_locality) (base : modpath) (cs : list global_reference) (tmDoWithDefinition : ident -> forall A : Type@{d}, A -> TemplateMonad A) : TemplateMonad unit
529+
Polymorphic Definition tmMakeQuotationOfConstants_gen@{U d t u u' _T _above_u _above_u' _above_gr} {debug:debug_opt} (work_around_coq_bug_17303 : bool) (include_submodule : list ident -> bool) (include_supermodule : list ident -> list ident -> bool) (existing_instance : option hint_locality) (base : modpath) (cs : list global_reference) (tmDoWithDefinition : ident -> forall A : Type@{d}, A -> TemplateMonad A) : TemplateMonad unit
528530
:= let tmDebugMsg s := (if debug
529531
then tmMsg s
530532
else tmReturn tt) in
531533
let tmDebugPrint {T : Type@{_T}} (v : T)
532534
:= (if debug
533535
then tmPrint v
534536
else tmReturn tt) in
535-
ps <- tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} work_aronud_coq_bug_17303 include_submodule include_supermodule base cs;;
537+
ps <- tmPrepareMakeQuotationOfConstants@{U t u u' _T _above_u _above_u'} work_around_coq_bug_17303 include_submodule include_supermodule base cs;;
536538
_ <- tmDebugMsg "tmMakeQuotationOfConstants_gen: defining module constants";;
537539
ps <- monad_map@{_ _ _above_gr _above_u'}
538540
(fun '(name, tyv)
539-
=> let tmTyv := tmRetypeAroundMetaCoqBug853 tyv in
541+
=> let tmTyv := tmRetypeAroundMetaCoqBug853 name tyv in
540542
_ <- tmDebugPrint tmTyv;;
541543
'{| my_projT1 := ty ; my_projT2 := v |} <- tmTyv;;
542544
tmDef_name <- tmEval cbv (@tmDoWithDefinition (name:string));;

0 commit comments

Comments
 (0)