Module Qcert.Translation.Lang.ImpDatatoImpEJson

Require Import String.
Require Import List.
Require Import Bool.
Require Import Arith.
Require Import Utils.
Require Import JsAst.JsNumber.
Require Import Fresh.
Require Import DataRuntime.
Require Import ImpRuntime.
Require Import ForeignDataToEJson.
Require Import ForeignToEJsonRuntime.
Require Import DataToEJson.

Section ImpDatatoImpEJson.
  Import ListNotations.

  Context {fruntime:foreign_runtime}.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.
  Context {foreign_ejson_runtime_op : Set}.
  Context {fetojson:foreign_to_ejson foreign_ejson_model foreign_ejson_runtime_op}.
  Context {fejruntime:foreign_ejson_runtime foreign_ejson_runtime_op}.
  Context {fejtoruntime:foreign_to_ejson_runtime}.

  Context (h:brand_relation_t).

  Section Util.
    Definition mk_imp_ejson_expr_error msg : @imp_ejson_expr foreign_ejson_model foreign_ejson_runtime_op :=
      ImpExprError msg.
    Definition mk_imp_ejson_op op el : @imp_ejson_expr foreign_ejson_model foreign_ejson_runtime_op := ImpExprOp op el.
    Definition mk_imp_ejson_runtime_call op el : @imp_ejson_expr foreign_ejson_model foreign_ejson_runtime_op := ImpExprRuntimeCall op el.

    Definition mk_string s : @imp_ejson_expr foreign_ejson_model foreign_ejson_runtime_op := ImpExprConst (cejstring s).
    Definition mk_left e : imp_ejson_expr := mk_imp_ejson_op (EJsonOpObject ["$left"%string]) [ e ].
    Definition mk_right e : imp_ejson_expr := mk_imp_ejson_op (EJsonOpObject ["$right"%string]) [ e ].

    Definition mk_array el : imp_ejson_expr := mk_imp_ejson_runtime_call EJsonRuntimeArray el.
    Definition mk_object (el:list (string * imp_ejson_expr)) : imp_ejson_expr :=
      mk_imp_ejson_op (EJsonOpObject (map fst el)) (map snd el).
    Definition mk_string_array sl : imp_ejson_expr := mk_array (map ImpExprConst (map cejstring sl)).

    Fixpoint ejson_to_expr (j:ejson) : imp_ejson_expr
      := match j with
         | ejnull => ImpExprConst cejnull
         | ejnumber f => ImpExprConst (cejnumber f)
         | ejbigint n => ImpExprConst (cejbigint n)
         | ejbool b => ImpExprConst (cejbool b)
         | ejstring s => ImpExprConst (cejstring s)
         | ejarray ls => mk_array (map ejson_to_expr ls)
         | ejobject ls => mk_object (map (fun xy => (fst xy, ejson_to_expr (snd xy))) ls)
         | ejforeign fd => ImpExprConst (cejforeign fd)
         end.

    Definition sortCriterias_to_ejson_expr (scl: list (string * SortDesc)) : imp_ejson_expr :=
      mk_array (map ejson_to_expr (map sortCriteria_to_ejson scl)).

    Definition brands_to_ejson_expr sl : imp_ejson_expr :=
      mk_string_array sl.

    Definition mk_either_expr (el:list imp_ejson_expr) : imp_ejson_expr :=
      mk_imp_ejson_runtime_call EJsonRuntimeEither el.

    Definition mk_to_left_expr (el:list imp_ejson_expr) : imp_ejson_expr :=
      mk_imp_ejson_runtime_call EJsonRuntimeToLeft el.

    Definition mk_to_right_expr (el:list imp_ejson_expr) : imp_ejson_expr :=
      mk_imp_ejson_runtime_call EJsonRuntimeToRight el.

    Lemma imp_data_model_to_list_comm d :
      lift (map ejson_to_data) (imp_ejson_model_to_list (data_to_ejson d)) =
      imp_data_model_to_list d.

    Lemma imp_ejson_model_to_list_comm d :
      (imp_ejson_model_to_list (data_to_ejson d)) =
      lift (map data_to_ejson) (imp_data_model_to_list d).

    Lemma data_to_bool_ejson_to_bool_correct j:
      imp_data_model_to_bool (ejson_to_data j) = imp_ejson_model_to_bool j.

    Lemma ejson_to_data_to_Z_comm j:
      imp_data_model_to_Z (ejson_to_data j) = imp_ejson_model_to_Z j.

    Lemma data_to_ejson_to_Z_comm d:
      imp_data_model_to_Z d = imp_ejson_model_to_Z (data_to_ejson d).

    Lemma ejson_lifted_fbag_comm l:
      lifted_fbag l =
      ejson_numbers (map data_to_ejson l).

    Lemma ejson_lifted_stringbag_comm l:
      lifted_stringbag l =
      ejson_strings (map data_to_ejson l).

  End Util.

  Section Translation.
    
    Definition imp_data_unary_op_to_imp_ejson (op:unary_op) el : imp_ejson_expr :=
      match el with
      | [e] =>
        match op with
        | OpIdentity => e
        | OpNeg => mk_imp_ejson_op EJsonOpNot [ e ]
        | OpRec s => mk_imp_ejson_op (EJsonOpObject [key_encode s]) [ e ]
        | OpDot s => mk_imp_ejson_runtime_call EJsonRuntimeRecDot [ e; ImpExprConst (cejstring (key_encode s)) ]
        | OpRecRemove s => mk_imp_ejson_runtime_call EJsonRuntimeRecRemove [ e; mk_string (key_encode s) ]
        | OpRecProject fl =>
          mk_imp_ejson_runtime_call
            EJsonRuntimeRecProject ([ e ] ++ [ mk_string_array (map key_encode fl) ])
        | OpBag => mk_array el
        | OpSingleton => mk_imp_ejson_runtime_call EJsonRuntimeSingleton el
        | OpFlatten => mk_imp_ejson_runtime_call EJsonRuntimeFlatten el
        | OpDistinct => mk_imp_ejson_runtime_call EJsonRuntimeDistinct el
        | OpOrderBy scl =>
          mk_imp_ejson_runtime_call
            EJsonRuntimeSort (sortCriterias_to_ejson_expr scl :: e :: nil)
        | OpCount => mk_imp_ejson_runtime_call EJsonRuntimeCount el
        | OpToString => mk_imp_ejson_runtime_call EJsonRuntimeToString el
        | OpToText => mk_imp_ejson_runtime_call EJsonRuntimeToText el
        | OpLength => mk_imp_ejson_runtime_call EJsonRuntimeLength el
        | OpSubstring start len =>
          let start := ImpExprConst (cejbigint start) in
          match len with
          | Some len =>
            let args :=
                let len := ImpExprConst (cejbigint len) in
                [ e; start; len ]
            in
            mk_imp_ejson_runtime_call EJsonRuntimeSubstring args
          | None =>
            let args := [ e; start ] in
            mk_imp_ejson_runtime_call EJsonRuntimeSubstringEnd args
          end
        | OpLike pat =>
          mk_imp_ejson_runtime_call EJsonRuntimeLike [ ImpExprConst (cejstring pat); e ]
        | OpLeft => mk_left e
        | OpRight => mk_right e
        | OpBrand b =>
          mk_object [ ("$class"%string, brands_to_ejson_expr (canon_brands h b)); ("$data"%string, e) ]
        | OpUnbrand => mk_imp_ejson_runtime_call EJsonRuntimeUnbrand el
        | OpCast b =>
          mk_imp_ejson_runtime_call EJsonRuntimeCast [ brands_to_ejson_expr b; e ]
        | OpNatUnary u =>
          let op :=
              match u with
              | NatAbs => EJsonRuntimeNatAbs
              | NatLog2 => EJsonRuntimeNatLog2
              | NatSqrt => EJsonRuntimeNatSqrt
              end
          in
          mk_imp_ejson_runtime_call op [ e ]
        | OpNatSum => mk_imp_ejson_runtime_call EJsonRuntimeNatSum el
        | OpNatMin => mk_imp_ejson_runtime_call EJsonRuntimeNatMin el
        | OpNatMax => mk_imp_ejson_runtime_call EJsonRuntimeNatMax el
        | OpNatMean => mk_imp_ejson_runtime_call EJsonRuntimeNatArithMean el
        | OpFloatOfNat => mk_imp_ejson_runtime_call EJsonRuntimeFloatOfNat el
        | OpFloatUnary u =>
          let op :=
              match u with
              | FloatNeg => EJsonOpNeg
              | FloatSqrt => EJsonOpMathSqrt
              | FloatExp => EJsonOpMathExp
              | FloatLog => EJsonOpMathLog
              | FloatLog10 => EJsonOpMathLog10
              | FloatCeil => EJsonOpMathCeil
              | FloatFloor => EJsonOpMathFloor
              | FloatAbs => EJsonOpMathAbs
              end
          in mk_imp_ejson_op op [ e ]
        | OpFloatTruncate => mk_imp_ejson_runtime_call EJsonRuntimeNatOfFloat [ e ]
        | OpFloatSum => mk_imp_ejson_runtime_call EJsonRuntimeFloatSum el
        | OpFloatMean => mk_imp_ejson_runtime_call EJsonRuntimeFloatArithMean el
        | OpFloatBagMin => mk_imp_ejson_runtime_call EJsonRuntimeFloatMin [ e ]
        | OpFloatBagMax => mk_imp_ejson_runtime_call EJsonRuntimeFloatMax [ e ]
        | OpForeignUnary fu =>
          mk_imp_ejson_runtime_call (EJsonRuntimeForeign (foreign_to_ejson_runtime_of_unary_op fu)) el
        end
      | _ => mk_imp_ejson_expr_error "wrong number of arguments"
      end.

    Definition imp_data_binary_op_to_imp_ejson (op:binary_op) el : imp_ejson_expr :=
      match el with
      | [e1; e2] =>
        match op with
        | OpEqual => mk_imp_ejson_runtime_call EJsonRuntimeEqual el
        | OpRecConcat => mk_imp_ejson_runtime_call EJsonRuntimeRecConcat el
        | OpRecMerge => mk_imp_ejson_runtime_call EJsonRuntimeRecMerge el
        | OpAnd => mk_imp_ejson_op EJsonOpAnd el
        | OpOr => mk_imp_ejson_op EJsonOpOr el
        | OpLt => mk_imp_ejson_runtime_call EJsonRuntimeNatLt el
        | OpLe => mk_imp_ejson_runtime_call EJsonRuntimeNatLe el
        | OpBagUnion => mk_imp_ejson_runtime_call EJsonRuntimeUnion [e1; e2]
        | OpBagDiff => mk_imp_ejson_runtime_call EJsonRuntimeMinus [e1; e2]
        | OpBagMin => mk_imp_ejson_runtime_call EJsonRuntimeMin [e1; e2]
        | OpBagMax => mk_imp_ejson_runtime_call EJsonRuntimeMax [e1; e2]
        | OpBagNth => mk_imp_ejson_runtime_call EJsonRuntimeNth [e1; e2]
        | OpContains => mk_imp_ejson_runtime_call EJsonRuntimeContains [e1; e2]
        | OpStringConcat => mk_imp_ejson_op EJsonOpAddString el
        | OpStringJoin => mk_imp_ejson_runtime_call EJsonRuntimeStringJoin [e1; e2]
        | OpNatBinary opa =>
          match opa with
          | NatPlus => mk_imp_ejson_runtime_call EJsonRuntimeNatPlus [e1; e2]
          | NatMinus => mk_imp_ejson_runtime_call EJsonRuntimeNatMinus [e1; e2]
          | NatMult => mk_imp_ejson_runtime_call EJsonRuntimeNatMult [e1; e2]
          | NatDiv => mk_imp_ejson_runtime_call EJsonRuntimeNatDiv [e1; e2]
          | NatRem => mk_imp_ejson_runtime_call EJsonRuntimeNatRem [e1; e2]
          | NatMin => mk_imp_ejson_runtime_call EJsonRuntimeNatMinPair [e1; e2]
          | NatMax => mk_imp_ejson_runtime_call EJsonRuntimeNatMaxPair [e1; e2]
          end
        | OpFloatBinary opa =>
          match opa with
          | FloatPlus => mk_imp_ejson_op EJsonOpAddNumber [e1; e2]
          | FloatMinus => mk_imp_ejson_op EJsonOpSub [e1; e2]
          | FloatMult => mk_imp_ejson_op EJsonOpMult [e1; e2]
          | FloatDiv => mk_imp_ejson_op EJsonOpDiv [e1; e2]
          | FloatPow => mk_imp_ejson_op EJsonOpMathPow [e1; e2]
          | FloatMin => mk_imp_ejson_op EJsonOpMathMin [e1; e2]
          | FloatMax => mk_imp_ejson_op EJsonOpMathMax [e1; e2]
          end
        | OpFloatCompare opa =>
          match opa with
          | FloatLt => mk_imp_ejson_op EJsonOpLt [e1; e2]
          | FloatLe => mk_imp_ejson_op EJsonOpLe [e1; e2]
          | FloatGt => mk_imp_ejson_op EJsonOpGt [e1; e2]
          | FloatGe => mk_imp_ejson_op EJsonOpGe [e1; e2]
          end
        | OpForeignBinary fb =>
          mk_imp_ejson_runtime_call (EJsonRuntimeForeign (foreign_to_ejson_runtime_of_binary_op fb)) el
        end
      | _ => mk_imp_ejson_expr_error "imp_data_binary_op_to_imp_ejson: wrong number of arguments"
      end.

    Definition imp_data_op_to_imp_ejson (op:imp_data_op) el : imp_ejson_expr :=
      match op with
      | DataOpUnary op => imp_data_unary_op_to_imp_ejson op el
      | DataOpBinary op => imp_data_binary_op_to_imp_ejson op el
      end.

    Definition imp_data_runtime_call_to_imp_ejson
               (op:imp_data_runtime_op)
               (el:list imp_ejson_expr) : imp_ejson_expr :=
      match op with
      | DataRuntimeGroupby s ls =>
        mk_imp_ejson_runtime_call
          EJsonRuntimeGroupBy
          ((ImpExprConst (cejstring (key_encode s)))
             :: (mk_string_array (map key_encode ls))
             :: el)
      | DataRuntimeEither => mk_either_expr el
      | DataRuntimeToLeft => mk_to_left_expr el
      | DataRuntimeToRight => mk_to_right_expr el
      end.

    Fixpoint imp_data_expr_to_imp_ejson (exp: imp_data_expr) : imp_ejson_expr :=
      match exp with
      | ImpExprError msg => ImpExprError msg
      | ImpExprVar v => ImpExprVar v
      | ImpExprConst d => ejson_to_expr (data_to_ejson (normalize_data h d))
      | ImpExprOp op el => imp_data_op_to_imp_ejson op (map imp_data_expr_to_imp_ejson el)
      | ImpExprRuntimeCall op el => imp_data_runtime_call_to_imp_ejson op (map imp_data_expr_to_imp_ejson el)
      end.

    Fixpoint imp_data_stmt_to_imp_ejson (stmt: imp_data_stmt): imp_ejson_stmt :=
      match stmt with
      | ImpStmtBlock lv ls =>
        ImpStmtBlock
          (map (fun xy => (fst xy, lift imp_data_expr_to_imp_ejson (snd xy))) lv)
          (map imp_data_stmt_to_imp_ejson ls)
      | ImpStmtAssign v e =>
        ImpStmtAssign v (imp_data_expr_to_imp_ejson e)
      | ImpStmtFor v e s =>
        ImpStmtFor v
                   (imp_data_expr_to_imp_ejson e)
                   (imp_data_stmt_to_imp_ejson s)
      | ImpStmtForRange v e1 e2 s =>
        ImpStmtForRange v
                        (imp_data_expr_to_imp_ejson e1)
                        (imp_data_expr_to_imp_ejson e2)
                        (imp_data_stmt_to_imp_ejson s)
      | ImpStmtIf e s1 s2 =>
        ImpStmtIf (imp_data_expr_to_imp_ejson e)
                  (imp_data_stmt_to_imp_ejson s1)
                  (imp_data_stmt_to_imp_ejson s2)
      end.

    Definition imp_data_function_to_imp_ejson (f:imp_data_function) : imp_ejson_function :=
      match f with
      | ImpFun v s ret => ImpFun v (imp_data_stmt_to_imp_ejson s) ret
      end.

    Definition imp_data_to_imp_ejson (i:imp_data) : imp_ejson :=
      match i with
      | ImpLib l =>
        ImpLib
          (List.map
             (fun (decl: string * imp_data_function) =>
                let (name, def) := decl in (name, imp_data_function_to_imp_ejson def))
             l)
      end.
  End Translation.

  Section Correctness.
    Lemma dsum_to_ejson_sum l :
      match match dsum l with
            | Some a' => Some (dnat a')
            | None => None
            end with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_bigints (map data_to_ejson l) with
      | Some zl => Some (ejbigint (fold_right BinInt.Z.add BinNums.Z0 zl))
      | None => None
      end.

    Lemma lifted_zbag_is_ejson_bigint l:
      lifted_zbag l = ejson_bigints (map data_to_ejson l).

    Lemma dmin_to_ejson_min l:
      match lifted_min l with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_bigints (map data_to_ejson l) with
      | Some zl => Some (ejbigint (bnummin zl))
      | None => None
      end.

    Lemma dmax_to_ejson_max l:
      match lifted_max l with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_bigints (map data_to_ejson l) with
      | Some zl => Some (ejbigint (bnummax zl))
      | None => None
      end.

    Ltac rewrite_string_dec_from_neq H
      := let d := fresh "d" in
          let neq := fresh "neq" in
          destruct (string_dec_from_neq H) as [d neq]
          ; repeat rewrite neq in *
          ; clear d neq.

    Lemma eval_ejson_to_expr_string_array_correct σ l:
      olift (imp_ejson_runtime_eval h EJsonRuntimeArray)
            (lift_map (fun x : option imp_ejson_model => x)
                      (map (fun x : imp_ejson_expr => imp_ejson_expr_eval h (lift_pd_bindings σ) x)
                           (map ImpExprConst (map cejstring l))))
      = Some (ejarray (map ejstring l)).

    Lemma eval_ejson_to_expr_sort_criteria_correct σ a:
      imp_ejson_expr_eval h (lift_pd_bindings σ) (ejson_to_expr (sortCriteria_to_ejson a))
      = Some (sortCriteria_to_ejson a).

    Lemma eval_ejson_to_expr_sort_criterias_correct σ s:
      olift (imp_ejson_runtime_eval h EJsonRuntimeArray)
            (lift_map (fun x : option imp_ejson_model => x)
                      (map (fun x : imp_ejson_expr => imp_ejson_expr_eval h (lift_pd_bindings σ) x)
                           (map ejson_to_expr (map sortCriteria_to_ejson s))))
      = Some (ejarray (map sortCriteria_to_ejson s)).

    Lemma imp_data_unary_op_to_imp_ejson_expr_correct
           (σ:pd_bindings) (u:unary_op) (el:list imp_expr) :
      Forall
        (fun exp : imp_expr =>
           unlift_result (imp_data_expr_eval h σ exp) =
           imp_ejson_expr_eval
             h (lift_pd_bindings σ) (imp_data_expr_to_imp_ejson exp)) el ->
      unlift_result (imp_data_expr_eval h σ (ImpExprOp (DataOpUnary u) el)) =
      imp_ejson_expr_eval h
                          (lift_pd_bindings σ)
                          (imp_data_unary_op_to_imp_ejson u (map imp_data_expr_to_imp_ejson el)).

    Lemma imp_data_binary_op_to_imp_ejson_expr_correct
           (σ:pd_bindings) (b:binary_op) (el:list imp_expr) :
      Forall
        (fun exp : imp_expr =>
           unlift_result (imp_data_expr_eval h σ exp) =
           imp_ejson_expr_eval
             h
             (lift_pd_bindings σ) (imp_data_expr_to_imp_ejson exp)) el ->
      unlift_result (imp_data_expr_eval h σ (ImpExprOp (DataOpBinary b) el)) =
      imp_ejson_expr_eval h (lift_pd_bindings σ)
                          (imp_data_binary_op_to_imp_ejson b (map imp_data_expr_to_imp_ejson el)).

    Lemma Forall_lift_map σ el :
      Forall
        (fun exp : imp_expr =>
           unlift_result (imp_data_expr_eval h σ exp) =
           imp_ejson_expr_eval h (lift_pd_bindings σ) (imp_data_expr_to_imp_ejson exp)) el ->
      lift (map data_to_ejson) (lift_map (fun x : ImpEval.imp_expr => imp_data_expr_eval h σ x) el)
      =
      (lift_map
         (fun x : imp_data_expr =>
            imp_ejson_expr_eval h (lift_pd_bindings σ) (imp_data_expr_to_imp_ejson x)) el).

    Lemma data_to_ejson_drec_not_left l jl:
      data_to_ejson (drec l) <> ejobject [("$left"%string, jl)].

    Lemma data_to_ejson_drec_not_right l jl:
      data_to_ejson (drec l) <> ejobject [("$right"%string, jl)].

    Lemma imp_data_runtime_call_to_imp_ejson_correct
          (σ:pd_bindings) (rt:imp_data_runtime_op) (el:list imp_expr) :
      Forall
        (fun exp : imp_expr =>
           unlift_result (imp_data_expr_eval h σ exp) =
           imp_ejson_expr_eval h (lift_pd_bindings σ) (imp_data_expr_to_imp_ejson exp)) el ->
      unlift_result (imp_data_expr_eval h σ (ImpExprRuntimeCall rt el)) =
      imp_ejson_expr_eval h (lift_pd_bindings σ)
                          (imp_data_runtime_call_to_imp_ejson rt (map imp_data_expr_to_imp_ejson el)).

    Lemma imp_data_op_to_imp_ejson_correct
          (σ:pd_bindings) (op:imp_data_op) (el:list imp_expr) :
      Forall
        (fun exp : imp_expr =>
           unlift_result (imp_data_expr_eval h σ exp) =
           imp_ejson_expr_eval h (lift_pd_bindings σ) (imp_data_expr_to_imp_ejson exp)) el ->
      unlift_result (imp_data_expr_eval h σ (ImpExprOp op el)) =
      imp_ejson_expr_eval h (lift_pd_bindings σ)
                          (imp_data_op_to_imp_ejson op (map imp_data_expr_to_imp_ejson el)).

    Lemma ejson_to_expr_string_array_to_constant (l:list string) :
      map ejson_to_expr (map ejstring l)
      = map ImpExprConst (map cejstring l).

    Lemma zip_both_map {A} {B} (l:list (A * B)) :
      zip (map fst l) (map snd l) = Some l.
      
    Lemma eval_map_snd_ejson_constant_to_expr_correct σ r:
      Forall
        (fun ab : string * ejson =>
           imp_ejson_expr_eval h (lift_pd_bindings σ) (ejson_to_expr (snd ab)) = Some (snd ab)) r ->
      lift_map
        (fun x : string * ejson => imp_ejson_expr_eval h (lift_pd_bindings σ) (ejson_to_expr (snd x))) r
      =
      Some (map snd r).

    Lemma eval_ejson_constant_to_expr_correct σ j:
      imp_ejson_expr_eval h (lift_pd_bindings σ) (ejson_to_expr j)
      = Some j.

    Lemma imp_data_expr_to_imp_ejson_expr_correct (σ:pd_bindings) (exp:imp_data_expr) :
      unlift_result (imp_data_expr_eval h σ exp) =
      imp_ejson_expr_eval h (lift_pd_bindings σ)
                          (imp_data_expr_to_imp_ejson exp).

    Lemma map_lift_pd_bindings_unfold_eq (σ : pd_bindings) :
      map (fun xy : string * option ejson => (fst xy, lift ejson_to_data (snd xy)))
          (map (fun xy : string * option data => (fst xy, lift data_to_ejson (snd xy))) σ) = σ.

    Lemma map_lift_pd_bindings_eq (σ : pd_bindings) :
      map (fun xy : string * option ejson => (fst xy, lift ejson_to_data (snd xy))) (lift_pd_bindings σ) = σ.

    Lemma imp_data_decls_to_imp_ejson_decls_correct
          (σ:pd_bindings)
          (el:list (string * option imp_data_expr)) :
      unlift_result_env
        (imp_data_decls_eval h σ el) =
      imp_ejson_decls_eval
        h (lift_pd_bindings σ)
        (map (fun xy : var * option imp_data_expr => (fst xy, lift imp_data_expr_to_imp_ejson (snd xy))) el).

    Lemma imp_fold_qcert_stmt_to_imp_ejson_stmt_correct (σ:pd_bindings) sl :
      (Forall
         (fun stmt : imp_stmt =>
            forall (σ : pd_bindings),
              unlift_result_env (imp_data_stmt_eval h stmt σ) =
              imp_ejson_stmt_eval
                h (imp_data_stmt_to_imp_ejson stmt) (lift_pd_bindings σ)) sl) ->
      (unlift_result_env
        (fold_left
           (fun (c : option ImpEval.pd_rbindings) (s : ImpEval.imp_stmt) =>
              match c with
              | Some σ' => imp_data_stmt_eval h s σ'
              | None => None
              end) sl
           (Some
              (map
                 (fun xy : string * option ejson =>
                    (fst xy, match snd xy with
                             | Some a' => Some (ejson_to_data a')
                             | None => None
                             end)) (lift_pd_bindings σ))))
         =
         fold_left
           (fun (c : option ImpEval.pd_rbindings) (s : ImpEval.imp_stmt) =>
              match c with
              | Some σ' => imp_ejson_stmt_eval h s σ'
              | None => None
              end) (map (imp_data_stmt_to_imp_ejson) sl) (Some (lift_pd_bindings σ))).

    Lemma imp_data_stmt_to_imp_ejson_stmt_correct (σ:pd_bindings) (stmt:imp_data_stmt) :
      unlift_result_env (imp_data_stmt_eval h stmt σ) =
      imp_ejson_stmt_eval h (imp_data_stmt_to_imp_ejson stmt) (lift_pd_bindings σ).

    Lemma imp_data_function_to_imp_ejson_function_correct (d:data) (f:imp_data_function) :
      imp_data_function_eval h f d =
      lift ejson_to_data (imp_ejson_function_eval h (imp_data_function_to_imp_ejson f) (data_to_ejson d)).

    Lemma imp_data_function_to_imp_ejson_function_aux_correct (d:data) (f:imp_data_function) :
      lift data_to_ejson (imp_data_function_eval h f d) =
      imp_ejson_function_eval h (imp_data_function_to_imp_ejson f) (data_to_ejson d).

    Lemma push_rec_sort_in_map env :
      (rec_sort (map (fun xy : string * data => (fst xy, data_to_ejson (snd xy))) env))
      = (map (fun xy : string * data => (fst xy, data_to_ejson (snd xy))) (rec_sort env)).

    Theorem imp_data_to_imp_ejson_correct (σc:bindings) (q:imp_data) :
      imp_data_eval_top h σc q =
      imp_ejson_eval_top h σc (imp_data_to_imp_ejson q).

  End Correctness.

End ImpDatatoImpEJson.