Module ILCorrectness

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

From Velus Require Import Common.
From Velus Require Import Operators Environment.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Clocks.
From Velus Require Import CoindStreams IndexedStreams.
From Velus Require Import CoindIndexed.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LOrdered Lustre.LTyping Lustre.LClocking Lustre.LSemantics Lustre.LClockedSemantics.
From Velus Require Import Lustre.InlineLocal.InlineLocal Lustre.InlineLocal.ILTyping Lustre.InlineLocal.ILClocking.
From Velus Require Import Lustre.SubClock.SCCorrectness.

Module Type ILCORRECTNESS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Ty : LTYPING Ids Op OpAux Cks Senv Syn)
       (Import Cl : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Import Ord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Ord CStr)
       (Import LCS : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Cl Ord CStr Sem)
       (Import IL : INLINELOCAL Ids Op OpAux Cks Senv Syn).

  Module Import SCT := SCCorrectnessFun Ids Op OpAux Cks CStr Senv Syn Cl Ord Sem LCS SC. Import SC.

  Module Typing := ILTypingFun Ids Op OpAux Cks Senv Syn Ty IL.
  Module Clocking := ILClockingFun Ids Op OpAux Cks Senv Syn Cl IL.

  Fact mask_hist_sub sub : forall k r H H',
      (forall x y vs, Env.find x sub = Some y -> sem_var H (Var x) vs -> sem_var H' (Var y) vs) ->
      forall x y vs, Env.find x sub = Some y -> sem_var (mask_hist k r H) (Var x) vs -> sem_var (mask_hist k r H') (Var y) vs.
  Proof.

  Fact mask_hist_nsub (sub : Env.t ident) : forall k r H H',
      (forall x vs, Env.find x sub = None -> sem_var H (Var x) vs -> sem_var H' (Var x) vs) ->
      forall x vs, Env.find x sub = None -> sem_var (mask_hist k r H) (Var x) vs -> sem_var (mask_hist k r H') (Var x) vs.
  Proof.

  Import List.

  Fact find_snd_spec {A} : forall (locs : list (ident * A)) (locs' : list ident) x y,
      NoDup locs' ->
      In (x, y) (combine (map fst locs) locs') ->
      find (fun '(_, y') => Var y' ==b Var y) (combine (map fst locs) locs') = Some (x, y).
  Proof.

  Section inlinelocal_node_sem.
    Variable G1 : @global noswitch switch_prefs.
    Variable G2 : @global nolocal local_prefs.

    Hypothesis HGref : global_sem_refines G1 G2.
    Hypothesis HwG1 : wc_global G1.

    Fact InMembers_sub {A} : forall (sub : Env.t ident) (xs : list (ident * A)) x,
        InMembers x (map_filter (fun '(x, vs) => option_map (fun y : ident => (y, vs)) (Env.find x sub)) xs) ->
        exists y, Env.MapsTo y x sub.
    Proof.

    Fact InMembers_sub_iff {A} : forall (sub : Env.t ident) (xs : list (ident * A)) x,
        InMembers x (map_filter (fun '(x, vs) => option_map (fun y : ident => (y, vs)) (Env.find x sub)) xs) <->
        exists y, InMembers y xs /\ Env.MapsTo y x sub.
    Proof.

    Fact NoDupMembers_sub {A} : forall (sub : Env.t ident) (xs : list (ident * A)),
        NoDupMembers xs ->
        NoDup (map snd (Env.elements sub)) ->
        NoDupMembers (map_filter (fun '(x, vs) => option_map (fun y => (y, vs)) (Env.find x sub)) xs).
    Proof.

Induction on blocks

    Import Permutation.

    Local Hint Resolve InMembers_incl : datatypes.
    Local Hint Resolve <- fst_InMembers InMembers_idck InMembers_idty : datatypes.
    Local Hint Resolve -> fst_InMembers InMembers_idck InMembers_idty : datatypes.

    Fact mmap_inlinelocal_block_sem : forall Γ blks sub Γ' Γ'' locs' blks' st st' bs Hi1 Hi2,
        Forall
          (fun blk => forall sub Γ' Γ'' locs' blks' st st' bs Hi1 Hi2,
               (forall x, ~IsLast (Γ++Γ'++Γ'') x) ->
               (forall x, IsVar Γ x -> ~IsVar Γ' x) ->
               (forall x, Env.In x sub <-> IsVar Γ' x) ->
               (forall x y, Env.MapsTo x y sub -> InMembers y Γ' \/ exists n hint, y = gensym local hint n) ->
               (forall x y vs, Env.find x sub = Some y -> sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var y) vs) ->
               (forall x vs, IsVar Γ x -> sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var x) vs) ->
               NoDupMembers (Γ++Γ') ->
               noswitch_block blk ->
               NoDupLocals (map fst Γ++map fst Γ'++map fst Γ'') blk ->
               Forall (AtomOrGensym switch_prefs) (map fst Γ) ->
               GoodLocals switch_prefs blk ->
               dom_ub Hi1 (Γ++Γ') ->
               sem_block_ck G1 Hi1 bs blk ->
               dom Hi2 (Γ++Γ'') ->
               sc_vars (Γ++Γ'') Hi2 bs ->
               st_valid st ->
               Forall (fun x => st_In x st) (map fst (Γ ++ Γ'')) ->
               inlinelocal_block sub blk st = (locs', blks', st') ->
               exists Hi3,
                 Hi2Hi3 /\
                 dom Hi3 (Γ++Γ''++senv_of_anns locs') /\
                 sc_vars (Γ++Γ''++senv_of_anns locs') Hi3 bs /\
                 Forall (sem_block_ck G2 Hi3 bs) blks')
          blks ->
        (forall x, ~IsLast (Γ++Γ'++Γ'') x) ->
        (forall x, IsVar Γ x -> ~IsVar Γ' x) ->
        (forall x, Env.In x sub <-> IsVar Γ' x) ->
        (forall x y, Env.MapsTo x y sub -> InMembers y Γ' \/ exists n hint, y = gensym local hint n) ->
        (forall x y vs, Env.find x sub = Some y -> sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var y) vs) ->
        (forall x vs, IsVar Γ x -> sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var x) vs) ->
        NoDupMembers (Γ++Γ') ->
        Forall noswitch_block blks ->
        Forall (NoDupLocals (map fst Γ++map fst Γ'++map fst Γ'')) blks ->
        Forall (AtomOrGensym switch_prefs) (map fst Γ) ->
        Forall (GoodLocals switch_prefs) blks ->
        dom_ub Hi1 (Γ++Γ') ->
        Forall (sem_block_ck G1 Hi1 bs) blks ->
        dom Hi2 (Γ++Γ'') ->
        sc_vars (Γ++Γ'') Hi2 bs ->
        st_valid st ->
        Forall (fun x => st_In x st) (map fst (Γ ++ Γ'')) ->
        mmap2 (inlinelocal_block sub) blks st = (locs', blks', st') ->
        exists Hi3,
          Hi2Hi3 /\
          dom Hi3 (Γ++Γ''++senv_of_anns (concat locs')) /\
          sc_vars (Γ++Γ''++senv_of_anns (concat locs')) Hi3 bs /\
          Forall (sem_block_ck G2 Hi3 bs) (concat blks').
    Proof with

    Ltac inv_scope :=
      (Syn.inv_scope || Ty.inv_scope || Cl.inv_scope || Sem.inv_scope || LCS.inv_scope).

Central correctness lemma
    Lemma inlinelocal_block_sem Γ : forall blk sub Γ' Γ'' locs' blks' st st' bs Hi1 Hi2,
        (forall x, ~IsLast (Γ++Γ'++Γ'') x) ->
        (forall x, IsVar Γ x -> ~IsVar Γ' x) ->
        (forall x, Env.In x sub <-> IsVar Γ' x) ->
        (forall x y, Env.MapsTo x y sub -> InMembers y Γ' \/ exists n hint, y = gensym local hint n) ->
        (forall x y vs, Env.find x sub = Some y -> sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var y) vs) ->
        (forall x vs, IsVar Γ x -> sem_var Hi1 (Var x) vs -> sem_var Hi2 (Var x) vs) ->
        NoDupMembers (Γ++Γ') ->
        noswitch_block blk ->
        NoDupLocals (map fst Γ++map fst Γ'++map fst Γ'') blk ->
        Forall (AtomOrGensym switch_prefs) (map fst Γ) ->
        GoodLocals switch_prefs blk ->
        dom_ub Hi1 (Γ++Γ') ->
        sem_block_ck G1 Hi1 bs blk ->
        dom Hi2 (Γ ++ Γ'') ->
        sc_vars (Γ++Γ'') Hi2 bs ->
        st_valid st ->
        Forall (fun x => st_In x st) (map fst (Γ ++ Γ'')) ->
        inlinelocal_block sub blk st = (locs', blks', st') ->
        exists Hi3,
          Hi2Hi3 /\
          dom Hi3 (Γ++Γ''++senv_of_anns locs') /\
          sc_vars (Γ++Γ''++senv_of_anns locs') Hi3 bs /\
          Forall (sem_block_ck G2 Hi3 bs) blks'.
    Proof with

    Lemma inlinelocal_node_sem : forall f n ins outs,
        Ordered_nodes (Global G1.(types) G1.(externs) (n::G1.(nodes))) ->
        Ordered_nodes (Global G2.(types) G2.(externs) ((inlinelocal_node n)::G2.(nodes))) ->
        sem_node_ck (Global G1.(types) G1.(externs) (n::G1.(nodes))) f ins outs ->
        sem_node_ck (Global G2.(types) G2.(externs) ((inlinelocal_node n)::G2.(nodes))) f ins outs.
    Proof with

  End inlinelocal_node_sem.

  Lemma inlinelocal_global_refines : forall G,
      wc_global G ->
      global_sem_refines G (inlinelocal_global G).
  Proof with

  Theorem inlinelocal_global_sem : forall G f ins outs,
      wc_global G ->
      sem_node_ck G f ins outs ->
      sem_node_ck (inlinelocal_global G) f ins outs.
  Proof.

End ILCORRECTNESS.

Module ILCorrectnessFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Ty : LTYPING Ids Op OpAux Cks Senv Syn)
       (Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr)
       (LClockSem : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Clo Lord CStr Sem)
       (IL : INLINELOCAL Ids Op OpAux Cks Senv Syn)
       <: ILCORRECTNESS Ids Op OpAux Cks CStr Senv Syn Ty Clo Lord Sem LClockSem IL.
  Include ILCORRECTNESS Ids Op OpAux Cks CStr Senv Syn Ty Clo Lord Sem LClockSem IL.
End ILCorrectnessFun.