Module Qcert.EJson.Model.EJson

Require Import List.
Require Import Ascii.
Require Import String.
Require Import ZArith.
Require Import Bool.
Require Import FloatAdd.
Require Import ToString.
Require Import CoqLibAdd.
Require Import StringAdd.
Require Import Digits.
Require Import EquivDec.
Require Import ForeignEJson.
Require Import Utils.

Section EJson.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.

  Unset Elimination Schemes.

  Inductive ejson : Set :=
  | ejnull : ejson
  | ejnumber : float -> ejson
  | ejbigint : Z -> ejson
  | ejbool : bool -> ejson
  | ejstring : string -> ejson
  | ejarray : list ejson -> ejson
  | ejobject : list (string * ejson) -> ejson
  | ejforeign : foreign_ejson_model -> ejson
  .

  Set Elimination Schemes.

  Definition ejson_rect (P : ejson -> Type)
             (fnull : P ejnull)
             (fnumber : forall n : float, P (ejnumber n))
             (fbigint : forall n : Z, P (ejbigint n))
             (fbool : forall b : bool, P (ejbool b))
             (fstring : forall s : string, P (ejstring s))
             (farray : forall c : list ejson, Forallt P c -> P (ejarray c))
             (fobject : forall r : list (string * ejson), Forallt (fun ab => P (snd ab)) r -> P (ejobject r))
             (fforeign: forall fd, P (ejforeign fd))
    :=
      fix F (j : ejson) : P j :=
    match j as j0 return (P j0) with
      | ejnull => fnull
      | ejnumber x => fnumber x
      | ejbigint x => fbigint x
      | ejbool x => fbool x
      | ejstring x => fstring x
      | ejarray x => farray x ((fix F2 (c : list ejson) : Forallt P c :=
                            match c as c0 with
                              | nil => Forallt_nil _
                              | cons j c0 => @Forallt_cons _ P j c0 (F j) (F2 c0)
                            end) x)
      | ejobject x => fobject x ((fix F3 (r : list (string*ejson)) : Forallt (fun ab => P (snd ab)) r :=
                           match r as c0 with
                             | nil => Forallt_nil _
                             | cons sj c0 => @Forallt_cons _ (fun ab => P (snd ab)) sj c0 (F (snd sj)) (F3 c0)
                           end) x)
      | ejforeign fd => fforeign fd
    end.

  Definition ejson_ind (P : ejson -> Prop)
             (fnull : P ejnull)
             (fnumber : forall n : float, P (ejnumber n))
             (fbigint : forall n : Z, P (ejbigint n))
             (fbool : forall b : bool, P (ejbool b))
             (fstring : forall s : string, P (ejstring s))
             (farray : forall c : list ejson, Forall P c -> P (ejarray c))
             (fobject : forall r : list (string * ejson), Forall (fun ab => P (snd ab)) r -> P (ejobject r))
             (fforeign: forall fd, P (ejforeign fd))
    :=
      fix F (j : ejson) : P j :=
    match j as j0 return (P j0) with
      | ejnull => fnull
      | ejnumber x => fnumber x
      | ejbigint x => fbigint x
      | ejbool x => fbool x
      | ejstring x => fstring x
      | ejarray x => farray x ((fix F2 (c : list ejson) : Forall P c :=
                            match c with
                              | nil => Forall_nil _
                              | cons j c0 => @Forall_cons _ P j c0 (F j) (F2 c0)
                            end) x)
      | ejobject x => fobject x ((fix F3 (r : list (string*ejson)) : Forall (fun ab => P (snd ab)) r :=
                           match r with
                             | nil => Forall_nil _
                             | cons sj c0 => @Forall_cons _ (fun ab => P (snd ab)) sj c0 (F (snd sj)) (F3 c0)
                           end) x)
      | ejforeign fd => fforeign fd
    end.

  Definition ejson_rec (P:ejson->Set) := ejson_rect P.

  Lemma ejsonInd2 (P : ejson -> Prop)
        (f : P ejnull)
        (f0 : forall n : float, P (ejnumber n))
        (f1 : forall n : Z, P (ejbigint n))
        (f2 : forall b : bool, P (ejbool b))
        (f3 : forall s : string, P (ejstring s))
        (f4 : forall c : list ejson, (forall x, In x c -> P x) -> P (ejarray c))
        (f5 : forall r : list (string * ejson), (forall x y, In (x,y) r -> P y) -> P (ejobject r))
        (fforeign : forall fd, P (ejforeign fd)):
    forall d, P d.

  Lemma ejson_eq_dec : forall x y:ejson, {x=y}+{x<>y}.

  Global Instance ejson_eqdec : EqDec ejson eq := ejson_eq_dec.

  Section toString.

    Local Open Scope string.

    Fixpoint ejsonStringify (quotel:string) (j : ejson) : string
      := match j with
         | ejnull => "null"
         | ejnumber n => toString n
         | ejbigint n => toString n
         | ejbool b => toString b
         | ejstring s => stringToStringQuote quotel s
         | ejarray ls =>
           let ss := map (ejsonStringify quotel) ls in
           "[" ++ (concat ", " ss) ++ "]"
         | ejobject ls =>
           let ss := (map (fun kv =>
                             let '(k,v) := kv in
                             "" ++ quotel ++ "" ++ k ++ ""
                                ++ quotel ++ ": " ++ (ejsonStringify quotel v)) ls)
           in "{" ++ (concat ", " ss) ++ "}"
         | ejforeign fd => toString fd
         end.

  End toString.

  Section Util.
    Fixpoint of_string_list (d:list ejson) : option (list string) :=
      match d with
      | nil => Some nil
      | (ejstring s1) :: d' =>
        match of_string_list d' with
        | Some s' => Some (s1::s')
        | None => None
        end
      | _ => None
      end.

    Lemma of_string_list_map_ejstring sl :
      of_string_list (map ejstring sl) = Some sl.

    Lemma of_string_list_map_ejstring_f {A} (f:A -> string) (sl:list A) :
      of_string_list (map (fun x => (ejstring (f x))) sl) = Some (map f sl).

    Definition ejson_brands (d:list ejson) : option (list string) := of_string_list d.

    Lemma ejson_brands_map_ejstring b : ejson_brands (map ejstring b) = Some b.
    
    Fixpoint ejson_bigints (d:list ejson) : option (list Z) :=
      match d with
      | nil => Some nil
      | (ejbigint z1) :: d' =>
        match ejson_bigints d' with
        | Some s' => Some (z1::s')
        | None => None
        end
      | _ => None
      end.

    Fixpoint ejson_numbers (d:list ejson) : option (list float) :=
      match d with
      | nil => Some nil
      | (ejnumber n) :: d' =>
        match ejson_numbers d' with
        | Some s' => Some (n::s')
        | None => None
        end
      | _ => None
      end.

    Fixpoint ejson_strings (d:list ejson) : option (list string) :=
      match d with
      | nil => Some nil
      | (ejstring n) :: d' =>
        match ejson_strings d' with
        | Some s' => Some (n::s')
        | None => None
        end
      | _ => None
      end.

    Definition jflatten (d:list ejson) : option (list ejson) :=
      lift_flat_map (fun x =>
                       match x with
                       | ejarray y => Some y
                       | _ => None end) d.
    
    Definition ejson_is_record (j:ejson) : option (list (string * ejson)) :=
      match j with
      | ejobject ((s1,j')::nil) =>
        if (string_dec s1 "$left") then None
        else if (string_dec s1 "$right") then None
             else Some ((s1,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 => None
            | None => Some ((s1,ejarray j1)::(s2,j2)::nil)
            end
          else Some ((s1,ejarray j1)::(s2,j2)::nil)
        else Some ((s1,ejarray j1)::(s2,j2)::nil)
      | ejobject r => Some r
      | _ => None
      end.

    Definition ejson_is_either (j:ejson) : option (option ejson * option ejson) :=
      match j with
      | ejobject ((s1,j')::nil) =>
        if (string_dec s1 "$left") then Some (Some j', None)
        else if (string_dec s1 "$right") then Some (None, Some j')
             else None
      | ejobject _ => None
      | _ => None
      end.

  End Util.

  Section Env.
    Definition jbindings := list (string * ejson).
    Definition pd_jbindings := list (string * option ejson).
  End Env.

  Section CEJson.
    Inductive cejson : Set :=
    | cejnull : cejson
    | cejnumber : float -> cejson
    | cejbigint : Z -> cejson
    | cejbool : bool -> cejson
    | cejstring : string -> cejson
    | cejforeign : foreign_ejson_model -> cejson
    .

    Definition cejsonStringify (quotel:string) (j : cejson) : string
      := match j with
         | cejnull => "null"
         | cejnumber n => toString n
         | cejbigint n => toString n
         | cejbool b => toString b
         | cejstring s => stringToStringQuote quotel s
         | cejforeign fd => toString fd
         end.

  End CEJson.
End EJson.