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

1 files changed, 42 insertions, 36 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 89254d8dc9..1cef86ee59 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