Module NLNormalArgs

From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import Clocks.
From Velus Require Import NLustre.NLSyntax.

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

       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import CESyn : CESYNTAX Op)
       (Import Syn : NLSYNTAX Ids Op CESyn).

The normal_args predicate defines a normalization condition on node arguments -- those that are not on the base clock can only be instantiated with constants or variables -- that is necessary for correct generation of Obc/Clight. To see why this is necessary. Consider the NLustre equation: y = f(1, 3 when ck / x) with x on the clock ck, and y on the base clock. The generated Obc code is y := f(1, 3 / x) which has no semantics when ck = false, since x = None then 3 / x is not given a meaning. Consider what would happen were the semantics of 3 / x = None. There are two possible problems. If x is a local variable, then x = None in Obc implies that x = VUndef in Clight and 3 / VUndef has no semantics. I.e., the Obc program having a semantics would not be enough to guarantee that the Clight program generated from it does. If x is a state variable, then x = None in Obc implies that x could be anything in Clight (though it would be defined since state variables are stored in a global structure). We might then prove that x is never 0 (when ck = true) in the original Lustre program. This would guarantee the absence of division by zero in the generated Obc (since x is None when ck = false), but not in the generated Clight code; since None in Obc means "don't care" in Clight, x may well contain the value 0 when ck is false (for instance, if ck = false at the first reaction).

  Inductive normal_args_eq (G: global) : equation -> Prop :=
  | CEqDef:
      forall x ck ce,
        normal_args_eq G (EqDef x ck ce)
  | CEqApp:
      forall xs ck f les r n,
        find_node f G = Some n ->
        Forall2 noops_exp (map (fun '(_, (_, ck)) => ck) n.(n_in)) les ->
        normal_args_eq G (EqApp xs ck f les r)
  | CEqFby:
      forall x ck v0 le,
        normal_args_eq G (EqFby x ck v0 le).

  Definition normal_args_node (G: global) (n: node) : Prop :=
    Forall (normal_args_eq G) n.(n_eqs).

  Fixpoint normal_args (G: list node) : Prop :=
    match G with
    | [] => True
    | n :: G' => normal_args_node G n /\ normal_args G'


Module NLNormalArgsFun
       (Ids : IDS)
       (Op : OPERATORS)
       (CESyn : CESYNTAX Op)
       (Syn : NLSYNTAX Ids Op CESyn)
  Include NLNORMALARGS Ids Op CESyn Syn.
End NLNormalArgsFun.