Module Qcert.Translation.DatatoSparkDF

Require Import Basics.
Require Import List.
Require Import String.
Require Import EquivDec.
Require Import Types.
Require Import Utils.
Require Import CommonRuntime.
Require Import ForeignDataTyping.
Require Import NNRCtoJavaScript.

Section DatatoSparkDF.

  Context {f:foreign_runtime}.
  Context {h:brand_relation_t}.
  Context {fttojs: ForeignToJavaScript.foreign_to_javascript}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.
  Context {m:brand_model}.
  Context {ftjson:foreign_to_JSON}.

  Definition data_to_blob (d: data): string :=
    dataToJS quotel_double d.

  Lemma dataToJS_correctly_escapes_quote_inside_string:
    dataToJS """" (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 jnil
    | 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, (Collet) =>
      let listo := map (flip typed_data_to_json et) xs in
      lift jarray (listo_to_olist listo)
    | drec fs, RecClosed 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 in
      lift (fun fields => jobject (("$blob"%string, jstring "")
                                     :: ("$known"%string, jobject fields) :: nil))
           (convert_fields fs ft)
    | drec fs, RecOpen 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
              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
    | dleft l, Eitherlt rt =>
      lift (fun l => jobject (("$left"%string, l)::("$right"%string, jnil)::nil))
           (typed_data_to_json l lt)
    | dright r, Eitherlt rt =>
      lift (fun r => jobject (("$left"%string, jnil)::("$right"%string, r)::nil))
           (typed_data_to_json r rt)
    | dbrand bs v, Brandbts =>
      Some (jobject (("$data"%string, jstring (data_to_blob v))
                       :: ("$type"%string, jarray (map jstring bs)) :: nil))
    | _, _ => None

  Definition typed_data_to_json_string (d: data) (r: rtype): string :=
    match typed_data_to_json d (proj1_sig r) with
    | Some json => jsonToJS """" 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."

  Context {ftojson:foreign_to_JSON}.
  Definition data_to_sjson (d:data) (r:rtype) : option string :=
    lift (jsonToJS """") (typed_data_to_json d (proj1_sig r)).

End DatatoSparkDF.