Module Qcert.cNNRC.Lang.cNNRCNorm


Section cNNRCNorm.
  Require Import String.
  Require Import List.
  Require Import Arith.
  Require Import EquivDec.
  Require Import Morphisms.
  Require Import Utils.
  Require Import CommonRuntime.
  Require Import cNNRC.

  Context {fruntime:foreign_runtime}.
  Context (h:brand_relation_t).
  Context (c:bindings).
 
cNNRC evaluation preserves data normalization.
  Lemma nnrc_core_eval_normalized env e {o} :
    Forall (data_normalized h) (map snd c) ->
    nnrc_core_eval h c env e = Some o ->
    Forall (data_normalized h) (map snd env) ->
    data_normalized h o.
Proof.
    revert env o. nnrc_cases (induction e) Case; simpl; intros env o Hc; intros.
    - Case "NNRCGetConstant"%string.
      rewrite Forall_forall in Hc.
      unfold edot in H. apply assoc_lookupr_in in H.
      apply (Hc o).
      rewrite in_map_iff.
      exists (v,o); eauto.
    - Case "NNRCVar"%string.
      rewrite Forall_forall in H0.
      apply lookup_in in H.
      apply (H0 o).
      rewrite in_map_iff.
      exists (v,o); eauto.
    - Case "NNRCConst"%string.
      inversion H; subst; intros.
      apply normalize_normalizes.
    - Case "NNRCBinop"%string.
      case_eq (nnrc_core_eval h c env e1); [intros ? eqq1 | intros eqq1];
      (rewrite eqq1 in *;
      case_eq (nnrc_core_eval h c env e2); [intros ? eqq2 | intros eqq2];
      rewrite eqq2 in *); simpl in *; try discriminate.
      eapply binary_op_eval_normalized; eauto.
    - Case "NNRCUnop"%string.
      case_eq (nnrc_core_eval h c env e); [intros ? eqq1 | intros eqq1];
      rewrite eqq1 in *;
        simpl in *; try discriminate.
      eapply unary_op_eval_normalized; eauto.
    - Case "NNRCLet"%string.
      case_eq (nnrc_core_eval h c env e1); [intros ? eqq1 | intros eqq1];
      rewrite eqq1 in *;
        simpl in *; try discriminate.
      case_eq (nnrc_core_eval h c ((v,d)::env) e2); [intros ? eqq2 | intros eqq2];
      rewrite eqq2 in *;
        simpl in *; try discriminate.
      inversion H; subst.
      eapply IHe2; eauto.
      constructor; eauto.
    - Case "NNRCFor"%string.
      case_eq (nnrc_core_eval h c env e1); [intros ? eqq1 | intros eqq1];
      rewrite eqq1 in *;
      simpl in *; try discriminate.
      destruct d; try discriminate.
      specialize (IHe1 _ _ Hc eqq1 H0).
      inversion IHe1; subst.
      apply some_lift in H.
      destruct H; subst.
      constructor.
      apply (lift_map_Forall e H2); intros.
      apply (IHe2 _ _ Hc H).
      constructor; eauto.
    - Case "NNRCIf"%string.
      case_eq (nnrc_core_eval h c env e1); [intros ? eqq1 | intros eqq1];
      rewrite eqq1 in *;
      simpl in *; try discriminate.
      destruct d; try discriminate.
      destruct b; eauto.
    - Case "NNRCEither"%string.
      case_eq (nnrc_core_eval h c env e1); [intros ? eqq1 | intros eqq1];
      rewrite eqq1 in *;
      simpl in *; try discriminate.
      specialize (IHe1 _ _ Hc eqq1 H0).
      destruct d; try discriminate; inversion IHe1; subst.
      + eapply IHe2; eauto.
         constructor; eauto.
      + eapply IHe3; eauto.
        constructor; eauto.
    - Case "NNRCGroupBy"%string.
      simpl; intros; congruence.
  Qed.

End cNNRCNorm.

Hint Resolve nnrc_core_eval_normalized.