Module Qcert.Translation.Model.DataToEJson

Require Import List.
Require Import String.
Require Import Ascii.
Require Import ZArith.
Require Import Utils.
Require Import DataRuntime.
Require Import EJsonRuntime.
Require Import ForeignDataToEJson.

Section DataToEJson.
  Context {fruntime:foreign_runtime}.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.
  Context {foreign_ejson_runtime_op : Set}.
  Context {fdatatoejson:foreign_to_ejson foreign_ejson_model foreign_ejson_runtime_op}.

  Lemma string_dec_from_neq {a b} (pf:a <> b) : exists pf2, string_dec a b = right pf2.

  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.

  Section toData.
    Fixpoint ejson_to_data (j:ejson) : data :=
      match j with
      | ejnull => dunit
      | ejnumber n => dfloat n
      | ejbigint n => dnat n
      | ejbool b => dbool b
      | ejstring s => dstring s
      | ejarray c => dcoll (map ejson_to_data c)
      | ejobject ((s1,j')::nil) =>
        if (string_dec s1 "$left") then dleft (ejson_to_data j')
        else if (string_dec s1 "$right") then dright (ejson_to_data j')
             else drec ((key_decode s1, ejson_to_data j')::nil)
      | ejobject ((s1,ejarray j1)::(s2,j2)::nil) =>
        if (string_dec s1 "$class") then
          if (string_dec s2 "$data") then
            match (ejson_brands j1) with
            | Some br => dbrand br (ejson_to_data j2)
            | None => drec ((key_decode s1, dcoll (map ejson_to_data j1))::(key_decode s2, ejson_to_data j2)::nil)
            end
          else drec ((key_decode s1, dcoll (map ejson_to_data j1))::(key_decode s2, ejson_to_data j2)::nil)
        else drec ((key_decode s1, dcoll (map ejson_to_data j1))::(key_decode s2, ejson_to_data j2)::nil)
      | ejobject r => (drec (map (fun x => (key_decode (fst x), ejson_to_data (snd x))) r))
      | ejforeign fd => dforeign (foreign_to_ejson_to_data fd)
      end.

    Lemma ejson_is_record_some (j:ejson) r :
      ejson_is_record j = Some r ->
      ejson_to_data j = drec (map (fun x => (key_decode (fst x), ejson_to_data (snd x))) r).

    Lemma ejson_is_record_none (j:ejson):
      ejson_is_record j = None ->
      (forall r, ejson_to_data j <> drec r).

    Lemma ejson_is_either_some_left (j:ejson) jl :
      ejson_is_either j = Some (Some jl, None) ->
      ejson_to_data j = dleft (ejson_to_data jl).

    Lemma ejson_is_either_some_right (j:ejson) jr :
      ejson_is_either j = Some (None, Some jr) ->
      ejson_to_data j = dright (ejson_to_data jr).
      
    Lemma ejson_is_either_none (j:ejson) :
      ejson_is_either j = None ->
      (forall jl jr, ejson_to_data j <> dleft jl /\ ejson_to_data j <> dright jr).

  End toData.

  Section toEJson.

    Fixpoint data_to_ejson (d:data) : ejson :=
      match d with
      | dunit => ejnull
      | dnat n => ejbigint n
      | dfloat n => ejnumber n
      | dbool b => ejbool b
      | dstring s => ejstring s
      | dcoll c => ejarray (map data_to_ejson c)
      | drec r => ejobject (map (fun x => (key_encode (fst x), data_to_ejson (snd x))) r)
      | dleft d' => ejobject (("$left"%string, data_to_ejson d')::nil)
      | dright d' => ejobject (("$right"%string, data_to_ejson d')::nil)
      | dbrand b d' =>
        ejobject (("$class"%string, ejarray (map ejstring b))::("$data"%string, (data_to_ejson d'))::nil)
      | dforeign fd => ejforeign (foreign_to_ejson_from_data fd)
      end.

    Lemma data_to_ejson_on_drec r:
      data_to_ejson (drec (rec_sort r))
      = ejobject (rec_sort (map (fun xy : string * data => (key_encode (fst xy), data_to_ejson (snd xy))) r)).

    Lemma ejson_record_of_record r :
      ejson_is_record (data_to_ejson (drec r)) =
      Some (map (fun x => (key_encode (fst x), data_to_ejson (snd x))) r).

  End toEJson.

  Section ModelRoundTrip.
    Lemma ejson_brands_map_ejstring b : ejson_brands (map (@ejstring foreign_ejson_model) b) = Some b.

    Lemma data_to_ejson_idempotent d:
      ejson_to_data (data_to_ejson d) = d.

    Lemma data_to_ejson_inj j1 j2:
      data_to_ejson j1 = data_to_ejson j2 -> j1 = j2.

    Lemma data_to_ejson_equiv j1 j2:
      data_to_ejson j1 = data_to_ejson j2 <-> j1 = j2.
  End ModelRoundTrip.

  Section RuntimeLemmas.
    Lemma ejson_to_data_jobj_nbool l b : (ejson_to_data (ejobject l)) <> dbool b.

    Lemma ejson_to_data_jobj_nnat l n : (ejson_to_data (ejobject l)) <> dnat n.

    Lemma ejson_to_data_jobj_nfloat l f : (ejson_to_data (ejobject l)) <> dfloat f.

    Lemma ejson_to_data_jobj_nstring l s : (ejson_to_data (ejobject l)) <> dstring s.

    Lemma ejson_to_data_jobj_ncoll l c : (ejson_to_data (ejobject l)) <> dcoll c.

    Lemma ejson_to_data_object_not_boolean l b:
      ~(ejson_to_data (ejobject l) = dbool b).

    Lemma ejson_to_data_object_not_nat l n:
      ~(ejson_to_data (ejobject l) = dnat n).

    Lemma ejson_to_data_object_not_float l n:
      ~(ejson_to_data (ejobject l) = dfloat n).

    Lemma ejson_to_data_object_not_string l b:
      ~(ejson_to_data (ejobject l) = dstring b).

    Lemma ejson_to_data_object_not_coll l j:
      ~(ejson_to_data (ejobject l) = dcoll j).

    Lemma rec_ekey_encode_roundtrip s i0:
      drec ((s, ejson_to_data i0)::nil) = ejson_to_data (ejobject ((key_encode s, i0)::nil)).

    Lemma assoc_lookupr_key_encode_comm l s:
      match assoc_lookupr string_eqdec l s with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      assoc_lookupr
        string_eqdec (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l)
        (key_encode s).

    Lemma edot_key_encode_comm d s:
      match match d with
            | drec r => assoc_lookupr ODT_eqdec r s
            | _ => None
            end with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_is_record (data_to_ejson d) with
      | Some r => assoc_lookupr ODT_eqdec r (key_encode s)
      | None => None
      end.

    Lemma rremove_key_encode_comm d s:
      match
        match d with
        | drec r => Some (drec (rremove r s))
        | _ => None
        end
      with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_is_record (data_to_ejson d) with
      | Some r => Some (ejobject (rremove r (key_encode s)))
      | None => None
      end.

    Lemma map_rproject_key_encode_correct l pl:
      map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) (rproject l pl) =
      rproject (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l) (map key_encode pl).

    Lemma rproject_key_encode_comm d pl:
      match match d with
            | drec r => Some (drec (rproject r pl))
            | _ => None
            end with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_is_record (data_to_ejson d) with
      | Some r =>
        match match of_string_list (map (@ejstring foreign_ejson_model) (map key_encode pl)) with
              | Some a' => Some (rproject r a')
              | None => None
              end with
        | Some a' => Some (ejobject a')
        | None => None
        end
      | None => None
      end.

    Lemma mult_ejson_to_data a l :
      mult (bdistinct l) a =
      mult (map data_to_ejson (bdistinct l)) (data_to_ejson a).

    Lemma bdistinct_ejson_to_data_comm l :
      map data_to_ejson (bdistinct l) = bdistinct (map data_to_ejson l).

    Lemma lift_flat_map_eobject_is_none l l' :
      lift_flat_map
        (fun x : data => match x with
                         | dcoll y => Some y
                         | _ => None
                         end)
        (map (fun x : ejson => ejson_to_data x) (ejobject l :: l')) = None.

    Lemma flat_map_jflatten_roundtrip l :
      match
        match lift_flat_map (fun x : data => match x with
                                             | dcoll y => Some y
                                             | _ => None
                                             end) l with
        | Some a' => Some (dcoll a')
        | None => None
        end
      with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match jflatten (map data_to_ejson l) with
      | Some a' => Some (ejarray a')
      | None => None
      end.

    Lemma ejson_to_data_jobj_nbrand s e b d: (ejson_to_data (ejobject ((s, e)::nil))) <> dbrand b d.

    Lemma ejson_to_data_jobj_nbrand_long s e p p0 l b d:
      (ejson_to_data (ejobject ((s, e) :: p :: p0 :: l))) <> dbrand b d.

    Lemma ejson_to_data_jobj_nbrand_no_data e s0 e0 b d:
      s0 <> "$data"%string ->
      ejson_to_data (ejobject (("$class"%string, e)::(s0, e0)::nil)) <> dbrand b d.
      
    Lemma ejson_to_data_jobj_nbrand_no_class e s e0 b d:
      s <> "$class"%string ->
      ejson_to_data (ejobject ((s, e)::("$data"%string, e0)::nil)) <> dbrand b d.

    Lemma ejson_to_data_jobj_nbrand_no_class_no_data s e s0 e0 b d:
      s <> "$class"%string ->
      s0 <> "$data"%string ->
      ejson_to_data (ejobject ((s, e)::(s0, e0)::nil)) <> dbrand b d.

    Lemma ejson_data_maybe_brand s s0 e e0 :
      match ejson_to_data (ejobject ((s, e)::(s0, e0)::nil)) with
      | dbrand _ d' => Some d'
      | _ => None
      end =
      match
        match e with
        | ejarray j1 =>
          if string_dec s "$class"
          then
            if string_dec s0 "$data"
            then match ejson_brands j1 with
                 | Some _ => Some e0
                 | None => None
                 end
            else None
          else None
        | _ => None
        end
      with
      | Some a' => Some (ejson_to_data a')
      | None => None
      end.

    Lemma ejson_data_maybe_cast h b s s0 e e0 :
      match ejson_to_data (ejobject ((s, e)::(s0, e0)::nil)) with
      | dbrand b' _ =>
        if sub_brands_dec h b' b then Some (dsome (ejson_to_data (ejobject ((s, e)::(s0, e0)::nil)))) else Some dnone
      | _ => None
      end =
      match
        match e with
        | ejarray jl2 =>
          if string_dec s "$class"
          then
            if string_dec s0 "$data"
            then
              match ejson_brands jl2 with
              | Some b2 =>
                if sub_brands_dec h b2 b
                then Some (ejobject (("$left"%string, ejobject ((s, e)::(s0, e0)::nil))::nil))
                else Some (ejobject (("$right"%string, ejnull)::nil))
              | None => None
              end
            else None
          else None
        | _ => None
        end
      with
      | Some a' => Some (ejson_to_data a')
      | None => None
      end.

    Lemma bunion_map_comm l l0:
      map data_to_ejson (bunion l l0) =
      bunion (map data_to_ejson l) (map data_to_ejson l0).

    Lemma rec_concat_key_encode_comm l l0 :
      map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) (rec_sort (l ++ l0)) =
      rec_sort
        (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l ++
             map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l0).

    Lemma rconcat_key_encode_comm d d0:
      match
        match d with
        | drec r1 => match d0 with
                     | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
                     | _ => None
                     end
        | _ => None
        end
      with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_is_record (data_to_ejson d) with
      | Some r1 =>
        match ejson_is_record (data_to_ejson d0) with
        | Some r2 => Some (ejobject (rec_sort (r1 ++ r2)))
        | None => None
        end
      | None => None
      end.
    
    Lemma compatible_with_key_encode_comm s d l:
      compatible_with s d l =
      compatible_with (key_encode s) (data_to_ejson d)
                      (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l).

    Lemma compatible_key_encode_comm l l0:
      Compat.compatible l l0
      = Compat.compatible (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l)
                          (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l0).

    Lemma merge_bindings_key_encode_comm l l0 :
      lift
        (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))))
        (merge_bindings l l0) =
      merge_bindings (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l)
                     (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) l0).

    Lemma rmerge_key_encode_comm d d0:
      match
        match d with
        | drec r1 =>
          match d0 with
          | drec r2 =>
            match merge_bindings r1 r2 with
            | Some x => Some (dcoll (drec x::nil))
            | None => Some (dcoll nil)
            end
          | _ => None
          end
        | _ => None
        end
      with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_is_record (data_to_ejson d) with
      | Some r1 =>
        match ejson_is_record (data_to_ejson d0) with
        | Some r2 =>
          match merge_bindings r1 r2 with
          | Some x => Some (ejarray (ejobject x::nil))
          | None => Some (ejarray nil)
          end
        | None => None
        end
      | None => None
      end.
      
    Lemma nth_error_to_ejson_comm l n:
      lift data_to_ejson (nth_error l n)
      = nth_error (map data_to_ejson l) n.

    Lemma in_data_to_ejson_comm d l:
      In (data_to_ejson d) (map data_to_ejson l) <-> In d l.

    Lemma bunion_ejson_to_data_comm l1 l2:
      map data_to_ejson (bunion l1 l2) = bunion (map data_to_ejson l1) (map data_to_ejson l2).

    Lemma remove_one_ejson_to_data_comm d l:
      map data_to_ejson (remove_one d l) = remove_one (data_to_ejson d) (map data_to_ejson l).

    Lemma bminus_ejson_to_data_comm l1 l2:
      map data_to_ejson (bminus l1 l2) = bminus (map data_to_ejson l1) (map data_to_ejson l2).
    
    Lemma bmin_ejson_to_data_comm l1 l2:
      map data_to_ejson (bmin l1 l2) = bmin (map data_to_ejson l1) (map data_to_ejson l2).
    
    Lemma bmax_ejson_to_data_comm l1 l2:
      map data_to_ejson (bmax l1 l2) = bmax (map data_to_ejson l1) (map data_to_ejson l2).

    Definition data_to_ejson_partition (l:list (data * list data)) : list (ejson * list ejson) :=
      (map (fun xy => (data_to_ejson (fst xy),
                       (map data_to_ejson (snd xy))))) l.

    Lemma ejson_lift_map_rproject_correct kl l:
      lift (map data_to_ejson)
           (lift_map (fun d : data => match d with
                                      | drec r => Some (drec (rproject r kl))
                                      | _ => None
                                      end) l)
      =
      lift_map
        (fun d : ejson =>
           match ejson_is_record d with
           | Some r => Some (ejobject (rproject r (map key_encode kl)))
           | None => None
           end) (map data_to_ejson l).

    Lemma data_to_ejson_drec_inv kl l:
      ejobject (map (fun x : string * data => (key_encode (fst x), data_to_ejson (snd x))) (rproject l kl))
      = data_to_ejson (drec (rproject l kl)).

    Lemma ejson_key_is_eq_r_correct kl a a0:
      (key_is_eq_r (fun d : data => match d with
                                    | drec r => Some (drec (rproject r kl))
                                    | _ => None
                                    end) a0 a)
      =
      ejson_key_is_eq_r
        (fun j : ejson =>
           match ejson_is_record j with
           | Some r => Some (ejobject (rproject r (map key_encode kl)))
           | None => None
           end) (data_to_ejson a0) (data_to_ejson a).

    Lemma ejson_group_of_key_correct kl a l1:
      lift (map data_to_ejson)
           (group_of_key (fun d : data => match d with
                                          | drec r => Some (drec (rproject r kl))
                                          | _ => None
                                          end) a l1) =
      ejson_group_of_key
        (fun j : ejson =>
           match ejson_is_record j with
           | Some r => Some (ejobject (rproject r (map key_encode kl)))
           | None => None
           end) (data_to_ejson a) (map data_to_ejson l1).

    Lemma ejson_lift_map_group_of_key_correct kl l1 l2:
      lift data_to_ejson_partition
           (lift_map
              (fun k : data =>
                 match
                   group_of_key (fun d : data => match d with
                                                 | drec r => Some (drec (rproject r kl))
                                                 | _ => None
                                                 end) k l1
                 with
                 | Some x' => Some (k, x')
                 | None => None
                 end) l2)
      = lift_map
          (fun k : ejson =>
             match
               ejson_group_of_key
                 (fun j : ejson =>
                    match ejson_is_record j with
                    | Some r => Some (ejobject (rproject r (map key_encode kl)))
                    | None => None
                    end) k (map data_to_ejson l1)
             with
             | Some x' => Some (k, x')
             | None => None
             end) (map data_to_ejson l2).

    Lemma ejson_group_by_nested_eval_correct kl l:
      lift data_to_ejson_partition
           (group_by_nested_eval
              (fun d : data => match d with
                               | drec r => Some (drec (rproject r kl))
                               | _ => None
                               end) l)
      =
      (ejson_group_by_nested_eval
         (fun j : ejson =>
            match ejson_is_record j with
            | Some r => Some (ejobject (rproject r (map key_encode kl)))
            | None => None
            end) (map data_to_ejson l)).

    Lemma ejson_group_to_partitions_correct g a:
      lift data_to_ejson (group_to_partitions g a)
      =
      ejson_group_to_partitions (key_encode g) (data_to_ejson (fst a), map data_to_ejson (snd a)).

    Lemma ejson_to_partition_correct g ol:
      lift (map data_to_ejson) (olift (to_partitions g) ol)
      = olift (ejson_to_partitions (key_encode g)) (lift data_to_ejson_partition ol).

    Lemma ejson_group_by_nested_eval_keys_correct g kl l:
      lift (map data_to_ejson)
           (group_by_nested_eval_keys_partition
              g
              (fun d : data => match d with
                               | drec r => Some (drec (rproject r kl))
                               | _ => None
                               end) l)
      =
      ejson_group_by_nested_eval_keys_partition
        (key_encode g)
        (fun j : ejson =>
           match ejson_is_record j with
           | Some r => Some (ejobject (rproject r (map key_encode kl)))
           | None => None
           end) (map data_to_ejson l).

    Lemma group_by_data_to_ejson_correct g kl l:
      match match group_by_nested_eval_table g kl l with
            | Some dl' => Some (dcoll dl')
            | None => None
            end with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end =
      match ejson_group_by_nested_eval_table (key_encode g) (map key_encode kl) (map data_to_ejson l) with
      | Some a' => Some (ejarray a')
      | None => None
      end.

    Definition sortCriteria_to_ejson (sc: string * SortDesc) : (@ejson foreign_ejson_model) :=
      let (lbl, c) := sc in
      match c with
      | Ascending => ejobject (("asc"%string, ejstring (key_encode lbl))::nil)
      | Descending => ejobject (("desc"%string, ejstring (key_encode lbl))::nil)
      end.

    Lemma get_criteria_to_ejson_correct sc r:
      get_criteria sc r
      = ejson_get_criteria (sortCriteria_to_ejson sc) (map (fun x => (key_encode (fst x), data_to_ejson (snd x))) r).

    Lemma sortable_data_ejson_correct a s:
      lift (fun xy =>
              (fst xy,
               map (fun xy => (key_encode (fst xy),
                               data_to_ejson (snd xy))) (snd xy)))
           (fsortable_data_of_data a (map get_criteria s))
      = fsortable_data_of_data
          (map (fun xy : string * data => (key_encode (fst xy), data_to_ejson (snd xy))) a)
          (map ejson_get_criteria (map sortCriteria_to_ejson s)).
      
    Lemma map_record_comm l:
      lift (map (fun x => map (fun xy => (key_encode (fst xy), data_to_ejson (snd xy))) x))
           (lift_map (fun d : data => match d with
                                 | drec r => Some r
                                 | _ => None
                                 end) l)
      = (lift_map ejson_is_record (map data_to_ejson l)).

    Lemma fsortable_data_of_data_to_ejson_correct s l:
      lift (map (fun xy => (fst xy, map (fun xy => (key_encode (fst xy), data_to_ejson (snd xy))) (snd xy))))
           (lift_map (fun d : list (string * data) => fsortable_data_of_data d (map get_criteria s)) l)
      =
      lift_map
        (fun d : list (string * ejson) =>
           fsortable_data_of_data d (map ejson_get_criteria (map sortCriteria_to_ejson s)))
        (map
           (fun x : list (string * data) =>
              map (fun xy : string * data => (key_encode (fst xy), data_to_ejson (snd xy))) x) l).
      
    Lemma sortable_coll_to_ejson_correct s l:
      lift (map (fun x => map (fun xy => (key_encode (fst xy), data_to_ejson (snd xy))) x))
           (lift coll_of_sortable_coll
                 (lift sort_sortable_coll
                       (fsortable_coll_of_coll (map get_criteria s) l)))
      = lift coll_of_sortable_coll
             (lift sort_sortable_coll
                   (fsortable_coll_of_coll (map ejson_get_criteria (map sortCriteria_to_ejson s))
                                           (map
                                              (fun x : list (string * data) =>
                                                 map (fun xy : string * data => (key_encode (fst xy), data_to_ejson (snd xy))) x)
                                              l))).

    Lemma order_by_to_ejson_correct s d :
      match data_sort (map get_criteria s) d with
      | Some a' => Some (data_to_ejson a')
      | None => None
      end
      = ejson_sort (map ejson_get_criteria (map sortCriteria_to_ejson s)) (data_to_ejson d).

  End RuntimeLemmas.

  Section Lift.
    Definition lift_bindings (env:bindings) : jbindings :=
      List.map (fun xy => (fst xy, data_to_ejson (snd xy))) env.
    Definition lift_pd_bindings (env:pd_bindings) : pd_jbindings :=
      List.map (fun xy => (fst xy, lift data_to_ejson (snd xy))) env.
    Definition lift_result (res:option ejson) : option data :=
      lift ejson_to_data res.
    Definition unlift_result (res:option data) : option ejson :=
      lift data_to_ejson res.
    Definition lift_result_env (res:option pd_jbindings) : option pd_bindings :=
      lift (fun env => List.map (fun xy => (fst xy, lift ejson_to_data (snd xy))) env) res.
    Definition unlift_result_env (res:option pd_bindings) : option pd_jbindings :=
      lift (fun env => List.map (fun xy => (fst xy, lift data_to_ejson (snd xy))) env) res.
  End Lift.

End DataToEJson.