diff options
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 34 |
1 files changed, 27 insertions, 7 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 22c8438126..1807ae0ecd 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -502,10 +502,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 = @@ -555,14 +564,23 @@ let check_subtyping cumi paramsctxt env inds = 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 len = AUContext.size (ACumulativityInfo.univ_context cumi) in - let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in + 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_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in - let cumul_cst = UContext.constraints cumul_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 @@ -586,6 +604,8 @@ let check_inductive env kn mib = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in let env = Environ.push_context ind_ctx env in + (** Locally set the oracle for further typechecking *) + let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) @@ -593,13 +613,13 @@ let check_inductive env kn mib = 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 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 *) |