Module DatatoSparkDF

Require Import Basics.
Require Import List.
Require Import String.
Require Import EquivDec.

Require Import Types.
Require Import BasicRuntime.
Require Import ForeignDataTyping.
Require Import NNRCtoJavaScript.
Require Import ForeignToJSON.
Require Import JSON.
Require Import JSONtoData.


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}.

  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 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, jnil)::nil))
           (typed_data_to_json l lt)
    | dright r, Either₀ lt rt =>
      lift (fun r => jobject (("$left"%string, jnil)::("$right"%string, r)::nil))
           (typed_data_to_json r rt)
    | dbrand bs v, Brand₀ bts =>
      Some (jobject (("$data"%string, jstring (data_to_blob v))
                       :: ("$type"%string, jarray (map jstring bs)) :: 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 => 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."
    end.

  Lemma test_json_with_toplevel_brand:
    (typed_data_to_json
       (dbrand ("Person"%string::nil)
               (drec (("age"%string, dnat 35)
                        :: ("name"%string, dstring "Fred")
                        :: ("friends"%string, dcoll ((dbrand ("Person"%string::nil)
                                                             (drec (("age"%string, dnat 42)
                                                                      :: ("name"%string, dstring "Berta")
                                                                      :: ("friends"%string, dcoll nil) :: nil))) :: nil)) :: nil)))
       (Brand₀ ("Person"%string::nil)))
    = Some
        (jobject
           (("$data"%string,
             jstring
               "{""age"": 35, ""name"": ""Fred"", ""friends"": [{""type"": [""Person""], ""data"": {""age"": 42, ""name"": ""Berta"", ""friends"": []}}]}")
              :: ("$type"%string, jarray (jstring "Person" :: nil)) :: nil)).

  Lemma test_json_with_nested_brand:
    (typed_data_to_json
       (drec (("age"%string, dnat 35)
                :: ("name"%string, dstring "Fred")
                :: ("friends"%string, dcoll ((dbrand ("Person"%string::nil)
                                                     (drec (("age"%string, dnat 42)
                                                              :: ("name"%string, dstring "Berta")
                                                              :: ("friends"%string, dcoll nil) :: nil))) :: nil)) :: nil))
       (Rec₀ Closed (("age"%string, Nat₀)
                       :: ("name"%string, String₀)
                       :: ("friends"%string, (Coll₀ (Brand₀ ("Person"%string::nil)))) :: nil)))
    = Some
        (jobject
           (("$blob"%string, jstring "")
              :: ("$known"%string,
                  jobject
                    (("age"%string, jnumber 35)
                       :: ("name"%string, jstring "Fred")
                       :: ("friends"%string,
                           jarray
                             (jobject
                                (("$data"%string, jstring "{""age"": 42, ""name"": ""Berta"", ""friends"": []}")
                                   :: ("$type"%string, jarray (jstring "Person" :: nil)) :: nil) :: nil)) :: nil)) :: nil)).

  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.