diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 27 | ||||
| -rw-r--r-- | plugins/extraction/common.mli | 2 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 2 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 94 | ||||
| -rw-r--r-- | plugins/extraction/scheme.ml | 6 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 6 |
8 files changed, 61 insertions, 90 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 3c5f6cb720..fc8d5356c8 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -67,7 +67,9 @@ let pp_boxed_tuple f = function blocks is less that a line length. To avoid this awkward situation, we attach a big virtual size to [fnl] newlines. *) -let fnl () = stras (1000000,"") ++ fnl () +(* EG: This looks quite suspicious... but beware of bugs *) +(* let fnl () = stras (1000000,"") ++ fnl () *) +let fnl () = fnl () let fnl2 () = fnl () ++ fnl () @@ -91,10 +93,7 @@ let begins_with_CoqXX s = let unquote s = if lang () != Scheme then s - else - let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done; - s + else String.map (fun c -> if c == '\'' then '~' else c) s let rec qualify delim = function | [] -> assert false @@ -145,7 +144,7 @@ type env = Id.t list * Id.Set.t (*s Generic renaming issues for local variable names. *) let rec rename_id id avoid = - if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id + if Id.Set.mem id avoid then rename_id (increment_subscript id) avoid else id let rec rename_vars avoid = function | [] -> @@ -308,15 +307,16 @@ end module DupMap = Map.Make(DupOrd) -let add_duplicate, check_duplicate = +let add_duplicate, get_duplicate = let index = ref 0 and dups = ref DupMap.empty in register_cleanup (fun () -> index := 0; dups := DupMap.empty); let add mp l = incr index; let ren = "Coq__" ^ string_of_int !index in dups := DupMap.add (mp,l) ren !dups - and check mp l = DupMap.find (mp, l) !dups - in (add,check) + and get mp l = + try Some (DupMap.find (mp, l) !dups) with Not_found -> None + in (add,get) type reset_kind = AllButExternal | Everything @@ -510,10 +510,11 @@ let pp_duplicate k' prefix mp rls olab = (* Here rls=s::rls', we search the label for s inside mp *) List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp in - try dottify (check_duplicate prefix lbl :: rls') - with Not_found -> - assert (get_phase () == Pre); (* otherwise it's too late *) - add_duplicate prefix lbl; dottify rls + match get_duplicate prefix lbl with + | Some ren -> dottify (ren :: rls') + | None -> + assert (get_phase () == Pre); (* otherwise it's too late *) + add_duplicate prefix lbl; dottify rls let fstlev_ks k = function | [] -> assert false diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 2f5601964e..b8e95afb38 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit -val check_duplicate : module_path -> Label.t -> string +val get_duplicate : module_path -> Label.t -> string option type reset_kind = AllButExternal | Everything diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 52f22ee603..2b12462ad5 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -472,13 +472,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 +508,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 +519,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 +535,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) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a980a43f53..2b19c2805f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -258,7 +258,7 @@ let rec extract_type env db j c args = | Const (kn,u as c) -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ,_ = Typeops.type_of_constant env c in + let typ = Typeops.type_of_constant_in env c in (match flag_of_type env typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 19fda4aead..3ed959cf2c 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -12,9 +12,9 @@ DECLARE PLUGIN "extraction_plugin" (* ML names *) +open Ltac_plugin open Genarg open Stdarg -open Constrarg open Pcoq.Prim open Pp open Names diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 5d10cb939d..d8e3821557 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -66,7 +66,7 @@ let pp_header_comment = function | None -> mt () | Some com -> pp_comment com ++ fnl2 () -let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl () +let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl () let pp_tdummy usf = if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt () @@ -555,24 +555,6 @@ let pp_decl = function | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) -let pp_alias_decl ren = function - | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } - | Dtype (r, l, _) -> - let name = pp_global Type r in - let l = rename_tvars keywords l in - let ids = pp_parameters l in - hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ - str (ren^".") ++ name) - | Dterm (r, a, t) -> - let name = pp_global Term r in - hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) - | Dfix (rv, _, _) -> - prvecti (fun i r -> if is_inline_custom r then mt () else - let name = pp_global Term r in - hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ - fnl ()) - rv - let pp_spec = function | Sval (r,_) when is_inline_custom r -> mt () | Stype (r,_,_) when is_inline_custom r -> mt () @@ -597,43 +579,32 @@ let pp_spec = function in hov 2 (str "type " ++ ids ++ name ++ def) -let pp_alias_spec ren = function - | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } - | Stype (r,l,_) -> - let name = pp_global Type r in - let l = rename_tvars keywords l in - let ids = pp_parameters l in - hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ - str (ren^".") ++ name) - | Sval _ -> assert false - let rec pp_specif = function | (_,Spec (Sval _ as s)) -> pp_spec s | (l,Spec s) -> - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> pp_spec s + | Some ren -> hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ - pp_alias_spec ren s - with Not_found -> pp_spec s) + str ("include module type of struct include "^ren^" end")) | (l,Smodule mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> Pp.mt () + | Some ren -> fnl () ++ hov 1 (str ("module "^ren^" :") ++ spc () ++ - str "module type of struct include " ++ name ++ str " end") - with Not_found -> Pp.mt ()) + str "module type of struct include " ++ name ++ str " end")) | (l,Smodtype mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module type "^ren^" = ") ++ name - with Not_found -> Pp.mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> Pp.mt () + | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name) and pp_module_type params = function | MTident kn -> @@ -647,15 +618,17 @@ and pp_module_type params = function push_visible mp params; let try_pp_specif l x = let px = pp_specif x in - if Pp.is_empty px then l else px::l + if Pp.ismt px then l else px::l in (* We cannot use fold_right here due to side effects in pp_specif *) let l = List.fold_left try_pp_specif [] sign in let l = List.rev l in pop_visible (); str "sig" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in let mp_mt = msid_of_mt mt in @@ -682,12 +655,11 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false let rec pp_structure_elem = function | (l,SEdecl d) -> - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> pp_decl d + | Some ren -> hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++ - fnl () ++ str "end" ++ fnl () ++ - pp_alias_decl ren d - with Not_found -> pp_decl d) + fnl () ++ str "end" ++ fnl () ++ str ("include "^ren)) | (l,SEmodule m) -> let typ = (* virtual printing of the type, in order to have a correct mli later*) @@ -700,18 +672,16 @@ let rec pp_structure_elem = function hov 1 (str "module " ++ name ++ typ ++ str " =" ++ (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module "^ren^" = ") ++ name - with Not_found -> mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name + | None -> mt ()) | (l,SEmodtype m) -> let def = pp_module_type [] m in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module type "^ren^" = ") ++ name - with Not_found -> mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> mt () + | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name) and pp_module_expr params = function | MEident mp -> pp_modname mp @@ -726,15 +696,17 @@ and pp_module_expr params = function push_visible mp params; let try_pp_structure_elem l x = let px = pp_structure_elem x in - if Pp.is_empty px then l else px::l + if Pp.ismt px then l else px::l in (* We cannot use fold_right here due to side effects in pp_structure_elem *) let l = List.fold_left try_pp_structure_elem [] sel in let l = List.rev l in pop_visible (); str "struct" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" let rec prlist_sep_nonempty sep f = function | [] -> mt () @@ -742,7 +714,7 @@ let rec prlist_sep_nonempty sep f = function | h::t -> let e = f h in let r = prlist_sep_nonempty sep f t in - if Pp.is_empty e then r + if Pp.ismt e then r else e ++ sep () ++ r let do_struct f s = diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index a6309e61f9..8d0cc4a0db 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -40,11 +40,7 @@ let preamble _ comment _ usf = (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) let pr_id id = - let s = Id.to_string id in - for i = 0 to String.length s - 1 do - if s.[i] == '\'' then s.[i] <- '~' - done; - str s + str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id) let paren = pp_par true diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ff66d915f5..d6a334c5fe 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -293,7 +293,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err ~hdr:"Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" @@ -773,9 +773,7 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = String.copy (string_of_modfile mp) in - if s.[0] != s0.[0] then s.[0] <- s0.[0]; - s + String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp) let add_blacklist_entries l = blacklist_table := |