From edf85b925939cb13ca82a10873ced589164391da Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 3 Jan 2015 18:50:53 +0100 Subject: Declarations.mli refactoring: module_type_body = module_body After this commit, module_type_body is a particular case of module_type. For a [module_type_body], the implementation field [mod_expr] is supposed to be always [Abstract]. This is verified by coqchk, even if this isn't so crucial, since [mod_expr] is never read in the case of a module type. Concretely, this amounts to the following rewrite on field names for module_type_body: - typ_expr --> mod_type - typ_expr_alg --> mod_type_alg - typ_* --> mod_* and adding two new fields to mtb: - mod_expr (always containing Abstract) - mod_retroknowledge (always containing []) This refactoring should be completely transparent for the user. Pros: code sharing, for instance subst_modtype = subst_module. Cons: a runtime invariant (mod_expr = Abstract) which isn't enforced by typing. I tried a polymorphic typing of mod_expr, to share field names while not having mtb = mb, but the OCaml typechecker isn't clever enough with polymorphic mutual fixpoints, and reject code sharing (e.g. between subst_modtype and subst_module). In the future (with ocaml>=4), some GADT could maybe help here, but for now the current solution seems good enough. --- checker/subtyping.ml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'checker/subtyping.ml') diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0144580bc..fe88a5071 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -354,52 +354,52 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 = | _ -> error_not_match l spec2 in let env = - add_module_type mtb2.typ_mp mtb2 - (add_module_type mtb1.typ_mp mtb1 env) + add_module_type mtb2.mod_mp mtb2 + (add_module_type mtb1.mod_mp mtb1 env) in check_modtypes env mtb1 mtb2 subst1 subst2 true in List.iter check_one_body sig2 and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = - if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then () + if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type then () else let rec check_structure env str1 str2 equiv subst1 subst2 = match str1,str2 with | NoFunctor (list1), NoFunctor (list2) -> - check_signatures env mtb1.typ_mp list1 list2 subst1 subst2; + check_signatures env mtb1.mod_mp list1 list2 subst1 subst2; if equiv then - check_signatures env mtb2.typ_mp list2 list1 subst1 subst2 + check_signatures env mtb2.mod_mp list2 list1 subst1 subst2 else () | MoreFunctor (arg_id1,arg_t1,body_t1), MoreFunctor (arg_id2,arg_t2,body_t2) -> check_modtypes env arg_t2 arg_t1 - (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2 + (map_mp arg_t1.mod_mp arg_t2.mod_mp) subst2 equiv; (* contravariant *) let env = add_module_type (MPbound arg_id2) arg_t2 env in let env = if is_functor body_t1 then env else - let env = shallow_remove_module mtb1.typ_mp env in - add_module {mod_mp = mtb1.typ_mp; + let env = shallow_remove_module mtb1.mod_mp env in + add_module {mod_mp = mtb1.mod_mp; mod_expr = Abstract; mod_type = body_t1; mod_type_alg = None; - mod_constraints = mtb1.typ_constraints; + mod_constraints = mtb1.mod_constraints; mod_retroknowledge = []; - mod_delta = mtb1.typ_delta} env + mod_delta = mtb1.mod_delta} env in check_structure env body_t1 body_t2 equiv (join (map_mbid arg_id1 (MPbound arg_id2)) subst1) subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 in - check_structure env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2 + check_structure env mtb1.mod_type mtb2.mod_type equiv subst1 subst2 let check_subtypes env sup super = - check_modtypes env (strengthen sup sup.typ_mp) super empty_subst - (map_mp super.typ_mp sup.typ_mp) false + check_modtypes env (strengthen sup sup.mod_mp) super empty_subst + (map_mp super.mod_mp sup.mod_mp) false -- cgit v1.2.3