summaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ExtrHaskellBasic.v15
-rw-r--r--plugins/extraction/ExtrOcamlNatInt.v1
-rw-r--r--plugins/extraction/common.ml3
-rw-r--r--plugins/extraction/extract_env.ml6
-rw-r--r--plugins/extraction/extraction_plugin.mllib1
-rw-r--r--plugins/extraction/g_extraction.ml42
-rw-r--r--plugins/extraction/haskell.ml36
-rw-r--r--plugins/extraction/json.ml278
-rw-r--r--plugins/extraction/json.mli1
-rw-r--r--plugins/extraction/miniml.mli1
-rw-r--r--plugins/extraction/ocaml.ml15
-rw-r--r--plugins/extraction/scheme.ml3
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--plugins/extraction/table.mli2
-rw-r--r--plugins/extraction/vo.itarget1
15 files changed, 350 insertions, 17 deletions
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
new file mode 100644
index 00000000..294d6102
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellBasic.v
@@ -0,0 +1,15 @@
+(** Extraction to Haskell : use of basic Haskell types *)
+
+Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive unit => "()" [ "()" ].
+Extract Inductive list => "([])" [ "([])" "(:)" ].
+Extract Inductive prod => "(,)" [ "(,)" ].
+
+Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
+Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
+Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
+
+Extract Inlined Constant andb => "(Prelude.&&)".
+Extract Inlined Constant orb => "(Prelude.||)".
+Extract Inlined Constant negb => "Prelude.not".
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 5f653ee1..a0930f15 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -59,6 +59,7 @@ Extract Constant Compare_dec.nat_compare =>
"fun n m -> if n=m then Eq else if n<m then Lt else Gt".
Extract Inlined Constant Compare_dec.leb => "(<=)".
Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
+Extract Inlined Constant Compare_dec.lt_dec => "(<)".
Extract Constant Compare_dec.lt_eq_lt_dec =>
"fun n m -> if n>m then None else Some (n<m)".
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 21819aa8..97f85694 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 -> dottify (List.map unquote rls)
| Haskell -> if modular () then pp_haskell_gen k mp rls else s
| Ocaml -> pp_ocaml_gen k mp rls (Some l)
@@ -628,7 +629,7 @@ let check_extract_ascii () =
try
let char_type = match lang () with
| Ocaml -> "char"
- | Haskell -> "Char"
+ | Haskell -> "Prelude.Char"
| _ -> raise Not_found
in
String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 42e69d34..0f846013 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -235,7 +235,7 @@ let rec extract_structure_spec env mp = function
and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
| MEident mp -> Visit.add_mp_all mp; MTident mp
- | MEwith(me',WithDef(idl,c))->
+ | MEwith(me',WithDef(idl,(c,ctx)))->
let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
let mt = extract_mexpr_spec env mp1 (me_struct,me') in
(match extract_with_type env' c with (* cb may contain some kn *)
@@ -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. *)
@@ -440,7 +441,8 @@ let mono_filename f =
let module_filename mp =
let f = file_of_modfile mp in
let d = descr () in
- Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
+ let p = d.file_naming mp ^ d.file_suffix in
+ Some p, Option.map ((^) f) d.sig_suffix, Id.of_string f
(*s Extraction of one decl to stdout. *)
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib
index b7f45861..ad321243 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 3caa558f..3fe5a8c0 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/haskell.ml b/plugins/extraction/haskell.ml
index 5e08fef5..37b41420 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -26,7 +26,7 @@ let pr_upper_id id = str (String.capitalize (Id.to_string id))
let keywords =
List.fold_right (fun s -> Id.Set.add (Id.of_string s))
- [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
+ [ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
"if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
"let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
"as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
@@ -38,7 +38,7 @@ let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
let preamble mod_name comment used_modules usf =
let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
in
- (if not usf.magic then mt ()
+ (if not (usf.magic || usf.tunknown) then mt ()
else
str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
@@ -52,19 +52,36 @@ let preamble mod_name comment used_modules usf =
str "import qualified Prelude" ++ fnl () ++
prlist pp_import used_modules ++ fnl () ++
(if List.is_empty used_modules then mt () else fnl ()) ++
- (if not usf.magic then mt ()
+ (if not (usf.magic || usf.tunknown) then mt ()
else str "\
\n#ifdef __GLASGOW_HASKELL__\
\nimport qualified GHC.Base\
+\nimport qualified GHC.Prim\
+\n#else\
+\n-- HUGS\
+\nimport qualified IOExts\
+\n#endif" ++ fnl2 ())
+ ++
+ (if not usf.magic then mt ()
+ else str "\
+\n#ifdef __GLASGOW_HASKELL__\
\nunsafeCoerce :: a -> b\
\nunsafeCoerce = GHC.Base.unsafeCoerce#\
\n#else\
\n-- HUGS\
-\nimport qualified IOExts\
\nunsafeCoerce :: a -> b\
\nunsafeCoerce = IOExts.unsafeCoerce\
\n#endif" ++ fnl2 ())
++
+ (if not usf.tunknown then mt ()
+ else str "\
+\n#ifdef __GLASGOW_HASKELL__\
+\ntype Any = GHC.Prim.Any\
+\n#else\
+\n-- HUGS\
+\ntype Any = ()\
+\n#endif" ++ fnl2 ())
+ ++
(if not usf.mldummy then mt ()
else str "__ :: any" ++ fnl () ++
str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
@@ -102,7 +119,7 @@ let rec pp_type par vl t =
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
| Tdummy _ -> str "()"
- | Tunknown -> str "()"
+ | Tunknown -> str "Any"
| Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
in
hov 0 (pp_rec par t)
@@ -243,12 +260,12 @@ let pp_logical_ind packet =
prvect_with_sep spc pr_id packet.ip_consnames)
let pp_singleton kn packet =
+ let name = pp_global Type (IndRef (kn,0)) in
let l = rename_tvars keywords packet.ip_vars in
- let l' = List.rev l in
- hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
+ hov 2 (str "type " ++ name ++ spc () ++
prlist_with_sep spc pr_id l ++
(if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
- pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
+ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
pp_comment (str "singleton inductive, whose constructor was " ++
pr_id packet.ip_consnames.(0)))
@@ -346,7 +363,7 @@ and pp_module_expr = function
| MEfunctor _ -> mt ()
(* for the moment we simply discard unapplied functors *)
| MEident _ | MEapply _ -> assert false
- (* should be expansed in extract_env *)
+ (* should be expanded in extract_env *)
let pp_struct =
let pp_sel (mp,sel) =
@@ -360,6 +377,7 @@ let pp_struct =
let haskell_descr = {
keywords = keywords;
file_suffix = ".hs";
+ file_naming = string_of_modfile;
preamble = preamble;
pp_struct = pp_struct;
sig_suffix = None;
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
new file mode 100644
index 00000000..125dc86b
--- /dev/null
+++ b/plugins/extraction/json.ml
@@ -0,0 +1,278 @@
+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) -> 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);
+ ("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 00000000..3ba240a1
--- /dev/null
+++ b/plugins/extraction/json.mli
@@ -0,0 +1 @@
+val json_descr : Miniml.language_descr
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 1e491d36..b7dee6cb 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -197,6 +197,7 @@ type language_descr = {
(* Concerning the source file *)
file_suffix : string;
+ file_naming : module_path -> string;
(* the second argument is a comment to add to the preamble *)
preamble :
Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 30ac3d3f..8c482b4b 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,7 +634,12 @@ and pp_module_type params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (mp, sign) ->
push_visible mp params;
- let l = List.map pp_specif sign in
+ let try_pp_specif l x =
+ try pp_specif x :: l with Failure "empty phrase" -> l
+ in
+ (* We cannot use fold_right here due to side effects in pp_specif *)
+ let l = List.fold_left try_pp_specif [] sign in
+ let l = List.rev l in
pop_visible ();
str "sig " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +712,12 @@ and pp_module_expr params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEstruct (mp, sel) ->
push_visible mp params;
- let l = List.map pp_structure_elem sel in
+ let try_pp_structure_elem l x =
+ try pp_structure_elem x :: l with Failure "empty phrase" -> l
+ in
+ (* We cannot use fold_right here due to side effects in pp_structure_elem *)
+ let l = List.fold_left try_pp_structure_elem [] sel in
+ let l = List.rev l in
pop_visible ();
str "struct " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -736,6 +746,7 @@ let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
let ocaml_descr = {
keywords = keywords;
file_suffix = ".ml";
+ file_naming = file_of_modfile;
preamble = preamble;
pp_struct = pp_struct;
sig_suffix = Some ".mli";
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 69dea25a..cc8b6d8e 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -212,7 +212,7 @@ and pp_module_expr = function
| MEfunctor _ -> mt ()
(* for the moment we simply discard unapplied functors *)
| MEident _ | MEapply _ -> assert false
- (* should be expansed in extract_env *)
+ (* should be expanded in extract_env *)
let pp_struct =
let pp_sel (mp,sel) =
@@ -225,6 +225,7 @@ let pp_struct =
let scheme_descr = {
keywords = keywords;
file_suffix = ".scm";
+ file_naming = file_of_modfile;
preamble = preamble;
pp_struct = pp_struct;
sig_suffix = None;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 44d760cc..a57c39ee 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 1acbe355..648f2321 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 ?
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 1fe09f6f..f0489048 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,3 +1,4 @@
+ExtrHaskellBasic.vo
ExtrOcamlBasic.vo
ExtrOcamlIntConv.vo
ExtrOcamlBigIntConv.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 05:03:05 +0000