Module Equiv

From Coq Require Import FSets.FMapPositive.
From Coq Require Import PArith.
From Velus Require Import Common.
From Velus Require Import CommonTyping.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import Obc.ObcSyntax.
From Velus Require Import Obc.ObcSemantics.
From Velus Require Import Obc.ObcTyping.

From Coq Require Import Relations.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.

Import List.

Equivalence of Obc programs


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

  Definition stmt_eval_eq s1 s2: Prop :=
    forall prog menv env menv' env',
      stmt_eval prog menv env s1 (menv', env')
      <->
      stmt_eval prog menv env s2 (menv', env').

  Lemma stmt_eval_eq_refl:
    reflexive stmt stmt_eval_eq.
  Proof.

  Lemma stmt_eval_eq_sym:
    symmetric stmt stmt_eval_eq.
  Proof.

  Lemma stmt_eval_eq_trans:
    transitive stmt stmt_eval_eq.
  Proof.

  Add Relation stmt (stmt_eval_eq)
      reflexivity proved by stmt_eval_eq_refl
      symmetry proved by stmt_eval_eq_sym
      transitivity proved by stmt_eval_eq_trans
        as stmt_eval_equiv.

  Global Instance stmt_eval_eq_Proper:
    Proper (eq ==> eq ==> eq ==> stmt_eval_eq ==> eq ==> iff) stmt_eval.
  Proof.

  Global Instance stmt_eval_eq_Comp_Proper:
    Proper (stmt_eval_eq ==> stmt_eval_eq ==> stmt_eval_eq) Comp.
  Proof.

  Lemma Comp_assoc:
    forall s1 s2 s3,
      stmt_eval_eq (Comp s1 (Comp s2 s3)) (Comp (Comp s1 s2) s3).
  Proof.

  Lemma stmt_eval_eq_Comp_Skip1:
    forall s, stmt_eval_eq (Comp Skip s) s.
  Proof.

  Lemma stmt_eval_eq_Comp_Skip2:
    forall s, stmt_eval_eq (Comp s Skip) s.
  Proof.

  Global Instance stmt_eval_eq_Switch_Proper:
    Proper (eq ==> Forall2 (orel stmt_eval_eq) ==> stmt_eval_eq ==> stmt_eval_eq) Switch.
  Proof.

A refinement relation for Obc. Refining programs are allowed to replace None by any value.

  Import Env.Notations.

  Lemma exp_eval_refines:
    forall menv' env1 env2 e v,
      env2env1 ->
      exp_eval menv' env2 e (Some v) ->
      exp_eval menv' env1 e (Some v).
  Proof.

  Lemma exp_eval_refines':
    forall menv env1 env2 e vo,
      env2env1 ->
      exp_eval menv env2 e vo ->
      exists vo', exp_eval menv env1 e vo' /\ (forall v, vo = Some v -> vo' = Some v).
  Proof.

  Lemma Forall2_exp_eval_refines':
    forall menv env1 env2 es vos,
      env2env1 ->
      Forall2 (exp_eval menv env2) es vos ->
      exists vos',
        Forall2 (exp_eval menv env1) es vos'
        /\ Forall2 (fun vo vo' => forall v, vo = Some v -> vo' = Some v) vos vos'.
  Proof.


  Definition stmt_refines prog1 prog2 P s1 s2 : Prop :=
    forall menv env1 env2 menv' env2',
      P env1 env2 ->
      env2env1 ->
      stmt_eval prog2 menv env2 s2 (menv', env2') ->
      (exists env1',
          env2' ⊑ env1'
          /\ stmt_eval prog1 menv env1 s1 (menv', env1')).

  Definition method_refines prog1 prog2 P m1 m2 : Prop :=
    m1.(m_in) = m2.(m_in)
    /\ m1.(m_out) = m2.(m_out)
    /\ stmt_refines prog1 prog2 (P m1.(m_in)) m1.(m_body) m2.(m_body).

  Definition class_refines prog1 prog2 P c1 c2 : Prop :=
    forall f m2,
      find_method f c2.(c_methods) = Some m2 ->
      exists m1,
        find_method f c1.(c_methods) = Some m1
        /\ method_refines prog1 prog2 (P f) m1 m2.

  Definition ltsuffix2_prog := rr ltsuffix_prog ltsuffix_prog.

  Lemma ltsuffix2_prog_wf: well_founded ltsuffix2_prog.
  Proof.

  Definition program_refines
             (P : ident -> ident -> list (ident * type)
                  -> Env.t value -> Env.t value -> Prop)
             (prog1 prog2 : program) : Prop :=
    (PFix ltsuffix2_prog_wf
          (fun (progs : program * program)
               (program_refines :
                  (forall (progs' : program * program),
                      ltsuffix2_prog progs' progs -> Prop)) =>
             (fst progs).(types) = (snd progs).(types)
             /\ (fst progs).(externs) = (snd progs).(externs)
             /\
             forall n c2 prog2'
               (Hf2: find_class n (snd progs) = Some (c2, prog2')),
             exists (c1 : class) (prog1' : program)
               (Hf1: find_class n (fst progs) = Some (c1, prog1')),
               class_refines prog1' prog2' (P n) c1 c2
               /\ program_refines (prog1', prog2')
                                 (conj (find_unit_ltsuffix_prog n (fst progs) c1 prog1' Hf1)
                                       (find_unit_ltsuffix_prog n (snd progs) c2 prog2' Hf2))
    )) (prog1, prog2).

  Lemma program_refines_def:
    forall (P : ident -> ident -> list (ident * type)
                -> Env.t value -> Env.t value -> Prop) prog1 prog2,
      program_refines P prog1 prog2 <->
      (prog1.(types) = prog2.(types)
       /\ prog1.(externs) = prog2.(externs)
       /\ forall n c2 prog2',
          find_class n prog2 = Some (c2, prog2') ->
          exists (c1 : class) (prog1' : program),
            find_class n prog1 = Some (c1, prog1')
            /\ class_refines prog1' prog2' (P n) c1 c2
            /\ program_refines P prog1' prog2').
  Proof.


  Lemma program_refines_by_class':
    forall (Pc : class -> class -> Prop) P p1 p2,
      wt_program p2 ->
      p1.(types) = p2.(types) ->
      p1.(externs) = p2.(externs) ->
      Forall2 (fun c1 c2 => forall p1' p2',
                   wt_program p2' ->
                   wt_class p2' c2 ->
                   program_refines P p1' p2' ->
                   Forall2 Pc p1'.(classes) p2'.(classes) ->
                   Pc c1 c2 ->
                   c1.(c_name) = c2.(c_name)
                   /\ class_refines p1' p2' (P c1.(c_name)) c1 c2) p1.(classes) p2.(classes) ->
      Forall2 Pc p1.(classes) p2.(classes) ->
      program_refines P p1 p2.
  Proof.

  Lemma stmt_refines_strengthen:
    forall P Q p1 p2 s1 s2,
      stmt_refines p1 p2 P s1 s2 ->
      (forall env1 env2, Q env1 env2 -> P env1 env2) ->
      stmt_refines p1 p2 Q s1 s2.
  Proof.

  Global Instance stmt_refines_Proper:
    Proper (eq ==> eq ==>
               pointwise_relation _
               (pointwise_relation _ (Basics.flip Basics.impl))
               ==> eq ==> eq ==> Basics.impl) stmt_refines.
  Proof.

  Lemma program_refines_stmt_call_eval:
    forall P p1 p2 omenv omenv' clsid f vos vos' rvos,
      program_refines P p1 p2 ->
      (forall cls prog' m,
          find_class clsid p2 = Some (cls, prog') ->
          find_method f cls.(c_methods) = Some m ->
          length vos = length m.(m_in) ->
          length vos' = length m.(m_in) ->
          P clsid f m.(m_in) (Env.adds_opt (map fst m.(m_in)) vos' vempty)
                             (Env.adds_opt (map fst m.(m_in)) vos vempty)) ->
      stmt_call_eval p2 omenv clsid f vos omenv' rvos ->
      Forall2 (fun vo vo' => forall v, vo = Some v -> vo' = Some v) vos vos' ->
      exists rvos',
        stmt_call_eval p1 omenv clsid f vos' omenv' rvos'
        /\ Forall2 (fun vo' vo => forall v, vo = Some v -> vo' = Some v) rvos' rvos.
  Proof.

  Lemma wt_exp_program_refines:
    forall P p1 p2 mems vars e,
      program_refines P p1 p2 ->
      wt_exp p2 mems vars e ->
      wt_exp p1 mems vars e.
  Proof.

  Lemma wt_stmt_program_refines:
    forall P p1 p2 insts mems vars s,
      program_refines P p1 p2 ->
      wt_stmt p2 insts mems vars s ->
      wt_stmt p1 insts mems vars s.
  Proof.

  Lemma program_refines_types:
    forall P p1 p2,
      program_refines P p1 p2 ->
      types p1 = types p2.
  Proof.

  Lemma program_refines_externs:
    forall P p1 p2,
      program_refines P p1 p2 ->
      externs p1 = externs p2.
  Proof.

End EQUIV.

Module EquivFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Syn : OBCSYNTAX Ids Op OpAux)
       (ComTyp: COMMONTYPING Ids Op OpAux)
       (Sem : OBCSEMANTICS Ids Op OpAux Syn)
       (Typ : OBCTYPING Ids Op OpAux Syn ComTyp Sem)
  <: EQUIV Ids Op OpAux Syn ComTyp Sem Typ.
  Include EQUIV Ids Op OpAux Syn ComTyp Sem Typ.
End EquivFun.