Revolution culturelle: suppression des arguments prop

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

5 files changed, 62 insertions, 48 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 7b997d48c..87e390116 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -96,7 +96,8 @@ and visit_ast m eenv a =
     | MLletin (_,a,b) -> visit a; visit b
     | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l
     | MLcase (a,br) -> 
-	visit a; Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br
+	visit a; 
+	Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br
     | MLfix (_,_,l) -> Array.iter visit l
     | MLcast (a,t) -> visit a; visit_type m eenv t
     | MLmagic a -> visit a
@@ -152,7 +153,8 @@ let local_optimize refs =
   optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
-  mSGNL [< 'sTR "User defined extraction:"; 'sPC; 'sTR (find_ml_extraction r) ; 'fNL>]
+  mSGNL [< 'sTR "User defined extraction:"; 
+	   'sPC; 'sTR (find_ml_extraction r) ; 'fNL>]
 
 let decl_in_r r0 = function 
   | Dglob (r,_) -> r = r0
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a16642ca7..9aecdd4c4 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -126,7 +126,7 @@ let id_of_name = function
 
 let rec list_of_ml_arrows = function
   | Tarr (Miniml.Tarity, b) -> assert false
-  | Tarr (Miniml.Tprop, b) -> list_of_ml_arrows b
+  | Tarr (Miniml.Tprop, b) -> assert false
   | Tarr (a, b) -> a :: list_of_ml_arrows b
   | t -> []
 
@@ -401,12 +401,6 @@ and extract_prod_lam env (n,t,d) vl flag =
 	let id' = next_ident_away (id_of_name n) vl in 
 	let env' = push_rel_assum (Name id', t) env in
 	extract_type_rec_info env' d (id'::vl) []
-    | (Logic, Arity), _ | _, Lam ->
-	extract_type_rec_info  env' d vl []
-    | (Logic, NotArity), Product ->
-	(match extract_type_rec_info env' d vl [] with 
-	   | Tmltype (mld, vl') -> Tmltype (Tarr (Miniml.Tprop, mld), vl')
-	   | et -> et)
     | (Info, NotArity), Product ->
 	(* It is important to treat [d] first and [t] in second. *)
 	(* This ensures that the end of [vl] correspond to external binders. *)
@@ -417,6 +411,7 @@ and extract_prod_lam env (n,t,d) vl flag =
 			(* Cf. relation between [extract_type] and [v_of_t] *)
 		  | Tmltype (mlt,vl'') -> Tmltype (Tarr(mlt,mld), vl''))
 	   | et -> et)
+    | _ -> extract_type_rec_info  env' d vl []
 	
  (* Auxiliary function dealing with type application. 
     Precondition: [r] is of type an arity. *)
@@ -543,13 +538,12 @@ and extract_term_info_wt env ctx c t =
      | Lambda (n, t, d) ->
 	 let v = v_of_t env t in 
 	 let env' = push_rel_assum (n,t) env in
-	 let ctx' = (snd v = NotArity) :: ctx in
+	 let ctx' = (v = default) :: ctx in
 	 let d' = extract_term_info env' ctx' d in
 	 (* If [d] was of type an arity, [c] too would be so *)
 	 (match v with
-	    | _,Arity -> d'
-	    | Logic,NotArity -> MLlam (prop_name, d')
-	    | Info,NotArity -> MLlam (id_of_name n, d'))
+	    | Info,NotArity -> MLlam (id_of_name n, d')
+	    | _ -> d')
      | LetIn (n, c1, t1, c2) ->
 	 let v = v_of_t env t1 in
 	 let env' = push_rel (n,Some c1,t1) env in
@@ -605,9 +599,7 @@ and abstract_constructor cp  =
 	MLcons (ConstructRef cp, rels)
     | (Info,NotArity) :: l -> 
 	MLlam (id_of_name Anonymous, abstract (i :: rels) (succ i) l)
-    | (Logic,NotArity) :: l ->
-	MLlam (id_of_name Anonymous, abstract rels (succ i) l)
-    | (_,Arity) :: l -> 
+    | _ :: l ->
 	abstract rels i l
   in
   anonym_lams (ml_lift n (abstract [] 1 s)) n
@@ -661,7 +653,7 @@ and extract_fix env ctx i (fi,ti,ci as recd) =
   let lb = Array.to_list (array_map2 (fun a b -> (a,b)) fi ti') in
   let env' = push_rels_assum (List.rev lb) env in
   let ctx' = 
-    (List.rev_map (fun (_,a) -> a = NotArity) (sign_of_lbinders env lb)) @ ctx
+    (List.rev_map (fun a -> a = default) (sign_of_lbinders env lb)) @ ctx
   in
   let extract_fix_body c t = 
     extract_constr_to_term_wt env' ctx' c (lift n t) in
@@ -681,11 +673,10 @@ and extract_app env ctx f args =
   let mlargs = 
     List.fold_right 
       (fun (v,a) args -> match v with
-	 | (_,Arity) -> args
-	 | (Logic,NotArity) -> MLprop :: args
 	 | (Info,NotArity) -> 
 	     (* We can't trust tag [default], so we use [extract_constr]. *)
-	     (extract_constr_to_term env ctx a) :: args)
+	     (extract_constr_to_term env ctx a) :: args
+	 | _ -> args)
       (List.combine (list_firstn nargs sf) args)
       []
   in
@@ -904,7 +895,7 @@ and extract_inductive_declaration sp =
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
 let false_rec_sp = path_of_string "Coq.Init.Specif.False_rec"
-let false_rec_e = MLlam (prop_name, MLexn "False_rec")
+let false_rec_e = MLexn "False_rec"
 
 let extract_declaration r = match r with
   | ConstRef sp when sp = false_rec_sp -> Dglob (r, false_rec_e)
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 3f71c1d89..39f8d08b7 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -37,5 +37,3 @@ val extract_constr : env -> constr -> extraction_result
 (*s ML declaration corresponding to a Coq reference. *)
 
 val extract_declaration : global_reference -> ml_decl
-
-val signature : env -> constr -> signature
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 72e81964b..93ec3d9c4 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -31,7 +31,7 @@ let prop_name = id_of_string "_"
 let no_prop_name = 
   List.map (fun i -> if i=prop_name then anonymous else i)
 
-(*s In an ML type, update the arguments to all inductive types [(sp,_)] *)		  
+(*s In an ML type, update the arguments to all inductive types [(sp,_)] *)  
 
 let rec update_args sp vl = function  
   | Tapp ( Tglob r :: l ) -> 
@@ -120,8 +120,8 @@ let rec test_eta_args_lift k n = function
   
 (*s Generic functions overs [ml_ast]. *)
 
-(* [ast_iter_rel f t] applies [f] on every [MLrel] in t. 
-   It takes care of the number of bingings crossed before reaching the [MLrel]. *)
+(* [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care 
+   of the number of bingings crossed before reaching the [MLrel]. *)
 
 let ast_iter f = 
   let rec iter n = function
@@ -202,8 +202,8 @@ let ml_lift k t =
 
 let ml_pop t = ml_lift (-1) t
 
-(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... Rel (k'+k)]
-   and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
+(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... 
+  Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
 
 let permut_rels k k' = 
   let rec permut n = function
@@ -240,7 +240,8 @@ let rec merge_app = function
   | a -> ast_map merge_app a
 
 (*s [check_and_generalize (r0,l,c)] transforms any [MLcons(r0,l)] in [MLrel 1]
-  and raises [Impossible] if any variable in [l] occurs outside such a [MLcons] *)
+  and raises [Impossible] if any variable in [l] occurs outside such a 
+  [MLcons] *)
 
 let check_and_generalize (r0,l,c) = 
   let nargs = List.length l in 
@@ -297,7 +298,8 @@ let is_atomic = function
   | _ -> false
 
 let all_constr br = 
-  try Array.iter (function (_,_,MLcons _)-> () | _ -> raise Impossible) br; true
+  try 
+    Array.iter (function (_,_,MLcons _)-> () | _ -> raise Impossible) br; true
   with Impossible -> false
 
 let rec simplify o = function
@@ -305,9 +307,10 @@ let rec simplify o = function
       simplify o f
   | MLapp (f, a) -> 
       simplify_app o (List.map (simplify o) a) (simplify o f)
-  | MLcons (r,[t]) when is_singleton r -> simplify o t (* Informative singleton *) 
+  | MLcons (r,[t]) when is_singleton r -> simplify o t 
+	(* Informative singleton *) 
   | MLcase (e,[||]) ->
-      MLexn "Empty inductive"
+      MLexn "empty inductive"
   | MLcase (e,[|r,[i],c|]) when is_singleton r -> (* Informative singleton *)
       simplify o (MLletin (i,e,c))
   | MLcase (e,br) ->
@@ -331,7 +334,8 @@ and simplify_app o a = function
 	 | _ -> 
 	     let a' = List.map (ml_lift 1) (List.tl a) in
 	     simplify o (MLletin (id, List.hd a, MLapp (t, a'))))
-  | MLletin (id,e1,e2) -> (* Application of a letin: we push arguments inside *)
+  | MLletin (id,e1,e2) -> 
+      (* Application of a letin: we push arguments inside *)
       MLletin (id, e1, simplify o (MLapp (e2, List.map (ml_lift 1) a)))
   | MLcase (e,br) -> (* Application of a case: we push arguments inside *)
       let br' = 
@@ -398,7 +402,8 @@ let optimize_fix a =
 	     let m = List.length args in 
 	     (match a' with 
 		| MLfix(_,[|_|],[|_|]) when 
-		    (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') -> a'
+		    (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') 
+		    -> a'
 		| MLfix(_,[|f|],[|c|]) -> 
 		    let v = Array.make n 0 in 
 		    for i=0 to (n-1) do v.(i)<-i done;
@@ -407,15 +412,17 @@ let optimize_fix a =
 		      | _ -> raise Impossible
 		    in
 		    (try 
-		      list_iter_i aux args; 
-		      let args_f = 
-			List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
-		      let new_f = 
-			anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in  
-		      let new_c = 
-			named_lams (normalize (MLapp ((ml_subst new_f c),args))) ids
-		      in MLfix(0,[|f|],[|new_c|])
-		    with Impossible -> a) 
+		       list_iter_i aux args; 
+		       let args_f = 
+			 List.rev_map 
+			   (fun i -> MLrel (i+m+1)) (Array.to_list v) in
+		       let new_f = 
+			 anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in  
+		       let new_c = 
+			 named_lams 
+			   (normalize (MLapp ((ml_subst new_f c),args))) ids
+		       in MLfix(0,[|f|],[|new_c|])
+		     with Impossible -> a) 
 		| _ -> a)
 	 | _ -> a)
 
@@ -572,6 +579,11 @@ let warning_expansion r =
 (*i    'sTR (" of size "^ (string_of_int (ml_size t))); i*)
     'sPC; 'sTR "is expanded." >])
 
+let warning_expansion_must r = 
+  wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
+		 Printer.pr_global r; 
+    'sPC; 'sTR "must be expanded." >])
+
 let print_ml_decl prm (r,_) = 
   not (to_inline r) || List.mem r prm.to_appear
 
@@ -593,6 +605,10 @@ let rec empty_ind = function
        | ids,r,[] -> Dabbrev (r,ids,Texn "empty inductive") :: l,l'
        | _ -> l,t::l')
 
+let is_exn = function 
+  | MLexn _ -> true
+  | _ -> false
+
 let rec optimize prm = function
   | [] -> 
       []
@@ -605,17 +621,24 @@ let rec optimize prm = function
       else optimize prm l
   | Dglob (r,t) :: l ->
       let t = normalize t in
-      let b = expand (strict_language prm.lang) r t in
+      let b = expand (strict_language prm.lang) r t
+      and b' = is_exn t in 
       let l = if b then 
 	begin
 	  if not (prm.toplevel) then if_verbose warning_expansion r;
 	  List.map (subst_glob_decl r t) l
 	end
+      else if b' then 
+	begin 
+	  if not (prm.toplevel) then if_verbose warning_expansion_must r;
+          List.map (subst_glob_decl r t) l
+	end
       else l in 
-      if (prm.mod_name <> None) || List.mem r prm.to_appear || not b then 
+      if not b' && 
+	(not b || prm.mod_name <> None || List.mem r prm.to_appear) then 
 	let t = optimize_fix t in
 	Dglob (r,t) :: (optimize prm l)
-      else
+      else 
 	optimize prm l
   | (Dtype ([],_) | Dabbrev _ | Dcustom _) as d :: l -> 
       d :: (optimize prm l)
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index f1f00d1e3..8c8138fd0 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -138,10 +138,10 @@ let print_inline () =
   mSG 
     [< 'sTR "Extraction Inline:"; 'fNL; 
        Refset.fold
-	 (fun r p -> [< p; 'sTR  "   " ; Printer.pr_global r ; 'fNL >]) i' [<>];
+	 (fun r p -> [< p; 'sTR "   " ; Printer.pr_global r ; 'fNL >]) i' [<>];
        'sTR "Extraction NoInline:"; 'fNL; 
        Refset.fold
-	 (fun r p -> [< p; 'sTR  "   " ; Printer.pr_global r ; 'fNL >]) n [<>]
+	 (fun r p -> [< p; 'sTR "   " ; Printer.pr_global r ; 'fNL >]) n [<>]
     >]
 
 let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline)