diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-04-05 12:26:57 -0400 |
|---|---|---|
| committer |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 12:09:03 +0200 |
| commit | 1688d4af1896effb42fa5dd191948795c59288a4 (patch) | |
| tree | da13a8bd88b01c35a45be17fd1590dd9ea412329 /plugins/extraction | |
| parent | fb8c4b8903e82b36ebcf28dfe18282fb05a93d4f (diff) | |
JSON extraction: make explicit each group of mutually-recursive fixpoints
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/json.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index f19fba6f1..125dc86b8 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -221,13 +221,16 @@ let pp_decl = function ("argnames", json_list (List.map json_id l)); ("value", json_type l t) ] - | Dfix (rv, defs, typs) -> prvecti_with_sep pr_comma (fun i r -> - json_dict [ - ("what", json_str "decl:fix"); - ("name", json_global Term rv.(i)); - ("type", json_type [] typs.(i)); - ("value", json_function (empty_env ()) defs.(i)) - ]) rv + | Dfix (rv, defs, typs) -> json_dict [ + ("what", json_str "decl:fixgroup"); + ("fixlist", json_listarr (Array.mapi (fun i r -> + json_dict [ + ("what", json_str "fixgroup:item"); + ("name", json_global Term rv.(i)); + ("type", json_type [] typs.(i)); + ("value", json_function (empty_env ()) defs.(i)) + ]) rv)) + ] | Dterm (r, a, t) -> json_dict [ ("what", json_str "decl:term"); ("name", json_global Term r); |