Skip to content
Snippets Groups Projects
Commit e7dade35 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[lib/json] adopt Yojson.Basic type

parent b6652e6b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/libraries/utils/json.mli
+ 21
− 18
View file @ e7dade35
......@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
(** Json Library
(** Json Library
Remarks:
- UTF-8 escaping is not supported;
......@@ -30,17 +30,20 @@
for instance Zarith.
*)
(** Json Objects *)
type t =
| Null
| True | False
| String of string
| Number of string
| Int of int
| Float of float
| Array of t list
| Assoc of (string * t) list
(** Json Objects
Same type than [Yojson.Basic.json]
*)
type json =
[ `Assoc of (string * json) list
| `Bool of bool
| `Float of float
| `Int of int
| `List of json list
| `Null
| `String of string ]
type t = json
val equal : t -> t -> bool (** Pervasives *)
val compare : t -> t -> int (** Pervasives *)
val pp : Format.formatter -> t -> unit
......@@ -79,11 +82,11 @@ val save_file : ?pretty:bool -> string -> t -> unit
format. *)
val bool : t -> bool
(** Extract [True] and [False] only.
(** Extract [True] and [False] only.
@raise Invalid_argument when the conversion fails. *)
val int : t -> int
(** Convert [Null], [Int], [Float], [Number] and [String] to an [int].
(** Convert [Null], [Int], [Float], [Number] and [String] to an [int].
Floats are truncated with [int_of_float] and [Null] to 0.
@raise Invalid_argument when the conversion fails. *)
......@@ -97,19 +100,19 @@ val float : t -> float
@raise Invalid_argument when the conversion fails. *)
val array : t -> t array
(** Extract the array of an [Array] object.
(** Extract the array of an [Array] object.
[Null] is considered an empty array.
@raise Invalid_argument if the object is not an array. *)
val list : t -> t list
(** Extract the list of an [Array] object.
(** Extract the list of an [Array] object.
[Null] is considered an empty list.
@raise Invalid_argument if the object is not a list. *)
val fold : (string -> t -> 'a -> 'a) -> t -> 'a -> 'a
(** Fold over all fields of the object.
(** Fold over all fields of the object.
[Null] is considered an empty object.
Typical usage is [fold M.add t M.empty] where [M=Map.Make(String)].
Typical usage is [fold M.add t M.empty] where [M=Map.Make(String)].
@raise Invalid_argument if the object is not an [Assoc] or [Null] object. *)
val field : string -> t -> t
......
src/libraries/utils/json.mll
+ 64
− 70
View file @ e7dade35
......@@ -26,16 +26,16 @@
{
type t =
| Null
| True | False
| String of string
| Number of string
| Int of int
| Float of float
| Array of t list
| Assoc of (string * t) list
type json =
[ `Assoc of (string * json) list
| `Bool of bool
| `Float of float
| `Int of int
| `List of json list
| `Null
| `String of string ]
type t = json
let equal = (=)
let compare = Pervasives.compare
......@@ -88,15 +88,15 @@ let skip input =
*)
let rec parse_value input =
match input.token with
| EOF -> Null
| TRUE -> skip input ; True
| FALSE -> skip input ; False
| NULL -> skip input ; Null
| STR a -> skip input ; String a
| INT a -> skip input ; (try Int(int_of_string a) with _ -> Number a)
| DEC a -> skip input ; (try Float(float_of_string a) with _ -> Number a)
| KEY '[' -> skip input ; Array (parse_array [] input)
| KEY '{' -> skip input ; Assoc (parse_object [] input)
| EOF -> `Null
| TRUE -> skip input ; `Bool true
| FALSE -> skip input ; `Bool false
| NULL -> skip input ; `Null
| STR a -> skip input ; `String a
| INT a -> skip input ; (try `Int(int_of_string a) with _ -> `String a)
| DEC a -> skip input ; (try `Float(float_of_string a) with _ -> `String a)
| KEY '[' -> skip input ; `List (parse_array [] input)
| KEY '{' -> skip input ; `Assoc (parse_object [] input)
| _ -> failwith "unexpected token"
and parse_array es input =
......@@ -163,20 +163,18 @@ let load_file file =
let rec pp fmt v = let open Format in
match v with
| Null -> pp_print_string fmt "null"
| True -> pp_print_string fmt "true"
| False -> pp_print_string fmt "false"
| String s -> fprintf fmt "%S" s
| Number s -> pp_print_string fmt s
| Int a -> pp_print_int fmt a
| Float f -> pp_print_float fmt f
| Array [] -> pp_print_string fmt "[]"
| Array (e::es) ->
| `Null -> pp_print_string fmt "null"
| `Bool b -> pp_print_bool fmt b
| `String s -> fprintf fmt "%S" s
| `Int a -> pp_print_int fmt a
| `Float f -> pp_print_float fmt f
| `List [] -> pp_print_string fmt "[]"
| `List (e::es) ->
Format.fprintf fmt "@[<hov 2>[ %a" pp e ;
List.iter (fun e -> Format.fprintf fmt ",@ %a" pp e) es ;
Format.fprintf fmt " ]@]"
| Assoc [] -> pp_print_string fmt "{}"
| Assoc (e::es) ->
| `Assoc [] -> pp_print_string fmt "{}"
| `Assoc (e::es) ->
Format.fprintf fmt "@[<hov 2>{ %a" pp_entry e ;
List.iter (fun e -> Format.fprintf fmt ",@ %a" pp_entry e) es ;
Format.fprintf fmt " }@]"
......@@ -188,20 +186,19 @@ let dump_string f s =
f quote ; f (String.escaped s) ; f quote
let rec dump f = function
| Null -> f "null"
| True -> f "true"
| False -> f "false"
| String s -> dump_string f s
| Number s -> f s
| Int a -> f (string_of_int a)
| Float x -> f (string_of_float x)
| Array [] -> f "[]"
| Array (e::es) ->
| `Null -> f "null"
| `Bool true -> f "true"
| `Bool false -> f "false"
| `String s -> dump_string f s
| `Int a -> f (string_of_int a)
| `Float x -> f (string_of_float x)
| `List [] -> f "[]"
| `List (e::es) ->
f "[" ; dump f e ;
List.iter (fun e -> f "," ; dump f e) es ;
f "]"
| Assoc [] -> f "{}"
| Assoc (e::es) ->
| `Assoc [] -> f "{}"
| `Assoc (e::es) ->
f "{" ;
dump_entry f e ;
List.iter (fun e -> f "," ; dump_entry f e) es ;
......@@ -244,57 +241,54 @@ let save_file ?(pretty=true) file v =
let invalid name = raise (Invalid_argument ("Json." ^ name))
let bool = function
| True -> true
| False -> false
| `Bool b -> b
| _ -> invalid "bool"
let int = function
| Null -> 0
| Int n -> n
| Float f -> (try int_of_float f with _ -> invalid "int")
| Number s | String s -> (try int_of_string s with _ -> invalid "int")
| `Null -> 0
| `Int n -> n
| `Float f -> (try int_of_float f with _ -> invalid "int")
| _ -> invalid "int"
let float = function
| Null -> 0.0
| Float f -> f
| Int n -> (try float_of_int n with _ -> invalid "float")
| Number s | String s -> (try float_of_string s with _ -> invalid "float")
| `Null -> 0.0
| `Float f -> f
| `Int n -> (try float_of_int n with _ -> invalid "float")
| _ -> invalid "float"
let string = function
| Null -> ""
| Int n -> string_of_int n
| Float f -> string_of_float f
| Number s | String s -> s
| `Null -> ""
| `Int n -> string_of_int n
| `Float f -> string_of_float f
| `String s -> s
| _ -> invalid "string"
let list = function
| Null -> []
| Array es -> es
| `Null -> []
| `List es -> es
| _ -> invalid "list"
let array = function
| Null -> [| |]
| Array es -> Array.of_list es
| `Null -> [| |]
| `List es -> Array.of_list es
| _ -> invalid "array"
let field f = function
| Null -> raise Not_found
| Assoc fs -> List.assoc f fs
| `Null -> raise Not_found
| `Assoc fs -> List.assoc f fs
| _ -> invalid "field"
let fold f v w = match v with
| Null -> w
| Assoc fs -> List.fold_left (fun w (e,v) -> f e v w) w fs
| `Null -> w
| `Assoc fs -> List.fold_left (fun w (e,v) -> f e v w) w fs
| _ -> invalid "fold"
let of_bool b = if b then True else False
let of_int k = Int k
let of_string s = String s
let of_float f = Float f
let of_list xs = Array xs
let of_array xs = Array (Array.to_list xs)
let of_fields m = Assoc m
let of_bool b = `Bool b
let of_int k = `Int k
let of_string s = `String s
let of_float f = `Float f
let of_list xs = `List xs
let of_array xs = `List (Array.to_list xs)
let of_fields m = `Assoc m
}
src/plugins/report/classify.ml
+ 3
− 3
View file @ e7dade35
......@@ -150,7 +150,7 @@ let get_queue env plugin =
let add_rule jvalue =
try
match jvalue with
| Json.Assoc fields ->
| `Assoc fields ->
let tgt , rule = List.fold_left rule_of_fields default fields in
let properties p =
if rule.r_plugin <> (snd default).r_plugin then
......@@ -177,7 +177,7 @@ let configure file =
R.feedback "Loading '%a'" Datatype.Filepath.pretty path;
try
match Json.load_file file with
| Json.Array values -> List.iter add_rule values
| `List values -> List.iter add_rule values
| _ -> failwith "Array expected"
with
| Json.Error(file,line,msg) ->
......@@ -230,7 +230,7 @@ let json_of_source = function
]
let json_of_event e =
Json.Assoc
`Assoc
begin [
"classid" , Json.of_string e.e_id ;
"action" , Json.of_string @@ string_of_action e.e_action ;
......
src/plugins/wp/ProofScript.ml
+ 58
− 58
View file @ e7dade35
......@@ -91,7 +91,7 @@ let pattern p =
let occur p t =
Footprint.locate ~inside:(Lang.F.e_prop p) ~select:t
let j_select s = "select" , Json.String s
let j_select s = "select" , `String s
let j_goal = j_select "clause-goal"
let j_step = j_select "clause-step"
let j_ingoal = j_select "inside-goal"
......@@ -99,51 +99,51 @@ let j_instep = j_select "inside-step"
let j_compose = j_select "compose"
let j_kint = j_select "kint"
let j_range = j_select "range"
let j_id a = "id" , Json.String a
let j_at s = "at" , Json.Int s.id
let j_int z = "val" , Json.String (Integer.to_string z)
let j_min a = "min" , Json.Int a
let j_max b = "max" , Json.Int b
let j_kind s = "kind" , Json.String (s_kind s)
let j_pattern p = "pattern" , Json.String p
let j_id a = "id" , `String a
let j_at s = "at" , `Int s.id
let j_int z = "val" , `String (Integer.to_string z)
let j_min a = "min" , `Int a
let j_max b = "max" , `Int b
let j_kind s = "kind" , `String (s_kind s)
let j_pattern p = "pattern" , `String p
let j_ppattern p = j_pattern (pattern p)
let j_occur k = "occur" , Json.Int k
let j_occur k = "occur" , `Int k
let j_pred p =
let tgt = Pretty_utils.to_string Lang.F.pp_pred p in
"target" , Json.String tgt
"target" , `String tgt
let j_term e =
let tgt = Pretty_utils.to_string Lang.F.pp_term e in
"target" , Json.String tgt
"target" , `String tgt
let rec json_of_selection = function
| Empty -> Json.Null
| Empty -> `Null
| Compose code -> json_of_compose code
| Clause (Goal p) ->
Json.(Assoc[ j_goal ; j_pred p ; j_ppattern p ])
`Assoc[ j_goal ; j_pred p ; j_ppattern p ]
| Clause (Step s) ->
let p = Conditions.head s in
Json.(Assoc[ j_step ; j_at s ; j_kind s ; j_pred p ; j_ppattern p ])
`Assoc[ j_step ; j_at s ; j_kind s ; j_pred p ; j_ppattern p ]
| Inside(Goal p,e) ->
let n,m = occur p e in
Json.(Assoc [ j_ingoal ; j_occur n ; j_term e ; j_pattern m ])
`Assoc [ j_ingoal ; j_occur n ; j_term e ; j_pattern m ]
| Inside(Step s,e) ->
let n,m = occur (Conditions.head s) e in
Json.(Assoc [ j_instep ; j_at s ; j_kind s ; j_occur n ;
j_term e ; j_pattern m ])
`Assoc [ j_instep ; j_at s ; j_kind s ; j_occur n ;
j_term e ; j_pattern m ]
and j_args = function
| [] -> []
| es -> ["args" , Json.Array (List.map json_of_selection es)]
| es -> ["args" , `List (List.map json_of_selection es)]
and json_of_compose = function
| Cint a -> Json.(Assoc [j_kint ; j_int a])
| Range(a,b) -> Json.(Assoc [j_range ; j_min a ; j_max b])
| Code(_,id,es) -> Json.(Assoc (j_compose :: j_id id :: j_args es))
| Cint a -> `Assoc [j_kint ; j_int a]
| Range(a,b) -> `Assoc [j_range ; j_min a ; j_max b]
| Code(_,id,es) -> `Assoc (j_compose :: j_id id :: j_args es)
(* -------------------------------------------------------------------------- *)
(* --- Json to Selection --- *)
......@@ -193,12 +193,12 @@ let rec selection_of_json ((hs,g) as s : sequent) js =
let selection_target js = js >? "target" |> Json.string
let json_of_named = function
| None -> Json.Null
| None -> `Null
| Some a ->
Json.Assoc Tactical.[
"id" , Json.String a.vid ;
"title" , Json.String a.title ;
"descr" , Json.String a.descr ;
`Assoc Tactical.[
"id" , `String a.vid ;
"title" , `String a.title ;
"descr" , `String a.descr ;
]
let named_of_json find js =
......@@ -219,7 +219,7 @@ let json_of_param (tac : tactical) = function
| Spinner(fd,_) -> ident fd , Json.of_int (tac#get_field fd)
| Composer(fd,_) -> ident fd , json_of_selection (tac#get_field fd)
| Selector(fd,options,equal) ->
ident fd , Json.String
ident fd , `String
begin
try
let a = tac#get_field fd in
......@@ -260,7 +260,7 @@ let param_of_json (tac : tactical) seq js = function
end
let json_of_parameters (tac : tactical) =
Json.Assoc (List.map (json_of_param tac) tac#params)
`Assoc (List.map (json_of_param tac) tac#params)
let parameters_of_json (tac : tactical) sequent js =
List.iter (param_of_json tac sequent js) tac#params
......@@ -285,27 +285,27 @@ let jtactic ~title (tac : tactical) (sel : selection) =
}
let json_of_tactic t js =
Json.(Assoc [
"header" , Json.String t.header ;
"tactic" , Json.String t.tactic ;
`Assoc [
"header" , `String t.header ;
"tactic" , `String t.tactic ;
"params" , t.params ;
"select" , t.select ;
"children" , Json.Assoc js ;
])
"children" , `Assoc js ;
]
let children_of_json = function
| Json.Array js ->
| `List js ->
Wp_parameters.warning ~current:false ~once:true
"Deprecated script(s) found ; consider using prover 'tip'" ;
List.map (fun j -> "",j) js
| Json.Assoc fs -> fs
| `Assoc fs -> fs
| _ -> []
let tactic_of_json js =
try
let header = js >? "header" |> Json.string in
let tactic = js >? "tactic" |> Json.string in
let params = try js >? "params" with Not_found -> Json.Null in
let select = try js >? "select" with Not_found -> Json.Null in
let params = try js >? "params" with Not_found -> `Null in
let select = try js >? "select" with Not_found -> `Null in
let children = try js >? "children" |> children_of_json with Not_found -> [] in
Some( { header ; tactic ; params ; select } , children )
with _ -> None
......@@ -315,31 +315,31 @@ let tactic_of_json js =
(* -------------------------------------------------------------------------- *)
let json_of_verdict = function
| VCS.NoResult | VCS.Checked | VCS.Computing _ -> Json.String "none"
| VCS.Valid -> Json.String "valid"
| VCS.Unknown -> Json.String "unknown"
| VCS.Timeout -> Json.String "timeout"
| VCS.Stepout -> Json.String "stepout"
| VCS.Invalid -> Json.String "invalid"
| VCS.Failed -> Json.String "failed"
| VCS.NoResult | VCS.Checked | VCS.Computing _ -> `String "none"
| VCS.Valid -> `String "valid"
| VCS.Unknown -> `String "unknown"
| VCS.Timeout -> `String "timeout"
| VCS.Stepout -> `String "stepout"
| VCS.Invalid -> `String "invalid"
| VCS.Failed -> `String "failed"
let verdict_of_json = function
| Json.String "valid" -> VCS.Valid
| Json.String "unknown" -> VCS.Unknown
| Json.String "timeout" -> VCS.Timeout
| Json.String "stepout" -> VCS.Stepout
| Json.String "invalid" -> VCS.Invalid
| Json.String "failed" -> VCS.Failed
| `String "valid" -> VCS.Valid
| `String "unknown" -> VCS.Unknown
| `String "timeout" -> VCS.Timeout
| `String "stepout" -> VCS.Stepout
| `String "invalid" -> VCS.Invalid
| `String "failed" -> VCS.Failed
| _ -> VCS.NoResult
let json_of_result (p : VCS.prover) (r : VCS.result) =
let open VCS in
let name = "prover" , Json.String (VCS.name_of_prover p) in
let name = "prover" , `String (VCS.name_of_prover p) in
let verdict = "verdict" , json_of_verdict r.verdict in
let time = if r.prover_time > 0.0 then [ "time" , Json.Float r.prover_time ] else [] in
let steps = if r.prover_steps > 0 then [ "steps" , Json.Int r.prover_steps ] else [] in
let depth = if r.prover_depth > 0 then [ "depth" , Json.Int r.prover_depth ] else [] in
Json.Assoc (name :: verdict :: (time @ steps @ depth))
let time = if r.prover_time > 0.0 then [ "time" , `Float r.prover_time ] else [] in
let steps = if r.prover_steps > 0 then [ "steps" , `Int r.prover_steps ] else [] in
let depth = if r.prover_depth > 0 then [ "depth" , `Int r.prover_depth ] else [] in
`Assoc (name :: verdict :: (time @ steps @ depth))
let prover_of_json js =
try VCS.prover_of_name (js >? "prover" |> Json.string)
......@@ -389,8 +389,8 @@ let a_tactic tac children = Tactic(subgoals 0 children,tac,children)
(* -------------------------------------------------------------------------- *)
let rec decode = function
| Json.Null -> []
| Json.Array alts -> List.map alternative alts
| `Null -> []
| `List alts -> List.map alternative alts
| js -> [Error("Invalid Script",js)]
and subscript (key,js) = key , decode js
......@@ -404,7 +404,7 @@ and alternative js =
a_tactic tactic (List.map subscript children)
| None -> Error("Invalid Tactic",js)
let rec encode script = Json.Array (alternatives script)
let rec encode script = `List (alternatives script)
and subgoal (k,alt) = k , encode alt
......
src/plugins/wp/ProofSession.ml
+ 2
− 2
View file @ e7dade35
......@@ -40,13 +40,13 @@ let exists wpo =
let load wpo =
let f = filename wpo in
if Sys.file_exists f then Json.load_file f else Json.Null
if Sys.file_exists f then Json.load_file f else `Null
let save wpo js =
let f = filename wpo in
let empty =
match js with
| Json.Null | Json.Array [] | Json.Assoc [] -> true
| `Null | `List [] | `Assoc [] -> true
| _ -> false
in
( if empty
......
src/plugins/wp/wpReport.ml
+ 7
− 7
View file @ e7dade35
......@@ -133,21 +133,21 @@ let add_qedstat (ts:float) (s:stats) =
if ts > s.time then s.time <- ts
let get_field js fd =
try Json.field fd js with Not_found | Invalid_argument _ -> Json.Null
try Json.field fd js with Not_found | Invalid_argument _ -> `Null
let json_assoc fields =
let fields = List.filter (fun (_,d) -> d<>Json.Null) fields in
if fields = [] then Json.Null else Json.Assoc fields
let fields = List.filter (fun (_,d) -> d<>`Null) fields in
if fields = [] then `Null else `Assoc fields
let json_of_stats s =
let add fd v w = if v > 0 then (fd , Json.Int v)::w else w in
let add fd v w = if v > 0 then (fd , `Int v)::w else w in
json_assoc
begin
add "total" s.total @@
add "valid" s.valid @@
add "failed" s.inconclusive @@
add "unknown" s.unsuccess @@
(if s.rank >= 0 then [ "rank" , Json.Int s.rank ] else [])
(if s.rank >= 0 then [ "rank" , `Int s.rank ] else [])
end
let rankify_stats s js =
......@@ -870,11 +870,11 @@ let export_json gstat jfile =
let js =
try
if Sys.file_exists jfile
then Json.load_file jfile else Json.Null
then Json.load_file jfile else `Null
with Json.Error(file,line,msg) ->
let source = Log.source ~file ~line in
Wp_parameters.error ~source "Incorrect json file: %s" msg ;
Json.Null
`Null
in
rankify_fcstat gstat js ;
Json.save_file jfile (json_of_fcstat gstat) ;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment