From 90b61424761c5ba1ddbecf20c29d78b485584ae7 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Mon, 12 Dec 2016 14:18:48 +0100 Subject: Extend Fast_typeops to be a replacement for Typeops This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors. --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a980a43f5..33fab74e1 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 (* FIXME constraints *) (match flag_of_type env typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> -- cgit v1.2.3 From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Sat, 28 Jan 2017 14:11:50 +0100 Subject: Remove useless comments --- kernel/typeops.mli | 8 -------- plugins/extraction/extraction.ml | 2 +- 2 files changed, 1 insertion(+), 9 deletions(-) (limited to 'plugins/extraction') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 73c63db68..007acae60 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,8 +98,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(* val type_of_constant : env -> pconstant -> types constrained *) - val type_of_constant_type : env -> constant_type -> types val type_of_projection_constant : env -> Names.projection puniverses -> types @@ -112,9 +107,6 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -(* val type_of_constant_knowing_parameters : *) -(* env -> pconstant -> types Lazy.t array -> types constrained *) - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 33fab74e1..2b19c2805 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_in env c in (* FIXME constraints *) + 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) -> -- cgit v1.2.3 From 5484ba750ef4526dde29ffc1474ca5d145f3ec04 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 4 Feb 2017 01:01:05 +0100 Subject: Extraction: fix complexity issue #5310 A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017... --- plugins/extraction/ocaml.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 1c29a9bc2..5d10cb939 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -618,12 +618,13 @@ let rec pp_specif = function with Not_found -> pp_spec s) | (l,Smodule mt) -> let def = pp_module_type [] mt in - 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 - fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def') + fnl () ++ + hov 1 (str ("module "^ren^" :") ++ spc () ++ + str "module type of struct include " ++ name ++ str " end") with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> let def = pp_module_type [] mt in -- cgit v1.2.3 From af4962a9211a707943e7b0627439a731c3e7d23f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 4 Feb 2017 19:29:15 +0100 Subject: Extraction : get_duplicates (via option) instead of check_duplicates (via Not_found) This clarifies the execution flow --- plugins/extraction/common.ml | 16 ++++++++------- plugins/extraction/common.mli | 2 +- plugins/extraction/ocaml.ml | 45 ++++++++++++++++++++----------------------- 3 files changed, 31 insertions(+), 32 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9446cf667..de97ba97c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -308,15 +308,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 +511,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 2f5601964..b8e95afb3 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/ocaml.ml b/plugins/extraction/ocaml.ml index 5d10cb939..31e481d12 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -610,30 +610,29 @@ let pp_alias_spec ren = function 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) + pp_alias_spec ren s) | (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 -> @@ -682,12 +681,12 @@ 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) + pp_alias_decl ren d) | (l,SEmodule m) -> let typ = (* virtual printing of the type, in order to have a correct mli later*) @@ -700,18 +699,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 -- cgit v1.2.3 From 8ef3bc0e8a65b3a0338da39aa54cd75b1c2c1bb7 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 4 Feb 2017 19:55:18 +0100 Subject: Extraction: simplify the generated code for difficult name conflicts No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely) --- plugins/extraction/ocaml.ml | 33 ++------------------------------- 1 file changed, 2 insertions(+), 31 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 31e481d12..404939cff 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -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,16 +579,6 @@ 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) -> @@ -615,7 +587,7 @@ let rec pp_specif = function | Some ren -> hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ - pp_alias_spec ren 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 @@ -685,8 +657,7 @@ let rec pp_structure_elem = function | 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) + 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*) -- cgit v1.2.3 From 69c4e7cfa0271f024b2178082e4be2e3ca3be263 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 5 Feb 2017 01:46:41 +0100 Subject: Extraction: avoid deprecated functions of module String - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co --- plugins/extraction/common.ml | 13 ++++++++----- plugins/extraction/common.mli | 3 +++ plugins/extraction/haskell.ml | 4 ++-- plugins/extraction/scheme.ml | 7 +------ plugins/extraction/table.ml | 11 ++++++----- 5 files changed, 20 insertions(+), 18 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index de97ba97c..b93a76b96 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -92,9 +92,11 @@ 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 + let b = Bytes.of_string s in + for i=0 to Bytes.length b - 1 do + if Bytes.get b i == '\'' then Bytes.set b i '~' + done; + Bytes.to_string b let rec qualify delim = function | [] -> assert false @@ -110,12 +112,13 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id)) +let lowercase_id id = + Id.of_string (String.uncapitalize_ascii (ascii_of_id id)) let uppercase_id id = let s = ascii_of_id id in assert (not (String.is_empty s)); if s.[0] == '_' then Id.of_string ("Coq_"^s) - else Id.of_string (String.capitalize s) + else Id.of_string (String.capitalize_ascii s) type kind = Term | Type | Cons | Mod diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index b8e95afb3..a6351fc4c 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -36,6 +36,9 @@ val pr_binding : Id.t list -> std_ppcmds val rename_id : Id.t -> Id.Set.t -> Id.t +(** For Scheme extraction, replace the ['] by [~] *) +val unquote : string -> string + type env = Id.t list * Id.Set.t val empty_env : unit -> env diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0692c88cd..83bb2e135 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -21,8 +21,8 @@ open Common (*s Haskell renaming issues. *) -let pr_lower_id id = str (String.uncapitalize (Id.to_string id)) -let pr_upper_id id = str (String.capitalize (Id.to_string id)) +let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id)) +let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id)) let keywords = List.fold_right (fun s -> Id.Set.add (Id.of_string s)) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index a6309e61f..3bd16138f 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -39,12 +39,7 @@ let preamble _ comment _ usf = str "(load \"macros_extr.scm\")\n\n" ++ (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 +let pr_id id = str (unquote (Id.to_string id)) let paren = pp_par true diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 5e7d810c9..a8d49ffda 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -55,7 +55,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) + | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let is_toplevel mp = @@ -773,13 +773,14 @@ 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 + let s = Bytes.of_string (string_of_modfile mp) in + let () = Bytes.set s 0 (s0.[0]) in + Bytes.to_string s let add_blacklist_entries l = blacklist_table := - List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s))) + List.fold_right + (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s))) l !blacklist_table (* Registration of operations for rollback. *) -- cgit v1.2.3 From 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 5 Feb 2017 02:01:56 +0100 Subject: Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore --- plugins/extraction/extract_env.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 52f22ee60..e019bb3c2 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -507,8 +507,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 -- cgit v1.2.3 From df14dac0e6e9d9819dcc3b1601e150af7c142597 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 5 Feb 2017 02:12:36 +0100 Subject: Extraction cosmetic: no whitespaces in printing empty modules --- plugins/extraction/ocaml.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 404939cff..d89bf95ee 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -625,8 +625,10 @@ and pp_module_type params = function 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 @@ -701,8 +703,10 @@ and pp_module_expr params = function 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 () -- cgit v1.2.3 From 3550120641c3b8d84290dc950e717aaf099775f9 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 7 Feb 2017 23:28:36 +0100 Subject: Revert "Extraction: avoid deprecated functions of module String" This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry... --- plugins/extraction/common.ml | 13 +++++-------- plugins/extraction/common.mli | 3 --- plugins/extraction/haskell.ml | 4 ++-- plugins/extraction/scheme.ml | 7 ++++++- plugins/extraction/table.ml | 11 +++++------ 5 files changed, 18 insertions(+), 20 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index b93a76b96..de97ba97c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -92,11 +92,9 @@ let begins_with_CoqXX s = let unquote s = if lang () != Scheme then s else - let b = Bytes.of_string s in - for i=0 to Bytes.length b - 1 do - if Bytes.get b i == '\'' then Bytes.set b i '~' - done; - Bytes.to_string b + let s = String.copy s in + for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done; + s let rec qualify delim = function | [] -> assert false @@ -112,13 +110,12 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = - Id.of_string (String.uncapitalize_ascii (ascii_of_id id)) +let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id)) let uppercase_id id = let s = ascii_of_id id in assert (not (String.is_empty s)); if s.[0] == '_' then Id.of_string ("Coq_"^s) - else Id.of_string (String.capitalize_ascii s) + else Id.of_string (String.capitalize s) type kind = Term | Type | Cons | Mod diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index a6351fc4c..b8e95afb3 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -36,9 +36,6 @@ val pr_binding : Id.t list -> std_ppcmds val rename_id : Id.t -> Id.Set.t -> Id.t -(** For Scheme extraction, replace the ['] by [~] *) -val unquote : string -> string - type env = Id.t list * Id.Set.t val empty_env : unit -> env diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 83bb2e135..0692c88cd 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -21,8 +21,8 @@ open Common (*s Haskell renaming issues. *) -let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id)) -let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id)) +let pr_lower_id id = str (String.uncapitalize (Id.to_string id)) +let pr_upper_id id = str (String.capitalize (Id.to_string id)) let keywords = List.fold_right (fun s -> Id.Set.add (Id.of_string s)) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 3bd16138f..a6309e61f 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -39,7 +39,12 @@ let preamble _ comment _ usf = str "(load \"macros_extr.scm\")\n\n" ++ (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) -let pr_id id = str (unquote (Id.to_string id)) +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 let paren = pp_par true diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a8d49ffda..5e7d810c9 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -55,7 +55,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f))) + | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let is_toplevel mp = @@ -773,14 +773,13 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = Bytes.of_string (string_of_modfile mp) in - let () = Bytes.set s 0 (s0.[0]) in - Bytes.to_string s + let s = String.copy (string_of_modfile mp) in + if s.[0] != s0.[0] then s.[0] <- s0.[0]; + s let add_blacklist_entries l = blacklist_table := - List.fold_right - (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s))) + List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s))) l !blacklist_table (* Registration of operations for rollback. *) -- cgit v1.2.3