aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml82
-rw-r--r--plugins/extraction/extract_env.mli4
-rw-r--r--plugins/extraction/g_extraction.ml46
-rw-r--r--plugins/extraction/modutil.ml9
-rw-r--r--plugins/extraction/modutil.mli1
5 files changed, 79 insertions, 23 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7d69cbff1..39826d744 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -175,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)
@@ -234,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') ->
@@ -258,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 ->
@@ -335,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;
@@ -685,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 f289b63ad..e10dcd48b 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -17,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/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 4372ea557..23452febd 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API.Pcoq.Prim
+open Pcoq.Prim
DECLARE PLUGIN "extraction_plugin"
@@ -65,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/modutil.ml b/plugins/extraction/modutil.ml
index a896a8d03..1e0c33190 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -17,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]. *)
@@ -36,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 ad60b58d5..17a6e8db6 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -17,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 07:56:56 +0000