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/cic.mli | 11 ++++++----- checker/declarations.ml | 18 ++++++++++++------ checker/mod_checking.ml | 2 +- checker/modops.ml | 14 ++++++++------ checker/values.ml | 5 +++-- 5 files changed, 30 insertions(+), 20 deletions(-) (limited to 'checker') diff --git a/checker/cic.mli b/checker/cic.mli index 59dd5bc4d..6724fa3f0 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -385,9 +385,9 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = +and 'a generic_module_body = { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; @@ -397,11 +397,12 @@ and module_body = mod_delta : delta_resolver; mod_retroknowledge : action list } +and module_body = module_implementation generic_module_body + (** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge] *) + implementation and also an empty [mod_retroknowledge] *) -and module_type_body = module_body +and module_type_body = unit generic_module_body (*************************************************************************) (** {4 From safe_typing.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 diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index b6816dd48..de568e636 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -70,7 +70,7 @@ let lookup_module mp env = let mk_mtb mp sign delta = { mod_mp = mp; - mod_expr = Abstract; + mod_expr = (); mod_type = sign; mod_type_alg = None; mod_constraints = Univ.ContextSet.empty; diff --git a/checker/modops.ml b/checker/modops.ml index 79cd5c29f..726988752 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -93,17 +93,19 @@ let strengthen_const mp_from l cb resolver = let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb - else strengthen_body true mp_from mp_to mb + else + let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in + strengthen_body mk_expr mp_from mp_to mb -and strengthen_body is_mod mp_from mp_to mb = +and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun mk_expr mp_from mp_to mb -> match mb.mod_type with | MoreFunctor _ -> mb | NoFunctor sign -> let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta in { mb with - mod_expr = - (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract); + mod_expr = mk_expr mp_to; mod_type = NoFunctor sign_out; mod_delta = resolve_out } @@ -130,7 +132,7 @@ and strengthen_sig mp_from sign mp_to resolver = resolve_out,item::rest' let strengthen mtb mp = - strengthen_body false mtb.mod_mp mp mtb + strengthen_body ignore mtb.mod_mp mp mtb let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) @@ -138,7 +140,7 @@ let subst_and_strengthen mb mp = let module_type_of_module mp mb = let mtb = { mb with - mod_expr = Abstract; + mod_expr = (); mod_type_alg = None; mod_retroknowledge = [] } in diff --git a/checker/values.ml b/checker/values.ml index c95c3f1b2..f1edabcfb 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 c802f941f368bedd96e931cda0559d67 checker/cic.mli +MD5 6bfeaec4872c9636faed4967db1502a0 checker/cic.mli *) @@ -54,6 +54,7 @@ let v_enum name n = Sum(name,n,[||]) let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 +let v_unit = v_enum "unit" 1 let v_ref v = v_tuple "ref" [|v|] let v_set v = @@ -311,7 +312,7 @@ and v_impl = Sum ("module_impl",2, (* Abstract, FullStruct *) [|[|v_mexpr|]; (* Algebraic *) [|v_sign|]|]) (* Struct *) -and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) +and v_noimpl = v_unit and v_module = Tuple ("module_body", [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) -- cgit v1.2.3