Module Qcert.NRA.Lang.NRA


Section NRA.
  Require Import String List Compare_dec.
  Require Import EquivDec.
  
  Require Import Utils BasicRuntime.

Nested Relational Algebra

By convention, "static" parameters come first, followed by dependent operators. This allows for instanciation on those parameters

  Context {fruntime:foreign_runtime}.
  
  Inductive nra : Set :=
  | AID : nra
  | AConst : data -> nra
  | ABinop : binOp -> nra -> nra -> nra
  | AUnop : unaryOp -> nra -> nra
  | AMap : nra -> nra -> nra
  | AMapConcat : nra -> nra -> nra
  | AProduct : nra -> nra -> nra
  | ASelect : nra -> nra -> nra
  | ADefault : nra -> nra -> nra
  | AEither : nra -> nra -> nra
  | AEitherConcat : nra -> nra -> nra
  | AApp : nra -> nra -> nra
  | AGetConstant : string -> nra
  .

  Global Instance nra_eqdec : EqDec nra eq.
Proof.
    change (forall x y : nra, {x = y} + {x <> y}).
    decide equality;
    try solve [apply binOp_eqdec | apply unaryOp_eqdec | apply data_eqdec | apply string_eqdec].
  Qed.

NRA Semantics

  Context (h:list(string*string)).
  Section Semantics.
    Context (constant_env:list (string*data)).
  
    Fixpoint nra_eval (op:nra) (x:data) : option data :=
      match op with
      | AID => Some x
      | AConst rd => Some (normalize_data h rd)
      | ABinop bop op1 op2 =>
        olift2 (fun d1 d2 => fun_of_binop h bop d1 d2) (nra_eval op1 x) (nra_eval op2 x)
      | AUnop uop op1 =>
        olift (fun d1 => fun_of_unaryop h uop d1) (nra_eval op1 x)
      | AMap op1 op2 =>
        let aux_map d :=
            lift_oncoll (fun c1 => lift dcoll (rmap (nra_eval op1) c1)) d
        in olift aux_map (nra_eval op2 x)
      | AMapConcat op1 op2 =>
        let aux_mapconcat d :=
            lift_oncoll (fun c1 => lift dcoll (rmap_concat (nra_eval op1) c1)) d
        in olift aux_mapconcat (nra_eval op2 x)
      | AProduct op1 op2 =>
        let aux_product d :=
            lift_oncoll (fun c1 => lift dcoll (rmap_concat (fun _ => nra_eval op2 x) c1)) d
        in olift aux_product (nra_eval op1 x)
      | ASelect op1 op2 =>
        let pred x' :=
            match nra_eval op1 x' with
              | Some (dbool b) => Some b
              | _ => None
            end
        in
        let aux_select d :=
            lift_oncoll (fun c1 => lift dcoll (lift_filter pred c1)) d
        in
        olift aux_select (nra_eval op2 x)
      | ADefault op1 op2 =>
        olift (fun d1 => match d1 with
                           | dcoll nil => nra_eval op2 x
                           | _ => Some d1
                         end) (nra_eval op1 x)
      | AEither opl opr =>
        match x with
          | dleft dl => nra_eval opl dl
          | dright dr => nra_eval opr dr
          | _ => None
        end
      | AEitherConcat op1 op2 =>
        match nra_eval op1 x, nra_eval op2 x with
          | Some (dleft (drec l)), Some (drec t) =>
            Some (dleft (drec (rec_concat_sort l t)))
          | Some (dright (drec r)), Some (drec t) =>
            Some (dright (drec (rec_concat_sort r t)))
          | _, _ => None
        end
      | AApp op1 op2 =>
        olift (fun d => (nra_eval op1 d)) (nra_eval op2 x)
      | AGetConstant s => edot constant_env s
    end.

    Lemma data_normalized_orecconcat {x y z}:
      orecconcat x y = Some z ->
      data_normalized h x -> data_normalized h y ->
      data_normalized h z.
Proof.
      destruct x; simpl; try discriminate.
      destruct y; simpl; try discriminate.
      inversion 1; subst.
      apply data_normalized_rec_concat_sort; trivial.
    Qed.

    Lemma nra_eval_normalized {op:nra} {d:data} {o} :
      Forall (fun x => data_normalized h (snd x)) constant_env ->
      nra_eval op d = Some o ->
      data_normalized h d ->
      data_normalized h o.
Proof.
      intro HconstNorm.
      revert d o.
      induction op; simpl.
      - inversion 1; subst; trivial.
      - inversion 1; subst; intros.
        apply normalize_normalizes.
      - intros.
        specialize (IHop1 d).
        specialize (IHop2 d).
        destruct (nra_eval op1 d); simpl in *; try discriminate.
        destruct (nra_eval op2 d); simpl in *; try discriminate.
        apply (fun_of_binop_normalized h) in H; eauto.
      - intros.
        specialize (IHop d).
        destruct (nra_eval op d); simpl in *; try discriminate.
        apply fun_of_unaryop_normalized in H; eauto.
      - intros;
          specialize (IHop2 d);
          destruct (nra_eval op2 d); simpl in *; try discriminate;
            specialize (IHop2 _ (eq_refl _) H0).
        destruct d0; simpl in *; try discriminate.
        apply some_lift in H; destruct H; subst.
        constructor.
        inversion IHop2; subst.
        apply (rmap_Forall e H1); eauto.
      - intros;
          specialize (IHop2 d);
          destruct (nra_eval op2 d); simpl in *; try discriminate;
            specialize (IHop2 _ (eq_refl _) H0).
        destruct d0; simpl in *; try discriminate.
        apply some_lift in H; destruct H; subst.
        constructor.
        inversion IHop2; subst.
        unfold rmap_concat in *.
        apply (oflat_map_Forall e H1); intros.
        specialize (IHop1 x0).
        unfold oomap_concat in H.
        match_destr_in H.
        specialize (IHop1 _ (eq_refl _) H2).
        unfold omap_concat in H.
        match_destr_in H.
        inversion IHop1; subst.
        apply (rmap_Forall H H4); intros.
        eapply (data_normalized_orecconcat H3); trivial.
      - intros;
           specialize (IHop1 d);
           destruct (nra_eval op1 d); simpl in *; try discriminate.
         specialize (IHop1 _ (eq_refl _) H0).
         destruct d0; simpl in *; try discriminate.
         apply some_lift in H; destruct H; subst.
         constructor.
         inversion IHop1; subst.
         unfold rmap_concat in *.
         apply (oflat_map_Forall e H1); intros.
         specialize (IHop2 d).
         unfold oomap_concat in H.
         match_destr_in H.
         specialize (IHop2 _ (eq_refl _) H0).
         unfold omap_concat in H.
         match_destr_in H.
         inversion IHop2; subst.
         apply (rmap_Forall H H4); intros.
         eapply (data_normalized_orecconcat H3); trivial.
      - intros;
          specialize (IHop2 d);
          destruct (nra_eval op2 d); simpl in *; try discriminate;
            specialize (IHop2 _ (eq_refl _) H0).
        destruct d0; simpl in *; try discriminate.
        apply some_lift in H; destruct H; subst.
        constructor.
        inversion IHop2; subst.
        unfold rmap_concat in *.
        apply (lift_filter_Forall e H1).
      - intros;
          specialize (IHop1 d);
          destruct (nra_eval op1 d); simpl in *; try discriminate.
        specialize (IHop1 _ (eq_refl _) H0).
        destruct d0; simpl in *; try solve [inversion H; subst; trivial].
        destruct l; simpl; eauto 3.
        inversion H; subst; trivial.
      - intros.
        destruct d; try discriminate; inversion H0; subst; eauto.
      - intros.
        specialize (IHop1 d).
        specialize (IHop2 d).
        destruct (nra_eval op1 d); simpl in *; try discriminate.
        destruct (nra_eval op2 d); simpl in *; try discriminate.
        specialize (IHop1 _ (eq_refl _) H0).
        specialize (IHop2 _ (eq_refl _) H0).
        destruct d0; try discriminate.
        + destruct d0; try discriminate.
          destruct d1; try discriminate.
          inversion IHop1; subst.
          inversion H; subst.
          constructor.
          apply data_normalized_rec_concat_sort; trivial.
        + destruct d0; try discriminate.
          destruct d1; try discriminate.
          inversion IHop1; subst.
          inversion H; subst.
          constructor.
          apply data_normalized_rec_concat_sort; trivial.
        + repeat (destruct d0; try discriminate).
      - intros. specialize (IHop2 d).
        destruct (nra_eval op2 d); simpl in *; try discriminate.
        eauto.
      - intros.
        unfold edot in H.
        apply assoc_lookupr_in in H.
        rewrite Forall_forall in HconstNorm.
        specialize (HconstNorm (s,o)); simpl in *.
        auto.
    Qed.
  End Semantics.
  
  Section Top.
    Definition nra_eval_top (q:nra) (cenv:bindings) : option data :=
      nra_eval (rec_sort cenv) q dunit.
  End Top.

  Section FreeVars.
    Fixpoint nra_free_variables (q:nra) : list string :=
      match q with
      | AID => nil
      | AConst _ => nil
      | ABinop _ q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | AUnop _ q1 =>
        (nra_free_variables q1)
      | AMap q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | AMapConcat q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | AProduct q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | ASelect q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | ADefault q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | AEither ql qr =>
        app (nra_free_variables ql) (nra_free_variables qr)
      | AEitherConcat q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | AApp q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | AGetConstant s => s :: nil
    end.
  End FreeVars.

End NRA.


Nraebraic plan application

Notation "hOp @ₐ xc" := (nra_eval h c Op x) (at level 10).


Delimit Scope nra_scope with nra.

Notation "'ID'" := (AID) (at level 50) : nra_scope.
Notation "CGETs ⟩" := (AGetConstant s) (at level 50) : nra_core_scope.

Notation "‵‵ c" := (AConst (dconst c)) (at level 0) : nra_scope.
Notation "‵ c" := (AConst c) (at level 0) : nra_scope.
Notation "‵{||}" := (AConst (dcoll nil)) (at level 0) : nra_scope.
Notation "‵[||]" := (AConst (drec nil)) (at level 50) : nra_scope.

Notation "r1r2" := (ABinop AAnd r1 r2) (right associativity, at level 65): nra_scope.
Notation "r1r2" := (ABinop AOr r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1r2" := (ABinop AEq r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1r2" := (ABinop ALt r1 r2) (no associativity, at level 70): nra_scope.
Notation "r1r2" := (ABinop AUnion r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1r2" := (ABinop AMinus r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1min r2" := (ABinop AMin r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1max r2" := (ABinop AMax r1 r2) (right associativity, at level 70): nra_scope.
Notation "pr" := ((ABinop AConcat) p r) (at level 70) : nra_scope.
Notation "pr" := ((ABinop AMergeConcat) p r) (at level 70) : nra_scope.

Notation "¬( r1 )" := (AUnop ANeg r1) (right associativity, at level 70): nra_scope.
Notation "ε( r1 )" := (AUnop ADistinct r1) (right associativity, at level 70): nra_scope.
Notation "♯count( r1 )" := (AUnop ACount r1) (right associativity, at level 70): nra_scope.
Notation "♯flatten( d )" := (AUnop AFlatten d) (at level 50) : nra_scope.
Notation "‵{| d |}" := ((AUnop AColl) d) (at level 50) : nra_scope.
Notation "‵[| ( s , r ) |]" := ((AUnop (ARec s)) r) (at level 50) : nra_scope.
Notation "¬π[ s1 ]( r )" := ((AUnop (ARecRemove s1)) r) (at level 50) : nra_scope.
Notation "π[ s1 ]( r )" := ((AUnop (ARecProject s1)) r) (at level 50) : nra_scope.
Notation "p · r" := ((AUnop (ADot r)) p) (left associativity, at level 40): nra_scope.

Notation "χ⟨ p ⟩( r )" := (AMap p r) (at level 70) : nra_scope.
Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (AMapConcat e2 e1) (at level 70) : nra_scope.
Notation "r1 × r2" := (AProduct r1 r2) (right associativity, at level 70): nra_scope.
Notation "σ⟨ p ⟩( r )" := (ASelect p r) (at level 70) : nra_scope.
Notation "r1r2" := (ADefault r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1r2" := (AApp r1 r2) (right associativity, at level 60): nra_scope.

Hint Resolve nra_eval_normalized.

Local Open Scope string_scope.
Tactic Notation "nra_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "AID"
  | Case_aux c "AConst"
  | Case_aux c "ABinop"
  | Case_aux c "AUnop"
  | Case_aux c "AMap"
  | Case_aux c "AMapConcat"
  | Case_aux c "AProduct"
  | Case_aux c "ASelect"
  | Case_aux c "ADefault"
  | Case_aux c "AEither"
  | Case_aux c "AEitherConcat"
  | Case_aux c "AApp"
  | Case_aux c "AGetConstant" ].