Qcert.NRAEnv.Core.cNRAEnv


Section cNRAEnv.


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 cnraenv : Set :=
  | ANID : cnraenv
  | ANConst : data → cnraenv
  | ANBinop : binOp → cnraenv → cnraenv → cnraenv
  | ANUnop : unaryOp → cnraenv → cnraenv
  | ANMap : cnraenv → cnraenv → cnraenv
  | ANMapConcat : cnraenv → cnraenv → cnraenv
  | ANProduct : cnraenv → cnraenv → cnraenv
  | ANSelect : cnraenv → cnraenv → cnraenv
  | ANDefault : cnraenv → cnraenv → cnraenv
  | ANEither : cnraenv → cnraenv → cnraenv
  | ANEitherConcat : cnraenv → cnraenv → cnraenv
  | ANApp : cnraenv → cnraenv → cnraenv
  | ANGetConstant : string → cnraenv
  | ANEnv : cnraenv
  | ANAppEnv : cnraenv → cnraenv → cnraenv
  | ANMapEnv : cnraenv → cnraenv
  .

  Tactic Notation "cnraenv_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 cnraenv_eqdec : EqDec cnraenv eq.

NRA+Env Semantics

  Context (h:list(string×string)).
  Context (constant_env:list (string×data)).
  Fixpoint cnraenv_eval (op:cnraenv) (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) (cnraenv_eval op1 env x) (cnraenv_eval op2 env x)
      | ANUnop uop op1 ⇒
        olift (fun d1 ⇒ fun_of_unaryop h uop d1) (cnraenv_eval op1 env x)
      | ANMap op1 op2 ⇒
        let aux_map d :=
            lift_oncoll (fun c1 ⇒ lift dcoll (rmap (cnraenv_eval op1 env) c1)) d
        in olift aux_map (cnraenv_eval op2 env x)
      | ANMapConcat op1 op2 ⇒
        let aux_mapconcat d :=
            lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (cnraenv_eval op1 env) c1)) d
        in olift aux_mapconcat (cnraenv_eval op2 env x)
      | ANProduct op1 op2 ⇒
        
        let aux_product d :=
            lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (fun _ ⇒ cnraenv_eval op2 env x) c1)) d
        in olift aux_product (cnraenv_eval op1 env x)
      | ANSelect op1 op2 ⇒
        let pred x' :=
            match cnraenv_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 (cnraenv_eval op2 env x)
      | ANEither opl opr ⇒
        match x with
          | dleft dl ⇒ cnraenv_eval opl env dl
          | dright dr ⇒ cnraenv_eval opr env dr
          | _ ⇒ None
        end
      | ANEitherConcat op1 op2 ⇒
        match cnraenv_eval op1 env x, cnraenv_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 ⇒ cnraenv_eval op2 env x
                               | _ ⇒ Some d1
                         end) (cnraenv_eval op1 env x)
      | ANApp op2 op1 ⇒
        olift (fun x' ⇒ cnraenv_eval op2 env x') (cnraenv_eval op1 env x)
      | ANGetConstant s ⇒ edot constant_env s
      | ANEnv ⇒ (Some env)
      | ANAppEnv op2 op1 ⇒
        
        
        olift (fun env' ⇒ cnraenv_eval op2 env' x) (cnraenv_eval op1 env x)
      | ANMapEnv op1 ⇒
        lift_oncoll (fun c1 ⇒ lift dcoll (rmap ((fun env' ⇒ cnraenv_eval op1 env' x)) c1)) env
    end.

Functions used to map dual input env/data into single input



  Definition ARecEither f :=
    AEither (AUnop ALeft (AUnop (ARec f) AID)) (AUnop ARight (AUnop (ARec f) AID)).

  Fixpoint nra_of_cnraenv (ae:cnraenv) : nra :=
    match ae with
      | ANID ⇒ pat_data
      | ANConst d ⇒ (AConst d)
      | ANBinop b ae1 ae2 ⇒ ABinop b (nra_of_cnraenv ae1) (nra_of_cnraenv ae2)
      | ANUnop u ae1 ⇒ AUnop u (nra_of_cnraenv ae1)
      | ANMap ea1 ea2 ⇒
        AMap (nra_of_cnraenv ea1)
             (unnest_two
                "a1"
                "PDATA"
                (AUnop AColl (pat_wrap_a1 (nra_of_cnraenv ea2))))
      | ANMapConcat ea1 ea2 ⇒
        (AMap (ABinop AConcat
                      (AUnop (ADot "PDATA") AID)
                      (AUnop (ADot "PDATA2") AID))
              (AMapConcat
                 (AMap (AUnop (ARec "PDATA2") AID) (nra_of_cnraenv ea1))
                 (unnest_two
                    "a1"
                    "PDATA"
                    (AUnop AColl (pat_wrap_a1 (nra_of_cnraenv ea2))))))
      | ANProduct ea1 ea2 ⇒ AProduct (nra_of_cnraenv ea1) (nra_of_cnraenv ea2)
      | ANSelect ea1 ea2 ⇒
        (AMap (AUnop (ADot "PDATA") AID)
              (ASelect (nra_of_cnraenv ea1)
                       (unnest_two
                          "a1"
                          "PDATA"
                          (AUnop AColl (pat_wrap_a1 (nra_of_cnraenv ea2))))))
      | ANDefault ea1 ea2 ⇒ ADefault (nra_of_cnraenv ea1) (nra_of_cnraenv ea2)
      | ANEither eal ear ⇒ AApp
                                  (AEither (nra_of_cnraenv eal) (nra_of_cnraenv ear))
                                  (AEitherConcat
                                     (AApp (ARecEither "PDATA") pat_data)
                                     (ABinop AConcat
                                             (AUnop (ARec "PBIND") pat_bind)
                                             (AUnop (ARec "PCONST") pat_const_env)))
      | ANEitherConcat ea1 ea2 ⇒ AEitherConcat (nra_of_cnraenv ea1) (nra_of_cnraenv ea2)
      | ANApp ea1 ea2 ⇒ AApp (nra_of_cnraenv ea1) (pat_wrap (nra_of_cnraenv ea2))
      | ANGetConstant s ⇒ AUnop (ADot s) pat_const_env
      | ANEnv ⇒ pat_bind
      | ANAppEnv ea1 ea2 ⇒
        AApp (nra_of_cnraenv ea1)
             (pat_context pat_const_env (nra_of_cnraenv ea2) pat_data)
      | ANMapEnv ea1 ⇒
        
        AMap (nra_of_cnraenv ea1)
             (unnest_two
                "a1"
                "PBIND"
                (AUnop AColl (pat_wrap_bind_a1 pat_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 c env a1 l :
    (rmap
       (fun x : data ⇒
          match x with
            | drec r1 ⇒
              Some
                (drec
                   (rec_concat_sort
                      (("PBIND", env) :: ("PCONST", c) :: ("a1", dcoll a1) :: nil) r1))
            | _ ⇒ None
          end)
       (map (fun x : data ⇒ drec (("PDATA", x) :: nil)) l))
    =
    Some (map (fun x : data ⇒ drec (("PBIND", env) :: ("PCONST", c) :: ("PDATA", x) :: ("a1", dcoll a1) :: nil)) l).

  Lemma rmap_map_rec3 c d a1 l :
    (rmap
       (fun x : data ⇒
          match x with
            | drec r1 ⇒
              Some
                (drec
                   (rec_concat_sort
                      (("PCONST", c) :: ("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) :: ("PCONST", c) :: ("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 c 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) :: ("PCONST", c) :: ("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 c env a1 l :
    omap_concat
      (drec (("PBIND", env) :: ("PCONST", c) :: ("a1", dcoll a1) :: nil))
      (map (fun x : data ⇒ drec (("PDATA", x) :: nil)) l)
    =
    Some (map (fun x : data ⇒ drec (("PBIND", env) :: ("PCONST", c) :: ("PDATA", x) :: ("a1", dcoll a1) :: nil)) l).

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

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

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

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

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

  Lemma rmap_remove1 c 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) :: ("PCONST", c) :: ("PDATA", x) :: ("a1", dcoll l2) :: nil))
         l)
    =
    Some (map (fun x: data ⇒ drec (("PBIND", env) :: ("PCONST", c) :: ("PDATA", x) :: nil)) l).

  Lemma rmap_remove2 c 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) :: ("PCONST", c) :: ("PDATA", d) :: ("a1", dcoll l2) :: nil))
         l)
    =
    Some (map (fun x: data ⇒ drec (("PBIND", x) :: ("PCONST", c) :: ("PDATA", d) :: nil)) l).

  Lemma rmap_one1 c env a l:
    rmap
      (fun x : data ⇒
         match x with
           | drec r ⇒ edot r "PDATA"
           | _ ⇒ None
         end) (drec (("PBIND", env) :: ("PCONST", c) :: ("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:cnraenv) (env:data) (x:data) :
    (cnraenv_eval ae env x) = (h ⊢ (nra_of_cnraenv ae) @ₐ (pat_context_data (drec constant_env) env x)).

End cNRAEnv.


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

Section RCnraenv2.

  Context {fruntime:foreign_runtime}.

  Lemma cnraenv_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:cnraenv) (env:data) (x:data) :
    (cnraenv_eval h c ae env x) = (h ⊢ (nra_of_cnraenv ae) @ₐ (pat_context_data (drec (rec_sort c)) env x)).

  Lemma cnraenv_eval_normalized h constant_env {op:cnraenv} {env d:data} {o} :
    cnraenv_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.

  End RCnraenv2.


Notation "'ID'" := (ANID) (at level 50) : cnraenv_scope.
Notation "'ENV'" := (ANEnv) (at level 50) : cnraenv_scope.
Notation "CGET⟨ s ⟩" := (ANGetConstant s) (at level 50) : cnraenv_scope.

Notation "‵‵ c" := (ANConst (dconst c)) (at level 0) : cnraenv_scope. Notation "‵ c" := (ANConst c) (at level 0) : cnraenv_scope. Notation "‵{||}" := (ANConst (dcoll nil)) (at level 0) : cnraenv_scope. Notation "‵[||]" := (ANConst (drec nil)) (at level 50) : cnraenv_scope.
Notation "r1 ∧ r2" := (ANBinop AAnd r1 r2) (right associativity, at level 65): cnraenv_scope. Notation "r1 ∨ r2" := (ANBinop AOr r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "r1 ≐ r2" := (ANBinop AEq r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "r1 ≤ r2" := (ANBinop ALt r1 r2) (no associativity, at level 70): cnraenv_scope. Notation "r1 ⋃ r2" := (ANBinop AUnion r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "r1 − r2" := (ANBinop AMinus r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "r1 ⋂min r2" := (ANBinop AMin r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "r1 ⋃max r2" := (ANBinop AMax r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "p ⊕ r" := ((ANBinop AConcat) p r) (at level 70) : cnraenv_scope. Notation "p ⊗ r" := ((ANBinop AMergeConcat) p r) (at level 70) : cnraenv_scope.
Notation "¬( r1 )" := (ANUnop ANeg r1) (right associativity, at level 70): cnraenv_scope. Notation "♯distinct( r1 )" := (ANUnop ADistinct r1) (right associativity, at level 70): cnraenv_scope. Notation "♯count( r1 )" := (ANUnop ACount r1) (right associativity, at level 70): cnraenv_scope. Notation "♯flatten( d )" := (ANUnop AFlatten d) (at level 50) : cnraenv_scope.
Notation "a1 ♯+ a2" := (ANBinop (ABArith ArithPlus) a1 a2) (right associativity, at level 70): cnraenv_scope.

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

Notation "‵{| d |}" := ((ANUnop AColl) d) (at level 50) : cnraenv_scope. Notation "‵[| ( s , r ) |]" := ((ANUnop (ARec s)) r) (at level 50) : cnraenv_scope. Notation "¬π[ s1 ]( r )" := ((ANUnop (ARecRemove s1)) r) (at level 50) : cnraenv_scope. Notation "π[ s1 ]( r )" := ((ANUnop (ARecProject s1)) r) (at level 50) : cnraenv_scope. Notation "p · r" := ((ANUnop (ADot r)) p) (left associativity, at level 40): cnraenv_scope.
Notation "χ⟨ p ⟩( r )" := (ANMap p r) (at level 70) : cnraenv_scope. Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (ANMapConcat e2 e1) (at level 70) : cnraenv_scope. Notation "r1 × r2" := (ANProduct r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "σ⟨ p ⟩( r )" := (ANSelect p r) (at level 70) : cnraenv_scope. Notation "r1 ∥ r2" := (ANDefault r1 r2) (right associativity, at level 70): cnraenv_scope. Notation "r1 ◯ r2" := (ANApp r1 r2) (right associativity, at level 60): cnraenv_scope.
Notation "r1 ◯ₑ r2" := (ANAppEnv r1 r2) (right associativity, at level 60): cnraenv_scope. Notation "χᵉ⟨ p ⟩" := (ANMapEnv p) (at level 70) : cnraenv_scope.

Tactic Notation "cnraenv_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].