From 1974816aca996fe3ee9420b83f11d15923e70fda Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Jul 2017 11:41:25 +0200 Subject: Separating the module_type and module_body types by using a type parameter. As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12). --- checker/declarations.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'checker/declarations.ml') diff --git a/checker/declarations.ml b/checker/declarations.ml index 093d999a3..884a1ef18 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -583,24 +583,30 @@ let rec subst_expr sub = function | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd) let rec subst_expression sub me = - functor_map (subst_module sub) (subst_expr sub) me + functor_map (subst_module_type sub) (subst_expr sub) me and subst_signature sub sign = - functor_map (subst_module sub) (subst_structure sub) sign + functor_map (subst_module_type sub) (subst_structure sub) sign and subst_structure sub struc = let subst_body = function | SFBconst cb -> SFBconst (subst_const_body sub cb) | SFBmind mib -> SFBmind (subst_mind sub mib) | SFBmodule mb -> SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb) + | SFBmodtype mtb -> SFBmodtype (subst_module_type sub mtb) in List.map (fun (l,b) -> (l,subst_body b)) struc -and subst_module sub mb = +and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun subst_impl sub mb -> { mb with mod_mp = subst_mp sub mb.mod_mp; - mod_expr = - implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr; + mod_expr = subst_impl sub mb.mod_expr; mod_type = subst_signature sub mb.mod_type; mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg } + +and subst_module sub mb = + subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb + +and subst_module_type sub mb = + subst_body (fun _ () -> ()) sub mb -- cgit v1.2.3