diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-18 22:55:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-19 01:23:54 +0200 |
| commit | e2e41c94f1f965e8c7d8bd4a93b58774821c2273 (patch) | |
| tree | a56b3021616cc46179bc994e52503b91ff82096f /checker/mod_checking.ml | |
| parent | 0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff) | |
Fixing the checker w.r.t. wrongly used abstract universe contexts.
It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.
This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 15e9ae295..4948f6008 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,22 +26,21 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Feedback.msg_notice (str " checking cst:" ++ prcon kn); - let env', u = + (** [env'] contains De Bruijn universe variables *) + let env' = match cb.const_universes with - | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty + | Monomorphic_const ctx -> push_context ~strict:true ctx env | Polymorphic_const auctx -> - let ctx = Univ.instantiate_univ_context auctx in - push_context ~strict:false ctx env, Univ.UContext.instance ctx + let ctx = Univ.AUContext.repr auctx in + push_context ~strict:false ctx env in let envty, ty = match cb.const_type with RegularArity ty -> - let ty = subst_instance_constr u ty in let ty', cu = refresh_arity ty in let envty = push_context_set cu env' in let _ = infer_type envty ty' in envty, ty | TemplateArity(ctxt,par) -> - assert(Univ.Instance.is_empty u); let _ = check_ctxt env' ctxt in check_polymorphic_arity env' ctxt par; env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt @@ -49,7 +48,6 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> - let bd = subst_instance_constr u bd in (match cb.const_proj with | None -> let j = infer envty bd in conv_leq envty j ty |