From 078344edd231b82b7d7e8c225fd6908fbd0ac860 Mon Sep 17 00:00:00 2001 From: Yann Leray Date: Sat, 16 Dec 2023 20:17:34 +0100 Subject: [PATCH] Fix translations --- common/theories/Universes.v | 7 +++++++ examples/demo.v | 8 ++++---- examples/typing_correctness.v | 12 ++++++------ test-suite/castprop.v | 2 +- test-suite/inferind.v | 7 +------ test-suite/tmFix.v | 18 ++++++++++++------ test-suite/univ.v | 12 ++++++------ translations/param_cheap_packed.v | 7 ++++++- translations/param_generous_packed.v | 10 +++++++--- translations/times_bool_fun.v | 6 +++++- 10 files changed, 55 insertions(+), 34 deletions(-) diff --git a/common/theories/Universes.v b/common/theories/Universes.v index 615cb5e05..eca654b27 100644 --- a/common/theories/Universes.v +++ b/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 diff --git a/examples/demo.v b/examples/demo.v index ff1349c19..0b6e0ddf1 100644 --- a/examples/demo.v +++ b/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 := diff --git a/examples/typing_correctness.v b/examples/typing_correctness.v index 52db52d6b..5637dd0a8 100644 --- a/examples/typing_correctness.v +++ b/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 diff --git a/test-suite/castprop.v b/test-suite/castprop.v index f1514c150..3fc76da7a 100644 --- a/test-suite/castprop.v +++ b/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; _)))). diff --git a/test-suite/inferind.v b/test-suite/inferind.v index db164e740..c45953788 100644 --- a/test-suite/inferind.v +++ b/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. diff --git a/test-suite/tmFix.v b/test-suite/tmFix.v index 85c370e11..ec702551e 100644 --- a/test-suite/tmFix.v +++ b/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 diff --git a/test-suite/univ.v b/test-suite/univ.v index ced8b4b93..bb1d830a8 100644 --- a/test-suite/univ.v +++ b/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. 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. diff --git a/translations/param_cheap_packed.v b/translations/param_cheap_packed.v index 7f5254513..79c1e4ad2 100644 --- a/translations/param_cheap_packed.v +++ b/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 diff --git a/translations/param_generous_packed.v b/translations/param_generous_packed.v index c8211e2b7..281844476 100644 --- a/translations/param_generous_packed.v +++ b/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)))) diff --git a/translations/times_bool_fun.v b/translations/times_bool_fun.v index ee85d7df2..41ae75cbe 100644 --- a/translations/times_bool_fun.v +++ b/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)