From 8589b9b487c1e9b996975bd5dc58f548d0d9280c Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 22 Jun 2015 13:42:13 +0200 Subject: Add a field in `mutual_inductive_body` to represent mutual inductive whose positivity is assumed. --- kernel/indtypes.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 92e121402..72b615cc8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -857,6 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_polymorphic = p; mind_universes = ctx; mind_private = prv; + mind_checked_positive = true; } (************************************************************************) -- cgit v1.2.3 From 9a1e80524e1650311b019fedbd7e774242d80ea4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 09:24:43 +0200 Subject: Add a corresponding field in `mutual_inductive_entry` (part 1). The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been. --- kernel/entries.mli | 5 ++++- kernel/indtypes.ml | 6 +++--- library/declare.ml | 3 ++- toplevel/command.ml | 3 ++- toplevel/discharge.ml | 3 ++- toplevel/record.ml | 3 ++- 6 files changed, 15 insertions(+), 8 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d35..1a27aa9f6 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -51,7 +51,10 @@ type mutual_inductive_entry = { mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; mind_entry_universes : Univ.universe_context; - mind_entry_private : bool option } + mind_entry_private : bool option; + mind_entry_check_positivity : bool; + (** [false] if positivity is to be assumed. *) +} (** {6 Constants (Definition/Axiom) } *) type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 72b615cc8..620c0f6d8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -752,7 +752,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs = +let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs is_checked = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -857,7 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_polymorphic = p; mind_universes = ctx; mind_private = prv; - mind_checked_positive = true; + mind_checked_positive = is_checked; } (************************************************************************) @@ -872,4 +872,4 @@ let check_inductive env kn mie = build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar params kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs + inds nmr recargs mie.mind_entry_check_positivity diff --git a/library/declare.ml b/library/declare.ml index c3181e4c7..02e6dadde 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -366,7 +366,8 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; - mind_entry_private = None }) + mind_entry_private = None; + mind_entry_check_positivity = true; }) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/toplevel/command.ml b/toplevel/command.ml index 1b396d57b..49bd37c69 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -553,7 +553,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = Evd.universe_context evd }, + mind_entry_universes = Evd.universe_context evd; + mind_entry_check_positivity = true; }, impls (* Very syntactical equality *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 7d5d61fb8..df4f77fa1 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -115,5 +115,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs + mind_entry_universes = univs; + mind_entry_check_positivity = mib.mind_checked_positive; } diff --git a/toplevel/record.ml b/toplevel/record.ml index 737b7fb59..2f7215adf 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -365,7 +365,8 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; mind_entry_private = None; - mind_entry_universes = ctx } in + mind_entry_universes = ctx; + mind_entry_check_positivity = true; } in let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in -- cgit v1.2.3 From 4a73e6b2bfb75451bcda7c74cf7478726a459799 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 15:44:31 +0200 Subject: Add a corresponding field in `mutual_inductive_entry` (part 2). The request for positivity to be assumed is honored. --- kernel/indtypes.ml | 46 +++++++++++++++++++++++++++++++--------------- 1 file changed, 31 insertions(+), 15 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 620c0f6d8..3516d4ef6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -480,8 +480,12 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else for use by the guard condition (terms at these positions are considered sub-terms) as well as the number of of non-uniform arguments (used to generate induction schemes, so a priori less - relevant to the kernel). *) -let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = + relevant to the kernel). + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity_one ~chkpos (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = let lparams = rel_context_length hyps in let nmr = rel_context_nhyps hyps in (** Positivity of one argument [c] of a constructor (i.e. the @@ -498,9 +502,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname recursive call. Occurrences in the right-hand side of the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with - None -> failwith_non_pos_list n ntypes [b] + | None when chkpos -> + failwith_non_pos_list n ntypes [b] + | None -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d | Some b -> - check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in let largs = List.map (whd_betadeltaiota env) largs in @@ -512,7 +519,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (** The case where one of the inductives of the mutually inductive block occurs as an argument of another is not known to be safe. So Coq rejects it. *) - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) @@ -527,8 +535,9 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) - if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + if not chkpos || + (noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs) then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) @@ -550,7 +559,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (** Inductives of the inductive block being defined are only allowed to appear nested in the parameters of another inductive type. Not in the proper indices. *) - if not (List.for_all (noccur_between n ntypes) auxlargs) then + if chkpos && + not (List.for_all (noccur_between n ntypes) auxlargs) then failwith_non_pos_list n ntypes auxlargs; (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in @@ -608,7 +618,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname | _ -> raise (IllFormedInd LocalNotConstructor) end else - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs in (nmr, List.rev lrec) @@ -628,9 +639,13 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) -(** [check_positivity kn env_ar params] checks that the mutually - inductive block [inds] is strictly positive. *) -let check_positivity kn env_ar params inds = +(** [check_positivity ~chkpos kn env_ar params] checks that the mutually + inductive block [inds] is strictly positive. + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity ~chkpos kn env_ar params inds = let ntypes = Array.length inds in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = Array.rev_to_list rc in @@ -641,7 +656,7 @@ let check_positivity kn env_ar params inds = List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in let nargs = rel_context_nhyps sign - nmr in - check_positivity_one ienv params (kn,i) nargs lcnames lc + check_positivity_one ~chkpos ienv params (kn,i) nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -866,10 +881,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in + let chkpos = mie.mind_entry_check_positivity in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par params inds in + let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par params inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar params kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs mie.mind_entry_check_positivity + inds nmr recargs chkpos -- cgit v1.2.3