aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml84
-rw-r--r--plugins/extraction/extract_env.mli4
-rw-r--r--plugins/extraction/extraction.ml8
-rw-r--r--plugins/extraction/g_extraction.ml46
-rw-r--r--plugins/extraction/mlutil.ml2
-rw-r--r--plugins/extraction/modutil.ml9
-rw-r--r--plugins/extraction/modutil.mli1
7 files changed, 85 insertions, 29 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7d69cbff1..89c2a0ae3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -132,7 +132,7 @@ let rec add_labels mp = function
exception Impossible
let check_arity env cb =
- let t = Typeops.type_of_constant_type env cb.const_type in
+ let t = cb.const_type in
if Reduction.is_arity env t then raise Impossible
let check_fix env cb i =
@@ -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/extraction.ml b/plugins/extraction/extraction.ml
index 3661faada..661842790 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -518,7 +518,7 @@ and mlt_env env r = match r with
match lookup_typedef kn cb with
| Some _ as o -> o
| None ->
- let typ = Typeops.type_of_constant_type env cb.const_type
+ let typ = cb.const_type
(* FIXME not sure if we should instantiate univs here *) in
match flag_of_type env typ with
| Info,TypeScheme ->
@@ -543,7 +543,7 @@ let record_constant_type env kn opt_typ =
| Some schema -> schema
| None ->
let typ = match opt_typ with
- | None -> Typeops.type_of_constant_type env cb.const_type
+ | None -> cb.const_type
| Some typ -> typ
in
let mlt = extract_type env [] 1 typ [] in
@@ -969,7 +969,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
let extract_constant env kn cb =
let r = ConstRef kn in
- let typ = Typeops.type_of_constant_type env cb.const_type in
+ let typ = cb.const_type in
let warn_info () = if not (is_custom r) then add_info_axiom r in
let warn_log () = if not (constant_has_body cb) then add_log_axiom r
in
@@ -1025,7 +1025,7 @@ let extract_constant env kn cb =
let extract_constant_spec env kn cb =
let r = ConstRef kn in
- let typ = Typeops.type_of_constant_type env cb.const_type in
+ let typ = cb.const_type in
try
match flag_of_type env typ with
| (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
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/mlutil.ml b/plugins/extraction/mlutil.ml
index f1bcde2f3..a4c2bcd88 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -120,7 +120,6 @@ let rec mgu = function
mgu (a, a'); mgu (b, b')
| Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
List.iter mgu (List.combine l l')
- | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
| Tdummy _, Tdummy _ -> ()
| Tvar i, Tvar j when Int.equal i j -> ()
| Tvar' i, Tvar' j when Int.equal i j -> ()
@@ -1052,6 +1051,7 @@ let rec simpl o = function
| MLmagic(MLcase(typ,e,br)) ->
let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
simpl o (MLcase(typ,e,br'))
+ | MLmagic(MLdummy _ as e) when lang () == Haskell -> e
| MLmagic(MLexn _ as e) -> e
| a -> ast_map (simpl o) a
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-06-22 04:23:43 +0000