summaryrefslogtreecommitdiff
path: root/pretyping/vnorm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/vnorm.ml')
-rw-r--r--pretyping/vnorm.ml19
1 files changed, 12 insertions, 7 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 465c062b..5d09570e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vnorm.ml 11017 2008-05-29 13:00:24Z barras $ i*)
+(*i $Id: vnorm.ml 11424 2008-09-30 12:10:28Z jforest $ i*)
open Names
open Declarations
@@ -20,7 +20,7 @@ open Vm
(* Calcul de la forme normal d'un terme *)
(*******************************************)
-let crazy_type = mkSet
+let crazy_type = mkSet
let decompose_prod env t =
let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
@@ -178,7 +178,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 = decompose_prod env typ in
+ let _,_,codom = try decompose_prod env typ with _ -> 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
@@ -187,6 +187,7 @@ and nf_stk env c t stk =
let params,realargs = Util.array_chop nparams allargs in
let pT =
hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
+ let pT = whd_betadeltaiota env pT in
let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
let btypes = build_branches_type env ind mib mip params dep p in
@@ -210,7 +211,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 = decompose_prod env pT in
+ let name,dom,codom = try decompose_prod env pT with _ -> 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)
@@ -232,7 +233,7 @@ and nf_args env vargs t =
let args =
Array.init len
(fun i ->
- let _,dom,codom = decompose_prod env !t in
+ let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
let c = nf_val env (arg vargs i) dom in
t := subst1 c codom; c) in
!t,args
@@ -243,7 +244,7 @@ and nf_bargs env b t =
let args =
Array.init len
(fun i ->
- let _,dom,codom = decompose_prod env !t in
+ let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
let c = nf_val env (bfield b i) dom in
t := subst1 c codom; c) in
args
@@ -251,7 +252,11 @@ and nf_bargs env b t =
and nf_fun env f typ =
let k = nb_rel env in
let vb = body_of_vfun k f in
- let name,dom,codom = decompose_prod env typ in
+ let name,dom,codom =
+ try decompose_prod env typ
+ with _ ->
+ raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
+ in
let body = nf_val (push_rel (name,None,dom) env) vb codom in
mkLambda(name,dom,body)