Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 444 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
deleted file mode 100644
index 73f44e68..00000000
--- a/contrib/extraction/common.ml
+++ /dev/null
@@ -1,444 +0,0 @@
-(************************************************************************)
-(*  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: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*)
-
-open Pp
-open Util
-open Names
-open Term
-open Declarations
-open Nameops
-open Libnames
-open Table
-open Miniml
-open Mlutil
-open Modutil
-open Mod_subst
-
-let string_of_id id = ascii_of_ident (Names.string_of_id id)
-
-(*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 dottify = function
-  | [] -> assert false
-  | [s] -> s
-  | s::[""] -> s
-  | s::l -> (dottify l)^"."^s
-
-(*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_ident 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 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: 
-  [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either 
-  be a [MPdot] over the last entry, or something new, mainly 
-  [MPself], or [MPfile] at the beginning.
-
-  - The [content] part is used to recoard all the names already
-  seen at this level.
-  
-  - The [subst] part is here mainly for printing signature
-  (in which names are still short, i.e. relative to a [msid]).
-*)
-
-type visible_layer = { mp : module_path;
-		       content : ((kind*string),unit) Hashtbl.t }
-
-let pop_visible, push_visible, get_visible, subst_mp =
-  let vis = ref [] and sub = ref [empty_subst] in
-  register_cleanup (fun () -> vis := []; sub := [empty_subst]);
-  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;
-    sub := List.tl !sub
-  and push mp o =
-    vis := { mp = mp; content = Hashtbl.create 97 } :: !vis;
-    let s = List.hd !sub in
-    let s = match o with None -> s | Some msid -> add_msid msid mp s in
-    sub := s :: !sub
-  and get () = !vis
-  and subst mp = subst_mp (List.hd !sub) mp
-  in (pop,push,get,subst)
-
-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 = Hashtbl.add (top_visible ()).content ks ()
-
-(* 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 (subst_mp 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
-  | MPself msid -> [modular_rename Mod (id_of_msid msid)]
-  | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)]
-  | 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 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 = subst_mp (modpath_of_r r) in
-  let l = mp_renaming mp 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_id_of_global r)) globs in
-      string_of_id id
-    else modular_rename k (safe_id_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 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 visible_clash mp0 ks =
-  let rec clash = function
-    | [] -> false
-    | v :: _ when v.mp = mp0 -> false
-    | v :: _ when Hashtbl.mem v.content ks -> true
-    | _ :: vis -> 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. 
-   Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
-
-let pp_gen k mp ls olab =
-  try (* what is the largest prefix of [mp] that belongs to [visible]? *)
-    let prefix = common_prefix_from_list mp (get_visible_mps ()) in
-    let delta = mp_length mp - mp_length prefix in
-    assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
-    let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in
-    let s,ls' = list_sep_last ls in
-    (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>].
-       Difficulty: in ocaml the prefix part cannot be used for
-       qualification (we are inside it) and the rest of the long
-       name may be hidden. 
-       Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
-    let k' = if ls' = [] then k else Mod in
-    if visible_clash prefix (k',s) then
-      let front = if ls' = [] && k <> Mod then [s] else ls' in
-      let lab = (* label associated with s *)
-	if delta = 0 && k <> Mod then Option.get olab
-	else get_nth_label_mp delta mp
-      in
-      try dottify (front @ [check_duplicate prefix lab])
-      with Not_found ->
-	assert (get_phase () = Pre); (* otherwise it's too late *)
-	add_duplicate prefix lab; dottify ls
-    else dottify ls
-  with Not_found ->
-    (* [mp] belongs to a closed module, not one of [visible]. *)
-    let base = base_mp mp in
-    let base_s,ls1 = list_sep_last ls in
-    let s,ls2 = list_sep_last ls1 in
-    (* [List.rev ls] is [base_s :: s :: List.rev ls2] *)
-    let k' = if ls2 = [] then k else Mod 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 ls1
-    else if visible_clash base (Mod,base_s) then
-      error_module_clash base_s
-    else dottify ls
-
-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 = subst_mp (modpath_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); unquote s)
-  else match lang () with
-    | Scheme -> unquote s (* no modular Scheme extraction... *)
-    | Haskell -> if modular () then dottify ls else s
-	(* for the moment we always qualify in modular Haskell... *)
-    | Ocaml -> pp_gen k mp ls (Some (label_of_r r))
-
-(* The next function is used only in Ocaml extraction...*)
-let pp_module mp =
-  let mp = subst_mp mp in
-  let ls = mp_renaming mp in
-  if List.length ls = 1 then dottify ls
-  else match mp with
-    | MPdot (mp0,_) 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); s
-    | _ -> pp_gen Mod mp ls None
-
-