Module CESemantics

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

From Coq Require Import Setoid.
From Coq Require Import Morphisms.

From Velus Require Import Common.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import VelusMemory.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import IndexedStreams.


Module Type CESEMANTICS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Syn : CESYNTAX Ids Op OpAux Cks)
       (Import Str : INDEXEDSTREAMS Ids Op OpAux Cks).

FEnvironment and history

  Definition env := @FEnv.t ident svalue.
  Definition history := stream env.

Instantaneous semantics

  Section InstantSemantics.

    Variable base: bool.
    Variable R: env.

    Definition sem_vars_instant (xs: list ident) (vs: list svalue) : Prop :=
      Forall2 (sem_var_instant R) xs vs.

    Definition sem_clocked_var_instant (x: ident) (ck: clock) : Prop :=
      (sem_clock_instant base R ck true <-> exists c, sem_var_instant R x (present c))
      /\ (sem_clock_instant base R ck false <-> sem_var_instant R x absent).

    Definition sem_clocked_vars_instant (xs: list (ident * clock)) : Prop :=
      Forall (fun xc => sem_clocked_var_instant (fst xc) (snd xc)) xs.

    Inductive sem_exp_instant: exp -> svalue -> Prop:=
    | Sconst:
        forall c v,
          v = (if base then present (Vscalar (sem_cconst c)) else absent) ->
          sem_exp_instant (Econst c) v
    | Senum:
        forall x v ty,
          v = (if base then present (Venum x) else absent) ->
          sem_exp_instant (Eenum x ty) v
    | Svar:
        forall x v ty,
          sem_var_instant R x v ->
          sem_exp_instant (Evar x ty) v
    | Swhen_eq:
        forall s x tx sc b,
          sem_var_instant R x (present (Venum b)) ->
          sem_exp_instant s (present sc) ->
          sem_exp_instant (Ewhen s (x, tx) b) (present sc)
    | Swhen_abs1:
        forall s x tx sc b b',
          sem_var_instant R x (present (Venum b')) ->
          b <> b' ->
          sem_exp_instant s (present sc) ->
          sem_exp_instant (Ewhen s (x, tx) b) absent
    | Swhen_abs:
        forall s x tx b,
          sem_var_instant R x absent ->
          sem_exp_instant s absent ->
          sem_exp_instant (Ewhen s (x, tx) b) absent
    | Sunop_eq:
        forall le op v v' ty,
          sem_exp_instant le (present v) ->
          sem_unop op v (typeof le) = Some v' ->
          sem_exp_instant (Eunop op le ty) (present v')
    | Sunop_abs:
        forall le op ty,
          sem_exp_instant le absent ->
          sem_exp_instant (Eunop op le ty) absent
    | Sbinop_eq:
        forall le1 le2 op v1 v2 v' ty,
          sem_exp_instant le1 (present v1) ->
          sem_exp_instant le2 (present v2) ->
          sem_binop op v1 (typeof le1) v2 (typeof le2) = Some v' ->
          sem_exp_instant (Ebinop op le1 le2 ty) (present v')
    | Sbinop_abs:
        forall le1 le2 op ty,
          sem_exp_instant le1 absent ->
          sem_exp_instant le2 absent ->
          sem_exp_instant (Ebinop op le1 le2 ty) absent.

    Definition sem_exps_instant (les: list exp) (vs: list svalue) :=
      Forall2 sem_exp_instant les vs.

    Inductive sem_cexp_instant: cexp -> svalue -> Prop :=
    | Smerge_pres:
        forall x tx es ty b es1 e es2 c,
          sem_var_instant R x (present (Venum b)) ->
          es = es1 ++ e :: es2 ->
          length es1 = b ->
          sem_cexp_instant e (present c) ->
          Forall (fun e => sem_cexp_instant e absent) (es1 ++ es2) ->
          sem_cexp_instant (Emerge (x, tx) es ty) (present c)
    | Smerge_abs:
        forall x tx es ty,
          sem_var_instant R x absent ->
          Forall (fun e => sem_cexp_instant e absent) es ->
          sem_cexp_instant (Emerge (x, tx) es ty) absent
    | Scase_pres:
        forall e es d b vs c,
          sem_exp_instant e (present (Venum b)) ->
          Forall2 (fun e v => sem_cexp_instant (or_default d e) (present v)) es vs ->
          nth_error vs b = Some c ->
          sem_cexp_instant (Ecase e es d) (present c)
    | Scase_abs:
        forall e es d,
          sem_exp_instant e absent ->
          Forall (fun e => sem_cexp_instant (or_default d e) absent) es ->
          sem_cexp_instant (Ecase e es d) absent
    | Sexp:
        forall e v,
          sem_exp_instant e v ->
          sem_cexp_instant (Eexp e) v.

    Inductive sem_rhs_instant: rhs -> svalue -> Prop :=
    | Sextcall_pres:
      forall f es tyout tyins vs v,
        Forall2 (fun e ty => typeof e = Tprimitive ty) es tyins ->
        Forall2 (fun e v => sem_exp_instant e (present (Vscalar v))) es vs ->
        sem_extern f tyins vs tyout v ->
        sem_rhs_instant (Eextcall f es tyout) (present (Vscalar v))
    | Sextcall_abs:
      forall f es tyout tyins,
        Forall2 (fun e ty => typeof e = Tprimitive ty) es tyins ->
        Forall (fun e => sem_exp_instant e absent) es ->
        sem_rhs_instant (Eextcall f es tyout) absent
    | Scexp:
      forall e v,
        sem_cexp_instant e v ->
        sem_rhs_instant (Ecexp e) v.

  End InstantSemantics.

  Global Hint Constructors sem_exp_instant sem_cexp_instant : nlsem stcsem.

  Section sem_cexp_instant_ind_2.

    Variable base: bool.
    Variable R: env.

    Variable P : cexp -> svalue -> Prop.

    Hypothesis merge_presCase:
      forall x tx es ty b es1 e es2 c,
        sem_var_instant R x (present (Venum b)) ->
        es = es1 ++ e :: es2 ->
        length es1 = b ->
        sem_cexp_instant base R e (present c) ->
        P e (present c) ->
        Forall (fun e => sem_cexp_instant base R e absent) (es1 ++ es2) ->
        Forall (fun e => P e absent) (es1 ++ es2) ->
        P (Emerge (x, tx) es ty) (present c).

    Hypothesis merge_absCase:
      forall x tx es ty,
        sem_var_instant R x absent ->
        Forall (fun e => sem_cexp_instant base R e absent) es ->
        Forall (fun e => P e absent) es ->
        P (Emerge (x, tx) es ty) absent.

    Hypothesis case_presCase:
      forall e es d b vs c,
        sem_exp_instant base R e (present (Venum b)) ->
        Forall2 (fun e v => sem_cexp_instant base R (or_default d e) (present v)) es vs ->
        Forall2 (fun e v => P (or_default d e) (present v)) es vs ->
        nth_error vs b = Some c ->
        P (Ecase e es d) (present c).

    Hypothesis case_absCase:
      forall e es d,
        sem_exp_instant base R e absent ->
        Forall (fun e => sem_cexp_instant base R (or_default d e) absent) es ->
        Forall (fun e => P (or_default d e) absent) es ->
        P (Ecase e es d) absent.

    Hypothesis expCase:
      forall e v,
        sem_exp_instant base R e v ->
        P (Eexp e) v.

    Fixpoint sem_cexp_instant_ind_2
             (ce: cexp) (v: svalue)
             (Sem: sem_cexp_instant base R ce v) {struct Sem}
      : P ce v.

  End sem_cexp_instant_ind_2.

  Global Hint Extern 4 (sem_exps_instant _ _ nil nil) => apply Forall2_nil : nlsem stcsem.

  Section InstantAnnotatedSemantics.

    Variable base : bool.
    Variable R: env.

    Inductive sem_annotated_instant {A}
              (sem_instant: bool -> env -> A -> svalue -> Prop)
      : clock -> A -> svalue -> Prop :=
    | Stick:
        forall ck a c,
          sem_instant base R a (present c) ->
          sem_clock_instant base R ck true ->
          sem_annotated_instant sem_instant ck a (present c)
    | Sabs:
        forall ck a,
          sem_instant base R a absent ->
          sem_clock_instant base R ck false ->
          sem_annotated_instant sem_instant ck a absent.

    Definition sem_aexp_instant := sem_annotated_instant sem_exp_instant.
    Definition sem_caexp_instant := sem_annotated_instant sem_cexp_instant.
    Definition sem_arhs_instant := sem_annotated_instant sem_rhs_instant.

  End InstantAnnotatedSemantics.

Liftings of instantaneous semantics

  Section LiftSemantics.

    Variable bk : stream bool.
    Variable H : history.

    Definition sem_vars (x: list ident) (xs: stream (list svalue)): Prop :=
      lift' H sem_vars_instant x xs.

    Definition sem_clocked_var (x: ident) (ck: clock): Prop :=
      forall n, sem_clocked_var_instant (bk n) (H n) x ck.

    Definition sem_clocked_vars (xs: list (ident * clock)) : Prop :=
      forall n, sem_clocked_vars_instant (bk n) (H n) xs.

    Definition sem_aexp ck (e: exp) (xs: stream svalue): Prop :=
      lift bk H (fun base R => sem_aexp_instant base R ck) e xs.

    Definition sem_exp (e: exp) (xs: stream svalue): Prop :=
      lift bk H sem_exp_instant e xs.

    Definition sem_exps (e: list exp) (xs: stream (list svalue)): Prop :=
      lift bk H sem_exps_instant e xs.

    Definition sem_caexp ck (c: cexp) (xs: stream svalue): Prop :=
      lift bk H (fun base R => sem_caexp_instant base R ck) c xs.

    Definition sem_cexp (c: cexp) (xs: stream svalue): Prop :=
      lift bk H sem_cexp_instant c xs.

    Definition sem_arhs ck (c: rhs) (xs: stream svalue) : Prop :=
      lift bk H (fun base R => sem_arhs_instant base R ck) c xs.

    Definition sem_rhs (c: rhs) (xs: stream svalue): Prop :=
      lift bk H sem_rhs_instant c xs.

  End LiftSemantics.

Time-dependent semantics

  Definition clock_of_instant (vs: list svalue) : bool :=
    existsb (fun v => v <>b absent) vs.

  Lemma clock_of_instant_false:
    forall xs,
      clock_of_instant xs = false <-> absent_list xs.

  Lemma clock_of_instant_true:
    forall xs,
      clock_of_instant xs = true <-> Exists (fun v => v <> absent) xs.

  Definition clock_of (xss: stream (list svalue)): stream bool :=
    fun n => clock_of_instant (xss n).



  Add Parametric Morphism : sem_exp_instant
      with signature @eq _ ==> FEnv.Equiv eq ==> @eq _ ==> @eq _ ==> Basics.impl
        as sem_exp_instant_morph.

  Add Parametric Morphism : sem_cexp_instant
      with signature @eq _ ==> FEnv.Equiv eq ==> @eq _ ==> @eq _ ==> Basics.impl
        as sem_cexp_instant_morph.

  Add Parametric Morphism : sem_rhs_instant
      with signature @eq _ ==> FEnv.Equiv eq ==> @eq _ ==> @eq _ ==> Basics.impl
        as sem_rhs_instant_morph.

  Add Parametric Morphism A sem
    (sem_compat: Proper (eq ==> FEnv.Equiv eq ==> eq ==> eq ==> Basics.impl) sem)
    : (fun b e => @sem_annotated_instant b e A sem)
      with signature eq ==> FEnv.Equiv eq ==> eq ==> eq ==> eq ==> Basics.impl
        as sem_annotated_instant_morph.

  Add Parametric Morphism : sem_aexp_instant
      with signature eq ==> FEnv.Equiv eq ==> eq ==> eq ==> eq ==> Basics.impl
        as sem_aexp_instant_morph.

  Add Parametric Morphism : sem_caexp_instant
      with signature eq ==> FEnv.Equiv eq ==> eq ==> eq ==> eq ==> Basics.impl
        as sem_caexp_morph.

  Add Parametric Morphism A B H sem e: (fun b xs => @lift b H A B sem e xs)
      with signature eq_str ==> @eq_str B ==> Basics.impl
        as lift_eq_str.

  Add Parametric Morphism A B sem H e: (@lift' H A B sem e)
      with signature @eq_str B ==> Basics.impl
        as lift'_eq_str.

  Add Parametric Morphism : clock_of
      with signature eq_str ==> eq_str
        as clock_of_eq_str.

  Add Parametric Morphism : (sem_clocked_var)
      with signature eq_str ==> eq ==> eq ==> eq ==> Basics.impl
        as sem_clocked_var_eq_str.

  Add Parametric Morphism : (sem_clocked_vars)
      with signature eq_str ==> eq ==> eq ==> Basics.impl
        as sem_clocked_vars_eq_str.

  Lemma not_subrate_clock:
    forall R ck,
      ~ sem_clock_instant false R ck true.

  Corollary not_subrate_clock_impl:
    forall R ck b,
      sem_clock_instant false R ck b ->
      b = false.

  Lemma sem_vars_gt0:
    forall H (xs: list (ident * type)) ls,
      0 < length xs ->
      sem_vars H (map fst xs) ls ->
      forall n, 0 < length (ls n).

  Lemma sem_arhs_instant_absent:
    forall R ck e v,
      sem_arhs_instant false R ck e v ->
      v = absent.

  Ltac assert_const_length xss :=
    match goal with
      H: sem_vars _ _ xss |- _ =>
      let H' := fresh in
      let k := fresh in
      let k' := fresh in
      assert (wf_streams xss)
        by (intros k k'; pose proof H as H';
            unfold sem_vars, lift in *;
            specialize (H k); specialize (H' k');
            apply Forall2_length in H; apply Forall2_length in H';
            now rewrite H in H')
    end.

  Lemma sem_exps_instant_cons:
    forall b R e es v vs,
      sem_exps_instant b R (e :: es) (v :: vs)
      <-> (sem_exp_instant b R e v /\ sem_exps_instant b R es vs).

Determinism of the semantics

Instantaneous semantics

  Section InstantDeterminism.

    Variable base: bool.
    Variable R: env.

    Lemma sem_exp_instant_det:
      forall e v1 v2,
        sem_exp_instant base R e v1
        -> sem_exp_instant base R e v2
        -> v1 = v2.

    Lemma sem_aexp_instant_det:
      forall ck e v1 v2,
        sem_aexp_instant base R ck e v1
        -> sem_aexp_instant base R ck e v2
        -> v1 = v2.

    Lemma sem_exps_instant_det:
      forall les cs1 cs2,
        sem_exps_instant base R les cs1 ->
        sem_exps_instant base R les cs2 ->
        cs1 = cs2.

  End InstantDeterminism.

  Lemma sem_cexp_instant_det:
    forall base R e v1,
      sem_cexp_instant base R e v1 ->
      forall v2,
        sem_cexp_instant base R e v2 ->
        v1 = v2.

  Lemma sem_caexp_instant_det:
    forall base R ck e v1 v2,
      sem_caexp_instant base R ck e v1
      -> sem_caexp_instant base R ck e v2
      -> v1 = v2.

Lifted semantics

  Section LiftDeterminism.

    Variable bk : stream bool.
    Variable H : history.

    Ltac apply_lift sem_det :=
      intros; eapply lift_det; try eassumption;
      compute; intros; eapply sem_det; eauto.

    Ltac apply_lift' sem_det :=
      intros; eapply lift'_det; try eassumption;
      compute; intros; eapply sem_det; eauto.

    Lemma sem_exp_det:
      forall e xs1 xs2,
        sem_exp bk H e xs1 -> sem_exp bk H e xs2 -> xs1 = xs2.

    Lemma sem_exps_det:
      forall les cs1 cs2,
        sem_exps bk H les cs1 ->
        sem_exps bk H les cs2 ->
        cs1 = cs2.

    Lemma sem_aexp_det:
      forall ck e xs1 xs2,
        sem_aexp bk H ck e xs1 -> sem_aexp bk H ck e xs2 -> xs1 = xs2.

    Lemma sem_cexp_det:
      forall c xs1 xs2,
        sem_cexp bk H c xs1 -> sem_cexp bk H c xs2 -> xs1 = xs2.

    Lemma sem_caexp_det:
      forall ck c xs1 xs2,
        sem_caexp bk H ck c xs1 -> sem_caexp bk H ck c xs2 -> xs1 = xs2.

  End LiftDeterminism.


  Ltac sem_det :=
    match goal with
    | H1: sem_clock_instant ?bk ?H ?C ?X,
          H2: sem_clock_instant ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_clock_instant_det; eexact H1 || eexact H2
    | H1: sem_clock ?bk ?H ?C ?X,
          H2: sem_clock ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_clock_det; eexact H1 || eexact H2
    | H1: sem_cexp_instant ?bk ?H ?C ?X,
          H2: sem_cexp_instant ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_cexp_instant_det; eexact H1 || eexact H2
    | H1: sem_cexp ?bk ?H ?C ?X,
          H2: sem_cexp ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_cexp_det; eexact H1 || eexact H2
    | H1: sem_exps_instant ?bk ?H ?C ?X,
          H2: sem_exps_instant ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_exps_instant_det; eexact H1 || eexact H2
    | H1: sem_exps ?bk ?H ?C ?X,
          H2: sem_exps ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_exps_det; eexact H1 || eexact H2
    | H1: sem_exp_instant ?bk ?H ?C ?X,
          H2: sem_exp_instant ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_exp_instant_det; eexact H1 || eexact H2
    | H1: sem_exp ?bk ?H ?C ?X,
          H2: sem_exp ?bk ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_exp_det; eexact H1 || eexact H2
    | H1: sem_aexp_instant ?bk ?H ?CK ?C ?X,
          H2: sem_aexp_instant ?bk ?H ?CK ?C ?Y |- ?X = ?Y =>
      eapply sem_aexp_instant_det; eexact H1 || eexact H2
    | H1: sem_aexp ?bk ?H ?CK ?C ?X,
          H2: sem_aexp ?bk ?H ?CK ?C ?Y |- ?X = ?Y =>
      eapply sem_aexp_det; eexact H1 || eexact H2
    | H1: sem_var_instant ?H ?C ?X,
          H2: sem_var_instant ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_var_instant_det; eexact H1 || eexact H2
    | H1: sem_var ?H ?C ?X,
          H2: sem_var ?H ?C ?Y |- ?X = ?Y =>
      eapply sem_var_det; eexact H1 || eexact H2
    end.

  Ltac by_sem_det :=
    repeat match goal with
           | H: exists _, _ |- _ => destruct H
           end;
    match goal with
    | H1: sem_clock_instant ?bk ?H ?C ?X,
          H2: sem_clock_instant ?bk ?H ?C ?Y |- _ =>
      assert (X = Y) by (eapply sem_clock_instant_det; eexact H1 || eexact H2)
    | H1: sem_cexp_instant ?bk ?H ?C ?X,
          H2: sem_cexp_instant ?bk ?H ?C ?Y |- _ =>
      assert (X = Y) by (eapply sem_cexp_instant_det; eexact H1 || eexact H2)
    | H1: sem_exps_instant ?bk ?H ?C ?X,
          H2: sem_exps_instant ?bk ?H ?C ?Y |- _ =>
      assert (X = Y) by (eapply sem_exps_instant_det; eexact H1 || eexact H2)
    | H1: sem_exp_instant ?bk ?H ?C ?X,
          H2: sem_exp_instant ?bk ?H ?C ?Y |- _ =>
     assert (X = Y) by (eapply sem_exp_instant_det; eexact H1 || eexact H2)
    | H1: sem_aexp_instant ?bk ?H ?CK ?C ?X,
          H2: sem_aexp_instant ?bk ?H ?CK ?C ?Y |- _ =>
      assert (X = Y) by (eapply sem_aexp_instant_det; eexact H1 || eexact H2)
    | H1: sem_var_instant ?H ?C ?X,
          H2: sem_var_instant ?H ?C ?Y |- _ =>
      assert (X = Y) by (eapply sem_var_instant_det; eexact H1 || eexact H2)
    end; discriminate.

End CESEMANTICS.

Module CESemanticsFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Syn : CESYNTAX Ids Op OpAux Cks)
       (Str : INDEXEDSTREAMS Ids Op OpAux Cks)
  <: CESEMANTICS Ids Op OpAux Cks Syn Str.
  Include CESEMANTICS Ids Op OpAux Cks Syn Str.
End CESemanticsFun.