Module LambdaNRAtoNRAEnv

Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import BasicRuntime.

Section LambdaNRAtoNRAEnv.

  Require Import LambdaNRA NRAEnvRuntime.

  Context {fruntime:foreign_runtime}.

  Fixpoint lambda_nra_to_nraenv (op:lambda_nra) : nraenv :=
    match op with
    | LNRAVar x => NRAEnvUnop (ADot x) NRAEnvEnv
    | LNRATable x => NRAEnvGetConstant x
    | LNRAConst d => NRAEnvConst d
    | LNRABinop b op1 op2 => NRAEnvBinop b (lambda_nra_to_nraenv op1) (lambda_nra_to_nraenv op2)
    | LNRAUnop u op1 => NRAEnvUnop u (lambda_nra_to_nraenv op1)
    | LNRAMap lop1 op2 => NRAEnvMap (nraenv_of_lnra_lambda lop1) (lambda_nra_to_nraenv op2)
    | LNRAMapConcat lop1 op2 => NRAEnvMapConcat (nraenv_of_lnra_lambda lop1) (lambda_nra_to_nraenv op2)
    | LNRAProduct op1 op2 => NRAEnvProduct (lambda_nra_to_nraenv op1) (lambda_nra_to_nraenv op2)
    | LNRAFilter lop1 op2 => NRAEnvSelect (nraenv_of_lnra_lambda lop1) (lambda_nra_to_nraenv op2)
    end
  with nraenv_of_lnra_lambda (lop:lnra_lambda) : nraenv :=
    match lop with
    | LNRALambda x op =>
      NRAEnvAppEnv (lambda_nra_to_nraenv op) (NRAEnvBinop AConcat NRAEnvEnv (NRAEnvUnop (ARec x) NRAEnvID))
    end.

  Context (h:brand_relation_t).

  Section Translation.
    Context (global_env:bindings).

    Lemma lambda_nra_to_nraenv_never_uses_id :
      forall env:bindings, forall q:lambda_nra, forall d1 d2:data,
            nraenv_eval h global_env
                        (lambda_nra_to_nraenv q) (drec env) d1 =
            nraenv_eval h global_env
                        (lambda_nra_to_nraenv q) (drec env) d2.

Proof.

      lambda_nra_cases (induction q) Case
      ; intros; unfold nraenv_eval in *; simpl in *
      ; autorewrite with lambda_nra; try reflexivity.
      - Case "LNRABinop"%string.
        rewrite (IHq1 d1 d2).
        rewrite (IHq2 d1 d2).
        reflexivity.
      - Case "LNRAUnop"%string.
        rewrite (IHq d1 d2).
        reflexivity.
      - Case "LNRAMap"%string.
        rewrite (IHq2 d1 d2).
        reflexivity.
      - Case "LNRAMapConcat"%string.
        rewrite (IHq2 d1 d2).
        reflexivity.
      - Case "LNRAProduct"%string.
        rewrite (IHq1 d1 d2).
        rewrite (IHq2 d1 d2).
        reflexivity.
      - Case "LNRAFilter"%string.
        rewrite (IHq2 d1 d2).
        reflexivity.
    Qed.

Evaluation for lambda nra is the same as evaluation for translated expression to NRAEnv - Note that only the global and local environments matter. The 'input value' for NRA (d in the theorem) is not used on the LambdaNRA side. This is consistent with the previous theorem showing that any 'd' does not matter.

    Theorem lambda_nra_to_nraenv_correct :
      forall q:lambda_nra, forall env:bindings, forall d:data,
            lambda_nra_eval h global_env env q =
            nraenv_eval h global_env
                        (lambda_nra_to_nraenv q) (drec env) d.

Proof.

      lambda_nra_cases (induction q) Case
      ; intros; unfold nraenv_eval in *; simpl in *
      ; autorewrite with lambda_nra; try reflexivity.
      - Case "LNRABinop"%string.
        rewrite (IHq1 _ d).
        rewrite (IHq2 _ d).
        reflexivity.
      - Case "LNRAUnop"%string.
        rewrite (IHq _ d).
        reflexivity.
      - Case "LNRAMap"%string.
        rewrite <- (IHq2 _ d).
        simpl.
        apply olift_ext; intros.
        apply lift_oncoll_ext; intros.
        subst.
        f_equal.
        apply rmap_ext; intros.
        autorewrite with lambda_nra.
        rewrite (IHq1 _ x).
        reflexivity.
      - Case "LNRAMapConcat"%string.
        rewrite <- (IHq2 _ d).
        apply olift_ext; intros.
        apply lift_oncoll_ext; intros.
        subst.
        f_equal.
        apply rmap_concat_ext; intros.
        autorewrite with lambda_nra.
        rewrite (IHq1 _ x).
        reflexivity.
      - Case "LNRAProduct"%string.
        rewrite (IHq1 _ d).
        rewrite (IHq2 _ d).
        reflexivity.
      - Case "LNRAFilter"%string.
        rewrite <- (IHq2 _ d).
        apply olift_ext; intros.
        apply lift_oncoll_ext; intros.
        subst.
        f_equal.
        apply lift_filter_ext; intros.
        autorewrite with lambda_nra.
        rewrite (IHq1 _ x).
        reflexivity.
    Qed.

    Theorem nraenv_of_lnra_lambda_correct :
      forall env:bindings, forall lop:lnra_lambda, forall d:data,
            lnra_lambda_eval h global_env env lop d =
            nraenv_eval h global_env
                        (nraenv_of_lnra_lambda lop) (drec env) d.

Proof.

      destruct lop.
      revert env s.
      lambda_nra_cases (induction l) Case
      ; intros; unfold nraenv_eval in *; simpl in *
      ; autorewrite with lambda_nra.
      - Case "LNRAVar"%string.
        unfold edot, rec_concat_sort.
        rewrite assoc_lookupr_drec_sort.
        trivial.
      - Case "LNRATable"%string.
        unfold edot, rec_concat_sort.
        trivial.
      - Case "LNRAConst"%string.
        trivial.
      - Case "LNRABinop"%string.
        rewrite <- IHl1, <- IHl2.
        trivial.
      - Case "LNRAUnop"%string.
        rewrite <- IHl.
        trivial.
      - Case "LNRAMap"%string.
        rewrite <- IHl2.
        apply olift_ext; intros.
        apply lift_oncoll_ext; intros.
        subst.
        f_equal.
        apply rmap_ext; intros.
        rewrite IHl1.
        rewrite rec_sort_rec_sort_app1.
        trivial.
      - Case "LNRAMapConcat"%string.
        rewrite <- IHl2.
        apply olift_ext; intros.
        apply lift_oncoll_ext; intros.
        subst.
        f_equal.
        apply rmap_concat_ext; intros.
        rewrite IHl1.
        rewrite rec_sort_rec_sort_app1.
        trivial.
      - Case "LNRAProduct"%string.
        rewrite <- IHl1, <- IHl2.
        trivial.
      - Case "LNRAFilter"%string.
        rewrite <- IHl2.
        apply olift_ext; intros.
        apply lift_oncoll_ext; intros.
        subst.
        f_equal.
        apply lift_filter_ext; intros.
        rewrite IHl1.
        rewrite rec_sort_rec_sort_app1.
        trivial.
    Qed.

    Definition eval_nraenv_q (Qe:nraenv) (input:data) : option data :=
      nraenv_eval h global_env Qe (drec nil) input.

    Theorem eval_nraenv_q_correct (Q:lambda_nra -> lambda_nra) (input:data) :
      lnra_lambda_eval_top h Q global_env input = eval_nraenv_q (nraenv_of_lnra_lambda (q_to_lambda Q)) input.

Proof.

      unfold lnra_lambda_eval_top, eval_nraenv_q.
      rewrite nraenv_of_lnra_lambda_correct.
      reflexivity.
    Qed.

  End Translation.

  Section Top.
    Definition lambda_nra_to_nraenv_top (q:lambda_nra) : nraenv :=
      lambda_nra_to_nraenv q.

    Theorem lambda_nra_to_nraenv_top_correct :
      forall q:lambda_nra, forall global_env:bindings,
          lambda_nra_eval_top h q global_env =
          nraenv_eval_top h (lambda_nra_to_nraenv_top q) global_env.

Proof.

      intros.
      unfold lambda_nra_to_nraenv_top.
      unfold lambda_nra_eval_top.
      unfold nraenv_eval_top.
      rewrite (lambda_nra_to_nraenv_correct (rec_sort global_env) q nil dunit).
      reflexivity.
    Qed.

End Top.

End LambdaNRAtoNRAEnv.