[serlib] [genarg] Fix Yojson serialization.

This is a quick fix, but should work for now.

CHANGES.md

@@ -10,6 +10,7 @@
             (@ejgallego)
  - [serlib] Large refactoring on Serlib, using functors, see serlib/README.md
             (@ejgallego)
+ - [serlib] Fix JSON serialization for generic arguments (@ejgallego, #321)
 
 ## Version 0.15.2:
 

serlib/plugins/ltac/ser_tacarg.ml

@@ -458,7 +458,7 @@ let register () =
   Ser_genarg.register_genser G_obligations.wit_withtac ser_wit_withtac;
 
   Ser_genarg.register_genser Extraargs.wit_by_arg_tac ser_wit_by_arg_tac;
-  (* XXX *)
+  (* XXX: seems gone from Coq *)
   (* Ser_genarg.register_genser Extraargs.wit_casted_constr ser_wit_casted_constr; *)
   Ser_genarg.register_genser Extraargs.wit_glob ser_wit_lglob;
   Ser_genarg.register_genser Extraargs.wit_hloc ser_wit_hloc;

serlib/ser_genarg.ml

@@ -286,8 +286,23 @@ let generic_argument_of_sexp _lvl sexp : 'a Genarg.generic_argument =
   let (RG ga) = gen_abstype_of_sexp sexp in
   Obj.magic ga
 
-let generic_argument_of_yojson _lvl _json = Error "not supported generic_argument_of_yojson"
-let generic_argument_to_yojson _lvl _g = `String "foo"
+let rec yojson_to_sexp json = match json with
+  | `String s -> Sexp.Atom s
+  | `List s -> Sexp.List (List.map yojson_to_sexp s)
+  | _ -> raise (Failure "ser_genarg: yojson_to_sexp")
+
+let rec sexp_to_yojson sexp : Yojson.Safe.t =
+  match sexp with
+  | Sexp.Atom s -> `String s
+  | List l -> `List (List.map sexp_to_yojson l)
+
+let generic_argument_of_yojson lvl json =
+  let sexp = yojson_to_sexp json in
+  Result.Ok (generic_argument_of_sexp lvl sexp)
+
+let generic_argument_to_yojson : type a. (a -> Yojson.Safe.t) -> a generic_argument -> Yojson.Safe.t =
+  fun _level_tag g ->
+  sexp_of_generic_argument (fun _ -> Atom "") g |> sexp_to_yojson
 
 type 'a generic_argument = 'a Genarg.generic_argument