diff --git a/proofs/psnj_toolbox/bin/dune b/proofs/psnj_toolbox/bin/dune
index d1bcdc12be50c1dd3e076c2f6323124298167132..b401347dc45bb6899da03ae4d7d4fbe6fffe8d26 100644
--- a/proofs/psnj_toolbox/bin/dune
+++ b/proofs/psnj_toolbox/bin/dune
@@ -1,7 +1,7 @@
(executable
(public_name psnj)
(name main)
- (modules main dopth chainprops appaxiom autosolve qfo split)
+ (modules main dopth chainprops appaxiom autosolve qfo split group)
(libraries
ezjsonm
personoj
diff --git a/proofs/psnj_toolbox/bin/group.ml b/proofs/psnj_toolbox/bin/group.ml
new file mode 100644
index 0000000000000000000000000000000000000000..693d11fad4cf8e0df60fbe5f0e996d307fb4f0c2
--- /dev/null
+++ b/proofs/psnj_toolbox/bin/group.ml
@@ -0,0 +1,74 @@
+module StrMap = Map.Make (String)
+
+let add (k : string) (o : Ezjsonm.value) (m : Ezjsonm.value list StrMap.t) :
+ Ezjsonm.value list StrMap.t =
+ let objs =
+ match StrMap.find_opt k m with None -> [ o ] | Some objs -> o :: objs
+ in
+ StrMap.add k objs m
+
+let group minify group_by =
+ let groups = ref StrMap.empty in
+ (try
+ while true do
+ let line = input_line stdin in
+ let json : Ezjsonm.value = Ezjsonm.from_string line in
+ let name = Ezjsonm.(find json [ group_by ] |> get_string) in
+ groups := add name json !groups
+ done
+ with End_of_file -> ());
+ let m =
+ StrMap.map List.rev !groups
+ |> StrMap.map (Ezjsonm.list Fun.id)
+ |> StrMap.map Ezjsonm.value
+ in
+ let obj = StrMap.to_seq m |> List.of_seq |> Ezjsonm.dict in
+ Ezjsonm.to_channel ~minify stdout obj
+
+open Cmdliner
+
+let minify = Arg.(value & flag & info [ "m" ])
+
+let group_by =
+ let doc = "Group objects using field $(docv)" in
+ Arg.(value & opt string "name" & info [ "group-by"; "g" ] ~doc ~docv:"FIELD")
+
+let cmd =
+ let doc = "Group JSON objects in arrays depending on a field" in
+ let man =
+ [
+ `S Manpage.s_description;
+ `P
+ "$(tname) is a filter that reads a list of JSON objects and group them \
+ in a dictionary. Groups are determined by the value of a name (which \
+ is-confusingly-$(b,name) by default). The values associated to this \
+ name become the keys of the dictionary.";
+ `S Manpage.s_examples;
+ `P "Given JSON objects";
+ `Pre
+ {|{ "name": "foo", "attr": "baz" }
+{ "name": "bar", "attr": "frobz" }
+{ "name": "foo", "attr": "nitz" }|};
+ `P "The output of $(tname) -g name is";
+ `Pre
+ {|{
+ "bar": [
+ {
+ "name": "bar",
+ "attr": "frobz"
+ }
+ ],
+ "foo": [
+ {
+ "name": "foo",
+ "attr": "nitz"
+ },
+ {
+ "name": "foo",
+ "attr": "baz"
+ }
+ ]
+ }|};
+ ]
+ in
+ (Term.(const group $ minify $ group_by), Term.info "jgroup" ~doc ~man)
diff --git a/proofs/psnj_toolbox/bin/main.ml b/proofs/psnj_toolbox/bin/main.ml
index ee41eb416d726a7715161be13215d3dc4f92bdaa..53599e307b7f26b6d2b0a2d0cf821c813d335a1a 100644
--- a/proofs/psnj_toolbox/bin/main.ml
+++ b/proofs/psnj_toolbox/bin/main.ml
@@ -6,6 +6,14 @@ let default_cmd =
(Term.(ret @@ const @@ `Help (`Pager, None)), Term.info "psnj" ~doc ~exits)
let cmds =
- [ Dopth.cmd; Chainprops.cmd; Appaxiom.cmd; Autosolve.cmd; Qfo.cmd; Split.cmd ]
+ [
+ Dopth.cmd;
+ Chainprops.cmd;
+ Appaxiom.cmd;
+ Autosolve.cmd;
+ Qfo.cmd;
+ Split.cmd;
+ Group.cmd;
+ ]
let () = Term.(exit @@ eval_choice default_cmd cmds)
diff --git a/proofs/psnj_toolbox/bin/split.ml b/proofs/psnj_toolbox/bin/split.ml
index 7db3920341f2870cb4385dc924cff10438f08d49..9f46eccfee446591be9201abd25a2c01feb158eb 100644
--- a/proofs/psnj_toolbox/bin/split.ml
+++ b/proofs/psnj_toolbox/bin/split.ml
@@ -1,16 +1,19 @@
let split prefix =
+ let fnames = ref [] in
try
while true do
let line = input_line stdin in
let json = Ezjsonm.from_string line in
let name = Ezjsonm.(find json [ "name" ] |> get_string) in
- let fname = String.concat "_" [ prefix; name ] in
+ let fname = String.concat "_" [ prefix; name ] ^ ".json" in
+ fnames := fname :: !fnames;
let oc = open_out fname in
at_exit (fun () -> close_out oc);
output_string oc line;
output_char oc '\n'
done
- with End_of_file -> ()
+ with End_of_file ->
+ List.(iter (Format.printf "%s@\n") (sort_uniq String.compare !fnames))
open Cmdliner
@@ -28,7 +31,8 @@ let cmd =
"$(tname) reads a newline-seprated list of json objects on its \
standard input and copies each object to a file $(i,pr)_$(i,n).json \
where $(i,n) is the value associated to the (json) name $(b,name) and \
- $(i,pr) is a chosen prefix.";
+ $(i,pr) is a chosen prefix. The list of created files is returned on \
+ standard output. Files appear at most once in the list.";
`S Manpage.s_examples;
`P "Faced with input";
`Pre
diff --git a/proofs/psnj_toolbox/test/jgroup/dune b/proofs/psnj_toolbox/test/jgroup/dune
new file mode 100644
index 0000000000000000000000000000000000000000..2284a0ba048942afd4ee986189dedf28cacb836e
--- /dev/null
+++ b/proofs/psnj_toolbox/test/jgroup/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps input.json))
diff --git a/proofs/psnj_toolbox/test/jgroup/input.json b/proofs/psnj_toolbox/test/jgroup/input.json
new file mode 100644
index 0000000000000000000000000000000000000000..874e472de3108e4eb0aeeccf5245fe8bffa5d2dd
--- /dev/null
+++ b/proofs/psnj_toolbox/test/jgroup/input.json
@@ -0,0 +1,3 @@
+{ "name": "foo", "attr": "baz" }
+{ "name": "bar", "attr": "frobz" }
+{ "name": "foo", "attr": "nitz" }
diff --git a/proofs/psnj_toolbox/test/jgroup/jgroup.t b/proofs/psnj_toolbox/test/jgroup/jgroup.t
new file mode 100644
index 0000000000000000000000000000000000000000..b8dea681cccde354ba2ffedc9ae15e2af0eceddc
--- /dev/null
+++ b/proofs/psnj_toolbox/test/jgroup/jgroup.t
@@ -0,0 +1,19 @@
+ $ psnj jgroup < input.json
+ {
+ "bar": [
+ {
+ "name": "bar",
+ "attr": "frobz"
+ }
+ ],
+ "foo": [
+ {
+ "name": "foo",
+ "attr": "baz"
+ },
+ {
+ "name": "foo",
+ "attr": "nitz"
+ }
+ ]
+ }
diff --git a/proofs/psnj_toolbox/test/jsplit/jsplit.t b/proofs/psnj_toolbox/test/jsplit/jsplit.t
index 4650034f6ea1df594968744d1cc390df641bf566..c1d20b0fe20fe33597b6632ba62752aef1adca9d 100644
--- a/proofs/psnj_toolbox/test/jsplit/jsplit.t
+++ b/proofs/psnj_toolbox/test/jsplit/jsplit.t
@@ -1,7 +1,11 @@
- $ psnj jsplit -p ff < input.json; find . -type f -printf "\n%p\n" -exec cat {} \;
+ $ psnj jsplit -p ff < input.json
+ ff_bar.json
+ ff_foo.json
+
+ $ find . -type f -printf "\n%p\n" -exec cat {} \;
- ./ff_bar
- { "name": "bar", "attr": "frobz" }
-
- ./ff_foo
+ ./ff_foo.json
{ "name": "foo", "attr": "baz" }
+
+ ./ff_bar.json
+ { "name": "bar", "attr": "frobz" }