diff options
| -rw-r--r-- | interp/modintern.ml | 4 | ||||
| -rw-r--r-- | kernel/declarations.mli | 2 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 27 | ||||
| -rw-r--r-- | kernel/modops.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 |
5 files changed, 22 insertions, 17 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index fdc6e609b..bf0b2f980 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,7 +61,9 @@ let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> - WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*) + let c, ectx = interp_constr env (Evd.from_env env) c in + let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in + WithDef (fqid,(c,ctx)) let loc_of_module = function | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc 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 diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 42e69d342..90ee6d0ef 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -235,7 +235,7 @@ let rec extract_structure_spec env mp = function and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp - | MEwith(me',WithDef(idl,c))-> + | MEwith(me',WithDef(idl,(c,ctx)))-> let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in let mt = extract_mexpr_spec env mp1 (me_struct,me') in (match extract_with_type env' c with (* cb may contain some kn *) |