Module LSyntax

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Coq Require Import PArith.
From Coq Require Import Sorting.Permutation.
From Coq Require Import Setoid Morphisms.

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

The Lustre dataflow language


Module Type LSYNTAX
       (Import Ids : IDS)
       (Import Op : OPERATORS).

Expressions



  Definition ann : Type := (type * nclock)%type.
  Definition lann : Type := (list type * nclock)%type.

  Definition idents xs := List.map (@fst ident (type * clock)) xs.

  Inductive exp : Type :=
  | Econst : const -> exp
  | Evar : ident -> ann -> exp
  | Eunop : unop -> exp -> ann -> exp
  | Ebinop : binop -> exp -> exp -> ann -> exp

  | Efby : list exp -> list exp -> list ann -> exp
  | Earrow : list exp -> list exp -> list ann -> exp
  | Ewhen : list exp -> ident -> bool -> lann -> exp
  | Emerge : ident -> list exp -> list exp -> lann -> exp
  | Eite : exp -> list exp -> list exp -> lann -> exp

  | Eapp : ident -> list exp -> option exp -> list ann -> exp.

  Implicit Type e: exp.

Equations


  Definition equation : Type := (list ident * list exp)%type.

  Implicit Type eqn: equation.

Node


  Fixpoint numstreams (e: exp) : nat :=
    match e with
    | Econst c => 1
    | Efby _ _ anns
    | Earrow _ _ anns
    | Eapp _ _ _ anns => length anns
    | Evar _ _
    | Eunop _ _ _
    | Ebinop _ _ _ _ => 1
    | Ewhen _ _ _ (tys, _)
    | Emerge _ _ _ (tys, _)
    | Eite _ _ _ (tys, _) => length tys
    end.


  Fixpoint annot (e: exp): list (type * nclock) :=
    match e with
    | Econst c => [(type_const c, (Cbase, None))]
    | Efby _ _ anns
    | Earrow _ _ anns
    | Eapp _ _ _ anns => anns
    | Evar _ ann
    | Eunop _ _ ann
    | Ebinop _ _ _ ann => [ann]
    | Ewhen _ _ _ (tys, ck)
    | Emerge _ _ _ (tys, ck)
    | Eite _ _ _ (tys, ck) => map (fun ty=> (ty, ck)) tys
    end.

  Definition annots (es: list exp): list (type * nclock) :=
    flat_map annot es.

  Fixpoint typeof (e: exp): list type :=
    match e with
    | Econst c => [type_const c]
    | Efby _ _ anns
    | Earrow _ _ anns
    | Eapp _ _ _ anns => map fst anns
    | Evar _ ann
    | Eunop _ _ ann
    | Ebinop _ _ _ ann => [fst ann]
    | Ewhen _ _ _ anns
    | Emerge _ _ _ anns
    | Eite _ _ _ anns => fst anns
    end.

  Definition typesof (es: list exp): list type :=
    flat_map typeof es.

  Definition clock_of_nclock {A} (ann: A * nclock): clock := stripname (snd ann).
  Definition stream_name {A} (ann: A * nclock) : option ident := snd (snd ann).

  Definition unnamed_stream {A} (ann: A * nclock): Prop := snd (snd ann) = None.

  Fixpoint clockof (e: exp): list clock :=
    match e with
    | Econst c => [Cbase]
    | Efby _ _ anns
    | Earrow _ _ anns
    | Eapp _ _ _ anns => map clock_of_nclock anns
    | Evar _ ann
    | Eunop _ _ ann
    | Ebinop _ _ _ ann => [clock_of_nclock ann]
    | Ewhen _ _ _ anns
    | Emerge _ _ _ anns
    | Eite _ _ _ anns => map (fun _ => clock_of_nclock anns) (fst anns)
    end.

  Definition clocksof (es: list exp): list clock :=
    flat_map clockof es.

  Fixpoint nclockof (e: exp): list nclock :=
    match e with
    | Econst c => [(Cbase, None)]
    | Efby _ _ anns
    | Earrow _ _ anns
    | Eapp _ _ _ anns => map snd anns
    | Evar _ ann
    | Eunop _ _ ann
    | Ebinop _ _ _ ann => [snd ann]
    | Ewhen _ _ _ anns
    | Emerge _ _ _ anns
    | Eite _ _ _ anns => map (fun _ => snd anns) (fst anns)
    end.

  Definition nclocksof (es: list exp): list nclock :=
    flat_map nclockof es.

  Definition vars_defined (eqs: list equation) : list ident :=
    flat_map fst eqs.

  Definition anon_streams (anns : list ann) :=
    map_filter (fun '(ty, (cl, name)) => match name with
                                      | None => None
                                      | Some x => Some (x, (ty, cl))
                                      end) anns.

  Fixpoint fresh_in (e : exp) : list (ident * (type * clock)) :=
    match e with
    | Econst _ => []
    | Evar _ _ => []
    | Eunop _ e _ => fresh_in e
    | Ebinop _ e1 e2 _ => (fresh_in e1)++(fresh_in e2)
    | Efby e0s es _
    | Earrow e0s es _ => concat (map fresh_in e0s)++concat (map fresh_in es)
    | Ewhen es _ _ _ => concat (map fresh_in es)
    | Emerge _ ets efs _ => concat (map fresh_in ets)++concat (map fresh_in efs)
    | Eite e ets efs _ => (fresh_in e)++concat (map fresh_in ets)++concat (map fresh_in efs)
    | Eapp _ es None anns => concat (map fresh_in es)++anon_streams anns
    | Eapp _ es (Some r) anns => concat (map fresh_in es)++fresh_in r++anon_streams anns
    end.

  Definition fresh_ins (es : list exp) : list (ident * (type * clock)) :=
    concat (map fresh_in es).

  Definition anon_in (e : exp) : list (ident * (type * clock)) :=
    match e with
    | Eapp _ es None _ => fresh_ins es
    | Eapp _ es (Some r) _ => fresh_ins es++fresh_in r
    | e => fresh_in e
    end.

  Definition anon_ins (es : list exp) : list (ident * (type * clock)) :=
    concat (map anon_in es).

  Definition anon_in_eq (eq : equation) : list (ident * (type * clock)) :=
    anon_ins (snd eq).

  Definition anon_in_eqs (eqs : list equation) : list (ident * (type * clock)) :=
    concat (map anon_in_eq eqs).

  Record node : Type :=
    mk_node {
        n_name : ident;
        n_hasstate : bool;
        n_in : list (ident * (type * clock));
        n_out : list (ident * (type * clock));
        n_vars : list (ident * (type * clock));
        n_eqs : list equation;

        n_prefixes : PS.t;
        n_ingt0 : 0 < length n_in;
        n_outgt0 : 0 < length n_out;
        n_defd : Permutation (vars_defined n_eqs)
                                 (map fst (n_vars ++ n_out));
        n_nodup : NoDupMembers (n_in ++ n_vars ++ n_out ++ anon_in_eqs n_eqs);
        n_good : Forall (AtomOrGensym n_prefixes) (map fst (n_in ++ n_vars ++ n_out ++ anon_in_eqs n_eqs)) /\ atom n_name
      }.

Program


  Definition global := list node.


  Definition find_node (f : ident) : global -> option node :=
    List.find (fun n=> ident_eqb n.(n_name) f).

find_node

  Lemma find_node_Exists:
    forall f G, find_node f G <> None <-> List.Exists (fun n=> n.(n_name) = f) G.
Proof.

  Lemma find_node_tl:
    forall f node G,
      node.(n_name) <> f
      -> find_node f (node::G) = find_node f G.
Proof.

  Lemma find_node_other:
    forall f node G node',
      node.(n_name) <> f
      -> (find_node f (node::G) = Some node'
         <-> find_node f G = Some node').
Proof.

  Lemma find_node_split:
    forall f G node,
      find_node f G = Some node
      -> exists bG aG,
        G = bG ++ node :: aG.
Proof.

  Lemma find_node_In : forall G n,
      In n G ->
      NoDup (map n_name G) ->
      find_node (n_name n) G = Some n.
Proof.

  Lemma find_node_incl : forall f G G' n,
      incl G G' ->
      NoDup (map n_name G) ->
      NoDup (map n_name G') ->
      find_node f G = Some n ->
      find_node f G' = Some n.
Proof.

Structural properties

  Section exp_ind2.

    Variable P : exp -> Prop.

    Hypothesis EconstCase:
      forall c,
        P (Econst c).

    Hypothesis EvarCase:
      forall x a,
        P (Evar x a).

    Hypothesis EunopCase:
      forall op e a,
        P e ->
        P (Eunop op e a).

    Hypothesis EbinopCase:
      forall op e1 e2 a,
        P e1 ->
        P e2 ->
        P (Ebinop op e1 e2 a).

    Hypothesis EfbyCase:
      forall e0s es a,
        Forall P e0s ->
        Forall P es ->
        P (Efby e0s es a).

    Hypothesis EarrowCase:
      forall e0s es a,
        Forall P e0s ->
        Forall P es ->
        P (Earrow e0s es a).

    Hypothesis EwhenCase:
      forall es x b a,
        Forall P es ->
        P (Ewhen es x b a).

    Hypothesis EmergeCase:
      forall x ets efs a,
        Forall P ets ->
        Forall P efs ->
        P (Emerge x ets efs a).

    Hypothesis EiteCase:
      forall e ets efs a,
        P e ->
        Forall P ets ->
        Forall P efs ->
        P (Eite e ets efs a).

    Hypothesis EappCase:
      forall f es ro a,
        (match ro with None => True | Some r => P r end) ->
        Forall P es ->
        P (Eapp f es ro a).

    Local Ltac SolveForall :=
      match goal with
      | |- Forall ?P ?l => induction l; auto
      | _ => idtac
      end.

    Fixpoint exp_ind2 (e: exp) : P e.
Proof.

  End exp_ind2.

annots

  Fact length_annot_numstreams : forall e,
      length (annot e) = numstreams e.
Proof.

typesof

  Fact typeof_annot : forall e,
      typeof e = map fst (annot e).
Proof.

  Corollary length_typeof_numstreams : forall e,
      length (typeof e) = numstreams e.
Proof.

  Fact typesof_annots : forall es,
      typesof es = map fst (annots es).
Proof.

  Corollary length_typesof_annots : forall es,
      length (typesof es) = length (annots es).
Proof.

  Fact typeof_concat_typesof : forall l,
      concat (map typeof (concat l)) = concat (map typesof l).
Proof.

clocksof

  Fact clockof_annot : forall e,
      clockof e = map fst (map snd (annot e)).
Proof.

  Corollary length_clockof_numstreams : forall e,
      length (clockof e) = numstreams e.
Proof.

  Fact clocksof_annots : forall es,
      clocksof es = map fst (map snd (annots es)).
Proof.

  Corollary length_clocksof_annots : forall es,
      length (clocksof es) = length (annots es).
Proof.

  Lemma In_clocksof:
    forall sck es,
      In sck (clocksof es) ->
      exists e, In e es /\ In sck (clockof e).
Proof.

  Fact clockof_concat_clocksof : forall l,
      concat (map clockof (concat l)) = concat (map clocksof l).
Proof.

nclockof and nclocksof

  Fact nclockof_annot : forall e,
      nclockof e = map snd (annot e).
Proof.

  Corollary length_nclockof_numstreams : forall e,
      length (nclockof e) = numstreams e.
Proof.

  Fact nclocksof_annots : forall es,
      nclocksof es = map snd (annots es).
Proof.

  Corollary length_nclocksof_annots : forall es,
      length (nclocksof es) = length (annots es).
Proof.

  Lemma clockof_nclockof:
    forall e,
      clockof e = map stripname (nclockof e).
Proof.

  Lemma nclockof_length :
    forall e, length (nclockof e) = length (clockof e).
Proof.

  Lemma clocksof_nclocksof:
    forall es,
      clocksof es = map stripname (nclocksof es).
Proof.

  Lemma In_nclocksof:
    forall nck es,
      In nck (nclocksof es) ->
      exists e, In e es /\ In nck (nclockof e).
Proof.

  Corollary In_snd_nclocksof:
    forall n es,
      In n (map snd (nclocksof es)) ->
      exists e, In e es /\ In n (map snd (nclockof e)).
Proof.

fresh_in and anon_in specification and properties

  Lemma anon_in_fresh_in : forall e,
      incl (anon_in e) (fresh_in e).
Proof.

  Lemma fresh_ins_nil:
    forall e es,
      fresh_ins (e::es) = [] ->
      fresh_in e = [].
Proof.

Interface equivalence between nodes

  Section interface_eq.

Nodes are equivalent if their interface are equivalent, that is if they have the same identifier and the same input/output types
    Definition node_iface_eq n n' : Prop :=
      n.(n_name) = n'.(n_name) /\
      n.(n_hasstate) = n'.(n_hasstate) /\
      n.(n_in) = n'.(n_in) /\
      n.(n_out) = n'.(n_out).

    Fact node_iface_eq_refl : Reflexive node_iface_eq.
Proof.

    Fact node_iface_eq_sym : Symmetric node_iface_eq.
Proof.

    Fact node_iface_eq_trans : Transitive node_iface_eq.
Proof.

    Global Instance node_iface_eq_eq : Equivalence node_iface_eq.
Proof.

Globals are equivalent if they contain equivalent nodes
    Definition global_iface_eq G G' : Prop :=
      forall f, orel node_iface_eq (find_node f G) (find_node f G').

    Fact global_eq_refl : Reflexive global_iface_eq.
Proof.

    Fact global_eq_sym : Symmetric global_iface_eq.
Proof.

    Fact global_eq_trans : Transitive global_iface_eq.
Proof.

    Global Instance global_iface_eq_eq : Equivalence global_iface_eq.
Proof.

    Fact global_iface_eq_cons : forall G G' n n',
        global_iface_eq G G' ->
        n.(n_name) = n'.(n_name) ->
        n.(n_hasstate) = n'.(n_hasstate) ->
        n.(n_in) = n'.(n_in) ->
        n.(n_out) = n'.(n_out) ->
        global_iface_eq (n::G) (n'::G').
Proof.

    Fact global_iface_eq_find : forall G G' f n,
        global_iface_eq G G' ->
        find_node f G = Some n ->
        exists n', (find_node f G' = Some n' /\
               node_iface_eq n n').
Proof.

  End interface_eq.

Property of length in expressions; is implied by wc and wt


  Inductive wl_exp : global -> exp -> Prop :=
  | wl_Const : forall G c,
      wl_exp G (Econst c)
  | wl_Evar : forall G x a,
      wl_exp G (Evar x a)
  | wl_Eunop : forall G op e a,
      wl_exp G e ->
      numstreams e = 1 ->
      wl_exp G (Eunop op e a)
  | wl_Ebinop : forall G op e1 e2 a,
      wl_exp G e1 ->
      wl_exp G e2 ->
      numstreams e1 = 1 ->
      numstreams e2 = 1 ->
      wl_exp G (Ebinop op e1 e2 a)
  | wl_Efby : forall G e0s es anns,
      Forall (wl_exp G) e0s ->
      Forall (wl_exp G) es ->
      length (annots e0s) = length anns ->
      length (annots es) = length anns ->
      wl_exp G (Efby e0s es anns)
  | wl_Earrow : forall G e0s es anns,
      Forall (wl_exp G) e0s ->
      Forall (wl_exp G) es ->
      length (annots e0s) = length anns ->
      length (annots es) = length anns ->
      wl_exp G (Earrow e0s es anns)
  | wl_Ewhen : forall G es x b tys nck,
      Forall (wl_exp G) es ->
      length (annots es) = length tys ->
      wl_exp G (Ewhen es x b (tys, nck))
  | wl_Emerge : forall G x ets efs tys nck,
      Forall (wl_exp G) ets ->
      Forall (wl_exp G) efs ->
      length (annots ets) = length tys ->
      length (annots efs) = length tys ->
      wl_exp G (Emerge x ets efs (tys, nck))
  | wl_Eifte : forall G e ets efs tys nck,
      wl_exp G e ->
      Forall (wl_exp G) ets ->
      Forall (wl_exp G) efs ->
      numstreams e = 1 ->
      length (annots ets) = length tys ->
      length (annots efs) = length tys ->
      wl_exp G (Eite e ets efs (tys, nck))
  | wl_Eapp : forall G f n es anns,
      Forall (wl_exp G) es ->
      find_node f G = Some n ->
      length (annots es) = length (n_in n) ->
      length anns = length (n_out n) ->
      wl_exp G (Eapp f es None anns)
  | wl_EappReset : forall G f n es r anns,
      wl_exp G r ->
      Forall (wl_exp G) es ->
      numstreams r = 1 ->
      find_node f G = Some n ->
      length (annots es) = length (n_in n) ->
      length anns = length (n_out n) ->
      wl_exp G (Eapp f es (Some r) anns).

  Definition wl_equation G (eq : equation) :=
    let (xs, es) := eq in
    Forall (wl_exp G) es /\ length xs = length (annots es).

  Definition wl_node G (n : node) :=
    Forall (wl_equation G) (n_eqs n).

  Inductive wl_global : global -> Prop :=
  | wlg_nil:
      wl_global []
  | wlg_cons: forall n ns,
      wl_global ns ->
      wl_node ns n ->
      wl_global (n::ns).

fresh_in, anon_in properties


  Fact fresh_in_incl : forall e es,
      In e es ->
      incl (fresh_in e) (fresh_ins es).
Proof.

  Fact anon_in_incl : forall e es,
      In e es ->
      incl (anon_in e) (anon_ins es).
Proof.

  Fact anon_in_eq_incl : forall eq eqs,
      In eq eqs ->
      incl (anon_in_eq eq) (anon_in_eqs eqs).
Proof.

  Fact InMembers_fresh_in : forall x e es,
      In e es ->
      InMembers x (fresh_in e) ->
      InMembers x (fresh_ins es).
Proof.

  Fact InMembers_anon_in : forall x e es,
      In e es ->
      InMembers x (anon_in e) ->
      InMembers x (anon_ins es).
Proof.

  Fact InMembers_anon_in_eq : forall x eq eqs,
      In eq eqs ->
      InMembers x (anon_in_eq eq) ->
      InMembers x (anon_in_eqs eqs).
Proof.

  Fact Ino_In_anon_streams : forall x anns,
      Ino x (map (fun x => snd (snd x)) anns) ->
      InMembers x (anon_streams anns).
Proof.

  Fact NoDupMembers_fresh_in : forall e es,
      In e es ->
      NoDupMembers (fresh_ins es) ->
      NoDupMembers (fresh_in e).
Proof.

  Corollary NoDupMembers_fresh_in' : forall vars e es,
      In e es ->
      NoDupMembers (vars ++ fresh_ins es) ->
      NoDupMembers (vars ++ fresh_in e).
Proof.

  Fact NoDupMembers_anon_in : forall e es,
      In e es ->
      NoDupMembers (anon_ins es) ->
      NoDupMembers (anon_in e).
Proof.

  Corollary NoDupMembers_anon_in' : forall vars e es,
      In e es ->
      NoDupMembers (vars ++ anon_ins es) ->
      NoDupMembers (vars ++ anon_in e).
Proof.

  Fact NoDupMembers_anon_in_eq : forall eq eqs,
      In eq eqs ->
      NoDupMembers (anon_in_eqs eqs) ->
      NoDupMembers (anon_in_eq eq).
Proof.

  Corollary NoDupMembers_anon_in_eq' : forall vars eq eqs,
      In eq eqs ->
      NoDupMembers (vars ++ anon_in_eqs eqs) ->
      NoDupMembers (vars ++ anon_in_eq eq).
Proof.

Additional properties


  Lemma node_NoDup : forall n,
      NoDup (map fst (n_in n ++ n_vars n ++ n_out n)).
Proof.

  Lemma in_vars_defined_NoDup : forall n,
      NoDup (map fst (n_in n) ++ vars_defined (n_eqs n)).
Proof.

  Corollary NoDup_vars_defined_n_eqs:
    forall n,
      NoDup (vars_defined n.(n_eqs)).
Proof.

  Instance vars_defined_Proper:
    Proper (@Permutation equation ==> @Permutation ident)
           vars_defined.
Proof.

  Fact vars_defined_app : forall eqs1 eqs2,
      vars_defined (eqs1++eqs2) = vars_defined eqs1 ++ vars_defined eqs2.
Proof.

End LSYNTAX.

Module LSyntaxFun
       (Ids : IDS)
       (Op : OPERATORS) <: LSYNTAX Ids Op.
  Include LSYNTAX Ids Op.
End LSyntaxFun.