Module NLTyping

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

From Velus Require Import Common.
From Velus Require Import Operators Environment.
From Velus Require Import Clocks.
From Velus Require Import Fresh.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LTyping.
From Velus Require Import Lustre.NormLast.NormLast.

Module Type NLTYPING
       (Import Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Clo : LTYPING Ids Op OpAux Cks Senv Syn)
       (Import NL : NORMLAST Ids Op OpAux Cks Senv Syn).

  Import Fresh Notations Facts Tactics.

Phase 1

  Section init_block.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable G : @global PSyn prefs.

    Variable sub : Env.t ident.

    Variable Γ Γ' : static_env.

    Hypothesis Hty : forall x ty, HasType Γ x ty -> HasType Γ' x ty.
    Hypothesis Hvar : forall x y ty, Env.find x sub = Some y -> HasType Γ x ty -> HasType Γ' y ty.
    Hypothesis Hlast : forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x.

    Lemma init_exp_wt : forall e,
        wt_exp G Γ e ->
        wt_exp G Γ' (init_exp sub e).

    Lemma init_block_wt : forall blk,
        unnested_block blk ->
        wt_block G Γ blk ->
        wt_block G Γ' (init_block sub blk).

  End init_block.

  Lemma init_top_block_wt {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk outs' blk' st st',
      unnested outs blk ->
      NoDupMembers (ins ++ senv_of_decls outs) ->
      NoDupLocals (map fst (ins ++ senv_of_decls outs)) blk ->
      Forall (fun '(_, ann) => OpAux.wt_type (types G) (typ ann)) (senv_of_decls outs) ->
      wt_clocks G.(types) (ins ++ senv_of_decls outs) (senv_of_decls outs) ->
      wt_block G (ins ++ senv_of_decls outs) blk ->
      init_top_block outs blk st = (outs', blk', st') ->
      wt_block G (ins ++ senv_of_decls outs') blk'.

Phase 2

  Section rename_block.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable G : @global PSyn prefs.

    Variable sub : Env.t ident.

    Variable Γ Γ' : static_env.

    Hypothesis Hty : forall x ty, HasType Γ x ty -> HasType Γ' x ty.
    Hypothesis Hvar : forall x y ty, Env.find x sub = Some y -> HasType Γ x ty -> HasType Γ' y ty.
    Hypothesis Hlast : forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x.
    Hypothesis Hnlast : forall x y, Env.find x sub = Some y -> IsLast Γ x -> IsLast Γ' y.

    Lemma rename_exp_wt : forall e,
        wt_exp G Γ e ->
        wt_exp G Γ' (rename_exp sub e).

    Lemma rename_block_wt : forall blk,
        unnested_block blk ->
        wt_block G Γ blk ->
        Forall (wt_block G Γ') (rename_block sub blk).

  End rename_block.

  Lemma output_top_block_wt {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk blk' st st',
      unnested outs blk ->
      NoDupMembers (ins ++ senv_of_decls outs) ->
      NoDupLocals (map fst (ins ++ senv_of_decls outs)) blk ->
      Forall (fun '(_, ann) => OpAux.wt_type (types G) (typ ann)) (senv_of_decls outs) ->
      wt_clocks G.(types) (ins ++ senv_of_decls outs) (senv_of_decls outs) ->
      wt_block G (ins ++ senv_of_decls outs) blk ->
      output_top_block outs blk st = (blk', st') ->
      wt_block G (ins ++ senv_of_decls (remove_lasts outs)) blk'.

Phase 3

  Section unnest_block.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable G : @global PSyn prefs.

    Variable sub : Env.t ident.

    Variable Γ Γ' : static_env.

    Hypothesis Hty : forall x ty, HasType Γ x ty -> HasType Γ' x ty.
    Hypothesis Hvar : forall x y ty, Env.find x sub = Some y -> HasType Γ x ty -> HasType Γ' y ty.
    Hypothesis Hlast : forall x, Env.find x sub = None -> IsLast Γ x -> IsLast Γ' x.
    Hypothesis Hnlast : forall x y, Env.find x sub = Some y -> IsLast Γ x -> IsLast Γ' y.

    Lemma unnest_block_wt : forall blk,
        unnested_block blk ->
        wt_block G Γ blk ->
        wt_block G Γ' (unnest_block sub blk).
  End unnest_block.

  Lemma unnest_top_block_wt {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk blk' st st',
      unnested outs blk ->
      NoDupMembers (senv_of_ins ins ++ senv_of_decls outs) ->
      NoDupLocals (map fst (senv_of_ins ins ++ senv_of_decls outs)) blk ->
      wt_block G (senv_of_ins ins ++ senv_of_decls outs) blk ->
      unnest_top_block blk st = (blk', st') ->
      wt_block G (senv_of_ins ins ++ senv_of_decls outs) blk'.

  Lemma normlast_top_block_wt {PSyn prefs} (G: @global PSyn prefs) : forall ins outs blk blk' st st',
      let Γ := senv_of_ins ins ++ senv_of_decls outs in
      let Γ' := senv_of_ins ins ++ senv_of_decls (remove_lasts outs) in
      unnested outs blk ->
      (exists ls : list ident, LastsDefined blk ls /\ Permutation.Permutation ls (lasts_of_decls outs)) ->
      NoDupMembers Γ ->
      NoDupLocals (map fst Γ) blk ->
      Forall (AtomOrGensym norm1_prefs) (map fst ins ++ map fst outs) ->
      GoodLocals norm1_prefs blk ->
      wt_clocks (types G) Γ (senv_of_decls outs) ->
      Forall (fun '(_, ann) => OpAux.wt_type (types G) (typ ann)) (senv_of_decls outs) ->
      wt_block G Γ blk ->
      normlast_top_block outs blk st = (blk', st') ->
      wt_block G Γ' blk'.


  Lemma normlast_node_wt : forall G1 G2 (n : @node _ _),
      global_iface_incl G1 G2 ->
      wt_node G1 n ->
      wt_node G2 (normlast_node n).

  Theorem normlast_global_wt : forall G,
      wt_global G ->
      wt_global (normlast_global G).

End NLTYPING.

Module NLTypingFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Clo : LTYPING Ids Op OpAux Cks Senv Syn)
       (NL : NORMLAST Ids Op OpAux Cks Senv Syn)
       <: NLTYPING Ids Op OpAux Cks Senv Syn Clo NL.
  Include NLTYPING Ids Op OpAux Cks Senv Syn Clo NL.
End NLTypingFun.