Require Import List.
Require Import Arith.

Require Import MatchCompNat.

Require Syntax.
Module SetProgram(My_Program: Syntax.Program).

Import My_Program.

Require Binders.
Module My_Binders := Binders.SetProgram(My_Program).

Import My_Binders.

Lemma Var_eqdec:
  forall (x y: Var), { x = y } + { x <> y }
.

Definition termSubst_in_var (x: Var) (i: nat) (u: Term): Term :=
  (match_comp_nat3 x i _
    (Term_var x)
    (lift_in_term u i)
    (Term_var (pred x))
  )
.

Fixpoint termSubst_in_term (t': Term) (x: nat) (u: Term) {struct t'} : Term :=
  match t' with
  | (Term_var i) => (termSubst_in_var i x u)
  | (Term_select t f) => (Term_select (termSubst_in_term t x u) f)
  | (Term_call t m R ts) => (Term_call (termSubst_in_term t x u) m R
                                           (termSubst_in_term ts x u))
  | (Term_new T fts) => (Term_new T (termSubst_in_term fts x u))
  | Term_nil => Term_nil
  | (Term_cons t ts) => (Term_cons (termSubst_in_term t x u)
                                           (termSubst_in_term ts x u))
  | FieldTerm_nil => FieldTerm_nil
  | (FieldTerm_cons f t fts) => (FieldTerm_cons f (termSubst_in_term t x u)
                                                  (termSubst_in_term fts x u))
  end
.

Definition typeSubst_in_typeVar (X: TypeVar) (s: nat) (R: TypeS): TypeS :=
  (match_comp_nat3 X s TypeS
    (Type_var X)
    (lift_in_type R s)
    (Type_var (pred X))
  )
.

Fixpoint typeSubst_in_type (t: TypeS) (X: nat) (R: TypeS) {struct t} : TypeS :=
  match t with
    
    | (Type_proj R' i) => (Type_proj (typeSubst_in_type R' X R) i)
    | (Type_class C) => (Type_class C)
    | (Type_fun Pi T) => (Type_fun (typeSubst_in_type Pi X R) (typeSubst_in_type T (S X) R))
    
    | (Type_apply K R') => (Type_apply (typeSubst_in_type K X R) (typeSubst_in_type R' X R))
    
    | (Type_var Y) => (typeSubst_in_typeVar Y X R)
    | (Type_tuple Ks) => (Type_tuple (typeSubst_in_type Ks X R))
    
    | (Type_param Pi T) => (Type_param (typeSubst_in_type Pi X R) (typeSubst_in_type T (S X) R))
    
    | (Type_section Ps) => (Type_section (typeSubst_in_type Ps (S X) R))
    
    | Type_none => Type_none
    | (Type_some T) => (Type_some (typeSubst_in_type T X R))
    
    | Type_nil => Type_nil
    | (Type_cons u us) => (Type_cons (typeSubst_in_type u X R) (typeSubst_in_type us X R))
  end
.

Fixpoint typeSubst_in_typeEnv (D: TypeEnv) (X: TypeVar) (R: TypeS) {struct D} : TypeEnv :=
  match D with
    | nil => nil
    | (Pi :: D') => (typeSubst_in_type Pi X R) :: (typeSubst_in_typeEnv D' (S X) R)
  end
.

Fixpoint typeSubst_in_term (t': Term) (X: nat) (R: TypeS) {struct t'} : Term :=
  match t' with
  | (Term_var i) => (Term_var i)
  | (Term_select t f) => (Term_select (typeSubst_in_term t X R) f)
  | (Term_call t m R' ts) => (Term_call (typeSubst_in_term t X R) m
                                           (typeSubst_in_type R' X R)
                                           (typeSubst_in_term ts X R))
  | (Term_new T ts) => (Term_new (typeSubst_in_type T X R)
                                          (typeSubst_in_term ts X R))
  | Term_nil => Term_nil
  | (Term_cons t ts) => (Term_cons (typeSubst_in_term t X R)
                                           (typeSubst_in_term ts X R))
  | FieldTerm_nil => FieldTerm_nil
  | (FieldTerm_cons f t fts) => (FieldTerm_cons f (typeSubst_in_term t X R)
                                                  (typeSubst_in_term fts X R))
  end
.


End SetProgram.