1 files changed, 441 insertions, 0 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
new file mode 100644
index 00000000..53a2631e
--- /dev/null
+++ b/contrib/extraction/common.ml
@@ -0,0 +1,441 @@
+(************************************************************************)
+(*  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,v 1.51.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Nameops
+open Libnames
+open Table
+open Miniml
+open Modutil
+open Ocaml
+
+(*S Renamings. *)
+
+(*s Tables of global renamings *)
+
+let keywords = ref Idset.empty
+let global_ids = ref Idset.empty
+let modular = ref false
+
+(* For each [global_reference], this table will contain the different parts 
+   of its renamings, in [string list] form. *)
+let renamings = Hashtbl.create 97
+let rename r l = Hashtbl.add renamings r l
+let get_renamings r = Hashtbl.find renamings r 
+
+(* Idem for [module_path]. *)
+let mp_renamings = Hashtbl.create 97
+let mp_rename mp l = Hashtbl.add mp_renamings mp l
+let mp_get_renamings mp = Hashtbl.find mp_renamings mp 
+
+let modvisited = ref MPset.empty
+let modcontents = ref Gset.empty
+let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents
+let module_contents mp s = Gset.mem (mp,s) !modcontents
+
+let to_qualify = ref Refset.empty
+
+let mod_1st_level = ref Idmap.empty
+
+(*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
+
+(* 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 up id = 
+  let s = string_of_id id in
+  let prefix = if up then "Coq_" else "coq_" in 
+  let check = if up then is_upper else is_lower in 
+  if not (check s) ||
+    (Idset.mem id !keywords) ||
+    (String.length s >= 4 && String.sub s 0 4 = prefix) 
+  then prefix ^ s
+  else s
+
+let rename_module = modular_rename true 
+
+(* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when 
+   [mpl] is the context of visible modules. More precisely, we check if 
+   there exists a mp1, module (sub-)path of an element of [mpl], such as 
+   module [mp1-l] contains [s]. 
+   The verification stops if we encounter [mp1=mp0]. *)
+
+exception Stop 
+
+let clash mp0 l s mpl = 
+  let rec clash_one mp = match mp with
+    | _ when mp = mp0 -> raise Stop
+    | MPdot (mp',_) -> 
+	(module_contents (add_labels_mp mp l) s) || (clash_one mp') 
+    | mp when is_toplevel mp -> false
+    | _ -> module_contents (add_labels_mp mp l) s
+  in
+  let rec clash_list = function 
+    | [] -> false
+    | mp :: mpl -> (clash_one mp) || (clash_list mpl) 
+  in try clash_list mpl with Stop -> false
+
+(*s [contents_first_level mp] finds the names of the first-level objects 
+  exported by module [mp]. Nota: it might fail if [mp] isn't a directly 
+  visible module. Ex: [MPself] under functor, [MPbound], etc ... *)
+
+let contents_first_level mp = 
+  if not (MPset.mem mp !modvisited) then begin 
+    modvisited := MPset.add mp !modvisited; 
+    match (Global.lookup_module mp).mod_type with 
+      | MTBsig (msid,msb) -> 
+	  let add b id = add_module_contents mp (modular_rename b id) in 
+	  let upper_type = (lang () = Haskell) in
+	  List.iter 
+	    (function 
+	       | (l, SPBconst cb) -> 
+		   (match Extraction.constant_kind (Global.env ()) cb with 
+		      | Extraction.Logical -> () 
+		      | Extraction.Type -> add upper_type (id_of_label l)
+		      | Extraction.Term -> add false (id_of_label l))
+	       | (_, SPBmind mib) ->
+		   Array.iter 
+		     (fun mip -> if mip.mind_sort <> (Prop Null) then begin
+			add upper_type mip.mind_typename; 
+			Array.iter (add true) mip.mind_consnames
+		      end)
+		     mib.mind_packets
+	       | _ -> ())
+	    (Modops.subst_signature_msid msid mp msb)
+      | _ -> ()
+  end
+
+(*s Initial renamings creation, for modular extraction. *) 
+
+let rec mp_create_modular_renamings mp = 
+  try mp_get_renamings mp 
+  with Not_found -> 
+    let ren = match mp with 
+      | MPdot (mp,l) -> 
+	  (rename_module (id_of_label l)) :: (mp_create_modular_renamings mp)
+      | MPself msid -> [rename_module (id_of_msid msid)]
+      | MPbound mbid -> [rename_module (id_of_mbid mbid)]
+      | MPfile f -> [String.capitalize (string_of_id (List.hd (repr_dirpath f)))]
+    in mp_rename mp ren; ren
+
+
+let create_modular_renamings struc = 
+  let current_module = fst (List.hd struc) in 
+  let modfiles = ref MPset.empty in 
+  let { up = u ; down = d } = struct_get_references_set struc 
+  in 
+  (* 1) creates renamings of objects *)
+  let add upper r = 
+    let mp = modpath (kn_of_r r) in 
+    let l = mp_create_modular_renamings mp in 
+    let s = modular_rename upper (id_of_global r) in 
+    global_ids := Idset.add (id_of_string s) !global_ids;    
+    rename r (s::l); 
+    begin try 
+      let mp = modfile_of_mp mp in 
+      if mp <> current_module then modfiles := MPset.add mp !modfiles
+    with Not_found -> () 
+    end; 
+  in
+  Refset.iter (add true) u; 
+  Refset.iter (add false) d; 
+  
+  (* 2) determines the opened libraries. *)
+  let used_modules = MPset.elements !modfiles in 
+
+  (* [s] will contain all first-level sub-modules of [cur_mp] *)
+  let s = ref Stringset.empty in 
+  begin 
+    let add l = s := Stringset.add (rename_module (id_of_label l)) !s in 
+    match (Global.lookup_module current_module).mod_type with 
+      | MTBsig (_,msb) ->
+	  List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb
+      | _ -> ()
+  end;
+  (* We now compare [s] with the modules coming from [used_modules]. *)
+  List.iter 
+    (function 
+       | MPfile d -> 
+	   let s_mp = 
+	     String.capitalize (string_of_id (List.hd (repr_dirpath d))) in 
+	   if Stringset.mem s_mp !s then error_module_clash s_mp 
+	   else s:= Stringset.add s_mp !s 
+       | _ -> assert false)
+    used_modules;
+
+  (* 3) determines the potential clashes *)
+  List.iter contents_first_level used_modules; 
+  let used_modules' = List.rev used_modules in 
+  let needs_qualify r = 
+    let mp = modpath (kn_of_r r) in 
+    if (is_modfile mp) && mp <> current_module && 
+      (clash mp [] (List.hd (get_renamings r)) used_modules')
+    then to_qualify := Refset.add r !to_qualify
+  in
+  Refset.iter needs_qualify u;
+  Refset.iter needs_qualify d; 
+  used_modules
+
+(*s Initial renamings creation, for monolithic extraction. *)
+
+let begins_with_CoqXX s = 
+  (String.length s >= 4) && 
+  (String.sub s 0 3 = "Coq") &&
+  (try 
+     for i = 4 to (String.index s '_')-1 do 
+       match s.[i] with 
+	 | '0'..'9' -> () 
+	 | _ -> raise Not_found
+     done; 
+     true
+   with Not_found -> false)
+
+let mod_1st_level_rename l =
+  let coqid = id_of_string "Coq" in 
+  let id = id_of_label l in 
+  try 
+    let coqset = Idmap.find id !mod_1st_level in 
+    let nextcoq = next_ident_away coqid coqset in 
+    mod_1st_level := Idmap.add id (nextcoq::coqset) !mod_1st_level; 
+    (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
+      (mod_1st_level := Idmap.add id [coqid] !mod_1st_level; "Coq_"^s)
+    else
+      (mod_1st_level := Idmap.add id [] !mod_1st_level; s)
+
+let rec mp_create_mono_renamings mp = 
+  try mp_get_renamings mp 
+  with Not_found -> 
+    let ren = match mp with 
+       | _ when (at_toplevel mp) -> [""]
+       | MPdot (mp,l) -> 
+	   let lmp = mp_create_mono_renamings mp in
+	   if lmp = [""] then (mod_1st_level_rename l)::lmp
+	   else (rename_module (id_of_label l))::lmp
+       | MPself msid -> [rename_module (id_of_msid msid)]
+       | MPbound mbid -> [rename_module (id_of_mbid mbid)]
+       | _ -> assert false
+    in mp_rename mp ren; ren
+
+let create_mono_renamings struc = 
+  let { up = u ; down = d } = struct_get_references_list struc in 
+  let add upper r = 
+    let mp = modpath (kn_of_r r) in 
+    let l = mp_create_mono_renamings mp in
+    let mycase = if upper then uppercase_id else lowercase_id in 
+    let id = 
+      if l = [""] then 
+	next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids)
+      else id_of_string (modular_rename upper (id_of_global r))
+    in 
+    global_ids := Idset.add id !global_ids;    
+    rename r ((string_of_id id)::l) 
+  in
+  List.iter (add true) (List.rev u); 
+  List.iter (add false) (List.rev d)
+		    
+(*s Renaming issues at toplevel *)
+
+module TopParams = struct
+  let globals () = Idset.empty
+  let pp_global _ r = pr_id (id_of_global r)
+  let pp_module _ mp = str (string_of_mp mp)
+end
+
+(*s Renaming issues for a monolithic or modular extraction. *)
+
+module StdParams = struct
+
+  let globals () = !global_ids
+
+  (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *)
+
+  let rec dottify = function 
+    | [] -> assert false 
+    | [s] -> s 
+    | s::[""] -> s 
+    | s::l -> (dottify l)^"."^s
+
+  let pp_global mpl r = 
+    let ls = get_renamings r in 
+    let s = List.hd ls in 
+    let mp = modpath (kn_of_r r) in 
+    let ls = 
+      if mp = List.hd mpl then [s] (* simpliest situation *)
+      else 
+	try (* has [mp] something in common with one of those in [mpl] ? *)
+	  let pref = common_prefix_from_list mp mpl in 
+	  (*i TODO: possibilit� de clash i*)
+	  list_firstn ((mp_length mp)-(mp_length pref)+1) ls
+	with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
+	  let base = base_mp mp in 
+	  if !modular &&  
+	    (at_toplevel mp) && 
+	    not (Refset.mem r !to_qualify) && 
+	    not (clash base [] s mpl) 
+	  then snd (list_sep_last ls)
+	  else ls
+    in 
+    add_module_contents mp s; (* update the visible environment *)
+    str (dottify ls)
+
+  let pp_module mpl mp = 
+    let ls = 
+      if !modular 
+      then mp_create_modular_renamings mp 
+      else mp_create_mono_renamings mp 
+    in 
+    let ls = 
+      try (* has [mp] something in common with one of those in [mpl] ? *)
+	let pref = common_prefix_from_list mp mpl in 
+	(*i TODO: clash possible i*)
+	list_firstn ((mp_length mp)-(mp_length pref)) ls
+      with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
+	let base = base_mp mp in 
+	if !modular && (at_toplevel mp) 
+	then snd (list_sep_last ls)
+	else ls
+    in str (dottify ls) 
+
+end
+
+module ToplevelPp = Ocaml.Make(TopParams)
+module OcamlPp = Ocaml.Make(StdParams)
+module HaskellPp = Haskell.Make(StdParams)
+module SchemePp = Scheme.Make(StdParams)
+
+let pp_decl mp d = match lang () with 
+  | Ocaml -> OcamlPp.pp_decl mp d 
+  | Haskell -> HaskellPp.pp_decl mp d
+  | Scheme -> SchemePp.pp_decl mp d 
+  | Toplevel -> ToplevelPp.pp_decl mp d 
+
+let pp_struct s = match lang () with 
+  | Ocaml -> OcamlPp.pp_struct s 
+  | Haskell -> HaskellPp.pp_struct s
+  | Scheme -> SchemePp.pp_struct s
+  | Toplevel -> ToplevelPp.pp_struct s
+
+let pp_signature s = match lang () with 
+  | Ocaml -> OcamlPp.pp_signature s 
+  | Haskell -> HaskellPp.pp_signature s
+  | _ -> assert false
+
+let set_keywords () =
+  (match lang () with 
+    | Ocaml -> keywords := Ocaml.keywords
+    | Haskell -> keywords := Haskell.keywords
+    | Scheme -> keywords := Scheme.keywords
+    | Toplevel -> keywords := Idset.empty);
+  global_ids := !keywords; 
+  to_qualify := Refset.empty
+    
+let preamble prm = match lang () with 
+  | Ocaml -> Ocaml.preamble prm   
+  | Haskell -> Haskell.preamble prm
+  | Scheme -> Scheme.preamble prm
+  | Toplevel -> (fun _ _ -> mt ())
+
+let preamble_sig prm = match lang () with 
+  | Ocaml -> Ocaml.preamble_sig prm   
+  | _ -> assert false
+
+(*S Extraction of one decl to stdout. *)
+
+let print_one_decl struc mp decl = 
+  set_keywords (); 
+  modular := false; 
+  create_mono_renamings struc;
+  msgnl (pp_decl [mp] decl)
+
+(*S Extraction to a file. *)
+
+let info f = 
+  Options.if_verbose msgnl 
+    (str ("The file "^f^" has been created by extraction."))
+
+let print_structure_to_file f prm struc =
+  cons_cofix := Refset.empty;
+  Hashtbl.clear renamings;
+  mod_1st_level := Idmap.empty; 
+  modcontents := Gset.empty;
+  modvisited := MPset.empty; 
+  set_keywords ();
+  modular := prm.modular; 
+  let used_modules =
+    if lang () = Toplevel then []
+    else if prm.modular then create_modular_renamings struc
+    else (create_mono_renamings struc; [])
+  in 
+  let print_dummys =
+    (struct_ast_search MLdummy struc, 
+     struct_type_search Tdummy struc, 
+     struct_type_search Tunknown struc)
+  in
+  (* print the implementation *)
+  let cout = option_app (fun (f,_) -> open_out f) f in 
+  let ft = match cout with 
+    | None -> !Pp_control.std_ft
+    | Some cout -> Pp_control.with_output_to cout in 
+  begin try 
+    msg_with ft (preamble prm used_modules print_dummys);
+    msg_with ft (pp_struct struc);
+    option_iter close_out cout; 
+  with e -> 
+    option_iter close_out cout; raise e
+  end;
+  option_iter (fun (f,_) -> info f) f;
+  (* print the signature *)
+  match f with 
+    | Some (_,f) when lang () = Ocaml -> 
+	let cout = open_out f in
+	let ft = Pp_control.with_output_to cout in
+	begin try 
+	  msg_with ft (preamble_sig prm used_modules print_dummys);
+	  msg_with ft (pp_signature (signature_of_structure struc));
+	  close_out cout;
+	with e -> 
+	  close_out cout; raise e 
+	end; 
+	info f 
+    | _ -> ()
+	  
+
+(*i 
+  (* DO NOT REMOVE: used when making names resolution *)
+  let cout = open_out (f^".ren") in 
+  let ft = Pp_control.with_output_to cout in
+  Hashtbl.iter 
+    (fun r id -> 
+       if short_module r = !current_module then 
+	 msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r)))
+    renamings;
+  pp_flush_with ft ();
+  close_out cout;
+i*)    
+
+
+
+
+
+
+