Library MetaCoq.SafeChecker.PCUICSafeChecker
Lemma All_sq {A} {P : A → Type} {l}
: All (fun x ⇒ ∥ P x ∥) l → ∥ All P l ∥.
Lemma All2_sq {A B} {R : A → B → Type} {l1 l2}
: All2 (fun x y ⇒ ∥ R x y ∥) l1 l2 → ∥ All2 R l1 l2 ∥.
Lemma weakening_sq `{cf : checker_flags} {Σ Γ} Γ' {t T} :
∥ wf Σ.1 ∥ → ∥ wf_local Σ (Γ ,,, Γ') ∥ →
∥ Σ ;;; Γ |- t : T ∥ →
∥ Σ ;;; Γ ,,, Γ' |- lift0 #|Γ'| t : lift0 #|Γ'| T ∥.
Definition wf_local_rel_abs_sq `{cf : checker_flags} {Σ Γ Γ' A na} :
∥ wf_local_rel Σ Γ Γ' ∥ → {u & ∥ Σ ;;; Γ ,,, Γ' |- A : tSort u ∥ }
→ ∥ wf_local_rel Σ Γ (Γ',, vass na A) ∥.
Definition wf_local_rel_def_sq `{cf : checker_flags} {Σ Γ Γ' t A na} :
∥ wf_local_rel Σ Γ Γ' ∥ → ∥ isType Σ (Γ ,,, Γ') A ∥ → ∥ Σ ;;; Γ ,,, Γ' |- t : A ∥
→ ∥ wf_local_rel Σ Γ (Γ',, vdef na t A) ∥.
Definition wf_local_rel_app_inv_sq `{cf : checker_flags} {Σ Γ1 Γ2 Γ3} :
∥ wf_local_rel Σ Γ1 Γ2 ∥ → ∥ wf_local_rel Σ (Γ1 ,,, Γ2) Γ3 ∥
→ ∥ wf_local_rel Σ Γ1 (Γ2 ,,, Γ3) ∥.
Fixpoint monad_All {T} {M : Monad T} {A} {P} (f : ∀ x, T (P x)) l : T (@All A P l)
:= match l with
| [] ⇒ ret All_nil
| a :: l ⇒ X <- f a ;;
Y <- monad_All f l ;;
ret (All_cons X Y)
end.
Fixpoint monad_All2 {T E} {M : Monad T} {M' : MonadExc E T} wrong_sizes
{A B R} (f : ∀ x y, T (R x y)) l1 l2
: T (@All2 A B R l1 l2)
:= match l1, l2 with
| [], [] ⇒ ret (All2_nil R)
| a :: l1, b :: l2 ⇒ X <- f a b ;;
Y <- monad_All2 wrong_sizes f l1 l2 ;;
ret (All2_cons R a b l1 l2 X Y)
| _, _ ⇒ raise wrong_sizes
end.
Definition monad_prod {T} {M : Monad T} {A B} (x : T A) (y : T B): T (A × B)
:= X <- x ;; Y <- y ;; ret (X, Y).
Definition check_dec {T E} {M : Monad T} {M' : MonadExc E T} (e : E) {P}
(H : {P} + {¬ P})
: T P
:= match H with
| left x ⇒ ret x
| right _ ⇒ raise e
end.
Definition check_eq_true {T E} {M : Monad T} {M' : MonadExc E T} b (e : E)
: T (b = true)
:= if b return T (b = true) then ret eq_refl else raise e.
Program Definition check_eq_nat {T E} {M : Monad T} {M' : MonadExc E T} n m (e : E)
: T (n = m)
:= match Nat.eq_dec n m with
| left p ⇒ ret p
| right p ⇒ raise e
end.
Definition mkApps_decompose_app_rec t l :
mkApps t l = mkApps (fst (decompose_app_rec t l)) (snd (decompose_app_rec t l)).
Definition mkApps_decompose_app t :
t = mkApps (fst (decompose_app t)) (snd (decompose_app t))
:= mkApps_decompose_app_rec t [].
Inductive type_error :=
| UnboundRel (n : nat)
| UnboundVar (id : string)
| UnboundEvar (ev : nat)
| UndeclaredConstant (c : string)
| UndeclaredInductive (c : inductive)
| UndeclaredConstructor (c : inductive) (i : nat)
| NotCumulSmaller (Γ : context) (t u t' u' : term)
| NotConvertible (Γ : context) (t u : term)
| NotASort (t : term)
| NotAProduct (t t' : term)
| NotAnInductive (t : term)
| IllFormedFix (m : mfixpoint term) (i : nat)
| UnsatisfiedConstraints (c : ConstraintSet.t)
| Msg (s : string).
Lemma lookup_env_id Σ id decl
: lookup_env Σ id = Some decl → id = global_decl_ident decl.
Definition string_of_list_aux {A} (f : A → string) (l : list A) : string :=
let fix aux l :=
match l return string with
| nil ⇒ ""
| cons a nil ⇒ f a
| cons a l ⇒ f a ++ "," ++ aux l
end
in aux l.
Definition string_of_list {A} (f : A → string) (l : list A) : string :=
"[" ++ string_of_list_aux f l ++ "]".
Definition string_of_level (l : Level.t) : string :=
match l with
| Level.lProp ⇒ "Prop"
| Level.lSet ⇒ "Set"
| Level.Level s ⇒ s
| Level.Var n ⇒ "Var " ++ string_of_nat n
end.
Definition string_of_level_expr (l : Level.t × bool) : string :=
let '(l, b) := l in
string_of_level l ++ (if b then "+1" else "").
Definition string_of_sort (u : universe) :=
string_of_list string_of_level_expr u.
Definition string_of_name (na : name) :=
match na with
| nAnon ⇒ "_"
| nNamed n ⇒ n
end.
Definition string_of_universe_instance u :=
string_of_list string_of_level u.
Definition string_of_def {A : Set} (f : A → string) (def : def A) :=
"(" ++ string_of_name (dname def) ++ "," ++ f (dtype def) ++ "," ++ f (dbody def) ++ ","
++ string_of_nat (rarg def) ++ ")".
Definition string_of_inductive (i : inductive) :=
(inductive_mind i) ++ "," ++ string_of_nat (inductive_ind i).
Fixpoint string_of_term (t : term) :=
match t with
| tRel n ⇒ "#" ++ string_of_nat n
| tVar n ⇒ "Var(" ++ n ++ ")"
| tEvar ev args ⇒ "Evar(" ++ string_of_nat ev ++ "TODO" ++ ")"
| tSort s ⇒ "Sort(" ++ string_of_sort s ++ ")"
| tProd na b t ⇒ "Pi (" ++ string_of_name na ++ " : " ++
string_of_term b ++ ") (" ++ string_of_term t ++ ")"
| tLambda na b t ⇒ "Lam (" ++ string_of_name na ++ " : " ++ string_of_term b
++ ") (" ++ string_of_term t ++ ")"
| tLetIn na b t' t ⇒ "LetIn(" ++ string_of_name na ++ "," ++ string_of_term b
++ "," ++ string_of_term t' ++ "," ++ string_of_term t ++ ")"
| tApp f l ⇒ string_of_term f ++ " @ (" ++ string_of_term l ++ ")"
| tConst c u ⇒ "Const(" ++ c ++ "," ++ string_of_universe_instance u ++ ")"
| tInd i u ⇒ "Ind(" ++ string_of_inductive i ++ "," ++ string_of_universe_instance u ++ ")"
| tConstruct i n u ⇒ "Construct(" ++ string_of_inductive i ++ "," ++ string_of_nat n ++ ","
++ string_of_universe_instance u ++ ")"
| tCase (ind, i) t p brs ⇒
"Case(" ++ string_of_inductive ind ++ "," ++ string_of_nat i ++ "," ++ string_of_term t ++ ","
++ string_of_term p ++ "," ++ string_of_list (fun b ⇒ string_of_term (snd b)) brs ++ ")"
| tProj (ind, i, k) c ⇒
"Proj(" ++ string_of_inductive ind ++ "," ++ string_of_nat i ++ "," ++ string_of_nat k ++ ","
++ string_of_term c ++ ")"
| tFix l n ⇒ "Fix(" ++ (string_of_list (string_of_def string_of_term) l) ++ "," ++ string_of_nat n ++ ")"
| tCoFix l n ⇒ "CoFix(" ++ (string_of_list (string_of_def string_of_term) l) ++ "," ++ string_of_nat n ++ ")"
end.
Definition string_of_type_error (e : type_error) : string :=
match e with
| UnboundRel n ⇒ "Unboound rel " ++ string_of_nat n
| UnboundVar id ⇒ "Unbound var " ++ id
| UnboundEvar ev ⇒ "Unbound evar " ++ string_of_nat ev
| UndeclaredConstant c ⇒ "Undeclared constant " ++ c
| UndeclaredInductive c ⇒ "Undeclared inductive " ++ (inductive_mind c)
| UndeclaredConstructor c i ⇒ "Undeclared inductive " ++ (inductive_mind c)
| NotCumulSmaller Γ t u t' u' ⇒ "Terms are not <= for cumulativity: " ++
string_of_term t ++ " and " ++ string_of_term u ++ " after reduction: " ++
string_of_term t' ++ " and " ++ string_of_term u'
| NotConvertible Γ t u ⇒ "Terms are not convertible: " ++
string_of_term t ++ " and " ++ string_of_term u
| NotASort t ⇒ "Not a sort"
| NotAProduct t t' ⇒ "Not a product"
| NotAnInductive t ⇒ "Not an inductive"
| IllFormedFix m i ⇒ "Ill-formed recursive definition"
| UnsatisfiedConstraints c ⇒ "Unsatisfied constraints"
| Msg s ⇒ "Msg: " ++ s
end.
Inductive typing_result (A : Type) :=
| Checked (a : A)
| TypeError (t : type_error).
Instance typing_monad : Monad typing_result :=
{| ret A a := Checked a ;
bind A B m f :=
match m with
| Checked a ⇒ f a
| TypeError t ⇒ TypeError t
end
|}.
Instance monad_exc : MonadExc type_error typing_result :=
{ raise A e := TypeError e;
catch A m f :=
match m with
| Checked a ⇒ m
| TypeError t ⇒ f t
end
}.
Lemma wf_local_rel_inv `{checker_flags} {Σ Γ1 Γ2} (w : wf_local_rel Σ Γ1 Γ2) :
∀ d Γ2', Γ2 = Γ2' ,, d →
wf_local_rel Σ Γ1 Γ2' × (∑ u, Σ ;;; Γ1 ,,, Γ2' |- d.(decl_type) : tSort u) ×
match d.(decl_body) with
| Some b ⇒ Σ ;;; Γ1 ,,, Γ2' |- b : d.(decl_type)
| None ⇒ True
end.
Definition strengthening_wf_local_rel `{cf : checker_flags} Σ Γ1 Γ2 Γ3 Γ4 :
wf Σ.1 → wf_local_rel Σ Γ1 (Γ2 ,,, Γ3 ,,, lift_context #|Γ3| 0 Γ4)
→ wf_local_rel Σ Γ1 (Γ2 ,,, Γ4).
Definition wf_local_app_inv `{cf : checker_flags} {Σ Γ1 Γ2} :
wf_local Σ Γ1 → wf_local_rel Σ Γ1 Γ2
→ wf_local Σ (Γ1 ,,, Γ2).
Definition fix_context_i i mfix :=
List.rev (mapi_rec (fun i (d : BasicAst.def term)
⇒ vass (dname d) ((lift0 i) (dtype d))) mfix i).
Lemma lift_fix_context mfix : ∀ k k' j, j ≤ k →
fix_context_i (k + k') mfix = lift_context k' j (fix_context_i k mfix).
Lemma wf_ext_gc_of_uctx {cf:checker_flags} {Σ : global_env_ext} (HΣ : ∥ wf_ext Σ ∥)
: ∑ uctx', gc_of_uctx (global_ext_uctx Σ) = Some uctx'.
Lemma wf_ext_is_graph {cf:checker_flags} {Σ : global_env_ext} (HΣ : ∥ wf_ext Σ ∥)
: ∑ G, is_graph_of_uctx G (global_ext_uctx Σ).
Lemma map_squash {A B} (f : A → B) : ∥ A ∥ → ∥ B ∥.
Section Typecheck.
Context {cf : checker_flags} {Σ : global_env_ext} (HΣ : ∥ wf Σ ∥)
(Hφ : ∥ on_udecl Σ.1 Σ.2 ∥)
(G : universes_graph) (HG : is_graph_of_uctx G (global_ext_uctx Σ)).
Definition isType_wellformed {Γ t}
: isType Σ Γ t → wellformed Σ Γ t.
Lemma validity_wf {Γ t T} :
∥ wf_local Σ Γ ∥ → ∥ Σ ;;; Γ |- t : T ∥ → wellformed Σ Γ T.
Definition hnf := reduce_term RedFlags.default Σ HΣ.
Theorem hnf_sound {Γ t h} : ∥ red (fst Σ) Γ t (hnf Γ t h) ∥.
Program Definition reduce_to_sort Γ t (h : wellformed Σ Γ t)
: typing_result (∑ u, ∥ red (fst Σ) Γ t (tSort u) ∥) :=
match t with
| tSort s ⇒ ret (s; sq (refl_red _ _ _))
| _ ⇒
match hnf Γ t h with
| tSort s ⇒ ret (s; _)
| _ ⇒ raise (NotASort t)
end
end.
Program Definition reduce_to_prod Γ t (h : wellformed Σ Γ t)
: typing_result (∑ na a b, ∥ red (fst Σ) Γ t (tProd na a b) ∥) :=
match t with
| tProd na a b ⇒ ret (na; a; b; sq (refl_red _ _ _))
| _ ⇒
match hnf Γ t h with
| tProd na a b ⇒ ret (na; a; b; _)
| t' ⇒ raise (NotAProduct t t')
end
end.
Fixpoint stack_to_apps π : typing_result (list term) :=
match π with
| Empty ⇒ ret []
| App t π ⇒ l <- stack_to_apps π ;; ret (t :: l)
| _ ⇒ raise (Msg "not some applications")
end.
Lemma zip_stack_to_apps t π l :
stack_to_apps π = Checked l → zipc t π = mkApps t l.
Program Definition reduce_to_ind Γ t (h : wellformed Σ Γ t)
: typing_result (∑ i u l, ∥ red (fst Σ) Γ t (mkApps (tInd i u) l) ∥) :=
match decompose_app t with
| (tInd i u, l) ⇒ ret (i; u; l; sq _)
| _ ⇒
match reduce_stack RedFlags.default Σ HΣ Γ t Empty h with
| (tInd i u, π) ⇒ match stack_to_apps π with
| Checked l ⇒ ret (i; u; l; _)
| TypeError e ⇒ raise e
end
| _ ⇒ raise (NotAnInductive t)
end
end.
Definition iscumul Γ := isconv_term RedFlags.default Σ HΣ Hφ G HG Γ Cumul.
Program Definition convert_leq Γ t u
(ht : wellformed Σ Γ t) (hu : wellformed Σ Γ u)
: typing_result (∥ Σ ;;; Γ |- t ≤ u ∥) :=
match leqb_term G t u with true ⇒ ret _ | false ⇒
match iscumul Γ t ht u hu with
| true ⇒ ret _
| false ⇒
let t' := hnf Γ t ht in
let u' := hnf Γ u hu in
raise (NotCumulSmaller Γ t u t' u')
end end.
Section InferAux.
Variable (infer : ∀ Γ (HΓ : ∥ wf_local Σ Γ ∥) (t : term),
typing_result ({ A : term & ∥ Σ ;;; Γ |- t : A ∥ })).
Program Definition infer_type Γ HΓ t
: typing_result ({u : universe & ∥ Σ ;;; Γ |- t : tSort u ∥}) :=
tx <- infer Γ HΓ t ;;
u <- reduce_to_sort Γ tx.π1 _ ;;
ret (u.π1; _).
Program Definition infer_cumul Γ HΓ t A (hA : ∥ isType Σ Γ A ∥)
: typing_result (∥ Σ ;;; Γ |- t : A ∥) :=
A' <- infer Γ HΓ t ;;
X <- convert_leq Γ A'.π1 A _ _ ;;
ret _.
End InferAux.
Program Definition lookup_ind_decl ind
: typing_result
({decl & {body & declared_inductive (fst Σ) decl ind body}}) :=
match lookup_env (fst Σ) ind.(inductive_mind) with
| Some (InductiveDecl _ decl) ⇒
match nth_error decl.(ind_bodies) ind.(inductive_ind) with
| Some body ⇒ ret (decl; body; _)
| None ⇒ raise (UndeclaredInductive ind)
end
| _ ⇒ raise (UndeclaredInductive ind)
end.
Lemma check_constraints_spec ctrs
: check_constraints G ctrs → valid_constraints (global_ext_constraints Σ) ctrs.
Lemma is_graph_of_uctx_levels l :
wGraph.VSet.mem l (uGraph.wGraph.V G) →
LevelSet.mem l (global_ext_levels Σ).
Program Definition check_consistent_instance uctx u
: typing_result (consistent_instance_ext Σ uctx u)
:= match uctx with
| Monomorphic_ctx _ ⇒
check_eq_nat #|u| 0 (Msg "monomorphic instance should be of length 0")
| Polymorphic_ctx (inst, cstrs)
| Cumulative_ctx ((inst, cstrs), _) ⇒
let '(inst, cstrs) := AUContext.repr (inst, cstrs) in
check_eq_true (forallb (fun l ⇒ match no_prop_of_level l with
| Some l ⇒ wGraph.VSet.mem l (uGraph.wGraph.V G)
| None ⇒ false
end) u)
(Msg "instance does not have the right length") ;;
X <- check_eq_nat #|u| #|inst|
(Msg "instance does not have the right length");;
match check_constraints G (subst_instance_cstrs u cstrs) with
| true ⇒ ret (conj _ _)
| false ⇒ raise (Msg "ctrs not satisfiable")
end
end.
Definition eqb_opt_term (t u : option term) :=
match t, u with
| Some t, Some u ⇒ eqb_term G t u
| None, None ⇒ true
| _, _ ⇒ false
end.
Lemma eqb_opt_term_spec t u
: eqb_opt_term t u → eq_opt_term (global_ext_constraints Σ) t u.
Definition eqb_decl (d d' : context_decl) :=
eqb_opt_term d.(decl_body) d'.(decl_body) && eqb_term G d.(decl_type) d'.(decl_type).
Lemma eqb_decl_spec d d'
: eqb_decl d d' → eq_decl (global_ext_constraints Σ) d d'.
Definition eqb_context (Γ Δ : context) := forallb2 eqb_decl Γ Δ.
Lemma eqb_context_spec Γ Δ
: eqb_context Γ Δ → eq_context (global_ext_constraints Σ) Γ Δ.
Definition check_correct_arity decl ind u ctx pars pctx :=
let inddecl :=
{| decl_name := nNamed decl.(ind_name);
decl_body := None;
decl_type := mkApps (tInd ind u) (map (lift0 #|ctx|) pars ++ to_extended_list ctx) |}
in eqb_context (inddecl :: ctx) pctx.
Lemma check_correct_arity_spec decl ind u ctx pars pctx
: check_correct_arity decl ind u ctx pars pctx
→ PCUICTyping.check_correct_arity (global_ext_constraints Σ) decl ind u ctx pars pctx.
Program Fixpoint infer (Γ : context) (HΓ : ∥ wf_local Σ Γ ∥) (t : term) {struct t}
: typing_result ({ A : term & ∥ Σ ;;; Γ |- t : A ∥ }) :=
match t with
| tRel n ⇒
match nth_error Γ n with
| Some c ⇒ ret ((lift0 (S n)) (decl_type c); _)
| None ⇒ raise (UnboundRel n)
end
| tVar n ⇒ raise (UnboundVar n)
| tEvar ev args ⇒ raise (UnboundEvar ev)
| tSort u ⇒
match u with
| NEL.sing (l, false) ⇒
check_eq_true (LevelSet.mem l (global_ext_levels Σ)) (Msg ("undeclared level " ++ string_of_level l));;
ret (tSort (Universe.super l); _)
| _ ⇒ raise (Msg (string_of_sort u ++ " is not a level"))
end
| tProd na A B ⇒
s1 <- infer_type infer Γ HΓ A ;;
s2 <- infer_type infer (Γ ,, vass na A) _ B ;;
ret (tSort (Universe.sort_of_product s1.π1 s2.π1); _)
| tLambda na A t ⇒
s1 <- infer_type infer Γ HΓ A ;;
B <- infer (Γ ,, vass na A) _ t ;;
ret (tProd na A B.π1; _)
| tLetIn n b b_ty b' ⇒
infer_type infer Γ HΓ b_ty ;;
infer_cumul infer Γ HΓ b b_ty _ ;;
b'_ty <- infer (Γ ,, vdef n b b_ty) _ b' ;;
ret (tLetIn n b b_ty b'_ty.π1; _)
| tApp t u ⇒
ty <- infer Γ HΓ t ;;
pi <- reduce_to_prod Γ ty.π1 _ ;;
infer_cumul infer Γ HΓ u pi.π2.π1 _ ;;
ret (subst10 u pi.π2.π2.π1; _)
| tConst cst u ⇒
match lookup_env (fst Σ) cst with
| Some (ConstantDecl _ d) ⇒
check_consistent_instance d.(cst_universes) u ;;
let ty := subst_instance_constr u d.(cst_type) in
ret (ty; _)
| _ ⇒ raise (UndeclaredConstant cst)
end
| tInd ind u ⇒
d <- lookup_ind_decl ind ;;
check_consistent_instance d.π1.(ind_universes) u ;;
let ty := subst_instance_constr u d.π2.π1.(ind_type) in
ret (ty; _)
| tConstruct ind k u ⇒
d <- lookup_ind_decl ind ;;
match nth_error d.π2.π1.(ind_ctors) k with
| Some cdecl ⇒
check_consistent_instance d.π1.(ind_universes) u ;;
ret (type_of_constructor d.π1 cdecl (ind, k) u; _)
| None ⇒ raise (UndeclaredConstructor ind k)
end
| tCase (ind, par) p c brs ⇒
cty <- infer Γ HΓ c ;;
I <- reduce_to_ind Γ cty.π1 _ ;;
let '(ind'; I') := I in let '(u; I'') := I' in let '(args; H) := I'' in
check_eq_true (eqb ind ind')
(NotConvertible Γ (tInd ind u) (tInd ind' u)) ;;
d <- lookup_ind_decl ind' ;;
let '(decl; d') := d in let '(body; HH) := d' in
check_eq_true (ind_npars decl =? par)
(Msg "not the right number of parameters") ;;
pty <- infer Γ HΓ p ;;
match types_of_case ind decl body (firstn par args) u p pty.π1 with
| None ⇒ raise (Msg "not the type of a case")
| Some (indctx, pctx, ps, btys) ⇒
check_eq_true
(check_correct_arity body ind u indctx (firstn par args) pctx)
(Msg "not correct arity") ;;
check_eq_true
(existsb (leb_sort_family (universe_family ps)) (ind_kelim body))
(Msg "cannot eliminate over this sort") ;;
(fix check_branches (brs btys : list (nat × term))
(HH : Forall (squash ∘ (isType Σ Γ) ∘ snd) btys) {struct brs}
: typing_result
(All2 (fun x y ⇒ fst x = fst y ∧ ∥ Σ ;;; Γ |- snd x : snd y ∥) brs btys)
:= match brs, btys with
| [], [] ⇒ ret (All2_nil _)
| (n, t) :: brs , (m, A) :: btys ⇒
W <- check_dec (Msg "not nat eq")
(EqDecInstances.nat_eqdec n m) ;;
Z <- infer_cumul infer Γ HΓ t A _ ;;
X <- check_branches brs btys _ ;;
ret (All2_cons _ _ _ _ _ (conj _ _) X)
| [], _ :: _
| _ :: _, [] ⇒ raise (Msg "wrong number of branches")
end) brs btys _ ;;
ret (mkApps p (List.skipn par args ++ [c]); _)
end
| tProj (ind, n, k) c ⇒
d <- lookup_ind_decl ind ;;
match nth_error d.π2.π1.(ind_projs) k with
| Some pdecl ⇒
c_ty <- infer Γ HΓ c ;;
I <- reduce_to_ind Γ c_ty.π1 _ ;;
let '(ind'; I') := I in let '(u; I'') := I' in let '(args; H) := I'' in
check_eq_true (eqb ind ind')
(NotConvertible Γ (tInd ind u) (tInd ind' u)) ;;
check_eq_true (ind_npars d.π1 =? n)
(Msg "not the right number of parameters") ;;
check_eq_true (#|args| =? ind_npars d.π1)
(Msg "not the right number of parameters") ;;
let ty := snd pdecl in
ret (subst0 (c :: List.rev args) (subst_instance_constr u ty);
_)
| None ⇒ raise (Msg "projection not found")
end
| tFix mfix n ⇒
match nth_error mfix n with
| None ⇒ raise (IllFormedFix mfix n)
| Some decl ⇒
XX <- (fix check_types (mfix : mfixpoint term) acc (Hacc : ∥ wf_local_rel Σ Γ acc ∥) {struct mfix}
: typing_result (∥ wf_local_rel Σ (Γ ,,, acc) (fix_context_i #|acc| mfix) ∥)
:= match mfix with
| [] ⇒ ret (sq wf_local_rel_nil)
| def :: mfix ⇒
W <- infer_type infer Γ HΓ (dtype def) ;;
let W' := weakening_sq acc _ _ W.π2 in
Z <- check_types mfix
(acc ,, vass (dname def) ((lift0 #|acc|) (dtype def)))
(wf_local_rel_abs_sq Hacc (W.π1; W')) ;;
ret (wf_local_rel_app_inv_sq
(wf_local_rel_abs_sq (sq wf_local_rel_nil) (W.π1; W')) Z)
end)
mfix [] (sq wf_local_rel_nil);;
YY <- (fix check_bodies (mfix' : mfixpoint term)
(XX' : ∥ wf_local_rel Σ Γ (fix_context mfix') ∥) {struct mfix'}
: typing_result (All (fun d ⇒
∥ Σ ;;; Γ ,,, fix_context mfix |- dbody d : (lift0 #|fix_context mfix|) (dtype d) ∥
∧ isLambda (dbody d) = true) mfix')
:= match mfix' with
| [] ⇒ ret All_nil
| def :: mfix' ⇒
W1 <- infer_cumul infer (Γ ,,, fix_context mfix) _ (dbody def)
(lift0 #|fix_context mfix| (dtype def)) _ ;;
W2 <- check_eq_true (isLambda (dbody def))
(Msg "not a lambda") ;;
Z <- check_bodies mfix' _ ;;
ret (All_cons (conj W1 W2) Z)
end) mfix _ ;;
guarded <- check_eq_true (fix_guard mfix) (Msg "Unguarded fixpoint") ;;
ret (dtype decl; _)
end
| tCoFix mfix n ⇒
allowcofix <- check_eq_true allow_cofix (Msg "cofix not allowed") ;;
match nth_error mfix n with
| None ⇒ raise (IllFormedFix mfix n)
| Some decl ⇒
XX <- (fix check_types (mfix : mfixpoint term) acc (Hacc : ∥ wf_local_rel Σ Γ acc ∥) {struct mfix}
: typing_result (∥ wf_local_rel Σ (Γ ,,, acc) (fix_context_i #|acc| mfix) ∥)
:= match mfix with
| [] ⇒ ret (sq wf_local_rel_nil)
| def :: mfix ⇒
W <- infer_type infer Γ HΓ (dtype def) ;;
let W' := weakening_sq acc _ _ W.π2 in
Z <- check_types mfix
(acc ,, vass (dname def) ((lift0 #|acc|) (dtype def)))
(wf_local_rel_abs_sq Hacc (W.π1; W')) ;;
ret (wf_local_rel_app_inv_sq
(wf_local_rel_abs_sq (sq wf_local_rel_nil) (W.π1; W')) Z)
end)
mfix [] (sq wf_local_rel_nil);;
YY <- (fix check_bodies (mfix' : mfixpoint term) (XX' : ∥ wf_local_rel Σ Γ (fix_context mfix') ∥) {struct mfix'}
: typing_result (All (fun d ⇒
∥ Σ ;;; Γ ,,, fix_context mfix |- dbody d : (lift0 #|fix_context mfix|) (dtype d) ∥
) mfix')
:= match mfix' with
| [] ⇒ ret All_nil
| def :: mfix' ⇒
W1 <- infer_cumul infer (Γ ,,, fix_context mfix) _ (dbody def)
(lift0 #|fix_context mfix| (dtype def)) _ ;;
Z <- check_bodies mfix' _ ;;
ret (All_cons W1 Z)
end) mfix _ ;;
ret (dtype decl; _)
end
end.
Lemma sq_wfl_nil : ∥ wf_local Σ [] ∥.
Program Fixpoint check_context Γ : typing_result (∥ wf_local Σ Γ ∥)
:= match Γ with
| [] ⇒ ret sq_wfl_nil
| {| decl_body := None; decl_type := A |} :: Γ ⇒
HΓ <- check_context Γ ;;
XX <- infer_type infer Γ HΓ A ;;
ret _
| {| decl_body := Some t; decl_type := A |} :: Γ ⇒
HΓ <- check_context Γ ;;
XX <- infer_type infer Γ HΓ A ;;
XX <- infer_cumul infer Γ HΓ t A _ ;;
ret _
end.
Program Definition check_isWfArity Γ (HΓ : ∥ wf_local Σ Γ ∥) A
: typing_result (∥ isWfArity typing Σ Γ A ∥) :=
match destArity [] A with
| None ⇒ raise (Msg (string_of_term A ++ " is not an arity"))
| Some (ctx, s) ⇒ XX <- check_context (Γ ,,, ctx) ;;
ret _
end.
Program Definition check_wellformed Γ (HΓ : ∥ wf_local Σ Γ ∥) A
: typing_result (wellformed Σ Γ A) :=
match infer Γ HΓ A with
| Checked (ty; Hty) ⇒ ret _
| TypeError e ⇒ match check_isWfArity Γ HΓ A with
| Checked HA ⇒ ret (or_intror HA)
| TypeError _ ⇒
raise (Msg (string_of_term A ++ " is not wellformed. The type error is: " ++ string_of_type_error e))
end
end.
Program Definition check_isType Γ (HΓ : ∥ wf_local Σ Γ ∥) A
: typing_result (∥ isType Σ Γ A ∥) :=
s <- infer Γ HΓ A ;;
s' <- reduce_to_sort Γ s.π1 _ ;;
ret _.
Program Definition check Γ (HΓ : ∥ wf_local Σ Γ ∥) t A
: typing_result (∥ Σ;;; Γ |- t : A ∥) :=
check_isType Γ HΓ A ;;
infer_cumul infer Γ HΓ t A _.
End Typecheck.
Definition infer' {cf:checker_flags} {Σ} (HΣ : ∥ wf_ext Σ ∥)
:= infer (map_squash fst HΣ) (map_squash snd HΣ).
Definition make_graph_and_infer {cf:checker_flags} {Σ} (HΣ : ∥ wf_ext Σ ∥)
:= let '(G; HG) := wf_ext_is_graph HΣ in infer' HΣ G HG.
Print Assumptions infer.
Section CheckEnv.
Context {cf:checker_flags}.
Inductive env_error :=
| IllFormedDecl (e : string) (e : type_error)
| AlreadyDeclared (id : string).
Inductive EnvCheck (A : Type) :=
| CorrectDecl (a : A)
| EnvError (e : env_error).
Instance envcheck_monad : Monad EnvCheck :=
{| ret A a := CorrectDecl a ;
bind A B m f :=
match m with
| CorrectDecl a ⇒ f a
| EnvError e ⇒ EnvError e
end
|}.
Instance envcheck_monad_exc : MonadExc env_error EnvCheck :=
{ raise A e := EnvError e;
catch A m f :=
match m with
| CorrectDecl a ⇒ m
| EnvError t ⇒ f t
end
}.
Definition wrap_error {A} (id : string) (check : typing_result A) : EnvCheck A :=
match check with
| Checked a ⇒ CorrectDecl a
| TypeError e ⇒ EnvError (IllFormedDecl id e)
end.
Definition check_wf_type id Σ HΣ HΣ' G HG t
: EnvCheck (∑ u, ∥ Σ;;; [] |- t : tSort u ∥)
:= wrap_error id (@infer_type _ Σ HΣ (@infer _ Σ HΣ HΣ' G HG) [] sq_wfl_nil t).
Definition check_wf_judgement id Σ HΣ HΣ' G HG t ty
: EnvCheck (∥ Σ;;; [] |- t : ty ∥)
:= wrap_error id (@check _ Σ HΣ HΣ' G HG [] sq_wfl_nil t ty).
Definition infer_term Σ HΣ HΣ' G HG t :=
wrap_error "toplevel term" (@infer _ Σ HΣ HΣ' G HG [] sq_wfl_nil t).
Program Fixpoint check_fresh id env : EnvCheck (∥ fresh_global id env ∥) :=
match env with
| [] ⇒ ret (sq (Forall_nil _))
| g :: env ⇒
p <- check_fresh id env;;
match eq_constant id (global_decl_ident g) with
| true ⇒ EnvError (AlreadyDeclared id)
| false ⇒ ret _
end
end.
Definition add_uctx (uctx : wGraph.VSet.t × GoodConstraintSet.t)
(G : universes_graph) : universes_graph
:= let levels := wGraph.VSet.union uctx.1 G.1.1 in
let edges := wGraph.VSet.fold
(fun l E ⇒
match l with
| lSet ⇒ E
| vtn ll ⇒ wGraph.EdgeSet.add (edge_of_level ll) E
end)
uctx.1 G.1.2 in
let edges := GoodConstraintSet.fold
(fun ctr ⇒ wGraph.EdgeSet.add (edge_of_constraint ctr))
uctx.2 edges in
(levels, edges, G.2).
Definition Build_on_inductive_sq {Σ ind mdecl}
: ∥ Alli (on_ind_body (lift_typing typing) Σ ind mdecl) 0 (ind_bodies mdecl) ∥ →
∥ wf_local Σ (ind_params mdecl) ∥ →
context_assumptions (ind_params mdecl) = ind_npars mdecl →
ind_guard mdecl → ∥ on_inductive (lift_typing typing) Σ ind mdecl ∥.
Program Fixpoint monad_Alli {T} {M : Monad T} {A} {P} (f : ∀ n x, T (∥ P n x ∥)) l n
: T (∥ @Alli A P n l ∥)
:= match l with
| [] ⇒ ret (sq (Alli_nil _ _))
| a :: l ⇒ X <- f n a ;;
Y <- monad_Alli f l (S n) ;;
ret _
end.
Lemma check_one_ind_body:
∀ Σ : global_env_ext,
∥ wf Σ ∥ →
∥ on_udecl Σ.1 Σ.2 ∥ →
∀ G : universes_graph,
is_graph_of_uctx G (global_ext_uctx Σ) →
∀ (id : kername) (mdecl : mutual_inductive_body)
(n : nat) (x : one_inductive_body),
EnvCheck (∥ on_ind_body (lift_typing typing) Σ id mdecl n x ∥).
Program Definition check_wf_decl (Σ : global_env_ext) HΣ HΣ' G HG
(d : global_decl)
: EnvCheck (∥ on_global_decl (lift_typing typing) Σ d ∥) :=
match d with
| ConstantDecl id cst ⇒
match cst.(cst_body) with
| Some term ⇒ check_wf_judgement id Σ HΣ HΣ' G HG term cst.(cst_type) ;; ret _
| None ⇒ check_wf_type id Σ HΣ HΣ' G HG cst.(cst_type) ;; ret _
end
| InductiveDecl id mdecl ⇒
X1 <- monad_Alli (check_one_ind_body Σ HΣ HΣ' G HG id mdecl) _ _ ;;
X2 <- wrap_error id (check_context HΣ HΣ' G HG (ind_params mdecl)) ;;
X3 <- wrap_error id (check_eq_nat (context_assumptions (ind_params mdecl))
(ind_npars mdecl)
(Msg "wrong number of parameters")) ;;
X4 <- wrap_error id (check_eq_true (ind_guard mdecl) (Msg "guard"));;
ret (Build_on_inductive_sq X1 X2 X3 X4)
end.
Definition uctx_of_udecl u : ContextSet.t :=
(levels_of_udecl u, constraints_of_udecl u).
Lemma add_uctx_make_graph levels1 levels2 ctrs1 ctrs2
: add_uctx (levels1, ctrs1) (make_graph (levels2, ctrs2))
= make_graph (wGraph.VSet.union levels1 levels2,
GoodConstraintSet.union ctrs1 ctrs2).
Lemma gc_of_constraints_union S S'
: gc_of_constraints (ConstraintSet.union S S') =
(S1 <- gc_of_constraints S ;;
S2 <- gc_of_constraints S' ;;
ret (GoodConstraintSet.union S1 S2)).
Lemma no_prop_levels_union S S'
: no_prop_levels (LevelSet.union S S')
= wGraph.VSet.union (no_prop_levels S) (no_prop_levels S').
Axiom graph_eq : ∀ (G G' : universes_graph),
wGraph.VSet.Equal G.1.1 G'.1.1
→ wGraph.EdgeSet.Equal G.1.2 G'.1.2
→ G.2 = G'.2
→ G = G'.
Program Definition check_udecl id (Σ : global_env) (HΣ : ∥ wf Σ ∥) G
(HG : is_graph_of_uctx G (global_uctx Σ)) (udecl : universes_decl)
: EnvCheck (∑ uctx', gc_of_uctx (uctx_of_udecl udecl) = Some uctx' ∧
∥ on_udecl Σ udecl ∥) :=
let levels := levels_of_udecl udecl in
let global_levels := global_levels Σ in
let all_levels := LevelSet.union levels global_levels in
check_eq_true (LevelSet.for_all (fun l ⇒ negb (LevelSet.mem l global_levels))
levels) (IllFormedDecl id (Msg ("non fresh level in " ++ Pretty.print_lset levels)));;
check_eq_true (ConstraintSet.for_all (fun '(l1, _, l2) ⇒ LevelSet.mem l1 all_levels && LevelSet.mem l2 all_levels) (constraints_of_udecl udecl))
(IllFormedDecl id (Msg ("non declared level in " ++ Pretty.print_lset levels ++
" |= " ++ Pretty.print_constraint_set (constraints_of_udecl udecl))));;
check_eq_true match udecl with
| Monomorphic_ctx ctx
⇒ LevelSet.for_all (negb ∘ Level.is_var) ctx.1
| _ ⇒ true
end (IllFormedDecl id (Msg "Var level in monomorphic context")) ;;
match gc_of_uctx (uctx_of_udecl udecl) as X' return (X' = _ → EnvCheck _) with
| None ⇒ fun _ ⇒
raise (IllFormedDecl id (Msg "constraints trivially not satisfiable"))
| Some uctx' ⇒ fun Huctx ⇒
check_eq_true (wGraph.is_acyclic (add_uctx uctx' G))
(IllFormedDecl id (Msg "constraints not satisfiable"));;
ret (uctx'; (conj _ _))
end eq_refl.
Program Fixpoint check_wf_env (Σ : global_env)
: EnvCheck (∑ G, (is_graph_of_uctx G (global_uctx Σ) ∧ ∥ wf Σ ∥)) :=
match Σ with
| [] ⇒ ret (init_graph; _)
| d :: Σ ⇒
G <- check_wf_env Σ ;;
check_fresh (global_decl_ident d) Σ ;;
let udecl := universes_decl_of_decl d in
uctx <- check_udecl (global_decl_ident d) Σ _ G.π1 (proj1 G.π2) udecl ;;
let G' := add_uctx uctx.π1 G.π1 in
check_wf_decl (Σ, udecl) _ _ G' _ d ;;
match udecl with
| Monomorphic_ctx _ ⇒ ret (G'; _)
| Polymorphic_ctx _ ⇒ ret (G.π1; _)
| Cumulative_ctx _ ⇒ ret (G.π1; _)
end
end.
Lemma wf_consistent Σ : wf Σ → consistent (global_constraints Σ).
Program Definition typecheck_program (p : program)
: EnvCheck (∑ A, ∥ empty_ext (List.rev p.1) ;;; [] |- p.2 : A ∥) :=
let Σ := List.rev (fst p) in
G <- check_wf_env Σ ;;
@infer_term (empty_ext Σ) (proj2 G.π2) _ G.π1 _ (snd p).
End CheckEnv.