diff --git a/.Makefile.lint b/.Makefile.lint index 61f5274d3a2ed6cdbdca5c321d880466d842a100..f213229e55714480b8766486a7538600f510672a 100644 --- a/.Makefile.lint +++ b/.Makefile.lint @@ -215,7 +215,6 @@ ML_LINT_KO+=src/libraries/utils/hptset.ml ML_LINT_KO+=src/libraries/utils/hptset.mli ML_LINT_KO+=src/libraries/utils/indexer.ml ML_LINT_KO+=src/libraries/utils/indexer.mli -ML_LINT_KO+=src/libraries/utils/json.mli ML_LINT_KO+=src/libraries/utils/leftistheap.mli ML_LINT_KO+=src/libraries/utils/pretty_utils.ml ML_LINT_KO+=src/libraries/utils/pretty_utils.mli diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli index 82027243df20fa6471ef0272ba18fdf9c7c86911..8057272785205973440efcdd6826a79555f93c87 100644 --- a/src/libraries/utils/json.mli +++ b/src/libraries/utils/json.mli @@ -20,27 +20,30 @@ (* *) (**************************************************************************) -(** Json Library +(** Json Library Remarks: - - UTF-8 escaping is not supported; - - Parsers are less {i strict} than Json format; - - Printers are supposed to {i strictly} conforms to Json format; - - [Number] can be used to encode non OCaml-primitive numbers, + - UTF-8 escaping is not supported; + - Parsers are less {i strict} than Json format; + - Printers are supposed to {i strictly} conforms to Json format; + - [Number] can be used to encode non OCaml-primitive numbers, 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 diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll index 3a18621bf642a982d41c2a7f65d4c4bb0a9806d5..214c8c83f5e24c6dbd917139b0f20e57c1be65a9 100644 --- a/src/libraries/utils/json.mll +++ b/src/libraries/utils/json.mll @@ -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 } diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml index d7844aa7a51d29087ca33fe2802617c21bf7de2e..933fb6b55a6b20f08b9e4cadb8c159ec2a997a67 100644 --- a/src/plugins/report/classify.ml +++ b/src/plugins/report/classify.ml @@ -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 ; diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml index d3d6b9c26f6aed8e5e2dfe5edecdf31f8f48c988..1b2356ceb669a77ec93a9f72c425935db378f4fb 100644 --- a/src/plugins/wp/ProofScript.ml +++ b/src/plugins/wp/ProofScript.ml @@ -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 ; - "params" , t.params ; - "select" , t.select ; - "children" , Json.Assoc js ; - ]) + `Assoc [ + "header" , `String t.header ; + "tactic" , `String t.tactic ; + "params" , t.params ; + "select" , t.select ; + "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 diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml index 4806d19fff05fd0d5a4fd99b110d7a1eb054d5ec..384bcb40e669f8c22a046f6cdaf12fcd4d819f42 100644 --- a/src/plugins/wp/ProofSession.ml +++ b/src/plugins/wp/ProofSession.ml @@ -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 diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml index a53ad90325a31a4002910915182b9d32ea53c4de..411a15cc855375d1fc881b85724b4b70e2025300 100644 --- a/src/plugins/wp/wpReport.ml +++ b/src/plugins/wp/wpReport.ml @@ -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) ;