révision du traitement des axiomes non réalisés

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

9 files changed, 40 insertions, 42 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index df1069c184..247bd137b5 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -762,15 +762,16 @@ let extract_constant env kn cb =
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) -> 
-	       if is_custom r then Dtype (r, [], Tunknown) 
-	       else error_axiom r
+	       if not (is_custom r) then warning_info_ax r; 
+	       let n = type_scheme_nb_args env typ in 
+	       let ids = iterate (fun l -> anonymous::l) n [] in 
+	       Dtype (r, ids, Taxiom) 
            | (Info,Default) -> 
-	       if is_custom r then 
-		 let t = snd (record_constant_type env kn (Some typ)) in 
-		 Dterm (r, MLexn "axiom!", type_expunge env t) 
-	       else error_axiom r
-           | (Logic,TypeScheme) -> warning_axiom r; Dtype (r, [], Tdummy)
-	   | (Logic,Default) -> warning_axiom r; Dterm (r, MLdummy, Tdummy))
+	       if not (is_custom r) then warning_info_ax r; 
+	       let t = snd (record_constant_type env kn (Some typ)) in 
+	       Dterm (r, MLaxiom, type_expunge env t) 
+           | (Logic,TypeScheme) -> warning_log_ax r; Dtype (r, [], Tdummy)
+	   | (Logic,Default) -> warning_log_ax r; Dterm (r, MLdummy, Tdummy))
     | Some body ->
 	(match flag_of_type env typ with
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 15101037b9..abe59c88e9 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -80,6 +80,7 @@ let rec pp_type par vl t =
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "()"
     | Tunknown -> str "()"
+    | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
     | Tcustom s -> str s
  in 
   hov 0 (pp_rec par t)
@@ -144,8 +145,8 @@ let rec pp_expr par env args =
 	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLcast (a,t) -> pp_expr par env args a
     | MLmagic a ->  pp_expr par env args a
+    | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
 
 and pp_pat env pv = 
   let pp_one_pat (name,ids,t) =
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 1ed396c2d6..784fc627c8 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -34,6 +34,7 @@ type ml_type =
   | Tmeta   of ml_meta (* used during ML type reconstruction *)
   | Tdummy
   | Tunknown
+  | Taxiom
   | Tcustom of string
 
 and ml_meta = { id : int; mutable contents : ml_type option }
@@ -83,7 +84,7 @@ type ml_ast =
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
   | MLdummy
-  | MLcast   of ml_ast * ml_type
+  | MLaxiom
   | MLmagic  of ml_ast
 
 (*s ML declarations. *)
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index b035d2b325..bf1b200f07 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -332,9 +332,8 @@ let ast_iter_rel f =
     | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,l) ->  List.iter (iter n) l
-    | MLcast (a,_) -> iter n a
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy -> ()
+    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
   in iter 0 
 
 (*s Map over asts. *)
@@ -348,9 +347,8 @@ let ast_map f = function
   | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
   | MLapp (a,l) -> MLapp (f a, List.map f l)
   | MLcons (c,l) -> MLcons (c, List.map f l)
-  | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -364,9 +362,8 @@ let ast_map_lift f n = function
       let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
   | MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
   | MLcons (c,l) -> MLcons (c, List.map (f n) l)
-  | MLcast (a,t) -> MLcast (f n a, t)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a	
 
 (*s Iter over asts. *) 
 
@@ -379,9 +376,8 @@ let ast_iter f = function
   | MLfix (i,ids,v) -> Array.iter f v
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (c,l) -> List.iter f l
-  | MLcast (a,t) -> f a
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -425,9 +421,8 @@ let nb_occur_match =
     | MLlam (_,a) -> nb (k+1) a
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l 
-    | MLcast (a,_) -> nb k a
     | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy -> 0
+    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
   in nb 1
 
 (*s Lifting on terms.
@@ -974,7 +969,6 @@ let rec ml_size = function
       1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
-  | MLcast (t,_) -> ml_size t
   | MLmagic t -> ml_size t
   | _ -> 0
 
@@ -1047,8 +1041,6 @@ let rec non_stricts add cand = function
 	   let cand = pop n (non_stricts add cand t) in
 	   Sort.merge (<=) cand c) [] v
 	(* [merge] may duplicates some indices, but I don't mind. *)
-  | MLcast (t,_) -> 
-      non_stricts add cand t
   | MLmagic t -> 
       non_stricts add cand t
   | _ -> 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 0ab363bc68..cd3134a7e1 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -171,7 +171,6 @@ let ast_iter_references do_term do_cons do_type a =
       | MLglob r -> do_term r
       | MLcons (r,_) -> do_cons r
       | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
-      | MLcast (_,t) -> type_iter_references do_type t 
       | _ -> ()
   in iter a
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f6d8ab04bb..4960f5a698 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -170,7 +170,7 @@ let empty_env () = [], P.globals ()
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
-    | Tmeta _ | Tvar' _ -> assert false
+    | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
 		 with _ -> (str "'a" ++ int i))
     | Tglob (r,[]) -> pp_global r
@@ -291,12 +291,11 @@ let rec pp_expr par env args =
 	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLcast (a,t) ->
-	apply (pp_par true 
-		 (pp_expr true env [] a ++ spc () ++ str ":" ++ 
-		  spc () ++ pp_type true [] t))
     | MLmagic a ->
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
+    | MLaxiom -> 
+	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
+
 	  
 and pp_record_pat (projs, args) =
    str "{ " ++
@@ -482,11 +481,14 @@ let pp_decl mpl =
 	  let l = rename_tvars keywords l in 
 	  let ids, def = try 
 	    let ids,s = find_type_custom r in 
-	    pp_string_parameters ids, str s 
-	  with not_found -> pp_parameters l, pp_type false l t
+	    pp_string_parameters ids, str "=" ++ spc () ++ str s 
+	  with not_found -> 
+	    pp_parameters l, 
+	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
+	    else str "=" ++ spc () ++ pp_type false l t
 	  in 
 	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ 
-		 spc () ++ str "=" ++ spc () ++ def)
+		 spc () ++ def)
     | Dterm (r, a, t) -> 
 	if is_inline_custom r then failwith "empty phrase"
 	else 
@@ -524,7 +526,8 @@ let pp_spec mpl =
 	    with not_found -> 
 	      let ids = pp_parameters l in 
 	      match ot with 
-		| None -> ids, mt () 
+		| None -> ids, mt ()
+		| Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" 
 		| Some t -> ids, str "=" ++ spc () ++ pp_type false l t 
 	  in 
 	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def)
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index a47607fa82..84daae82b1 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -106,10 +106,10 @@ let rec pp_expr env args =
 	paren (str "absurd")
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLcast (a,t) ->
-	pp_expr env args a
     | MLmagic a ->
 	pp_expr env args a
+    | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n")
+	
 
 and pp_one_pat env (r,ids,t) = 
   let pp_arg id = str "?" ++ pr_id id in 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index b503ba202b..96da2259d4 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -133,12 +133,13 @@ let error_axiom_scheme r i =
        pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
        str " type variable(s).") 
 
-let error_axiom r =
-  err (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_global r ++ spc () ++ str "first.")
+let warning_info_ax r =
+  Options.if_verbose msg_warning
+    (str "You must realize axiom " ++
+     pr_global r ++ str " in the extracted code.")
 
-let warning_axiom r = 
-  Options.if_verbose warn 
+let warning_log_ax r = 
+  Options.if_verbose msg_warning
     (str "This extraction depends on logical axiom" ++ spc () ++ 
      pr_global r ++ str "." ++ spc() ++ 
      str "Having false logical axiom in the environment when extracting" ++ 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 5c6029e3e1..1e8371d1e7 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -17,8 +17,8 @@ val id_of_global : global_reference -> identifier
 (*s Warning and Error messages. *)
 
 val error_axiom_scheme : global_reference -> int -> 'a
-val error_axiom : global_reference -> 'a
-val warning_axiom : global_reference -> unit
+val warning_info_ax : global_reference -> unit
+val warning_log_ax : global_reference -> unit
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a