aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.lang2
-rw-r--r--plugins/extraction/common.ml1
-rw-r--r--plugins/extraction/extract_env.ml1
-rw-r--r--plugins/extraction/extraction_plugin.mllib1
-rw-r--r--plugins/extraction/g_extraction.ml42
-rw-r--r--plugins/extraction/json.ml275
-rw-r--r--plugins/extraction/json.mli1
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--plugins/extraction/table.mli2
9 files changed, 284 insertions, 3 deletions
diff --git a/ide/coq.lang b/ide/coq.lang
index 38dabda50..65150d6a9 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -164,7 +164,7 @@
<keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
<keyword>\%{locality}Infix</keyword>
<keyword>Declare\%{space}ML\%{space}Module</keyword>
- <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme)</keyword>
+ <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
</context>
<context id="hint-command" style-ref="vernac-keyword">
<prefix>\%{locality}Hint\%{space}</prefix>
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0748af1ea..094d91d20 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -600,6 +600,7 @@ let pp_global k r =
let rls = List.rev ls in (* for what come next it's easier this way *)
match lang () with
| Scheme -> unquote s (* no modular Scheme extraction... *)
+ | JSON -> unquote s (* no modular JSON extraction... *)
| Haskell -> if modular () then pp_haskell_gen k mp rls else s
| Ocaml -> pp_ocaml_gen k mp rls (Some l)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5ea4fb763..0f846013b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -410,6 +410,7 @@ let descr () = match lang () with
| Ocaml -> Ocaml.ocaml_descr
| Haskell -> Haskell.haskell_descr
| Scheme -> Scheme.scheme_descr
+ | JSON -> Json.json_descr
(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
Works similarly for the other languages. *)
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib
index b7f458611..ad3212434 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mllib
@@ -6,6 +6,7 @@ Common
Ocaml
Haskell
Scheme
+Json
Extract_env
G_extraction
Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 3caa558f9..3fe5a8c04 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -41,12 +41,14 @@ let pr_language = function
| Ocaml -> str "Ocaml"
| Haskell -> str "Haskell"
| Scheme -> str "Scheme"
+ | JSON -> str "JSON"
VERNAC ARGUMENT EXTEND language
PRINTED BY pr_language
| [ "Ocaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
+| [ "JSON" ] -> [ JSON ]
END
(* Extraction commands *)
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
new file mode 100644
index 000000000..f19fba6f1
--- /dev/null
+++ b/plugins/extraction/json.ml
@@ -0,0 +1,275 @@
+open Pp
+open Errors
+open Util
+open Names
+open Nameops
+open Globnames
+open Table
+open Miniml
+open Mlutil
+open Common
+
+let json_str s =
+ qs s
+
+let json_int i =
+ int i
+
+let json_bool b =
+ if b then str "true" else str "false"
+
+let json_null =
+ str "null"
+
+let json_global typ ref =
+ json_str (Common.pp_global typ ref)
+
+let json_id id =
+ json_str (Id.to_string id)
+
+let json_dict_one (k, v) =
+ json_str k ++ str (": ") ++ v
+
+let json_dict_open l =
+ str ("{") ++ fnl () ++
+ str (" ") ++ hov 0 (prlist_with_sep pr_comma json_dict_one l)
+
+let json_dict l =
+ json_dict_open l ++ fnl () ++
+ str ("}")
+
+let json_list l =
+ str ("[") ++ fnl () ++
+ str (" ") ++ hov 0 (prlist_with_sep pr_comma (fun x -> x) l) ++ fnl () ++
+ str ("]")
+
+let json_listarr a =
+ str ("[") ++ fnl () ++
+ str (" ") ++ hov 0 (prvect_with_sep pr_comma (fun x -> x) a) ++ fnl () ++
+ str ("]")
+
+
+let preamble mod_name comment used_modules usf =
+ (match comment with
+ | None -> mt ()
+ | Some s -> str "/* " ++ hov 0 s ++ str " */" ++ fnl ()) ++
+ json_dict_open [
+ ("what", json_str "module");
+ ("name", json_id mod_name);
+ ("need_magic", json_bool (usf.magic));
+ ("need_dummy", json_bool (usf.mldummy));
+ ("used_modules", json_list
+ (List.map (fun mf -> json_str (file_of_modfile mf)) used_modules))
+ ]
+
+
+(*s Pretty-printing of types. *)
+
+let rec json_type vl = function
+ | Tmeta _ | Tvar' _ -> assert false
+ | Tvar i -> (try
+ let varid = List.nth vl (pred i) in json_dict [
+ ("what", json_str "type:var");
+ ("name", json_id varid)
+ ]
+ with Failure _ -> json_dict [
+ ("what", json_str "type:varidx");
+ ("name", json_int i)
+ ])
+ | Tglob (r, l) -> json_dict [
+ ("what", json_str "type:glob");
+ ("name", json_global Type r);
+ ("args", json_list (List.map (json_type vl) l))
+ ]
+ | Tarr (t1,t2) -> json_dict [
+ ("what", json_str "type:arrow");
+ ("left", json_type vl t1);
+ ("right", json_type vl t2)
+ ]
+ | Tdummy _ -> json_dict [("what", json_str "type:dummy")]
+ | Tunknown -> json_dict [("what", json_str "type:unknown")]
+ | Taxiom -> json_dict [("what", json_str "type:axiom")]
+
+
+(*s Pretty-printing of expressions. *)
+
+let rec json_expr env = function
+ | MLrel n -> json_dict [
+ ("what", json_str "expr:rel");
+ ("name", json_id (get_db_name n env))
+ ]
+ | MLapp (f, args) -> json_dict [
+ ("what", json_str "expr:apply");
+ ("func", json_expr env f);
+ ("args", json_list (List.map (json_expr env) args))
+ ]
+ | MLlam _ as a ->
+ let fl, a' = collect_lams a in
+ let fl, env' = push_vars (List.map id_of_mlid fl) env in
+ json_dict [
+ ("what", json_str "expr:lambda");
+ ("argnames", json_list (List.map json_id (List.rev fl)));
+ ("body", json_expr env' a')
+ ]
+ | MLletin (id, a1, a2) ->
+ let i, env' = push_vars [id_of_mlid id] env in
+ json_dict [
+ ("what", json_str "expr:let");
+ ("name", json_id (List.hd i));
+ ("nameval", json_expr env a1);
+ ("body", json_expr env' a2)
+ ]
+ | MLglob r -> json_dict [
+ ("what", json_str "expr:global");
+ ("name", json_global Term r)
+ ]
+ | MLcons (_, r, a) -> json_dict [
+ ("what", json_str "expr:constructor");
+ ("name", json_global Cons r);
+ ("args", json_list (List.map (json_expr env) a))
+ ]
+ | MLtuple l -> json_dict [
+ ("what", json_str "expr:tuple");
+ ("items", json_list (List.map (json_expr env) l))
+ ]
+ | MLcase (typ, t, pv) -> json_dict [
+ ("what", json_str "expr:case");
+ ("expr", json_expr env t);
+ ("cases", json_listarr (Array.map (fun x -> json_one_pat env x) pv))
+ ]
+ | MLfix (i, ids, defs) ->
+ let ids', env' = push_vars (List.rev (Array.to_list ids)) env in
+ let ids' = Array.of_list (List.rev ids') in
+ json_dict [
+ ("what", json_str "expr:fix");
+ ("funcs", json_listarr (Array.map (fun (fi, ti) ->
+ json_dict [
+ ("what", json_str "fix:item");
+ ("name", json_id fi);
+ ("body", json_function env' ti)
+ ]) (Array.map2 (fun a b -> a,b) ids' defs)))
+ ]
+ | MLexn s -> json_dict [
+ ("what", json_str "expr:exception");
+ ("msg", json_str s)
+ ]
+ | MLdummy -> json_dict [("what", json_str "expr:dummy")]
+ | MLmagic a -> json_dict [
+ ("what", json_str "expr:coerce");
+ ("value", json_expr env a)
+ ]
+ | MLaxiom -> json_dict [("what", json_str "expr:axiom")]
+
+and json_one_pat env (ids,p,t) =
+ let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
+ ("what", json_str "case");
+ ("pat", json_gen_pat (List.rev ids') env' p);
+ ("body", json_expr env' t)
+ ]
+
+and json_gen_pat ids env = function
+ | Pcons (r, l) -> json_cons_pat r (List.map (json_gen_pat ids env) l)
+ | Pusual r -> json_cons_pat r (List.map json_id ids)
+ | Ptuple l -> json_dict [
+ ("what", json_str "pat:tuple");
+ ("items", json_list (List.map (json_gen_pat ids env) l))
+ ]
+ | Pwild -> json_dict [("what", json_str "pat:wild")]
+ | Prel n -> json_dict [
+ ("what", json_str "pat:rel");
+ ("name", json_id (get_db_name n env))
+ ]
+
+and json_cons_pat r ppl = json_dict [
+ ("what", json_str "pat:constructor");
+ ("name", json_global Cons r);
+ ("argnames", json_list ppl)
+ ]
+
+and json_function env t =
+ let bl, t' = collect_lams t in
+ let bl, env' = push_vars (List.map id_of_mlid bl) env in
+ json_dict [
+ ("what", json_str "expr:lambda");
+ ("argnames", json_list (List.map json_id (List.rev bl)));
+ ("body", json_expr env' t')
+ ]
+
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let json_ind ip pl cv = json_dict [
+ ("what", json_str "decl:ind");
+ ("name", json_global Type (IndRef ip));
+ ("argnames", json_list (List.map json_id pl));
+ ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [
+ ("name", json_global Cons (ConstructRef (ip, idx+1)));
+ ("argtypes", json_list (List.map (json_type pl) c))
+ ]) cv))
+ ]
+
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl = function
+ | Dind (kn, defs) -> prvecti_with_sep pr_comma
+ (fun i p -> if p.ip_logical then str ""
+ else json_ind (kn, i) p.ip_vars p.ip_types) defs.ind_packets
+ | Dtype (r, l, t) -> json_dict [
+ ("what", json_str "decl:type");
+ ("name", json_global Type r);
+ ("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
+ | Dterm (r, a, t) -> json_dict [
+ ("what", json_str "decl:term");
+ ("name", json_global Term r);
+ ("type", json_type [] t);
+ ("value", json_function (empty_env ()) a)
+ ]
+
+let rec pp_structure_elem = function
+ | (l,SEdecl d) -> [ pp_decl d ]
+ | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr
+ | (l,SEmodtype m) -> []
+ (* for the moment we simply discard module type *)
+
+and pp_module_expr = function
+ | MEstruct (mp,sel) -> List.concat (List.map pp_structure_elem sel)
+ | MEfunctor _ -> []
+ (* for the moment we simply discard unapplied functors *)
+ | MEident _ | MEapply _ -> assert false
+ (* should be expansed in extract_env *)
+
+let pp_struct mls =
+ let pp_sel (mp,sel) =
+ push_visible mp [];
+ let p = prlist_with_sep pr_comma identity
+ (List.concat (List.map pp_structure_elem sel)) in
+ pop_visible (); p
+ in
+ str "," ++ fnl () ++
+ str " " ++ qs "declarations" ++ str ": [" ++ fnl () ++
+ str " " ++ hov 0 (prlist_with_sep pr_comma pp_sel mls) ++ fnl () ++
+ str " ]" ++ fnl () ++
+ str "}" ++ fnl ()
+
+
+let json_descr = {
+ keywords = Id.Set.empty;
+ file_suffix = ".json";
+ file_naming = file_of_modfile;
+ preamble = preamble;
+ pp_struct = pp_struct;
+ sig_suffix = None;
+ sig_preamble = (fun _ _ _ _ -> mt ());
+ pp_sig = (fun _ -> mt ());
+ pp_decl = pp_decl;
+}
diff --git a/plugins/extraction/json.mli b/plugins/extraction/json.mli
new file mode 100644
index 000000000..3ba240a1d
--- /dev/null
+++ b/plugins/extraction/json.mli
@@ -0,0 +1 @@
+val json_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 44d760ccd..a57c39eef 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -554,7 +554,7 @@ let _ = declare_string_option
(*s Extraction Lang *)
-type lang = Ocaml | Haskell | Scheme
+type lang = Ocaml | Haskell | Scheme | JSON
let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 1acbe3555..648f23211 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -142,7 +142,7 @@ val file_comment : unit -> string
(*s Target language. *)
-type lang = Ocaml | Haskell | Scheme
+type lang = Ocaml | Haskell | Scheme | JSON
val lang : unit -> lang
(*s Extraction modes: modular or monolithic, library or minimal ?
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 19:37:16 +0000