Skip to content

Commit 70a621a

Browse files
yannl35133yannl35133
committed
Fix translations
1 parent 3a488f5 commit 70a621a

File tree

9 files changed

+49
-28
lines changed

9 files changed

+49
-28
lines changed

‎common/theories/Universes.v

+7
Original file line numberDiff line numberDiff line change
@@ -1486,6 +1486,13 @@ Module Sort.
14861486

14871487
#[global] Instance eq_dec_sort {univ} `{EqDec univ} : EqDec (t_ univ) := ltac:(intros s s'; decide equality).
14881488

1489+
Definition map {u u'} (f : u -> u') s :=
1490+
match s with
1491+
| sType u => sType (f u)
1492+
| sProp => sProp
1493+
| sSProp => sSProp
1494+
end.
1495+
14891496
Definition on_sort {univ} {T} (P: univ -> T) (def: T) (s : t_ univ) :=
14901497
match s with
14911498
| sProp | sSProp => def

‎examples/demo.v

+4-4
Original file line numberDiff line numberDiff line change
@@ -374,10 +374,10 @@ Inductive T : Type :=
374374
MetaCoq Quote Recursively Definition TT := T.
375375

376376
Unset MetaCoq Strict Unquote Universe Mode.
377-
MetaCoq Unquote Definition t := (tSort (Universe.make (Level.level "Top.20000"))).
378-
MetaCoq Unquote Definition t' := (tSort fresh_universe).
379-
MetaCoq Unquote Definition myProp := (tSort (Universe.lProp)).
380-
MetaCoq Unquote Definition mySet := (tSort (Universe.make Level.lzero)).
377+
MetaCoq Unquote Definition t := (tSort (sType (Universe.make' (Level.level "Top.20000")))).
378+
MetaCoq Unquote Definition t' := (tSort (sType fresh_universe)).
379+
MetaCoq Unquote Definition myProp := (tSort sProp).
380+
MetaCoq Unquote Definition mySet := (tSort (sType (Universe.make' Level.lzero))).
381381

382382
(** Cofixpoints *)
383383
CoInductive streamn : Set :=

‎test-suite/castprop.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,4 +18,4 @@ Definition setprop : { x : nat | x = 0 } := exist _ 0 eq_refl.
1818
MetaCoq Quote Recursively Definition q_setprop := setprop.
1919

2020
Notation proof t :=
21-
(Ast.tCast t BasicAst.Cast (Ast.tCast _ BasicAst.Cast (Ast.tSort ((Universes.Universe.lProp :: nil)%list; _)))).
21+
(Ast.tCast t BasicAst.Cast (Ast.tCast _ BasicAst.Cast (Ast.tSort ((Universes.sProp :: nil)%list; _)))).

‎test-suite/inferind.v

+1-6
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,7 @@ Definition qlist := Eval compute in match <% list %> with
1212

1313
Definition refresh_sort t :=
1414
match t with
15-
| tSort s =>
16-
match s with
17-
| Universe.lProp => tSort Universe.lProp
18-
| Universe.lSProp => tSort Universe.lSProp
19-
| Universe.lType _ => tSort Universes.fresh_universe
20-
end
15+
| tSort s => tSort (Sort.map (fun _ => fresh_universe) s)
2116
| _ => t
2217
end.
2318

‎test-suite/tmFix.v

+12-6
Original file line numberDiff line numberDiff line change
@@ -71,12 +71,18 @@ Module Unquote.
7171
Local Unset Universe Minimization ToSet.
7272
(* idk why this is needed... *)
7373
#[local] Hint Extern 1 (Monad _) => refine TemplateMonad_Monad : typeclass_instances.
74-
Definition tmQuoteUniverse@{U t u} : TemplateMonad@{t u} sort
75-
:= u <- @tmQuote Prop (Type@{U} -> True);;
76-
match u with
77-
| tProd _ (tSort u) _ => ret u
78-
| _ => tmFail "Anomaly: tmQuote (Type -> True) should be (tProd _ (tSort _) _)!"%bs
79-
end.
74+
Definition tmQuoteSort@{U t u} : TemplateMonad@{t u} sort
75+
:= p <- @tmQuote Prop (Type@{U} -> True);;
76+
match p with
77+
| tProd _ (tSort s) _ => ret s
78+
| _ => tmFail "Anomaly: tmQuote (Type -> True) should be (tProd _ (tSort _) _)!"%bs
79+
end.
80+
Definition tmQuoteUniverse@{U t u} : TemplateMonad@{t u} Universe.t
81+
:= s <- @tmQuoteSort@{U t u};;
82+
match s with
83+
| sType u => ret u
84+
| _ => tmFail "Sort does not carry a universe (is not Type)"%bs
85+
end.
8086
Definition tmQuoteLevel@{U t u} : TemplateMonad@{t u} Level.t
8187
:= u <- tmQuoteUniverse@{U t u};;
8288
match Universe.get_is_level u with

‎test-suite/univ.v

+6-6
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ MetaCoq Quote Definition a_random_univ := Type.
1717

1818
Example a_random_univ_ex :
1919
exists l, a_random_univ =
20-
tSort (Universe.from_kernel_repr (Level.level l, false) []).
20+
tSort (sType (Universe.make' (Level.level l))).
2121
Proof. eexists. reflexivity. Qed.
2222

2323
(* Back and forth *)
@@ -30,18 +30,18 @@ Check eq_refl : univ_foo = univ_foo_back.
3030

3131
Print univ_foo_back.
3232

33-
Fail MetaCoq Unquote Definition t1 := (tSort (Universe.make (Level.level "Top.400"))).
33+
Fail MetaCoq Unquote Definition t1 := (tSort (sType (Universe.make' (Level.level "Top.400")))).
3434
(* Fails with "Level Top.<something> not a declared level and you are in Strict Unquote Universe Mode." *)
3535

3636
Unset MetaCoq Strict Unquote Universe Mode.
37-
MetaCoq Unquote Definition t2 := (tSort fresh_universe).
38-
MetaCoq Unquote Definition t3 := (tSort (Universe.make (Level.level "Top.400"))).
37+
MetaCoq Unquote Definition t2 := (tSort (sType fresh_universe)).
38+
MetaCoq Unquote Definition t3 := (tSort (sType (Universe.make' (Level.level "Top.400")))).
3939

4040
Monomorphic Universe i j.
4141

4242
Set MetaCoq Strict Unquote Universe Mode.
4343
MetaCoq Test Quote (Type@{j} -> Type@{i}).
44-
MetaCoq Unquote Definition T'' := (tSort (Universe.make (Level.level "j"))).
44+
MetaCoq Unquote Definition T'' := (tSort (sType (Universe.make' (Level.level "j")))).
4545
Unset MetaCoq Strict Unquote Universe Mode.
4646

4747

@@ -196,7 +196,7 @@ Definition nNamedR (s : string) := mkBindAnn (nNamed s) Relevant.
196196
Definition nAnonR := mkBindAnn nAnon Relevant.
197197

198198
Unset MetaCoq Strict Unquote Universe Mode.
199-
MetaCoq Unquote Definition bla' := (tLambda (nNamedR "T") (tSort (Universe.make (Level.level "Top.46"))) (tLambda (nNamedR "T2") (tSort (Universe.make (Level.level "Top.477"))) (tProd nAnonR (tRel 1) (tRel 1)))).
199+
MetaCoq Unquote Definition bla' := (tLambda (nNamedR "T") (tSort (sType (Universe.make' (Level.level "Top.46")))) (tLambda (nNamedR "T2") (tSort (sType (Universe.make' (Level.level "Top.477")))) (tProd nAnonR (tRel 1) (tRel 1)))).
200200

201201
Set Printing Universes.
202202
Print bla.

‎translations/param_cheap_packed.v

+6-1
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,14 @@ Local Existing Instance config.default_checker_flags.
88
Local Existing Instance default_fuel.
99

1010

11+
Definition refresh_universe u :=
12+
if Universe.is_level u then u else fresh_universe.
13+
14+
Definition refresh_sort_universe := Sort.map refresh_universe.
15+
1116
Fixpoint refresh_universes (t : term) {struct t} :=
1217
match t with
13-
| tSort s => tSort (if Universe.is_level s then s else fresh_universe)
18+
| tSort s => tSort (refresh_sort_universe s)
1419
| tProd na b t => tProd na b (refresh_universes t)
1520
| tLetIn na b t' t => tLetIn na b t' (refresh_universes t)
1621
| _ => t

‎translations/param_generous_packed.v

+7-3
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,14 @@ Definition proj2 (t : term) : term
2828
Definition proj (b : bool) (t : term) : term
2929
:= tProj (mkProjection sigma_ind 2 (if b then 0 else S 0)) t.
3030

31+
Definition refresh_universe u :=
32+
if Universe.is_level u then u else fresh_universe.
33+
34+
Definition refresh_sort_universe := Sort.map refresh_universe.
3135

3236
Fixpoint refresh_universes (t : term) {struct t} :=
3337
match t with
34-
| tSort s => tSort (if Universe.is_level s then s else fresh_universe)
38+
| tSort s => tSort (refresh_sort_universe s)
3539
| tProd na b t => tProd na b (refresh_universes t)
3640
| tLetIn na b t' t => tLetIn na b t' (refresh_universes t)
3741
| _ => t
@@ -108,8 +112,8 @@ with tsl_term (fuel : nat) (Σ : global_env_ext) (E : tsl_table) (Γ : context)
108112
| tRel n => ret (tRel n)
109113

110114
| tSort s =>
111-
ret (pair (tSort fresh_universe)
112-
(tLambda (nNamed "A") (tSort fresh_universe) (tProd nAnon (tRel 0) (tSort fresh_universe)))
115+
ret (pair (tSort (sType fresh_universe))
116+
(tLambda (nNamed "A") (tSort (sType fresh_universe)) (tProd nAnon (tRel 0) (tSort (sType fresh_universe))))
113117
(tSort s)
114118
(tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))))
115119

‎translations/times_bool_fun.v

+5-1
Original file line numberDiff line numberDiff line change
@@ -207,10 +207,14 @@ Definition tsl_mind_body (ΣE : tsl_context) (mp : modpath) (kn : kername)
207207
exact (fun A Γ' => Γ' ,, vass (decl_name A) (tsl Γ' (decl_type A))).
208208
Defined.
209209

210+
Definition refresh_universe u :=
211+
if Universe.is_level u then u else fresh_universe.
212+
213+
Definition refresh_sort_universe := Sort.map refresh_universe.
210214

211215
Fixpoint refresh_universes (t : term) {struct t} :=
212216
match t with
213-
| tSort s => tSort (if Universe.is_level s then s else fresh_universe)
217+
| tSort s => tSort (refresh_sort_universe s)
214218
| tProd na b t => tProd na b (refresh_universes t)
215219
| tLetIn na b t' t => tLetIn na b t' (refresh_universes t)
216220
| tCast x x0 x1 => tCast (refresh_universes x) x0 (refresh_universes x1)

0 commit comments

Comments
 (0)