diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 22 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 5 | ||||
| -rw-r--r-- | kernel/reduction.ml | 260 | ||||
| -rw-r--r-- | kernel/reduction.mli | 22 | ||||
| -rw-r--r-- | kernel/term.ml | 6 | ||||
| -rw-r--r-- | kernel/term.mli | 12 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/univ.ml | 136 | ||||
| -rw-r--r-- | kernel/univ.mli | 58 |
9 files changed, 267 insertions, 257 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b117f8714b..cfca335d32 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = CumulativityInfo.subtyping_susbst cumi in - let dosubst = subst_univs_level_constr sbsubst in let uctx = CumulativityInfo.univ_context cumi in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in + let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) + LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + in + let dosubst = subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env = Environ.push_context uctx env_ar in let env = Environ.push_context uctx_other env in - let env = push_context (CumulativityInfo.subtyp_context cumi) env in + let subtyp_constraints = + CumulativityInfo.leq_constraints cumi + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> () + | TemplateArity _ -> + anomaly ~label:"check_subtyping" + Pp.(str "template polymorphism and cumulative polymorphism are not compatible") ) inds (* Type-check an inductive definition. Does not check positivity diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 4e7d6b218c..1e35f6c036 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -157,9 +157,8 @@ let call_linker ?(fatal=true) prefix f upds = register_native_file prefix with Dynlink.Error e as exn -> let exn = CErrors.push exn in - let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); + if fatal then iraise exn + else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1724f210db..da7042713f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -200,13 +200,9 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> Sorts.t -> Sorts.t -> '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 @@ -215,18 +211,68 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a 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 @@ -325,9 +371,8 @@ and eqappr 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) -> @@ -343,6 +388,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if Evar.equal ev1 ev2 then + 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) @@ -351,6 +398,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 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 l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -395,6 +444,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then + 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 *) @@ -434,6 +485,8 @@ and eqappr 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 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 @@ -441,6 +494,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = 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 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 @@ -509,15 +564,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos) 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 l2r infos lft1 lft2 v1 v2 cuniv + 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)) -> @@ -527,16 +579,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos) 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 l2r infos lft1 lft2 v1 v2 cuniv + 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 *) @@ -562,6 +610,8 @@ and eqappr 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 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 l2r infos @@ -577,6 +627,8 @@ and eqappr 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 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 l2r infos @@ -653,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 @@ -773,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 = @@ -936,6 +882,18 @@ let hnf_prod_app env t n = 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 = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 573e4c8bde..6f7e3f8f8f 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -35,15 +35,11 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL -type 'a universe_compare = +type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> Sorts.t -> Sorts.t -> '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 @@ -51,6 +47,12 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> + Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t + +val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int +val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int + val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare @@ -103,6 +105,12 @@ val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> constr diff --git a/kernel/term.ml b/kernel/term.ml index fae990d45f..a4c92bd333 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -352,10 +352,11 @@ let lambda_applist_assum 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 "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Lambda(_,_,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 lambda/let's.") in app n [] c l @@ -377,10 +378,11 @@ let prod_applist_assum 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 "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term 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 diff --git a/kernel/term.mli b/kernel/term.mli index c9a8cf6e1e..b4597676a3 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr val lambda_appvect : constr -> constr array -> constr (** In [lambda_applist_assum n c args], [c] is supposed to have the - form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) val lambda_applist_assum : int -> constr -> constr list -> constr @@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) -val prod_appvect : constr -> constr array -> constr -val prod_applist : constr -> constr list -> constr +val prod_appvect : types -> constr array -> types +val prod_applist : types -> constr list -> types (** In [prod_appvect_assum n c args], [c] is supposed to have the - form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) -val prod_appvect_assum : int -> constr -> constr array -> constr -val prod_applist_assum : int -> constr -> constr list -> constr +val prod_appvect_assum : int -> types -> constr array -> types +val prod_applist_assum : int -> types -> constr list -> types (** {5 Other term destructors. } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5f501bff10..9b864440d1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -223,9 +223,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let feedback_completion_typecheck = - let open Feedback in Option.iter (fun state_id -> - feedback ~id:state_id Feedback.Complete) + Feedback.feedback ~id:state_id Feedback.Complete) let abstract_constant_universes = function | Monomorphic_const_entry uctx -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 835dbee087..fbb0473644 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -745,7 +745,48 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -module Instance : sig +module Variance = +struct + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + let sup x y = + match x, y with + | Irrelevant, s | s, Irrelevant -> s + | Invariant, _ | _, Invariant -> Invariant + | Covariant, Covariant -> Covariant + + let pr = function + | Irrelevant -> str "*" + | Covariant -> str "+" + | Invariant -> str "=" + + let leq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant -> enforce_leq_level u u' csts + | Invariant -> enforce_eq_level u u' csts + + let eq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant | Invariant -> enforce_eq_level u u' csts + + let leq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 leq_constraint csts variance u u' + + let eq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 eq_constraint csts variance u u' +end + +module Instance : sig type t = Level.t array val empty : t @@ -765,7 +806,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : (Level.t -> Pp.t) -> t -> Pp.t + val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t val levels : t -> LSet.t end = struct @@ -841,8 +882,12 @@ struct let levels x = LSet.of_array x - let pr = - prvect_with_sep spc + let pr prl ?variance = + let ppu i u = + let v = Option.map (fun v -> v.(i)) variance in + pr_opt_no_spc Variance.pr v ++ prl u + in + prvecti_with_sep spc ppu let equal t u = t == u || @@ -906,9 +951,9 @@ struct let empty = (Instance.empty, Constraint.empty) let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst - let pr prl (univs, cst as ctx) = + let pr prl ?variance (univs, cst as ctx) = if is_empty ctx then mt() else - h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) + h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -944,66 +989,42 @@ end type abstract_universe_context = AUContext.t let hcons_abstract_universe_context = AUContext.hcons -(** Universe info for cumulative inductive types: - A context of universe levels - with universe constraints, representing local universe variables - and constraints, together with a context of universe levels with - universe constraints, representing conditions for subtyping used - for inductive types. +(** Universe info for cumulative inductive types: A context of + universe levels with universe constraints, representing local + universe variables and constraints, together with an array of + Variance.t. - This data structure maintains the invariant that the context for - subtyping constraints is exactly twice as big as the context for - universe constraints. *) + This data structure maintains the invariant that the variance + array has the same length as the universe instance. *) module CumulativityInfo = struct - type t = universe_context * universe_context + type t = universe_context * Variance.t array let make x = - if (Instance.length (UContext.instance (snd x))) = - (Instance.length (UContext.instance (fst x))) * 2 then x + if (Instance.length (UContext.instance (fst x))) = + (Array.length (snd x)) then x else anomaly (Pp.str "Invalid subtyping information encountered!") - let empty = (UContext.empty, UContext.empty) - let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst + let empty = (UContext.empty, [||]) + let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance - let halve_context ctx = - let len = Array.length (Instance.to_array ctx) in - let halflen = len / 2 in - (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), - Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen)) + let pr prl (univs, variance) = + UContext.pr prl ~variance univs - let pr prl (univcst, subtypcst) = - if UContext.is_empty univcst then mt() else - let (ctx, ctx') = halve_context (UContext.instance subtypcst) in - (UContext.pr prl univcst) ++ fnl () ++ fnl () ++ - h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ") - ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) + let hcons (univs, variance) = (* should variance be hconsed? *) + (UContext.hcons univs, variance) - let hcons (univcst, subtypcst) = - (UContext.hcons univcst, UContext.hcons subtypcst) - - let univ_context (univcst, subtypcst) = univcst - let subtyp_context (univcst, subtypcst) = subtypcst - - let create_trivial_subtyping ctx ctx' = - CArray.fold_left_i - (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst) - Constraint.empty (Instance.to_array ctx) + let univ_context (univs, subtypcst) = univs + let variance (univs, variance) = variance (** This function takes a universe context representing constraints - of an inductive and a Instance.t of fresh universe names for the - subtyping (with the same length as the context in the given - universe context) and produces a UInfoInd.t that with the - trivial subtyping relation. *) - let from_universe_context univcst freshunivs = - let inst = (UContext.instance univcst) in - assert (Instance.length freshunivs = Instance.length inst); - (univcst, UContext.make (Instance.append inst freshunivs, - create_trivial_subtyping inst freshunivs)) - - let subtyping_susbst (univcst, subtypcst) = - let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in - Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' + of an inductive and produces a CumulativityInfo.t with the + trivial subtyping relation. *) + let from_universe_context univs = + (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant)) + + let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts + let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts end @@ -1171,10 +1192,9 @@ let abstract_universes ctx = let ctx = UContext.make (instance, cstrs) in instance, ctx -let abstract_cumulativity_info (univcst, substcst) = - let instance, univcst = abstract_universes univcst in - let _, substcst = abstract_universes substcst in - (instance, (univcst, substcst)) +let abstract_cumulativity_info (univs, variance) = + let subst, univs = abstract_universes univs in + subst, (univs, variance) (** Pretty-printing *) diff --git a/kernel/univ.mli b/kernel/univ.mli index f550872ba8..c45ebe21cc 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -245,6 +245,20 @@ type universe_level_subst_fn = Level.t -> Level.t type universe_subst = Universe.t universe_map type universe_level_subst = Level.t universe_map +module Variance : +sig + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + val sup : t -> t -> t + + val pr : t -> Pp.t + +end + (** {6 Universe instances} *) module Instance : @@ -280,7 +294,7 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val pr : (Level.t -> Pp.t) -> t -> Pp.t + val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t (** Pretty-printing, no comments *) val levels : t -> LSet.t @@ -354,36 +368,32 @@ end type abstract_universe_context = AUContext.t [@@ocaml.deprecated "Use AUContext.t"] -(** Universe info for inductive types: A context of universe levels - with universe Constraint.t, representing local universe variables - and Constraint.t, together with a context of universe levels with - universe Constraint.t, representing conditions for subtyping used - for inductive types. +(** Universe info for cumulative inductive types: A context of + universe levels with universe constraints, representing local + universe variables and constraints, together with an array of + Variance.t. - This data structure maintains the invariant that the context for - subtyping Constraint.t is exactly twice as big as the context for - universe Constraint.t. *) + This data structure maintains the invariant that the variance + array has the same length as the universe instance. *) module CumulativityInfo : sig type t - val make : UContext.t * UContext.t -> t + val make : UContext.t * Variance.t array -> t val empty : t val is_empty : t -> bool val univ_context : t -> UContext.t - val subtyp_context : t -> UContext.t - - (** This function takes a universe context representing Constraint.t - of an inductive and a Instance.t of fresh universe names for the - subtyping (with the same length as the context in the given - universe context) and produces a UInfoInd.t that with the - trivial subtyping relation. *) - val from_universe_context : UContext.t -> Instance.t -> t + val variance : t -> Variance.t array - val subtyping_susbst : t -> universe_level_subst + (** This function takes a universe context representing constraints + of an inductive and produces a CumulativityInfo.t with the + trivial subtyping relation. *) + val from_universe_context : UContext.t -> t + val leq_constraints : t -> Instance.t constraint_function + val eq_constraints : t -> Instance.t constraint_function end type cumulativity_info = CumulativityInfo.t @@ -394,7 +404,9 @@ sig type t val univ_context : t -> AUContext.t - val subtyp_context : t -> AUContext.t + val variance : t -> Variance.t array + val leq_constraints : t -> Instance.t constraint_function + val eq_constraints : t -> Instance.t constraint_function end type abstract_cumulativity_info = ACumulativityInfo.t @@ -488,9 +500,11 @@ val make_abstract_instance : AUContext.t -> Instance.t val pr_constraint_type : constraint_type -> Pp.t val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t -val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> + UContext.t -> Pp.t val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t -val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t +val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> + AUContext.t -> Pp.t val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t val explain_universe_inconsistency : (Level.t -> Pp.t) -> |