let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
  | O
  | S of nat

type ('a, 'b) prod =
  | Pair of 'a * 'b

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

type 'a sig2 = 'a
  (* singleton inductive, whose constructor was exist2 *)

(** val pred : nat -> nat **)

let pred n = match n with
  | O -> n
  | S u -> u

(** val plus : nat -> nat -> nat **)

let rec plus n m =
  match n with
    | O -> m
    | S p -> S (plus p m)

(** val eq_nat_dec : nat -> nat -> bool **)

let rec eq_nat_dec n m =
  match n with
    | O -> (match m with
              | O -> true
              | S m0 -> false)
    | S n0 -> (match m with
                 | O -> false
                 | S m0 -> eq_nat_dec n0 m0)

(** val lt_eq_lt_dec : nat -> nat -> bool option **)

let rec lt_eq_lt_dec n m =
  match n with
    | O -> (match m with
              | O -> Some false
              | S n0 -> Some true)
    | S n0 -> (match m with
                 | O -> None
                 | S m0 -> lt_eq_lt_dec n0 m0)

(** val le_lt_dec : nat -> nat -> bool **)

let rec le_lt_dec n m =
  match n with
    | O -> true
    | S n0 -> (match m with
                 | O -> false
                 | S m0 -> le_lt_dec n0 m0)

(** val le_gt_dec : nat -> nat -> bool **)

let le_gt_dec n m =
  le_lt_dec n m

type 'a list =
  | Nil
  | Cons of 'a * 'a list

type sort =
  | Kind
  | Prop

type term =
  | Srt of sort
  | Ref of nat
  | Abs of term * term
  | App of term * term
  | Prod of term * term

(** val lift_rec : nat -> term -> nat -> term **)

let rec lift_rec n t k =
  match t with
    | Srt s -> Srt s
    | Ref i -> if le_gt_dec k i then Ref (plus n i) else Ref i
    | Abs (t0, m) -> Abs ((lift_rec n t0 k), (lift_rec n m (S k)))
    | App (u, v) -> App ((lift_rec n u k), (lift_rec n v k))
    | Prod (a, b) -> Prod ((lift_rec n a k), (lift_rec n b (S k)))

(** val lift : nat -> term -> term **)

let lift n t =
  lift_rec n t O

(** val subst_rec : term -> term -> nat -> term **)

let rec subst_rec n m k =
  match m with
    | Srt s -> Srt s
    | Ref i ->
        (match lt_eq_lt_dec k i with
           | Some s -> if s then Ref (pred i) else lift k n
           | None -> Ref i)
    | Abs (a, b) -> Abs ((subst_rec n a k), (subst_rec n b (S k)))
    | App (u, v) -> App ((subst_rec n u k), (subst_rec n v k))
    | Prod (t, u) -> Prod ((subst_rec n t k), (subst_rec n u (S k)))

(** val subst : term -> term -> term **)

let subst n m =
  subst_rec n m O

(** val list_item : 'a1 list -> nat -> 'a1 option **)

let rec list_item e n =
  match e with
    | Nil -> None
    | Cons (h, f) -> (match n with
                        | O -> Some h
                        | S k -> list_item f k)

type env = term list

(** val compute_nf : term -> term sig2 **)

let rec compute_nf = function
  | Srt s -> Srt s
  | Ref n -> Ref n
  | Abs (t, t0) -> Abs ((compute_nf t), (compute_nf t0))
  | App (u, v) ->
      (match compute_nf u with
         | Srt s -> App ((Srt s), (compute_nf v))
         | Ref n -> App ((Ref n), (compute_nf v))
         | Abs (t, b) -> compute_nf (subst (compute_nf v) b)
         | App (u0, v0) -> App ((App (u0, v0)), (compute_nf v))
         | Prod (t, u0) -> App ((Prod (t, u0)), (compute_nf v)))
  | Prod (t, u) -> Prod ((compute_nf t), (compute_nf u))

(** val eqterm : term -> term -> bool **)

let rec eqterm t v0 =
  match t with
    | Srt s ->
        (match v0 with
           | Srt s0 ->
               (match s with
                  | Kind -> (match s0 with
                               | Kind -> true
                               | Prop -> false)
                  | Prop -> (match s0 with
                               | Kind -> false
                               | Prop -> true))
           | _ -> false)
    | Ref n -> (match v0 with
                  | Ref n0 -> eq_nat_dec n n0
                  | _ -> false)
    | Abs (t0, t1) ->
        (match v0 with
           | Abs (t2, t3) -> if eqterm t0 t2 then eqterm t1 t3 else false
           | _ -> false)
    | App (t0, t1) ->
        (match v0 with
           | App (t2, t3) -> if eqterm t0 t2 then eqterm t1 t3 else false
           | _ -> false)
    | Prod (t0, t1) ->
        (match v0 with
           | Prod (t2, t3) -> if eqterm t0 t2 then eqterm t1 t3 else false
           | _ -> false)

(** val is_conv : term -> term -> bool **)

let is_conv u v =
  eqterm (compute_nf u) (compute_nf v)

(** val is_sort : term -> sort option **)

let is_sort = function
  | Srt s -> Some s
  | _ -> None

(** val is_prod : term -> (term, term) prod option **)

let is_prod = function
  | Prod (t0, t1) -> Some (Pair (t0, t1))
  | _ -> None

(** val red_to_sort : term -> sort option **)

let red_to_sort t =
  is_sort (compute_nf t)

(** val red_to_prod : term -> (term, term) prod option **)

let red_to_prod t =
  match is_prod (compute_nf t) with
    | Some x -> let Pair (t0, u) = x in Some (Pair (t0, u))
    | None -> None

(** val infer : env -> term -> term option **)

let rec infer e = function
  | Srt s -> (match s with
                | Kind -> None
                | Prop -> Some (Srt Kind))
  | Ref n ->
      (match list_item e n with
         | Some x -> Some (lift (S n) x)
         | None -> None)
  | Abs (t0, t1) ->
      (match infer e t0 with
         | Some x ->
             (match red_to_sort x with
                | Some x0 ->
                    (match infer (Cons (t0, e)) t1 with
                       | Some x1 ->
                           if eqterm (Srt Kind) x1
                           then None
                           else Some (Prod (t0, x1))
                       | None -> None)
                | None -> None)
         | None -> None)
  | App (t0, t1) ->
      (match infer e t0 with
         | Some x ->
             (match red_to_prod x with
                | Some x0 ->
                    let Pair (v, ur) = x0 in
                    (match infer e t1 with
                       | Some x1 ->
                           if is_conv v x1 then Some (subst t1 ur) else None
                       | None -> None)
                | None -> None)
         | None -> None)
  | Prod (t0, t1) ->
      (match Obj.magic (fun e0 _ -> infer e0 t0) e __ with
         | Some x ->
             (match red_to_sort x with
                | Some x0 ->
                    (match infer (Cons (t0, e)) t1 with
                       | Some x1 ->
                           (match red_to_sort x1 with
                              | Some x2 -> Some (Srt x2)
                              | None -> None)
                       | None -> None)
                | None -> None)
         | None -> None)

(** val check_typ : env -> term -> term -> bool **)

let check_typ e t tp =
  match infer e t with
    | Some x ->
        if eqterm x (Srt Kind)
        then eqterm tp (Srt Kind)
        else (match infer e tp with
                | Some x0 -> is_conv x tp
                | None -> false)
    | None -> false

(** val add_typ : env -> term -> bool **)

let add_typ e t =
  match infer e t with
    | Some x ->
        (match red_to_sort x with
           | Some x0 -> true
           | None -> false)
    | None -> false