"server side" for Soq

JSON.v

Require Import Utf8 String ZArith.

(* IO is done through this JSON inductive type *)
Inductive JSON :=
  | JObject : list (string * JSON) → JSON
  | JArray : list JSON → JSON
  | JString : string → JSON
  | JNumber : Z → JSON
  | JBool : bool → JSON
  | JNull : JSON.

(* for your specific project you need to provide two functions,
   from and to your datastructure

   TODO: use lens
*)

Definition to_bool (input:JSON) : option bool :=
  match input with
  | JBool a => Some a
  | _ => None
  end.

Definition to_json (input: bool) : JSON := JBool input.

(* once safely in your domain, you can do what you want with the thing. *)
Definition f : bool → bool := negb.


(* This function is called by the python wrapper *)
Definition process (input:JSON) : JSON :=
  match to_bool input with
  | Some a => to_json (f a)
  | None => JNull
  end.

Delimit Scope json_scope with json.
Local Notation "[ ]" := (JArray nil) : json_scope.
Local Notation "[ a , .. , b ]" := (JArray (a%json :: .. (b%json :: nil) ..)) : json_scope.
Local Notation "{ }" := (JObject nil) : json_scope.
Local Notation "tag : body" := (tag%string, body%json) (at level 50, no associativity) : json_object_entry.
Delimit Scope json_object_entry with json_object_entry.
Local Notation "{ a , .. , b }" := (JObject (a%json_object_entry :: .. (b%json_object_entry :: nil) ..)) : json_scope. 
Open Scope json_scope.
Coercion JString : string >-> JSON.

Definition test := {"hello" : JString "world" }.


Eval compute in (process (JBool false)).