Require Import List.

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

Require WellFormedness.
Module My_WellFormedness := WellFormedness.SetProgram(My_Program).

Import My_WellFormedness.
Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.

Inductive evaluated_term: Term -> Prop :=

  | evaluated_new:
    forall (N: TypeS) (fvs: Term),
      (evaluated_term fvs) ->
      (evaluated_term (Term_new N fvs))



  | evaluated_term_nil:
    (evaluated_term Term_nil)

  | evaluated_term_cons:
    forall (v: Term) (vs: Term),
      (evaluated_term v) ->
      (evaluated_term vs) ->
      (evaluated_term (Term_cons v vs))



  | evaluated_fieldTerm_nil:
    (evaluated_term FieldTerm_nil)

  | evaluated_fieldTerm_cons:
    forall (f: FieldSym) (v: Term) (fvs: Term),
      (evaluated_term v) ->
      (evaluated_term fvs) ->
      (evaluated_term (FieldTerm_cons f v fvs))
.

Inductive fieldTerm_lookup: Term -> FieldSym -> Term -> Prop :=

  | fieldTerm_lookup_head:
    forall (f: FieldSym) (t: Term) (fts: Term),
      (fieldTerm_lookup (FieldTerm_cons f t fts) f t)
      
  | fieldTerm_lookup_tail:
    forall (f f': FieldSym) (t t': Term) (fts: Term),
      (fieldTerm_lookup fts f t) ->
      (fieldTerm_lookup (FieldTerm_cons f' t' fts) f t)
.

Fixpoint polyTermSubst_in_term (t: Term) (k: nat) (ts: (list Term)) {struct ts}: Term :=
  match ts with
    | nil => t
    | (u :: us) => (polyTermSubst_in_term (termSubst_in_term t (k + (length us)) u) k us)
  end
.

Fixpoint list_of_termList (ts': Term): (list Term) :=
  match ts' with
    | Term_nil => nil
    | (Term_cons t ts) => t :: (list_of_termList ts)
    | _ => nil
  end
.

Inductive RedTerm: Term -> Term -> Prop :=

  | R_select_redex:
    forall (N: TypeS) (v fvs: Term) (f: FieldSym),
      
      (fieldTerm_lookup fvs f v) ->
      
      (RedTerm (Term_select (Term_new N fvs) f) v)

  | R_call_redex:
    forall (vs fvs t: Term) (m: MethodSym) (N R R': TypeS) (C: ClassSym),
      let v := (Term_new N fvs) in


      (Class_subtyping N (Class_type C R')) ->
      (methodImpl m C) = (Some t) ->
      let u := (typeSubst_in_term (typeSubst_in_term t 1 R') 0 R) in

      let u' := (polyTermSubst_in_term u 0 (v :: (list_of_termList vs))) in
      
      (RedTerm (Term_call v m R vs) u')

  | R_select:
    forall (t t': Term) (f: FieldSym),
      (RedTerm t t') ->
      
      (RedTerm (Term_select t f) (Term_select t' f))

  | R_call_left:
    forall (t t' ts: Term) (m: MethodSym) (R: TypeS),
      (RedTerm t t') ->
      
      (RedTerm (Term_call t m R ts) (Term_call t' m R ts))

  | R_call_right:
    forall (t ts ts': Term) (m: MethodSym) (R: TypeS),
      (RedTerm ts ts') ->
      
      (RedTerm (Term_call t m R ts) (Term_call t m R ts'))

  | R_new:
    forall (N: TypeS) (fts fts': Term),
      (RedTerm fts fts') ->
      
      (RedTerm (Term_new N fts) (Term_new N fts'))



  | R_cons_left:
    forall (t t' ts: Term),
      (RedTerm t t') ->
      
      (RedTerm (Term_cons t ts) (Term_cons t' ts))

  | R_cons_right:
    forall (t ts ts': Term),
      (RedTerm ts ts') ->
      
      (RedTerm (Term_cons t ts) (Term_cons t ts'))


  
  | R_fieldTerm_cons_left:
    forall (f: FieldSym) (t t' fts: Term),
      (RedTerm t t') ->
      
      (RedTerm (FieldTerm_cons f t fts) (FieldTerm_cons f t' fts))

  | R_fieldTerm_cons_right:
    forall (f: FieldSym) (t fts fts': Term),
      (RedTerm fts fts') ->
      
      (RedTerm (FieldTerm_cons f t fts) (FieldTerm_cons f t fts'))
.

Inductive Evaluate: Term -> Term -> Prop :=

  | Evaluate_end:
    forall (v: Term),
      (evaluated_term v) ->
      (Evaluate v v)

  | Evaluate_step:
    forall (t u v: Term),
      (RedTerm t u) ->
      (Evaluate u v) ->
      (Evaluate t v)
.

Definition EvaluateMain (v: Term): Prop :=
  (Evaluate mainTerm v)
.

End SetProgram.