aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-02-12 22:41:40 +0100
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-02-12 22:43:00 +0100
commit5c603ebd99e4e8e7abb8b2036a6ffac5b19f66cf (patch)
tree5ea51c592bbf3304d1e54616a27313780055892c /kernel
parent43471abd4e61e7528fdaa2c576e7cb825a203c13 (diff)
Univs: fix bug #3978: carry around the universe context used to
typecheck with definitions and thread it accordingly when typechecking module expressions.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/mod_typing.ml27
-rw-r--r--kernel/modops.ml4
3 files changed, 18 insertions, 15 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index bec521227..cef920c6a 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -202,7 +202,7 @@ type ('ty,'a) functorize =
type with_declaration =
| WithMod of Id.t list * module_path
- | WithDef of Id.t list * constr
+ | WithDef of Id.t list * constr Univ.in_universe_context
type module_alg_expr =
| MEident of module_path
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 97c1d1fdf..99d353aae 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -54,7 +54,7 @@ let rec rebuild_mp mp l =
let (+++) = Univ.Constraint.union
-let rec check_with_def env struc (idl,c) mp equiv =
+let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let lab,idl = match idl with
| [] -> assert false
| id::idl -> Label.of_id id, idl
@@ -74,30 +74,33 @@ let rec check_with_def env struc (idl,c) mp equiv =
as long as they have the right type *)
let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
let env' = Environ.add_constraints ccst env' in
+ let newus, cst = Univ.UContext.dest ctx in
+ let env' = Environ.add_constraints cst env' in
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
let typ = Typeops.type_of_constant_type env' cb.const_type in
- let cst = Reduction.infer_conv_leq env' (Environ.universes env')
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
j.uj_type typ in
- j.uj_val,cst
+ j.uj_val,cst' +++ cst
| Def cs ->
- let cst = Reduction.infer_conv env' (Environ.universes env') c
+ let cst' = Reduction.infer_conv env' (Environ.universes env') c
(Mod_subst.force_constr cs) in
let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
- if cb.const_polymorphic then cst
- else ccst +++ cst
+ if cb.const_polymorphic then cst' +++ cst
+ else cst' +++ cst
in
c, cst
in
let def = Def (Mod_subst.from_val c') in
+ let ctx' = Univ.UContext.make (newus, cst) in
let cb' =
{ cb with
const_body = def;
- const_body_code = Cemitcodes.from_val (compile_constant_body env' def) }
- (* const_universes = Future.from_val cst } *)
+ const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
+ const_universes = ctx' }
in
- before@(lab,SFBconst(cb'))::after, c', cst
+ before@(lab,SFBconst(cb'))::after, c', ctx'
else
(* Definition inside a sub-module *)
let mb = match spec with
@@ -108,7 +111,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
| Abstract ->
let struc = Modops.destr_nofunctor mb.mod_type in
let struc',c',cst =
- check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
+ check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta
in
let mb' = { mb with
mod_type = NoFunctor struc';
@@ -204,8 +207,8 @@ let check_with env mp (sign,alg,reso,cst) = function
|WithDef(idl,c) ->
let struc = destr_nofunctor sign in
let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let alg' = mk_alg_with alg (WithDef (idl,c')) in
- (NoFunctor struc'),alg',reso, cst+++cst'
+ let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in
+ (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 392e667b8..83be03ffd 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -177,9 +177,9 @@ let subst_with_body sub = function
|WithMod(id,mp) as orig ->
let mp' = subst_mp sub mp in
if mp==mp' then orig else WithMod(id,mp')
- |WithDef(id,c) as orig ->
+ |WithDef(id,(c,ctx)) as orig ->
let c' = subst_mps sub c in
- if c==c' then orig else WithDef(id,c')
+ if c==c' then orig else WithDef(id,(c',ctx))
let rec subst_structure sub do_delta sign =
let subst_body ((l,body) as orig) = match body with