aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/term.ml47
-rw-r--r--kernel/term.mli4
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/decl_mode/decl_mode.ml7
-rw-r--r--plugins/firstorder/ground.ml3
-rw-r--r--plugins/rtauto/refl_tauto.ml2
-rw-r--r--pretyping/nativenorm.ml2
-rw-r--r--pretyping/vnorm.ml10
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.")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:45:56 +0000