Extraction: fix type_expunge_from_sign broken in last commit

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

3 files changed, 54 insertions, 61 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 69090bdd2..c11a8f128 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -122,30 +122,6 @@ let rec nb_default_params env c =
 	if is_default env t then n+1 else n
     | _ -> 0
 
-(* Classification of signatures *)
-
-type sign_kind =
-  | EmptySig
-  | NonLogicalSig (* at least a [Keep] *)
-  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
-  | SafeLogicalSig (* only [Kill Ktype] *)
-
-let rec sign_kind = function
-  | [] -> EmptySig
-  | Keep :: _ -> NonLogicalSig
-  | Kill k :: s ->
-      match sign_kind s with
-	| NonLogicalSig -> NonLogicalSig
-	| UnsafeLogicalSig -> UnsafeLogicalSig
-	| SafeLogicalSig | EmptySig ->
-	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
-
-(* Removing the final [Keep] in a signature *)
-
-let rec no_final_keeps = function
-  | [] -> []
-  | k :: s -> let s' = k :: no_final_keeps s in if s' = [Keep] then [] else s'
-
 (* Enriching a signature with implicit information *)
 
 let sign_with_implicits r s =
@@ -650,7 +626,7 @@ and extract_cst_app env mle mlt kn args =
   (* Now, the extraction of the arguments. *)
   let s_full = type2signature env (snd schema) in
   let s_full = sign_with_implicits (ConstRef kn) s_full in
-  let s = no_final_keeps s_full in
+  let s = sign_no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
   (* The ml arguments, already expunged from known logical ones *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 89254d8dc..1cef86ee5 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -274,23 +274,6 @@ let type_expand env t =
     | a -> a
   in if Table.type_expand () then expand t else t
 
-(*s Idem, but only at the top level of implications. *)
-
-let is_arrow = function Tarr _ -> true | _ -> false
-
-let type_weak_expand env t =
-  let rec expand = function
-    | Tmeta {contents = Some t} -> expand t
-    | Tglob (r,l) as t ->
-	(match env r with
-	   | Some mlt ->
-	       let u = expand (type_subst_list l mlt) in
-	       if is_arrow u then u else t
-	   | None -> t)
-    | Tarr (a,b) -> Tarr (a, expand b)
-    | a -> a
-  in expand t
-
 (*s Generating a signature from a ML type. *)
 
 let type_to_sign env t = match type_expand env t with
@@ -313,28 +296,51 @@ let sign_of_id = function
   | Dummy -> Kill Kother
   | _ -> Keep
 
+(* Classification of signatures *)
+
+type sign_kind =
+  | EmptySig
+  | NonLogicalSig (* at least a [Keep] *)
+  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
+  | SafeLogicalSig (* only [Kill Ktype] *)
+
+let rec sign_kind = function
+  | [] -> EmptySig
+  | Keep :: _ -> NonLogicalSig
+  | Kill k :: s ->
+      match sign_kind s with
+	| NonLogicalSig -> NonLogicalSig
+	| UnsafeLogicalSig -> UnsafeLogicalSig
+	| SafeLogicalSig | EmptySig ->
+	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
+
+(* Removing the final [Keep] in a signature *)
+
+let rec sign_no_final_keeps = function
+  | [] -> []
+  | k :: s ->
+      let s' = k :: sign_no_final_keeps s in
+      if s' = [Keep] then [] else s'
+
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
-  if s = [] then t
-  else if List.mem Keep s then
-    let rec f t s =
-      if List.exists isKill s then
-	match t with
-	  | Tmeta {contents = Some t} -> f t s
-	  | Tarr (a,b) ->
-	      let t = f b (List.tl s) in
-	      if List.hd s = Keep then Tarr (a, t) else t
-	  | Tglob (r,l) ->
-	      (match env r with
-		 | Some mlt -> f (type_subst_list l mlt) s
-		 | None -> assert false)
-	  | _ -> assert false
-      else t
-    in f t s
-  else if lang () <> Haskell && List.mem (Kill Kother) s then
-    Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t)))
-  else snd (type_decomp (type_weak_expand env t))
+  let rec expunge s t =
+    if s = [] then t else match t with
+      | Tmeta {contents = Some t} -> expunge s t
+      | Tarr (a,b) ->
+	  let t = expunge (List.tl s) b in
+	  if List.hd s = Keep then Tarr (a, t) else t
+      | Tglob (r,l) ->
+	  (match env r with
+	     | Some mlt -> expunge s (type_subst_list l mlt)
+	     | None -> assert false)
+      | _ -> assert false
+  in
+  let t = expunge (sign_no_final_keeps s) t in
+  if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then
+    Tarr (Tdummy Kother, t)
+  else t
 
 let type_expunge env t =
   type_expunge_from_sign env (type_to_signature env t) t
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index f4ab66746..42787a540 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -114,3 +114,14 @@ val inline : global_reference -> ml_ast -> bool
 
 exception Occurs of int
 
+(* Classification of signatures *)
+
+type sign_kind =
+  | EmptySig
+  | NonLogicalSig (* at least a [Keep] *)
+  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
+  | SafeLogicalSig (* only [Kill Ktype] *)
+
+val sign_kind : signature -> sign_kind
+
+val sign_no_final_keeps : signature -> signature