From Velus Require Import Common.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import VelusMemory.
From Velus Require Import Obc.ObcSyntax.
From Velus Require Import Obc.ObcSemantics.

From Coq Require Import Morphisms.

From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

Obc typing

Module Type OBCTYPING
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op)
       (Import Syn : OBCSYNTAX Ids Op OpAux)
       (Import Sem : OBCSEMANTICS Ids Op OpAux Syn).

  Section WellTyped.

    Variable p : program.
    Variable insts : list (ident * ident).
    Variable mems : list (ident * type).
    Variable vars : list (ident * type).

    Inductive wt_exp : exp -> Prop :=
    | wt_Var: forall x ty,
        In (x, ty) vars ->
        wt_exp (Var x ty)
    | wt_State: forall x ty,
        In (x, ty) mems ->
        wt_exp (State x ty)
    | wt_Const: forall c,
        wt_exp (Const c)
    | wt_Unop: forall op e ty,
        type_unop op (typeof e) = Some ty ->
        wt_exp e ->
        wt_exp (Unop op e ty)
    | wt_Binop: forall op e1 e2 ty,
        type_binop op (typeof e1) (typeof e2) = Some ty ->
        wt_exp e1 ->
        wt_exp e2 ->
        wt_exp (Binop op e1 e2 ty)
    | wt_Valid: forall x ty,
        In (x, ty) vars ->
        wt_exp (Valid x ty).

    Inductive wt_stmt : stmt -> Prop :=
    | wt_Assign: forall x e,
        In (x, typeof e) vars ->
        wt_exp e ->
        wt_stmt (Assign x e)
    | wt_AssignSt: forall x e,
        In (x, typeof e) mems ->
        wt_exp e ->
        wt_stmt (AssignSt x e)
    | wt_Ifte: forall e s1 s2,
        wt_exp e ->
        typeof e = bool_type ->
        wt_stmt s1 ->
        wt_stmt s2 ->
        wt_stmt (Ifte e s1 s2)
    | wt_Comp: forall s1 s2,
        wt_stmt s1 ->
        wt_stmt s2 ->
        wt_stmt (Comp s1 s2)
    | wt_Call: forall clsid cls p' o f fm ys es,
        In (o, clsid) insts ->
        find_class clsid p = Some(cls, p') ->
        find_method f cls.(c_methods) = Some fm ->
        NoDup ys ->
        Forall2 (fun y xt => In (y, snd xt) vars) ys fm.(m_out) ->
        Forall2 (fun e xt => typeof e = snd xt) es fm.(m_in) ->
        Forall wt_exp es ->
        wt_stmt (Call ys clsid o f es)
    | wt_Skip:
        wt_stmt Skip.

  End WellTyped.

  Definition wt_method (p : program)
                       (insts : list (ident * ident))
                       (mems : list (ident * type))
                       (m : method) : Prop
    := wt_stmt p insts mems (meth_vars m) m.(m_body).

  Definition wt_class (p : program) (cls: class) : Prop
    := (Forall (fun ocls=> find_class (snd ocls) p <> None) cls.(c_objs))
       /\ Forall (wt_method p cls.(c_objs) cls.(c_mems)) cls.(c_methods).

  Inductive wt_program : program -> Prop :=
  | wtp_nil:
      wt_program []
  | wtp_cons: forall cls p,
      wt_class p cls ->
      wt_program p ->
      Forall (fun cls' => cls.(c_name) <> cls'.(c_name)) p ->
      wt_program (cls::p).

  Hint Constructors wt_exp wt_stmt wt_program : obctyping.

  Instance wt_exp_Proper:
    Proper (@Permutation.Permutation (ident * type)
                                     ==> @Permutation.Permutation (ident * type)
                                     ==> @eq exp ==> iff) wt_exp.

  Instance wt_stmt_Proper:
    Proper (@eq program
                ==> @Permutation.Permutation (ident * ident)
                ==> @Permutation.Permutation (ident * type)
                ==> @Permutation.Permutation (ident * type)
                ==> @eq stmt ==> iff) wt_stmt.


  Definition wt_venv_val (ve: venv) (xty: ident * type) :=
    match Env.find (fst xty) ve with
    | None => True
    | Some v => wt_val v (snd xty)
    end.

  Definition wt_env (ve: venv) (vars: list (ident * type)) :=
    Forall (wt_venv_val ve) vars.

  Hint Unfold wt_env.

  Inductive wt_mem : menv -> program -> class -> Prop :=
  | WTmenv: forall me p cl,
      wt_env (values me) cl.(c_mems) ->
      Forall (wt_mem_inst me p) cl.(c_objs) ->
      wt_mem me p cl
  with wt_mem_inst : menv -> program -> (ident * ident) -> Prop :=
  | WTminst_empty: forall me p o c,
      find_inst o me = None ->
      wt_mem_inst me p (o, c)
  | WTminst: forall me p o c mo cls p',
      find_inst o me = Some mo ->
      find_class c p = Some (cls, p') ->
      wt_mem mo p' cls ->
      wt_mem_inst me p (o, c).

  Definition wt_state (p: program) (me: menv) (ve: venv) (c: class) (vars: list (ident * type)) : Prop :=
    wt_mem me p c /\ wt_env ve vars.

  Section wt_mem_mult.

    Variable P : forall me p cl, wt_mem me p cl -> Prop.
    Variable Pinst : forall me p oc, wt_mem_inst me p oc -> Prop.

    Arguments P {me p cl} H.
    Arguments Pinst {me p oc} H.
    Arguments WTmenv {me p cl} Hwt Hinsts.
    Arguments WTminst_empty {me} p {o} c Hfind.
    Arguments WTminst {me p o c mo cls p'} Hinst Hclass Hwt.

    Hypothesis WTmenvCase:
      forall me p cl
        (x : wt_env (values me) cl.(c_mems))
        (ys : Forall (wt_mem_inst me p) cl.(c_objs)),
        Forall (fun cl => exists H, @Pinst me p cl H) cl.(c_objs) ->
        @P me p cl (WTmenv x ys).

    Hypothesis WTminst_emptyCase:
      forall me p o c
        (Hfind: find_inst o me = None),
        Pinst (WTminst_empty p c Hfind).

    Hypothesis WTminstCase:
      forall me p o c mo cls p'
        (Hfind_inst: find_inst o me = Some mo)
        (Hfind_class: find_class c p = Some (cls, p'))
        (Hwt: wt_mem mo p' cls),
        P Hwt ->
        Pinst (WTminst Hfind_inst Hfind_class Hwt).

    Fixpoint wt_mem_ind_mult {me p cl} (H: wt_mem me p cl) {struct H} : P H
    with wt_mem_inst_ind_mult {me p oc} (H: wt_mem_inst me p oc) {struct H}: Pinst H.
    -
      destruct H as [? ? ? Hwt Hrec].
      apply WTmenvCase.
      induction Hrec as [| ? ? Hwt' Hrec' ]; constructor; auto.
      exists Hwt'; auto.
    -
      destruct H;
        clear wt_mem_inst_ind_mult;
        auto using WTminst_emptyCase, WTminstCase.
    Qed.