Module Complete

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

From Coq Require Import Permutation.

From Velus Require Import Common.
From Velus Require Import CommonTyping.
From Velus Require Import Environment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax.

Module Type COMPLETE
  (Import Ids : IDS)
  (Import 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).

  Section complete_branch.
    Context {A : Type}.

    Variable f_comp : A -> A.
    Variable add_equations : list equation -> A -> A.

    Variable must_def : PS.t.
    Variable is_def : PS.t.

    Definition complete_branch (env : Env.t type) (br : branch A) : branch A :=
      let 'Branch caus blks := br in
      let diff := PS.diff must_def is_def in
      let eqs := List.map (fun x => ([x], [Elast x (or_default OpAux.bool_velus_type (Env.find x env), Cbase)])) (PS.elements diff) in
      Branch caus (add_equations eqs (f_comp blks)).
  End complete_branch.

  Section complete_scope.
    Context {A : Type}.

    Variable f_comp : Env.t type -> A -> A.

    Definition complete_scope (env : Env.t type) (s : scope A) :=
      let 'Scope locs blks := s in
      let env' := Env.adds' (map_filter (fun '(x, (ty, ck, _, o)) => if isSome o then Some (x, ty) else None) locs) env in
      Scope locs (f_comp env' blks).
  End complete_scope.

  Fixpoint complete_block (env : Env.t type) (blk : block) :=
    match blk with
    | Beq _ | Blast _ _ => blk
    | Breset blks er => Breset (map (complete_block env) blks) er
    | Blocal s => Blocal (complete_scope (fun env => map (complete_block env)) env s)
    | Bswitch e brs =>
        let must_def := vars_defined (Bswitch e brs) in
        Bswitch e
          (map (fun '(k, br) =>
                  let br' := complete_branch
                               (map (complete_block env))
                               (fun eqs blks => map Beq eqs++blks)
                               must_def
                               (vars_defined_branch (fun blks => PSUnion (map vars_defined blks)) br)
                               env br
                  in (k, br')) brs)
    | Bauto aut ck ini sts =>
        let must_def := vars_defined (Bauto aut ck ini sts) in
        Bauto aut ck ini
          (map (fun '(k, br) =>
                  let br' := complete_branch
                               (fun '(unl, s) => (unl, complete_scope (fun env '(blks, unt) => (map (complete_block env) blks, unt)) env s))
                               (fun eq '(unl, Scope locs (blks, unt)) => (unl, Scope locs (map Beq eq++blks, unt)))
                               must_def
                               (vars_defined_branch (fun '(_, blks) => vars_defined_scope (fun '(blks0, _) => PSUnion (map vars_defined blks0)) blks) br)
                               env br
             in (k, br')) sts)
    end.


  Lemma complete_block_NoDupLocals : forall blk env xs,
      NoDupLocals xs blk ->
      NoDupLocals xs (complete_block env blk).


  Lemma complete_block_GoodLocals : forall blk env xs,
      GoodLocals xs blk ->
      GoodLocals xs (complete_block env blk).


  Lemma complete_scope_VarsDefined {A} P_nd P_vd1 (P_vd2: _ -> _ -> Prop) f_comp :
    forall locs (blks: A) env Γ,
      NoDupMembers Γ ->
      NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
      VarsDefinedScope P_vd1 (Scope locs blks) Γ ->
      (forall env Γ,
          NoDupMembers Γ ->
          P_nd (map fst Γ) blks ->
          P_vd1 blks Γ ->
          P_vd2 (f_comp env blks) (map fst Γ)) ->
      VarsDefinedCompScope P_vd2 (complete_scope f_comp env (Scope locs blks)) (map fst Γ).

  Opaque complete_scope.
  Lemma complete_block_VarsDefined : forall blk env Γ,
      NoDupMembers Γ ->
      NoDupLocals (map fst Γ) blk ->
      VarsDefined blk Γ ->
      VarsDefinedComp (complete_block env blk) (map fst Γ).
  Transparent complete_scope.

  Lemma complete_block_LastsDefined : forall blk env xs,
      LastsDefined blk xs ->
      LastsDefined (complete_block env blk) xs.

  Program Definition complete_node (n : @node (fun _ _ => True) elab_prefs) : @node complete elab_prefs :=
    let env := Env.from_list
                 (map_filter
                    (fun xtc => if isSome (snd (snd xtc))
                             then Some (fst xtc, fst (fst (fst (snd xtc))))
                             else None) (n_out n)) in
    {|
      n_name := n_name n;
      n_hasstate := n_hasstate n;
      n_in := n_in n;
      n_out := n_out n;
      n_block := complete_block env (n_block n);
      n_ingt0 := n_ingt0 n;
      n_outgt0 := n_outgt0 n;
    |}.

  Global Program Instance complete_node_transform_unit: TransformUnit (@node (fun _ _ => True) elab_prefs) (@node complete elab_prefs) :=
    { transform_unit := complete_node }.

  Global Program Instance complete_global_without_units : TransformProgramWithoutUnits (@global (fun _ _ => True) elab_prefs) (@global complete elab_prefs) :=
    { transform_program_without_units := fun g => Global g.(types) g.(externs) [] }.

  Definition complete_global : @global (fun _ _ => True) elab_prefs -> @global complete elab_prefs :=
    transform_units.

Equality of interfaces

  Lemma complete_global_iface_eq : forall G,
      global_iface_eq G (complete_global G).

End COMPLETE.

Module CompleteFun
       (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)
       <: COMPLETE Ids Op OpAux Cks Senv Syn.
  Include COMPLETE Ids Op OpAux Cks Senv Syn.
End CompleteFun.