diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 42 | ||||
| -rw-r--r-- | checker/check_stat.ml | 4 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
3 files changed, 38 insertions, 12 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index e606d60d96..62e732ce69 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string let check mind field b = if not b then raise (InductiveMismatch (mind,field)) -let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = +let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = let open Entries in let nparams = List.length mb.mind_params_ctxt in (* include letins *) let mind_entry_record = match mb.mind_record with @@ -28,7 +28,27 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = | PrimRecord data -> Some (Some (Array.map (fun (x,_,_,_) -> x) data)) in let mind_entry_universes = match mb.mind_universes with - | Monomorphic univs -> Monomorphic_entry univs + | Monomorphic _ -> + (* We only need to rebuild the set of constraints for template polymorphic + inductive types. The set of monomorphic constraints is already part of + the graph at that point, but we need to emulate a broken bound variable + mechanism for template inductive types. *) + let fold accu ind = match ind.mind_arity with + | RegularArity _ -> accu + | TemplateArity ar -> + match accu with + | None -> Some ar.template_context + | Some ctx -> + (* Ensure that all template contexts agree. This is enforced by the + kernel. *) + let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in + Some ctx + in + let univs = match Array.fold_left fold None mb.mind_packets with + | None -> ContextSet.empty + | Some ctx -> ctx + in + Monomorphic_entry univs | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> @@ -69,8 +89,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> Constr.equal ar.mind_user_arity mind_user_arity && Sorts.equal ar.mind_sort mind_sort - | TemplateArity ar, TemplateArity {template_param_levels;template_level} -> + | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} -> List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + ContextSet.equal template_context ar.template_context && UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> assert false @@ -136,7 +157,7 @@ let check_same_record r1 r2 = match r1, r2 with | (NotRecord | FakeRecord | PrimRecord _), _ -> false let check_inductive env mind mb = - let entry = to_entry mb in + let entry = to_entry mind mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes; mind_variance; mind_sec_variance; @@ -144,10 +165,15 @@ let check_inductive env mind mb = = (* Locally set typing flags for further typechecking *) let mb_flags = mb.mind_typing_flags in - let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded; - check_positive = mb_flags.check_positive; - check_universes = mb_flags.check_universes; - conv_oracle = mb_flags.conv_oracle} env in + let env = Environ.set_typing_flags + {env.env_typing_flags with + check_guarded = mb_flags.check_guarded; + check_positive = mb_flags.check_positive; + check_universes = mb_flags.check_universes; + conv_oracle = mb_flags.conv_oracle; + } + env + in Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in diff --git a/checker/check_stat.ml b/checker/check_stat.ml index a67945ae94..8854a23dd5 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -56,7 +56,6 @@ let pr_nonpositive env = let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in pr_assumptions "Inductives whose positivity is assumed" inds - let print_context env = if !output_context then begin Feedback.msg_notice @@ -67,7 +66,8 @@ let print_context env = str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_nonpositive env))) + str "* " ++ hov 0 (pr_nonpositive env ++ fnl())) + ) end let stats env = diff --git a/checker/values.ml b/checker/values.ml index fff166f27b..ed730cff8e 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -228,7 +228,7 @@ let v_oracle = |] let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] + v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -238,7 +238,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |