diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-28 14:23:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 17:24:31 +0200 |
| commit | 37b81fe10d2da12180d96d931ba2b76370e1eea5 (patch) | |
| tree | 60559a7e8894147a4fb4884d854d9efb4e404a5b /checker | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 7 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 2 | ||||
| -rw-r--r-- | checker/modops.ml | 4 | ||||
| -rw-r--r-- | checker/subtyping.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
5 files changed, 12 insertions, 7 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 6724fa3f0..753fd0fc0 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -395,7 +395,7 @@ and 'a generic_module_body = mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; - mod_retroknowledge : action list } + mod_retroknowledge : 'a module_retroknowledge; } and module_body = module_implementation generic_module_body @@ -404,6 +404,11 @@ and module_body = module_implementation generic_module_body and module_type_body = unit generic_module_body +and _ module_retroknowledge = +| ModBodyRK : + action list -> module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge + (*************************************************************************) (** {4 From safe_typing.ml} *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index de568e636..3c9e1cac5 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -75,7 +75,7 @@ let mk_mtb mp sign delta = mod_type_alg = None; mod_constraints = Univ.ContextSet.empty; mod_delta = delta; - mod_retroknowledge = []; } + mod_retroknowledge = ModTypeRK; } let rec check_module env mp mb = let (_:module_signature) = diff --git a/checker/modops.ml b/checker/modops.ml index 726988752..f0abc39ea 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -49,7 +49,7 @@ let destr_functor = function | NoFunctor _ -> error_not_a_functor () let module_body_of_type mp mtb = - { mtb with mod_mp = mp; mod_expr = Abstract } + { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] } let rec add_structure mp sign resolver env = let add_one env (l,elem) = @@ -142,7 +142,7 @@ let module_type_of_module mp mb = { mb with mod_expr = (); mod_type_alg = None; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } in match mp with | Some mp -> strengthen {mtb with mod_mp = mp} mp diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 68a467bea..98a9c8250 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -393,7 +393,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = mod_type = body_t1; mod_type_alg = None; mod_constraints = mtb1.mod_constraints; - mod_retroknowledge = []; + mod_retroknowledge = ModBodyRK []; mod_delta = mtb1.mod_delta} env in check_structure env body_t1 body_t2 equiv diff --git a/checker/values.ml b/checker/values.ml index f1edabcfb..afde84854 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 6bfeaec4872c9636faed4967db1502a0 checker/cic.mli +MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli *) @@ -318,7 +318,7 @@ and v_module = [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|]) (** kernel/safe_typing *) |