Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.

Declare Scope nra_scope.

Section NRA.
  Context {fruntime:foreign_runtime}.
  

Abstract Syntax

  Section Syntax.
  

    Inductive nra : Set :=
    | NRAGetConstant : string -> nra (* global variable lookup ($$v) *)
    | NRAID : nra (* current value (ID) *)
    | NRAConst : data -> nra (* constant data (d) *)
    | NRABinop : binary_op -> nra -> nra -> nra (* binary operator (e₁ ⊠ e₂) *)
    | NRAUnop : unary_op -> nra -> nra (* unary operator (⊞ e) *)
    | NRAMap : nra -> nra -> nra (* map operator (χ⟨e₂⟩(e₁)) *)
    | NRAMapProduct : nra -> nra -> nra (* dependent product operator (⋈ᵈ⟨e₂⟩(e₁)) *)
    | NRAProduct : nra -> nra -> nra (* product operator (e₁ × e₂) *)
    | NRASelect : nra -> nra -> nra (* selection operator (σ⟨e₂⟩(e₁)) *)
    | NRADefault : nra -> nra -> nra (* default operator (e₁ ∥ e₂) *)
    | NRAEither : nra -> nra -> nra (* either operator (either e₁ e₂) *)
    | NRAEitherConcat : nra -> nra -> nra (* either-concat operator (either⊕ e₁ e₂) *)
    | NRAApp : nra -> nra -> nra. (* compose operator (e₂ ∘ e₁) *)

    Tactic Notation "nra_cases" tactic(first) ident(c) :=
      first;
      [ Case_aux c "NRAGetConstant"%string
      | Case_aux c "NRAID"%string
      | Case_aux c "NRAConst"%string
      | Case_aux c "NRABinop"%string
      | Case_aux c "NRAUnop"%string
      | Case_aux c "NRAMap"%string
      | Case_aux c "NRAMapProduct"%string
      | Case_aux c "NRAProduct"%string
      | Case_aux c "NRASelect"%string
      | Case_aux c "NRADefault"%string
      | Case_aux c "NRAEither"%string
      | Case_aux c "NRAEitherConcat"%string
      | Case_aux c "NRAApp"%string ].

  
    Global Instance nra_eqdec : EqDec nra eq.

  End Syntax.

Semantics

  
  Section Semantics.

    Context (h:list(string*string)).
    Context (constant_env:list (string*data)).

Denotational Semantics

    
    
    
    
    Section Denotation.
      Inductive nra_sem: nra -> data -> data -> Prop :=
      | sem_NRAGetConstant : forall v d d1,
          edot constant_env v = Some d1 -> (* Γc(v) = d₁ *)
          nra_sem (NRAGetConstant v) d d1 (* ⇒ Γc ; d ⊢〚$$v〛⇓ d₁ *)
      | sem_NRAID : forall d,
          nra_sem NRAID d d (* Γc ; d ⊢ ID ⇓ d *)
      | sem_NRAConst : forall d d1 d2,
          normalize_data h d1 = d2 -> (* norm(d₁) = d₂ *)
          nra_sem (NRAConst d1) d d2 (* ⇒ Γc ; d ⊢〚d₁〛⇓ d₂ *)
      | sem_NRABinop : forall bop e1 e2 d d1 d2 d3,
          nra_sem e1 d d1 -> (* Γc ; d ⊢〚e₁〛⇓ d₁ *)
          nra_sem e2 d d2 -> (* ∧ Γc ; d ⊢〚e₂〛⇓ d₂ *)
          binary_op_eval h bop d1 d2 = Some d3 -> (* ∧ d₁ ⊠ d₂ = d₃ *)
          nra_sem (NRABinop bop e1 e2) d d3 (* ⇒ Γc ; d ⊢〚e₁ ⊠ e₂〛⇓ d₃ *)
      | sem_NRAUnop : forall uop e d d1 d2,
          nra_sem e d d1 -> (* Γc ; d ⊢〚e〛⇓ d₁ *)
          unary_op_eval h uop d1 = Some d2 -> (* ∧ ⊞ d₁ = d₂ *)
          nra_sem (NRAUnop uop e) d d2 (* ⇒ Γc ; d ⊢〚⊞ e〛⇓ d₂ *)
      | sem_NRAMap : forall e1 e2 d c1 c2,
          nra_sem e1 d (dcoll c1) -> (* Γc ; d ⊢〚e₁〛⇓ {c₁} *)
          nra_sem_map e2 c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e₂〛χ ⇓ {c₂} *)
          nra_sem (NRAMap e2 e1) d (dcoll c2) (* ⇒ Γc ; d ⊢〚χ⟨e₂⟩(e₁)〛⇓ {c₂} *)
      | sem_NRAMapProduct : forall e1 e2 d c1 c2,
          nra_sem e1 d (dcoll c1) -> (* Γc ; d ⊢〚e₁〛⇓ {c₁} *)
          nra_sem_map_product e2 c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e₂〛⋈ᵈ ⇓ {c₂} *)
          nra_sem (NRAMapProduct e2 e1) d (dcoll c2) (* ⇒ Γc ; d ⊢〚⋈ᵈ⟨e₂⟩(e₁)〛⇓ {c₂} *)
      | sem_NRAProduct_empty : forall e1 e2 d, (* Does not evaluate e₂ if e₁ is empty. This facilitates translation to cNNRC *)
          nra_sem e1 d (dcoll nil) -> (* Γc ; d ⊢〚e₁〛⇓ {} *)
          nra_sem (NRAProduct e1 e2) d (dcoll nil) (* ⇒ Γc ; d ⊢〚e₁ × e₂〛⇓ {} *)
      | sem_NRAProduct_nonEmpty : forall e1 e2 d c1 c2 c3,
          nra_sem e1 d (dcoll c1) -> (* Γc ; d ⊢〚e₁〛⇓ {c₁} *)
          c1 <> nil -> (* ∧ {c₁} ≠ {} *)
          nra_sem e2 d (dcoll c2) -> (* ∧ Γc ; d ⊢〚e₂〛⇓ {c₂} *)
          product_sem c1 c2 c3 -> (* ∧ {c₁} × {c₂} ⇓ {c₃} *)
          nra_sem (NRAProduct e1 e2) d (dcoll c3) (* ⇒ Γc ; d ⊢〚e₁ × e₂〛⇓ {c₃} *)
      | sem_NRASelect : forall e1 e2 d c1 c2,
          nra_sem e1 d (dcoll c1) -> (* Γc ; d ⊢〚e₁〛⇓ {c₁} *)
          nra_sem_select e2 c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e₂〛σ ⇓ {c₂} *)
          nra_sem (NRASelect e2 e1) d (dcoll c2) (* ⇒ Γc ; d ⊢〚σ⟨e₂⟩(e₁)〛⇓ {c₂} *)
      | sem_NRADefault_empty : forall e1 e2 d d2,
          nra_sem e1 d (dcoll nil) -> (* Γc ; d ⊢〚e₁〛⇓ {} *)
          nra_sem e2 d d2 -> (* ∧ Γc ; d ⊢〚e₂〛⇓ d₂ *)
          nra_sem (NRADefault e1 e2) d d2 (* ⇒ Γc ; d ⊢〚e₁ ∥ e₂〛⇓ d₂ *)
      | sem_NRADefault_not_empty : forall e1 e2 d d1,
          nra_sem e1 d d1 -> (* Γc ; d ⊢〚e₁〛⇓ d₁ *)
          d1 <> dcoll nil -> (* ∧ d₁ ≠ {} *)
          nra_sem (NRADefault e1 e2) d d1 (* ⇒ Γc ; d ⊢〚e₁ ∥ e₂〛⇓ d₁ *)
      | sem_NRAEither_left : forall e1 e2 d d1,
          nra_sem e1 d d1 -> (* Γc ; d ⊢〚e₁〛⇓ d₁ *)
          nra_sem (NRAEither e1 e2) (dleft d) d1 (* ⇒ Γc ; (dleft d) ⊢〚either e₁ e₂〛⇓ d₁ *)
      | sem_NRAEither_right : forall e1 e2 d d2,
          nra_sem e2 d d2 -> (* Γc ; d ⊢〚e₂〛⇓ d₂ *)
          nra_sem (NRAEither e1 e2) (dright d) d2 (* ⇒ Γc ; (dright d) ⊢〚either e₁ e₂〛⇓ d₂ *)
      | sem_NRAEitherConcat_left : forall e1 e2 d r1 r2,
          nra_sem e1 d (dleft (drec r1)) -> (* Γc ; d ⊢〚e₁〛⇓ (dleft [r₁]) *)
          nra_sem e2 d (drec r2) -> (* ∧ Γc ; d ⊢〚e₂〛⇓ [r₂] *)
          nra_sem (NRAEitherConcat e1 e2) d (* ⇒ Γc ; d ⊢〚either⊕ e₁ e₂〛⇓ (dleft [r₁]⊕[r₂]) *)
                  (dleft (drec (rec_concat_sort r1 r2)))
      | sem_NRAEitherConcat_right : forall e1 e2 d r1 r2,
          nra_sem e1 d (dright (drec r1)) -> (* Γc ; d ⊢〚e₁〛⇓ (dright [r₁]) *)
          nra_sem e2 d (drec r2) -> (* ∧ Γc ; d ⊢〚e₂〛⇓ [r₂] *)
          nra_sem (NRAEitherConcat e1 e2) d (* ⇒ Γc ; d ⊢〚either⊕ e₁ e₂〛⇓ (dright [r₁]⊕[r₂]) *)
                  (dright (drec (rec_concat_sort r1 r2)))
      | sem_NRAApp : forall e1 e2 d d1 d2,
          nra_sem e1 d d1 -> (* Γc ; d ⊢〚e₁〛⇓ d₁ *)
          nra_sem e2 d1 d2 -> (* Γc ; d₁ ⊢〚e₂〛⇓ d₂ *)
          nra_sem (NRAApp e2 e1) d d2 (* ⇒ Γc ; d ⊢〚e₂ ∘ e₁〛⇓ d₂ *)
      with nra_sem_map: nra -> list data -> list data -> Prop :=
      | sem_NRAMap_empty : forall e,
          nra_sem_map e nil nil (* Γc ; {} ⊢〚e〛χ ⇓ {} *)
      | sem_NRAMap_cons : forall e d1 c1 d2 c2,
          nra_sem e d1 d2 -> (* Γc ; d₁ ⊢〚e〛⇓ d₂ *)
          nra_sem_map e c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e〛χ ⇓ {c₂} *)
          nra_sem_map e (d1::c1) (d2::c2) (* ⇒ Γc ; {d₁::c₁} ⊢〚e〛χ ⇓ {d₂::c₂} *)
      with nra_sem_map_product: nra -> list data -> list data -> Prop :=
      | sem_NRAMapProduct_empty : forall e,
          nra_sem_map_product e nil nil (* Γc ; {} ⊢〚e〛⋈ᵈ ⇓ {} *)
      | sem_NRAMapProduct_cons : forall e d1 c1 c2 c3 c4,
          nra_sem e d1 (dcoll c3) -> (* Γc ; d₁ ⊢〚e〛⋈ᵈ ⇓ {c₃} *)
          map_concat_sem d1 c3 c4 -> (* ∧ d₁ χ⊕ c₃ ⇓ c₄ *)
          nra_sem_map_product e c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e〛⋈ᵈ ⇓ {c₂} *)
          nra_sem_map_product e (d1::c1) (c4 ++ c2) (* ⇒ Γc ; {d₁::c₁} ⊢〚e〛⋈ᵈ ⇓ {c₄}∪{c₂} *)
      with nra_sem_select: nra -> list data -> list data -> Prop :=
      | sem_NRASelect_empty : forall e,
          nra_sem_select e nil nil (* Γc ; {} ⊢〚e〛σ ⇓ {} *)
      | sem_NRASelect_true : forall e d1 c1 c2,
          nra_sem e d1 (dbool true) -> (* Γc ; d₁ ⊢〚e〛σ ⇓ true *)
          nra_sem_select e c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e〛σ ⇓ {c₂} *)
          nra_sem_select e (d1::c1) (d1::c2) (* ⇒ Γc ; {d₁::c₁} ⊢〚e〛σ ⇓ {d₁::c₂} *)
      | sem_NRASelect_false : forall e d1 c1 c2,
          nra_sem e d1 (dbool false) -> (* Γc ; d₁ ⊢〚e〛σ ⇓ false *)
          nra_sem_select e c1 c2 -> (* ∧ Γc ; {c₁} ⊢〚e〛σ ⇓ {c₂} *)
          nra_sem_select e (d1::c1) c2 (* ⇒ Γc ; {d₁::c₁} ⊢〚e〛σ ⇓ {c₂} *)
      .

    End Denotation.

    Section Evaluation.
      
      Fixpoint nra_eval (e:nra) (din:data) : option data :=
        match e with
        | NRAGetConstant s =>
          edot constant_env s
        | NRAID =>
          Some din
        | NRAConst d =>
          Some (normalize_data h d)
        | NRABinop bop e1 e2 =>
          olift2
            (fun d1 d2 => binary_op_eval h bop d1 d2)
            (nra_eval e1 din) (nra_eval e2 din)
        | NRAUnop uop e =>
          olift (fun d1 => unary_op_eval h uop d1) (nra_eval e din)
        | NRAMap e2 e1 =>
          let aux_map c1 :=
              lift_oncoll (fun d1 => lift dcoll (lift_map (nra_eval e2) d1)) c1
          in olift aux_map (nra_eval e1 din)
        | NRAMapProduct e2 e1 =>
          let aux_mapconcat c1 :=
              lift_oncoll (fun d1 => lift dcoll (omap_product (nra_eval e2) d1)) c1
          in olift aux_mapconcat (nra_eval e1 din)
        | NRAProduct e1 e2 =>
          let aux_product d :=
              lift_oncoll
                (fun c1 => lift dcoll (omap_product (fun _ => nra_eval e2 din) c1)) d
          in olift aux_product (nra_eval e1 din)
        | NRASelect e2 e1 =>
          let pred d1 :=
              match nra_eval e2 d1 with
              | Some (dbool b) => Some b
              | _ => None
              end
          in
          let aux_select d :=
              lift_oncoll (fun d1 => lift dcoll (lift_filter pred d1)) d
          in
          olift aux_select (nra_eval e1 din)
        | NRADefault e1 e2 =>
          olift (fun d1 =>
                   match d1 with
                   | dcoll nil => nra_eval e2 din
                   | _ => Some d1
                   end)
                (nra_eval e1 din)
        | NRAEither e1 e2 =>
          match din with
          | dleft d1 => nra_eval e1 d1
          | dright d2 => nra_eval e2 d2
          | _ => None
          end
        | NRAEitherConcat e1 e2 =>
          match nra_eval e1 din, nra_eval e2 din 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
        | NRAApp e2 e1 =>
          olift (fun d1 => (nra_eval e2 d1)) (nra_eval e1 din)
        end.
    End Evaluation.

    Section EvalCorrect.
      Lemma nra_eval_map_correct : forall e l1 l2,
        (forall d1 d2 : data, nra_eval e d1 = Some d2 -> nra_sem e d1 d2) ->
        lift_map (nra_eval e) l1 = Some l2 ->
        nra_sem_map e l1 l2.
          
      Lemma nra_eval_map_product_correct : forall e l1 l2,
        (forall d1 d2 : data, nra_eval e d1 = Some d2 -> nra_sem e d1 d2) ->
        omap_product (nra_eval e) l1 = Some l2 ->
        nra_sem_map_product e l1 l2.

      Lemma nra_eval_select_correct e l1 l2 :
        (forall d1 d2 : data, nra_eval e d1 = Some d2 -> nra_sem e d1 d2) ->
        lift_filter
          (fun d1 : data =>
             match nra_eval e d1 with
             | Some dunit => None
             | Some (dnat _) => None
             | Some (dfloat _) => None
             | Some (dbool b) => Some b
             | Some (dstring _) => None
             | Some (dcoll _) => None
             | Some (drec _) => None
             | Some (dleft _) => None
             | Some (dright _) => None
             | Some (dbrand _ _) => None
             | Some (dforeign _) => None
             | None => None
             end) l1 = Some l2 ->
        nra_sem_select e l1 l2.

      Lemma omap_product_some_is_oproduct d1 d2 l1 l2 :
        omap_product (fun _ : data => Some d2) (d1 :: l1) = Some l2 ->
        exists l, d2 = dcoll l /\ oproduct (d1::l1) l = Some l2.


      Lemma nra_eval_correct : forall e d1 d2,
          nra_eval e d1 = Some d2 ->
          nra_sem e d1 d2.
 

      Lemma nra_map_eval_complete e c1 c2:
        (forall d1 d2 : data, nra_sem e d1 d2 -> nra_eval e d1 = Some d2) ->
        (nra_sem_map e c1 c2) ->
        lift dcoll (lift_map (nra_eval e) c1) = Some (dcoll c2).
        
      Lemma nra_map_product_eval_complete e c1 c2:
        (forall d1 d2 : data, nra_sem e d1 d2 -> nra_eval e d1 = Some d2) ->
        (nra_sem_map_product e c1 c2) ->
        lift dcoll (omap_product (nra_eval e) c1) = Some (dcoll c2).
        
      Lemma nra_select_eval_complete e c1 c2:
        (forall d1 d2 : data, nra_sem e d1 d2 -> nra_eval e d1 = Some d2) ->
        (nra_sem_select e c1 c2) ->
        lift dcoll
             (lift_filter
                (fun d0 : data =>
                   match nra_eval e d0 with
                   | Some dunit => None
                   | Some (dnat _) => None
                   | Some (dfloat _) => None
                   | Some (dbool b) => Some b
                   | Some (dstring _) => None
                   | Some (dcoll _) => None
                   | Some (drec _) => None
                   | Some (dleft _) => None
                   | Some (dright _) => None
                   | Some (dbrand _ _) => None
                   | Some (dforeign _) => None
                   | None => None
                   end) c1) = Some (dcoll c2).


      Lemma nra_eval_complete : forall e d1 d2,
          nra_sem e d1 d2 ->
          nra_eval e d1 = Some d2.

      
      Theorem nra_eval_correct_and_complete : forall e d d',
          nra_eval e d = Some d' <-> nra_sem e d d'.

    End EvalCorrect.

    Section EvalNormalized.
      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 EvalNormalized.
  End Semantics.
  
  Section Top.
    Context (h:list(string*string)).
    Definition nra_eval_top (q:nra) (cenv:bindings) : option data :=
      nra_eval h (rec_sort cenv) q dunit.
  End Top.

  Section FreeVars.
    Fixpoint nra_free_variables (q:nra) : list string :=
      match q with
      | NRAGetConstant s => s :: nil
      | NRAID => nil
      | NRAConst _ => nil
      | NRABinop _ q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRAUnop _ q1 =>
        (nra_free_variables q1)
      | NRAMap q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRAMapProduct q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRAProduct q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRASelect q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRADefault q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRAEither ql qr =>
        app (nra_free_variables ql) (nra_free_variables qr)
      | NRAEitherConcat q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
      | NRAApp q1 q2 =>
        app (nra_free_variables q1) (nra_free_variables q2)
    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'" := (NRAID) (at level 50) : nra_scope.
Notation "TABLE⟨ s ⟩" := (NRAGetConstant s) (at level 50) : nra_scope.
Notation "‵‵ c" := (NRAConst (dconst c)) (at level 0) : nra_scope.
Notation "‵ c" := (NRAConst c) (at level 0) : nra_scope.
Notation "‵{||}" := (NRAConst (dcoll nil)) (at level 0) : nra_scope.
Notation "‵[||]" := (NRAConst (drec nil)) (at level 50) : nra_scope.

Notation "r1 ∧ r2" := (NRABinop OpAnd r1 r2) (right associativity, at level 65): nra_scope.
Notation "r1 ∨ r2" := (NRABinop OpOr r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ≐ r2" := (NRABinop OpEqual r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ≤ r2" := (NRABinop OpLt r1 r2) (no associativity, at level 70): nra_scope.
Notation "r1 ⋃ r2" := (NRABinop OpBagUnion r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 − r2" := (NRABinop OpBagDiff r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ⋂min r2" := (NRABinop OpBagMin r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ⋃max r2" := (NRABinop OpBagMax r1 r2) (right associativity, at level 70): nra_scope.
Notation "p ⊕ r" := ((NRABinop OpRecConcat) p r) (at level 70) : nra_scope.
Notation "p ⊗ r" := ((NRABinop OpRecMerge) p r) (at level 70) : nra_scope.

Notation "¬( r1 )" := (NRAUnop OpNeg r1) (right associativity, at level 70): nra_scope.
Notation "ε( r1 )" := (NRAUnop OpDistinct r1) (right associativity, at level 70): nra_scope.
Notation "♯count( r1 )" := (NRAUnop OpCount r1) (right associativity, at level 70): nra_scope.
Notation "♯flatten( d )" := (NRAUnop OpFlatten d) (at level 50) : nra_scope.
Notation "‵{| d |}" := ((NRAUnop OpBag) d) (at level 50) : nra_scope.
Notation "‵[| ( s , r ) |]" := ((NRAUnop (OpRec s)) r) (at level 50) : nra_scope.
Notation "¬π[ s1 ]( r )" := ((NRAUnop (OpRecRemove s1)) r) (at level 50) : nra_scope.
Notation "π[ s1 ]( r )" := ((NRAUnop (OpRecProject s1)) r) (at level 50) : nra_scope.
Notation "p · r" := ((NRAUnop (OpDot r)) p) (left associativity, at level 40): nra_scope.

Notation "χ⟨ p ⟩( r )" := (NRAMap p r) (at level 70) : nra_scope.
Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (NRAMapProduct e2 e1) (at level 70) : nra_scope.
Notation "r1 × r2" := (NRAProduct r1 r2) (right associativity, at level 70): nra_scope.
Notation "σ⟨ p ⟩( r )" := (NRASelect p r) (at level 70) : nra_scope.
Notation "r1 ∥ r2" := (NRADefault r1 r2) (right associativity, at level 70): nra_scope.
Notation "r1 ◯ r2" := (NRAApp r1 r2) (right associativity, at level 60): nra_scope.

Global Hint Resolve nra_eval_normalized : qcert.

Tactic Notation "nra_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "NRAGetConstant"%string
  | Case_aux c "NRAID"%string
  | Case_aux c "NRAConst"%string
  | Case_aux c "NRABinop"%string
  | Case_aux c "NRAUnop"%string
  | Case_aux c "NRAMap"%string
  | Case_aux c "NRAMapProduct"%string
  | Case_aux c "NRAProduct"%string
  | Case_aux c "NRASelect"%string
  | Case_aux c "NRADefault"%string
  | Case_aux c "NRAEither"%string
  | Case_aux c "NRAEitherConcat"%string
  | Case_aux c "NRAApp"%string ].