From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/reduction.ml | 616 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 458 insertions(+), 158 deletions(-) (limited to 'kernel/reduction.ml') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 9982d4ba..4153b323 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* None - | ConstKey cst when not (Cpred.mem cst csts) -> None - | _ -> unfold_reference infos k +let left2right = ref false +let conv_key k = + match k with + VarKey id -> + VarKey id + | ConstKey (cst,_) -> + ConstKey cst + | RelKey n -> RelKey n + let rec is_empty_stack = function - [] -> true + [] -> true | Zupdate _::s -> is_empty_stack s | Zshift _::s -> is_empty_stack s | _ -> false @@ -51,20 +57,24 @@ let el_stack el stk = let compare_stack_shape stk1 stk2 = let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with - ([],[]) -> bal=0 + ([],[]) -> Int.equal bal 0 | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 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) -> - bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 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) -> + Int.equal 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 + Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 | (_,_) -> false in compare_rec 0 stk1 stk2 type lft_constr_stack_elt = Zlapp of (lift * fconstr) array + | Zlproj of 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 @@ -83,9 +93,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,e),(l,pstk)) -> + (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk) | (Zcase(ci,p,br),(l,pstk)) -> (l,Zlcase(ci,l,p,br)::pstk)) in snd (pure_rec lfts stk) @@ -94,17 +108,17 @@ let pure_stack lfts stk = (* Reduction Functions *) (****************************************************************************) -let whd_betaiota t = - whd_val (create_clos_infos betaiota empty_env) (inject t) +let whd_betaiota env t = + whd_val (create_clos_infos betaiota env) (inject t) -let nf_betaiota t = - norm_val (create_clos_infos betaiota empty_env) (inject t) +let nf_betaiota env t = + norm_val (create_clos_infos betaiota env) (inject t) -let whd_betaiotazeta x = +let whd_betaiotazeta env x = match kind_of_term x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x - | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) + | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_betadeltaiota env t = match kind_of_term t with @@ -126,14 +140,14 @@ let beta_appvect c v = Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl | _ -> applist (substl env t, stack) in stacklam [] c (Array.to_list v) - + let betazeta_appvect n c v = let rec stacklam n env t stack = - if n = 0 then applist (substl env t, stack) else + if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack - | _ -> anomaly "Not enough lambda/let's" in + | _ -> anomaly (Pp.str "Not enough lambda/let's") in stacklam n [] c (Array.to_list v) (********************************************************************) @@ -141,19 +155,76 @@ let betazeta_appvect n c v = (********************************************************************) (* Conversion utility functions *) -type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints -type 'a trans_conversion_function = transparent_state -> env -> 'a -> 'a -> Univ.constraints +type 'a conversion_function = env -> 'a -> 'a -> unit +type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function +type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit +type 'a trans_universe_conversion_function = + Names.transparent_state -> 'a universe_conversion_function exception NotConvertible exception NotConvertibleVect of int + +(* Convertibility of sorts *) + +(* The sort cumulativity is + + Prop <= Set <= Type 1 <= ... <= Type i <= ... + + and this holds whatever Set is predicative or impredicative +*) + +type conv_pb = + | CONV + | CUMUL + +let is_cumul = function CUMUL -> true | CONV -> false + +type 'a universe_compare = + { (* Might raise NotConvertible *) + compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; + compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + } + +type 'a universe_state = 'a * 'a universe_compare + +type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b + +type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints + +let sort_cmp_universes env pb s0 s1 (u, check) = + (check.compare env pb s0 s1 u, check) + +let convert_instances flex u u' (s, check) = + (check.compare_instances flex u u' s, check) + +let conv_table_key infos k1 k2 cuniv = + if k1 == k2 then cuniv else + match k1, k2 with + | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> + if Univ.Instance.equal u u' then cuniv + else + let flex = evaluable_constant cst (info_env infos) + && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) + in convert_instances flex u u' cuniv + | VarKey id, VarKey id' when Id.equal id id' -> cuniv + | RelKey n, RelKey n' when Int.equal n n' -> cuniv + | _ -> raise NotConvertible + let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = let rec cmp_rec pstk1 pstk2 cuniv = match (pstk1,pstk2) with | (z1::s1, z2::s2) -> let cu1 = cmp_rec s1 s2 cuniv in (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> array_fold_right2 f a1 a2 cu1 + | (Zlapp a1,Zlapp a2) -> + if !left2right then + Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2 + else Array.fold_right2 f a1 a2 cu1 + | (Zlproj (c1,l1),Zlproj (c2,l2)) -> + if not (eq_constant c1 c2) then + raise NotConvertible + else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 @@ -161,52 +232,21 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = if not (fmind ci1.ci_ind ci2.ci_ind) then raise NotConvertible; let cu2 = f (l1,p1) (l2,p2) cu1 in - array_fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 + Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 | _ -> assert false) | _ -> cuniv in if compare_stack_shape stk1 stk2 then cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv else raise NotConvertible -(* Convertibility of sorts *) - -(* The sort cumulativity is - - Prop <= Set <= Type 1 <= ... <= Type i <= ... - - and this holds whatever Set is predicative or impredicative -*) - -type conv_pb = - | CONV - | CUMUL - -let sort_cmp pb s0 s1 cuniv = - match (s0,s1) with - | (Prop c1, Prop c2) when pb = CUMUL -> - if c1 = Null or c2 = Pos then cuniv (* Prop <= Set *) - else raise NotConvertible - | (Prop c1, Prop c2) -> - if c1 = c2 then cuniv else raise NotConvertible - | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv - | (Type u1, Type u2) -> - assert (is_univ_variable u2); - (match pb with - | CONV -> enforce_eq u1 u2 cuniv - | CUMUL -> enforce_geq u2 u1 cuniv) - | (_, _) -> raise NotConvertible - - -let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint - -let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint - let rec no_arg_available = function | [] -> true | Zupdate _ :: stk -> no_arg_available stk | Zshift _ :: stk -> no_arg_available stk - | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk + | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk + | Zproj _ :: _ -> true | Zcase _ :: _ -> true + | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true let rec no_nth_arg_available n = function @@ -217,7 +257,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 @@ -225,30 +267,45 @@ 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 (_,_,p) :: _ -> 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 unfold_projection infos p c = + let unf = Projection.unfolded p in + if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then + (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with + | Some pb -> + let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + Projection.constant p) in + Some (c, s) + | None -> None) + else None + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = - Util.check_for_interrupt (); + Control.check_for_interrupt (); (* First head reduce both terms *) + let whd = whd_stack (infos_with_reds infos betaiotazeta) in let rec whd_both (t1,stk1) (t2,stk2) = - let st1' = whd_stack (snd infos) t1 stk1 in - let st2' = whd_stack (snd infos) t2 stk2 in + let st1' = whd t1 stk1 in + let st2' = whd t2 stk2 in (* Now, whd_stack on term2 might have modified st1 (due to sharing), and st1 might not be in whnf anymore. If so, we iterate ccnv. *) if in_whnf st1' then (st1',st2') else whd_both st1' st2' in @@ -263,143 +320,228 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match kind_of_term a1, kind_of_term a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly "conversion was given ill-typed terms (Sort)"; - sort_cmp cv_pb s1 s2 cuniv + anomaly (Pp.str "conversion was given ill-typed terms (Sort)"); + sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> - if n=m + if Int.equal n m then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> - if ev1=ev2 then - let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in + if Evar.equal ev1 ev2 then + let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in convert_vect l2r infos el1 el2 (Array.map (mk_clos env1) args1) - (Array.map (mk_clos env2) args2) u1 + (Array.map (mk_clos env2) args2) cuniv else raise NotConvertible (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> - if reloc_rel n el1 = reloc_rel m el2 + if Int.equal (reloc_rel n el1) (reloc_rel m el2) then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* 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 - then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - else raise NotConvertible - with NotConvertible -> - (* else the oracle tells which constant is to be expanded *) - let (app1,app2) = - if Conv_oracle.oracle_order l2r fl1 fl2 then - match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2) - | None -> - (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd_stack (snd infos) def2 v2)) - | None -> raise NotConvertible) - else - match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd_stack (snd infos) def2 v2)) - | None -> - (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2) - | None -> raise NotConvertible) in - eqappr cv_pb l2r infos app1 app2 cuniv) - + (try + let cuniv = conv_table_key infos fl1 fl2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with NotConvertible -> + (* else the oracle tells which constant is to be expanded *) + let oracle = Closure.oracle_of_infos infos in + let (app1,app2) = + if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then + match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd def2 v2)) + | None -> raise NotConvertible) + else + match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd def2 v2)) + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd def1 v1), appr2) + | None -> raise NotConvertible) + in + eqappr cv_pb l2r infos app1 app2 cuniv) + + | (FProj (p1,c1), FProj (p2, c2)) -> + (* Projections: prefer unfolding to first-order unification, + which will happen naturally if the terms c1, c2 are not in constructor + form *) + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + | None -> + match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + | None -> + if Constant.equal (Projection.constant p1) (Projection.constant p2) + && compare_stack_shape v1 v2 then + let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 u1 + else (* Two projections in WHNF: unfold *) + raise NotConvertible) + + | (FProj (p1,c1), t2) -> + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + | None -> + (match t2 with + | FFlex fl2 -> + (match unfold_reference infos fl2 with + | Some def2 -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + | None -> raise NotConvertible) + | _ -> raise NotConvertible)) + + | (t1, FProj (p2,c2)) -> + (match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + | None -> + (match t1 with + | FFlex fl1 -> + (match unfold_reference infos fl1 with + | Some def1 -> + eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + | None -> raise NotConvertible) + | _ -> raise NotConvertible)) + (* other constructors *) | (FLambda _, FLambda _) -> (* Inconsistency: we tolerate that v1, v2 contain shift and update but we throw them away *) if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly "conversion was given ill-typed terms (FLambda)"; + anomaly (Pp.str "conversion was given ill-typed terms (FLambda)"); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in - let u1 = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in - ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 u1 + let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in + ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly "conversion was given ill-typed terms (FProd)"; + anomaly (Pp.str "conversion was given ill-typed terms (FProd)"); (* Luo's system *) - let u1 = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 u1 + let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in + ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv (* Eta-expansion on the fly *) | (FLambda _, _) -> - if v1 <> [] then - anomaly "conversion was given unreduced term (FLambda)"; + let () = match v1 with + | [] -> () + | _ -> + anomaly (Pp.str "conversion was given unreduced term (FLambda)") + in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> - if v2 <> [] then - anomaly "conversion was given unreduced term (FLambda)"; + let () = match v2 with + | [] -> () + | _ -> + anomaly (Pp.str "conversion was given unreduced term (FLambda)") + in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr CONV l2r infos (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv - + (* only one constant, defined var or defined rel *) - | (FFlex fl1, _) -> - (match unfold_reference infos fl1 with - | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv - | None -> raise NotConvertible) - | (_, FFlex fl2) -> - (match unfold_reference infos fl2 with - | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv - | None -> raise NotConvertible) - + | (FFlex fl1, c2) -> + (match unfold_reference infos fl1 with + | Some def1 -> + eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + | None -> + match c2 with + | FConstruct ((ind2,j2),u2) -> + (try + let v2, v1 = + eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) + + | (c1, FFlex fl2) -> + (match unfold_reference infos fl2 with + | Some def2 -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + | None -> + match c1 with + | FConstruct ((ind1,j1),u1) -> + (try let v1, v2 = + eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) + (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd ind1, FInd ind2) -> + | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + (let cuniv = convert_instances false u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible - | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> - if j1 = j2 && eq_ind ind1 ind2 + | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> + if Int.equal j1 j2 && eq_ind ind1 ind2 then - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + (let cuniv = convert_instances false u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible - - | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> - if op1 = op2 + + (* Eta expansion of records *) + | (FConstruct ((ind1,j1),u1), _) -> + (try + let v1, v2 = + eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + + | (_, FConstruct ((ind2,j2),u2)) -> + (try + let v2, v1 = + eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + + | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> + if Int.equal i1 i2 && Array.equal Int.equal op1 op2 then let n = Array.length cl1 in let fty1 = Array.map (mk_clos e1) tys1 in let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in - let u2 = + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect l2r infos - (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in - convert_stacks l2r infos lft1 lft2 v1 v2 u2 + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> - if op1 = op2 + if Int.equal op1 op2 then let n = Array.length cl1 in let fty1 = Array.map (mk_clos e1) tys1 in let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let u1 = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in - let u2 = + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect l2r infos - (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in - convert_stacks l2r infos lft1 lft2 v1 v2 u2 + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv 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 *) @@ -407,53 +549,193 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 c) + (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) (eq_ind) lft1 stk1 lft2 stk2 cuniv and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in let lv2 = Array.length v2 in - if lv1 = lv2 + if Int.equal lv1 lv2 then - let rec fold n univ = - if n >= lv1 then univ + let rec fold n cuniv = + if n >= lv1 then cuniv else - let u1 = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) univ in - fold (n+1) u1 in + let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in + fold (n+1) cuniv in fold 0 cuniv else raise NotConvertible -let clos_fconv trans cv_pb l2r evars env t1 t2 = - let infos = trans, create_clos_infos ~evars betaiotazeta env in - ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) empty_constraint +let clos_fconv trans cv_pb l2r evars env univs t1 t2 = + let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in + let infos = create_clos_infos ~evars reds env in + ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs + + +let check_eq univs u u' = + if not (check_eq univs u u') then raise NotConvertible + +let check_leq univs u u' = + if not (check_leq univs u u') then raise NotConvertible + +let check_sort_cmp_universes env pb s0 s1 univs = + match (s0,s1) with + | (Prop c1, Prop c2) when is_cumul pb -> + begin match c1, c2 with + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible + end + | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible + | (Prop c1, Type u) -> + if not (type_in_type env) then + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) + | (Type u, Prop c) -> raise NotConvertible + | (Type u1, Type u2) -> + if not (type_in_type env) then + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) + +let checked_sort_cmp_universes env pb s0 s1 univs = + check_sort_cmp_universes env pb s0 s1 univs; univs + +let check_convert_instances _flex u u' univs = + if Univ.Instance.check_eq univs u u' then univs + else raise NotConvertible + +let checked_universes = + { compare = checked_sort_cmp_universes; + compare_instances = check_convert_instances } + +let infer_eq (univs, cstrs as cuniv) u u' = + if Univ.check_eq univs u u' then cuniv + else + univs, (Univ.enforce_eq u u' cstrs) -let trans_fconv reds cv_pb l2r evars env t1 t2 = - if eq_constr t1 t2 then empty_constraint - else clos_fconv reds cv_pb l2r evars env t1 t2 +let infer_leq (univs, cstrs as cuniv) u u' = + if Univ.check_leq univs u u' then cuniv + else + let cstrs' = Univ.enforce_leq u u' cstrs in + univs, cstrs' + +let infer_cmp_universes env pb s0 s1 univs = + match (s0,s1) with + | (Prop c1, Prop c2) when is_cumul pb -> + begin match c1, c2 with + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible + end + | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible + | (Prop c1, Type u) -> + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) + | (Type u, Prop c) -> raise NotConvertible + | (Type u1, Type u2) -> + if not (type_in_type env) then + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) + else univs + +let infer_convert_instances flex u u' (univs,cstrs) = + (univs, Univ.enforce_eq_instances u u' cstrs) + +let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare = + { compare = infer_cmp_universes; + compare_instances = infer_convert_instances } + +let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = + let b = + if cv_pb = CUMUL then leq_constr_univs univs t1 t2 + else eq_constr_univs univs t1 t2 + in + if b then () + else + let _ = clos_fconv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in + () + +(* Profiling *) +let trans_fconv_universes = + if Flags.profile then + let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in + Profile.profile8 trans_fconv_universes_key trans_fconv_universes + else trans_fconv_universes + +let trans_fconv reds cv_pb l2r evars env = + trans_fconv_universes reds cv_pb l2r evars env (universes env) let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None) let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars -let fconv = trans_fconv (Idpred.full, Cpred.full) +let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds = + trans_fconv_universes reds CONV l2r evars +let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = + trans_fconv_universes reds CUMUL l2r evars + +let fconv = trans_fconv (Id.Pred.full, Cpred.full) let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None) let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = - array_fold_left2_i - (fun i c t1 t2 -> - let c' = - try conv_leq ~l2r ~evars env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i) in - union_constraints c c') - empty_constraint + Array.fold_left2_i + (fun i _ t1 t2 -> + try conv_leq ~l2r ~evars env t1 t2 + with NotConvertible -> raise (NotConvertibleVect i)) + () v1 v2 +let generic_conv cv_pb l2r evars reds env univs t1 t2 = + let (s, _) = + clos_fconv reds cv_pb l2r evars env univs t1 t2 + in s + +let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = + let b, cstrs = + if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 + else Constr.eq_constr_univs_infer univs t1 t2 + in + if b then cstrs + else + let univs = ((univs, Univ.Constraint.empty), infered_universes) in + let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in + cstrs + +(* Profiling *) +let infer_conv_universes = + if Flags.profile then + let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in + Profile.profile8 infer_conv_universes_key infer_conv_universes + else infer_conv_universes + +let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) + env univs t1 t2 = + infer_conv_universes CONV l2r evars ts env univs t1 t2 + +let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) + env univs t1 t2 = + infer_conv_universes CUMUL l2r evars ts env univs t1 t2 + (* option for conversion *) +let nat_conv = ref (fun cv_pb sigma -> + fconv cv_pb false (sigma.Nativelambda.evars_val)) +let set_nat_conv f = nat_conv := f + +let native_conv cv_pb sigma env t1 t2 = + if eq_constr t1 t2 then () + else begin + let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in + let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in + !nat_conv cv_pb sigma env t1 t2 + end let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) let set_vm_conv f = vm_conv := f @@ -500,7 +782,7 @@ let conv env t1 t2 = let hnf_prod_app env t n = match kind_of_term (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 @@ -518,7 +800,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 @@ -530,10 +812,28 @@ let dest_prod_assum env = let d = (x,Some b,t) in prodec_rec (push_rel d env) (add_rel_decl 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 kind_of_term rty with + | Lambda (x,t,c) -> + let d = (x,None,t) in + lamec_rec (push_rel d env) (add_rel_decl d l) c + | LetIn (x,b,t,c) -> + let d = (x,Some b,t) in + lamec_rec (push_rel d env) (add_rel_decl d l) c + | Cast (c,_,_) -> lamec_rec env l c + | _ -> l,rty + in + lamec_rec env empty_rel_context + exception NotArity let dest_arity env c = -- cgit v1.2.3