Qcert.Backend.JSON

Section JSON.



  Context {fdata:foreign_data}.

  Inductive json : Set :=
  | jnil : json
  | jnumber : Z → json
  | jbool : bool → json
  | jstring : string → json
  | jarray : list json → json
  | jobject : list (string × json) → json
  | jforeign : foreign_data_type → json
  .

  Definition json_rect (P : json → Type)
             (fnil : P jnil)
             (fnumber : ∀ n : Z, P (jnumber n))
             (fbool : ∀ b : bool, P (jbool b))
             (fstring : ∀ s : string, P (jstring s))
             (farray : ∀ c : list json, Forallt P c → P (jarray c))
             (fobject : ∀ r : list (string × json), Forallt (fun ab ⇒ P (snd ab)) r → P (jobject r))
             (fforeign: ∀ fd, P (jforeign fd))
    :=
      fix F (j : json) : P j :=
    match j as j0 return (P j0) with
      | jnil ⇒ fnil
      | jnumber x ⇒ fnumber x
      | jbool x ⇒ fbool x
      | jstring x ⇒ fstring x
      | jarray x ⇒ farray x ((fix F2 (c : list json) : 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)
      | jobject x ⇒ fobject x ((fix F3 (r : list (string×json)) : 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)
      | jforeign fd ⇒ fforeign fd
    end.

  Definition json_ind (P : json → Prop)
             (fnil : P jnil)
             (fnumber : ∀ n : Z, P (jnumber n))
             (fbool : ∀ b : bool, P (jbool b))
             (fstring : ∀ s : string, P (jstring s))
             (farray : ∀ c : list json, Forall P c → P (jarray c))
             (fobject : ∀ r : list (string × json), Forall (fun ab ⇒ P (snd ab)) r → P (jobject r))
             (fforeign: ∀ fd, P (jforeign fd))
    :=
      fix F (j : json) : P j :=
    match j as j0 return (P j0) with
      | jnil ⇒ fnil
      | jnumber x ⇒ fnumber x
      | jbool x ⇒ fbool x
      | jstring x ⇒ fstring x
      | jarray x ⇒ farray x ((fix F2 (c : list json) : Forall P c :=
                            match c with
                              | nil ⇒ Forall_nil _
                              | cons j c0 ⇒ @Forall_cons _ P j c0 (F j) (F2 c0)
                            end) x)
      | jobject x ⇒ fobject x ((fix F3 (r : list (string×json)) : 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)
      | jforeign fd ⇒ fforeign fd
    end.

  Definition json_rec (P:json→Set) := json_rect P.

  Lemma jsonInd2 (P : json → Prop)
        (f : P jnil)
        (f0 : ∀ n : Z, P (jnumber n))
        (fb : ∀ b : bool, P (jbool b))
        (f1 : ∀ s : string, P (jstring s))
        (f2 : ∀ c : list json, (∀ x, In x c → P x) → P (jarray c))
        (f3 : ∀ r : list (string × json), (∀ x y, In (x,y) r → P y) → P (jobject r))
        (fforeign : ∀ fd, P (jforeign fd)):
    ∀ d, P d.

End JSON.