Axiom reduce_to_sort :
  global_env → context → term → typing_result universe.
Axiom reduce_to_prod :
  global_env → context → term → typing_result (term × term).

Axiom reduce_to_ind :
  global_env → context → term
  → typing_result ((inductive × list Level.t) × list term).

Section TypeOf.
  Context {cf : checker_flags}.
  Context `{F : Fuel}.
  Context (Σ : global_env_ext).

  Section SortOf.
    Context (type_of : context → term → typing_result term).

    Definition type_of_as_sort Γ t :=
      tx <- type_of Γ t ;;
      reduce_to_sort (fst Σ) Γ tx.

  End SortOf.

  Fixpoint type_of (Γ : context) (t : term) : typing_result term :=
    match t with
    | tRel n ⇒
      match nth_error Γ n with
      | Some d ⇒ ret (lift0 (S n) d.(decl_type))
      | None ⇒ raise (UnboundRel n)
      end

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

    | tSort s ⇒ ret (tSort (Universe.try_suc s))

    | tProd n t b ⇒
      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 ⇒
      t2 <- type_of (Γ ,, vass n t) b ;;
       ret (tProd n t t2)

    | tLetIn n b b_ty b' ⇒
      b'_ty <- type_of (Γ ,, vdef n b b_ty) b' ;;
      ret (tLetIn n b b_ty b'_ty)

    | tApp t a ⇒
      ty <- type_of Γ t ;;
      pi <- reduce_to_prod (fst Σ) Γ ty ;;
      let '(a1, b1) := pi in
      ret (subst10 a b1)

    | tConst cst u ⇒ lookup_constant_type Σ cst u

    | tInd (mkInd ind i) u ⇒ lookup_ind_type Σ ind i u

    | tConstruct (mkInd ind i) k u ⇒
      lookup_constructor_type Σ ind i k u

    | tCase (ind, par) p c brs ⇒
      ty <- type_of Γ c ;;
      indargs <- reduce_to_ind (fst Σ) Γ ty ;;
      let '(ind', u, args) := indargs in
      ret (mkApps p (List.skipn par args ++ [c]))

    | tProj p c ⇒
      ty <- type_of Γ c ;;
      indargs <- reduce_to_ind (fst Σ) Γ ty ;;
      
      ret ty

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

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

  Definition sort_of (Γ : context) (t : term) : typing_result universe :=
    ty <- type_of Γ t;;
    type_of_as_sort type_of Γ ty.


  Conjecture cumul_reduce_to_sort : ∀ {Γ T s},
    reduce_to_sort (fst Σ) Γ T = Checked s →
    Σ ;;; Γ |- T ≤ tSort s.

  Conjecture cumul_reduce_to_prod : ∀ {Γ T A B},
    reduce_to_prod (fst Σ) Γ T = Checked (A, B) →
    ∀ 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'.










  Theorem type_of_sound :
    ∀ {Γ t A B},
      Σ ;;; Γ |- t : A →
      type_of Γ t = Checked B →
      (Σ ;;; Γ |- t : B) × (Σ ;;; Γ |- B ≤ A).

End TypeOf.