From MetaCoq.Template Require Import config Environment Ast AstUtils utils
     LiftSubst UnivSubst uGraph Typing.
Import MCMonadNotation.

Local Notation " () " := Datatypes.unit : type_scope.
Local Notation " () " := tt.

Module RedFlags.

  Record t := mk
    { beta : bool;
      iota : bool;
      zeta : bool;
      delta : bool;
      fix_ : bool;
      cofix_ : bool }.

  Definition default := mk true true true true true true.
End RedFlags.

Inductive type_error :=
| UnboundRel (n : nat)
| UnboundVar (id : string)
| UnboundMeta (m : nat)
| UnboundEvar (ev : nat)
| UndeclaredConstant (c : kername)
| UndeclaredInductive (c : inductive)
| UndeclaredConstructor (c : inductive) (i : nat)
| NotConvertible (Γ : context) (t u t' u' : term)
| NotASort (t : term)
| NotAProduct (t t' : term)
| NotAnInductive (t : term)
| IllFormedFix (m : mfixpoint term) (i : nat)
| UnsatisfiedConstraints (c : ConstraintSet.t)
| UnsatisfiableConstraints (c : ConstraintSet.t)
| NotEnoughFuel (n : nat)
| NotSupported (s : string).

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
  | UnboundMeta m ⇒ "Unbound meta " ^ string_of_nat m
  | UnboundEvar ev ⇒ "Unbound evar " ^ string_of_nat ev
  | UndeclaredConstant c ⇒ "Undeclared constant " ^ string_of_kername c
  | UndeclaredInductive c ⇒ "Undeclared inductive " ^ string_of_kername (inductive_mind c)
  | UndeclaredConstructor c i ⇒ "Undeclared inductive " ^ string_of_kername (inductive_mind c)
  | NotConvertible Γ t u t' u' ⇒ "Terms are not convertible: " ^
      string_of_term t ^ " " ^ string_of_term u ^ " after reduction: " ^
      string_of_term t' ^ " " ^ 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"
  | UnsatisfiableConstraints c ⇒ "Unsatisfiable constraints"
  | NotEnoughFuel n ⇒ "Not enough fuel"
  | NotSupported s ⇒ s ^ " are not supported"
  end.

Inductive typing_result (A : Type) :=
| Checked (a : A)
| TypeError (t : type_error).
Global Arguments Checked {A} a.
Global Arguments TypeError {A} t.

Global 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
  |}.

Global 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
  }.

Section Lookups.
  Context (Σ : global_env).

  Definition polymorphic_constraints u :=
    match u with
    | Monomorphic_ctx ⇒ ConstraintSet.empty
    | Polymorphic_ctx ctx ⇒ (AUContext.repr ctx).2.2
    end.

  Definition lookup_constant_type cst u :=
    match lookup_env Σ cst with
    | Some (ConstantDecl {| cst_type := ty; cst_universes := uctx |}) ⇒
      ret (subst_instance u ty)
    | _ ⇒ raise (UndeclaredConstant cst)
    end.

  Definition lookup_constant_type_cstrs cst u :=
    match lookup_env Σ cst with
    | Some (ConstantDecl {| cst_type := ty; cst_universes := uctx |}) ⇒
      let cstrs := polymorphic_constraints uctx in
      ret (subst_instance u ty, subst_instance_cstrs u cstrs)
      | _ ⇒ raise (UndeclaredConstant cst)
    end.

  Definition lookup_ind_decl ind i :=
    match lookup_env Σ ind with
    | Some (InductiveDecl mdecl) ⇒
      match nth_error mdecl.(ind_bodies) i with
      | Some body ⇒ ret (mdecl, body)
      | None ⇒ raise (UndeclaredInductive (mkInd ind i))
      end
    | _ ⇒ raise (UndeclaredInductive (mkInd ind i))
    end.

  Definition lookup_ind_type ind i (u : list Level.t) :=
    res <- lookup_ind_decl ind i ;;
    ret (subst_instance u (snd res).(ind_type)).

  Definition lookup_ind_type_cstrs ind i (u : list Level.t) :=
    res <- lookup_ind_decl ind i ;;
    let '(mib, body) := res in
    let uctx := mib.(ind_universes) in
    let cstrs := polymorphic_constraints uctx in
    ret (subst_instance u body.(ind_type), subst_instance_cstrs u cstrs).

  Definition lookup_constructor_decl ind i k :=
    res <- lookup_ind_decl ind i;;
    let '(mib, body) := res in
    match nth_error body.(ind_ctors) k with
    | Some cdecl ⇒ ret (mib, cdecl)
    | None ⇒ raise (UndeclaredConstructor (mkInd ind i) k)
    end.

  Definition lookup_constructor_type ind i k u :=
    res <- lookup_constructor_decl ind i k ;;
    let '(mib, cdecl) := res in
    ret (subst0 (inds ind u mib.(ind_bodies)) (subst_instance u cdecl.(cstr_type))).

  Definition lookup_constructor_type_cstrs ind i k u :=
    res <- lookup_constructor_decl ind i k ;;
    let '(mib, cdecl) := res in
    let cstrs := polymorphic_constraints mib.(ind_universes) in
    ret (subst0 (inds ind u mib.(ind_bodies)) (subst_instance u cdecl.(cstr_type)),
        subst_instance_cstrs u cstrs).
End Lookups.

Section Reduce.
  Context (flags : RedFlags.t) (Σ : global_env).

  Definition zip (t : term × list term) := mkApps (fst t) (snd t).

  Fixpoint reduce_stack (Γ : context) (n : nat) (t : term) (stack : list term)
    : option (term × list term) :=
  match n with 0 ⇒ None | S n ⇒
  match t with

  | tRel c ⇒
    if RedFlags.zeta flags then
      d <- nth_error Γ c ;;
      match d.(decl_body) with
      | None ⇒ ret (t, stack)
      | Some b ⇒ reduce_stack Γ n (lift0 (S c) b) stack
      end
    else ret (t, stack)

  | tLetIn _ b _ c ⇒
    if RedFlags.zeta flags then
      reduce_stack Γ n (subst10 b c) stack
    else ret (t, stack)

  | tConst c u ⇒
    if RedFlags.delta flags then
      match lookup_env Σ c with
      | Some (ConstantDecl {| cst_body := Some body |}) ⇒
        let body' := subst_instance u body in
        reduce_stack Γ n body' stack
      | _ ⇒ ret (t, stack)
      end
    else ret (t, stack)

  | tApp f args ⇒ reduce_stack Γ n f (args ++ stack)

  | tLambda na ty b ⇒
    if RedFlags.beta flags then
      match stack with
      | a :: args' ⇒
        

        
        reduce_stack Γ n (subst10 a b) args'
      | _ ⇒ ret (t, stack)
               
               
      end
    else ret (t, stack)

  | tFix mfix idx ⇒
    if RedFlags.fix_ flags then
      nf <- unfold_fix mfix idx ;;
      let '(narg, fn) := nf in
      match List.nth_error stack narg with
      | Some c ⇒
        c' <- reduce_stack Γ n c [] ;;
        match fst c' with
        | tConstruct _ _ _ ⇒ reduce_stack Γ n fn stack
        | _ ⇒ ret (t, stack)
        end
      | _ ⇒ ret (t, stack)
      end
    else ret (t, stack)

  | tProd _ _ _ ⇒ ret (t, stack)

    
    
    

  | tCast c _ _ ⇒ reduce_stack Γ n c stack

  | tCase ci p c brs ⇒
    if RedFlags.iota flags then
      c' <- reduce_stack Γ n c [] ;;
      match c' with
      | (tConstruct ind c _, args) ⇒
        match nth_error brs c with
        | Some br ⇒
          match lookup_constructor_decl Σ (inductive_mind ind) (inductive_ind ind) c with
          | Checked (mdecl, cdecl) ⇒
            let bctx := case_branch_context ind mdecl cdecl p br in
              reduce_stack Γ n (iota_red ci.(ci_npar) args bctx br) stack
          | TypeError e ⇒ ret (t, stack)
          end
        | None ⇒ ret (tCase ci p (zip c') brs, stack)
        end
      | _ ⇒ ret (tCase ci p (zip c') brs, stack)
      end
    else ret (t, stack)

  | _ ⇒ ret (t, stack)

  end
  end.

  Definition reduce_stack_term Γ n c :=
    res <- reduce_stack Γ n c [] ;;
    ret (zip res).

  Definition fix_decls (l : mfixpoint term) :=
    let fix aux acc ds :=
        match ds with
        | nil ⇒ acc
        | d :: ds ⇒ aux (vass d.(dname) d.(dtype) :: acc) ds
        end
    in aux [] l.

  Definition rebuild_case_predicate_ctx ind (p : predicate term) : context :=
    match lookup_ind_decl Σ (inductive_mind ind) (inductive_ind ind) with
    | TypeError _ ⇒ []
    | Checked (mib, oib) ⇒ case_predicate_context ind mib oib p
    end.

  Definition map_context_with_binders (f : context → term → term) (c : context) Γ : context :=
    fold_left (fun acc decl ⇒ map_decl (f (Γ ,,, acc)) decl :: acc) (List.rev c) [].

  Definition map_predicate_with_binders (f : context → term → term) Γ ind (p : predicate term) :=
    let pctx := rebuild_case_predicate_ctx ind p in
    let Γparams := map_context_with_binders f pctx Γ in
    {| pparams := map (f Γ) p.(pparams);
       puinst := p.(puinst);
       pcontext := p.(pcontext);
       preturn := f Γparams (preturn p) |}.

  Definition rebuild_case_branch_ctx ind i p br :=
    match lookup_constructor_decl Σ (inductive_mind ind) (inductive_ind ind) i with
    | TypeError _ ⇒ []
    | Checked (mib, cdecl) ⇒ case_branch_context ind mib cdecl p br
    end.

  Definition map_case_branch_with_binders ind i (f : context → term → term) Γ p br :=
    let ctx := rebuild_case_branch_ctx ind i p br in
    map_branch (f (Γ ,,, ctx)) br.

  Definition map_constr_with_binders (f : context → term → term) Γ (t : term) : term :=
    match t with
    | tRel i ⇒ t
    | tEvar ev args ⇒ tEvar ev (List.map (f Γ) args)
    | tLambda na T M ⇒ tLambda na (f Γ T) (f Γ M)
    | tApp u v ⇒ tApp (f Γ u) (List.map (f Γ) v)
    | tProd na A B ⇒
      let A' := f Γ A in
      tProd na A' (f (Γ ,, vass na A') B)
    | tCast c kind t ⇒ tCast (f Γ c) kind (f Γ t)
    | tLetIn na b t c ⇒
      let b' := f Γ b in
      let t' := f Γ t in
      tLetIn na b' t' (f (Γ ,, vdef na b' t') c)
    | tCase ci p c brs ⇒
      let p' := map_predicate_with_binders f Γ ci.(ci_ind) p in
      let brs' := mapi (fun i x ⇒ map_case_branch_with_binders ci.(ci_ind) i f Γ p' x) brs in
      tCase ci p' (f Γ c) brs'
    | tProj p c ⇒ tProj p (f Γ c)
    | tFix mfix idx ⇒
      let Γ' := fix_decls mfix ++ Γ in
      let mfix' := List.map (map_def (f Γ) (f Γ')) mfix in
      tFix mfix' idx
    | tCoFix mfix k ⇒
      let Γ' := fix_decls mfix ++ Γ in
      let mfix' := List.map (map_def (f Γ) (f Γ')) mfix in
      tCoFix mfix' k
    | x ⇒ x
    end.

  Fixpoint reduce_opt Γ n c :=
    match n with
    | 0 ⇒ None
    | S n ⇒
      match reduce_stack_term Γ n c with
      | Some c' ⇒
        Some (map_constr_with_binders
                (fun Γ t ⇒ match reduce_opt Γ n t with
                            | Some t ⇒ t
                            | None ⇒ t end) Γ c')
      | None ⇒ None
      end
    end.

End Reduce.

Definition isConstruct c :=
  match c with
  | tConstruct _ _ _ ⇒ true
  | tApp (tConstruct _ _ _) _ ⇒ true
  | _ ⇒ false
  end.

Definition isCoFix c :=
  match c with
  | tCoFix _ _ ⇒ true
  | _ ⇒ false
  end.

Inductive conv_pb :=
| Conv
| Cumul.

Definition eq_case_info (ci ci' : case_info) :=
  eq_inductive ci.(ci_ind) ci'.(ci_ind) && Nat.eqb ci.(ci_npar) ci'.(ci_npar).
Fixpoint eq_term `{checker_flags} (φ : universes_graph) (t u : term) {struct t} :=
  match t, u with
  | tRel n, tRel n' ⇒ Nat.eqb n n'
  | tEvar ev args, tEvar ev' args' ⇒ Nat.eqb ev ev' && forallb2 (eq_term φ) args args'
  | tVar id, tVar id' ⇒ eqb id id'
  | tSort s, tSort s' ⇒ check_eqb_universe φ s s'
  | tCast f k T, tCast f' k' T' ⇒ eq_term φ f f' && eq_term φ T T'
  | tApp f args, tApp f' args' ⇒ eq_term φ f f' && forallb2 (eq_term φ) args args'
  | tConst c u, tConst c' u' ⇒ eq_constant c c' && eqb_univ_instance φ u u'
  | tInd i u, tInd i' u' ⇒ eq_inductive i i' && eqb_univ_instance φ u u'
  | tConstruct i k u, tConstruct i' k' u' ⇒ eq_inductive i i' && Nat.eqb k k'
                                                    && eqb_univ_instance φ u u'
  | tLambda _ b t, tLambda _ b' t' ⇒ eq_term φ b b' && eq_term φ t t'
  | tProd _ b t, tProd _ b' t' ⇒ eq_term φ b b' && eq_term φ t t'
  | tLetIn _ b t c, tLetIn _ b' t' c' ⇒ eq_term φ b b' && eq_term φ t t' && eq_term φ c c'
  | tCase ci p c brs,
    tCase ci' p' c' brs' ⇒
    eq_case_info ci ci' &&
    eqb_predicate (eqb_univ_instance φ) (eq_term φ) p p' && eq_term φ c c' && forallb2 (fun br br' ⇒ eq_term φ br.(bbody) br'.(bbody)) brs brs'
  | tProj p c, tProj p' c' ⇒ eq_projection p p' && eq_term φ c c'
  | tFix mfix idx, tFix mfix' idx' ⇒
    forallb2 (fun x y ⇒
                eq_term φ x.(dtype) y.(dtype) && eq_term φ x.(dbody) y.(dbody)) mfix mfix' &&
    Nat.eqb idx idx'
  | tCoFix mfix idx, tCoFix mfix' idx' ⇒
    forallb2 (fun x y ⇒
                eq_term φ x.(dtype) y.(dtype) && eq_term φ x.(dbody) y.(dbody)) mfix mfix' &&
    Nat.eqb idx idx'
  | _, _ ⇒ false
  end.

Fixpoint leq_term `{checker_flags} (φ : universes_graph) (t u : term) {struct t} :=
  match t, u with
  | tRel n, tRel n' ⇒ Nat.eqb n n'
  | tEvar ev args, tEvar ev' args' ⇒ Nat.eqb ev ev' && forallb2 (eq_term φ) args args'
  | tVar id, tVar id' ⇒ eqb id id'
  | tSort s, tSort s' ⇒ check_leqb_universe φ s s'
  | tApp f args, tApp f' args' ⇒ eq_term φ f f' && forallb2 (eq_term φ) args args'
  | tCast f k T, tCast f' k' T' ⇒ eq_term φ f f' && eq_term φ T T'
  | tConst c u, tConst c' u' ⇒ eq_constant c c' && eqb_univ_instance φ u u'
  | tInd i u, tInd i' u' ⇒ eq_inductive i i' && eqb_univ_instance φ u u'
  | tConstruct i k u, tConstruct i' k' u' ⇒ eq_inductive i i' && Nat.eqb k k' &&
                                                    eqb_univ_instance φ u u'
  | tLambda _ b t, tLambda _ b' t' ⇒ eq_term φ b b' && eq_term φ t t'
  | tProd _ b t, tProd _ b' t' ⇒ eq_term φ b b' && leq_term φ t t'
  | tLetIn _ b t c, tLetIn _ b' t' c' ⇒ eq_term φ b b' && eq_term φ t t' && leq_term φ c c'
  | tCase ci p c brs, tCase ci' p' c' brs' ⇒
    eq_case_info ci ci' &&
    eqb_predicate (eqb_univ_instance φ) (eq_term φ) p p' && eq_term φ c c' && forallb2 (fun br br' ⇒ eq_term φ br.(bbody) br'.(bbody)) brs brs'
  | tProj p c, tProj p' c' ⇒ eq_projection p p' && eq_term φ c c'
  | tFix mfix idx, tFix mfix' idx' ⇒
    forallb2 (fun x y ⇒
                eq_term φ x.(dtype) y.(dtype) && eq_term φ x.(dbody) y.(dbody)) mfix mfix' &&
    Nat.eqb idx idx'
  | tCoFix mfix idx, tCoFix mfix' idx' ⇒
    forallb2 (fun x y ⇒
                eq_term φ x.(dtype) y.(dtype) && eq_term φ x.(dbody) y.(dbody)) mfix mfix' &&
    Nat.eqb idx idx'
  | _, _ ⇒ false
  end.

Section Conversion.

  Context `{checker_flags} (flags : RedFlags.t).
  Context (Σ : global_env) (G : universes_graph).

  Definition nodelta_flags := RedFlags.mk true true true false true true.

  Definition unfold_one_fix n Γ mfix idx l :=
    unf <- unfold_fix mfix idx ;;
    let '(arg, fn) := unf in
    c <- nth_error l arg ;;
    cred <- reduce_stack RedFlags.default Σ Γ n c [] ;;
    let '(cred, _) := cred in
    if negb (isConstruct cred) then None
    else Some fn.

  Definition unfold_one_case n Γ c :=
    cred <- reduce_stack_term RedFlags.default Σ Γ n c ;;
    if negb (isConstruct cred || isCoFix cred) then None
    else Some cred.

  Definition reducible_head n Γ c l :=
    match c with
    | tFix mfix idx ⇒ unfold_one_fix n Γ mfix idx l
    | tCase ind' p' c' brs ⇒
      match unfold_one_case n Γ c' with
      | None ⇒ None
      | Some c' ⇒ Some (tCase ind' p' c' brs)
      end
    | tProj p c ⇒
      match unfold_one_case n Γ c with
      | None ⇒ None
      | Some c' ⇒ Some (tProj p c')
      end
    | tConst c _ ⇒
      match lookup_env Σ c with
      | Some (ConstantDecl {| cst_body := Some body |}) ⇒ Some body
      | _ ⇒ None
      end
    | _ ⇒ None
    end.

  Definition lookup_env c := lookup_env Σ c.

  Definition opt_bool_to_bool (x : option bool) : bool :=
    match x with
    | Some b ⇒ b
    | None ⇒ false
    end.

  Fixpoint isconv (n : nat) (leq : conv_pb) (Γ : context)
           (t1 : term) (l1 : list term) (t2 : term) (l2 : list term) {struct n} : option bool :=
    match n with 0 ⇒ None | S n ⇒
    red1 <- reduce_stack nodelta_flags Σ Γ n t1 l1 ;;
    red2 <- reduce_stack nodelta_flags Σ Γ n t2 l2 ;;
    let '(t1,l1) := red1 in
    let '(t2,l2) := red2 in
    isconv_prog n leq Γ t1 l1 t2 l2
    end
  with isconv_prog (n : nat) (leq : conv_pb) (Γ : context)
                   (t1 : term) (l1 : list term) (t2 : term) (l2 : list term)
                   {struct n} : option bool :=
    match n with 0 ⇒ None | S n ⇒
    let isconv_stacks l1 l2 :=
        ret (forallb2 (fun x y ⇒ opt_bool_to_bool (isconv n Conv Γ x [] y [])) l1 l2)
    in
    let on_cond (b : bool) := if b then isconv_stacks l1 l2 else ret false in
    

    
    
    let fallback (x : unit) :=
      match reducible_head n Γ t1 l1 with
      | Some t1 ⇒
        redt <- reduce_stack nodelta_flags Σ Γ n t1 l1 ;;
        let '(t1, l1) := redt in
        isconv_prog n leq Γ t1 l1 t2 l2
      | None ⇒
        match reducible_head n Γ t2 l2 with
        | Some t2 ⇒
          redt <- reduce_stack nodelta_flags Σ Γ n t2 l2 ;;
          let '(t2, l2) := redt in
          isconv_prog n leq Γ t1 l1 t2 l2
        | None ⇒
          on_cond (match leq with
                   | Conv ⇒ eq_term G t1 t2
                   | Cumul ⇒ leq_term G t1 t2 end)
        end
      end
    in
    match t1, t2 with
    | tApp f args, tApp f' args' ⇒
      None

    | tCast t _ v, tCast u _ v' ⇒ None

    | tConst c u, tConst c' u' ⇒
      if eq_constant c c' then
        b <- isconv_stacks l1 l2 ;;
        if b then ret true
        else
          match lookup_env c with
          | Some (ConstantDecl {| cst_body := Some body |}) ⇒
            isconv n leq Γ body l1 body l2
          | _ ⇒ ret false
          end
      else
        match lookup_env c' with
        | Some (ConstantDecl {| cst_body := Some body |}) ⇒
          isconv n leq Γ t1 l1 body l2
        | _ ⇒
          match lookup_env c with
          | Some (ConstantDecl {| cst_body := Some body |}) ⇒
            isconv n leq Γ body l1 t2 l2
          | _ ⇒ ret false
          end
        end

    | tLambda na b t, tLambda _ b' t' ⇒
      cnv <- isconv n Conv Γ b [] b' [] ;;
      if (cnv : bool) then
        isconv n Conv (Γ ,, vass na b) t [] t' []
      else ret false

    | tProd na b t, tProd _ b' t' ⇒
      cnv <- isconv n Conv Γ b [] b' [] ;;
      if (cnv : bool) then
        isconv n leq (Γ ,, vass na b) t [] t' []
      else ret false

    | tCase ci p c brs,
      tCase ci' p' c' brs' ⇒
      if eq_case_info ci ci' && eqb_predicate (eqb_univ_instance G) (eq_term G) p p' && eq_term G c c'
      && forallb2 (fun br br' ⇒ eq_term G br.(bbody) br'.(bbody)) brs brs' then
        ret true
      else
        cred <- reduce_stack_term RedFlags.default Σ Γ n c ;;
        c'red <- reduce_stack_term RedFlags.default Σ Γ n c' ;;
        if eq_term G cred c && eq_term G c'red c' then ret true
        else
          isconv n leq Γ (tCase ci p cred brs) l1 (tCase ci' p c'red brs') l2

    | tProj p c, tProj p' c' ⇒ on_cond (eq_projection p p' && eq_term G c c')

    | tFix mfix idx, tFix mfix' idx' ⇒
      
      if eq_term G t1 t2 && opt_bool_to_bool (isconv_stacks l1 l2) then ret true
      else
        match unfold_one_fix n Γ mfix idx l1 with
        | Some t1 ⇒
          redt <- reduce_stack nodelta_flags Σ Γ n t1 l1 ;;
          let '(t1, l1) := redt in
          isconv_prog n leq Γ t1 l1 t2 l2
        | None ⇒
          match unfold_one_fix n Γ mfix' idx' l2 with
          | Some t2 ⇒
            redt <- reduce_stack nodelta_flags Σ Γ n t2 l2 ;;
            let '(t2, l2) := redt in
            isconv_prog n leq Γ t1 l1 t2 l2
          | None ⇒ ret false
          end
        end

    | tCoFix mfix idx, tCoFix mfix' idx' ⇒
      on_cond (eq_term G t1 t2)

    | _, _ ⇒ fallback ()
    end
    end.
End Conversion.

Definition try_reduce Σ Γ n t :=
  match reduce_opt RedFlags.default Σ Γ n t with
  | Some t' ⇒ t'
  | None ⇒ t
  end.

Definition check_conv_gen `{checker_flags} {F:Fuel} conv_pb Σ G Γ t u :=
  match isconv Σ G fuel conv_pb Γ t [] u [] with
  | Some b ⇒ if b then ret () else raise (NotConvertible Γ t u t u)
  | None ⇒ raise (NotEnoughFuel fuel)
  end.

Definition check_conv_leq `{checker_flags} {F:Fuel} := check_conv_gen Cumul.
Definition check_conv `{checker_flags} {F:Fuel} := check_conv_gen Conv.

Definition is_graph_of_global_env_ext `{checker_flags} Σ G :=
  is_graph_of_uctx G (global_ext_uctx Σ).

Section Typecheck.
  Context {F : Fuel}.
  Context (Σ : global_env).

  Definition hnf_stack Γ t :=
    match reduce_stack RedFlags.default Σ Γ fuel t [] with
    | Some t' ⇒ ret t'
    | None ⇒ raise (NotEnoughFuel fuel)
    end.

  Definition reduce Γ t :=
    match reduce_opt RedFlags.default Σ Γ fuel t with
    | Some t' ⇒ ret t'
    | None ⇒ raise (NotEnoughFuel fuel)
    end.

  Definition reduce_to_sort Γ (t : term) : typing_result Universe.t :=
    match t with
    | tSort s ⇒ ret s
    | _ ⇒
      t' <- hnf_stack Γ t ;;
      match t' with
      | (tSort s, []) ⇒ ret s
      | _ ⇒ raise (NotASort t)
      end
    end.

  Definition reduce_to_prod Γ (t : term) : typing_result (term × term) :=
    match t with
    | tProd _ a b ⇒ ret (a, b)
    | _ ⇒
      t' <- hnf_stack Γ t ;;
      match t' with
      | (tProd _ a b,[]) ⇒ ret (a, b)
      | _ ⇒ raise (NotAProduct t (zip t'))
      end
    end.

  Definition reduce_to_ind Γ (t : term) :
    typing_result (inductive × list Level.t × list term) :=
    match decompose_app t with
    | (tInd i u, l) ⇒ ret (i, u, l)
    | _ ⇒ t' <- hnf_stack Γ t ;;
           match t' with
           | (tInd i u, l) ⇒ ret (i, u, l)
           | _ ⇒ raise (NotAnInductive t)
           end
    end.
End Typecheck.

Section Typecheck.
  Context {cf : checker_flags} {F : Fuel}.
  Context (Σ : global_env) (G : universes_graph).

  Definition convert_leq Γ (t u : term) : typing_result unit :=
    if eq_term G t u then ret ()
    else
      match isconv Σ G fuel Cumul Γ t [] u [] with
      | Some b ⇒
        if b then ret ()
        else raise (NotConvertible Γ t u t u)
      | None ⇒
        t' <- reduce Σ Γ t ;;
        u' <- reduce Σ Γ u ;;
        if leq_term G t' u' then ret ()
        else raise (NotConvertible Γ t u t' u')
      end.

  Section InferAux.
    Variable (infer : context → term → typing_result term).

    Fixpoint infer_spine (Γ : context) (ty : term) (l : list term)
             {struct l} : typing_result term :=
    match l with
    | nil ⇒ ret ty
    | cons x xs ⇒
       pi <- reduce_to_prod Σ Γ ty ;;
       let '(a1, b1) := pi in
       tx <- infer Γ x ;;
       convert_leq Γ tx a1 ;;
       infer_spine Γ (subst10 x b1) xs
    end.

    Definition infer_type Γ t :=
      tx <- infer Γ t ;;
      reduce_to_sort Σ Γ tx.

    Definition infer_cumul Γ t t' :=
      tx <- infer Γ t ;;
      convert_leq Γ tx t'.

  End InferAux.

  Definition check_consistent_constraints cstrs :=
    if check_constraints G cstrs then ret tt
    else raise (UnsatisfiedConstraints cstrs).

  Fixpoint infer (Γ : 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.super s))

    | tCast c k t ⇒
      infer_type infer Γ t ;;
      infer_cumul infer Γ c t ;;
      ret t

    | tProd n t b ⇒
      s1 <- infer_type infer Γ t ;;
      s2 <- infer_type infer (Γ ,, vass n t) b ;;
      ret (tSort (Universe.sort_of_product s1 s2))

    | tLambda n t b ⇒
      infer_type infer Γ t ;;
      t2 <- infer (Γ ,, vass n t) b ;;
      ret (tProd n t t2)

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

    | tApp t l ⇒
      t_ty <- infer Γ t ;;
      infer_spine infer Γ t_ty l

    | tConst cst u ⇒
      tycstrs <- lookup_constant_type_cstrs Σ cst u ;;
      let '(ty, cstrs) := tycstrs in
      check_consistent_constraints cstrs;;
      ret ty

    | tInd (mkInd ind i) u ⇒
      tycstrs <- lookup_ind_type_cstrs Σ ind i u;;
      let '(ty, cstrs) := tycstrs in
      check_consistent_constraints cstrs;;
      ret ty

    | tConstruct (mkInd ind i) k u ⇒
      tycstrs <- lookup_constructor_type_cstrs Σ ind i k u ;;
      let '(ty, cstrs) := tycstrs in
      check_consistent_constraints cstrs;;
      ret ty

    | tCase ci p c brs ⇒
      ty <- infer Γ c ;;
      indargs <- reduce_to_ind Σ Γ ty ;;
      

      let '(ind, u, args) := indargs in
      if eq_inductive ind ci.(ci_ind) then
        let pctx := rebuild_case_predicate_ctx Σ ind p in
        let ptm := it_mkLambda_or_LetIn pctx p.(preturn) in
        ret (tApp ptm (List.skipn ci.(ci_npar) args ++ [c]))
      else
        let ind1 := tInd ind u in
        let ind2 := tInd ci.(ci_ind) u in
        raise (NotConvertible Γ ind1 ind2 ind1 ind2)

    | tProj p c ⇒
      ty <- infer Γ c ;;
      indargs <- reduce_to_ind Σ Γ 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 check (Γ : context) (t : term) (ty : term) : typing_result unit :=
    infer Γ ty ;;
    infer_cumul infer Γ t ty ;;
    ret ().

  Definition typechecking (Γ : context) (t ty : term) :=
    match check Γ t ty with
    | Checked _ ⇒ true
    | TypeError _ ⇒ false
    end.

End Typecheck.

Arguments bind _ _ _ _ ! _.
Open Scope monad.

Definition default_fuel : Fuel := Nat.pow 2 14.

Fixpoint fresh id (env : global_declarations) : bool :=
  match env with
  | nil ⇒ true
  | cons g env ⇒ negb (eq_constant g.1 id) && fresh id env
  end.

Section Checker.

  Context {cf : checker_flags} {F : Fuel}.

  Inductive env_error :=
  | IllFormedDecl (e : string) (e : type_error)
  | AlreadyDeclared (id : string).

  Inductive EnvCheck (A : Type) :=
  | CorrectDecl (a : A)
  | EnvError (e : env_error).
  Global Arguments EnvError {A} e.
  Global Arguments CorrectDecl {A} a.

  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
    |}.

  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 Σ G t :=
    wrap_error id (infer_type Σ (infer Σ G) [] t) ;; ret ().

  Definition check_wf_judgement id Σ G t ty :=
    wrap_error id (check Σ G [] t ty) ;; ret ().

  Definition infer_term Σ G t :=
    wrap_error "" (infer Σ G [] t).

  Definition check_wf_decl Σ G kn (g : global_decl) : EnvCheck () :=
    match g with
    | ConstantDecl cst ⇒
      match cst.(cst_body) with
      | Some term ⇒ check_wf_judgement (string_of_kername kn) Σ G term cst.(cst_type)
      | None ⇒ check_wf_type (string_of_kername kn) Σ G cst.(cst_type)
      end
    | InductiveDecl inds ⇒
      List.fold_left (fun acc body ⇒
                        acc ;; check_wf_type body.(ind_name) Σ G body.(ind_type))
                     inds.(ind_bodies) (ret ())
    end.

  Fixpoint check_fresh id (env : global_declarations) : EnvCheck () :=
    match env with
    | [] ⇒ ret ()
    | g :: env ⇒
      check_fresh id env;;
      if eq_constant id g.1 then
        EnvError (AlreadyDeclared (string_of_kername id))
      else ret ()
    end.

  Definition add_gc_constraints ctrs (G : universes_graph) : universes_graph
    := (G.1.1, GoodConstraintSet.fold
                  (fun ctr ⇒ wGraph.EdgeSet.add (edge_of_constraint ctr)) ctrs G.1.2,
        G.2).

  Fixpoint check_wf_declarations (univs : ContextSet.t) (G : universes_graph) (g : global_declarations)
    : EnvCheck () :=
    match g with
    | [] ⇒ ret tt
    | g :: env ⇒
      check_wf_declarations univs G env ;;
      check_wf_decl {| universes := univs; declarations := env |} G g.1 g.2 ;;
      check_fresh g.1 env ;;
      ret tt
    end.

  Definition typecheck_program (p : program) : EnvCheck term :=
    let Σ := fst p in
    let (univs, decls) := (Σ.(universes), Σ.(declarations)) in
    match gc_of_constraints (snd univs) with
    | None ⇒ EnvError (IllFormedDecl "toplevel"
        (UnsatisfiableConstraints univs.2))
    | Some ctrs ⇒
      let G := add_gc_constraints ctrs init_graph in
      if wGraph.is_acyclic G then
        check_wf_declarations univs G decls ;;
        infer_term Σ G (snd p)
      else EnvError (IllFormedDecl "toplevel"
        (UnsatisfiableConstraints univs.2))
    end.

End Checker.

Definition infer' `{checker_flags} `{Fuel} (Σ : global_env_ext) Γ t
  := let uctx := (global_ext_uctx Σ) in
    match gc_of_uctx uctx with
     | None ⇒ raise (UnsatisfiableConstraints uctx.2)
     | Some uctx ⇒ infer (fst Σ) (make_graph uctx) Γ t
     end.