summaryrefslogtreecommitdiff
path: root/plugins/extraction/extract_env.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/extract_env.ml')
-rw-r--r--plugins/extraction/extract_env.ml236
1 files changed, 161 insertions, 75 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 52f22ee6..397cb292 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,15 +1,18 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Miniml
-open Term
+open Constr
open Declarations
open Names
+open ModPath
open Libnames
open Globnames
open Pp
@@ -27,13 +30,13 @@ open Common
let toplevel_env () =
let get_reference = function
| (_,kn), Lib.Leaf o ->
- let mp,_,l = repr_kn kn in
+ let mp,_,l = KerName.repr kn in
begin match Libobject.object_tag o with
| "CONSTANT" ->
- let constant = Global.lookup_constant (constant_of_kn kn) in
+ let constant = Global.lookup_constant (Constant.make1 kn) in
Some (l, SFBconst constant)
| "INDUCTIVE" ->
- let inductive = Global.lookup_mind (mind_of_kn kn) in
+ let inductive = Global.lookup_mind (MutInd.make1 kn) in
Some (l, SFBmind inductive)
| "MODULE" ->
let modl = Global.lookup_module (MPdot (mp, l)) in
@@ -41,7 +44,7 @@ let toplevel_env () =
| "MODULE TYPE" ->
let modtype = Global.lookup_modtype (MPdot (mp, l)) in
Some (l, SFBmodtype modtype)
- | "INCLUDE" -> error "No extraction of toplevel Include yet."
+ | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.")
| _ -> None
end
| _ -> None
@@ -72,21 +75,21 @@ module type VISIT = sig
(* Add the module_path and all its prefixes to the mp visit list.
We'll keep all fields of these modules. *)
- val add_mp_all : module_path -> unit
+ val add_mp_all : ModPath.t -> unit
(* Add reference / ... in the visit lists.
These functions silently add the mp of their arg in the mp list *)
val add_ref : global_reference -> unit
- val add_kn : kernel_name -> unit
+ val add_kn : KerName.t -> unit
val add_decl_deps : ml_decl -> unit
val add_spec_deps : ml_spec -> unit
(* Test functions:
is a particular object a needed dependency for the current extraction ? *)
- val needed_ind : mutual_inductive -> bool
- val needed_cst : constant -> bool
- val needed_mp : module_path -> bool
- val needed_mp_all : module_path -> bool
+ val needed_ind : MutInd.t -> bool
+ val needed_cst : Constant.t -> bool
+ val needed_mp : ModPath.t -> bool
+ val needed_mp_all : ModPath.t -> bool
end
module Visit : VISIT = struct
@@ -101,8 +104,8 @@ module Visit : VISIT = struct
v.kn <- KNset.empty;
v.mp <- MPset.empty;
v.mp_all <- MPset.empty
- let needed_ind i = KNset.mem (user_mind i) v.kn
- let needed_cst c = KNset.mem (user_con c) v.kn
+ let needed_ind i = KNset.mem (MutInd.user i) v.kn
+ let needed_cst c = KNset.mem (Constant.user c) v.kn
let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
let needed_mp_all mp = MPset.mem mp v.mp_all
let add_mp mp =
@@ -111,10 +114,10 @@ module Visit : VISIT = struct
check_loaded_modfile mp;
v.mp <- MPset.union (prefixes_mp mp) v.mp;
v.mp_all <- MPset.add mp v.mp_all
- let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
+ let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn)
let add_ref = function
- | ConstRef c -> add_kn (user_con c)
- | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind)
+ | ConstRef c -> add_kn (Constant.user c)
+ | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind)
| VarRef _ -> assert false
let add_decl_deps = decl_iter_references add_ref add_ref add_ref
let add_spec_deps = spec_iter_references add_ref add_ref add_ref
@@ -131,25 +134,28 @@ 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 =
+let get_body lbody =
+ EConstr.of_constr (Mod_subst.force_constr lbody)
+
+let check_fix env sg cb i =
match cb.const_body with
| Def lbody ->
- (match kind_of_term (Mod_subst.force_constr lbody) with
- | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
+ (match EConstr.kind sg (get_body lbody) with
+ | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
| CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
| _ -> raise Impossible)
| Undef _ | OpaqueDef _ -> raise Impossible
-let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
+let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
Array.equal Name.equal na1 na2 &&
- Array.equal eq_constr ca1 ca2 &&
- Array.equal eq_constr ta1 ta2
+ Array.equal (EConstr.eq_constr sg) ca1 ca2 &&
+ Array.equal (EConstr.eq_constr sg) ta1 ta2
-let factor_fix env l cb msb =
- let _,recd as check = check_fix env cb 0 in
+let factor_fix env sg l cb msb =
+ let _,recd as check = check_fix env sg cb 0 in
let n = Array.length (let fi,_,_ = recd in fi) in
if Int.equal n 1 then [|l|], recd, msb
else begin
@@ -160,9 +166,9 @@ let factor_fix env l cb msb =
(fun j ->
function
| (l,SFBconst cb') ->
- let check' = check_fix env cb' (j+1) in
- if not ((fst check : bool) == (fst check') &&
- prec_declaration_equal (snd check) (snd check'))
+ let check' = check_fix env sg cb' (j+1) in
+ if not ((fst check : bool) == (fst check') &&
+ prec_declaration_equal sg (snd check) (snd check'))
then raise Impossible;
labels.(j+1) <- l;
| _ -> raise Impossible) msb';
@@ -174,26 +180,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
-
-(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
- To check with Elie. *)
+ Mod_typing.translate_mse env mpo inl me
-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)
@@ -233,20 +245,26 @@ 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
- (match extract_with_type env' c with (* cb may contain some kn *)
+ 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
+ let sg = Evd.from_env env in
+ (match extract_with_type env' sg (EConstr.of_constr 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') ->
@@ -257,8 +275,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 ->
@@ -270,7 +288,8 @@ and extract_msignature_spec env mp1 reso = function
MTfunsig (mbid, extract_mbody_spec env mp mtb,
extract_msignature_spec env' mp1 reso me)
-and extract_mbody_spec env mp mb = match mb.mod_type_alg with
+and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ =
+ fun env mp mb -> match mb.mod_type_alg with
| Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
| None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type
@@ -285,12 +304,13 @@ let rec extract_structure env mp reso ~all = function
| [] -> []
| (l,SFBconst cb) :: struc ->
(try
- let vl,recd,struc = factor_fix env l cb struc in
+ let sg = Evd.from_env env in
+ let vl,recd,struc = factor_fix env sg l cb struc in
let vc = Array.map (make_cst reso mp) vl in
let ms = extract_structure env mp reso ~all struc in
let b = Array.exists Visit.needed_cst vc in
if all || b then
- let d = extract_fixpoint env vc recd in
+ let d = extract_fixpoint env sg vc recd in
if (not b) && (logical_decl d) then ms
else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
else ms
@@ -330,11 +350,11 @@ let rec extract_structure env mp reso ~all = function
and extract_mexpr env mp = function
| MEwith _ -> assert false (* no 'with' syntax for modules *)
- | me when lang () != Ocaml ->
+ | me when lang () != Ocaml || Table.is_extrcompute () ->
(* 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;
@@ -435,7 +455,7 @@ let mono_filename f =
else
try Id.of_string (Filename.basename f)
with UserError _ ->
- error "Extraction: provided filename is not a valid identifier"
+ user_err Pp.(str "Extraction: provided filename is not a valid identifier")
in
Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
@@ -472,13 +492,14 @@ let formatter dry file =
if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
else
match file with
- | Some f -> Pp_control.with_output_to f
+ | Some f -> Topfmt.with_output_to f
| None -> Format.formatter_of_buffer buf
in
+ (* XXX: Fixme, this shouldn't depend on Topfmt *)
(* We never want to see ellipsis ... in extracted code *)
Format.pp_set_max_boxes ft max_int;
(* We reuse the width information given via "Set Printing Width" *)
- (match Pp_control.get_margin () with
+ (match Topfmt.get_margin () with
| None -> ()
| Some i ->
Format.pp_set_margin ft i;
@@ -507,8 +528,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
in
(* First, a dry run, for computing objects to rename or duplicate *)
set_phase Pre;
- let devnull = formatter true None in
- pp_with devnull (d.pp_struct struc);
+ ignore (d.pp_struct struc);
let opened = opened_libraries () in
(* Print the implementation *)
let cout = if dry then None else Option.map open_out fn in
@@ -519,8 +539,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
set_phase Impl;
pp_with ft (d.preamble mo comment opened unsafe_needs);
pp_with ft (d.pp_struct struc);
+ Format.pp_print_flush ft ();
Option.iter close_out cout;
with reraise ->
+ Format.pp_print_flush ft ();
Option.iter close_out cout; raise reraise
end;
if not dry then Option.iter info_file fn;
@@ -533,8 +555,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
set_phase Intf;
pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
pp_with ft (d.pp_sig (signature_of_structure struc));
+ Format.pp_print_flush ft ();
close_out cout;
with reraise ->
+ Format.pp_print_flush ft ();
close_out cout; raise reraise
end;
info_file si)
@@ -554,11 +578,12 @@ let print_structure_to_file (fn,si,mo) dry struc =
let reset () =
Visit.reset (); reset_tables (); reset_renaming_tables Everything
-let init modular library =
- check_inside_section (); check_inside_module ();
+let init ?(compute=false) ?(inner=false) modular library =
+ if not inner then (check_inside_section (); check_inside_module ());
set_keywords (descr ()).keywords;
set_modular modular;
set_library library;
+ set_extrcompute compute;
reset ();
if modular && lang () == Scheme then error_scheme ()
@@ -572,8 +597,8 @@ let warns () =
let rec locate_ref = function
| [] -> [],[]
| r::l ->
- let q = snd (qualid_of_reference r) in
- let mpo = try Some (Nametab.locate_module q) with Not_found -> None
+ let q = qualid_of_reference r in
+ let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None
and ro =
try Some (Smartlocate.global_with_alias r)
with Nametab.GlobalizationError _ | UserError _ -> None
@@ -583,7 +608,7 @@ let rec locate_ref = function
| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
| Some mp, Some r ->
- warning_ambiguous_name (q,mp,r);
+ warning_ambiguous_name (q.CAst.v,mp,r);
let refs,mps = locate_ref l in refs,mp::mps
(*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -621,7 +646,7 @@ let separate_extraction lr =
is \verb!Extraction! [qualid]. *)
let simple_extraction r =
- Vernacentries.dump_global (Misctypes.AN r);
+ Vernacentries.dump_global CAst.(make (Misctypes.AN r));
match locate_ref [r] with
| ([], [mp]) as p -> full_extr None p
| [r],[] ->
@@ -653,7 +678,7 @@ let extraction_library is_rec m =
let l = List.rev (environment_until (Some dir_m)) in
let select l (mp,struc) =
if Visit.needed_mp mp
- then (mp, extract_structure env mp no_delta true struc) :: l
+ then (mp, extract_structure env mp no_delta ~all:true struc) :: l
else l
in
let struc = List.fold_left select [] l in
@@ -668,15 +693,76 @@ let extraction_library is_rec m =
List.iter print struc;
reset ()
-let structure_for_compute c =
- init false false;
- let env = Global.env () in
- let ast, mlt = Extraction.extract_constr env c in
+(** For extraction compute, we flatten all the module structure,
+ getting rid of module types or unapplied functors *)
+
+let flatten_structure struc =
+ let rec flatten_elem (lab,elem) = match elem with
+ |SEdecl d -> [d]
+ |SEmodtype _ -> []
+ |SEmodule m -> match m.ml_mod_expr with
+ |MEfunctor _ -> []
+ |MEident _ | MEapply _ -> assert false (* should be expanded *)
+ |MEstruct (_,elems) -> flatten_elems elems
+ and flatten_elems l = List.flatten (List.map flatten_elem l)
+ in flatten_elems (List.flatten (List.map snd struc))
+
+let structure_for_compute env sg c =
+ init false false ~compute:true;
+ let ast, mlt = Extraction.extract_constr env sg c in
let ast = Mlutil.normalize ast in
let refs = ref Refset.empty in
let add_ref r = refs := Refset.add r !refs in
let () = ast_iter_references add_ref add_ref add_ref ast in
let refs = Refset.elements !refs in
let struc = optimize_struct (refs,[]) (mono_environment refs []) in
- let flatstruc = List.map snd (List.flatten (List.map snd struc)) in
- flatstruc, ast, mlt
+ (flatten_structure struc), 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")
+
+(* Show the extraction of the current ongoing proof *)
+
+let show_extraction () =
+ init ~inner:true false false;
+ let prf = Proof_global.give_me_the_proof () in
+ let sigma, env = Pfedit.get_current_context () in
+ let trms = Proof.partial_proof prf in
+ let extr_term t =
+ let ast, ty = extract_constr env sigma t in
+ let mp = Lib.current_mp () in
+ let l = Label.of_id (Proof_global.get_current_proof_name ()) in
+ let fake_ref = ConstRef (Constant.make2 mp l) in
+ let decl = Dterm (fake_ref, ast, ty) in
+ print_one_decl [] mp decl
+ in
+ Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl extr_term trms)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 01:48:06 +0000