Add Search Blacklist "_graph_mut".

Definition global_ext_uctx (Σ : global_env_ext) : ContextSet.t
  := (global_ext_levels Σ, global_ext_constraints Σ).

Section TypeOf.
  Context {cf : checker_flags}.
  Context (Σ : global_env_ext).
  Context (hΣ : ∥ wf Σ ∥) (Hφ : ∥ on_udecl Σ.1 Σ.2 ∥).
  Context (G : universes_graph) (HG : is_graph_of_uctx G (global_ext_uctx Σ)).

  Lemma typing_wellformed Γ t T : Σ ;;; Γ |- t : T → wellformed Σ Γ T.

  Section SortOf.
    Context (type_of : ∀ Γ t, welltyped Σ Γ t → typing_result (∑ T, ∥ Σ ;;; Γ |- t : T ∥)).

    Program Definition type_of_as_sort Γ t (wf : welltyped Σ Γ t) : typing_result universe :=
      tx <- type_of Γ t wf ;;
      wfs <- @reduce_to_sort cf Σ hΣ Γ (projT1 tx) _ ;;
      ret (m:=typing_result) (projT1 wfs).

  End SortOf.


  Program Definition option_or {A} (a : option A) (e : type_error) : typing_result (∑ x : A, a = Some x) :=
    match a with
    | Some d ⇒ ret (d; eq_refl)
    | None ⇒ raise e
    end.

  Program Fixpoint type_of (Γ : context) (t : term) : welltyped Σ Γ t →
                                                      typing_result (∑ T : term, ∥ Σ ;;; Γ |- t : T ∥) :=
    match t return welltyped Σ Γ t → typing_result (∑ T : term, ∥ Σ ;;; Γ |- t : T ∥) with
    | tRel n ⇒ fun wf ⇒
                  t <- option_or (option_map (lift0 (S n) ∘ decl_type) (nth_error Γ n)) (UnboundRel n);;
                  ret (t.π1; _)

    | tVar n ⇒ fun wf ⇒ raise (UnboundVar n)
    | tEvar ev args ⇒ fun wf ⇒ raise (UnboundEvar ev)

    | tSort s ⇒ fun wf ⇒ ret (tSort (Universe.try_suc s); _)

    | tProd n t b ⇒ fun wf ⇒
      s1 <- type_of_as_sort type_of Γ t _ ;;
      s2 <- type_of_as_sort type_of (Γ ,, vass n t) b _ ;;
      ret (tSort (Universe.sort_of_product s1 s2); _)

    | tLambda n t b ⇒ fun wf ⇒
      t2 <- type_of (Γ ,, vass n t) b _;;
      ret (tProd n t t2.π1; _)

    | tLetIn n b b_ty b' ⇒ fun wf ⇒
      b'_ty <- type_of (Γ ,, vdef n b b_ty) b' _ ;;
      ret (tLetIn n b b_ty b'_ty.π1; _)

    | tApp t a ⇒ fun wf ⇒
      ty <- type_of Γ t _ ;;
      pi <- reduce_to_prod hΣ Γ ty.π1 _ ;;
      ret (subst10 a pi.π2.π2.π1; _)

    | tConst cst u ⇒ fun wf ⇒
          match lookup_env (fst Σ) cst with
          | Some (ConstantDecl _ d) ⇒
            let ty := subst_instance_constr u d.(cst_type) in
            ret (ty; _)
          | _ ⇒ raise (UndeclaredConstant cst)
          end

    | tInd ind u ⇒ fun wf ⇒
          d <- @lookup_ind_decl Σ ind ;;
          let ty := subst_instance_constr u d.π2.π1.(ind_type) in
          ret (ty; _)

    | tConstruct ind k u ⇒ fun wf ⇒
          d <- @lookup_ind_decl Σ ind ;;
          match nth_error d.π2.π1.(ind_ctors) k with
          | Some cdecl ⇒
            ret (type_of_constructor d.π1 cdecl (ind, k) u; _)
          | None ⇒ raise (UndeclaredConstructor ind k)
          end

    | tCase (ind, par) p c brs ⇒ fun wf ⇒
      ty <- type_of Γ c _ ;;
      indargs <- reduce_to_ind hΣ Γ ty.π1 _ ;;
      ret (mkApps p (List.skipn par indargs.π2.π2.π1 ++ [c]); _)

    | tProj (ind, n, k) c ⇒ fun wf ⇒
       d <- @lookup_ind_decl Σ ind ;;
       match nth_error d.π2.π1.(ind_projs) k with
       | Some pdecl ⇒
            c_ty <- type_of Γ c _ ;;
            indargs <- reduce_to_ind hΣ Γ c_ty.π1 _ ;;
            let ty := snd pdecl in
            ret (subst0 (c :: List.rev (indargs.π2.π2.π1)) (subst_instance_constr indargs.π2.π1 ty);
                   _)
       | None ⇒ !
       end

    | tFix mfix n ⇒ fun wf ⇒
      match nth_error mfix n with
      | Some f ⇒ ret (f.(dtype); _)
      | None ⇒ raise (IllFormedFix mfix n)
      end

    | tCoFix mfix n ⇒ fun wf ⇒
      match nth_error mfix n with
      | Some f ⇒ ret (f.(dtype); _)
      | None ⇒ raise (IllFormedFix mfix n)
      end
    end.


  Solve All Obligations with program_simpl; match goal with
                                              [ |- ∥ _ ∥ ] ⇒ todo "PCUICSafeRetyping.type_of"
                                            | [ |- welltyped _ _ _ ] ⇒ todo "PCUICSafeRetyping.type_of"
                                            | [ |- wellformed _ _ _ ] ⇒ todo "PCUICSafeRetyping.type_of"
                             end.



  Conjecture cumul_reduce_to_sort : ∀ {Γ T wf s},
    reduce_to_sort hΣ Γ T wf = Checked s →
    Σ ;;; Γ |- T ≤ tSort s.π1.

  Conjecture cumul_reduce_to_prod : ∀ {Γ T wf na A B H},
    reduce_to_prod hΣ Γ T wf = Checked (na; A; B; H) →
    ∀ n, Σ ;;; Γ |- T ≤ tProd n A B.

  Conjecture congr_cumul_letin : ∀ {Γ n a A t n' a' A' t'},
    Σ ;;; Γ |- a ≤ a' →
    Σ ;;; Γ |- A ≤ A' →
    Σ ;;; Γ ,, vdef n a A' |- t ≤ t' →
    Σ ;;; Γ |- tLetIn n a A t ≤ tLetIn n' a' A' t'.










  Definition map_typing_result {A B} (f : A → B) (e : typing_result A) : typing_result B :=
    match e with
    | Checked a ⇒ Checked (f a)
    | TypeError e ⇒ TypeError e
    end.

  Theorem type_of_principal :
    ∀ {Γ t B} ,
      ∀ (wt : welltyped Σ Γ t) wt',
      type_of Γ t wt = Checked (B; wt') →
      ∀ A, Σ ;;; Γ |- t : A → Σ ;;; Γ |- B ≤ A.


End TypeOf.