aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml1
-rw-r--r--plugins/extraction/common.mli1
-rw-r--r--plugins/extraction/extract_env.ml83
-rw-r--r--plugins/extraction/extract_env.mli5
-rw-r--r--plugins/extraction/extraction.ml1
-rw-r--r--plugins/extraction/extraction.mli1
-rw-r--r--plugins/extraction/g_extraction.ml47
-rw-r--r--plugins/extraction/haskell.ml1
-rw-r--r--plugins/extraction/json.ml1
-rw-r--r--plugins/extraction/miniml.mli1
-rw-r--r--plugins/extraction/mlutil.ml1
-rw-r--r--plugins/extraction/mlutil.mli1
-rw-r--r--plugins/extraction/modutil.ml10
-rw-r--r--plugins/extraction/modutil.mli2
-rw-r--r--plugins/extraction/ocaml.ml1
-rw-r--r--plugins/extraction/scheme.ml1
-rw-r--r--plugins/extraction/table.ml8
-rw-r--r--plugins/extraction/table.mli1
18 files changed, 83 insertions, 44 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 19ba31fbbd..9772ebd641 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Pp
open Util
open Names
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 28a7c4d457..d6342b59c6 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Globnames
open Miniml
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 79d602dbe8..39826d7442 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Miniml
open Term
open Declarations
@@ -176,26 +175,32 @@ let factor_fix env l cb msb =
(hack proposed by Elie)
*)
-let expand_mexpr env mp me =
+let expand_mexpr env mpo me =
let inl = Some (Flags.get_inline_level()) in
- Mod_typing.translate_mse env (Some mp) inl me
+ Mod_typing.translate_mse env mpo inl me
-(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
- To check with Elie. *)
-
-let rec mp_of_mexpr = function
- | MEident mp -> mp
- | MEwith (seb,_) -> mp_of_mexpr seb
- | _ -> assert false
+let expand_modtype env mp me =
+ let inl = Some (Flags.get_inline_level()) in
+ Mod_typing.translate_modtype env mp inl ([],me)
let no_delta = Mod_subst.empty_delta_resolver
-let env_for_mtb_with_def env mp me idl =
+let flatten_modtype env mp me_alg struc_opt =
+ match struc_opt with
+ | Some me -> me, no_delta
+ | None ->
+ let mtb = expand_modtype env mp me_alg in
+ mtb.mod_type, mtb.mod_delta
+
+(** Ad-hoc update of environment, inspired by [Mod_typing.check_with_aux_def].
+*)
+
+let env_for_mtb_with_def env mp me reso idl =
let struc = Modops.destr_nofunctor me in
let l = Label.of_id (List.hd idl) in
let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in
let before = fst (List.split_when spot struc) in
- Modops.add_structure mp before no_delta env
+ Modops.add_structure mp before reso env
let make_cst resolver mp l =
Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
@@ -235,20 +240,24 @@ let rec extract_structure_spec env mp reso = function
[extract_mexpression_spec] should come from a [mod_type_alg] field.
This way, any encountered [MEident] should be a true module type. *)
-and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
+and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
| MEident mp -> Visit.add_mp_all mp; MTident mp
| 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
+ let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in
+ let env' = env_for_mtb_with_def env mp1 me_struct delta idl in
+ let mt = extract_mexpr_spec env mp1 (None,me') in
(match extract_with_type env' c with (* cb may contain some kn *)
| None -> mt
- | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
+ | Some (vl,typ) ->
+ type_iter_references Visit.add_ref typ;
+ MTwith(mt,ML_With_type(idl,vl,typ)))
| MEwith(me',WithMod(idl,mp))->
Visit.add_mp_all mp;
- MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
+ MTwith(extract_mexpr_spec env mp1 (None,me'), ML_With_module(idl,mp))
| MEapply _ ->
(* No higher-order module type in OCaml : we use the expanded version *)
- extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
+ let me_struct,delta = flatten_modtype env mp1 me_alg me_struct_o in
+ extract_msignature_spec env mp1 delta me_struct
and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
| MoreFunctor (mbid, mtb, me_alg') ->
@@ -259,8 +268,8 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
let mp = MPbound mbid in
let env' = Modops.add_module_type mp mtb env in
MTfunsig (mbid, extract_mbody_spec env mp mtb,
- extract_mexpression_spec env' mp1 (me_struct',me_alg'))
- | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
+ extract_mexpression_spec env' mp1 (me_struct',me_alg'))
+ | NoFunctor m -> extract_mexpr_spec env mp1 (Some me_struct,m)
and extract_msignature_spec env mp1 reso = function
| NoFunctor struc ->
@@ -336,7 +345,7 @@ and extract_mexpr env mp = function
(* In Haskell/Scheme, we expand everything.
For now, we also extract everything, dead code will be removed later
(see [Modutil.optimize_struct]. *)
- let sign,_,delta,_ = expand_mexpr env mp me in
+ let sign,_,delta,_ = expand_mexpr env (Some mp) me in
extract_msignature env mp delta ~all:true sign
| MEident mp ->
if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
@@ -686,3 +695,35 @@ let structure_for_compute c =
let struc = optimize_struct (refs,[]) (mono_environment refs []) in
let flatstruc = List.map snd (List.flatten (List.map snd struc)) in
flatstruc, ast, mlt
+
+(* For the test-suite :
+ extraction to a temporary file + run ocamlc on it *)
+
+let compile f =
+ try
+ let args = ["ocamlc";"-I";Filename.dirname f;"-c";f^"i";f] in
+ let res = CUnix.sys_command (Envars.ocamlfind ()) args in
+ match res with
+ | Unix.WEXITED 0 -> ()
+ | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+ CErrors.user_err
+ Pp.(str "Compilation of file " ++ str f ++
+ str " failed with exit code " ++ int n)
+ with Unix.Unix_error (e,_,_) ->
+ CErrors.user_err
+ Pp.(str "Compilation of file " ++ str f ++
+ str " failed with error " ++ str (Unix.error_message e))
+
+let remove f =
+ if Sys.file_exists f then Sys.remove f
+
+let extract_and_compile l =
+ if lang () != Ocaml then
+ CErrors.user_err (Pp.str "This command only works with OCaml extraction");
+ let f = Filename.temp_file "testextraction" ".ml" in
+ let () = full_extraction (Some f) l in
+ let () = compile f in
+ let () = remove f; remove (f^"i") in
+ let base = Filename.chop_suffix f ".ml" in
+ let () = remove (base^".cmo"); remove (base^".cmi") in
+ Feedback.msg_notice (str "Extracted code successfully compiled")
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 0629a84a03..e10dcd48b6 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -8,7 +8,6 @@
(*s This module declares the extraction commands. *)
-open API
open Names
open Libnames
open Globnames
@@ -18,6 +17,10 @@ val full_extraction : string option -> reference list -> unit
val separate_extraction : reference list -> unit
val extraction_library : bool -> Id.t -> unit
+(* For the test-suite : extraction to a temporary file + ocamlc on it *)
+
+val extract_and_compile : reference list -> unit
+
(* For debug / external output via coqtop.byte + Drop : *)
val mono_environment :
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d638c232bb..3661faadab 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,7 +7,6 @@
(************************************************************************)
(*i*)
-open API
open Util
open Names
open Term
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 5ee34103c5..e1d43f3405 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -8,7 +8,6 @@
(*s Extraction from Coq terms to Miniml. *)
-open API
open Names
open Term
open Declarations
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 2fa453e533..23452febdc 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,8 +8,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open API
-open Grammar_API.Pcoq.Prim
+open Pcoq.Prim
DECLARE PLUGIN "extraction_plugin"
@@ -66,6 +65,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
(* Monolithic extraction to a file *)
| [ "Extraction" string(f) ne_global_list(l) ]
-> [ full_extraction (Some f) l ]
+
+(* Extraction to a temporary file and OCaml compilation *)
+| [ "Extraction" "TestCompile" ne_global_list(l) ]
+ -> [ extract_and_compile l ]
END
VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6146f32bbe..0f537abece 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -8,7 +8,6 @@
(*s Production of Haskell syntax. *)
-open API
open Pp
open CErrors
open Util
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 1bf19f186b..e43c47d050 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,4 +1,3 @@
-open API
open Pp
open Util
open Names
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index ea966baee6..be8282da06 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -8,7 +8,6 @@
(*s Target language for extraction: a core ML called MiniML. *)
-open API
open Pp
open Names
open Globnames
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index f8c846725e..f1bcde2f3f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,7 +7,6 @@
(************************************************************************)
(*i*)
-open API
open Util
open Names
open Libnames
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 1db96413a8..42d22a7b45 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Globnames
open Miniml
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 365dc191ab..1e0c331901 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open ModPath
open Globnames
@@ -18,10 +17,15 @@ open Mlutil
(*S Functions upon ML modules. *)
+(** Note: a syntax like [(F M) with ...] is actually legal, see for instance
+ bug #4720. Hence the code below tries to handle [MTsig], maybe not in
+ a perfect way, but that should be enough for the use of [se_iter] below. *)
+
let rec msid_of_mt = function
| MTident mp -> mp
+ | MTsig(mp,_) -> mp
| MTwith(mt,_)-> msid_of_mt mt
- | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.")
+ | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *)
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
@@ -37,7 +41,7 @@ let se_iter do_decl do_spec do_mp =
List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
in
let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
- mt_iter mt; do_decl (Dtype(r,l,t))
+ mt_iter mt; do_spec (Stype(r,l,Some t))
| MTwith (mt,ML_With_module(idl,mp))->
let mp_mt = msid_of_mt mt in
let mp_w =
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 1d9db3a5fc..17a6e8db6f 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Globnames
open Miniml
@@ -18,6 +17,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
type do_ref = global_reference -> unit
+val type_iter_references : do_ref -> ml_type -> unit
val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 2ac411d06f..9cbc3fd713 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -8,7 +8,6 @@
(*s Production of Ocaml syntax. *)
-open API
open Pp
open CErrors
open Util
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index bb96489ab0..1ccc273704 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -8,7 +8,6 @@
(*s Production of Scheme syntax. *)
-open API
open Pp
open CErrors
open Util
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2642aeefa4..ca98f07e8d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open ModPath
open Term
@@ -445,9 +444,10 @@ let error_MPfile_as_mod mp b =
"Please "^s2^"use (Recursive) Extraction Library instead.\n"))
let argnames_of_global r =
- let typ = Global.type_of_global_unsafe r in
+ let env = Global.env () in
+ let typ, _ = Global.type_of_global_in_context env r in
let rels,_ =
- decompose_prod (Reduction.whd_all (Global.env ()) typ) in
+ decompose_prod (Reduction.whd_all env typ) in
List.rev_map fst rels
let msg_of_implicit = function
@@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s =
match g with
| ConstRef kn ->
let env = Global.env () in
- let typ = Global.type_of_global_unsafe (ConstRef kn) in
+ let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
let typ = Reduction.whd_all env typ in
if Reduction.is_arity env typ
then begin
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 0215aa8e48..2b3007f025 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Libnames
open Globnames
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:47:01 +0000