diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 483 |
1 files changed, 225 insertions, 258 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2bf9f43a5a..68f53c3556 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -18,7 +18,7 @@ open CErrors open Util open Names -open Term +open Constr open Vars open Environ open CClosure @@ -57,12 +57,14 @@ let compare_stack_shape stk1 stk2 = Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | (_,_) -> false in + | [], _ :: _ + | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false + in compare_rec 0 stk1 stk2 type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of constant * lift + | Zlproj of Constant.t * 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 @@ -107,11 +109,11 @@ let pure_stack lfts stk = (****************************************************************************) let whd_betaiota env t = - match kind_of_term t with + match kind t with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t | _ -> whd_val (create_clos_infos betaiota env) (inject t) end @@ -121,37 +123,46 @@ let nf_betaiota env t = norm_val (create_clos_infos betaiota env) (inject t) let whd_betaiotazeta env x = - match kind_of_term x with - | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| + match kind x with + | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ + | Case _ | Fix _ | CoFix _ | Proj _ -> + whd_val (create_clos_infos betaiotazeta env) (inject x) end - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ -> + whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_all env t = - match kind_of_term t with + match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ -> t - | _ -> whd_val (create_clos_infos all env) (inject t) + | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ + | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> + whd_val (create_clos_infos all env) (inject t) end - | _ -> whd_val (create_clos_infos all env) (inject t) + | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> + whd_val (create_clos_infos all env) (inject t) let whd_allnolet env t = - match kind_of_term t with + match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t - | _ -> whd_val (create_clos_infos allnolet env) (inject t) + | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ + | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> + whd_val (create_clos_infos allnolet env) (inject t) end - | _ -> whd_val (create_clos_infos allnolet env) (inject t) + | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ -> + whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) (* Conversion *) @@ -189,33 +200,79 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> - Univ.Instance.t -> int -> 'a -> 'a; - conv_constructors : (Declarations.mutual_inductive_body * int * int) -> - Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; - } + compare_cumul_instances : Univ.Constraint.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 -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = - (check.compare env pb s0 s1 u, check) + (check.compare_sorts env pb s0 s1 u, check) (* [flex] should be true for constants, false for inductive types and constructors. *) let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) - -let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) = - (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check) -let convert_constructors cons u1 sv1 u2 sv2 (s, check) = - (check.conv_constructors cons u1 sv1 u2 sv2 s, check) +let get_cumulativity_constraints cv_pb cumi u u' = + match cv_pb with + | CONV -> + Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty + | CUMUL -> + Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty + +let inductive_cumulativity_arguments (mind,ind) = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + +let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s = + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); + s + | Declarations.Polymorphic_ind _ -> + cmp_instances u1 u2 s + | Declarations.Cumulative_ind cumi -> + let num_param_arity = inductive_cumulativity_arguments (mind,ind) in + if not (Int.equal num_param_arity nargs) then + cmp_instances u1 u2 s + else + let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in + cmp_cumul csts s + +let convert_inductives cv_pb ind nargs u1 u2 (s, check) = + convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances + cv_pb ind nargs u1 u2 s, check + +let constructor_cumulativity_arguments (mind, ind, ctor) = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in + nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) + +let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); + s + | Declarations.Polymorphic_ind _ -> + cmp_instances u1 u2 s + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in + if not (Int.equal num_cnstr_args nargs) then + cmp_instances u1 u2 s + else + let csts = get_cumulativity_constraints CONV cumi u1 u2 in + cmp_cumul csts s + +let convert_constructors ctor nargs u1 u2 (s, check) = + convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances + ctor nargs u1 u2 s, check let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -239,7 +296,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (eq_constant c1 c2) then + if not (Constant.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> @@ -297,23 +354,12 @@ let in_whnf (t,stk) = | (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 env cv_pb l2r infos lft1 lft2 term1 term2 cuniv = - eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv +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 env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = +and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); (* First head reduce both terms *) let whd = whd_stack (infos_with_reds infos betaiotazeta) in @@ -325,41 +371,44 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if in_whnf st1' then (st1',st2') else whd_both st1' st2' in let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in - (* compute the lifts that apply to the head of the term (hd1 and hd2) *) - let el1 = el_stack lft1 v1 in - let el2 = el_stack lft2 v2 in + (** We delay the computation of the lifts that apply to the head of the term + with [el_stack] inside the branches where they are actually used. *) match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> - (match kind_of_term a1, kind_of_term a2 with + (match kind a1, kind a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then 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 Int.equal n m - then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if Evar.equal ev1 ev2 then - let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in - convert_vect env l2r infos el1 el2 + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + 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) cuniv else raise NotConvertible (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in if Int.equal (reloc_rel n el1) (reloc_rel m el2) - then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + 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 let cuniv = conv_table_key infos fl1 fl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in @@ -379,50 +428,52 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in - eqappr env cv_pb l2r infos app1 app2 cuniv) + 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 env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + (match unfold_projection infos p1 with + | Some s1 -> + eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv | None -> - match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + match unfold_projection infos p2 with + | Some s2 -> + eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then - let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 u1 + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + 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 env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + (match unfold_projection infos p1 with + | Some s1 -> + eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> - (match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + (match unfold_projection infos p2 with + | Some s2 -> + eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -434,15 +485,19 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = 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 cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in - ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + 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 (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) - let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + 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 _, _) -> @@ -452,7 +507,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in - eqappr env CONV l2r infos + eqappr CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> let () = match v2 with @@ -461,34 +516,43 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in - eqappr env CONV l2r infos + 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, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + (** By virtue of the previous case analyses, we know [c2] is rigid. + Conversion check to rigid terms eventually implies full weak-head + reduction, so instead of repeatedly performing small-step + unfoldings, we perform reduction with all flags on. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in + let r1 = whd_stack (infos_with_reds infos all) def1 v1 in + eqappr cv_pb l2r infos (lft1, r1) 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 env l2r infos lft1 lft2 v1 v2 cuniv + 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 env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + (** Symmetrical case of above. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in + let r2 = whd_stack (infos_with_reds infos all) def2 v2 in + eqappr cv_pb l2r infos appr1 (lft2, r2) 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 env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -497,37 +561,30 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) env in - let cuniv = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - convert_instances ~flex:false u1 u2 cuniv - | Declarations.Cumulative_ind cumi -> - convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) cuniv - in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + let mind = Environ.lookup_mind (fst ind1) (info_env infos) in + let nargs = CClosure.stack_args_size v1 in + if not (Int.equal nargs (CClosure.stack_args_size v2)) + then raise NotConvertible + else + let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) env in - let cuniv = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - convert_instances ~flex:false u1 u2 cuniv - | Declarations.Cumulative_ind _ -> - convert_constructors - (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) cuniv - in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + let mind = Environ.lookup_mind (fst ind1) (info_env infos) in + let nargs = CClosure.stack_args_size v1 in + if not (Int.equal nargs (CClosure.stack_args_size v2)) + then raise NotConvertible + else + let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -535,14 +592,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + 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 env l2r infos lft1 lft2 v1 v2 cuniv + 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)) -> @@ -553,11 +610,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = 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 cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect env l2r infos + convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> @@ -568,28 +627,30 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = 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 cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect env l2r infos + convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + 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 _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) - | (FLOCKED,_) | (_,FLOCKED) ) -> assert false + | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false - (* In all other cases, terms are not convertible *) - | _ -> raise NotConvertible + | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ + | FProd _ | FEvar _), _ -> raise NotConvertible -and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv = +and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv) + (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 env l2r infos lft1 lft2 v1 v2 cuniv = +and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in let lv2 = Array.length v2 in if Int.equal lv1 lv2 @@ -597,7 +658,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let rec fold n cuniv = if n >= lv1 then cuniv else - let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv 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 @@ -605,7 +666,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in - ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs + ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs let check_eq univs u u' = @@ -615,6 +676,7 @@ let check_leq univs u u' = if not (UGraph.check_leq univs u u') then raise NotConvertible let check_sort_cmp_universes env pb s0 s1 univs = + let open Sorts in match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with @@ -643,84 +705,14 @@ let check_convert_instances ~flex u u' univs = else raise NotConvertible (* general conversion and inference functions *) -let infer_check_conv_inductives - infer_check_convert_instances - infer_check_inductive_instances - cv_pb (mind, ind) u1 sv1 u2 sv2 univs = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - infer_check_convert_instances ~flex:false u1 u2 univs - | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - if not (num_param_arity = sv1 && num_param_arity = sv2) then - infer_check_convert_instances ~flex:false u1 u2 univs - else - infer_check_inductive_instances cv_pb cumi u1 u2 univs - -let infer_check_conv_constructors - infer_check_convert_instances - infer_check_inductive_instances - (mind, ind, cns) u1 sv1 u2 sv2 univs = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - infer_check_convert_instances ~flex:false u1 u2 univs - | Declarations.Cumulative_ind cumi -> - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) - in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - infer_check_convert_instances ~flex:false u1 u2 univs - else - infer_check_inductive_instances CONV cumi u1 u2 univs - -let check_inductive_instances cv_pb cumi u u' univs = - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - let comp_cst = - match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst - in - if (UGraph.check_constraints comp_cst univs) then univs - else raise NotConvertible - -let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = - infer_check_conv_inductives - check_convert_instances - check_inductive_instances - cv_pb ind u1 sv1 u2 sv2 univs - -let check_conv_constructors cns u1 sv1 u2 sv2 univs = - infer_check_conv_constructors - check_convert_instances - check_inductive_instances - cns u1 sv1 u2 sv2 univs +let check_inductive_instances csts univs = + if (UGraph.check_constraints csts univs) then univs + else raise NotConvertible let checked_universes = - { compare = checked_sort_cmp_universes; + { compare_sorts = checked_sort_cmp_universes; compare_instances = check_convert_instances; - conv_inductives = check_conv_inductives; - conv_constructors = check_conv_constructors} + compare_cumul_instances = check_inductive_instances; } let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv @@ -734,6 +726,7 @@ let infer_leq (univs, cstrs as cuniv) u u' = univs, cstrs' let infer_cmp_universes env pb s0 s1 univs = + let open Sorts in match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with @@ -762,49 +755,13 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - let comp_cst = - match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst - in - (univs, Univ.Constraint.union cstrs comp_cst) - - -let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = - infer_check_conv_inductives - infer_convert_instances - infer_inductive_instances - cv_pb ind u1 sv1 u2 sv2 univs - -let infer_conv_constructors cns u1 sv1 u2 sv2 univs = - infer_check_conv_constructors - infer_convert_instances - infer_inductive_instances - cns u1 sv1 u2 sv2 univs - -let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = - { compare = infer_cmp_universes; +let infer_inductive_instances csts (univs,csts') = + (univs, Univ.Constraint.union csts csts') + +let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = + { compare_sorts = infer_cmp_universes; compare_instances = infer_convert_instances; - conv_inductives = infer_conv_inductives; - conv_constructors = infer_conv_constructors} + compare_cumul_instances = infer_inductive_instances; } let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = @@ -820,8 +777,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then - let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in + CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs else gen_conv cv_pb l2r reds env evars univs let conv = gen_conv CONV @@ -847,8 +804,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = (* 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 + let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in + CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) @@ -869,7 +826,7 @@ let warn_bytecode_compiler_failed = (fun () -> strbrk "Bytecode compiler failed, " ++ strbrk "falling back to standard conversion") -let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f +let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 @@ -882,22 +839,22 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = let default_conv_leq = default_conv CUMUL (* -let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; +let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = - Profile.profile4 convleqkey conv_leq env t1 t2;; + CProfile.profile4 convleqkey conv_leq env t1 t2;; -let convkey = Profile.declare_profile "Kernel_reduction.conv";; +let convkey = CProfile.declare_profile "Kernel_reduction.conv";; let conv env t1 t2 = - Profile.profile4 convleqkey conv env t1 t2;; + CProfile.profile4 convleqkey conv env t1 t2;; *) (* Application with on-the-fly reduction *) let beta_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l - | _ -> applist (substl subst c, l) in + | _ -> Term.applist (substl subst c, l) in app [] c l let beta_appvect c v = beta_applist c (Array.to_list v) @@ -905,7 +862,7 @@ let beta_appvect c v = beta_applist c (Array.to_list v) let beta_app c a = beta_applist c [a] (* Compatibility *) -let betazeta_appvect = lambda_appvect_assum +let betazeta_appvect = Term.lambda_appvect_assum (********************************************************************) (* Special-Purpose Reduction *) @@ -918,19 +875,31 @@ let betazeta_appvect = lambda_appvect_assum * error message. *) let hnf_prod_app env t n = - match kind_of_term (whd_all env t) with + match kind (whd_all env t) with | Prod (_,_,b) -> subst1 n b | _ -> 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 +let hnf_prod_applist_assum env n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Too many arguments.") + else match kind (whd_allnolet env t), l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Dealing with arities *) let dest_prod env = let rec decrec env m c = let t = whd_all env c in - match kind_of_term t with + match kind t with | Prod (n,a,c0) -> let d = LocalAssum (n,a) in decrec (push_rel d env) (Context.Rel.add d m) c0 @@ -942,17 +911,16 @@ let dest_prod env = let dest_prod_assum env = let rec prodec_rec env l ty = let rty = whd_allnolet env ty in - match kind_of_term rty with + match kind rty with | Prod (x,t,c) -> let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c - | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_all env rty in - if Term.eq_constr rty' rty then l, rty + if Constr.equal rty' rty then l, rty else prodec_rec env l rty' in prodec_rec env Context.Rel.empty @@ -960,14 +928,13 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = let rty = whd_allnolet env ty in - match kind_of_term rty with + match kind rty with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c - | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in lamec_rec env Context.Rel.empty @@ -976,7 +943,7 @@ exception NotArity let dest_arity env c = let l, c = dest_prod_assum env c in - match kind_of_term c with + match kind c with | Sort s -> l,s | _ -> raise NotArity |