From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- checker/indtypes.ml | 112 ++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 99 insertions(+), 13 deletions(-) (limited to 'checker/indtypes.ml') diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 27f79e79..916934a8 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] - | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") + | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.") (* Prop and Set are small *) @@ -302,11 +304,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") (* Conclusion of constructors: check the inductive type is called with the expected parameters *) @@ -502,10 +504,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc indlc in mk_paths (Mrec ind) irecargs +let prrecarg = function + | Norec -> str "Norec" + | Mrec (mind,i) -> + str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + | Imbr (mind,i) -> + str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + let check_subtree t1 t2 = let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in if not (Rtree.equiv eq_recarg cmp_labels t1 t2) - then failwith "bad recursive trees" + then user_err Pp.(str "Bad recursive tree: found " ++ fnl () + ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl () + ++ Rtree.pp_tree prrecarg t2) (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) let check_positivity env_ar mind params nrecp inds = @@ -524,29 +535,104 @@ let check_positivity env_ar mind params nrecp inds = let wfp = Rtree.mk_rec irecargs in Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity = + let numchecked = ref 0 in + let basic_check ev tp = + if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp); + numchecked := !numchecked + 1 + in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check typ_env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = dest_prod env arcn in + let last_env = fold_rel_context_outside check_typ typs ~init:env in + if not is_arity then basic_check last_env codom else () + +(* Check that the subtyping information inferred for inductive types in the block is correct. *) +(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) +let check_subtyping cumi paramsctxt env inds = + let open Univ in + let numparams = rel_context_nhyps paramsctxt in + (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available. + We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] + and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together + with the cumulativity constraints [ cumul_cst ]. *) + let uctx = ACumulativityInfo.univ_context cumi in + let len = AUContext.size uctx in + let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in + + let other_context = ACumulativityInfo.univ_context cumi in + let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in + let cumul_cst = + Array.fold_left_i (fun i csts var -> + match var with + | Variance.Irrelevant -> csts + | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts + | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts) + Constraint.empty (ACumulativityInfo.variance cumi) + in + let env = Environ.push_context uctx_other env in + let env = Environ.add_constraints cumul_cst env in + + (* process individual inductive types: *) + Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> + match arity with + | RegularArity { mind_user_arity = full_arity} -> + check_subtyping_arity_constructor env inst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc + | TemplateArity _ -> () + ) inds + (************************************************************************) (************************************************************************) let check_inductive env kn mib = Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) - let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in + let env0 = + match mib.mind_universes with + | Monomorphic_ind _ -> env + | Polymorphic_ind auctx -> + let uctx = Univ.AUContext.repr auctx in + Environ.push_context uctx env + | Cumulative_ind cumi -> + let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in + Environ.push_context uctx env + in + (** Locally set the oracle for further typechecking *) + let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) if Array.length mib.mind_packets <> mib.mind_ntypes then - error "not the right number of packets"; + user_err Pp.(str "not the right number of packets"); (* check mind_params_ctxt *) let params = mib.mind_params_ctxt in - let _ = check_ctxt env params in + let _ = check_ctxt env0 params in (* check mind_nparams *) if rel_context_nhyps params <> mib.mind_nparams then - error "number the right number of parameters"; + user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) - let env_ar = typecheck_arity env params mib.mind_packets in + let env_ar = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; + (* check the inferred subtyping relation *) + let () = + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> () + | Cumulative_ind acumi -> + check_subtyping acumi params env_ar mib.mind_packets + in (* check mind_nparams_rec: positivity condition *) check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) -- cgit v1.2.3