Library MetaCoq.Erasure.EAstUtils

Fixpoint decompose_app_rec t l :=
  match t with
  | tApp f a ⇒ decompose_app_rec f (a :: l)
  | f ⇒ (f, l)
  end.

Definition decompose_app f := decompose_app_rec f [].

Lemma decompose_app_rec_mkApps f l l' :
  decompose_app_rec (mkApps f l) l' = decompose_app_rec f (l ++ l').

Lemma decompose_app_mkApps f l :
  isApp f = false → decompose_app (mkApps f l) = (f, l).

Lemma mkApps_app t l l' : mkApps t (l ++ l') = mkApps (mkApps t l) l'.

Lemma mkApps_nested f l l' : mkApps (mkApps f l) l' = mkApps f (l ++ l').

Lemma decompose_app_rec_inv {t l' f l} :
  decompose_app_rec t l' = (f, l) →
  mkApps t l' = mkApps f l.

Lemma decompose_app_inv {t f l} :
  decompose_app t = (f, l) → t = mkApps f l.

Lemma nApp_decompose_app t l : ~~ isApp t → decompose_app_rec t l = pair t l.

Lemma mkApps_eq_decompose_app_rec {f args t l} :
  mkApps f args = t →
  ~~ isApp f →
  match decompose_app_rec t l with
  | (f', args') ⇒ f' = f ∧ mkApps t l = mkApps f' args'
  end.

Lemma decompose_app_eq_right t l l' : decompose_app_rec t l = decompose_app_rec t l' → l = l'.

Lemma mkApps_eq_right t l l' : mkApps t l = mkApps t l' → l = l'.

Lemma mkApps_eq_decompose' {f args t} :
  mkApps f args = t →
  ~~ isApp f →
  match decompose_app t with
  | (f', args') ⇒ f' = f ∧ args' = args ∧ t = mkApps f' args'
  end.

Lemma decompose_app_rec_notApp :
  ∀ t l u l',
    decompose_app_rec t l = (u, l') →
    ~~ isApp u.

Lemma decompose_app_notApp :
  ∀ t u l,
    decompose_app t = (u, l) →
    ~~ isApp u.

Inductive mkApps_spec : term → list term → term → list term → term → Type :=
| mkApps_intro f l n :
    ~~ isApp f →
    mkApps_spec f l (mkApps f (firstn n l)) (skipn n l) (mkApps f l).

Lemma decompose_app_rec_eq f l :
  ~~ isApp f →
  decompose_app_rec f l = (f, l).

Lemma firstn_add {A} x y (args : list A) : firstn (x + y) args = firstn x args ++ firstn y (skipn x args).

Lemma decompose_app_rec_inv' f l hd args :
  decompose_app_rec f l = (hd, args) →
  ∑ n, ~~ isApp hd ∧ l = skipn n args ∧ f = mkApps hd (firstn n args).

Lemma mkApps_elim_rec t l l' :
  let app' := decompose_app_rec (mkApps t l) l' in
  mkApps_spec app'.1 app'.2 t (l ++ l') (mkApps t (l ++ l')).

Lemma mkApps_elim t l :
  let app' := decompose_app (mkApps t l) in
  mkApps_spec app'.1 app'.2 t l (mkApps t l).

Lemma mkApps_eq_inj {t t' l l'} :
  mkApps t l = mkApps t' l' →
  ~~ isApp t → ~~ isApp t' → t = t' ∧ l = l'.


Definition isEvar t :=
  match t with
  | tEvar _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isFix t :=
  match t with
  | tFix _ _ ⇒ true
  | _ ⇒ false
  end.

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

Definition isConstruct t :=
  match t with
  | tConstruct _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isBox t :=
  match t with
  | tBox ⇒ true
  | _ ⇒ false
  end.


Definition string_of_def {A : Set} (f : A → string) (def : def A) :=
  "(" ++ string_of_name (dname def) ++ "," ++ f (dbody def) ++ ","
      ++ string_of_nat (rarg def) ++ ")".

Fixpoint string_of_term (t : term) : string :=
  match t with
  | tBox ⇒ "∎"
  | tRel n ⇒ "Rel(" ++ string_of_nat n ++ ")"
  | tVar n ⇒ "Var(" ++ n ++ ")"
  | tEvar ev args ⇒ "Evar(" ++ string_of_nat ev ++ "[]" ++ ")"
  | tLambda na t ⇒ "Lambda(" ++ string_of_name na ++ "," ++ string_of_term t ++ ")"
  | tLetIn na b t ⇒ "LetIn(" ++ string_of_name na ++ "," ++ string_of_term b ++ "," ++ string_of_term t ++ ")"
  | tApp f l ⇒ "App(" ++ string_of_term f ++ "," ++ string_of_term l ++ ")"
  | tConst c ⇒ "Const(" ++ c ++ ")"
  | tConstruct i n ⇒ "Construct(" ++ string_of_inductive i ++ "," ++ string_of_nat n ++ ")"
  | tCase (ind, i) t brs ⇒
    "Case(" ++ string_of_inductive ind ++ "," ++ string_of_nat i ++ "," ++ string_of_term t ++ ","
            ++ 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.