summaryrefslogtreecommitdiff
path: root/checker/indtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/indtypes.ml')
-rw-r--r--checker/indtypes.ml112
1 files changed, 99 insertions, 13 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open CErrors
@@ -100,7 +102,7 @@ let rec sorts_of_constr_args env t =
let env1 = push_rel (LocalDef (name,def,ty)) env in
sorts_of_constr_args env1 c
| _ when is_constructor_head t -> []
- | _ -> 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... *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 00:48:50 +0000