Fix translations

Author: yannl35133

common/theories/Universes.v

@@ -1486,6 +1486,13 @@ Module Sort.
 
   #[global] Instance eq_dec_sort {univ} `{EqDec univ} : EqDec (t_ univ) := ltac:(intros s s'; decide equality).
 
+  Definition map {u u'} (f : u -> u') s :=
+    match s with
+    | sType u => sType (f u)
+    | sProp => sProp
+    | sSProp => sSProp
+    end.
+
   Definition on_sort {univ} {T} (P: univ -> T) (def: T) (s : t_ univ) :=
     match s with
     | sProp | sSProp => def

examples/demo.v

@@ -374,10 +374,10 @@ Inductive T : Type :=
 MetaCoq Quote Recursively Definition TT := T.
 
 Unset MetaCoq Strict Unquote Universe Mode.
-MetaCoq Unquote Definition t := (tSort (Universe.make (Level.level "Top.20000"))).
-MetaCoq Unquote Definition t' := (tSort fresh_universe).
-MetaCoq Unquote Definition myProp := (tSort (Universe.lProp)).
-MetaCoq Unquote Definition mySet := (tSort (Universe.make Level.lzero)).
+MetaCoq Unquote Definition t := (tSort (sType (Universe.make' (Level.level "Top.20000")))).
+MetaCoq Unquote Definition t' := (tSort (sType fresh_universe)).
+MetaCoq Unquote Definition myProp := (tSort sProp).
+MetaCoq Unquote Definition mySet := (tSort (sType (Universe.make' Level.lzero))).
 
 (** Cofixpoints *)
 CoInductive streamn : Set :=

examples/typing_correctness.v

@@ -145,9 +145,9 @@ Ltac fill_inh t :=
   | [ |- inh _ ?Γ _ ] => fail "Missing local wellformedness assumption for" Γ
   end.
 
-(* Lemma identity_typing (u := Universe.make univ): inh gctx_wf_env [] (tImpl (tSort u) (tSort u)).
+(* Lemma identity_typing (s := sType (Universe.make' univ)): inh gctx_wf_env [] (tImpl (tSort s) (tSort s)).
 Proof.
-  set (impl := tLambda (bNamed "s") (tSort u) (tRel 0)).
+  set (impl := tLambda (bNamed "s") (tSort s) (tRel 0)).
   assert (wfΓ : forall Σ0 : global_env_ext,
   abstract_env_ext_rel gctx_wf_env Σ0 -> ∥ wf_local Σ0 [] ∥) by do 2 constructor.
 
@@ -156,7 +156,7 @@ Proof.
 Time Qed. *)
 
 
-Lemma identity_typing (u := Universe.make univ):
+Lemma identity_typing (s := sType (Universe.make' univ)):
      (∑ t : term,
         forall Σ0 : global_env_ext,
         Σ0 =
@@ -168,13 +168,13 @@ Lemma identity_typing (u := Universe.make univ):
            retroknowledge := Retroknowledge.empty
          |}, Monomorphic_ctx) ->
         ∥ Σ0;;; [] |- t
-          : tProd (bNamed "s") (tSort u) (tImpl (tRel 0) (tRel 0)) ∥).
+          : tProd (bNamed "s") (tSort s) (tImpl (tRel 0) (tRel 0)) ∥).
 (* inh gctx_wf_env [] (tProd (bNamed "s") (tSort u) (tImpl (tRel 0) (tRel 0))). *)
 Proof.
-  set (impl := tLambda (bNamed "s") (tSort u) (tLambda bAnon (tRel 0) (tRel 0))).
+  set (impl := tLambda (bNamed "s") (tSort s) (tLambda bAnon (tRel 0) (tRel 0))).
   assert (wfΓ : forall Σ0 : global_env_ext,
   abstract_env_ext_rel gctx_wf_env Σ0 -> ∥ wf_local Σ0 [] ∥) by do 2 constructor.
-  pose (T := tProd (bNamed "s") (tSort u) (tImpl (tRel 0) (tRel 0))).
+  pose (T := tProd (bNamed "s") (tSort s) (tImpl (tRel 0) (tRel 0))).
   pose (Σ := gctx_wf_env).
   let t := uconstr:(check_inh Σ [] wfΓ impl (T:=T)) in
   let proof := eval hnf in t in

test-suite/castprop.v

@@ -18,4 +18,4 @@ Definition setprop : { x : nat | x = 0 } := exist _ 0 eq_refl.
 MetaCoq Quote Recursively Definition q_setprop := setprop.
 
 Notation proof t :=
-  (Ast.tCast t BasicAst.Cast (Ast.tCast _ BasicAst.Cast (Ast.tSort ((Universes.Universe.lProp :: nil)%list; _)))).
+  (Ast.tCast t BasicAst.Cast (Ast.tCast _ BasicAst.Cast (Ast.tSort ((Universes.sProp :: nil)%list; _)))).

test-suite/inferind.v

@@ -12,12 +12,7 @@ Definition qlist := Eval compute in match <% list %> with
 
 Definition refresh_sort t :=
   match t with
-  | tSort s =>
-      match s with
-      | Universe.lProp => tSort Universe.lProp
-      | Universe.lSProp => tSort Universe.lSProp
-      | Universe.lType _ => tSort Universes.fresh_universe
-      end
+  | tSort s => tSort (Sort.map (fun _ => fresh_universe) s)
   | _ => t
   end.
 

test-suite/tmFix.v

@@ -71,12 +71,18 @@ Module Unquote.
   Local Unset Universe Minimization ToSet.
   (* idk why this is needed... *)
   #[local] Hint Extern 1 (Monad _) => refine TemplateMonad_Monad : typeclass_instances.
-  Definition tmQuoteUniverse@{U t u} : TemplateMonad@{t u} sort
-    := u <- @tmQuote Prop (Type@{U} -> True);;
-       match u with
-       | tProd _ (tSort u) _ => ret u
-       | _ => tmFail "Anomaly: tmQuote (Type -> True) should be (tProd _ (tSort _) _)!"%bs
-       end.
+  Definition tmQuoteSort@{U t u} : TemplateMonad@{t u} sort
+    := p <- @tmQuote Prop (Type@{U} -> True);;
+      match p with
+      | tProd _ (tSort s) _ => ret s
+      | _ => tmFail "Anomaly: tmQuote (Type -> True) should be (tProd _ (tSort _) _)!"%bs
+      end.
+  Definition tmQuoteUniverse@{U t u} : TemplateMonad@{t u} Universe.t
+    := s <- @tmQuoteSort@{U t u};;
+      match s with
+      | sType u => ret u
+      | _ => tmFail "Sort does not carry a universe (is not Type)"%bs
+      end.
   Definition tmQuoteLevel@{U t u} : TemplateMonad@{t u} Level.t
     := u <- tmQuoteUniverse@{U t u};;
        match Universe.get_is_level u with

test-suite/univ.v

@@ -17,7 +17,7 @@ MetaCoq Quote Definition a_random_univ := Type.
 
 Example a_random_univ_ex :
   exists l, a_random_univ =
-            tSort (Universe.from_kernel_repr (Level.level l, false) []).
+            tSort (sType (Universe.make' (Level.level l))).
 Proof. eexists. reflexivity. Qed.
 
 (* Back and forth *)
@@ -30,18 +30,18 @@ Check eq_refl : univ_foo = univ_foo_back.
 
 Print univ_foo_back.
 
-Fail MetaCoq Unquote Definition t1 := (tSort (Universe.make (Level.level "Top.400"))).
+Fail MetaCoq Unquote Definition t1 := (tSort (sType (Universe.make' (Level.level "Top.400")))).
 (* Fails with "Level Top.<something> not a declared level and you are in Strict Unquote Universe Mode." *)
 
 Unset MetaCoq Strict Unquote Universe Mode.
-MetaCoq Unquote Definition t2 := (tSort fresh_universe).
-MetaCoq Unquote Definition t3 := (tSort (Universe.make (Level.level "Top.400"))).
+MetaCoq Unquote Definition t2 := (tSort (sType fresh_universe)).
+MetaCoq Unquote Definition t3 := (tSort (sType (Universe.make' (Level.level "Top.400")))).
 
 Monomorphic Universe i j.
 
 Set MetaCoq Strict Unquote Universe Mode.
 MetaCoq Test Quote (Type@{j} -> Type@{i}).
-MetaCoq Unquote Definition T'' := (tSort (Universe.make (Level.level "j"))).
+MetaCoq Unquote Definition T'' := (tSort (sType (Universe.make' (Level.level "j")))).
 Unset MetaCoq Strict Unquote Universe Mode.
 
 
@@ -196,7 +196,7 @@ Definition nNamedR (s : string) := mkBindAnn (nNamed s) Relevant.
 Definition nAnonR := mkBindAnn nAnon Relevant.
 
 Unset MetaCoq Strict Unquote Universe Mode.
-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)))).
+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)))).
 
 Set Printing Universes.
 Print bla.

translations/param_cheap_packed.v

@@ -8,9 +8,14 @@ Local Existing Instance config.default_checker_flags.
 Local Existing Instance default_fuel.
 
 
+Definition refresh_universe u :=
+  if Universe.is_level u then u else fresh_universe.
+
+Definition refresh_sort_universe := Sort.map refresh_universe.
+
 Fixpoint refresh_universes (t : term) {struct t} :=
   match t with
-  | tSort s => tSort (if Universe.is_level s then s else fresh_universe)
+  | tSort s => tSort (refresh_sort_universe s)
   | tProd na b t => tProd na b (refresh_universes t)
   | tLetIn na b t' t => tLetIn na b t' (refresh_universes t)
   | _ => t

translations/param_generous_packed.v

@@ -28,10 +28,14 @@ Definition proj2 (t : term) : term
 Definition proj (b : bool) (t : term) : term
   := tProj (mkProjection sigma_ind 2 (if b then 0 else S 0)) t.
 
+Definition refresh_universe u :=
+  if Universe.is_level u then u else fresh_universe.
+
+Definition refresh_sort_universe := Sort.map refresh_universe.
 
 Fixpoint refresh_universes (t : term) {struct t} :=
   match t with
-  | tSort s => tSort (if Universe.is_level s then s else fresh_universe)
+  | tSort s => tSort (refresh_sort_universe s)
   | tProd na b t => tProd na b (refresh_universes t)
   | tLetIn na b t' t => tLetIn na b t' (refresh_universes t)
   | _ => t
@@ -108,8 +112,8 @@ with tsl_term  (fuel : nat) (Σ : global_env_ext) (E : tsl_table) (Γ : context)
   | tRel n => ret (tRel n)
 
   | tSort s =>
-    ret (pair (tSort fresh_universe)
-              (tLambda (nNamed "A") (tSort fresh_universe) (tProd nAnon (tRel 0) (tSort fresh_universe)))
+    ret (pair (tSort (sType fresh_universe))
+              (tLambda (nNamed "A") (tSort (sType fresh_universe)) (tProd nAnon (tRel 0) (tSort (sType fresh_universe))))
               (tSort s)
               (tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))))
 

translations/times_bool_fun.v

@@ -207,10 +207,14 @@ Definition tsl_mind_body (ΣE : tsl_context) (mp : modpath) (kn : kername)
     exact (fun A Γ' => Γ' ,, vass (decl_name A) (tsl Γ' (decl_type A))).
 Defined.
 
+Definition refresh_universe u :=
+  if Universe.is_level u then u else fresh_universe.
+
+Definition refresh_sort_universe := Sort.map refresh_universe.
 
 Fixpoint refresh_universes (t : term) {struct t} :=
   match t with
-  | tSort s => tSort (if Universe.is_level s then s else fresh_universe)
+  | tSort s => tSort (refresh_sort_universe s)
   | tProd na b t => tProd na b (refresh_universes t)
   | tLetIn na b t' t => tLetIn na b t' (refresh_universes t)
   | tCast x x0 x1 => tCast (refresh_universes x) x0 (refresh_universes x1)