Ca a tout pété -> Bactrack a la version d'hier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3622 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 114 insertions, 184 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index b304e0aab5..0f07658fb7 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -121,19 +121,6 @@ let contents_first_level mp =
     | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; (mp,!s)
     | _ -> mp,!s
 
-(* The previous functions might fail if [mp] isn't a directly visible module. *)
-(* Ex: [MPself] under functor, [MPbound], etc ... *)
-(* Exception [Not_found] is catched in [pp_global]. *) 
-
-let contents_first_level = 
-  let cache = ref MPmap.empty in 
-  fun mp -> 
-    try MPmap.find mp !cache 
-    with Not_found -> 
-      let res = contents_first_level mp in 
-      cache := MPmap.add mp res !cache; 
-      res
-
 let modules_first_level mp = 
   let s = ref Stringset.empty in 
   let add id = s := Stringset.add (rename_module id) !s in 
@@ -145,6 +132,15 @@ let modules_first_level mp =
     | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s
     | _ -> !s
 
+let contents_first_level = 
+  let cache = ref MPmap.empty in 
+  fun mp -> 
+    try MPmap.find mp !cache 
+    with Not_found -> 
+      let res = contents_first_level mp in 
+      cache := MPmap.add mp res !cache; 
+      res
+
 let rec clash_in_contents mp0 s = function  
   | [] -> false
   | (mp,_) :: _ when mp = mp0 -> false
@@ -229,7 +225,7 @@ let create_mono_renamings struc =
 module ToplevelParams = struct
   let globals () = Idset.empty
   let pp_global _ r = pr_global r
-  let pp_long_module _ mp = str (string_of_mp mp)
+  let pp_long_module mp = str (string_of_mp mp)
   let pp_short_module id = pr_id id
 end
 
@@ -266,29 +262,21 @@ module StdParams = struct
       if (Refset.mem r !must_qualify) || (lang () = Haskell)
       then str (string_of_ren l s)
       else 
-	try 
-	  if clash_in_contents mp s (decreasing_contents cur_mp) 
-	  then str (string_of_ren l s)
-	  else str s
-	with Not_found -> str (string_of_ren l s) 
+	if clash_in_contents mp s (decreasing_contents cur_mp) 
+	then str (string_of_ren l s)
+	else str s
     else 
       let nl = List.length l in 
       if n = nl && nl < List.length cur_l then (* strict prefix *)
-	try 
-	  if clash_in_contents mp s (decreasing_contents cur_mp) 
-	  then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
-	  else str s
-	with Not_found -> str (string_of_ren l s)
+	if clash_in_contents mp s (decreasing_contents cur_mp) 
+	then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
+	else str s
       else (* [cur_mp] and [mp] are orthogonal *)
 	let l = remove_common cur_l l 
 	in str (string_of_ren l s)
 	     
-  let pp_long_module cur_mp mp = 
-    let cur_mp = long_mp cur_mp in 
-    let cur_l = if !modular then mp_to_list cur_mp else mp_to_list' cur_mp in 
-    let mp = long_mp mp in 
-    let l = if !modular then mp_to_list mp else mp_to_list' mp in 
-    str (string_of_modlist (remove_common cur_l l))
+  let pp_long_module mp = 
+    str (string_of_modlist (if !modular then mp_to_list mp else mp_to_list' mp))
 
   let pp_short_module id = str (rename_module id)
 end
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 325e2c8c5e..ab798eebfc 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -424,29 +424,7 @@ let extraction_module m =
 	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
 	let l = environment_until (Some dir_m) in 
 	init_env l;
-(* TEMPORARY: make Extraction Module look like Recursive Extraction Module *)
-	let struc = 
-	  let select l (mp,meb) = 
-	    if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l
-	  in List.fold_left select [] (List.rev l)
-	in 
-	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-	let struc = optimize_struct dummy_prm None struc in 
-	let rec print = function 
-	  | [] -> () 
-	  | (MPfile dir, _) :: l when dir <> dir_m -> print l 
-	  | (MPfile dir, sel) as e :: l -> 
-	      let short_m = snd (split_dirpath dir) in
-	      let f = module_file_name short_m in 
-	      let prm = {modular=true;mod_name=short_m;to_appear=[]} in
-	      print_structure_to_file (Some f) prm [e]; 
-	      print l 
-	  | _ -> assert false
-	in print struc; 
-	reset_tables ()
-
-
-(*i	let mp,meb = list_last l in 
+	let mp,meb = list_last l in 
 	let struc = [mp, unpack (extract_meb v true meb)] in 
 	let extern_decls = 
 	  let filter kn l = 
@@ -457,8 +435,6 @@ let extraction_module m =
 	let struc = optimize_struct prm (Some extern_decls) struc in 
 	print_structure_to_file (Some (module_file_name m)) prm struc; 
 	reset_tables ()
-i*)
-
 	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 873c5d8fff..b3038aa4ae 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -185,30 +185,26 @@ let rec extract_type env db j c args =
     | Const kn -> 
 	let kn = long_kn kn in 
 	let r = ConstRef kn in 
-	let cb = lookup_constant kn env in 
-	let typ = cb.const_type in 
-	(match flag_of_type env typ with 
-	   | (Info, TypeScheme) -> 
-	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
-	       (match cb.const_body with 
-		  | None -> mlt
-		  | Some _ when is_custom r -> mlt 
-		  | Some lbody -> 
-		      let newc = applist (Declarations.force lbody, args) in 
-		      let mlt' = extract_type env db j newc [] in 
-		      (* ML type abbreviations interact badly with Coq *)
-		      (* reduction, so [mlt] and [mlt'] might be different: *)
-		      (* The more precise is [mlt'], extracted after reduction *)
-		      (* The shortest is [mlt], which use abbreviations *)
-		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if type_eq (mlt_env env) mlt mlt' then mlt else mlt')
-	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	       (match cb.const_body with 
-		  | None -> Tunknown (* Brutal approximation ... *)
-		  | Some lbody -> 
-		     (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in 
-		      extract_type env db j newc []))
+	if is_custom r then Tglob (r,[])
+	else if is_axiom env kn then 
+	  (* There are two kinds of informative axioms here, *)
+	  (* - the types that should be realized via [Extract Constant] *)
+	  (* - the type schemes that are not realizable (yet). *) 
+	  (* TODO: in modular extraction, we should try not to fail here !!! *)
+	  if args = [] then Tglob (r,[]) else error_axiom_scheme r
+	else 
+	  let body = constant_value env kn in 
+	  let mlt1 = extract_type env db j (applist (body, args)) [] in 
+	  (match mlt_env env r with 
+	     | Some mlt ->
+		 if mlt = Tdummy then Tdummy
+		 else 
+		   let s = type_sign env (constant_type env kn) in 
+		   let mlt2 = extract_type_app env db (r,s) args in 
+		   (* ML type abbreviation behave badly with respect to Coq *)
+		   (* reduction. Try to find the shortest correct answer. *) 
+		   if type_eq (mlt_env env) mlt1 mlt2 then mlt2 else mlt1
+	     | None -> mlt1)
     | Ind ((kn,i) as ip) ->
 	let kn = long_kn kn in
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in  
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 3b255a4404..235847f323 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -141,7 +141,7 @@ type ml_signature = (module_path * ml_module_sig) list
 module type Mlpp_param = sig
   val globals : unit -> Idset.t
   val pp_global : module_path -> global_reference -> std_ppcmds
-  val pp_long_module : module_path -> module_path -> std_ppcmds
+  val pp_long_module : module_path -> std_ppcmds
   val pp_short_module : identifier -> std_ppcmds
 end
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1892d6e952..f7a07f5816 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -65,8 +65,6 @@ let space_if = function true -> str " " | false -> mt ()
 
 let sec_space_if = function true -> spc () | false -> mt ()
 
-let fnl2 () = fnl () ++ fnl () 
-
 (*s Generic renaming issues. *)
 
 let rec rename_id id avoid = 
@@ -346,7 +344,7 @@ and pp_fix par env i (ids,bl) args =
 
 let pp_val e typ = 
   str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ 
-  str " **)"  ++ fnl2 ()
+  str " **)"  ++ fnl () ++ fnl ()
 
 (*s Pretty-printing of [Dfix] *)
 
@@ -357,11 +355,12 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
     if is_inline_custom r then pp_Dfix init (i+1) fix
     else 
       let e = pp_global r in
-      (if init then mt () else fnl2 ()) ++
+      (if init then mt () else fnl ()) ++
       pp_val e t.(i) ++
       str (if init then "let rec " else "and ") ++
       (if is_custom r then e ++ str " = " ++ str (find_custom r)
        else pp_function (empty_env ()) e c.(i)) ++
+      fnl () ++ 
       pp_Dfix false (i+1) fix 
 	
 (*s Pretty-printing of inductive types declaration. *)
@@ -409,7 +408,7 @@ let pp_record kn packet =
   str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
 	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) 
-  ++ str " }"
+  ++ str " }" ++ fnl () 
 
 let pp_coind ip pl = 
   let r = IndRef ip in 
@@ -417,85 +416,72 @@ let pp_coind ip pl =
   pp_parameters pl ++ pp_global r ++ str " = " ++ 
   pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t"
 
-exception Empty
-
-let pp_ind co kn ind =
-  let some = ref false in 
-  let init= ref (str "type ") in 
-  let rec pp i =  
-    if i >= Array.length ind.ind_packets then mt () 
+let rec pp_ind co first kn i ind =
+  if i >= Array.length ind.ind_packets then 
+    if first then mt () else fnl ()
+  else 
+    let ip = (kn,i) in 
+    let p = ind.ind_packets.(i) in 
+    if is_custom (IndRef (kn,i)) then pp_ind co first kn (i+1) ind
     else 
-      let ip = (kn,i) in 
-      let p = ind.ind_packets.(i) in 
-      if is_custom (IndRef (kn,i)) then pp (i+1)
-      else begin 
-	some := true; 
-	if p.ip_logical then pp_logical_ind ip p ++ pp (i+1)
-	else 
-	  let s = !init in 
-	  begin 
-	    init := (fnl () ++ str "and "); 
-	    s ++
-	    (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ())
-	    ++ pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
-	    pp (i+1)
-	  end
-      end
-  in 
-  let st = pp 0 in if !some then st else raise Empty
-	     
+      if p.ip_logical then  
+	pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind
+      else 
+	str (if first then "type " else "and ") ++
+	(if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ 
+	pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
+	fnl () ++ pp_ind co false kn (i+1) ind
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_mind kn i = 
   let kn = long_kn kn in 
   (match i.ind_info with 
-     | Singleton -> pp_singleton kn i.ind_packets.(0)
+     | Singleton -> pp_singleton kn i.ind_packets.(0) ++ fnl ()
      | Coinductive -> 
 	 let nop _ = () 
 	 and add r = cons_cofix := Refset.add (long_r r) !cons_cofix in 
 	 decl_iter_references nop add nop (Dind (kn,i)); 
-	 pp_ind true kn i
-     | Record -> pp_record kn i.ind_packets.(0)
-     | _ -> pp_ind false kn i)
-
+	 hov 0 (pp_ind true true kn 0 i) ++ fnl () 
+     | Record -> pp_record kn i.ind_packets.(0) ++ fnl () 
+     | _ -> hov 0 (pp_ind false true kn 0 i))
+  
 let pp_decl mp = 
   local_mp := mp; 
   function
     | Dind (kn,i) as d -> pp_mind kn i
     | Dtype (r, l, t) ->
-	if is_inline_custom r then raise Empty
+	if is_inline_custom r then mt () 
 	else 
 	  let l = rename_tvars keywords l in 
 	  let def = try str (find_custom r) with not_found -> pp_type false l t 
 	  in 
-	  hov 2 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ 
-		 spc () ++ str "=" ++ spc () ++ def)
+	  hov 0 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ 
+		 spc () ++ str "=" ++ spc () ++ def ++ fnl () ++ fnl ())
     | Dterm (r, a, t) -> 
-	if is_inline_custom r then raise Empty
+	if is_inline_custom r then mt () 
 	else 
 	  let e = pp_global r in 
 	  pp_val e t ++
 	  hov 0 
 	    (str "let " ++ 
-	     if is_custom r then 
-	       e ++ str " = " ++ str (find_custom r) ++ fnl () 
+	     if is_custom r then e ++ str " = " ++ str (find_custom r) ++ fnl () 
 	     else if is_projection r then e ++ str " x = x." ++ e ++ fnl () 
-	     else pp_function (empty_env ()) e a)
+	     else pp_function (empty_env ()) e a ++ fnl ()) ++ fnl ()
     | Dfix (rv,defs,typs) ->
-	pp_Dfix true 0 (rv,defs,typs)
+	hov 0 (pp_Dfix true 0 (rv,defs,typs)) ++ fnl ()
 
 let pp_spec mp = 
   local_mp := mp; 
   function 
     | Sind (kn,i) -> pp_mind kn i
     | Sval (r,t) -> 
-	if is_inline_custom r then raise Empty
+	if is_inline_custom r then mt () 
 	else 
-	  hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
-		 pp_type false [] t)
+	  hov 0 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
+		 pp_type false [] t ++ fnl () ++ fnl ())
     | Stype (r,vl,ot) -> 
-	if is_inline_custom r then raise Empty
+	if is_inline_custom r then mt () 
 	else 
 	  let l = rename_tvars keywords vl in 
 	  let def = 
@@ -505,88 +491,72 @@ let pp_spec mp =
 		| None -> mt () 
 		| Some t -> str "=" ++ spc () ++ pp_type false l t 
 	  in 
-	  hov 2 (str "type" ++ spc () ++ pp_parameters l ++ 
-		 pp_global r ++ spc () ++ def)
+	  hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
+		 pp_global r ++ spc () ++ def ++ fnl () ++ fnl ())
 
 let rec pp_structure_elem mp = function 
   | (_,SEdecl d) -> pp_decl mp d
   | (l,SEmodule m) ->
-      hov 1 
-	(str "module " ++ P.pp_short_module (id_of_label l) ++ 
-	 (match m.ml_mod_equiv with 
-	    | None -> 
-		str " :" ++ fnl () ++ 
-		pp_module_type mp m.ml_mod_type ++ fnl () ++
-		str "= " ++ fnl () ++ 
-		(match m.ml_mod_expr with 
-		   | None -> assert false (* see Jacek *)
-		   | Some me -> pp_module_expr mp me)
-	    | Some mp' -> 
-		str " = " ++ P.pp_long_module mp mp'))
+      str "module " ++ P.pp_short_module (id_of_label l) ++ 
+      (match m.ml_mod_equiv with 
+	 | None -> 
+	     str ":" ++ fnl () ++ pp_module_type m.ml_mod_type ++ fnl () ++ 
+	     str " = " ++ fnl () ++ 
+	     (match m.ml_mod_expr with 
+		| None -> failwith "TODO: if this happens, see Jacek"
+		| Some me -> pp_module_expr me ++ fnl ())
+	 | Some mp -> str " = " ++ P.pp_long_module mp ++ fnl ()) ++ fnl ()
   | (l,SEmodtype m) -> 
-      hov 1 
-	(str "module type " ++ P.pp_short_module (id_of_label l) ++
-	 str " = " ++ fnl () ++ pp_module_type mp m)
+      str "module type " ++ P.pp_short_module (id_of_label l) ++
+      str " = " ++ pp_module_type m ++ fnl () ++ fnl ()
 
-and pp_module_expr mp = function 
-  | MEident mp' -> P.pp_long_module mp mp'
+and pp_module_expr = function 
+  | MEident mp -> P.pp_long_module mp 
   | MEfunctor (mbid, mt, me) -> 
       str "functor (" ++ 
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
-      pp_module_type mp mt ++
-      str ") ->" ++ fnl () ++
-      pp_module_expr mp me
+      pp_module_type mt ++
+      str ") ->" ++
+      pp_module_expr me
   | MEapply (me, me') -> 
-      str "(" ++ pp_module_expr mp me ++ spc () ++ pp_module_expr mp me' ++ 
-      str ")"
+      str "(" ++ pp_module_expr me ++ str " (" ++ pp_module_expr me' ++ str ")"
   | MEstruct (msid, sel) -> 
-      let l = map_succeed (pp_structure_elem (MPself msid)) sel in 
       str "struct " ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
-      fnl () ++ str "end" 
+      prlist_with_sep fnl (pp_structure_elem (MPself msid)) sel ++ fnl () ++
+      str "end" 
 
-and pp_module_type mp = function 
+and pp_module_type = function 
   | MTident kn -> 
-      let mp',_,l = repr_kn kn in P.pp_long_module mp (MPdot (mp,l)) 
+      let mp,_,l = repr_kn kn in P.pp_long_module (MPdot (mp,l)) 
   | MTfunsig (mbid, mt, mt') -> 
       str "functor (" ++ 
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
-      pp_module_type mp mt ++
-      str ") ->" ++ fnl () ++
-      pp_module_type mp mt'
+      pp_module_type mt ++
+      str ") ->" ++ 
+      pp_module_type mt'
   | MTsig (msid, sign) -> 
-      let l = map_succeed (pp_specif (MPself msid)) sign in 
       str "sig " ++ fnl () ++ 
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
-      fnl () ++ str "end"
+      prlist_with_sep fnl (pp_specif (MPself msid)) sign ++ fnl () ++
+      str "end"
 
 and pp_specif mp = function 
   | (_,Spec s) -> pp_spec mp s 
   | (l,Smodule mt) -> 
-      hov 1 
-	(str "module " ++ 
-	 P.pp_short_module (id_of_label l) ++
-	 str " : " ++ fnl () ++ pp_module_type mp mt)
+      str "module " ++ 
+      P.pp_short_module (id_of_label l) ++
+      str " : " ++ pp_module_type mt ++ fnl () ++ fnl ()
   | (l,Smodtype mt) -> 
-      hov 1
-	(str "module type " ++
-	 P.pp_short_module (id_of_label l) ++
-	 str " = " ++ fnl () ++ pp_module_type mp mt)
-
-let pp_struct s =
-  let l mp sel = map_succeed (pp_structure_elem mp) sel in 
-  prlist (fun (mp,sel) -> prlist_with_sep fnl2 identity (l mp sel)) s ++ 
-  fnl2 ()
-
-let pp_signature s = 
-  let l mp sign = map_succeed (pp_specif mp) sign in 
-  prlist (fun (mp,sign) -> prlist_with_sep fnl2 identity (l mp sign)) s ++ 
-  fnl2 ()
-
-let pp_decl mp d = 
-  try pp_decl mp d with Empty -> mt () 
+      str "module type " ++
+      P.pp_short_module (id_of_label l) ++
+      str " : " ++ pp_module_type mt ++ fnl () ++ fnl ()
+
+let pp_struct =
+  prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel)
+
+let pp_signature = 
+  prlist (fun (mp,sign) -> prlist (pp_specif mp) sign)
 
 end