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

Declare Scope nraenv_core_scope.

Section cNRAEnv.
  Context {fruntime:foreign_runtime}.

Abstract Syntax

  Section Syntax.
  

    Inductive nraenv_core : Set :=
    | cNRAEnvGetConstant : string -> nraenv_core
    | cNRAEnvID : nraenv_core
    | cNRAEnvConst : data -> nraenv_core
    | cNRAEnvBinop : binary_op -> nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvUnop : unary_op -> nraenv_core -> nraenv_core
    | cNRAEnvMap : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvMapProduct : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvProduct : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvSelect : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvDefault : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvEither : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvEitherConcat : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvApp : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvEnv : nraenv_core
    | cNRAEnvAppEnv : nraenv_core -> nraenv_core -> nraenv_core
    | cNRAEnvMapEnv : nraenv_core -> nraenv_core
    .

  
    Global Instance nraenv_core_eqdec : EqDec nraenv_core eq.

  End Syntax.

  Tactic Notation "nraenv_core_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "cNRAEnvGetConstant"%string
    | Case_aux c "cNRAEnvID"%string
    | Case_aux c "cNRAEnvConst"%string
    | Case_aux c "cNRAEnvBinop"%string
    | Case_aux c "cNRAEnvUnop"%string
    | Case_aux c "cNRAEnvMap"%string
    | Case_aux c "cNRAEnvMapProduct"%string
    | Case_aux c "cNRAEnvProduct"%string
    | Case_aux c "cNRAEnvSelect"%string
    | Case_aux c "cNRAEnvDefault"%string
    | Case_aux c "cNRAEnvEither"%string
    | Case_aux c "cNRAEnvEitherConcat"%string
    | Case_aux c "cNRAEnvApp"%string
    | Case_aux c "cNRAEnvEnv"%string
    | Case_aux c "cNRAEnvAppEnv"%string
    | Case_aux c "cNRAEnvMapEnv"%string].
  

Semantics

  
  Section Semantics.

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

Denotational Semantics

    
    
    
    
    
    Section Denotation.
      Inductive nraenv_core_sem: nraenv_core -> data -> data -> data -> Prop :=
      | sem_cNRAEnvGetConstant : forall v env d d1,
          edot constant_env v = Some d1 -> (* Γc(v) = d₁ *)
          nraenv_core_sem (cNRAEnvGetConstant v) env d d1 (* ⇒ Γc ; γ ; d ⊢〚$$v〛⇓ d₁ *)
      | sem_cNRAEnvID : forall env d,
          nraenv_core_sem cNRAEnvID env d d (* Γc ; γ ; d ⊢ ID ⇓ d *)
      | sem_cNRAEnvConst : forall env d d1 d2,
          normalize_data h d1 = d2 -> (* norm(d₁) = d₂ *)
          nraenv_core_sem (cNRAEnvConst d1) env d d2 (* ⇒ Γc ; γ ; d ⊢〚d₁〛⇓ d₂ *)
      | sem_cNRAEnvBinop : forall bop e1 e2 env d d1 d2 d3,
          nraenv_core_sem e1 env d d1 -> (* Γc ; γ ; d ⊢〚e₁〛⇓ d₁ *)
          nraenv_core_sem e2 env d d2 -> (* ∧ Γc ; γ ; d ⊢〚e₂〛⇓ d₂ *)
          binary_op_eval h bop d1 d2 = Some d3 -> (* ∧ d₁ ⊠ d₂ = d₃ *)
          nraenv_core_sem (cNRAEnvBinop bop e1 e2) env d d3 (* ⇒ Γc ; γ ; d ⊢〚e₁ ⊠ e₂〛⇓ d₃ *)
      | sem_cNRAEnvUnop : forall uop e env d d1 d2,
          nraenv_core_sem e env d d1 -> (* Γc ; γ ; d ⊢〚e〛⇓ d₁ *)
          unary_op_eval h uop d1 = Some d2 -> (* ∧ ⊞ d₁ = d₂ *)
          nraenv_core_sem (cNRAEnvUnop uop e) env d d2 (* ⇒ Γc ; γ ; d ⊢〚⊞ e〛⇓ d₂ *)
      | sem_cNRAEnvMap : forall e1 e2 env d c1 c2,
          nraenv_core_sem e1 env d (dcoll c1) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ {c₁} *)
          nraenv_core_sem_map e2 env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e₂〛χ ⇓ {c₂} *)
          nraenv_core_sem (cNRAEnvMap e2 e1) env d (dcoll c2)(* ⇒ Γc ; γ ; d ⊢〚χ⟨e₂⟩(e₁)〛⇓ {c₂} *)
      | sem_cNRAEnvMapProduct : forall e1 e2 env d c1 c2,
          nraenv_core_sem e1 env d (dcoll c1) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ {c₁} *)
          nraenv_core_sem_map_product e2 env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e₂〛⋈ᵈ ⇓ {c₂} *)
          nraenv_core_sem (* ⇒ Γc ; γ ; d ⊢〚⋈ᵈ⟨e₂⟩(e₁)〛⇓ {c₂} *)
            (cNRAEnvMapProduct e2 e1) env d (dcoll c2)
      | sem_cNRAEnvProduct_empty : forall e1 e2 env d, (* Does not evaluate e₂ if e₁ is empty. This facilitates translation to cNNRC *)
          nraenv_core_sem e1 env d (dcoll nil) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ {} *)
          nraenv_core_sem (* ⇒ Γc ; γ ; d ⊢〚e₁ × e₂〛⇓ {} *)
            (cNRAEnvProduct e1 e2) env d (dcoll nil)
      | sem_cNRAEnvProduct_nonEmpty : forall e1 e2 env d c1 c2 c3,
          nraenv_core_sem e1 env d (dcoll c1) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ {c₁} *)
          c1 <> nil -> (* ∧ {c₁} ≠ {} *)
          nraenv_core_sem e2 env d (dcoll c2) -> (* ∧ Γc ; γ ; d ⊢〚e₂〛⇓ {c₂} *)
          product_sem c1 c2 c3 -> (* ∧ {c₁} × {c₂} ⇓ {c₃} *)
          nraenv_core_sem (* ⇒ Γc ; γ ; d ⊢〚e₁ × e₂〛⇓ {c₃} *)
            (cNRAEnvProduct e1 e2) env d (dcoll c3)
      | sem_cNRAEnvSelect : forall e1 e2 env d c1 c2,
          nraenv_core_sem e1 env d (dcoll c1) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ {c₁} *)
          nraenv_core_sem_select e2 env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e₂〛σ ⇓ {c₂} *)
          nraenv_core_sem (* ⇒ Γc ; γ ; d ⊢〚σ⟨e₂⟩(e₁)〛⇓ {c₂} *)
            (cNRAEnvSelect e2 e1) env d (dcoll c2)
      | sem_cNRAEnvDefault_empty : forall e1 e2 env d d2,
          nraenv_core_sem e1 env d (dcoll nil) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ {} *)
          nraenv_core_sem e2 env d d2 -> (* ∧ Γc ; γ ; d ⊢〚e₂〛⇓ d₂ *)
          nraenv_core_sem (cNRAEnvDefault e1 e2) env d d2 (* ⇒ Γc ; γ ; d ⊢〚e₁ ∥ e₂〛⇓ d₂ *)
      | sem_cNRAEnvDefault_not_empty : forall e1 e2 env d d1,
          nraenv_core_sem e1 env d d1 -> (* Γc ; γ ; d ⊢〚e₁〛⇓ d₁ *)
          d1 <> dcoll nil -> (* ∧ d₁ ≠ {} *)
          nraenv_core_sem (cNRAEnvDefault e1 e2) env d d1 (* ⇒ Γc ; γ ; d ⊢〚e₁ ∥ e₂〛⇓ d₁ *)
      | sem_cNRAEnvEither_left : forall e1 e2 env d d1,
          nraenv_core_sem e1 env d d1 -> (* Γc ; γ ; d ⊢〚e₁〛⇓ d₁ *)
          nraenv_core_sem (* ⇒ Γc ; γ ; (dleft d) ⊢〚either e₁ e₂〛⇓ d₁ *)
            (cNRAEnvEither e1 e2) env (dleft d) d1
      | sem_cNRAEnvEither_right : forall e1 e2 env d d2,
          nraenv_core_sem e2 env d d2 -> (* Γc ; γ ; d ⊢〚e₂〛⇓ d₂ *)
          nraenv_core_sem (* ⇒ Γc ; γ ; (dright d) ⊢〚either e₁ e₂〛⇓ d₂ *)
            (cNRAEnvEither e1 e2) env (dright d) d2
      | sem_cNRAEnvEitherConcat_left : forall e1 e2 env d r1 r2,
          nraenv_core_sem e1 env d (dleft (drec r1)) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ (dleft [r₁]) *)
          nraenv_core_sem e2 env d (drec r2) -> (* ∧ Γc ; γ ; d ⊢〚e₂〛⇓ [r₂] *)
          nraenv_core_sem (* ⇒ Γc ; γ ; d ⊢〚either⊕ e₁ e₂〛⇓ (dleft [r₁]⊕[r₂]) *)
            (cNRAEnvEitherConcat e1 e2) env d
            (dleft (drec (rec_concat_sort r1 r2)))
      | sem_cNRAEnvEitherConcat_right : forall e1 e2 env d r1 r2,
          nraenv_core_sem e1 env d (dright (drec r1)) -> (* Γc ; γ ; d ⊢〚e₁〛⇓ (dright [r₁]) *)
          nraenv_core_sem e2 env d (drec r2) -> (* ∧ Γc ; γ ; d ⊢〚e₂〛⇓ [r₂] *)
          nraenv_core_sem (* ⇒ Γc ; γ ; d ⊢〚either⊕ e₁ e₂〛⇓ (dright [r₁]⊕[r₂]) *)
            (cNRAEnvEitherConcat e1 e2) env d
            (dright (drec (rec_concat_sort r1 r2)))
      | sem_cNRAEnvApp : forall e1 e2 env d d1 d2,
          nraenv_core_sem e1 env d d1 -> (* Γc ; γ ; d ⊢〚e₁〛⇓ d₁ *)
          nraenv_core_sem e2 env d1 d2 -> (* Γc ; γ ; d₁ ⊢〚e₂〛⇓ d₂ *)
          nraenv_core_sem (cNRAEnvApp e2 e1) env d d2 (* ⇒ Γc ; γ ; d ⊢〚e₂ ∘ e₁〛⇓ d₂ *)
      | sem_cNRAEnvEnv : forall env d,
          nraenv_core_sem cNRAEnvEnv env d env (* Γc ; γ ; d ⊢ ENV ⇓ γ *)
      | sem_cNRAEnvAppEnv : forall e1 e2 env d env1 d2,
          nraenv_core_sem e1 env d env1 -> (* Γc ; γ ; d ⊢〚e₁〛⇓ γ₁ *)
          nraenv_core_sem e2 env1 d d2 -> (* Γc ; γ₁ ; d ⊢〚e₂〛⇓ d₂ *)
          nraenv_core_sem (cNRAEnvAppEnv e2 e1) env d d2 (* ⇒ Γc ; γ ; d ⊢〚e₂ ∘ᵉ e₁〛⇓ d₂ *)
      | sem_cNRAEnvMapEnv : forall e c1 d c2,
          nraenv_core_sem_map_env e c1 d c2 -> (* ∧ Γc ; {c₁} ; d ⊢〚e〛χᵉ ⇓ {c₂} *)
          nraenv_core_sem (* ⇒ Γc ; {c₁} ; d ⊢〚χᵉ⟨e⟩〛⇓ {c₂} *)
            (cNRAEnvMapEnv e) (dcoll c1) d (dcoll c2)
      with nraenv_core_sem_map: nraenv_core -> data -> list data -> list data -> Prop :=
      | sem_cNRAEnvMap_empty : forall e env,
          nraenv_core_sem_map e env nil nil (* Γc ; γ ; {} ⊢〚e〛χ ⇓ {} *)
      | sem_cNRAEnvMap_cons : forall e env d1 c1 d2 c2,
          nraenv_core_sem e env d1 d2 -> (* Γc ; γ ; d₁ ⊢〚e〛⇓ d₂ *)
          nraenv_core_sem_map e env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e〛χ ⇓ {c₂} *)
          nraenv_core_sem_map e env (d1::c1) (d2::c2) (* ⇒ Γc ; γ ; {d₁::c₁} ⊢〚e〛χ ⇓ {d₂::c₂} *)
      with nraenv_core_sem_map_product: nraenv_core -> data -> list data -> list data -> Prop :=
      | sem_cNRAEnvMapProduct_empty : forall e env,
          nraenv_core_sem_map_product e env nil nil (* Γc ; γ ; {} ⊢〚e〛⋈ᵈ ⇓ {} *)
      | sem_cNRAEnvMapProduct_cons : forall e env d1 c1 c2 c3 c4,
          nraenv_core_sem e env d1 (dcoll c3) -> (* Γc ; γ ; d₁ ⊢〚e〛⋈ᵈ ⇓ {c₃} *)
          map_concat_sem d1 c3 c4 -> (* ∧ d₁ χ⊕ c₃ ⇓ c₄ *)
          nraenv_core_sem_map_product e env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e〛⋈ᵈ ⇓ {c₂} *)
          nraenv_core_sem_map_product e env (d1::c1) (c4 ++ c2) (* ⇒ Γc ; γ ; {d₁::c₁} ⊢〚e〛⋈ᵈ ⇓ {c₄}∪{c₂} *)
      with nraenv_core_sem_select: nraenv_core -> data -> list data -> list data -> Prop :=
      | sem_cNRAEnvSelect_empty : forall e env,
          nraenv_core_sem_select e env nil nil (* Γc ; γ ; {} ⊢〚e〛σ ⇓ {} *)
      | sem_cNRAEnvSelect_true : forall e env d1 c1 c2,
          nraenv_core_sem e env d1 (dbool true) -> (* Γc ; γ ; d₁ ⊢〚e〛σ ⇓ true *)
          nraenv_core_sem_select e env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e〛σ ⇓ {c₂} *)
          nraenv_core_sem_select e env (d1::c1) (d1::c2) (* ⇒ Γc ; γ ; {d₁::c₁} ⊢〚e〛σ ⇓ {d₁::c₂} *)
      | sem_cNRAEnvSelect_false : forall e env d1 c1 c2,
          nraenv_core_sem e env d1 (dbool false) -> (* Γc ; γ ; d₁ ⊢〚e〛σ ⇓ false *)
          nraenv_core_sem_select e env c1 c2 -> (* ∧ Γc ; γ ; {c₁} ⊢〚e〛σ ⇓ {c₂} *)
          nraenv_core_sem_select e env (d1::c1) c2 (* ⇒ Γc ; γ ; {d₁::c₁} ⊢〚e〛σ ⇓ {c₂} *)
      with nraenv_core_sem_map_env: nraenv_core -> list data -> data -> list data -> Prop :=
      | sem_cNRAEnvMapEnv_empty : forall e d,
          nraenv_core_sem_map_env e nil d nil (* Γc ; {} ; d ⊢〚e〛χᵉ ⇓ {} *)
      | sem_cNRAEnvMapEnv_cons : forall e d1 d c1 d2 c2,
          nraenv_core_sem e d1 d d2 -> (* Γc ; d₁ ; d ⊢〚e〛⇓ d₂ *)
          nraenv_core_sem_map_env e c1 d c2 -> (* ∧ Γc ; {c₁} ; d ⊢〚e〛χᵉ ⇓ {c₂} *)
          nraenv_core_sem_map_env e (d1::c1) d (d2::c2) (* ⇒ Γc ; {d₁::c₁} ; d ⊢〚e〛χᵉ ⇓ {d₂::c₂} *)
      .

    End Denotation.

    Section Evaluation.

      Fixpoint nraenv_core_eval (e:nraenv_core) (envin: data) (din:data) : option data :=
        match e with
        | cNRAEnvGetConstant s =>
          edot constant_env s
        | cNRAEnvID =>
          Some din
        | cNRAEnvConst rd =>
          Some (normalize_data h rd)
        | cNRAEnvBinop bop e1 e2 =>
          olift2 (fun d1 d2 => binary_op_eval h bop d1 d2)
                 (nraenv_core_eval e1 envin din) (nraenv_core_eval e2 envin din)
        | cNRAEnvUnop uop e =>
          olift (fun d1 => unary_op_eval h uop d1)
                (nraenv_core_eval e envin din)
        | cNRAEnvMap e2 e1 =>
          let aux_map d :=
              lift_oncoll
                (fun c1 => lift dcoll (lift_map (nraenv_core_eval e2 envin) c1)) d
          in olift aux_map (nraenv_core_eval e1 envin din)
        | cNRAEnvMapProduct e2 e1 =>
          let aux_mapconcat d :=
              lift_oncoll
                (fun c1 => lift dcoll (omap_product (nraenv_core_eval e2 envin) c1)) d
          in olift aux_mapconcat (nraenv_core_eval e1 envin din)
        | cNRAEnvProduct e1 e2 =>
          let aux_product d :=
              lift_oncoll
                (fun c1 => lift dcoll (omap_product (fun _ => nraenv_core_eval e2 envin din) c1)) d
          in olift aux_product (nraenv_core_eval e1 envin din)
        | cNRAEnvSelect e2 e1 =>
          let pred d1 :=
              match nraenv_core_eval e2 envin 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 (nraenv_core_eval e1 envin din)
        | cNRAEnvDefault e1 e2 =>
          olift (fun d1 =>
                   match d1 with
                   | dcoll nil => nraenv_core_eval e2 envin din
                   | _ => Some d1
                   end)
                (nraenv_core_eval e1 envin din)
        | cNRAEnvEither e1 e2 =>
          match din with
          | dleft d1 => nraenv_core_eval e1 envin d1
          | dright d2 => nraenv_core_eval e2 envin d2
          | _ => None
          end
        | cNRAEnvEitherConcat e1 e2 =>
          match nraenv_core_eval e1 envin din, nraenv_core_eval e2 envin 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
        | cNRAEnvApp e2 e1 =>
          olift (fun d1 => nraenv_core_eval e2 envin d1) (nraenv_core_eval e1 envin din)
        | cNRAEnvEnv =>
          Some envin
        | cNRAEnvAppEnv e2 e1 =>
          olift (fun env1 => nraenv_core_eval e2 env1 din) (nraenv_core_eval e1 envin din)
        | cNRAEnvMapEnv e =>
          lift_oncoll
            (fun c1 => lift dcoll
                            (lift_map ((fun env1 => nraenv_core_eval e env1 din)) c1)) envin
        end.

    End Evaluation.

    Section EvalCorrect.
      Lemma nraenv_core_eval_map_correct : forall e env l1 l2,
        (forall env d1 d2 : data,
            nraenv_core_eval e env d1 = Some d2 -> nraenv_core_sem e env d1 d2) ->
        lift_map (nraenv_core_eval e env) l1 = Some l2 ->
        nraenv_core_sem_map e env l1 l2.
          
      Lemma nraenv_core_eval_map_product_correct : forall e env l1 l2,
        (forall env d1 d2 : data,
            nraenv_core_eval e env d1 = Some d2 -> nraenv_core_sem e env d1 d2) ->
        omap_product (nraenv_core_eval e env) l1 = Some l2 ->
        nraenv_core_sem_map_product e env l1 l2.

      Lemma nraenv_core_eval_select_correct e env l1 l2 :
        (forall env d1 d2 : data,
            nraenv_core_eval e env d1 = Some d2 -> nraenv_core_sem e env d1 d2) ->
        lift_filter
          (fun d1 : data =>
             match nraenv_core_eval e env 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 ->
        nraenv_core_sem_select e env 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 nraenv_core_eval_map_env_correct : forall e l1 d l2,
        (forall env d1 d2 : data,
            nraenv_core_eval e env d1 = Some d2 -> nraenv_core_sem e env d1 d2) ->
        lift_map (fun env1 : data => nraenv_core_eval e env1 d) l1 = Some l2 ->
        nraenv_core_sem_map_env e l1 d l2.


      Lemma nraenv_core_eval_correct : forall e env d1 d2,
          nraenv_core_eval e env d1 = Some d2 ->
          nraenv_core_sem e env d1 d2.
 

      Lemma nraenv_core_map_eval_complete e env c1 c2:
        (forall env d1 d2 : data,
            nraenv_core_sem e env d1 d2 -> nraenv_core_eval e env d1 = Some d2) ->
        (nraenv_core_sem_map e env c1 c2) ->
        lift dcoll (lift_map (nraenv_core_eval e env) c1) = Some (dcoll c2).

      Lemma nraenv_core_map_product_eval_complete e env c1 c2:
        (forall env d1 d2 : data,
            nraenv_core_sem e env d1 d2 -> nraenv_core_eval e env d1 = Some d2) ->
        (nraenv_core_sem_map_product e env c1 c2) ->
        lift dcoll (omap_product (nraenv_core_eval e env) c1) = Some (dcoll c2).
        
      Lemma nraenv_core_select_eval_complete e env c1 c2:
        (forall env d1 d2 : data,
            nraenv_core_sem e env d1 d2 -> nraenv_core_eval e env d1 = Some d2) ->
        (nraenv_core_sem_select e env c1 c2) ->
        lift dcoll
             (lift_filter
                (fun d0 : data =>
                   match nraenv_core_eval e env 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 nraenv_core_map_env_eval_complete e c1 d c2:
        (forall env d1 d2 : data,
            nraenv_core_sem e env d1 d2 -> nraenv_core_eval e env d1 = Some d2) ->
        (nraenv_core_sem_map_env e c1 d c2) ->
        lift dcoll (lift_map (fun env1 : data => nraenv_core_eval e env1 d) c1) = Some (dcoll c2).


      Lemma nraenv_core_eval_complete : forall e env d1 d2,
          nraenv_core_sem e env d1 d2 ->
          nraenv_core_eval e env d1 = Some d2.

      
      Theorem nraenv_core_eval_correct_and_complete : forall e env d d',
          nraenv_core_eval e env d = Some d' <-> nraenv_core_sem e env d d'.

    End EvalCorrect.


    Local Open Scope string_scope.
    Local Open Scope list_scope.

    Fixpoint nra_of_nraenv_core (ae:nraenv_core) : nra :=
      match ae with
      | cNRAEnvGetConstant s =>
        NRAGetConstant s
      | cNRAEnvID =>
        nra_data
      | cNRAEnvConst d =>
        NRAConst d
      | cNRAEnvBinop b ae1 ae2 =>
        NRABinop b (nra_of_nraenv_core ae1) (nra_of_nraenv_core ae2)
      | cNRAEnvUnop u ae1 =>
        NRAUnop u (nra_of_nraenv_core ae1)
      | cNRAEnvMap ea1 ea2 =>
        NRAMap (nra_of_nraenv_core ea1)
               (unnest_two
                  "a1"
                  "PDATA"
                  (NRAUnop OpBag (nra_wrap_a1 (nra_of_nraenv_core ea2))))
      | cNRAEnvMapProduct ea1 ea2 =>
        (NRAMap (NRABinop OpRecConcat
                          (NRAUnop (OpDot "PDATA") NRAID)
                          (NRAUnop (OpDot "PDATA2") NRAID))
                (NRAMapProduct
                   (NRAMap (NRAUnop (OpRec "PDATA2") NRAID) (nra_of_nraenv_core ea1))
                   (unnest_two
                      "a1"
                      "PDATA"
                      (NRAUnop OpBag (nra_wrap_a1 (nra_of_nraenv_core ea2))))))
      | cNRAEnvProduct ea1 ea2 =>
        NRAProduct (nra_of_nraenv_core ea1) (nra_of_nraenv_core ea2)
      | cNRAEnvSelect ea1 ea2 =>
        (NRAMap (NRAUnop (OpDot "PDATA") NRAID)
                (NRASelect (nra_of_nraenv_core ea1)
                           (unnest_two
                              "a1"
                              "PDATA"
                              (NRAUnop OpBag (nra_wrap_a1 (nra_of_nraenv_core ea2))))))
      | cNRAEnvDefault ea1 ea2 =>
        NRADefault (nra_of_nraenv_core ea1) (nra_of_nraenv_core ea2)
      | cNRAEnvEither eal ear =>
        NRAApp
          (NRAEither (nra_of_nraenv_core eal) (nra_of_nraenv_core ear))
          (NRAEitherConcat
             (NRAApp (NRARecEither "PDATA") nra_data)
             (NRAUnop (OpRec "PBIND") nra_bind))
      | cNRAEnvEitherConcat ea1 ea2 =>
        NRAEitherConcat (nra_of_nraenv_core ea1) (nra_of_nraenv_core ea2)
      | cNRAEnvApp ea1 ea2 =>
        NRAApp (nra_of_nraenv_core ea1)
               (nra_wrap (nra_of_nraenv_core ea2))
      | cNRAEnvEnv => nra_bind
      | cNRAEnvAppEnv ea1 ea2 =>
        NRAApp (nra_of_nraenv_core ea1)
               (nra_context (nra_of_nraenv_core ea2) nra_data)
      | cNRAEnvMapEnv ea1 =>
        NRAMap (nra_of_nraenv_core ea1)
               (unnest_two
                  "a1"
                  "PBIND"
                  (NRAUnop OpBag (nra_wrap_bind_a1 nra_data)))
      end.

    Lemma lift_map_map_rec1 l s:
      lift_map (fun x : data => Some (drec ((s, x) :: nil))) l =
      Some (map (fun x : data => (drec ((s, x) :: nil))) l).
    
    Lemma lift_map_map_rec2 env a1 l :
      (lift_map
         (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 lift_map_map_rec3 d a1 l :
      (lift_map
         (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 lift_map_map_unnest2 env a l0 l1 :
      lift_map
        (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))
             (lift_map
                (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)
             (lift_map
                (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 lift_map_remove1 env l l2:
      lift_map
        (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 lift_map_remove2 d l l2:
    lift_map
      (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 lift_map_one1 env a l:
    lift_map
      (fun x : data =>
         match x with
           | drec r => edot r "PDATA"
           | _ => None
         end) (drec (("PBIND", env) :: ("PDATA", a) :: nil) :: l)
    =
    match
      lift_map
        (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 Semantics.
  
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
      | cNRAEnvGetConstant s => s :: nil
      | cNRAEnvID => nil
      | cNRAEnvConst rd => nil
      | cNRAEnvBinop _ q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvUnop _ q1 =>
        nraenv_core_free_vars q1
      | cNRAEnvMap q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvMapProduct q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvProduct q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvSelect q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvEither ql qr =>
        nraenv_core_free_vars ql ++ nraenv_core_free_vars qr
      | cNRAEnvEitherConcat q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvDefault q1 q2 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvApp q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvEnv => nil
      | cNRAEnvAppEnv q2 q1 =>
        nraenv_core_free_vars q1 ++ nraenv_core_free_vars q2
      | cNRAEnvMapEnv q1 =>
        nraenv_core_free_vars q1
      end.
  End FreeVars.

End RcNRAEnv2.

  
Notation "'ID'" := (cNRAEnvID) (at level 50) : nraenv_core_scope.
Notation "'ENV'" := (cNRAEnvEnv) (at level 50) : nraenv_core_scope.
Notation "CGET⟨ s ⟩" := (cNRAEnvGetConstant s) (at level 50) : nraenv_core_scope.
  
Notation "‵‵ c" := (cNRAEnvConst (dconst c)) (at level 0) : nraenv_core_scope.
Notation "‵ c" := (cNRAEnvConst c) (at level 0) : nraenv_core_scope.
Notation "‵{||}" := (cNRAEnvConst (dcoll nil)) (at level 0) : nraenv_core_scope.
Notation "‵[||]" := (cNRAEnvConst (drec nil)) (at level 50) : nraenv_core_scope.

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

Notation "¬( r1 )" := (cNRAEnvUnop OpNeg r1) (right associativity, at level 70): nraenv_core_scope.
Notation "♯distinct( r1 )" := (cNRAEnvUnop OpDistinct r1) (right associativity, at level 70): nraenv_core_scope.
Notation "♯count( r1 )" := (cNRAEnvUnop OpCount r1) (right associativity, at level 70): nraenv_core_scope.
Notation "♯flatten( d )" := (cNRAEnvUnop OpFlatten d) (at level 50) : nraenv_core_scope.

Notation "a1 ♯+ a2" := (cNRAEnvBinop (OpNatBinary NatPlus) a1 a2) (right associativity, at level 70): nraenv_core_scope.

Notation "a1 ♯- a2" := (cNRAEnvBinop (OpNatBinary NatMinus) a1 a2) (right associativity, at level 70): nraenv_core_scope.

Notation "‵{| d |}" := ((cNRAEnvUnop OpBag) d) (at level 50) : nraenv_core_scope.
Notation "‵[| ( s , r ) |]" := ((cNRAEnvUnop (OpRec s)) r) (at level 50) : nraenv_core_scope.
Notation "¬π[ s1 ]( r )" := ((cNRAEnvUnop (OpRecRemove s1)) r) (at level 50) : nraenv_core_scope.
Notation "π[ s1 ]( r )" := ((cNRAEnvUnop (OpRecProject s1)) r) (at level 50) : nraenv_core_scope.
Notation "p · r" := ((cNRAEnvUnop (OpDot r)) p) (left associativity, at level 40): nraenv_core_scope.

Notation "χ⟨ p ⟩( r )" := (cNRAEnvMap p r) (at level 70) : nraenv_core_scope.
Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (cNRAEnvMapProduct e2 e1) (at level 70) : nraenv_core_scope.
Notation "r1 × r2" := (cNRAEnvProduct r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "σ⟨ p ⟩( r )" := (cNRAEnvSelect p r) (at level 70) : nraenv_core_scope.
Notation "r1 ∥ r2" := (cNRAEnvDefault r1 r2) (right associativity, at level 70): nraenv_core_scope.
Notation "r1 ◯ r2" := (cNRAEnvApp r1 r2) (right associativity, at level 60): nraenv_core_scope.

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

Global Hint Resolve nraenv_core_eval_normalized : qcert.

Tactic Notation "nraenv_core_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "cNRAEnvGetConstant"%string
  | Case_aux c "cNRAEnvID"%string
  | Case_aux c "cNRAEnvConst"%string
  | Case_aux c "cNRAEnvBinop"%string
  | Case_aux c "cNRAEnvUnop"%string
  | Case_aux c "cNRAEnvMap"%string
  | Case_aux c "cNRAEnvMapProduct"%string
  | Case_aux c "cNRAEnvProduct"%string
  | Case_aux c "cNRAEnvSelect"%string
  | Case_aux c "cNRAEnvDefault"%string
  | Case_aux c "cNRAEnvEither"%string
  | Case_aux c "cNRAEnvEitherConcat"%string
  | Case_aux c "cNRAEnvApp"%string
  | Case_aux c "cNRAEnvEnv"%string
  | Case_aux c "cNRAEnvAppEnv"%string
  | Case_aux c "cNRAEnvMapEnv"%string].