summaryrefslogtreecommitdiff
path: root/contrib/extraction/extract_env.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/extraction/extract_env.ml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/extraction/extract_env.ml')
-rw-r--r--contrib/extraction/extract_env.ml382
1 files changed, 382 insertions, 0 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
new file mode 100644
index 00000000..d725a1d7
--- /dev/null
+++ b/contrib/extraction/extract_env.ml
@@ -0,0 +1,382 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: extract_env.ml,v 1.74.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+
+open Term
+open Declarations
+open Names
+open Libnames
+open Pp
+open Util
+open Miniml
+open Table
+open Extraction
+open Modutil
+open Common
+
+(*s Obtaining Coq environment. *)
+
+let toplevel_env () =
+ let seg = Lib.contents_after None in
+ let get_reference = function
+ | (_,kn), Lib.Leaf o ->
+ let mp,_,l = repr_kn kn in
+ let seb = match Libobject.object_tag o with
+ | "CONSTANT" -> SEBconst (Global.lookup_constant kn)
+ | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn)
+ | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l)))
+ | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn)
+ | _ -> failwith "caught"
+ in l,seb
+ | _ -> failwith "caught"
+ in
+ match current_toplevel () with
+ | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg))
+ | _ -> assert false
+
+let environment_until dir_opt =
+ let rec parse = function
+ | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
+ | [] -> []
+ | d :: l ->
+ match (Global.lookup_module (MPfile d)).mod_expr with
+ | Some meb ->
+ if dir_opt = Some d then [MPfile d, meb]
+ else (MPfile d, meb) :: (parse l)
+ | _ -> assert false
+ in parse (Library.loaded_libraries ())
+
+type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
+
+let in_kn v kn = KNset.mem kn v.kn
+let in_mp v mp = MPset.mem mp v.mp
+
+let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
+let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
+let visit_ref v r = visit_kn v (kn_of_r r)
+
+exception Impossible
+
+let check_arity env cb =
+ if Reduction.is_arity env cb.const_type then raise Impossible
+
+let check_fix env cb i =
+ match cb.const_body with
+ | None -> raise Impossible
+ | Some lbody ->
+ match kind_of_term (Declarations.force lbody) with
+ | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
+ | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
+ | _ -> raise Impossible
+
+let factor_fix env l cb msb =
+ let _,recd as check = check_fix env cb 0 in
+ let n = Array.length (let fi,_,_ = recd in fi) in
+ if n = 1 then [|l|], recd, msb
+ else begin
+ if List.length msb < n-1 then raise Impossible;
+ let msb', msb'' = list_chop (n-1) msb in
+ let labels = Array.make n l in
+ list_iter_i
+ (fun j ->
+ function
+ | (l,SEBconst cb') ->
+ if check <> check_fix env cb' (j+1) then raise Impossible;
+ labels.(j+1) <- l;
+ | _ -> raise Impossible) msb';
+ labels, recd, msb''
+ end
+
+let get_decl_references v d =
+ let f = visit_ref v in decl_iter_references f f f d
+
+let get_spec_references v s =
+ let f = visit_ref v in spec_iter_references f f f s
+
+let rec extract_msig env v mp = function
+ | [] -> []
+ | (l,SPBconst cb) :: msig ->
+ let kn = make_kn mp empty_dirpath l in
+ let s = extract_constant_spec env kn cb in
+ if logical_spec s then extract_msig env v mp msig
+ else begin
+ get_spec_references v s;
+ (l,Spec s) :: (extract_msig env v mp msig)
+ end
+ | (l,SPBmind cb) :: msig ->
+ let kn = make_kn mp empty_dirpath l in
+ let s = Sind (kn, extract_inductive env kn) in
+ if logical_spec s then extract_msig env v mp msig
+ else begin
+ get_spec_references v s;
+ (l,Spec s) :: (extract_msig env v mp msig)
+ end
+ | (l,SPBmodule {msb_modtype=mtb}) :: msig ->
+(*i let mpo = Some (MPdot (mp,l)) in i*)
+ (l,Smodule (extract_mtb env v None (*i mpo i*) mtb)) :: (extract_msig env v mp msig)
+ | (l,SPBmodtype mtb) :: msig ->
+ (l,Smodtype (extract_mtb env v None mtb)) :: (extract_msig env v mp msig)
+
+and extract_mtb env v mpo = function
+ | MTBident kn -> visit_kn v kn; MTident kn
+ | MTBfunsig (mbid, mtb, mtb') ->
+ let mp = MPbound mbid in
+ let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
+ MTfunsig (mbid, extract_mtb env v None mtb,
+ extract_mtb env' v None mtb')
+ | MTBsig (msid, msig) ->
+ let mp, msig = match mpo with
+ | None -> MPself msid, msig
+ | Some mp -> mp, Modops.subst_signature_msid msid mp msig
+ in
+ let env' = Modops.add_signature mp msig env in
+ MTsig (msid, extract_msig env' v mp msig)
+
+let rec extract_msb env v mp all = function
+ | [] -> []
+ | (l,SEBconst cb) :: msb ->
+ (try
+ let vl,recd,msb = factor_fix env l cb msb in
+ let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in
+ let ms = extract_msb env v mp all msb in
+ let b = array_exists (in_kn v) vkn in
+ if all || b then
+ let d = extract_fixpoint env vkn recd in
+ if (not b) && (logical_decl d) then ms
+ else begin get_decl_references v d; (l,SEdecl d) :: ms end
+ else ms
+ with Impossible ->
+ let ms = extract_msb env v mp all msb in
+ let kn = make_kn mp empty_dirpath l in
+ let b = in_kn v kn in
+ if all || b then
+ let d = extract_constant env kn cb in
+ if (not b) && (logical_decl d) then ms
+ else begin get_decl_references v d; (l,SEdecl d) :: ms end
+ else ms)
+ | (l,SEBmind mib) :: msb ->
+ let ms = extract_msb env v mp all msb in
+ let kn = make_kn mp empty_dirpath l in
+ let b = in_kn v kn in
+ if all || b then
+ let d = Dind (kn, extract_inductive env kn) in
+ if (not b) && (logical_decl d) then ms
+ else begin get_decl_references v d; (l,SEdecl d) :: ms end
+ else ms
+ | (l,SEBmodule mb) :: msb ->
+ let ms = extract_msb env v mp all msb in
+ let mp = MPdot (mp,l) in
+ if all || in_mp v mp then
+ (l,SEmodule (extract_module env v mp true mb)) :: ms
+ else ms
+ | (l,SEBmodtype mtb) :: msb ->
+ let ms = extract_msb env v mp all msb in
+ let kn = make_kn mp empty_dirpath l in
+ if all || in_kn v kn then
+ (l,SEmodtype (extract_mtb env v None mtb)) :: ms
+ else ms
+
+and extract_meb env v mpo all = function
+ | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *)
+ | MEBident mp -> visit_mp v mp; MEident mp
+ | MEBapply (meb, meb',_) ->
+ MEapply (extract_meb env v None true meb,
+ extract_meb env v None true meb')
+ | MEBfunctor (mbid, mtb, meb) ->
+ let mp = MPbound mbid in
+ let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
+ MEfunctor (mbid, extract_mtb env v None mtb,
+ extract_meb env' v None true meb)
+ | MEBstruct (msid, msb) ->
+ let mp,msb = match mpo with
+ | None -> MPself msid, msb
+ | Some mp -> mp, subst_msb (map_msid msid mp) msb
+ in
+ let env' = add_structure mp msb env in
+ MEstruct (msid, extract_msb env' v mp all msb)
+
+and extract_module env v mp all mb =
+ (* [mb.mod_expr <> None ], since we look at modules from outside. *)
+ (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
+ let meb = out_some mb.mod_expr in
+ let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in
+ (* Because of the "with" construct, the module type can be [MTBsig] with *)
+ (* a msid different from the one of the module. Here is the patch. *)
+ let mtb = replicate_msid meb mtb in
+ { ml_mod_expr = extract_meb env v (Some mp) all meb;
+ ml_mod_type = extract_mtb env v None mtb }
+
+let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
+
+let mono_environment refs mpl =
+ let l = environment_until None in
+ let v =
+ let add_kn r = KNset.add (kn_of_r r) in
+ let kns = List.fold_right add_kn refs KNset.empty in
+ let add_mp mp = MPset.union (prefixes_mp mp) in
+ let mps = List.fold_right add_mp mpl MPset.empty in
+ let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in
+ { kn = kns; mp = mps }
+ in
+ let env = Global.env () in
+ List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m))
+ (List.rev l)
+
+(*s Recursive extraction in the Coq toplevel. The vernacular command is
+ \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
+ to get the saturated environment to extract. *)
+
+let mono_extraction (f,m) qualids =
+ check_inside_section ();
+ check_inside_module ();
+ let rec find = function
+ | [] -> [],[]
+ | q::l ->
+ let refs,mps = find l in
+ try
+ let mp = Nametab.locate_module (snd (qualid_of_reference q))
+ in refs,(mp::mps)
+ with Not_found -> (Nametab.global q)::refs, mps
+ in
+ let refs,mps = find qualids in
+ let prm = {modular=false; mod_name = m; to_appear= refs} in
+ let struc = optimize_struct prm None (mono_environment refs mps) in
+ print_structure_to_file f prm struc;
+ reset_tables ()
+
+let extraction_rec = mono_extraction (None,id_of_string "Main")
+
+(*s Extraction in the Coq toplevel. We display the extracted term in
+ Ocaml syntax and we use the Coq printers for globals. The
+ vernacular command is \verb!Extraction! [qualid]. *)
+
+let extraction qid =
+ check_inside_section ();
+ check_inside_module ();
+ try
+ let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in
+ extraction_rec [qid]
+ with Not_found ->
+ let r = Nametab.global qid in
+ if is_custom r then
+ msgnl (str "User defined extraction:" ++ spc () ++
+ str (find_custom r) ++ fnl ())
+ else begin
+ let prm =
+ { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
+ let kn = kn_of_r r in
+ let struc = optimize_struct prm None (mono_environment [r] []) in
+ let d = get_decl_in_structure r struc in
+ print_one_decl struc (modpath kn) d;
+ reset_tables ()
+ end
+
+(*s Extraction to a file (necessarily recursive).
+ The vernacular command is
+ \verb!Extraction "file"! [qualid1] ... [qualidn].*)
+
+let lang_suffix () = match lang () with
+ | Ocaml -> ".ml",".mli"
+ | Haskell -> ".hs",".hi"
+ | Scheme -> ".scm",".scm"
+ | Toplevel -> assert false
+
+let filename f =
+ let s,s' = lang_suffix () in
+ if Filename.check_suffix f s then
+ let f' = Filename.chop_suffix f s in
+ Some (f,f'^s'),id_of_string f'
+ else Some (f^s,f^s'),id_of_string f
+
+let extraction_file f vl =
+ if lang () = Toplevel then error_toplevel ()
+ else mono_extraction (filename f) vl
+
+(*s Extraction of a module at the toplevel. *)
+
+let extraction_module m =
+ check_inside_section ();
+ check_inside_module ();
+ match lang () with
+ | Toplevel -> error_toplevel ()
+ | Scheme -> error_scheme ()
+ | _ ->
+ let q = snd (qualid_of_reference m) in
+ let mp =
+ try Nametab.locate_module q
+ with Not_found -> error_unknown_module q
+ in
+ let b = is_modfile mp in
+ let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
+ let l = environment_until None in
+ let v = { kn = KNset.empty ; mp = prefixes_mp mp } in
+ let env = Global.env () in
+ let struc =
+ List.rev_map
+ (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) b m))
+ (List.rev l)
+ in
+ let struc = optimize_struct prm None struc in
+ let struc =
+ let bmp = base_mp mp in
+ try [bmp, List.assoc bmp struc] with Not_found -> assert false
+ in
+ print_structure_to_file None prm struc;
+ reset_tables ()
+
+(*s (Recursive) Extraction of a library. The vernacular command is
+ \verb!(Recursive) Extraction Library! [M]. *)
+
+let module_file_name m = match lang () with
+ | Ocaml -> let f = String.uncapitalize (string_of_id m) in f^".ml", f^".mli"
+ | Haskell -> let f = String.capitalize (string_of_id m) in f^".hs", f^".hi"
+ | _ -> assert false
+
+let dir_module_of_id m =
+ let q = make_short_qualid m in
+ try Nametab.full_name_module q with Not_found -> error_unknown_module q
+
+let extraction_library is_rec m =
+ check_inside_section ();
+ check_inside_module ();
+ match lang () with
+ | Toplevel -> error_toplevel ()
+ | Scheme -> error_scheme ()
+ | _ ->
+ let dir_m = dir_module_of_id m in
+ let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in
+ let l = environment_until (Some dir_m) in
+ let struc =
+ let env = Global.env () in
+ let select l (mp,meb) =
+ if in_mp v mp (* [mp] est long -> [in_mp] peut etre sans [long_mp] *)
+ then (mp, unpack (extract_meb env v (Some mp) true meb)) :: l
+ else l
+ in
+ List.fold_left select [] (List.rev l)
+ in
+ let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+ let struc = optimize_struct dummy_prm None struc in
+ let rec print = function
+ | [] -> ()
+ | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l
+ | (MPfile dir, sel) as e :: l ->
+ let short_m = snd (split_dirpath dir) in
+ let f = module_file_name short_m in
+ let prm = {modular=true;mod_name=short_m;to_appear=[]} in
+ print_structure_to_file (Some f) prm [e];
+ print l
+ | _ -> assert false
+ in print struc;
+ reset_tables ()
+
+
+
+
+