Set Implicit Arguments.

Require Import RelExtras.
Require Import ListExtras.
Require Import TermsSig.
Require Import Setoid.

Module TermsDef (Sig : Signature).

  Export Sig.

  Fixpoint TypeEq (A B: SimpleType) { struct A } : Prop :=
  match A, B with
  | A1-->A2, B1-->B2 ⇒ TypeEq A1 B1 ∧ TypeEq A2 B2
  | #_, #_ ⇒ True
  | _, _ ⇒ False
  end.

  Notation "A == B" := (TypeEq A B) (at level 50).
  Hint Unfold TypeEq : terms.

  Definition isArrowType (A: SimpleType) : Prop :=
    match A with
    | _ --> _ ⇒ True
    | _ ⇒ False
    end.

  Definition isBaseType (A: SimpleType) : Prop :=
    match A with
    | #b ⇒ True
    | _ ⇒ False
    end.

  Hint Unfold isArrowType isBaseType : terms.

  Definition type_left (A: SimpleType) : SimpleType :=
     match A with
     | #b ⇒ #b
     | A1 --> A2 ⇒ A1
     end.

  Definition type_right (A: SimpleType) : SimpleType :=
    match A with
    | #b ⇒ #b
    | A1 --> A2 ⇒ A2
    end.

  Lemma type_eq_equiv : ∀ A B, A = B → A == B.

  Proof.
    induction A; intros; rewrite <- H; simpl; auto.
  Qed.
  Hint Resolve type_eq_equiv : terms.

  Definition Env := list (option SimpleType).
  Definition EmptyEnv : Env := nil.
  Implicit Type x y : nat.
  Implicit Type E : Env.

  Definition VarD E x A := nth_error E x = Some (Some A).
  Definition VarUD E x := nth_error E x = None ∨
                          nth_error E x = Some None.
  Notation "E |= x := A" := (VarD E x A) (at level 60).
  Notation "E |= x :!" := (VarUD E x) (at level 60).

  Definition decl A E := Some A::E.
  Infix "[#]" := decl (at level 20, right associativity).
  Definition declDummy E := None::E.
  Hint Unfold VarD VarUD decl declDummy EmptyEnv : terms.

  Inductive Preterm : Type :=
   | Var(x: nat)
   | Fun(f: FunctionSymbol)
   | Abs(A: SimpleType)(M: Preterm)
   | App(M N: Preterm).

  Implicit Type Pt : Preterm.
  Notation "^ f" := (Fun f) (at level 20).
  Notation "% x" := (Var x) (at level 20).
  Infix "@@" := App (at level 25, left associativity).
  Notation "s [ x ]" := (s @@ x) (at level 50).
  Notation "s [ x , y ]" := (s @@ x @@ y) (at level 50).
  Notation "s [ x , y , z ]" := (s @@ x @@ y @@ z) (at level 50).
  Notation "s [ x , y , z , w ]" := (s @@ x @@ y @@ z @@ w)
    (at level 50).
  Notation "s [ x , y , z , w , v ]" := (s @@ x @@ y @@ z @@ w @@ v)
    (at level 50).
  Notation "\ A => M" := (Abs A M) (at level 35).

  Reserved Notation "E |- Pt := A" (at level 60).
  Inductive Typing : Env → Preterm → SimpleType → Type :=
  | TVar: ∀ E x A,
            E |= x := A →
            E |- %x := A
  | TFun: ∀ E f,
            E |- ^f := f_type f
  | TAbs: ∀ E A B Pt,
            A [#] E |- Pt := B →
            E |- \A ⇒ Pt := A --> B
  | TApp: ∀ E A B PtL PtR,
            E |- PtL := A --> B →
            E |- PtR := A →
            E |- PtL @@ PtR := B
  where "E |- Pt := A" := (Typing E Pt A).

  Hint Constructors Typing : terms.
  Hint Extern 5 (?X1 |- %?X2 := ?X3) ⇒
         (apply TVar; auto with terms) : terms.
  Hint Extern 5 (?X1 |- ^?X2 := ?X3) ⇒
         (apply TFun with (f := X2); auto with terms) : terms.
  Hint Extern 5 (?X1 |- \?X2 ⇒ ?X3 := ?X4) ⇒
         (apply TAbs; auto with terms) : terms.

  Record Term : Type := buildT {
    env: Env;
    term: Preterm;
    type: SimpleType;
    typing: Typing env term type
  }.
  Implicit Types M N T : Term.
  Definition TermTyping M : Type := Typing M.(env) M.(term) M.(type).

  Ltac term_inv X :=
     let env := fresh "E"
     with term := fresh "Pt"
     with termL := fresh "PtL"
     with termR := fresh "PtR"
     with type := fresh "A"
     with type' := fresh "B"
     with typing := fresh "T"
     with name := fresh "Tr"
     with var := fresh "x"
     with funS := fresh "f"
     in (
       first [intros until X | idtac];
       set (name := X) in *;
       destruct X as [env term type typing];
       destruct typing as [ env var type typing
                          | env funS
                          | env type type' term typing
                          | env type type' termL termR
                          ];
       try_solve
     ).

  Ltac term_type_inv X :=
     let env := fresh "E"
     with term := fresh "Pt"
     with type := fresh "A"
     with typing := fresh "Typ"
     in (
       first [simpl in X | intros until X];
       destruct X as [env term type typing];
       destruct type;
       try_solve
     ).

End TermsDef.