diff options
Diffstat (limited to 'contrib/extraction/extract_env.ml')
-rw-r--r-- | contrib/extraction/extract_env.ml | 453 |
1 files changed, 271 insertions, 182 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 825b3554..311b42c0 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 10209 2007-10-09 21:49:37Z letouzey $ i*) +(*i $Id: extract_env.ml 10794 2008-04-15 00:12:06Z letouzey $ i*) open Term open Declarations @@ -21,7 +21,9 @@ open Modutil open Common open Mod_subst -(*s Obtaining Coq environment. *) +(***************************************) +(*S Part I: computing Coq environment. *) +(***************************************) let toplevel_env () = let seg = Lib.contents_after None in @@ -29,16 +31,17 @@ let toplevel_env () = | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in let seb = match Libobject.object_tag o with - | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn)) - | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) - | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l))) - | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn) + | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn)) + | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) + | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) + | "MODULE TYPE" -> + SFBmodtype (Global.lookup_modtype (MPdot (mp,l))) | _ -> failwith "caught" in l,seb | _ -> failwith "caught" in match current_toplevel () with - | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg)) + | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg)) | _ -> assert false let environment_until dir_opt = @@ -130,58 +133,87 @@ let factor_fix env l cb msb = list_iter_i (fun j -> function - | (l,SEBconst cb') -> + | (l,SFBconst cb') -> if check <> check_fix env cb' (j+1) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; labels, recd, msb'' end -let rec extract_msig env mp = function +(* From a [structure_body] (i.e. a list of [structure_field_body]) + to specifications. *) + +let rec extract_sfb_spec env mp = function | [] -> [] - | (l,SPBconst cb) :: msig -> + | (l,SFBconst cb) :: msig -> let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in - if logical_spec s then extract_msig env mp msig - else begin - Visit.add_spec_deps s; - (l,Spec s) :: (extract_msig env mp msig) - end - | (l,SPBmind cb) :: msig -> + let specs = extract_sfb_spec env mp msig in + if logical_spec s then specs + else begin Visit.add_spec_deps s; (l,Spec s) :: specs end + | (l,SFBmind 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 mp msig - else begin - Visit.add_spec_deps s; - (l,Spec s) :: (extract_msig env mp msig) - end - | (l,SPBmodule {msb_modtype=mtb}) :: msig -> - (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig) - | (l,SPBmodtype mtb) :: msig -> - (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig) - -and extract_mtb env mpo = function - | MTBident kn -> Visit.add_kn kn; MTident kn - | MTBfunsig (mbid, mtb, mtb') -> + let specs = extract_sfb_spec env mp msig in + if logical_spec s then specs + else begin Visit.add_spec_deps s; (l,Spec s) :: specs end + | (l,SFBmodule mb) :: msig -> + let specs = extract_sfb_spec env mp msig in + let mtb = Modops.type_of_mb env mb in + let spec = extract_seb_spec env (mb.mod_type<>None) mtb in + (l,Smodule spec) :: specs + | (l,SFBmodtype mtb) :: msig -> + let specs = extract_sfb_spec env mp msig in + (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs + | (l,SFBalias(mp1,_))::msig -> + extract_sfb_spec env mp + ((l,SFBmodule {mod_expr = Some (SEBident mp1); + mod_type = None; + mod_constraints = Univ.Constraint.empty; + mod_alias = Mod_subst.empty_subst; + mod_retroknowledge = []})::msig) + +(* From [struct_expr_body] to specifications *) + + +and extract_seb_spec env truetype = function + | SEBident kn when truetype -> Visit.add_mp kn; MTident kn + | SEBwith(mtb',With_definition_body(idl,cb))-> + let mtb''= extract_seb_spec env truetype mtb' in + (match extract_with_type env cb with (* cb peut contenir des kn *) + | None -> mtb'' + | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) + | SEBwith(mtb',With_module_body(idl,mp,_))-> + Visit.add_mp mp; + MTwith(extract_seb_spec env truetype mtb', + ML_With_module(idl,mp)) + | SEBfunctor (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 None mtb, - extract_mtb env' 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_module mp (Modops.module_body_of_type mtb) env in + MTfunsig (mbid, extract_seb_spec env true mtb.typ_expr, + extract_seb_spec env' truetype mtb') + | SEBstruct (msid, msig) -> + let mp = MPself msid in let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_msig env' mp msig) + MTsig (msid, extract_sfb_spec env' mp msig) + | (SEBapply _|SEBident _ (*when not truetype*)) as mtb -> + extract_seb_spec env truetype (Modops.eval_struct env mtb) + + +(* From a [structure_body] (i.e. a list of [structure_field_body]) + to implementations. -let rec extract_msb env mp all = function + NB: when [all=false], the evaluation order of the list is + important: last to first ensures correct dependencies. +*) + +let rec extract_sfb env mp all = function | [] -> [] - | (l,SEBconst cb) :: msb -> + | (l,SFBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in let vc = Array.map (make_con mp empty_dirpath) vl in - let ms = extract_msb env mp all msb in + let ms = extract_sfb env mp all msb in let b = array_exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in @@ -189,7 +221,7 @@ let rec extract_msb env mp all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_msb env mp all msb in + let ms = extract_sfb env mp all msb in let c = make_con mp empty_dirpath l in let b = Visit.needed_con c in if all || b then @@ -197,8 +229,8 @@ let rec extract_msb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) - | (l,SEBmind mib) :: msb -> - let ms = extract_msb env mp all msb in + | (l,SFBmind mib) :: msb -> + let ms = extract_sfb env mp all msb in let kn = make_kn mp empty_dirpath l in let b = Visit.needed_kn kn in if all || b then @@ -206,48 +238,68 @@ let rec extract_msb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms - | (l,SEBmodule mb) :: msb -> - let ms = extract_msb env mp all msb in + | (l,SFBmodule mb) :: msb -> + let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodule (extract_module env mp true mb)) :: ms else ms - | (l,SEBmodtype mtb) :: msb -> - let ms = extract_msb env mp all msb in - let kn = make_kn mp empty_dirpath l in - if all || Visit.needed_kn kn then - (l,SEmodtype (extract_mtb env None mtb)) :: ms + | (l,SFBmodtype mtb) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms + else ms + | (l,SFBalias (mp1,cst)) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true + {mod_expr = Some (SEBident mp1); + mod_type = None; + mod_constraints= Univ.Constraint.empty; + mod_alias = empty_subst; + mod_retroknowledge = []})) :: ms else ms -and extract_meb env mpo all = function - | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *) - | MEBident mp -> Visit.add_mp mp; MEident mp - | MEBapply (meb, meb',_) -> - MEapply (extract_meb env None true meb, - extract_meb env None true meb') - | MEBfunctor (mbid, mtb, meb) -> +(* From [struct_expr_body] to implementations *) + +and extract_seb env mpo all = function + | SEBident mp -> + if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; + Visit.add_mp mp; MEident mp + | SEBapply (meb, meb',_) -> + MEapply (extract_seb env None true meb, + extract_seb env None true meb') + | SEBfunctor (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 None mtb, - extract_meb env' None true meb) - | MEBstruct (msid, msb) -> + MEfunctor (mbid, extract_seb_spec env true mtb.typ_expr, + extract_seb env' None true meb) + | SEBstruct (msid, msb) -> let mp,msb = match mpo with | None -> MPself msid, msb - | Some mp -> mp, subst_msb (map_msid msid mp) msb + | Some mp -> mp, Modops.subst_structure (map_msid msid mp) msb in - let env' = add_structure mp msb env in - MEstruct (msid, extract_msb env' mp all msb) + let env' = Modops.add_signature mp msb env in + MEstruct (msid, extract_sfb env' mp all msb) + | SEBwith (_,_) -> anomaly "Not available yet" and extract_module env 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 + let meb = Option.get mb.mod_expr in + let mtb = match mb.mod_type with + | None -> Modops.eval_struct env meb + | 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 (Some mp) all meb; - ml_mod_type = extract_mtb env None mtb } + (* PL 26/02/2008: is this still relevant ? + let mtb = replicate_msid meb mtb in *) + { ml_mod_expr = extract_seb env (Some mp) all meb; + ml_mod_type = extract_seb_spec env (mb.mod_type<>None) mtb } + let unpack = function MEstruct (_,sel) -> sel | _ -> assert false @@ -258,161 +310,198 @@ let mono_environment refs mpl = let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l + (fun (mp,m) -> mp, unpack (extract_seb env (Some mp) false m)) l + +(**************************************) +(*S Part II : Input/Output primitives *) +(**************************************) + +let descr () = match lang () with + | Ocaml -> Ocaml.ocaml_descr + | Haskell -> Haskell.haskell_descr + | Scheme -> Scheme.scheme_descr + +(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" + Works similarly for the other languages. *) + +let default_id = id_of_string "Main" + +let mono_filename f = + let d = descr () in + match f with + | None -> None, None, default_id + | Some f -> + let f = + if Filename.check_suffix f d.file_suffix then + Filename.chop_suffix f d.file_suffix + else f + in + let id = + if lang () <> Haskell then default_id + else try id_of_string (Filename.basename f) + with _ -> error "Extraction: provided filename is not a valid identifier" + in + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id + +(* Builds a suitable filename from a module id *) + +let module_filename m = + let d = descr () in + let f = if d.capital_file then String.capitalize else String.uncapitalize in + let fn = f (string_of_id m) in + Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m + +(*s Extraction of one decl to stdout. *) + +let print_one_decl struc mp decl = + let d = descr () in + reset_renaming_tables AllButExternal; + ignore (create_renamings struc); + push_visible mp; + msgnl (d.pp_decl decl); + pop_visible () + +(*s Extraction of a ml struct to a file. *) + +let print_structure_to_file (fn,si,mo) struc = + let d = descr () in + reset_renaming_tables AllButExternal; + let used_modules = create_renamings struc in + let unsafe_needs = { + mldummy = struct_ast_search ((=) MLdummy) struc; + tdummy = struct_type_search Mlutil.isDummy struc; + tunknown = struct_type_search ((=) Tunknown) struc; + magic = + if lang () <> Haskell then false + else struct_ast_search (function MLmagic _ -> true | _ -> false) struc } + in + (* print the implementation *) + let cout = Option.map open_out fn in + let ft = match cout with + | None -> !Pp_control.std_ft + | Some cout -> Pp_control.with_output_to cout in + begin try + msg_with ft (d.preamble mo used_modules unsafe_needs); + if lang () = Ocaml then begin + (* for computing objects to duplicate *) + let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in + msg_with devnull (d.pp_struct struc); + reset_renaming_tables OnlyLocal; + end; + msg_with ft (d.pp_struct struc); + Option.iter close_out cout; + with e -> + Option.iter close_out cout; raise e + end; + Option.iter info_file fn; + (* print the signature *) + Option.iter + (fun si -> + let cout = open_out si in + let ft = Pp_control.with_output_to cout in + begin try + msg_with ft (d.sig_preamble mo used_modules unsafe_needs); + reset_renaming_tables OnlyLocal; + msg_with ft (d.pp_sig (signature_of_structure struc)); + close_out cout; + with e -> + close_out cout; raise e + end; + info_file si) + si + + +(*********************************************) +(*s Part III: the actual extraction commands *) +(*********************************************) + + +let reset () = + Visit.reset (); reset_tables (); reset_renaming_tables Everything + +let init modular = + check_inside_section (); check_inside_module (); + set_keywords (descr ()).keywords; + set_modular modular; + reset (); + if modular && lang () = Scheme then error_scheme () + - (*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. *) + \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when + extracting to a file with the command: + \verb!Extraction "file"! [qualid1] ... [qualidn]. *) -let mono_extraction (f,m) qualids = - check_inside_section (); - check_inside_module (); +let full_extraction f qualids = + init false; 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) + let mp = Nametab.locate_module (snd (qualid_of_reference q)) in + if is_modfile mp then error_MPfile_as_mod mp true; + refs,(mp::mps) with Not_found -> (Nametab.global q)::refs, mps - in + 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; - Visit.reset (); - reset_tables () + let struc = optimize_struct refs (mono_environment refs mps) in + warning_axioms (); + print_structure_to_file (mono_filename f) struc; + reset () -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]. *) +(*s Simple extraction in the Coq toplevel. The vernacular command + is \verb!Extraction! [qualid]. *) -let extraction qid = - check_inside_section (); - check_inside_module (); +let simple_extraction qid = + init false; try - let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in - extraction_rec [qid] + let mp = Nametab.locate_module (snd (qualid_of_reference qid)) in + if is_modfile mp then error_MPfile_as_mod mp true; + full_extraction None [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 - let prm = - { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let struc = optimize_struct prm None (mono_environment [r] []) in + let struc = optimize_struct [r] (mono_environment [r] []) in let d = get_decl_in_structure r struc in + warning_axioms (); print_one_decl struc (modpath_of_r r) d; - Visit.reset (); - reset_tables () - -(*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 (); - begin match lang () with - | Toplevel -> error_toplevel () - | Scheme -> error_scheme () - | _ -> () - end; - 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 - Visit.reset (); - Visit.add_mp mp; - let env = Global.env () in - let l = List.rev (environment_until None) in - let struc = - List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) 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; - Visit.reset (); - reset_tables () + reset () (*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 (); - begin match lang () with - | Toplevel -> error_toplevel () - | Scheme -> error_scheme () - | _ -> () - end; - let dir_m = dir_module_of_id m in - Visit.reset (); + init true; + let dir_m = + let q = make_short_qualid m in + try Nametab.full_name_module q with Not_found -> error_unknown_module q + in Visit.add_mp (MPfile dir_m); let env = Global.env () in let l = List.rev (environment_until (Some dir_m)) in let select l (mp,meb) = if Visit.needed_mp mp - then (mp, unpack (extract_meb env (Some mp) true meb)) :: l + then (mp, unpack (extract_seb env (Some mp) true meb)) :: l else l in let struc = List.fold_left select [] l in - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let struc = optimize_struct dummy_prm None struc in + let struc = optimize_struct [] struc in + warning_axioms (); + record_contents_fstlev struc; 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_structure_to_file (module_filename short_m) [e]; print l | _ -> assert false in print struc; - Visit.reset (); - reset_tables () - - - - - + reset () |