travail sur les types extraits

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

4 files changed, 38 insertions, 16 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 52ff05439..32264a004 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -183,15 +183,17 @@ let rec extract_type env db j c args =
 	   | (Info, Default) -> 
 	       (* Standard case: two [extract_type] ... *)
 	       let mld = extract_type env' (0::db) j d [] in 
-	       if mld = Tdummy then Tdummy 
+	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
 	       else Tarr (extract_type env db 0 t [], mld) 
 	   | (Info, TypeScheme) when j > 0 -> 
 	       (* A new type var. *)
 	       let mld = extract_type env' (j::db) (j+1) d [] in 
-	       if mld = Tdummy then Tdummy else Tarr (Tdummy, mld)
+	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
+	       else Tarr (Tdummy, mld)
 	   | _ -> 
 	       let mld = extract_type env' (0::db) j d [] in 
-	       if mld = Tdummy then Tdummy else Tarr (Tdummy, mld))
+	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
+	       else Tarr (Tdummy, mld))
     | Sort _ -> Tdummy (* The two logical cases. *)
     | _ when sort_of env (applist (c, args)) = InProp -> Tdummy 
     | Rel n -> 
@@ -614,7 +616,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in 
   (* Then, the usual variables [s], [ls], [la], ... *)
-  let s = List.map ((<>) Tdummy) types in
+  let s = List.map (type_neq env Tdummy) types in
   let ls = List.length s in 
   let la = List.length args in 
   assert (la <= ls + params_nb);
@@ -685,10 +687,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* The types of the arguments of the corresponding constructor. *)
 	let f t = type_subst_vect metas (type_expand env t) in 
 	let l = List.map f oi.ip_types.(i) in
+	(* the corresponding signature *)
+	let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in 
 	(* We suppress dummy arguments according to signature. *)
-	let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
+	let ids,e = case_expunge s e in
 	(ConstructRef (ip,i+1), List.rev ids, e)
       in
       if mi.ind_info = Singleton then 
@@ -741,7 +745,7 @@ let extract_std_constant env kn body typ =
   (* The real type [t']: without head lambdas, expanded, *)
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
   let l,t' = type_decomp (type_expand env (var2var' t)) in 
-  let s = List.map ((<>) Tdummy) l in 
+  let s = List.map (type_neq env 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]. *)
@@ -851,7 +855,8 @@ let logical_decl = function
   | Dterm (_,MLdummy,Tdummy) -> true
   | Dtype (_,[],Tdummy) -> true 
   | Dfix (_,av,tv) -> 
-      (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv)
+      (array_for_all ((=) MLdummy) av) && 
+      (array_for_all ((=) Tdummy) tv)
   | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index b8764d85d..c55d3746f 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -209,7 +209,7 @@ end
 (*s Does a section path occur in a ML type ? *)
 
 let rec type_mem_kn kn = function 
-  | Tmeta _ -> assert false
+  | Tmeta {contents = Some t} -> type_mem_kn kn t
   | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
   | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
@@ -218,7 +218,7 @@ let rec type_mem_kn kn = function
 
 let type_maxvar t = 
   let rec parse n = function 
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> parse n t
     | Tvar i -> max i n 
     | Tarr (a,b) -> parse (parse n a) b
     | Tglob (_,l) -> List.fold_left parse n l 
@@ -228,7 +228,7 @@ let type_maxvar t =
 (*s From [a -> b -> c] to [[a;b],c]. *) 
 
 let rec type_decomp = function 
-  | Tmeta _ -> assert false
+  | Tmeta {contents = Some t} -> type_decomp t 
   | Tarr (a,b) -> let l,h = type_decomp b in a::l, h 
   | a -> [],a
 
@@ -241,7 +241,7 @@ let rec type_recomp (l,t) = match l with
 (*s Translating [Tvar] to [Tvar'] to avoid clash. *)
 
 let rec var2var' = function 
-  | Tmeta _ -> assert false
+  | Tmeta {contents = Some t} -> var2var' t
   | Tvar i -> Tvar' i
   | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
   | Tglob (r,l) -> Tglob (r, List.map var2var' l)
@@ -252,16 +252,17 @@ type abbrev_map = global_reference -> ml_type option
 (*s Delta-reduction of type constants everywhere in a ML type [t].
    [env] is a function of type [ml_type_env]. *)
 
+
 let type_expand env t = 
   let rec expand = function
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> expand t
     | Tglob (r,l) as t ->    
 	(match env r with 
 	   | Some mlt -> expand (type_subst_list l mlt) 
 	   | None -> Tglob (r, List.map expand l))
     | Tarr (a,b) -> Tarr (expand a, expand b)
     | a -> a
-  in expand t
+  in if Table.type_expand () then expand t else t
 
 (*s Idem, but only at the top level of implications. *)
 
@@ -269,7 +270,7 @@ let is_arrow = function Tarr _ -> true | _ -> false
 
 let type_weak_expand env t = 
   let rec expand = function
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> expand t
     | Tglob (r,l) as t ->    
 	(match env r with 
 	   | Some mlt -> 
@@ -290,7 +291,7 @@ let type_neq env t t' = (type_expand env t <> type_expand env t')
 
 let type_to_sign env t = 
   let rec f = function 
-    | Tmeta _ -> assert false
+    | Tmeta {contents = Some t} -> f t 
     | Tarr (a,b) -> (Tdummy <> a) :: (f b)
     | _ -> [] 
   in f (type_expand env t)
@@ -304,7 +305,7 @@ let type_expunge env t =
     let rec f t s = 
       if List.mem false s then 
 	match t with 
-	  | Tmeta _ -> assert false
+	  | Tmeta {contents = Some t} -> f t s
 	  | Tarr (a,b) -> 
 	      let t = f b (List.tl s) in 
 	      if List.hd s then Tarr (a, t) else t  
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 7c010ab4f..f95f81ee9 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -221,6 +221,18 @@ let _ = declare_bool_option
 	   optread = auto_inline; 
 	   optwrite = (:=) auto_inline_ref}
 
+(*s Extraction TypeExpand *)
+
+let type_expand_ref = ref true
+
+let type_expand () = !type_expand_ref
+
+let _ = declare_bool_option 
+	  {optsync = true;
+	   optname = "Extraction TypeExpand";
+	   optkey = SecondaryTable ("Extraction", "TypeExpand");
+	   optread = type_expand; 
+	   optwrite = (:=) type_expand_ref}
 
 (*s Extraction Optimize *)
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 0b69a7412..6be869e59 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -71,6 +71,10 @@ val reset_tables : unit -> unit
 
 val auto_inline : unit -> bool
 
+(*s TypeExpand parameter *) 
+
+val type_expand : unit -> bool
+
 (*s Optimize parameter *) 
 
 type opt_flag =