Module cNRAEnv

Section cNRAEnv.
  Require Import String List Compare_dec.
  Require Import EquivDec.

  Require Import Utils BasicRuntime.



  Context {fruntime:foreign_runtime}.

  Inductive nraenv_core : Set :=
  | ANID : nraenv_core
  | ANConst : data -> nraenv_core
  | ANBinop : binOp -> nraenv_core -> nraenv_core -> nraenv_core
  | ANUnop : unaryOp -> nraenv_core -> nraenv_core
  | ANMap : nraenv_core -> nraenv_core -> nraenv_core
  | ANMapConcat : nraenv_core -> nraenv_core -> nraenv_core
  | ANProduct : nraenv_core -> nraenv_core -> nraenv_core
  | ANSelect : nraenv_core -> nraenv_core -> nraenv_core
  | ANDefault : nraenv_core -> nraenv_core -> nraenv_core
  | ANEither : nraenv_core -> nraenv_core -> nraenv_core
  | ANEitherConcat : nraenv_core -> nraenv_core -> nraenv_core
  | ANApp : nraenv_core -> nraenv_core -> nraenv_core
  | ANGetConstant : string -> nraenv_core
  | ANEnv : nraenv_core
  | ANAppEnv : nraenv_core -> nraenv_core -> nraenv_core
  | ANMapEnv : nraenv_core -> nraenv_core
  .

  Tactic Notation "nraenv_core_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "ANID"%string
  | Case_aux c "ANConst"%string
  | Case_aux c "ANBinop"%string
  | Case_aux c "ANUnop"%string
  | Case_aux c "ANMap"%string
  | Case_aux c "ANMapConcat"%string
  | Case_aux c "ANProduct"%string
  | Case_aux c "ANSelect"%string
  | Case_aux c "ANDefault"%string
  | Case_aux c "ANEither"%string
  | Case_aux c "ANEitherConcat"%string
  | Case_aux c "ANApp"%string
  | Case_aux c "ANGetConstant"%string
  | Case_aux c "ANEnv"%string
  | Case_aux c "ANAppEnv"%string
  | Case_aux c "ANMapEnv"%string].
  
  Global Instance nraenv_core_eqdec : EqDec nraenv_core eq.


  Context (h:list(string*string)).
  Context (constant_env:list (string*data)).
  Fixpoint nraenv_core_eval (op:nraenv_core) (env: data) (x:data) : option data :=
    match op with
      | ANID => Some x
      | ANConst rd => Some (normalize_data h rd)
      | ANBinop bop op1 op2 =>
        olift2 (fun d1 d2 => fun_of_binop h bop d1 d2) (nraenv_core_eval op1 env x) (nraenv_core_eval op2 env x)
      | ANUnop uop op1 =>
        olift (fun d1 => fun_of_unaryop h uop d1) (nraenv_core_eval op1 env x)
      | ANMap op1 op2 =>
        let aux_map d :=
            lift_oncoll (fun c1 => lift dcoll (rmap (nraenv_core_eval op1 env) c1)) d
        in olift aux_map (nraenv_core_eval op2 env x)
      | ANMapConcat op1 op2 =>
        let aux_mapconcat d :=
            lift_oncoll (fun c1 => lift dcoll (rmap_concat (nraenv_core_eval op1 env) c1)) d
        in olift aux_mapconcat (nraenv_core_eval op2 env x)
      | ANProduct op1 op2 =>
        let aux_product d :=
            lift_oncoll (fun c1 => lift dcoll (rmap_concat (fun _ => nraenv_core_eval op2 env x) c1)) d
        in olift aux_product (nraenv_core_eval op1 env x)
      | ANSelect op1 op2 =>
        let pred x' :=
            match nraenv_core_eval op1 env 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 (nraenv_core_eval op2 env x)
      | ANEither opl opr =>
        match x with
          | dleft dl => nraenv_core_eval opl env dl
          | dright dr => nraenv_core_eval opr env dr
          | _ => None
        end
      | ANEitherConcat op1 op2 =>
        match nraenv_core_eval op1 env x, nraenv_core_eval op2 env 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
      | ANDefault op1 op2 =>
        olift (fun d1 => match d1 with
                               | dcoll nil => nraenv_core_eval op2 env x
                               | _ => Some d1
                         end) (nraenv_core_eval op1 env x)
      | ANApp op2 op1 =>
        olift (fun x' => nraenv_core_eval op2 env x') (nraenv_core_eval op1 env x)
      | ANGetConstant s => edot constant_env s
      | ANEnv => (Some env)
      | ANAppEnv op2 op1 =>
        olift (fun env' => nraenv_core_eval op2 env' x) (nraenv_core_eval op1 env x)
      | ANMapEnv op1 =>
        lift_oncoll (fun c1 => lift dcoll (rmap ((fun env' => nraenv_core_eval op1 env' x)) c1)) env
    end.


  Require Import NRARuntime.
  Require Import String List RList.
  
  Local Open Scope string_scope.
  Local Open Scope list_scope.

  Definition ARecEither f :=
    AEither (AUnop ALeft (AUnop (ARec f) AID)) (AUnop ARight (AUnop (ARec f) AID)).
  
  Fixpoint nra_of_nraenv_core (ae:nraenv_core) : nra :=
    match ae with
      | ANID => nra_data
      | ANConst d => (AConst d)
      | ANBinop b ae1 ae2 => ABinop b (nra_of_nraenv_core ae1) (nra_of_nraenv_core ae2)
      | ANUnop u ae1 => AUnop u (nra_of_nraenv_core ae1)
      | ANMap ea1 ea2 =>
        AMap (nra_of_nraenv_core ea1)
             (unnest_two
                "a1"
                "PDATA"
                (AUnop AColl (nra_wrap_a1 (nra_of_nraenv_core ea2))))
      | ANMapConcat ea1 ea2 =>
        (AMap (ABinop AConcat
                      (AUnop (ADot "PDATA") AID)
                      (AUnop (ADot "PDATA2") AID))
              (AMapConcat
                 (AMap (AUnop (ARec "PDATA2") AID) (nra_of_nraenv_core ea1))
                 (unnest_two
                    "a1"
                    "PDATA"
                    (AUnop AColl (nra_wrap_a1 (nra_of_nraenv_core ea2))))))
      | ANProduct ea1 ea2 => AProduct (nra_of_nraenv_core ea1) (nra_of_nraenv_core ea2)
      | ANSelect ea1 ea2 =>
        (AMap (AUnop (ADot "PDATA") AID)
              (ASelect (nra_of_nraenv_core ea1)
                       (unnest_two
                          "a1"
                          "PDATA"
                          (AUnop AColl (nra_wrap_a1 (nra_of_nraenv_core ea2))))))
      | ANDefault ea1 ea2 => ADefault (nra_of_nraenv_core ea1) (nra_of_nraenv_core ea2)
      | ANEither eal ear => AApp
                                  (AEither (nra_of_nraenv_core eal) (nra_of_nraenv_core ear))
                                  (AEitherConcat
                                     (AApp (ARecEither "PDATA") nra_data)
                                     (AUnop (ARec "PBIND") nra_bind))
      | ANEitherConcat ea1 ea2 => AEitherConcat (nra_of_nraenv_core ea1) (nra_of_nraenv_core ea2)
      | ANApp ea1 ea2 => AApp (nra_of_nraenv_core ea1)
                              (nra_wrap (nra_of_nraenv_core ea2))
      | ANGetConstant s => AGetConstant s
      | ANEnv => nra_bind
      | ANAppEnv ea1 ea2 =>
        AApp (nra_of_nraenv_core ea1)
             (nra_context (nra_of_nraenv_core ea2) nra_data)
      | ANMapEnv ea1 =>
        AMap (nra_of_nraenv_core ea1)
             (unnest_two
                "a1"
                "PBIND"
                (AUnop AColl (nra_wrap_bind_a1 nra_data)))
    end.

  Lemma rmap_map_rec1 l s:
    rmap (fun x : data => Some (drec ((s, x) :: nil))) l =
    Some (map (fun x : data => (drec ((s, x) :: nil))) l).

  Lemma rmap_map_rec2 env a1 l :
    (rmap
       (fun x : data =>
          match x with
            | drec r1 =>
              Some
                (drec
                   (rec_concat_sort
                      (("PBIND", env) :: ("a1", dcoll a1) :: nil) r1))
            | _ => None
          end)
       (map (fun x : data => drec (("PDATA", x) :: nil)) l))
    =
    Some (map (fun x : data => drec (("PBIND", env) :: ("PDATA", x) :: ("a1", dcoll a1) :: nil)) l).

  Lemma rmap_map_rec3 d a1 l :
    (rmap
       (fun x : data =>
          match x with
            | drec r1 =>
              Some
                (drec
                   (rec_concat_sort
                      (("PDATA", d) :: ("a1", dcoll a1) :: nil) r1))
            | _ => None
          end)
       (map (fun x : data => drec (("PBIND", x) :: nil)) l))
    =
    Some (map (fun x : data => drec (("PBIND", x) :: ("PDATA", d) :: ("a1", dcoll a1) :: nil)) l).

  Lemma option_id {A} (x:option A) :
    (match x with None => None | Some y => Some y end) = x.
  
  Lemma rmap_map_unnest2 env a l0 l1 :
    rmap
      (fun x : data =>
         olift2
           (fun d1 d2 : data =>
              match d1 with
                | drec r1 =>
                  match d2 with
                    | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
                    | _ => None
                  end
                | _ => None
              end)
           match x with
             | drec r => edot r "PDATA"
             | _ => None
           end
           match x with
             | drec r => edot r "PDATA2"
             | _ => None
           end)
      (map
         (fun x : data =>
            drec (("PBIND", env) :: ("PDATA", a) :: ("PDATA2", x) :: nil)) l0 ++ l1)
    =
    olift2 (fun d1 d2 => Some (d1 ++ d2))
           (rmap
              (fun x : data =>
                 match a with
                   | drec r2 =>
                     match x with
                       | drec r1 => Some (drec (rec_concat_sort r2 r1))
                       | _ => None
                     end
                   | _ => None
                 end) l0)
           (rmap
              (fun x : data =>
                 olift2
                   (fun d1 d2 : data =>
                      match d1 with
                        | drec r1 =>
                          match d2 with
                            | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
                            | _ => None
                          end
                        | _ => None
                      end)
                   match x with
                     | drec r => edot r "PDATA"
                     | _ => None
                   end
                   match x with
                     | drec r => edot r "PDATA2"
                     | _ => None
                   end)
              l1).

  Lemma omap_concat_map_rec env a1 l :
    omap_concat
      (drec (("PBIND", env) :: ("a1", dcoll a1) :: nil))
      (map (fun x : data => drec (("PDATA", x) :: nil)) l)
    =
    Some (map (fun x : data => drec (("PBIND", env) :: ("PDATA", x) :: ("a1", dcoll a1) :: nil)) l).

  Lemma omap_concat_map_rec2 env a l :
    omap_concat (drec (("PBIND", env) :: ("PDATA", a) :: nil))
                (map (fun x : data => drec (("PDATA2", x) :: nil)) l)

    =
    Some (map (fun x : data => drec (("PBIND", env) :: ("PDATA", a) :: ("PDATA2", x) :: nil)) l).

  Lemma omap_concat_map_rec3 d a1 l :
    omap_concat
      (drec (("PDATA", d) :: ("a1", dcoll a1) :: nil))
      (map (fun x : data => drec (("PBIND", x) :: nil)) l)
    =
    Some (map (fun x : data => drec (("PBIND", x) :: ("PDATA", d) :: ("a1", dcoll a1) :: nil)) l).

  Lemma omap_concat_unnest env a a1 l :
    omap_concat
      (drec (("PBIND", env) :: ("a1", dcoll a1) :: nil))
      (drec (("PDATA", a) :: nil)
            :: map (fun x : data => drec (("PDATA", x) :: nil)) l)
    =
    Some (drec (("PBIND", env) :: ("PDATA", a) :: ("a1", dcoll a1) :: nil) ::
               (map (fun x : data => drec (("PBIND", env) :: ("PDATA", x) :: ("a1", dcoll a1) :: nil)) l)).

  Lemma omap_concat_unnest2 d a a1 l :
    omap_concat
      (drec (("PDATA", d) :: ("a1", dcoll a1) :: nil))
      (drec (("PBIND", a) :: nil)
            :: map (fun x : data => drec (("PBIND", x) :: nil)) l)
    =
    Some (drec (("PBIND", a) :: ("PDATA", d) :: ("a1", dcoll a1) :: nil) ::
               (map (fun x : data => drec (("PBIND", x) :: ("PDATA", d) :: ("a1", dcoll a1) :: nil)) l)).

  Lemma rmap_remove1 env l l2:
    rmap
      (fun x : data =>
         match x with
           | drec r => Some (drec (rremove r "a1"))
           | _ => None
         end)
      (map
         (fun x : data =>
            drec
              (("PBIND", env) :: ("PDATA", x) :: ("a1", dcoll l2) :: nil))
         l)
    =
    Some (map (fun x: data => drec (("PBIND", env) :: ("PDATA", x) :: nil)) l).
  
  Lemma rmap_remove2 d l l2:
    rmap
      (fun x : data =>
         match x with
           | drec r => Some (drec (rremove r "a1"))
           | _ => None
         end)
      (map
         (fun x : data =>
            drec
              (("PBIND", x) :: ("PDATA", d) :: ("a1", dcoll l2) :: nil))
         l)
    =
    Some (map (fun x: data => drec (("PBIND", x) :: ("PDATA", d) :: nil)) l).
  
  Lemma rmap_one1 env a l:
    rmap
      (fun x : data =>
         match x with
           | drec r => edot r "PDATA"
           | _ => None
         end) (drec (("PBIND", env) :: ("PDATA", a) :: nil) :: l)
    =
    match
      rmap
        (fun x : data =>
           match x with
             | drec r => edot r "PDATA"
             | _ => None
           end) l
    with
      | Some a' => Some (a :: a')
      | None => None
    end.

  Lemma unfold_env_nra (ae:nraenv_core) (env:data) (x:data) :
    (nraenv_core_eval ae env x) = (h ⊢ (nra_of_nraenv_core ae) @ₐ (nra_context_data env x) ⊣ constant_env).
  
End cNRAEnv.

Delimit Scope nraenv_core_scope with nraenv_core.

Notation "h ⊢ₑ op @ₑ x ⊣ c ; env " := (nraenv_core_eval h c op env x) (at level 10) : nraenv_core_scope.

Section RcNRAEnv2.
  Local Open Scope nraenv_core.

  Context {fruntime:foreign_runtime}.

  Lemma nraenv_core_eval_const_sort h p x c env :
    h ⊢ₑ p @ₑ x ⊣ (rec_sort c); env = h ⊢ₑ p @ₑ x ⊣ c; env.

  Lemma unfold_env_nra_sort h c (ae:nraenv_core) (env:data) (x:data) :
    (nraenv_core_eval h c ae env x) = (h ⊢ (nra_of_nraenv_core ae) @ₐ (nra_context_data env x) ⊣ (rec_sort c)).

  Lemma nraenv_core_eval_normalized h constant_env {op:nraenv_core} {env d:data} {o} :
    nraenv_core_eval h constant_env op env d = Some o ->
    Forall (fun x => data_normalized h (snd x)) constant_env ->
    data_normalized h env ->
    data_normalized h d ->
    data_normalized h o.

  Section Top.
    Context (h:list(string*string)).

    Definition nraenv_core_eval_top (q:nraenv_core) (env:bindings) :=
      nraenv_core_eval h (rec_sort env) q (drec nil) dunit.
  End Top.

  Section FreeVars.
    Fixpoint nraenv_core_free_vars (q:nraenv_core) : list string :=
      match q with
      | ANID => nil
      | ANConst rd => nil
      | ANBinop _ q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANUnop _ q1 =>
        nraenv_core_free_vars q1
      | ANMap q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANMapConcat q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANProduct q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANSelect q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANEither ql qr =>
        nraenv_core_free_vars ql ++ nraenv_core_free_vars qr
      | ANEitherConcat q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANDefault q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANApp q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANGetConstant s => s :: nil
      | ANEnv => nil
      | ANAppEnv q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | ANMapEnv q1 =>
        nraenv_core_free_vars q1
      end.
  End FreeVars.

End RcNRAEnv2.

  
Notation "'ID'" := (ANID) (at level 50) : nraenv_core_scope.
Notation "'ENV'" := (ANEnv) (at level 50) : nraenv_core_scope.
Notation "CGET⟨ s ⟩" := (ANGetConstant s) (at level 50) : nraenv_core_scope.
  
Notation "‵‵ c" := (ANConst (dconst c)) (at level 0) : nraenv_core_scope.
Notation "‵ c" := (ANConst c) (at level 0) : nraenv_core_scope.
Notation "‵{||}" := (ANConst (dcoll nil)) (at level 0) : nraenv_core_scope.
Notation "‵[||]" := (ANConst (drec nil)) (at level 50) : nraenv_core_scope.

Notation "r1 ∧ r2" := (ANBinop AAnd r1 r2) (right associativity, at level 65): nraenv_core_scope.
Notation "r1 ∨ r2" := (ANBinop AOr r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 ≐ r2" := (ANBinop AEq r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 ≤ r2" := (ANBinop ALt r1 r2) (no associativity, at level 70): nraenv_core_scope.
Notation "r1 ⋃ r2" := (ANBinop AUnion r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 − r2" := (ANBinop AMinus r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 ⋂min r2" := (ANBinop AMin r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 ⋃max r2" := (ANBinop AMax r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "p ⊕ r" := ((ANBinop AConcat) p r) (at level 70) : nraenv_core_scope.
Notation "p ⊗ r" := ((ANBinop AMergeConcat) p r) (at level 70) : nraenv_core_scope.

Notation "¬( r1 )" := (ANUnop ANeg r1) (right associativity, at level 70): nraenv_core_scope.
Notation "♯distinct( r1 )" := (ANUnop ADistinct r1) (right associativity, at level 70): nraenv_core_scope.
Notation "♯count( r1 )" := (ANUnop ACount r1) (right associativity, at level 70): nraenv_core_scope.
Notation "♯flatten( d )" := (ANUnop AFlatten d) (at level 50) : nraenv_core_scope.

Notation "a1 ♯+ a2" := (ANBinop (ABArith ArithPlus) a1 a2) (right associativity, at level 70): nraenv_core_scope.

Notation "a1 ♯- a2" := (ANBinop (ABArith ArithMinus) a1 a2) (right associativity, at level 70): nraenv_core_scope.

Notation "‵{| d |}" := ((ANUnop AColl) d) (at level 50) : nraenv_core_scope.
Notation "‵[| ( s , r ) |]" := ((ANUnop (ARec s)) r) (at level 50) : nraenv_core_scope.
Notation "¬π[ s1 ]( r )" := ((ANUnop (ARecRemove s1)) r) (at level 50) : nraenv_core_scope.
Notation "π[ s1 ]( r )" := ((ANUnop (ARecProject s1)) r) (at level 50) : nraenv_core_scope.
Notation "p · r" := ((ANUnop (ADot r)) p) (left associativity, at level 40): nraenv_core_scope.

Notation "χ⟨ p ⟩( r )" := (ANMap p r) (at level 70) : nraenv_core_scope.
Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (ANMapConcat e2 e1) (at level 70) : nraenv_core_scope.
Notation "r1 × r2" := (ANProduct r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "σ⟨ p ⟩( r )" := (ANSelect p r) (at level 70) : nraenv_core_scope.
Notation "r1 ∥ r2" := (ANDefault r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 ◯ r2" := (ANApp r1 r2) (right associativity, at level 60): nraenv_core_scope.

Notation "r1 ◯ₑ r2" := (ANAppEnv r1 r2) (right associativity, at level 60): nraenv_core_scope.
Notation "χᵉ⟨ p ⟩" := (ANMapEnv p) (at level 70) : nraenv_core_scope.

Hint Resolve nraenv_core_eval_normalized.

Tactic Notation "nraenv_core_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "ANID"%string
  | Case_aux c "ANConst"%string
  | Case_aux c "ANBinop"%string
  | Case_aux c "ANUnop"%string
  | Case_aux c "ANMap"%string
  | Case_aux c "ANMapConcat"%string
  | Case_aux c "ANProduct"%string
  | Case_aux c "ANSelect"%string
  | Case_aux c "ANDefault"%string
  | Case_aux c "ANEither"%string
  | Case_aux c "ANEitherConcat"%string
  | Case_aux c "ANApp"%string
  | Case_aux c "ANGetConstant"%string
  | Case_aux c "ANEnv"%string
  | Case_aux c "ANAppEnv"%string
  | Case_aux c "ANMapEnv"%string].