1 files changed, 535 insertions, 0 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
new file mode 100644
index 00000000..1db1c786
--- /dev/null
+++ b/plugins/extraction/common.ml
@@ -0,0 +1,535 @@
+(************************************************************************)
+(*  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$ i*)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Namegen
+open Nameops
+open Libnames
+open Table
+open Miniml
+open Mlutil
+open Modutil
+open Mod_subst
+
+let string_of_id id =
+  let s = Names.string_of_id id in
+  for i = 0 to String.length s - 2 do
+    if s.[i] = '_' && s.[i+1] = '_' then warning_id s
+  done;
+  ascii_of_ident s
+
+let is_mp_bound = function MPbound _ -> true | _ -> false
+
+(*s Some pretty-print utility functions. *)
+
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+
+let pp_apply st par args = match args with
+  | [] -> st
+  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+
+let pr_binding = function
+  | [] -> mt ()
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+
+let fnl2 () = fnl () ++ fnl ()
+
+let space_if = function true -> str " " | false -> mt ()
+
+let sec_space_if = function true -> spc () | false -> mt ()
+
+let is_digit = function
+  | '0'..'9' -> true
+  | _ -> false
+
+let begins_with_CoqXX s =
+  let n = String.length s in
+  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*)
+    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
+  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 rec qualify delim = function
+  | [] -> assert false
+  | [s] -> s
+  | ""::l -> qualify delim l
+  | s::l -> s^delim^(qualify delim l)
+
+let dottify = qualify "."
+let pseudo_qualify = qualify "__"
+
+(*s Uppercase/lowercase renamings. *)
+
+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 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)
+
+type kind = Term | Type | Cons | Mod
+
+let upperkind = function
+  | Type -> lang () = Haskell
+  | Term -> false
+  | Cons | Mod -> true
+
+let kindcase_id k id =
+  if upperkind k then uppercase_id id else lowercase_id id
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.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
+
+let rec rename_vars avoid = function
+  | [] ->
+      [], avoid
+  | id :: idl when id == dummy_name ->
+      (* we don't rename dummy binders *)
+      let (idl', avoid') = rename_vars avoid idl in
+      (id :: idl', avoid')
+  | 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)
+
+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
+	(id :: idl, avoid) in
+  fst (rename avoid l)
+
+let push_vars ids (db,avoid) =
+  let ids',avoid' = rename_vars avoid ids in
+  ids', (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
+
+
+(*S Renamings of global objects. *)
+
+(*s Tables of global renamings *)
+
+let register_cleanup, do_cleanup =
+  let funs = ref [] in
+  (fun f -> funs:=f::!funs), (fun () -> List.iter (fun f -> f ()) !funs)
+
+type phase = Pre | Impl | Intf
+
+let set_phase, get_phase =
+  let ph = ref Impl in ((:=) ph), (fun () -> !ph)
+
+let set_keywords, get_keywords =
+  let k = ref Idset.empty in
+  ((:=) k), (fun () -> !k)
+
+let add_global_ids, get_global_ids =
+  let ids = ref Idset.empty in
+  register_cleanup (fun () -> ids := get_keywords ());
+  let add s = ids := Idset.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.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+
+(* A table recording objects in the first level of all MPfile *)
+
+let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
+  mktable false
+
+(*s The list of external modules that will be opened initially *)
+
+let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
+  let m = ref MPset.empty in
+  let add mp = m:=MPset.add mp !m
+  and mem mp = MPset.mem mp !m
+  and list () = MPset.elements !m
+  and clear () = m:=MPset.empty
+  in
+  register_cleanup clear;
+  (add,mem,list,clear)
+
+(*s List of module parameters that we should alpha-rename *)
+
+let params_ren_add, params_ren_mem =
+  let m = ref MPset.empty in
+  let add mp = m:=MPset.add mp !m
+  and mem mp = MPset.mem mp !m
+  and clear () = m:=MPset.empty
+  in
+  register_cleanup clear;
+  (add,mem)
+
+(*s table indicating the visible horizon at a precise moment,
+    i.e. the stack of structures we are inside.
+
+  - The sequence of [mp] parts should have the following form:
+  a [MPfile] at the beginning, and then more and more [MPdot]
+  over this [MPfile], or [MPbound] when inside the type of a
+  module parameter.
+
+  - the [params] are the [MPbound] when [mp] is a functor,
+    the innermost [MPbound] coming first in the list.
+
+  - The [content] part is used to record all the names already
+  seen at this level.
+*)
+
+type visible_layer = { mp : module_path;
+		       params : module_path list;
+		       content : ((kind*string),label) Hashtbl.t }
+
+let pop_visible, push_visible, get_visible =
+  let vis = ref [] in
+  register_cleanup (fun () -> vis := []);
+  let pop () =
+    let v = List.hd !vis in
+    (* we save the 1st-level-content of MPfile for later use *)
+    if get_phase () = Impl && modular () && is_modfile v.mp
+    then add_mpfiles_content v.mp v.content;
+    vis := List.tl !vis
+  and push mp mps =
+    vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !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
+
+(* table of local module wrappers used to provide non-ambiguous names *)
+
+let add_duplicate, check_duplicate =
+  let index = ref 0 and dups = ref Gmap.empty in
+  register_cleanup (fun () -> index := 0; dups := Gmap.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
+  in (add,check)
+
+type reset_kind = AllButExternal | Everything
+
+let reset_renaming_tables flag =
+  do_cleanup ();
+  if flag = Everything then clear_mpfiles_content ()
+
+(*S Renaming functions *)
+
+(* This function creates from [id] a correct uppercase/lowercase identifier.
+   This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes
+   with previous [Coq_id] variable, these prefixes are duplicated if already
+   existing. *)
+
+let modular_rename k id =
+  let s = string_of_id id in
+  let prefix,is_ok =
+    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)
+  then prefix ^ s
+  else s
+
+(*s For monolithic extraction, first-level modules might have to be renamed
+    with unique numbers *)
+
+let modfstlev_rename =
+  let add_prefixes,get_prefixes,_ = mktable true in
+  fun l ->
+    let coqid = id_of_string "Coq" in
+    let id = id_of_label l in
+    try
+      let coqset = get_prefixes id in
+      let nextcoq = next_ident_away coqid coqset in
+      add_prefixes id (nextcoq::coqset);
+      (string_of_id nextcoq)^"_"^(string_of_id id)
+    with Not_found ->
+      let s = string_of_id id in
+      if is_lower s || begins_with_CoqXX s then
+	(add_prefixes id [coqid]; "Coq_"^s)
+      else
+	(add_prefixes id []; s)
+
+(*s Creating renaming for a [module_path] : first, the real function ... *)
+
+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
+  | MPbound mbid ->
+      let s = modular_rename Mod (id_of_mbid mbid) in
+      if not (params_ren_mem mp) then [s]
+      else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
+  | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
+  | MPfile _ ->
+      assert (get_phase () = Pre);
+      let current_mpfile = (list_last (get_visible ())).mp in
+      if 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
+  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
+
+(*s Renamings creation for a [global_reference]: we build its fully-qualified
+    name in a [string list] form (head is the short name). *)
+
+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 s =
+    if l = [""] (* this happens only at toplevel of the monolithic case *)
+    then
+      let globs = Idset.elements (get_global_ids ()) in
+      let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in
+      string_of_id id
+    else modular_rename k (safe_basename_of_global r)
+  in
+  add_global_ids (id_of_string s);
+  s::l
+
+(* Cached version of the last function *)
+
+let ref_renaming =
+  let add,get,_ = mktable true in
+  fun x ->
+    try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x
+    with Not_found -> let y = ref_renaming_fun x in add x y; y
+
+(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
+   can be printed as [s] in the current context of visible
+   modules. More precisely, we check if there exists a
+   visible [mp] that contains [s].
+   The verification stops if we encounter [mp=mp0]. *)
+
+let rec clash mem mp0 ks = function
+  | [] -> false
+  | mp :: _ when 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
+    (List.rev (mpfiles_list ()))
+
+let rec params_lookup mp0 ks = function
+  | [] -> false
+  | param :: _ when mp0 = param -> true
+  | param :: params ->
+      if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param;
+      params_lookup mp0 ks params
+
+let visible_clash mp0 ks =
+  let rec clash = function
+    | [] -> false
+    | v :: _ when v.mp = mp0 -> false
+    | v :: vis ->
+	let b = Hashtbl.mem v.content ks in
+	if b && not (is_mp_bound mp0) then true
+	else begin
+	  if b then params_ren_add mp0;
+	  if params_lookup mp0 ks v.params then false
+	  else clash vis
+	end
+  in clash (get_visible ())
+
+(* Same, but with verbose output (and mp0 shouldn't be a MPbound) *)
+
+let visible_clash_dbg mp0 ks =
+  let rec clash = function
+    | [] -> None
+    | v :: _ when v.mp = mp0 -> None
+    | v :: vis ->
+	try Some (v.mp,Hashtbl.find v.content ks)
+	with Not_found ->
+	  if params_lookup mp0 ks v.params then None
+	  else clash vis
+  in clash (get_visible ())
+
+(* After the 1st pass, we can decide which modules will be opened initially *)
+
+let opened_libraries () =
+  if not (modular ()) then []
+  else
+    let used = mpfiles_list () in
+    let rec check_elsewhere avoid = function
+      | [] -> []
+      | mp :: mpl ->
+	  let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in
+	  if List.exists clash avoid
+	  then check_elsewhere avoid mpl
+	  else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl
+    in
+    let opened = check_elsewhere [] used in
+    mpfiles_clear ();
+    List.iter mpfiles_add opened;
+    opened
+
+(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
+
+(* First, a function that factorize the printing of both [global_reference]
+   and module names for ocaml. When [k=Mod] then [olab=None], otherwise it
+   contains the label of the reference to print.
+   [rls] is the string list giving the qualified name, short name at the end.
+   Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *)
+
+(* In Coq, we can qualify [M.t] even if we are inside [M], but in Ocaml we
+   cannot do that. So, if [t] gets hidden and we need a long name for it,
+   we duplicate the _definition_ of t in a Coq__XXX module, and similarly
+   for a sub-module [M.N] *)
+
+let pp_duplicate k' prefix mp rls olab =
+  let rls', lbl =
+    if k'<>Mod then
+      (* Here rls=[s], the ref to print is <prefix>.<s>, and olab<>None *)
+      rls, Option.get olab
+    else
+      (* 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
+
+let fstlev_ks k = function
+  | [] -> assert false
+  | [s] -> k,s
+  | s::_ -> Mod,s
+
+(* [pp_ocaml_local] : [mp] has something in common with [top_visible ()]
+   but isn't equal to it *)
+
+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
+  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'
+  else pp_duplicate (fst k's) prefix mp rls' olab
+
+(* [pp_ocaml_bound] : [mp] starts with a [MPbound], and we are not inside
+   (i.e. we are not printing the type of the module parameter) *)
+
+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));
+  dottify rls
+
+(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
+
+let pp_ocaml_extern k base rls = match rls with
+  | [] | [_] -> assert false
+  | base_s :: rls' ->
+      let k's = fstlev_ks k rls' in
+      if modular () && (mpfiles_mem base) &&
+	(not (mpfiles_clash base k's)) &&
+	(not (visible_clash base k's))
+      then (* Standard situation of an object in another file: *)
+	(* Thanks to the "open" of this file we remove its name *)
+	dottify rls'
+      else match visible_clash_dbg base (Mod,base_s) with
+	| None -> dottify rls
+	| Some (mp,l) -> error_module_clash base (MPdot (mp,l))
+
+(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *)
+
+let pp_ocaml_gen k mp rls olab =
+  match common_prefix_from_list mp (get_visible_mps ()) with
+    | Some prefix -> pp_ocaml_local k prefix mp rls olab
+    | None ->
+	let base = base_mp mp in
+	if is_mp_bound base then pp_ocaml_bound base rls
+	else pp_ocaml_extern k base rls
+
+(* For Haskell, things are simplier: we have removed (almost) all structures *)
+
+let pp_haskell_gen k mp rls = match rls with
+  | [] -> assert false
+  | s::rls' ->
+      (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^
+	(if upperkind k then "" else "_") ^ pseudo_qualify rls'
+
+(* Main name printing function for a reference *)
+
+let pp_global k r =
+  let ls = ref_renaming (k,r) in
+  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
+    (* simpliest situation: definition of r (or use in the same context) *)
+    (* we update the visible environment *)
+    (add_visible (k,s) l; unquote s)
+  else
+    let rls = List.rev ls in (* for what come next it's easier this way *)
+    match lang () with
+      | Scheme -> unquote s (* no modular Scheme extraction... *)
+      | Haskell -> if modular () then pp_haskell_gen k mp rls else s
+      | Ocaml -> pp_ocaml_gen k mp rls (Some l)
+
+(* The next function is used only in Ocaml extraction...*)
+
+let pp_module mp =
+  let ls = mp_renaming mp in
+  match mp with
+    | MPdot (mp0,l) when 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
+	add_visible (Mod,s) l; s
+    | _ -> pp_ocaml_gen Mod mp (List.rev ls) None
+
+