Term.dest* functions now raise specific DestKO exn instead of Invalid_argument

**Warning** the ml code of plugins may have to be adapted after this.

Concerning coq itself, I've done the adaptations, let's hope I've
forgotten none. In practice, the number of changes are relatively low,
and the code is quite cleaner this way.

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

8 files changed, 42 insertions, 37 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index a052d6dfc..1a829c3a4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -271,34 +271,37 @@ let kind_of_type = function
 (**********************************************************************)
 
 (* Destructor operations : partial functions
-   Raise invalid_arg "dest*" if the const has not the expected form *)
+   Raise [DestKO] if the const has not the expected form *)
+
+exception DestKO
 
 (* Destructs a DeBrujin index *)
 let destRel c = match kind_of_term c with
   | Rel n -> n
-  | _ -> invalid_arg "destRel"
+  | _ -> raise DestKO
 
 (* Destructs an existential variable *)
 let destMeta c = match kind_of_term c with
   | Meta n -> n
-  | _ -> invalid_arg "destMeta"
+  | _ -> raise DestKO
 
 let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
-let isMetaOf mv c = match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false
+let isMetaOf mv c =
+  match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false
 
 (* Destructs a variable *)
 let destVar c = match kind_of_term c with
   | Var id -> id
-  | _ -> invalid_arg "destVar"
+  | _ -> raise DestKO
 
 (* Destructs a type *)
 let isSort c = match kind_of_term c with
-  | Sort s -> true
+  | Sort _ -> true
   | _ -> false
 
 let destSort c = match kind_of_term c with
   | Sort s -> s
-  | _ -> invalid_arg "destSort"
+  | _ -> raise DestKO
 
 let rec isprop c = match kind_of_term c with
   | Sort (Prop _) -> true
@@ -336,18 +339,20 @@ let isEvar_or_Meta c = match kind_of_term c with
 (* Destructs a casted term *)
 let destCast c = match kind_of_term c with
   | Cast (t1,k,t2) -> (t1,k,t2)
-  | _ -> invalid_arg "destCast"
+  | _ -> raise DestKO
 
 let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
 
 
 (* Tests if a de Bruijn index *)
 let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
-let isRelN n c = match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
+let isRelN n c =
+  match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
 
 (* Tests if a variable *)
 let isVar c = match kind_of_term c with Var _ -> true | _ -> false
-let isVarId id c = match kind_of_term c with Var id' -> Id.equal id id' | _ -> false
+let isVarId id c =
+  match kind_of_term c with Var id' -> Id.equal id id' | _ -> false
 
 (* Tests if an inductive *)
 let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
@@ -355,28 +360,28 @@ let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
 (* Destructs the product (x:t1)t2 *)
 let destProd c = match kind_of_term c with
   | Prod (x,t1,t2) -> (x,t1,t2)
-  | _ -> invalid_arg "destProd"
+  | _ -> raise DestKO
 
 let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
 
 (* Destructs the abstraction [x:t1]t2 *)
 let destLambda c = match kind_of_term c with
   | Lambda (x,t1,t2) -> (x,t1,t2)
-  | _ -> invalid_arg "destLambda"
+  | _ -> raise DestKO
 
 let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
 
 (* Destructs the let [x:=b:t1]t2 *)
 let destLetIn c = match kind_of_term c with
   | LetIn (x,b,t1,t2) -> (x,b,t1,t2)
-  | _ -> invalid_arg "destLetIn"
+  | _ -> raise DestKO
 
 let isLetIn c =  match kind_of_term c with LetIn _ -> true | _ -> false
 
 (* Destructs an application *)
 let destApp c = match kind_of_term c with
   | App (f,a) -> (f, a)
-  | _ -> invalid_arg "destApplication"
+  | _ -> raise DestKO
 
 let destApplication = destApp
 
@@ -385,43 +390,43 @@ let isApp c = match kind_of_term c with App _ -> true | _ -> false
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
   | Const kn -> kn
-  | _ -> invalid_arg "destConst"
+  | _ -> raise DestKO
 
 let isConst c = match kind_of_term c with Const _ -> true | _ -> false
 
 (* Destructs an existential variable *)
 let destEvar c = match kind_of_term c with
   | Evar (kn, a as r) -> r
-  | _ -> invalid_arg "destEvar"
+  | _ -> raise DestKO
 
 (* Destructs a (co)inductive type named kn *)
 let destInd c = match kind_of_term c with
   | Ind (kn, a as r) -> r
-  | _ -> invalid_arg "destInd"
+  | _ -> raise DestKO
 
 (* Destructs a constructor *)
 let destConstruct c = match kind_of_term c with
   | Construct (kn, a as r) -> r
-  | _ -> invalid_arg "dest"
+  | _ -> raise DestKO
 
 let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind_of_term c with
   | Case (ci,p,c,v) -> (ci,p,c,v)
-  | _ -> invalid_arg "destCase"
+  | _ -> raise DestKO
 
 let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
 
 let destFix c = match kind_of_term c with
   | Fix fix -> fix
-  | _ -> invalid_arg "destFix"
+  | _ -> raise DestKO
 
 let isFix c =  match kind_of_term c with Fix _ -> true | _ -> false
 
 let destCoFix c = match kind_of_term c with
   | CoFix cofix -> cofix
-  | _ -> invalid_arg "destCoFix"
+  | _ -> raise DestKO
 
 let isCoFix c =  match kind_of_term c with CoFix _ -> true | _ -> false
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 753fc990d..65963e3e9 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -262,7 +262,9 @@ val is_small : sorts -> bool
 
 (** {6 Term destructors } *)
 (** Destructor operations are partial functions and
-    @raise Invalid_argument "dest*" if the term has not the expected form. *)
+    @raise [DestKO] if the term has not the expected form. *)
+
+exception DestKO
 
 (** Destructs a DeBrujin index *)
 val destRel : constr -> int
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 9a2f23d64..3a2711622 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -220,9 +220,7 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype outtype (cstr:constructor) special default gls=
   let env=pf_env gls in
-  let (h,argv) =
-    try destApp intype with
-	Invalid_argument _ -> (intype,[||])  in
+  let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in
   let ind=destInd h in
   let types=Inductiveops.arities_of_constructors env ind in
   let lp=Array.length types in
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 8b5fe85e7..1187d9d76 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -113,8 +113,7 @@ let get_top_stack pts =
     let info = get_info sigma gl in
     info.pm_stack
 
-let get_last env =
-  try
-    let (id,_,_) =  List.hd (Environ.named_context env) in id
-  with Invalid_argument _ -> error "no previous statement to use"
+let get_last env = match Environ.named_context env with
+  | (id,_,_)::_ -> id
+  | [] -> error "no previous statement to use"
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 48e60d798..6c1709140 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -20,7 +20,8 @@ let update_flags ()=
     try
       let kn=destConst (Classops.get_coercion_value coe) in
 	predref:=Names.Cpred.add kn !predref
-    with Invalid_argument "destConst"-> () in
+    with DestKO -> ()
+  in
     List.iter f (Classops.coercions ());
     red_flags:=
     Closure.RedFlags.red_add_transparent
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index ceaf2a79b..597b6afb6 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -122,7 +122,7 @@ let rec make_form atom_env gls term =
 		  let fb=make_form atom_env gls argv.(1) in
 		    Disjunct (fa,fb)
 		else make_atom atom_env (normalize term)
-	    with Invalid_argument _ -> make_atom atom_env (normalize term)
+	    with DestKO -> make_atom atom_env (normalize term)
 	  end
       | _ -> make_atom atom_env (normalize term)
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index f65ccc5ba..a4f00bc45 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -170,7 +170,7 @@ let rec nf_val env v typ =
       let lvl = nb_rel env in
       let name,dom,codom = 
 	try decompose_prod env typ
-	with Invalid_argument _ ->
+	with DestKO ->
           Errors.anomaly
             (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b18719cc2..1ccc10375 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -176,7 +176,7 @@ and nf_stk env c t stk  =
       nf_stk env (mkApp(c,args)) t stk
   | Zfix (f,vargs) :: stk ->
       let fa, typ = nf_fix_app env f vargs in
-      let _,_,codom = try decompose_prod env typ with _ -> exit 120 in
+      let _,_,codom = try decompose_prod env typ with DestKO -> exit 120 in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
       let (mind,_ as ind),allargs = find_rectype_a env t in
@@ -206,7 +206,7 @@ and nf_predicate env ind mip params v pT =
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
+      let name,dom,codom = try decompose_prod env pT with DestKO -> exit 121 in
       let dep,body =
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
@@ -228,7 +228,7 @@ and nf_args env vargs t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
+	let _,dom,codom = try decompose_prod env !t with DestKO -> exit 123 in
 	let c = nf_val env (arg vargs i) dom in
 	t := subst1 c codom; c) in
   !t,args
@@ -239,7 +239,7 @@ and nf_bargs env b t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
+	let _,dom,codom = try decompose_prod env !t with DestKO -> exit 124 in
 	let c = nf_val env (bfield b i) dom in
 	t := subst1 c codom; c) in
   args
@@ -249,7 +249,7 @@ and nf_fun env f typ =
   let vb = body_of_vfun k f in
   let name,dom,codom =
     try decompose_prod env typ
-    with Invalid_argument _ ->
+    with DestKO ->
       (* 27/2/13: Turned this into an anomaly *)
       Errors.anomaly
         (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")