Module JSONtoData

Section JSONtoData.

  Require Import List String.
  Require Import ZArith.
  Require Import Utils.
  Require Import BasicRuntime.
  Require Import JSON.
  Require Import ForeignToJSON.

  Context {fdata:foreign_data}.
  Fixpoint json_brands (d:list json) : option (list string) :=
    match d with
    | nil => Some nil
    | (jstring s1) :: d' =>
      match json_brands d' with
      | Some s' => Some (s1::s')
      | None => None
      end
    | _ => None
    end.

  Section toData.
    Context {ftojson:foreign_to_JSON}.


    Fixpoint json_to_data_pre (j:json) : data :=
      match foreign_to_JSON_to_data j with
      | Some fd => dforeign fd
      | None =>
        match j with
        | jnil => dunit
        | jnumber n => dnat n
        | jbool b => dbool b
        | jstring s => dstring s
        | jarray c => dcoll (map json_to_data_pre c)
        | jobject nil => drec nil
        | jobject ((s1,j')::nil) =>
          if (string_dec s1 "left") then dleft (json_to_data_pre j')
          else if (string_dec s1 "right") then dright (json_to_data_pre j')
               else drec ((s1, json_to_data_pre j')::nil)
        | jobject ((s1,jarray j1)::(s2,j2)::nil) =>
          if (string_dec s1 "type") then
            if (string_dec s2 "data") then
              match (json_brands j1) with
              | Some br => dbrand br (json_to_data_pre j2)
              | None => drec ((s1, dcoll (map json_to_data_pre j1))::(s2, json_to_data_pre j2)::nil)
              end
            else drec ((s1, dcoll (map json_to_data_pre j1))::(s2, json_to_data_pre j2)::nil)
          else drec ((s1, dcoll (map json_to_data_pre j1))::(s2, json_to_data_pre j2)::nil)
        | jobject ((s1,j1)::(s2,jarray j2)::nil) =>
          if (string_dec s1 "data") then
            if (string_dec s2 "type") then
              match (json_brands j2) with
              | Some br => dbrand br (json_to_data_pre j1)
              | None => drec ((s1, json_to_data_pre j1)::(s2, dcoll (map json_to_data_pre j2))::nil)
              end
            else drec ((s1, json_to_data_pre j1)::(s2, dcoll (map json_to_data_pre j2))::nil)
          else drec ((s1, json_to_data_pre j1)::(s2, dcoll (map json_to_data_pre j2))::nil)
        | jobject r => (drec (map (fun x => (fst x, json_to_data_pre (snd x))) r))
        | jforeign fd => dforeign fd
        end
      end.

    Definition json_to_data h (j:json) :=
      normalize_data h (json_to_data_pre j).


    Fixpoint json_enhanced_to_data_pre (j:json) :=
      match foreign_to_JSON_to_data j with
      | Some fd => dforeign fd
      | None =>
        match j with
        | jnil => dright dunit
        | jnumber n => dnat n
        | jbool b => dbool b
        | jstring s => dstring s
        | jarray c => dcoll (map json_enhanced_to_data_pre c)
        | jobject r =>
          let rfields := domain r in
          if (in_dec string_dec "key"%string rfields)
          then
            match edot r "key" with
            | Some (jstring key) => dleft (dstring key)
            | _ => drec (map (fun x => (fst x, json_enhanced_to_data_pre (snd x))) r)
            end
          else
            if (in_dec string_dec "$class"%string rfields)
            then
              match r with
              | (s1,jstring j1) :: rest =>
                if (string_dec s1 "$class") then
                  match (json_brands ((jstring j1)::nil)) with
                  | Some br => dbrand br (drec (map (fun x => (fst x, json_enhanced_to_data_pre (snd x))) rest))
                  | None => drec ((s1, dstring j1)::(map (fun x => (fst x, json_enhanced_to_data_pre (snd x))) rest))
                  end
                else drec (map (fun x => (fst x, json_enhanced_to_data_pre (snd x))) r)
              | _ =>
                drec (map (fun x => (fst x, json_enhanced_to_data_pre (snd x))) r)
              end
            else
              drec (map (fun x => (fst x, json_enhanced_to_data_pre (snd x))) r)
        | jforeign fd => dforeign fd
        end
      end.

    Definition json_enhanced_to_data h (j:json) :=
      normalize_data h (json_enhanced_to_data_pre j).
    
  End toData.

  Section toJSON.
    Context {ftojson:foreign_to_JSON}.

    Fixpoint data_enhanced_to_json (d:data) : json :=
      match d with
      | dunit => jnil
      | dnat n => jnumber n
      | dbool b => jbool b
      | dstring s => jstring s
      | dcoll c => jarray (map data_enhanced_to_json c)
      | drec r => jobject (map (fun x => (fst x, data_enhanced_to_json (snd x))) r)
      | dleft d' => jobject (("left"%string, data_enhanced_to_json d')::nil)
      | dright d' => jobject (("right"%string, data_enhanced_to_json d')::nil)
      | dbrand b (drec r) => jobject (("$class "%string, jarray (map jstring b))::(map (fun x => (fst x, data_enhanced_to_json (snd x))) r))
      | dbrand b d' => jobject (("$class"%string, jarray (map jstring b))::("$data"%string, (data_enhanced_to_json d'))::nil)
      | dforeign fd => foreign_to_JSON_from_data fd
      end.

    Fixpoint data_to_json (d:data) : json :=
      match d with
      | dunit => jnil
      | dnat n => jnumber n
      | dbool b => jbool b
      | dstring s => jstring s
      | dcoll c => jarray (map data_to_json c)
      | drec r => jobject (map (fun x => (fst x, data_to_json (snd x))) r)
      | dleft d' => jobject (("left"%string, data_to_json d')::nil)
      | dright d' => jobject (("right"%string, data_to_json d')::nil)
      | dbrand b d' => jobject (("type"%string, jarray (map jstring b))::("data"%string, (data_to_json d'))::nil)
      | dforeign fd => foreign_to_JSON_from_data fd
      end.
  End toJSON.

  Section toRType.
    Require Import Types.
    Require Import RTypeNorm.
    Require Import ForeignTypeToJSON.
    Context {ftype:foreign_type}.
    Context {ftypeToJSON:foreign_type_to_JSON}.

    Fixpoint json_to_rtype₀ (j:json) : rtype₀ :=
      match j with
      | jnil => Unit₀
      | jnumber _ => Unit₀
      | jbool _ => Unit₀
      | jarray _ => Unit₀
      | jstring "String" => String₀
      | jstring "Nat" => Nat₀
      | jstring "Bool" => Bool₀
      | jstring _ => Unit₀
      | jobject nil => Rec₀ Open nil
      | jobject (("$brand"%string,jarray jl)::nil) =>
        match json_brands jl with
        | Some brs => Brand₀ brs
        | None => Unit₀
        end
      | jobject (("$coll"%string,j')::nil) => Coll₀ (json_to_rtype₀ j')
      | jobject (("$option"%string,j')::nil) => Either₀ (json_to_rtype₀ j') Unit₀
      | jobject jl => Rec₀ Open (map (fun kj => ((fst kj), (json_to_rtype₀ (snd kj)))) jl)
      | jforeign _ => Unit₀
      end.

    Definition json_to_rtype {br:brand_relation} (j:json) :=
      normalize_rtype₀_to_rtype (json_to_rtype₀ j).

    Fixpoint json_to_rtype₀_with_fail (j:json) : option rtype₀ :=
      match j with
      | jnil => Some Unit₀
      | jnumber _ => None
      | jbool _ => None
      | jarray _ => None
      | jstring "String" => Some String₀
      | jstring "Nat" => Some Nat₀
      | jstring "Bool" => Some Bool₀
      | jstring s => lift Foreign₀ (foreign_to_string_to_type s)
      | jobject nil => Some (Rec₀ Open nil)
      | jobject (("$brand"%string,jarray jl)::nil) =>
        match json_brands jl with
        | Some brs => Some (Brand₀ brs)
        | None => None
        end
      | jobject (("$coll"%string,j')::nil) => lift Coll₀ (json_to_rtype₀_with_fail j')
      | jobject (("$option"%string,j')::nil) => lift (fun x => Either₀ x Unit₀) (json_to_rtype₀_with_fail j')
      | jobject jl =>
        lift (fun x => Rec₀ Open x)
             ((fix rmap_rec (l: list (string * json)) : option (list (string * rtype₀)) :=
                 match l with
                 | nil => Some nil
                 | (x,y)::l' =>
                   match rmap_rec l' with
                   | None => None
                   | Some l'' =>
                     match json_to_rtype₀_with_fail y with
                     | None => None
                     | Some y'' => Some ((x,y'') :: l'')
                     end
                   end
                 end) jl)
      | jforeign _ => None
      end.

    Definition json_to_rtype_with_fail {br:brand_relation} (j:json) : option rtype :=
      lift normalize_rtype₀_to_rtype (json_to_rtype₀_with_fail j).

  End toRType.

  Section toDType.
    Require Import Types.
    Require Import RTypeNorm.
    Require Import ForeignTypeToJSON.
    Context {ftype:foreign_type}.
    Context {ftypeToJSON:foreign_type_to_JSON}.

    Definition json_to_drtype {br:brand_relation} (j:json) : drtype :=
      match j with
      | jobject (("$dist"%string,j')::nil) => Tdistr (json_to_rtype j')
      | _ => Tlocal (json_to_rtype j)
      end.

    Definition json_to_drtype_with_fail {br:brand_relation} (j:json) : option drtype :=
      match j with
      | jobject (("$dist"%string,j')::nil) => lift Tdistr (json_to_rtype_with_fail j')
      | _ => lift Tlocal (json_to_rtype_with_fail j)
      end.

  End toDType.

  Section toVType.
    Require Import Types.
    Require Import RTypeNorm.
    Require Import ForeignTypeToJSON.
    Context {ftype:foreign_type}.
    Context {ftypeToJSON:foreign_type_to_JSON}.

    Definition json_to_vrtype_with_fail {br:brand_relation} (j:json) : option (string * rtype) :=
      match j with
      | jobject (("dist"%string,jstring s)::("type"%string,j')::nil) =>
        lift (fun x => (s,x)) (json_to_rtype_with_fail j')
      | jobject (("type"%string,j')::("dist"%string,jstring s)::nil) =>
        lift (fun x => (s,x)) (json_to_rtype_with_fail j')
      | _ => None
      end.

  End toVType.

  Section RoundTripping.
    Inductive json_data : data -> Prop :=
    | json_null : json_data dunit
    | json_nat n : json_data (dnat n)
    | json_bool b : json_data (dbool b)
    | json_string s : json_data (dstring s)
    | json_array dl : Forall (fun d => json_data d) dl -> json_data (dcoll dl)
    | json_rec r :
        is_list_sorted ODT_lt_dec (domain r) = true ->
        Forall (fun ab => json_data (snd ab)) r ->
        json_data (drec r)
    .
  
    Inductive pure_data : data -> Prop :=
    | pure_null : pure_data dunit
    | pure_nat n : pure_data (dnat n)
    | pure_bool b : pure_data (dbool b)
    | pure_string s : pure_data (dstring s)
    | pure_array dl : Forall (fun d => pure_data d) dl -> pure_data (dcoll dl)
    | pure_rec r :
        assoc_lookupr string_dec r "$left"%string = None ->
        assoc_lookupr string_dec r "$right"%string = None ->
        assoc_lookupr string_dec r "$class"%string = None ->
        is_list_sorted ODT_lt_dec (domain r) = true ->
        Forall (fun ab => pure_data (snd ab)) r ->
        pure_data (drec r)
    | pure_left d :
        pure_data d -> pure_data (dleft d)
    | pure_right d :
        pure_data d -> pure_data (dright d)
    | pure_brand b r :
        pure_data (drec r) -> pure_data (dbrand b (drec r))
    .

    Lemma pure_dcoll_inv c:
      Forall (fun d : data => pure_data d) c <-> pure_data (dcoll c).

    Lemma no_assoc_with_map (r:list (string*data)) (f:data->data) s:
      assoc_lookupr string_dec r s = None ->
      assoc_lookupr string_dec (map (fun x => (fst x, f (snd x))) r) s = None.
    
    Lemma domains_with_map (r:list (string*data)) (f:data->data):
      domain (map (fun x : string * data => (fst x, f (snd x))) r) = domain r.

    Lemma assoc_lookupr_skip {A} (a:string*A) (l:list (string*A)) (s:string):
      assoc_lookupr string_dec (a::l) s = None ->
      assoc_lookupr string_dec l s = None.

    Lemma pure_drec_cons_inv a r:
      pure_data (drec (a::r)) -> (pure_data (drec r) /\ pure_data (snd a)).
  End RoundTripping.

End JSONtoData.