bugs/améliorations trouvés via FTA

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

7 files changed, 114 insertions, 75 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0b5b10e21..a02dff295 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -33,19 +33,6 @@ let add_structure mp msb env =
       | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
   in List.fold_left add_one env msb
 
-(* Add _all_ direct subobjects of a module, not only those exported. 
-   Build on the Modops.add_signature model. *)
-
-let add_structure mp msb env = 
-  let add_one env (l,elem) = 
-    let kn = make_kn mp empty_dirpath l in 
-    match elem with 
-      | SEBconst cb -> Environ.add_constant kn cb env 
-      | SEBmind mib -> Environ.add_mind kn mib env 
-      | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
-      | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
-  in List.fold_left add_one env msb
-
 let add_functor mbid mtb env = 
   Modops.add_module (MPbound mbid) (Modops.module_body_of_type mtb) env 
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 294f962dc..401e4f98f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -98,6 +98,14 @@ let rec type_sign_vl env c =
 	else true::s, (next_ident_away (id_of_name n) vl) :: vl
     | _ -> [],[]
 
+let rec nb_default_params env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) ->
+	let n = nb_default_params (push_rel_assum (n,t) env) d in 
+	if is_default env t then n+1 else n
+    | _ -> 0
+
+
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]  
@@ -332,11 +340,12 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  with Not_found -> raise (I Standard);
 	in 
 	let s = List.map (type_neq (mlt_env env) Tdummy) typ in
+	let n = nb_default_params env mip0.mind_nf_arity in
 	let check (_,o) = match o with 
 	  | None -> raise (I Standard)
 	  | Some kn -> ConstRef kn 
 	in  
-	add_record kn (List.map check (List.filter fst (List.combine s projs))); 
+	add_record kn n (List.map check (List.filter fst (List.combine s projs))); 
 	raise (I Record)
       with (I info) -> info
     in
@@ -509,31 +518,44 @@ and extract_cst_app env mle mlt kn args =
   let schema = nb, type_expand env t in 
   (* Then the expected type of this constant. *)
   let metas = List.map new_meta args in 
-  let type_head = type_recomp (metas,mlt) in 
-  (* The head gets a magic if stored and expected types differ. *)
-  let head = 
-    let h = MLglob (ConstRef kn) in 
-    put_magic (type_recomp (metas,mlt), instantiation schema) h in
+  (* We compare stored and expected types in two steps. *)
+  (* First, can [kn] be applied to all args ? *)
+  let a = new_meta () in 
+  let magic1 = needs_magic (type_recomp (metas, a), instantiation schema) in 
+  (* Second, is the resulting type compatible with the expected type [mlt] ? *)
+  let magic2 = needs_magic (a, mlt) in 
+  (* The internal head receives a magic if [magic1] *)
+  let head = put_magic_if magic1 (MLglob (ConstRef kn)) in 
   (* Now, the extraction of the arguments. *)
   let s = type_to_sign env (snd schema) in 
   let ls = List.length s in 
   let la = List.length args in
   let mla = make_mlargs env mle s args metas in 
+  let mla =
+    if not magic1 then 
+      try 
+	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in 
+	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
+	else mla
+      with _ -> mla
+    else mla
+  in 			    
   (* Different situations depending of the number of arguments: *)
-  if ls = 0 then head
+  if ls = 0 then put_magic_if magic2 head
   else if List.mem true s then 
-    if la >= ls then MLapp (head, mla)
+    if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
     else 
       (* Not enough arguments. We complete via eta-expansion. *)
       let ls' = ls-la in
       let s' = list_lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
-      anonym_or_dummy_lams (MLapp (head, mla)) s'
+      put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
   else 
     (* In the special case of always false signature, one dummy lam is left. *)
     (* So a [MLdummy] is left accordingly. *) 
-    if la >= ls then MLapp (head, MLdummy :: mla)
-    else dummy_lams head (ls-la-1)
+    if la >= ls 
+    then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
+    else put_magic_if magic2 (dummy_lams head (ls-la-1))
 
 (*s Extraction of an inductive constructor applied to arguments. *)
 
@@ -564,26 +586,29 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let args' = list_lastn la' args in 
   (* Now, we build the expected type of the constructor *)
   let metas = List.map new_meta args' in 
-  let type_head = type_recomp (metas, mlt) in
   (* If stored and expected types differ, then magic! *)
-  let magic = needs_magic (type_cons, type_head) in 
+  let a = new_meta () in 
+  let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
+  let magic2 = needs_magic (a, mlt) in 
   let head mla = 
     if mi.ind_info = Singleton then 
-      put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *)
-    else put_magic_if magic (MLcons (ConstructRef cp, mla))
+      put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
+    else put_magic_if magic1 (MLcons (ConstructRef cp, mla))
   in 
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then 
     let head' = head (eta_args_sign ls s) in 
-    dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)
+    put_magic_if magic2 
+      (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
   else 
     let mla = make_mlargs env mle s args' metas in 
-    if la = ls + params_nb then head mla
+    if la = ls + params_nb 
+    then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *) 
       let ls' = params_nb + ls - la in 
       let s' = list_lastn ls' s in 
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
-      anonym_or_dummy_lams (head mla) s'
+      put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
 
 (*S Extraction of a case. *)
 
@@ -658,9 +683,9 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], 
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta env c t = 
-  let rels = fst (splay_prod env none t) in 
-  let n = List.length rels in 
+let rec decomp_lams_eta_n n env c t = 
+  let rels = fst (decomp_n_prod env none n t) in 
+  let rels = List.map (fun (id,_,c) -> (id,c)) rels in 
   let m = nb_lam c in 
   if m >= n then decompose_lam_n n c 
   else
@@ -674,13 +699,6 @@ let rec decomp_lams_eta env c t =
 (*s From a constant to a ML declaration. *)
 
 let extract_std_constant env kn body typ = 
-  (* Decomposing the top level lambdas of [body]. *)
-  let rels,c = decomp_lams_eta env body typ in
-  (* The lambdas names. *)
-  let ids = List.map (fun (n,_) -> id_of_name n) rels in 
-  (* The according Coq environment. *)
-  let env = push_rels_assum rels env in
-  (* The ML part: *)
   reset_meta_count (); 
   (* The short type [t] (i.e. possibly with abbreviations). *)
   let t = snd (record_constant_type env kn (Some typ)) in 
@@ -690,6 +708,12 @@ let extract_std_constant env kn body typ =
   let s = List.map ((<>) Tdummy) l in 
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
+  (* Decomposing the top level lambdas of [body]. *)
+  let rels,c = decomp_lams_eta_n (List.length s) env body typ in
+  (* The lambdas names. *)
+  let ids = List.map (fun (n,_) -> id_of_name n) rels in 
+  (* The according Coq environment. *)
+  let env = push_rels_assum rels env in
   (* The real extraction: *)
   let e = extract_term env mle t' c [] in
   (* Expunging term and type from dummy lambdas. *) 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 3355fc2aa..ba0659b32 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -401,7 +401,7 @@ let ast_occurs k t =
 (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)] 
    in [t] with [k<=i<=k'] *)
 
-let occurs_itvl k k' t = 
+let ast_occurs_itvl k k' t = 
   try 
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false 
   with Found -> true
@@ -561,7 +561,7 @@ let eta_red e =
 	else
 	  let a1,a2 = list_chop m a in 
 	  let f = if m = 0 then f else MLapp (f,a1) in 
-	  if test_eta_args_lift 0 n a2 && not (occurs_itvl 1 n f)
+	  if test_eta_args_lift 0 n a2 && not (ast_occurs_itvl 1 n f)
 	  then ast_lift (-n) f
 	  else e 
     | _ -> e
@@ -601,12 +601,12 @@ let check_constant_case br =
   if br = [||] then raise Impossible; 
   let (r,l,t) = br.(0) in
   let n = List.length l in 
-  if occurs_itvl 1 n t then raise Impossible; 
+  if ast_occurs_itvl 1 n t then raise Impossible; 
   let cst = ast_lift (-n) t in 
   for i = 1 to Array.length br - 1 do 
     let (r,l,t) = br.(i) in
     let n = List.length l in
-    if (occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) 
+    if (ast_occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) 
     then raise Impossible
   done; cst
 
@@ -683,7 +683,7 @@ let rec simpl o = function
 	simpl o (ast_subst c e)
   | MLfix(i,ids,c) as t when o -> 
       let n = Array.length ids in 
-      if occurs_itvl 1 n c.(i) then 
+      if ast_occurs_itvl 1 n c.(i) then 
 	MLfix (i, ids, Array.map (simpl o) c)
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
   | a -> ast_map (simpl o) a 
@@ -917,7 +917,7 @@ 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') 
+		 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a') 
 		 -> a'
 	     | MLfix(_,[|f|],[|c|]) -> 
 		 (try general_optimize_fix f ids n args m c
@@ -1061,8 +1061,8 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && not (is_inline_custom r) 
   && (to_inline r (* The user DOES want to inline it *) 
-     || (auto_inline () && lang () <> Haskell 
-	 && (is_recursor r || manual_inline r || inline_test t)))
+     || (auto_inline () && lang () <> Haskell && not (is_projection r)
+         && (is_recursor r || manual_inline r || inline_test t)))
 
 (*S Optimization. *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index b8f817eab..13f37b32b 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -96,6 +96,7 @@ val eta_args_sign : int -> bool list -> ml_ast list
 
 val ast_iter : (ml_ast -> unit) -> ml_ast -> unit
 val ast_occurs : int -> ml_ast -> bool
+val ast_occurs_itvl : int -> int -> ml_ast -> bool
 val ast_lift : int -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 311c346d5..d65a46710 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -222,11 +222,12 @@ let rec pp_expr par env args =
 		(hov 2 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ 
 		 spc () ++ str "in") ++ 
 	      spc () ++ hov 0 pp_a2))
-    | MLglob r when is_projection r && args <> [] ->
-	let record = List.hd args in 
-	pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
     | MLglob r -> 
-	apply (pp_global r)
+	(try 
+	   let _,args = list_chop (projection_arity r) args in 
+	   let record = List.hd args in 
+	   pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
+	 with _ -> apply (pp_global r))
     | MLcons (r,[]) ->
 	assert (args=[]);
 	if Refset.mem (long_r r) !cons_cofix then 
@@ -250,22 +251,43 @@ let rec pp_expr par env args =
 	  (pp_expr false env [] t) 
 	in 
 	let record = 
-	  try ignore (find_projections (kn_of_r r)); true with Not_found -> false
+	  try Some (find_projections (kn_of_r r)) with Not_found -> None
 	in 
-	if Array.length pv = 1 && not record then 
-	  let s1,s2 = pp_one_pat env pv.(0) in 
-	  apply 
-	    (hv 0 
-	       (pp_par par' 
-		  (hv 0 
-		     (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) 
-		      ++ spc () ++ str "in") ++ 
-		   spc () ++ hov 0 s2)))
-	else
-	  apply
-      	    (pp_par par' 
-      	       (v 0 (str "match " ++ expr ++ str " with" ++
-		     fnl () ++ str "  | " ++ pp_pat env pv)))
+	(try 
+	   match record with 
+	     | None -> raise Not_found 
+	     | Some projs -> 
+		 let (_, ids, c) = pv.(0) in 
+		 let n = List.length ids in 
+		 match c with 
+		   | MLrel i when i <= n -> 
+		       apply (pp_par par' (pp_expr true env [] t ++ str "." ++ 
+					   pp_global (List.nth projs (n-i)))) 
+		   | MLapp (MLrel i, a) when i <= n -> 
+		       if List.exists (ast_occurs_itvl 1 n) a 
+		       then raise Not_found
+		       else
+			 let ids,env' = push_vars (List.rev ids) env in
+			 (pp_apply 
+			    (pp_expr true env [] t ++ str "." ++ 
+			     pp_global (List.nth projs (n-i)))
+			    par ((List.map (pp_expr true env' []) a) @ args))
+	     | _ -> raise Not_found
+	 with Not_found -> 
+	   if Array.length pv = 1 && record = None then 
+	     let s1,s2 = pp_one_pat env pv.(0) in 
+	     apply 
+	       (hv 0 
+		  (pp_par par' 
+		     (hv 0 
+			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) 
+			 ++ spc () ++ str "in") ++ 
+		      spc () ++ hov 0 s2)))
+	   else
+	     apply
+      	       (pp_par par' 
+      		  (v 0 (str "match " ++ expr ++ str " with" ++
+			fnl () ++ str "  | " ++ pp_pat env pv))))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -476,7 +498,10 @@ let pp_decl mp =
 	    (str "let " ++ 
 	     if is_custom r then 
 	       e ++ str " = " ++ str (find_custom r)
-	     else if is_projection r then e ++ str " x = x." ++ e
+	     else if is_projection r then 
+	       let s = prvecti (fun _ -> str) 
+			 (Array.make (projection_arity r) " _") in 
+	       e ++ s ++ str " x = x." ++ e
 	     else pp_function (empty_env ()) e a)
     | Dfix (rv,defs,typs) ->
 	pp_Dfix true 0 (rv,defs,typs)
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 1f13d9ce1..9f0b2cf73 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -154,15 +154,16 @@ let is_recursor = function
 let records = ref (KNmap.empty : global_reference list KNmap.t)
 let init_records () = records := KNmap.empty
 
-let projs = ref Refset.empty
-let init_projs () = projs := Refset.empty
+let projs = ref (Refmap.empty : int Refmap.t)
+let init_projs () = projs := Refmap.empty
 
-let add_record kn l = 
+let add_record kn n l = 
   records := KNmap.add (long_kn kn) l !records; 
-  projs := List.fold_right (fun r -> Refset.add (long_r r)) l !projs
+  projs := List.fold_right (fun r -> Refmap.add (long_r r) n) l !projs
 
 let find_projections kn = KNmap.find (long_kn kn) !records
-let is_projection r = Refset.mem (long_r r) !projs
+let is_projection r = Refmap.mem (long_r r) !projs
+let projection_arity r = Refmap.find (long_r r) !projs
 
 (*s Tables synchronization. *)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 413fa8ed3..e4169a9bf 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -62,9 +62,10 @@ val lookup_ind : kernel_name -> ml_ind
 val add_recursors : Environ.env -> kernel_name -> unit
 val is_recursor : global_reference -> bool 
 
-val add_record : kernel_name -> global_reference list -> unit
+val add_record : kernel_name -> int -> global_reference list -> unit
 val find_projections : kernel_name -> global_reference list
 val is_projection : global_reference -> bool 
+val projection_arity : global_reference -> int
 
 val add_aliases : module_path -> module_path -> unit
 val long_mp : module_path -> module_path