summaryrefslogtreecommitdiff
path: root/plugins/extraction/common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/common.ml')
-rw-r--r--plugins/extraction/common.ml203
1 files changed, 119 insertions, 84 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 558b8359..21819aa8 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,23 +9,20 @@
open Pp
open Util
open Names
-open Term
-open Declarations
open Namegen
open Nameops
open Libnames
+open Globnames
open Table
open Miniml
open Mlutil
-open Modutil
-open Mod_subst
let string_of_id id =
- let s = Names.string_of_id id in
+ let s = Names.Id.to_string id in
for i = 0 to String.length s - 2 do
- if s.[i] = '_' && s.[i+1] = '_' then warning_id s
+ if s.[i] == '_' && s.[i+1] == '_' then warning_id s
done;
- ascii_of_ident s
+ Unicode.ascii_of_ident s
let is_mp_bound = function MPbound _ -> true | _ -> false
@@ -42,7 +39,7 @@ let pp_apply st par args = match args with
(** Same as [pp_apply], but with also protection of the head by parenthesis *)
let pp_apply2 st par args =
- let par' = args <> [] || par in
+ let par' = not (List.is_empty args) || par in
pp_apply (pp_par par' st) par args
let pr_binding = function
@@ -82,20 +79,20 @@ let is_digit = function
let begins_with_CoqXX s =
let n = String.length s in
- n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+ n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' &&
let i = ref 3 in
try while !i < n do
- if s.[!i] = '_' then i:=n (*Stop*)
+ if s.[!i] == '_' then i:=n (*Stop*)
else if is_digit s.[!i] then incr i
else raise Not_found
done; true
with Not_found -> false
let unquote s =
- if lang () <> Scheme then 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;
+ for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
s
let rec qualify delim = function
@@ -112,17 +109,28 @@ 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 (string_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id))
let uppercase_id id =
let s = string_of_id id in
- assert (s<>"");
- if s.[0] = '_' then id_of_string ("Coq_"^s)
- else id_of_string (String.capitalize s)
+ assert (not (String.is_empty s));
+ if s.[0] == '_' then Id.of_string ("Coq_"^s)
+ else Id.of_string (String.capitalize s)
type kind = Term | Type | Cons | Mod
+module KOrd =
+struct
+ type t = kind * string
+ let compare (k1, s1) (k2, s2) =
+ let c = Pervasives.compare k1 k2 (** OK *) in
+ if c = 0 then String.compare s1 s2
+ else c
+end
+
+module KMap = Map.Make(KOrd)
+
let upperkind = function
- | Type -> lang () = Haskell
+ | Type -> lang () == Haskell
| Term -> false
| Cons | Mod -> true
@@ -131,12 +139,12 @@ let kindcase_id k id =
(*s de Bruijn environments for programs *)
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
(*s Generic renaming issues for local variable names. *)
let rec rename_id id avoid =
- if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
+ if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
let rec rename_vars avoid = function
| [] ->
@@ -148,14 +156,14 @@ let rec rename_vars avoid = function
| id :: idl ->
let (idl, avoid) = rename_vars avoid idl in
let id = rename_id (lowercase_id id) avoid in
- (id :: idl, Idset.add id avoid)
+ (id :: idl, Id.Set.add id avoid)
let rename_tvars avoid l =
let rec rename avoid = function
| [] -> [],avoid
| id :: idl ->
let id = rename_id (lowercase_id id) avoid in
- let idl, avoid = rename (Idset.add id avoid) idl in
+ let idl, avoid = rename (Id.Set.add id avoid) idl in
(id :: idl, avoid) in
fst (rename avoid l)
@@ -165,7 +173,7 @@ let push_vars ids (db,avoid) =
let get_db_name n (db,_) =
let id = List.nth db (pred n) in
- if id = dummy_name then id_of_string "__" else id
+ if Id.equal id dummy_name then Id.of_string "__" else id
(*S Renamings of global objects. *)
@@ -182,37 +190,44 @@ let set_phase, get_phase =
let ph = ref Impl in ((:=) ph), (fun () -> !ph)
let set_keywords, get_keywords =
- let k = ref Idset.empty in
+ let k = ref Id.Set.empty in
((:=) k), (fun () -> !k)
let add_global_ids, get_global_ids =
- let ids = ref Idset.empty in
+ let ids = ref Id.Set.empty in
register_cleanup (fun () -> ids := get_keywords ());
- let add s = ids := Idset.add s !ids
+ let add s = ids := Id.Set.add s !ids
and get () = !ids
in (add,get)
let empty_env () = [], get_global_ids ()
-let mktable autoclean =
- let h = Hashtbl.create 97 in
- if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
- (Hashtbl.replace h, Hashtbl.find h, fun () -> Hashtbl.clear h)
-
(* We might have built [global_reference] whose canonical part is
inaccurate. We must hence compare only the user part,
hence using a Hashtbl might be incorrect *)
+let mktable_id autoclean =
+ let m = ref Id.Map.empty in
+ let clear () = m := Id.Map.empty in
+ if autoclean then register_cleanup clear;
+ (fun r v -> m := Id.Map.add r v !m), (fun r -> Id.Map.find r !m), clear
+
let mktable_ref autoclean =
let m = ref Refmap'.empty in
let clear () = m := Refmap'.empty in
if autoclean then register_cleanup clear;
(fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
+let mktable_modpath autoclean =
+ let m = ref MPmap.empty in
+ let clear () = m := MPmap.empty in
+ if autoclean then register_cleanup clear;
+ (fun r v -> m := MPmap.add r v !m), (fun r -> MPmap.find r !m), clear
+
(* A table recording objects in the first level of all MPfile *)
let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
- mktable false
+ mktable_modpath false
let get_mpfiles_content mp =
try get_mpfiles_content mp
@@ -258,7 +273,7 @@ let params_ren_add, params_ren_mem =
type visible_layer = { mp : module_path;
params : module_path list;
- content : ((kind*string),label) Hashtbl.t }
+ mutable content : Label.t KMap.t; }
let pop_visible, push_visible, get_visible =
let vis = ref [] in
@@ -269,35 +284,47 @@ let pop_visible, push_visible, get_visible =
| v :: vl ->
vis := vl;
(* we save the 1st-level-content of MPfile for later use *)
- if get_phase () = Impl && modular () && is_modfile v.mp
+ if get_phase () == Impl && modular () && is_modfile v.mp
then add_mpfiles_content v.mp v.content
and push mp mps =
- vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
+ vis := { mp = mp; params = mps; content = KMap.empty } :: !vis
and get () = !vis
in (pop,push,get)
let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
let top_visible_mp () = (top_visible ()).mp
-let add_visible ks l = Hashtbl.add (top_visible ()).content ks l
+let add_visible ks l =
+ let visible = top_visible () in
+ visible.content <- KMap.add ks l visible.content
(* table of local module wrappers used to provide non-ambiguous names *)
+module DupOrd =
+struct
+ type t = ModPath.t * Label.t
+ let compare (mp1, l1) (mp2, l2) =
+ let c = Label.compare l1 l2 in
+ if Int.equal c 0 then ModPath.compare mp1 mp2 else c
+end
+
+module DupMap = Map.Make(DupOrd)
+
let add_duplicate, check_duplicate =
- let index = ref 0 and dups = ref Gmap.empty in
- register_cleanup (fun () -> index := 0; dups := Gmap.empty);
+ 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 := Gmap.add (mp,l) ren !dups
- and check mp l = Gmap.find (mp, l) !dups
+ 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)
type reset_kind = AllButExternal | Everything
let reset_renaming_tables flag =
do_cleanup ();
- if flag = Everything then clear_mpfiles_content ()
+ if flag == Everything then clear_mpfiles_content ()
(*S Renaming functions *)
@@ -312,8 +339,8 @@ let modular_rename k id =
if upperkind k then "Coq_",is_upper else "coq_",is_lower
in
if not (is_ok s) ||
- (Idset.mem id (get_keywords ())) ||
- (String.length s >= 4 && String.sub s 0 4 = prefix)
+ (Id.Set.mem id (get_keywords ())) ||
+ (String.length s >= 4 && String.equal (String.sub s 0 4) prefix)
then prefix ^ s
else s
@@ -321,10 +348,10 @@ let modular_rename k id =
with unique numbers *)
let modfstlev_rename =
- let add_prefixes,get_prefixes,_ = mktable true in
+ let add_prefixes,get_prefixes,_ = mktable_id true in
fun l ->
- let coqid = id_of_string "Coq" in
- let id = id_of_label l in
+ let coqid = Id.of_string "Coq" in
+ let id = Label.to_id l in
try
let coqset = get_prefixes id in
let nextcoq = next_ident_away coqid coqset in
@@ -343,23 +370,26 @@ let rec mp_renaming_fun mp = match mp with
| _ when not (modular ()) && at_toplevel mp -> [""]
| MPdot (mp,l) ->
let lmp = mp_renaming mp in
- if lmp = [""] then (modfstlev_rename l)::lmp
- else (modular_rename Mod (id_of_label l))::lmp
+ let mp = match lmp with
+ | [""] -> modfstlev_rename l
+ | _ -> modular_rename Mod (Label.to_id l)
+ in
+ mp ::lmp
| MPbound mbid ->
- let s = modular_rename Mod (id_of_mbid mbid) in
+ let s = modular_rename Mod (MBId.to_id mbid) in
if not (params_ren_mem mp) then [s]
- else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
+ else let i,_,_ = MBId.repr mbid in [s^"__"^string_of_int i]
| MPfile _ ->
assert (modular ()); (* see [at_toplevel] above *)
- assert (get_phase () = Pre);
- let current_mpfile = (list_last (get_visible ())).mp in
- if mp <> current_mpfile then mpfiles_add mp;
+ assert (get_phase () == Pre);
+ let current_mpfile = (List.last (get_visible ())).mp in
+ if not (ModPath.equal mp current_mpfile) then mpfiles_add mp;
[string_of_modfile mp]
(* ... and its version using a cache *)
and mp_renaming =
- let add,get,_ = mktable true in
+ let add,get,_ = mktable_modpath true in
fun x ->
try if is_mp_bound (base_mp x) then raise Not_found; get x
with Not_found -> let y = mp_renaming_fun x in add x y; y
@@ -370,17 +400,17 @@ and mp_renaming =
let ref_renaming_fun (k,r) =
let mp = modpath_of_r r in
let l = mp_renaming mp in
- let l = if lang () <> Ocaml && not (modular ()) then [""] else l in
+ let l = if lang () != Ocaml && not (modular ()) then [""] else l in
let s =
let idg = safe_basename_of_global r in
- if l = [""] (* this happens only at toplevel of the monolithic case *)
- then
- let globs = Idset.elements (get_global_ids ()) in
+ match l with
+ | [""] -> (* this happens only at toplevel of the monolithic case *)
+ let globs = Id.Set.elements (get_global_ids ()) in
let id = next_ident_away (kindcase_id k idg) globs in
string_of_id id
- else modular_rename k idg
+ | _ -> modular_rename k idg
in
- add_global_ids (id_of_string s);
+ add_global_ids (Id.of_string s);
s::l
(* Cached version of the last function *)
@@ -399,27 +429,30 @@ let ref_renaming =
let rec clash mem mp0 ks = function
| [] -> false
- | mp :: _ when mp = mp0 -> false
+ | mp :: _ when ModPath.equal mp mp0 -> false
| mp :: _ when mem mp ks -> true
| _ :: mpl -> clash mem mp0 ks mpl
let mpfiles_clash mp0 ks =
- clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
+ clash (fun mp k -> KMap.mem k (get_mpfiles_content mp)) mp0 ks
(List.rev (mpfiles_list ()))
let rec params_lookup mp0 ks = function
| [] -> false
- | param :: _ when mp0 = param -> true
+ | param :: _ when ModPath.equal mp0 param -> true
| param :: params ->
- if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param;
+ let () = match ks with
+ | (Mod, mp) when String.equal (List.hd (mp_renaming param)) mp -> params_ren_add param
+ | _ -> ()
+ in
params_lookup mp0 ks params
let visible_clash mp0 ks =
let rec clash = function
| [] -> false
- | v :: _ when v.mp = mp0 -> false
+ | v :: _ when ModPath.equal v.mp mp0 -> false
| v :: vis ->
- let b = Hashtbl.mem v.content ks in
+ let b = KMap.mem ks v.content in
if b && not (is_mp_bound mp0) then true
else begin
if b then params_ren_add mp0;
@@ -433,9 +466,9 @@ let visible_clash mp0 ks =
let visible_clash_dbg mp0 ks =
let rec clash = function
| [] -> None
- | v :: _ when v.mp = mp0 -> None
+ | v :: _ when ModPath.equal v.mp mp0 -> None
| v :: vis ->
- try Some (v.mp,Hashtbl.find v.content ks)
+ try Some (v.mp,KMap.find ks v.content)
with Not_found ->
if params_lookup mp0 ks v.params then None
else clash vis
@@ -455,7 +488,7 @@ let opened_libraries () =
let to_open =
List.filter
(fun mp ->
- not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks))
+ not (List.exists (fun k -> KMap.mem k (get_mpfiles_content mp)) used_ks))
used_files
in
mpfiles_clear ();
@@ -476,7 +509,7 @@ let opened_libraries () =
let pp_duplicate k' prefix mp rls olab =
let rls', lbl =
- if k'<>Mod then
+ if k' != Mod then
(* Here rls=[s], the ref to print is <prefix>.<s>, and olab<>None *)
rls, Option.get olab
else
@@ -485,7 +518,7 @@ let pp_duplicate k' prefix mp rls olab =
in
try dottify (check_duplicate prefix lbl :: rls')
with Not_found ->
- assert (get_phase () = Pre); (* otherwise it's too late *)
+ assert (get_phase () == Pre); (* otherwise it's too late *)
add_duplicate prefix lbl; dottify rls
let fstlev_ks k = function
@@ -498,8 +531,8 @@ let fstlev_ks k = function
let pp_ocaml_local k prefix mp rls olab =
(* what is the largest prefix of [mp] that belongs to [visible]? *)
- assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
- let rls' = list_skipn (mp_length prefix) rls in
+ assert (k != Mod || not (ModPath.equal mp prefix)); (* mp as whole module isn't in itself *)
+ let rls' = List.skipn (mp_length prefix) rls in
let k's = fstlev_ks k rls' in
(* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
if not (visible_clash prefix k's) then dottify rls'
@@ -510,7 +543,7 @@ let pp_ocaml_local k prefix mp rls olab =
let pp_ocaml_bound base rls =
(* clash with a MPbound will be detected and fixed by renaming this MPbound *)
- if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls));
+ if get_phase () == Pre then ignore (visible_clash base (Mod,List.hd rls));
dottify rls
(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
@@ -519,7 +552,7 @@ let pp_ocaml_extern k base rls = match rls with
| [] -> assert false
| base_s :: rls' ->
if (not (modular ())) (* Pseudo qualification with "" *)
- || (rls' = []) (* Case of a file A.v used as a module later *)
+ || (List.is_empty rls') (* Case of a file A.v used as a module later *)
|| (not (mpfiles_mem base)) (* Module not opened *)
|| (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
|| (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
@@ -549,7 +582,7 @@ let pp_haskell_gen k mp rls = match rls with
| s::rls' ->
let str = pseudo_qualify rls' in
let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
- let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
+ let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in
prf ^ str
(* Main name printing function for a reference *)
@@ -559,7 +592,7 @@ let pp_global k r =
assert (List.length ls > 1);
let s = List.hd ls in
let mp,_,l = repr_of_r r in
- if mp = top_visible_mp () then
+ if ModPath.equal mp (top_visible_mp ()) then
(* simpliest situation: definition of r (or use in the same context) *)
(* we update the visible environment *)
(add_visible (k,s) l; unquote s)
@@ -575,7 +608,7 @@ let pp_global k r =
let pp_module mp =
let ls = mp_renaming mp in
match mp with
- | MPdot (mp0,l) when mp0 = top_visible_mp () ->
+ | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) ->
(* simpliest situation: definition of mp (or use in the same context) *)
(* we update the visible environment *)
let s = List.hd ls in
@@ -587,7 +620,7 @@ let pp_module mp =
the constants are directly turned into chars *)
let mk_ind path s =
- make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
+ MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s)
let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
@@ -598,7 +631,7 @@ let check_extract_ascii () =
| Haskell -> "Char"
| _ -> raise Not_found
in
- find_custom (IndRef (ind_ascii,0)) = char_type
+ String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
with Not_found -> false
let is_list_cons l =
@@ -606,14 +639,16 @@ let is_list_cons l =
let is_native_char = function
| MLcons(_,ConstructRef ((kn,0),1),l) ->
- kn = ind_ascii && check_extract_ascii () && is_list_cons l
+ MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
| _ -> false
-let pp_native_char c =
+let get_native_char c =
let rec cumul = function
| [] -> 0
| MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
| _ -> assert false
in
let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
- str ("'"^Char.escaped (Char.chr (cumul l))^"'")
+ Char.chr (cumul l)
+
+let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 23:11:00 +0000