Module NRA

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



  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.


  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.

    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.
  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.



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


Delimit Scope nra_scope with nra.

Notation "'ID'" := (AID) (at level 50) : nra_scope.
Notation "CGET⟨ s ⟩" := (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 "r1 ∧ r2" := (ABinop AAnd r1 r2) (right associativity, at level 65): nra_scope.
Notation "r1 ∨ r2" := (ABinop AOr r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ≐ r2" := (ABinop AEq r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ≤ r2" := (ABinop ALt r1 r2) (no associativity, at level 70): nra_scope.
Notation "r1 ⋃ r2" := (ABinop AUnion r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 − r2" := (ABinop AMinus r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ⋂min r2" := (ABinop AMin r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ⋃max r2" := (ABinop AMax r1 r2) (right associativity, at level 70): nra_scope.
Notation "p ⊕ r" := ((ABinop AConcat) p r) (at level 70) : nra_scope.
Notation "p ⊗ r" := ((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 "r1 ∥ r2" := (ADefault r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ◯ r2" := (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" ].