diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-03 18:50:53 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-01-11 09:56:39 +0100 |
commit | edf85b925939cb13ca82a10873ced589164391da (patch) | |
tree | 557735a0f0233f08a49e00169bb2f6afb6f695e2 /checker/mod_checking.ml | |
parent | d103a645df233dd40064e968fa8693607defa6a7 (diff) |
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.
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9e61d3491..998e23c6e 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -64,6 +64,15 @@ let lookup_module mp env = with Not_found -> failwith ("Unknown module: "^string_of_mp mp) +let mk_mtb mp sign delta = + { mod_mp = mp; + mod_expr = Abstract; + mod_type = sign; + mod_type_alg = None; + mod_constraints = Univ.Constraint.empty; + mod_delta = delta; + mod_retroknowledge = []; } + let rec check_module env mp mb = let (_:module_signature) = check_signature env mb.mod_type mb.mod_mp mb.mod_delta @@ -76,25 +85,14 @@ let rec check_module env mp mb = match optsign with |None -> () |Some sign -> - let mtb1 = - {typ_mp=mp; - typ_expr=sign; - typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; - typ_delta = mb.mod_delta;} - and mtb2 = - {typ_mp=mp; - typ_expr=mb.mod_type; - typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; - typ_delta = mb.mod_delta;} - in + let mtb1 = mk_mtb mp sign mb.mod_delta + and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in let env = add_module_type mp mtb1 env in Subtyping.check_subtypes env mtb1 mtb2 and check_module_type env mty = let (_:module_signature) = - check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in + check_signature env mty.mod_type mty.mod_mp mty.mod_delta in () and check_structure_field env mp lab res = function |