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


Eval compute in (process (JBool false)).