Library MetaRocq.Examples.metarocq_tour_prelude
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import config Universes.
From MetaRocq.Template Require Import Loader.
From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping PCUICSN PCUICLiftSubst.
From MetaRocq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker.
From Equations Require Import Equations.
Import MRMonadNotation.
Global Existing Instance default_checker_flags.
Global Existing Instance default_normalizing.
Definition bAnon := {| binder_name := nAnon; binder_relevance := Relevant |}.
Definition bNamed s := {| binder_name := nNamed s; binder_relevance := Relevant |}.
Definition tImpl X Y := tProd bAnon X (lift0 1 Y).
Definition univ := Level.level "s".
Definition gctx : global_env_ext :=
({| universes := (LS.union (LevelSet.singleton Level.lzero) (LevelSet.singleton univ), ConstraintSet.empty);
declarations := []; retroknowledge := Retroknowledge.empty |}, Monomorphic_ctx).
From MetaRocq.Common Require Import config Universes.
From MetaRocq.Template Require Import Loader.
From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping PCUICSN PCUICLiftSubst.
From MetaRocq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker.
From Equations Require Import Equations.
Import MRMonadNotation.
Global Existing Instance default_checker_flags.
Global Existing Instance default_normalizing.
Definition bAnon := {| binder_name := nAnon; binder_relevance := Relevant |}.
Definition bNamed s := {| binder_name := nNamed s; binder_relevance := Relevant |}.
Definition tImpl X Y := tProd bAnon X (lift0 1 Y).
Definition univ := Level.level "s".
Definition gctx : global_env_ext :=
({| universes := (LS.union (LevelSet.singleton Level.lzero) (LevelSet.singleton univ), ConstraintSet.empty);
declarations := []; retroknowledge := Retroknowledge.empty |}, Monomorphic_ctx).
We use the environment checker to produce the proof that gctx, which is a singleton with only
universe "s" declared is well-formed.
Definition kername_of_string (s : string) : kername :=
(MPfile [], s).
Global Program Instance fake_guard_impl : abstract_guard_impl :=
{| guard_impl := fake_guard_impl |}.
Next Obligation. Admitted.
Global Existing Instance normalization. Global Instance assume_normalization : Normalization.
Admitted.
Definition make_wf_env_ext (Σ : global_env_ext) : EnvCheck wf_env_ext wf_env_ext :=
'(exist Σ' pf) <- check_wf_ext optimized_abstract_env_impl Σ ;;
ret Σ'.
Definition gctx_wf_env : wf_env_ext.
Proof.
let wf_proof := eval hnf in (make_wf_env_ext gctx) in
match wf_proof with
| CorrectDecl _ ?x ⇒ exact x
| _ ⇒ fail "Couldn't prove the global environment is well-formed"
end.
Defined.
There is always a proof of `forall x : Sort s, x -> x`
Definition inh (Σ : wf_env_ext) Γ T := (∑ t, ∀ Σ0 : global_env_ext, abstract_env_ext_rel Σ Σ0 → ∥ typing Σ0 Γ t T ∥).
Definition check_inh (Σ : wf_env_ext) Γ
(wfΓ : ∀ Σ0 : global_env_ext, abstract_env_ext_rel Σ Σ0 → ∥ wf_local Σ0 Γ ∥) t {T} : typing_result (inh Σ Γ T) :=
prf <- check_type_wf_env_fast optimized_abstract_env_impl Σ Γ wfΓ t (T := T) ;;
ret (t; prf).
Ltac fill_inh t :=
lazymatch goal with
[ wfΓ : ∀ _ _ , ∥ wf_local _ ?Γ ∥ |- inh ?Σ ?Γ ?T ] ⇒
let t := uconstr:(check_inh Σ Γ wfΓ t (T:=T)) in
let proof := eval cbn in t in
match proof with
| Checked ?d ⇒ exact_no_check d
| TypeError ?e ⇒
let str := eval cbn in (string_of_type_error Σ e) in
fail "Failed to inhabit " T " : " str
| _ ⇒ fail "Anomaly: unexpected return value: " proof
end
| [ |- inh _ ?Γ _ ] ⇒ fail "Missing local wellformedness assumption for" Γ
end.