diff options
| -rw-r--r-- | checker/environ.ml | 9 | ||||
| -rw-r--r-- | checker/environ.mli | 1 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 28 | ||||
| -rw-r--r-- | checker/subtyping.ml | 6 | ||||
| -rw-r--r-- | checker/subtyping.mli | 3 |
5 files changed, 31 insertions, 16 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index fbe9d9ee25..99b3645794 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -191,6 +191,15 @@ let shallow_add_module mp mb env = env_modules = new_mods } in { env with env_globals = new_globals } +let shallow_remove_module mp env = + if not (MPmap.mem mp env.env_globals.env_modules) then + Printf.ksprintf anomaly "Module %s is unknown" + (string_of_mp mp); + let new_mods = MPmap.remove mp env.env_globals.env_modules in + let new_globals = + { env.env_globals with + env_modules = new_mods } in + { env with env_globals = new_globals } let lookup_module mp env = MPmap.find mp env.env_globals.env_modules diff --git a/checker/environ.mli b/checker/environ.mli index add7c70603..628febbb09 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -69,5 +69,6 @@ val add_modtype : module_path -> Declarations.module_type_body -> env -> env val shallow_add_module : module_path -> Declarations.module_body -> env -> env +val shallow_remove_module : module_path -> env -> env val lookup_module : module_path -> env -> Declarations.module_body val lookup_modtype : module_path -> env -> Declarations.module_type_body diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 315571705c..9942816d12 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -253,18 +253,22 @@ and check_module env mp mb = let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in let (_:struct_expr_body) = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in - check_subtypes env - {typ_mp=mp; - typ_expr=sign; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;} - {typ_mp=mp; - typ_expr=mb.mod_type; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;}; - + let mtb1 = + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} + and mtb2 = + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} + in + let env = add_module (module_body_of_type mp mtb1) env in + check_subtypes env mtb1 mtb2 + and check_structure_field env mp lab res = function | SFBconst cb -> let c = make_con mp empty_dirpath lab in diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0603300baa..0c97254b56 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -348,7 +348,8 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = (module_body_of_type (MPbound arg_id2) arg_t2) env in let env = match body_t1 with - SEBstruct str -> + SEBstruct str -> + let env = shallow_remove_module mtb1.typ_mp env in add_module {mod_mp = mtb1.typ_mp; mod_expr = None; mod_type = body_t1; @@ -367,8 +368,5 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = else check_structure env mtb1' mtb2' equiv subst1 subst2 let check_subtypes env sup super = - (*if sup<>super then*) - let env = add_module (module_body_of_type sup.typ_mp sup) env - in check_modtypes env (strengthen sup sup.typ_mp) super empty_subst (map_mp super.typ_mp sup.typ_mp) false diff --git a/checker/subtyping.mli b/checker/subtyping.mli index 07f48789d9..ecdf557757 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -13,6 +13,9 @@ open Declarations open Environ (*i*) +(** Invariant: the first [module_type_body] is now supposed to be + known by [env] *) + val check_subtypes : env -> module_type_body -> module_type_body -> unit |