diff options
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 3a666a60..ec16aa26 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Cic open Term @@ -92,13 +92,13 @@ let whd_betaiotazeta x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t @@ -167,8 +167,9 @@ let sort_cmp env univ pb s0 s1 = CUMUL -> () | _ -> raise NotConvertible) | (Type u1, Type u2) -> - if snd (engagement env) == StratifiedType - && not + (** FIXME: handle type-in-type option here *) + if (* snd (engagement env) == StratifiedType && *) + not (match pb with | CONV -> Univ.check_eq univ u1 u2 | CUMUL -> Univ.check_leq univ u1 u2) @@ -476,7 +477,7 @@ let vm_conv cv_pb = fconv cv_pb true * error message. *) let hnf_prod_app env t n = - match whd_betadeltaiota env t with + match whd_all env t with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -487,10 +488,10 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in match t with | Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in decrec (push_rel d env) (d::m) c0 | _ -> m,t in @@ -499,17 +500,17 @@ let dest_prod env = (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match rty with | Prod (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let rty' = whd_betadeltaiota env rty in + let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in @@ -517,13 +518,13 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match rty with | Lambda (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty |