summaryrefslogtreecommitdiff
path: root/checker/reduction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/reduction.ml')
-rw-r--r--checker/reduction.ml190
1 files changed, 139 insertions, 51 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 91b59a08..185c6edf 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,15 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Errors
open Util
-open Names
+open Cic
open Term
-open Univ
open Closure
open Esubst
open Environ
@@ -40,7 +40,10 @@ let compare_stack_shape stk1 stk2 =
| (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
| (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
| (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
- | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
+ | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+ Int.equal bal 0 && compare_rec 0 s1 s2
+ | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
+ (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) ->
bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -49,6 +52,7 @@ let compare_stack_shape stk1 stk2 =
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
+ | Zlproj of Names.constant * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -67,9 +71,13 @@ let pure_stack lfts stk =
| (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
| (Zapp a, (l,pstk)) ->
(l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
+ | (Zproj (n,m,c), (l,pstk)) ->
+ (l, Zlproj (c,l)::pstk)
| (Zfix(fx,a),(l,pstk)) ->
let (lfx,pa) = pure_rec l a in
(l, Zlfix((lfx,fx),pa)::pstk)
+ | (ZcaseT(ci,p,br,env),(l,pstk)) ->
+ (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk)
| (Zcase(ci,p,br),(l,pstk)) ->
(l,Zlcase(ci,l,p,br)::pstk)) in
snd (pure_rec lfts stk)
@@ -115,20 +123,27 @@ type 'a conversion_function = env -> 'a -> 'a -> unit
exception NotConvertible
exception NotConvertibleVect of int
+let convert_universes univ u u' =
+ if Univ.Instance.check_eq univ u u' then ()
+ else raise NotConvertible
+
let compare_stacks f fmind lft1 stk1 lft2 stk2 =
let rec cmp_rec pstk1 pstk2 =
match (pstk1,pstk2) with
| (z1::s1, z2::s2) ->
cmp_rec s1 s2;
(match (z1,z2) with
- | (Zlapp a1,Zlapp a2) -> array_iter2 f a1 a2
+ | (Zlapp a1,Zlapp a2) -> Array.iter2 f a1 a2
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
f fx1 fx2; cmp_rec a1 a2
+ | (Zlproj (c1,l1),Zlproj (c2,l2)) ->
+ if not (Names.eq_con_chk c1 c2) then
+ raise NotConvertible
| (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
if not (fmind ci1.ci_ind ci2.ci_ind) then
raise NotConvertible;
f (l1,p1) (l2,p2);
- array_iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2
+ Array.iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2
| _ -> assert false)
| _ -> () in
if compare_stack_shape stk1 stk2 then
@@ -143,7 +158,7 @@ type conv_pb =
let sort_cmp univ pb s0 s1 =
match (s0,s1) with
- | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos & c2 = Null then raise NotConvertible
+ | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
| (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
| (Prop c1, Type u) ->
(match pb with
@@ -152,8 +167,8 @@ let sort_cmp univ pb s0 s1 =
| (Type u1, Type u2) ->
if not
(match pb with
- | CONV -> check_eq univ u1 u2
- | CUMUL -> check_geq univ u2 u1)
+ | CONV -> Univ.check_eq univ u1 u2
+ | CUMUL -> Univ.check_leq univ u1 u2)
then raise NotConvertible
| (_, _) -> raise NotConvertible
@@ -162,7 +177,9 @@ let rec no_arg_available = function
| Zupdate _ :: stk -> no_arg_available stk
| Zshift _ :: stk -> no_arg_available stk
| Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
+ | Zproj _ :: _ -> true
| Zcase _ :: _ -> true
+ | ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
let rec no_nth_arg_available n = function
@@ -173,7 +190,9 @@ let rec no_nth_arg_available n = function
let k = Array.length v in
if n >= k then no_nth_arg_available (n-k) stk
else false
+ | Zproj _ :: _ -> true
| Zcase _ :: _ -> true
+ | ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
let rec no_case_available = function
@@ -181,17 +200,19 @@ let rec no_case_available = function
| Zupdate _ :: stk -> no_case_available stk
| Zshift _ :: stk -> no_case_available stk
| Zapp _ :: stk -> no_case_available stk
+ | Zproj (_,_,_) :: _ -> false
| Zcase _ :: _ -> false
+ | ZcaseT _ :: _ -> false
| Zfix _ :: _ -> true
let in_whnf (t,stk) =
match fterm_of t with
- | (FLetIn _ | FCases _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
+ | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
| FLambda _ -> no_arg_available stk
| FConstruct _ -> no_case_available stk
| FCoFix _ -> no_case_available stk
| FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk
- | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true
+ | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
| FLOCKED -> assert false
let oracle_order fl1 fl2 =
@@ -200,13 +221,18 @@ let oracle_order fl1 fl2 =
| _, ConstKey _ -> true
| _ -> false
+let unfold_projection infos p c =
+ let pb = lookup_projection p (infos_env infos) in
+ let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
+ (c, s)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
- Util.check_for_interrupt ();
+ Control.check_for_interrupt ();
(* First head reduce both terms *)
let rec whd_both (t1,stk1) (t2,stk2) =
let st1' = whd_stack infos t1 stk1 in
@@ -246,7 +272,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
- if eq_table_key fl1 fl2
+ if eq_table_key fl1 fl2
then convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
with NotConvertible ->
@@ -254,19 +280,27 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
let (app1,app2) =
if oracle_order fl1 fl2 then
match unfold_reference infos fl1 with
- | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
- | None ->
- (match unfold_reference infos fl2 with
- | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
- | None -> raise NotConvertible)
+ | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+ | None ->
+ (match unfold_reference infos fl2 with
+ | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+ | None -> raise NotConvertible)
else
match unfold_reference infos fl2 with
- | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
- | None ->
- (match unfold_reference infos fl1 with
- | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
- | None -> raise NotConvertible) in
- eqappr univ cv_pb infos app1 app2)
+ | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+ | None ->
+ (match unfold_reference infos fl1 with
+ | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+ | None -> raise NotConvertible) in
+ eqappr univ cv_pb infos app1 app2)
+
+ | (FProj (p1,c1), _) ->
+ let (def1, s1) = unfold_projection infos p1 c1 in
+ eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+
+ | (_, FProj (p2,c2)) ->
+ let (def2, s2) = unfold_projection infos p2 c2 in
+ eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
(* other constructors *)
| (FLambda _, FLambda _) ->
@@ -287,43 +321,76 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
- anomaly "conversion was given unreduced term (FLambda)";
+ anomaly (Pp.str "conversion was given unreduced term (FLambda)");
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
eqappr univ CONV infos
(el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
| (_, FLambda _) ->
if v2 <> [] then
- anomaly "conversion was given unreduced term (FLambda)";
+ anomaly (Pp.str "conversion was given unreduced term (FLambda)");
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
eqappr univ CONV infos
(el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
(* only one constant, defined var or defined rel *)
- | (FFlex fl1, _) ->
+ | (FFlex fl1, c2) ->
(match unfold_reference infos fl1 with
| Some def1 ->
eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
- | None -> raise NotConvertible)
- | (_, FFlex fl2) ->
+ | None ->
+ match c2 with
+ | FConstruct ((ind2,j2),u2) ->
+ (try
+ let v2, v1 =
+ eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1)
+ in convert_stacks univ infos lft1 lft2 v1 v2
+ with Not_found -> raise NotConvertible)
+ | _ -> raise NotConvertible)
+
+ | (c1, FFlex fl2) ->
(match unfold_reference infos fl2 with
| Some def2 ->
eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
- | None -> raise NotConvertible)
+ | None ->
+ match c1 with
+ | FConstruct ((ind1,j1),u1) ->
+ (try let v1, v2 =
+ eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2)
+ in convert_stacks univ infos lft1 lft2 v1 v2
+ with Not_found -> raise NotConvertible)
+ | _ -> raise NotConvertible)
(* Inductive types: MutInd MutConstruct Fix Cofix *)
- | (FInd ind1, FInd ind2) ->
- if mind_equiv_infos infos ind1 ind2
- then
- convert_stacks univ infos lft1 lft2 v1 v2
- else raise NotConvertible
+ | (FInd (ind1,u1), FInd (ind2,u2)) ->
+ if mind_equiv_infos infos ind1 ind2
+ then
+ (let () = convert_universes univ u1 u2 in
+ convert_stacks univ infos lft1 lft2 v1 v2)
+ else raise NotConvertible
- | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
- if j1 = j2 && mind_equiv_infos infos ind1 ind2
+ | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+ if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
then
- convert_stacks univ infos lft1 lft2 v1 v2
+ (let () = convert_universes univ u1 u2 in
+ convert_stacks univ infos lft1 lft2 v1 v2)
else raise NotConvertible
+ (* Eta expansion of records *)
+ | (FConstruct ((ind1,j1),u1), _) ->
+ (try
+ let v1, v2 =
+ eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2)
+ in convert_stacks univ infos lft1 lft2 v1 v2
+ with Not_found -> raise NotConvertible)
+
+ | (_, FConstruct ((ind2,j2),u2)) ->
+ (try
+ let v2, v1 =
+ eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1)
+ in convert_stacks univ infos lft1 lft2 v1 v2
+ with Not_found -> raise NotConvertible)
+
| (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
if op1 = op2
then
@@ -353,8 +420,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
- | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
- | (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
+ | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
+ | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
| (FLOCKED,_) | (_,FLOCKED) ) -> assert false
(* In all other cases, terms are not convertible *)
@@ -367,23 +434,25 @@ and convert_stacks univ infos lft1 lft2 stk1 stk2 =
lft1 stk1 lft2 stk2
and convert_vect univ infos lft1 lft2 v1 v2 =
- array_iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
+ Array.iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
-let clos_fconv cv_pb env t1 t2 =
- let infos = create_clos_infos betaiotazeta env in
+let clos_fconv cv_pb eager_delta env t1 t2 =
+ let infos =
+ create_clos_infos
+ (if eager_delta then betadeltaiota else betaiotazeta) env in
let univ = universes env in
ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2)
-let fconv cv_pb env t1 t2 =
+let fconv cv_pb eager_delta env t1 t2 =
if eq_constr t1 t2 then ()
- else clos_fconv cv_pb env t1 t2
+ else clos_fconv cv_pb eager_delta env t1 t2
-let conv = fconv CONV
-let conv_leq = fconv CUMUL
+let conv = fconv CONV false
+let conv_leq = fconv CUMUL false
(* option for conversion : no compilation for the checker *)
-let vm_conv = fconv
+let vm_conv cv_pb = fconv cv_pb true
(********************************************************************)
(* Special-Purpose Reduction *)
@@ -398,7 +467,7 @@ let vm_conv = fconv
let hnf_prod_app env t n =
match whd_betadeltaiota env t with
| Prod (_,_,b) -> subst1 n b
- | _ -> anomaly "hnf_prod_app: Need a product"
+ | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
@@ -416,7 +485,7 @@ let dest_prod env =
in
decrec env empty_rel_context
-(* The same but preserving lets *)
+(* 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
@@ -428,10 +497,29 @@ let dest_prod_assum env =
let d = (x,Some b,t) in
prodec_rec (push_rel d env) (d::l) c
| Cast (c,_,_) -> prodec_rec env l c
- | _ -> l,rty
+ | _ ->
+ let rty' = whd_betadeltaiota env rty in
+ if Term.eq_constr rty' rty then l, rty
+ else prodec_rec env l rty'
in
prodec_rec env empty_rel_context
+let dest_lam_assum env =
+ let rec lamec_rec env l ty =
+ let rty = whd_betadeltaiota_nolet env ty in
+ match rty with
+ | Lambda (x,t,c) ->
+ let d = (x,None,t) in
+ lamec_rec (push_rel d env) (d::l) c
+ | LetIn (x,b,t,c) ->
+ let d = (x,Some b,t) in
+ lamec_rec (push_rel d env) (d::l) c
+ | Cast (c,_,_) -> lamec_rec env l c
+ | _ -> l,rty
+ in
+ lamec_rec env empty_rel_context
+
+
let dest_arity env c =
let l, c = dest_prod_assum env c in
match c with
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 16:21:26 +0000