Qcert.NRAEnv.Lang.NRAEnv

Section NRAEnv.





  Context {fruntime:foreign_runtime}.

  Definition join (op1 op2 op3 : cnraenv) : cnraenv :=
    (ANSelect op1 (ANProduct op2 op3)).

  Definition semi_join (op1 op2 op3 : cnraenv) : cnraenv :=
    ANSelect (ANUnop ANeg (ANBinop AEq (ANSelect op1 (ANProduct ((ANUnop AColl) ANID) op3)) (ANConst (dcoll nil)))) op2.

  Definition anti_join (op1 op2 op3 : cnraenv) : cnraenv :=
    ANSelect (ANBinop AEq (ANSelect op1 (ANProduct ((ANUnop AColl) ANID) op3)) (ANConst (dcoll nil))) op2.


  Definition map_add_rec (s:string) (op1 op2 : cnraenv) : cnraenv :=
    ANMap ((ANBinop AConcat) ANID ((ANUnop (ARec s)) op1)) op2.
  Definition map_to_rec (s:string) (op : cnraenv) : cnraenv :=
    ANMap (ANUnop (ARec s) ANID) op.

  Definition flat_map (op1 op2 : cnraenv) : cnraenv :=
    ANUnop AFlatten (ANMap op1 op2).

  Definition project (fields:list string) (op:cnraenv) : cnraenv
    := ANMap (ANUnop (ARecProject fields) ANID) op.

  Definition project_remove (s:string) (op:cnraenv) : cnraenv :=
    ANMap ((ANUnop (ARecRemove s)) ANID) op.

  Definition map_rename_rec (s1 s2:string) (op:cnraenv) : cnraenv :=
    ANMap ((ANBinop AConcat) ((ANUnop (ARec s2)) ((ANUnop (ADot s1)) ANID))
                  ((ANUnop (ARecRemove s1)) ANID)) op.





  Definition group_by_no_env (g:string) (sl:list string) (op : cnraenv) : cnraenv :=
    ANMap
      (ANBinop AConcat
               (ANUnop (ADot "1") (ANUnop (ADot "2") ANID))
               (ANUnop (ARec g)
                       (ANMap (ANUnop (ADot "3") ANID)
                              (ANSelect
                                 (ANBinop AEq
                                          (ANUnop (ARecProject sl) (ANUnop (ADot "1") ANID))
                                          (ANUnop (ARecProject sl) (ANUnop (ADot "3") ANID)))
                                 (ANProduct (ANUnop AColl (ANUnop (ADot "2") ANID))
                                            (ANUnop (ADot "4") ANID))))))
      (ANProduct
         (ANUnop AColl (ANUnop (ARec "4") (map_to_rec "3" op)))
         (map_to_rec "2" (map_to_rec "1" (ANUnop ADistinct (project sl op))))).

  Definition group_by_with_env (g:string) (sl:list string) (op : cnraenv) : cnraenv :=
    let op_pregroup := ANUnop (ADot "$pregroup") ANEnv in
    ANAppEnv
      (ANMap
         (ANBinop AConcat
                  (ANUnop (ARec g)
                          (ANAppEnv (ANSelect (ANBinop AEq
                                                       (ANUnop (ARecProject sl) ANID)
                                                       (ANUnop (ADot "$key") ANEnv))
                                              op_pregroup
                                    )
                                    (ANBinop AConcat (ANUnop (ARec "$key") ANID) ANEnv)
                          )
                  )
                  ANID
         )
         (ANUnop ADistinct (project sl op_pregroup))
      )
      (ANUnop (ARec "$pregroup") op).



  Definition unnest_one (s:string) (op:cnraenv) : cnraenv :=
    ANMap ((ANUnop (ARecRemove s)) ANID) (ANMapConcat ((ANUnop (ADot s)) ANID) op).

  Definition unnest (a b:string) (op:cnraenv) : cnraenv :=
    ANMap ((ANUnop (ARecRemove a)) ANID) (ANMapConcat (ANMap ((ANUnop (ARec b)) ANID) ((ANUnop (ADot a)) ANID)) op).


  Inductive nraenv : Set :=
  
  | NRAEnvID : nraenv
  | NRAEnvConst : data → nraenv
  | NRAEnvBinop : binOp → nraenv → nraenv → nraenv
  | NRAEnvUnop : unaryOp → nraenv → nraenv
  | NRAEnvMap : nraenv → nraenv → nraenv
  | NRAEnvMapConcat : nraenv → nraenv → nraenv
  | NRAEnvProduct : nraenv → nraenv → nraenv
  | NRAEnvSelect : nraenv → nraenv → nraenv
  | NRAEnvDefault : nraenv → nraenv → nraenv
  | NRAEnvEither : nraenv → nraenv → nraenv
  | NRAEnvEitherConcat : nraenv → nraenv → nraenv
  | NRAEnvApp : nraenv → nraenv → nraenv
  | NRAEnvGetConstant : string → nraenv
  | NRAEnvEnv : nraenv
  | NRAEnvAppEnv : nraenv → nraenv → nraenv
  | NRAEnvMapEnv : nraenv → nraenv
  
  | NRAEnvFlatMap : nraenv → nraenv → nraenv
  | NRAEnvJoin : nraenv → nraenv → nraenv → nraenv
  | NRAEnvProject : list string → nraenv → nraenv
  | NRAEnvGroupBy : string → list string → nraenv → nraenv
  | NRAEnvUnnest : string → string → nraenv → nraenv
  .

  Global Instance nraenv_eqdec : EqDec nraenv eq.

  Fixpoint cnraenv_of_nraenv (e:nraenv) : cnraenv :=
    match e with
      | NRAEnvID ⇒ ANID
      | NRAEnvConst d ⇒ ANConst d
      | NRAEnvBinop b e1 e2 ⇒ ANBinop b (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvUnop u e1 ⇒ ANUnop u (cnraenv_of_nraenv e1)
      | NRAEnvMap e1 e2 ⇒ ANMap (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvMapConcat e1 e2 ⇒ ANMapConcat (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvProduct e1 e2 ⇒ ANProduct (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvSelect e1 e2 ⇒ ANSelect (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvDefault e1 e2 ⇒ ANDefault (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvEither opl opr ⇒ ANEither (cnraenv_of_nraenv opl) (cnraenv_of_nraenv opr)
      | NRAEnvEitherConcat op1 op2 ⇒ ANEitherConcat (cnraenv_of_nraenv op1) (cnraenv_of_nraenv op2)
      | NRAEnvApp e1 e2 ⇒ ANApp (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvGetConstant s ⇒ ANGetConstant s
      | NRAEnvEnv ⇒ ANEnv
      | NRAEnvAppEnv e1 e2 ⇒ ANAppEnv (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvMapEnv e1 ⇒ ANMapEnv (cnraenv_of_nraenv e1)
      | NRAEnvFlatMap e1 e2 ⇒ flat_map (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2)
      | NRAEnvJoin e1 e2 e3 ⇒ join (cnraenv_of_nraenv e1) (cnraenv_of_nraenv e2) (cnraenv_of_nraenv e3)
      | NRAEnvProject ls e1 ⇒ project ls (cnraenv_of_nraenv e1)
      | NRAEnvGroupBy s ls e1 ⇒ group_by_with_env s ls (cnraenv_of_nraenv e1)
      | NRAEnvUnnest a b e1 ⇒ unnest a b (cnraenv_of_nraenv e1)
    end.

  Fixpoint nraenv_of_cnraenv (a:cnraenv) : nraenv :=
    match a with
      | ANID ⇒ NRAEnvID
      | ANConst d ⇒ NRAEnvConst d
      | ANBinop b e1 e2 ⇒ NRAEnvBinop b (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANUnop u e1 ⇒ NRAEnvUnop u (nraenv_of_cnraenv e1)
      | ANMap e1 e2 ⇒ NRAEnvMap (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANMapConcat e1 e2 ⇒ NRAEnvMapConcat (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANProduct e1 e2 ⇒ NRAEnvProduct (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANSelect e1 e2 ⇒ NRAEnvSelect (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANDefault e1 e2 ⇒ NRAEnvDefault (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANEither opl opr ⇒ NRAEnvEither (nraenv_of_cnraenv opl) (nraenv_of_cnraenv opr)
      | ANEitherConcat op1 op2 ⇒ NRAEnvEitherConcat (nraenv_of_cnraenv op1) (nraenv_of_cnraenv op2)
      | ANApp e1 e2 ⇒ NRAEnvApp (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANGetConstant s ⇒ NRAEnvGetConstant s
      | ANEnv ⇒ NRAEnvEnv
      | ANAppEnv e1 e2 ⇒ NRAEnvAppEnv (nraenv_of_cnraenv e1) (nraenv_of_cnraenv e2)
      | ANMapEnv e1 ⇒ NRAEnvMapEnv (nraenv_of_cnraenv e1)
    end.

  Lemma nraenv_roundtrip (a:cnraenv) :
    (cnraenv_of_nraenv (nraenv_of_cnraenv a)) = a.

  Context (h:list(string×string)).

  Definition nraenv_eval c (e:nraenv) (env:data) (x:data) : option data :=
    cnraenv_eval h c (cnraenv_of_nraenv e) env x.

  Lemma initial_nraenv_ident c (e:cnraenv) (env:data) (x:data) :
    nraenv_eval c (nraenv_of_cnraenv e) env x = cnraenv_eval h c e env x.

End NRAEnv.


Tactic Notation "nraenv_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "NRAEnvID"
  | Case_aux c "NRAEnvConst"
  | Case_aux c "NRAEnvBinop"
  | Case_aux c "NRAEnvUnop"
  | Case_aux c "NRAEnvMap"
  | Case_aux c "NRAEnvMapConcat"
  | Case_aux c "NRAEnvProduct"
  | Case_aux c "NRAEnvSelect"
  | Case_aux c "NRAEnvDefault"
  | Case_aux c "NRAEnvEither"
  | Case_aux c "NRAEnvEitherConcat"
  | Case_aux c "NRAEnvApp"
  | Case_aux c "NRAEnvGetConstant"
  | Case_aux c "NRAEnvEnv"
  | Case_aux c "NRAEnvAppEnv"
  | Case_aux c "NRAEnvMapEnv"
  | Case_aux c "NRAEnvFlatMap"
  | Case_aux c "NRAEnvJoin"
  | Case_aux c "NRAEnvProject"
  | Case_aux c "NRAEnvGroupBy"
  | Case_aux c "NRAEnvUnnest"].