diff options
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/ExtrHaskellBasic.v | 15 | ||||
-rw-r--r-- | plugins/extraction/ExtrOcamlNatInt.v | 1 | ||||
-rw-r--r-- | plugins/extraction/common.ml | 3 | ||||
-rw-r--r-- | plugins/extraction/extract_env.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/extraction_plugin.mllib | 1 | ||||
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 2 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 36 | ||||
-rw-r--r-- | plugins/extraction/json.ml | 278 | ||||
-rw-r--r-- | plugins/extraction/json.mli | 1 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 1 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 15 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 3 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 2 | ||||
-rw-r--r-- | plugins/extraction/vo.itarget | 1 |
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 |