Module Qcert.Translation.Lang.DatatoSparkDF

Require Import Basics.
Require Import List.
Require Import String.
Require Import EquivDec.
Require Import Types.
Require Import Utils.
Require Import DataRuntime.
Require Import ForeignDataTyping.
Require Import JSONRuntime.
Require Import EJsonRuntime.
Require Import ForeignDataToEJson.
Require Import DataToEJson.

Section DatatoSparkDF.

  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}.
  Context {h:brand_relation_t}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.
  Context {m:brand_model}.

  Definition data_to_blob (d: data): string :=
    ejsonStringify quotel_double (data_to_ejson d).

  Lemma dataToJS_correctly_escapes_quote_inside_string:
    data_to_blob (dstring "abc""cde") = """abc\""cde"""%string.
  
  Fixpoint typed_data_to_json (d: data) (r: rtype₀): option json :=
    match d, r with
    | _, Top₀ => Some (jstring (data_to_blob d))
    | dunit, Unit₀ => Some jnull
    | dnat i, Nat₀ => Some (jnumber (float_of_int i))
    | dfloat i, Float₀ => Some (jnumber i)
    | dbool b, Bool₀ => Some (jbool b)
    | dstring s, String₀ => Some (jstring s)
    | dcoll xs, (Coll₀ et) =>
      let listo := map (flip typed_data_to_json et) xs in
      lift jarray (listo_to_olist listo)
    | drec fs, Rec₀ Closed ft =>
      let fix convert_fields ds ts :=
          match ds, ts with
          | nil, nil => Some nil
          | nil, _ => None
          | _, nil => None
          | ((f, d)::ds), ((_, t)::ts) =>
            match typed_data_to_json d t, convert_fields ds ts with
            | Some json, Some tail => Some ((f, json)::tail)
            | _, _ => None
            end
          end in
      lift (fun fields => jobject (("$blob"%string, jstring "")
                                     :: ("$known"%string, jobject fields) :: nil))
           (convert_fields fs ft)
    | drec fs, Rec₀ Open ft =>
      let fix convert_known_fields ds ts us :=
          match ts, ds with
          | nil, ds => Some (nil, us ++ ds)
          | _, nil => None
          | ((tf, t)::ts), ((df, d)::ds) =>
            if string_dec tf df
            then match typed_data_to_json d t, convert_known_fields ds ts us with
                 | Some json, Some (tail, us) => Some (((tf, json)::tail), us)
                 | _, _ => None
                 end
            else
              convert_known_fields ds ts ((df, d)::us)
          end in
      match convert_known_fields fs ft nil with
      | Some (typed_fields, dotdot) =>
        Some (jobject (("$blob"%string, jstring (data_to_blob (drec dotdot)))
                         :: ("$known"%string, jobject typed_fields) :: nil))
      | None => None
      end
    | dleft l, Either₀ lt rt =>
      lift (fun l => jobject (("$left"%string, l)::("$right"%string, jnull)::nil))
           (typed_data_to_json l lt)
    | dright r, Either₀ lt rt =>
      lift (fun r => jobject (("$left"%string, jnull)::("$right"%string, r)::nil))
           (typed_data_to_json r rt)
    | dbrand bs v, Brand₀ bts =>
      Some (jobject (("$class"%string, jarray (map jstring bs))
                       ::("$data"%string, jstring (data_to_blob v))
                       ::nil))
    | _, _ => None
    end.


  Definition typed_data_to_json_string (d: data) (r: rtype): string :=
    match typed_data_to_json d (proj1_sig r) with
    | Some json => jsonStringify """" json
    | None => "typed_data_to_json_string failed. This cannot happen. Get rid of this case by proving that typed_data_to_json always succeeds for well-typed data."
    end.

  
  Definition data_to_sjson (d:data) (r:rtype) : option string :=
    lift (jsonStringify """") (typed_data_to_json d (proj1_sig r)).

End DatatoSparkDF.