diff options
31 files changed, 1402 insertions, 1791 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index fd3351674..0b732e4b9 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -276,8 +276,30 @@ type mutual_inductive_body = { mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) } -(** {6 Modules: signature component specifications, module types, and - module declarations } *) +(** {6 Module declarations } *) + +(** Functor expressions are forced to be on top of other expressions *) + +type ('ty,'a) functorize = + | NoFunctor of 'a + | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize + +(** The fully-algebraic module expressions : names, applications, 'with ...'. + They correspond to the user entries of non-interactive modules. + They will be later expanded into module structures in [Mod_typing], + and won't play any role into the kernel after that : they are kept + only for short module printing and for extraction. *) + +type with_declaration = + | WithMod of Id.t list * module_path + | WithDef of Id.t list * constr + +type module_alg_expr = + | MEident of module_path + | MEapply of module_alg_expr * module_path + | MEwith of module_alg_expr * with_declaration + +(** A component of a module structure *) type structure_field_body = | SFBconst of constant_body @@ -285,45 +307,51 @@ type structure_field_body = | SFBmodule of module_body | SFBmodtype of module_type_body -and structure_body = (label * structure_field_body) list +(** A module structure is a list of labeled components. + + Note : we may encounter now (at most) twice the same label in + a [structure_body], once for a module ([SFBmodule] or [SFBmodtype]) + and once for an object ([SFBconst] or [SFBmind]) *) + +and structure_body = (Label.t * structure_field_body) list + +(** A module signature is a structure, with possibly functors on top of it *) + +and module_signature = (module_type_body,structure_body) functorize + +(** A module expression is an algebraic expression, possibly functorized. *) + +and module_expression = (module_type_body,module_alg_expr) functorize -and struct_expr_body = - | SEBident of module_path - | SEBfunctor of MBId.t * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints - | SEBstruct of structure_body - | SEBwith of struct_expr_body * with_declaration_body +and module_implementation = + | Abstract (** no accessible implementation *) + | Algebraic of module_expression (** non-interactive algebraic expression *) + | Struct of module_signature (** interactive body *) + | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and with_declaration_body = - With_module_body of Id.t list * module_path - | With_definition_body of Id.t list * constant_body and module_body = - { (** absolute path of the module *) - mod_mp : module_path; - (** Implementation *) - mod_expr : struct_expr_body option; - (** Signature *) - mod_type : struct_expr_body; - (** algebraic structure expression is kept - if it's relevant for extraction *) - mod_type_alg : struct_expr_body option; - (** set of all constraint in the module *) - mod_constraints : Univ.constraints; - (** quotiented set of equivalent constant and inductive name *) - mod_delta : delta_resolver; - mod_retroknowledge : action list} + { mod_mp : module_path; (** absolute path of the module *) + mod_expr : module_implementation; (** implementation *) + mod_type : module_signature; (** expanded type *) + (** algebraic type, kept if it's relevant for extraction *) + mod_type_alg : module_expression option; + (** set of all constraints in the module *) + mod_constraints : Univ.constraints; + (** quotiented set of equivalent constants and inductive names *) + mod_delta : delta_resolver; + mod_retroknowledge : action list } + +(** A [module_type_body] is similar to a [module_body], with + no implementation and retroknowledge fields *) and module_type_body = - { - (** Path of the module type *) - typ_mp : module_path; - typ_expr : struct_expr_body; - (** algebraic structure expression is kept - if it's relevant for extraction *) - typ_expr_alg : struct_expr_body option ; - typ_constraints : Univ.constraints; - (** quotiented set of equivalent constant and inductive name *) - typ_delta : delta_resolver} + { typ_mp : module_path; (** path of the module type *) + typ_expr : module_signature; (** expanded type *) + (** algebraic expression, kept if it's relevant for extraction *) + typ_expr_alg : module_expression option; + typ_constraints : Univ.constraints; + (** quotiented set of equivalent constants and inductive names *) + typ_delta : delta_resolver} (*************************************************************************) diff --git a/checker/declarations.ml b/checker/declarations.ml index 0981cfd1a..eec76ba39 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -529,71 +529,50 @@ let subst_mind sub mib = (* Modules *) -let rec subst_with_body sub = function - | With_module_body(id,mp) -> - With_module_body(id,subst_mp sub mp) - | With_definition_body(id,cb) -> - With_definition_body( id,subst_const_body sub cb) +let rec functor_map fty f0 = function + | NoFunctor a -> NoFunctor (f0 a) + | MoreFunctor (mbid,ty,e) -> MoreFunctor(mbid,fty ty,functor_map fty f0 e) + +let implem_map fs fa = function + | Struct s -> Struct (fs s) + | Algebraic a -> Algebraic (fa a) + | impl -> impl + +let subst_with_body sub = function + | WithMod(id,mp) -> WithMod(id,subst_mp sub mp) + | WithDef(id,c) -> WithDef(id,subst_mps sub c) + +let rec subst_expr sub = function + | MEident mp -> MEident (subst_mp sub mp) + | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2) + | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd) + +let rec subst_expression sub me = + functor_map (subst_modtype sub) (subst_expr sub) me + +and subst_signature sub sign = + functor_map (subst_modtype sub) (subst_structure sub) sign and subst_modtype sub mtb= - let typ_expr' = subst_struct_expr sub mtb.typ_expr in - let typ_alg' = - Option.smartmap - (subst_struct_expr sub) mtb.typ_expr_alg in - let mp = subst_mp sub mtb.typ_mp - in - if typ_expr'==mtb.typ_expr && - typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then - mtb - else - {mtb with - typ_mp = mp; - typ_expr = typ_expr'; - typ_expr_alg = typ_alg'} + { mtb with + typ_mp = subst_mp sub mtb.typ_mp; + typ_expr = subst_signature sub mtb.typ_expr; + typ_expr_alg = Option.smartmap (subst_expression sub) mtb.typ_expr_alg } -and 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_modtype sub mtb) + | 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_modtype sub mtb) in - List.map (fun (l,b) -> (l,subst_body b)) sign - + List.map (fun (l,b) -> (l,subst_body b)) struc and subst_module sub mb = - let mtb' = subst_struct_expr sub mb.mod_type in - let typ_alg' = Option.smartmap - (subst_struct_expr sub ) mb.mod_type_alg in - let me' = Option.smartmap - (subst_struct_expr sub) mb.mod_expr in - let mp = subst_mp sub mb.mod_mp in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mp == mb.mod_mp - then mb else - { mb with - mod_mp = mp; - mod_expr = me'; - mod_type_alg = typ_alg'; - mod_type=mtb'} - -and subst_struct_expr sub = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (mbid, mtb, meb') -> - SEBfunctor(mbid,subst_modtype sub mtb - ,subst_struct_expr sub meb') - | SEBstruct (str)-> - SEBstruct( subst_structure sub str) - | SEBapply (meb1,meb2,cst)-> - SEBapply(subst_struct_expr sub meb1, - subst_struct_expr sub meb2, - cst) - | SEBwith (meb,wdb)-> - SEBwith(subst_struct_expr sub meb, - subst_with_body sub wdb) - + { mb with + mod_mp = subst_mp sub mb.mod_mp; + mod_expr = + implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr; + mod_type = subst_signature sub mb.mod_type; + mod_type_alg = Option.map (subst_expression sub) mb.mod_type_alg } diff --git a/checker/declarations.mli b/checker/declarations.mli index 64234e8cd..ab74114d5 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -37,9 +37,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive val subst_const_body : constant_body subst_fun val subst_mind : mutual_inductive_body subst_fun -val subst_modtype : substitution -> module_type_body -> module_type_body -val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body -val subst_structure : substitution -> structure_body -> structure_body +val subst_signature : substitution -> module_signature -> module_signature val subst_module : substitution -> module_body -> module_body val join : substitution -> substitution -> substitution diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 66f1194d3..b0f20da70 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -13,8 +13,7 @@ open Subtyping open Declarations open Environ -(************************************************************************) -(* Checking constants *) +(** {6 Checking constants } *) let refresh_arity ar = let ctxt, hd = decompose_prod_assum ar in @@ -43,339 +42,95 @@ let check_constant_declaration env kn cb = check_polymorphic_arity env ctxt par); add_constant kn cb env -(************************************************************************) -(* Checking modules *) +(** {6 Checking modules } *) -exception Not_path - -let path_of_mexpr = function - | SEBident mp -> mp - | _ -> raise Not_path - -let is_modular = function - | SFBmodule _ | SFBmodtype _ -> true - | SFBconst _ | SFBmind _ -> false - -let rec list_split_assoc ((k,m) as km) rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after - | h::tail -> list_split_assoc km (h::rev_before) tail - -let check_definition_sub env cb1 cb2 = - let check_type env t1 t2 = - - (* If the type of a constant is generated, it may mention - non-variable algebraic universes that the general conversion - algorithm is not ready to handle. Anyway, generated types of - constants are functions of the body of the constant. If the - bodies are the same in environments that are subtypes one of - the other, the types are subtypes too (i.e. if Gamma <= Gamma', - Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). - Hence they don't have to be checked again *) - - let t1,t2 = - if isArity t2 then - let (ctx2,s2) = destArity t2 in - match s2 with - | Type v when not (Univ.is_univ_variable v) -> - (* The type in the interface is inferred and is made of algebraic - universes *) - begin try - let (ctx1,s1) = dest_arity env t1 in - match s1 with - | Type u when not (Univ.is_univ_variable u) -> - (* Both types are inferred, no need to recheck them. We - cheat and collapse the types to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | Prop _ -> - (* The type in the interface is inferred, it may be the case - that the type in the implementation is smaller because - the body is more reduced. We safely collapse the upper - type to Prop *) - mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) - | Type _ -> - (* The type in the interface is inferred and the type in the - implementation is not inferred or is inferred but from a - more reduced body so that it is just a variable. Since - constraints of the form "univ <= max(...)" are not - expressible in the system of algebraic universes: we fail - (the user has to use an explicit type in the interface *) - raise Reduction.NotConvertible - with UserError _ (* "not an arity" *) -> - raise Reduction.NotConvertible end - | _ -> t1,t2 - else - (t1,t2) in - Reduction.conv_leq env t1 t2 - in - (*Start by checking types*) - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_type env typ1 typ2; - (* In the spirit of subtyping.check_constant, we accept - any implementations of parameters and opaques terms, - as long as they have the right type *) - (match cb2.const_body with - | Undef _ | OpaqueDef _ -> () - | Def lc2 -> - (match cb1.const_body with - | Def lc1 -> - let c1 = force_constr lc1 in - let c2 = force_constr lc2 in - Reduction.conv env c1 c2 - (* Coq only places transparent cb in With_definition_body *) - | _ -> assert false)) - -let lookup_modtype mp env = - try Environ.lookup_modtype mp env - with Not_found -> - failwith ("Unknown module type: "^string_of_mp mp) +(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields. + The only delicate part is when [mod_expr] is an algebraic expression : + we need to expand it before checking it is indeed a subtype of [mod_type]. + Fortunately, [mod_expr] cannot contain any [MEwith]. *) let lookup_module mp env = try Environ.lookup_module mp env with Not_found -> failwith ("Unknown module: "^string_of_mp mp) -let rec check_with env mtb with_decl mp= - match with_decl with - | With_definition_body (idl,c) -> - check_with_def env mtb (idl,c) mp; - mtb - | With_module_body (idl,mp1) -> - check_with_mod env mtb (idl,mp1) mp; - mtb - -and check_with_def env mtb (idl,c) mp = - let sig_b = match mtb with - | SEBstruct(sig_b) -> - sig_b - | _ -> error_signature_expected mtb +let rec check_module env mp mb = + let (_:module_signature) = + check_signature env mb.mod_type mb.mod_mp mb.mod_delta in - let id,idl = match idl with - | [] -> assert false - | id::idl -> id,idl + let optsign = match mb.mod_expr with + |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta) + |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta) + |Abstract|FullStruct -> None in - let l = Label.of_id id in - try - let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in - let before = List.rev rev_before in - let env' = Modops.add_signature mp before empty_delta_resolver env in - if idl = [] then - let cb = match spec with - SFBconst cb -> cb - | _ -> error_not_a_constant l - in - check_definition_sub env' c cb - else - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - begin - match old.mod_expr with - | None -> - check_with_def env' old.mod_type (idl,c) (MPdot(mp,l)) - | Some msb -> - error_a_generative_module_expected l - end - with - Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l - -and check_with_mod env mtb (idl,mp1) mp = - let sig_b = - match mtb with - | SEBstruct(sig_b) -> - sig_b - | _ -> error_signature_expected mtb in - let id,idl = match idl with - | [] -> assert false - | id::idl -> id,idl - in - let l = Label.of_id id in - try - let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in - let before = List.rev rev_before in - let env' = Modops.add_signature mp before empty_delta_resolver env in - if idl = [] then - let _ = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - let (_:module_body) = (Environ.lookup_module mp1 env) in () - else - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - begin - match old.mod_expr with - None -> - check_with_mod env' - old.mod_type (idl,mp1) (MPdot(mp,l)) - | Some msb -> - error_a_generative_module_expected l - end - with - Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l + match optsign with + |None -> () + |Some sign -> + let mtb1 = + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} + and mtb2 = + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.empty_constraint; + typ_delta = 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 (_:struct_expr_body) = - check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in + let (_:module_signature) = + check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in () - -and check_module env mp mb = - match mb.mod_expr, mb.mod_type with - | None,mtb -> - let (_:struct_expr_body) = - check_modtype env mtb mb.mod_mp mb.mod_delta in () - | Some mexpr, mtb when mtb==mexpr -> - let (_:struct_expr_body) = - check_modtype env mtb mb.mod_mp mb.mod_delta in () - | Some mexpr, _ -> - let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in - let (_:struct_expr_body) = - check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in - let mtb1 = - {typ_mp=mp; - typ_expr=sign; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;} - and mtb2 = - {typ_mp=mp; - typ_expr=mb.mod_type; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;} - in - let env = add_module (module_body_of_type mp mtb1) env in - check_subtypes env mtb1 mtb2 - and check_structure_field env mp lab res = function | SFBconst cb -> let c = Constant.make2 mp lab in - check_constant_declaration env c cb + check_constant_declaration env c cb | SFBmind mib -> let kn = MutInd.make2 mp lab in let kn = mind_of_delta res kn in - Indtypes.check_inductive env kn mib + Indtypes.check_inductive env kn mib | SFBmodule msb -> - let (_:unit) = check_module env (MPdot(mp,lab)) msb in - Modops.add_module msb env + let () = check_module env (MPdot(mp,lab)) msb in + Modops.add_module msb env | SFBmodtype mty -> check_module_type env mty; add_modtype (MPdot(mp,lab)) mty env - -and check_modexpr env mse mp_mse res = match mse with - | SEBident mp -> + +and check_mexpr env mse mp_mse res = match mse with + | MEident mp -> let mb = lookup_module mp env in (subst_and_strengthen mb mp_mse).mod_type - | SEBfunctor (arg_id, mtb, body) -> - check_module_type env mtb ; - let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in - let sign = check_modexpr env' body mp_mse res in - SEBfunctor (arg_id, mtb, sign) - | SEBapply (f,m,cst) -> - let sign = check_modexpr env f mp_mse res in - let farg_id, farg_b, fbody_b = destr_functor env sign in - let mp = - try (path_of_mexpr m) - with Not_path -> error_application_to_not_path m - (* place for nondep_supertype *) in - let mtb = module_type_of_module (Some mp) (lookup_module mp env) in - check_subtypes env mtb farg_b; - (subst_struct_expr (map_mbid farg_id mp) fbody_b) - | SEBwith(mte, with_decl) -> - let sign = check_modexpr env mte mp_mse res in - let sign = check_with env sign with_decl mp_mse in - sign - | SEBstruct(msb) -> - let (_:env) = List.fold_left (fun env (lab,mb) -> - check_structure_field env mp_mse lab res mb) env msb in - SEBstruct(msb) - -and check_modtype env mse mp_mse res = match mse with - | SEBident mp -> - let mtb = lookup_modtype mp env in - mtb.typ_expr - | SEBfunctor (arg_id, mtb, body) -> - check_module_type env mtb; - let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in - let body = check_modtype env' body mp_mse res in - SEBfunctor(arg_id,mtb,body) - | SEBapply (f,m,cst) -> - let sign = check_modtype env f mp_mse res in - let farg_id, farg_b, fbody_b = destr_functor env sign in - let mp = - try (path_of_mexpr m) - with Not_path -> error_application_to_not_path m - (* place for nondep_supertype *) in + | MEapply (f,mp) -> + let sign = check_mexpr env f mp_mse res in + let farg_id, farg_b, fbody_b = destr_functor sign in let mtb = module_type_of_module (Some mp) (lookup_module mp env) in - check_subtypes env mtb farg_b; - subst_struct_expr (map_mbid farg_id mp) fbody_b - | SEBwith(mte, with_decl) -> - let sign = check_modtype env mte mp_mse res in - let sign = check_with env sign with_decl mp_mse in - sign - | SEBstruct(msb) -> - let (_:env) = List.fold_left (fun env (lab,mb) -> - check_structure_field env mp_mse lab res mb) env msb in - SEBstruct(msb) - -(* - let rec add_struct_expr_constraints env = function - | SEBident _ -> env - - | SEBfunctor (_,mtb,meb) -> - add_struct_expr_constraints - (add_modtype_constraints env mtb) meb - - | SEBstruct (_,structure_body) -> - List.fold_left - (fun env (l,item) -> add_struct_elem_constraints env item) - env - structure_body - - | SEBapply (meb1,meb2,cst) -> -(* let g = Univ.merge_constraints cst Univ.initial_universes in -msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ - Univ.pr_universes g++str"============="++fnl()); -*) - Environ.add_constraints cst - (add_struct_expr_constraints - (add_struct_expr_constraints env meb1) - meb2) - | SEBwith(meb,With_definition_body(_,cb))-> - Environ.add_constraints cb.const_constraints - (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_,cst))-> - Environ.add_constraints cst - (add_struct_expr_constraints env meb) + check_subtypes env mtb farg_b; + subst_signature (map_mbid farg_id mp) fbody_b + | MEwith _ -> error_with_module () -and add_struct_elem_constraints env = function - | SFBconst cb -> Environ.add_constraints cb.const_constraints env - | SFBmind mib -> Environ.add_constraints mib.mind_constraints env - | SFBmodule mb -> add_module_constraints env mb - | SFBalias (mp,Some cst) -> Environ.add_constraints cst env - | SFBalias (mp,None) -> env - | SFBmodtype mtb -> add_modtype_constraints env mtb - -and add_module_constraints env mb = - let env = match mb.mod_expr with - | None -> env - | Some meb -> add_struct_expr_constraints env meb - in - let env = match mb.mod_type with - | None -> env - | Some mtb -> - add_struct_expr_constraints env mtb - in - Environ.add_constraints mb.mod_constraints env +and check_mexpression env sign mp_mse res = match sign with + | MoreFunctor (arg_id, mtb, body) -> + check_module_type env mtb; + let env' = add_module_type (MPbound arg_id) mtb env in + let body = check_mexpression env' body mp_mse res in + MoreFunctor(arg_id,mtb,body) + | NoFunctor me -> check_mexpr env me mp_mse res -and add_modtype_constraints env mtb = - add_struct_expr_constraints env mtb.typ_expr -*) +and check_signature env sign mp_mse res = match sign with + | MoreFunctor (arg_id, mtb, body) -> + check_module_type env mtb; + let env' = add_module_type (MPbound arg_id) mtb env in + let body = check_signature env' body mp_mse res in + MoreFunctor(arg_id,mtb,body) + | NoFunctor struc -> + let (_:env) = List.fold_left (fun env (lab,mb) -> + check_structure_field env mp_mse lab res mb) env struc + in + NoFunctor struc diff --git a/checker/modops.ml b/checker/modops.ml index 20f330812..89ffcb50b 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -19,7 +19,7 @@ open Declarations let error_not_a_constant l = error ("\""^(Label.to_string l)^"\" is not a constant") -let error_not_a_functor _ = error "Application of not a functor" +let error_not_a_functor () = error "Application of not a functor" let error_incompatible_modtypes _ _ = error "Incompatible module types" @@ -38,61 +38,52 @@ let error_not_a_module_loc loc s = let error_not_a_module s = error_not_a_module_loc Loc.ghost s -let error_with_incorrect l = - error ("Incorrect constraint for label \""^(Label.to_string l)^"\"") +let error_with_module () = + error "Unsupported 'with' constraint in module implementation" -let error_a_generative_module_expected l = - error ("The module " ^ Label.to_string l ^ " is not generative. Only " ^ - "component of generative modules can be changed using the \"with\" " ^ - "construct.") +let is_functor = function + | MoreFunctor _ -> true + | NoFunctor _ -> false -let error_signature_expected mtb = - error "Signature expected" +let destr_functor = function + | MoreFunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) + | NoFunctor _ -> error_not_a_functor () -let error_application_to_not_path _ = error "Application to not path" - -let destr_functor env mtb = - match mtb with - | SEBfunctor (arg_id,arg_t,body_t) -> - (arg_id,arg_t,body_t) - | _ -> error_not_a_functor mtb - -let module_body_of_type mp mtb = +let module_body_of_type mp mtb = { mod_mp = mp; mod_type = mtb.typ_expr; mod_type_alg = mtb.typ_expr_alg; - mod_expr = None; + mod_expr = Abstract; mod_constraints = mtb.typ_constraints; mod_delta = mtb.typ_delta; mod_retroknowledge = []} -let rec add_signature mp sign resolver env = +let rec add_structure mp sign resolver env = let add_one env (l,elem) = let kn = KerName.make2 mp l in let con = Constant.make1 kn in let mind = mind_of_delta resolver (MutInd.make1 kn) in match elem with - | SFBconst cb -> + | SFBconst cb -> (* let con = constant_of_delta resolver con in*) Environ.add_constant con cb env - | SFBmind mib -> + | SFBmind mib -> (* let mind = mind_of_delta resolver mind in*) Environ.add_mind mind mib env | SFBmodule mb -> add_module mb env (* adds components as well *) | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env in - List.fold_left add_one env sign + List.fold_left add_one env sign -and add_module mb env = +and add_module mb env = let mp = mb.mod_mp in let env = Environ.shallow_add_module mp mb env in - match mb.mod_type with - | SEBstruct (sign) -> - add_signature mp sign mb.mod_delta env - | SEBfunctor _ -> env - | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") + match mb.mod_type with + | NoFunctor struc -> add_structure mp struc mb.mod_delta env + | MoreFunctor _ -> env +let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env let strengthen_const mp_from l cb resolver = match cb.const_body with @@ -107,20 +98,20 @@ let rec strengthen_mod mp_from mp_to mb = mb else match mb.mod_type with - | SEBstruct (sign) -> - let resolve_out,sign_out = - strengthen_sig mp_from sign mp_to mb.mod_delta in - { mb with - mod_expr = Some (SEBident mp_to); - mod_type = SEBstruct(sign_out); - mod_type_alg = mb.mod_type_alg; - mod_constraints = mb.mod_constraints; - mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to - (add_delta_resolver mb.mod_delta resolve_out)*); - mod_retroknowledge = mb.mod_retroknowledge} - | SEBfunctor _ -> mb - | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") - + | NoFunctor (sign) -> + let resolve_out,sign_out = + strengthen_sig mp_from sign mp_to mb.mod_delta + in + { mb with + mod_expr = Algebraic (NoFunctor (MEident mp_to)); + mod_type = NoFunctor sign_out; + mod_type_alg = mb.mod_type_alg; + mod_constraints = mb.mod_constraints; + mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to + (add_delta_resolver mb.mod_delta resolve_out)*); + mod_retroknowledge = mb.mod_retroknowledge} + | MoreFunctor _ -> mb + and strengthen_sig mp_from sign mp_to resolver = match sign with | [] -> empty_delta_resolver,[] @@ -139,21 +130,20 @@ and strengthen_sig mp_from sign mp_to resolver = let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in resolve_out (*add_delta_resolver resolve_out mb.mod_delta*), item':: rest' - | (l,SFBmodtype mty as item) :: rest -> + | (l,SFBmodtype mty as item) :: rest -> let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in resolve_out,item::rest' -let strengthen mtb mp = - match mtb.typ_expr with - | SEBstruct (sign) -> - let resolve_out,sign_out = - strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in - {mtb with - typ_expr = SEBstruct(sign_out); - typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta - (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} - | SEBfunctor _ -> mtb - | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") +let strengthen mtb mp = match mtb.typ_expr with + | NoFunctor sign -> + let resolve_out,sign_out = + strengthen_sig mtb.typ_mp sign mp mtb.typ_delta + in + { mtb with + typ_expr = NoFunctor sign_out; + typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta + (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} + | MoreFunctor _ -> mtb let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) @@ -161,17 +151,16 @@ let subst_and_strengthen mb mp = let module_type_of_module mp mb = match mp with - Some mp -> - strengthen { - typ_mp = mp; - typ_expr = mb.mod_type; - typ_expr_alg = None; - typ_constraints = mb.mod_constraints; - typ_delta = mb.mod_delta} mp - - | None -> - {typ_mp = mb.mod_mp; - typ_expr = mb.mod_type; - typ_expr_alg = None; - typ_constraints = mb.mod_constraints; - typ_delta = mb.mod_delta} + | Some mp -> + strengthen { + typ_mp = mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} mp + | None -> + { typ_mp = mb.mod_mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} diff --git a/checker/modops.mli b/checker/modops.mli index 0b94edb54..396eb8e7c 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -15,20 +15,18 @@ open Environ (* Various operations on modules and module types *) -(* make the envirconment entry out of type *) -val module_body_of_type : module_path -> module_type_body -> module_body +val module_type_of_module : + module_path option -> module_body -> module_type_body -val module_type_of_module : module_path option -> module_body -> - module_type_body +val is_functor : ('ty,'a) functorize -> bool -val destr_functor : - env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body - -val add_signature : module_path -> structure_body -> delta_resolver -> env -> env +val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize (* adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env +val add_module_type : module_path -> module_type_body -> env -> env + val strengthen : module_type_body -> module_path -> module_type_body val subst_and_strengthen : module_body -> module_path -> module_body @@ -38,19 +36,13 @@ val error_incompatible_modtypes : val error_not_match : label -> structure_field_body -> 'a -val error_with_incorrect : label -> 'a +val error_with_module : unit -> 'a val error_no_such_label : label -> 'a val error_no_such_label_sub : label -> module_path -> 'a -val error_signature_expected : struct_expr_body -> 'a - val error_not_a_constant : label -> 'a val error_not_a_module : label -> 'a - -val error_a_generative_module_expected : label -> 'a - -val error_application_to_not_path : struct_expr_body -> 'a diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 150e99bc9..7903c33c5 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -320,55 +320,52 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 = | Modtype mtb -> mtb | _ -> error_not_match l spec2 in - let env = add_module (module_body_of_type mtb2.typ_mp mtb2) - (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in - check_modtypes env mtb1 mtb2 subst1 subst2 true + let env = + add_module_type mtb2.typ_mp mtb2 + (add_module_type mtb1.typ_mp mtb1 env) + in + check_modtypes env mtb1 mtb2 subst1 subst2 true in - List.iter check_one_body sig2 + List.iter check_one_body sig2 -and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = - if mtb1==mtb2 then () else - let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in - let rec check_structure env str1 str2 equiv subst1 subst2 = - match str1,str2 with - | SEBstruct (list1), - SEBstruct (list2) -> - check_signatures env - mtb1.typ_mp list1 list2 subst1 subst2; - if equiv then - check_signatures env - mtb2.typ_mp list2 list1 subst1 subst2 - else - () - | SEBfunctor (arg_id1,arg_t1,body_t1), - SEBfunctor (arg_id2,arg_t2,body_t2) -> - check_modtypes env - arg_t2 arg_t1 - (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2 - equiv ; - (* contravariant *) - let env = add_module - (module_body_of_type (MPbound arg_id2) arg_t2) env - in - let env = match body_t1 with - SEBstruct str -> - let env = shallow_remove_module mtb1.typ_mp env in - add_module {mod_mp = mtb1.typ_mp; - mod_expr = None; - mod_type = body_t1; - mod_type_alg= None; - mod_constraints=mtb1.typ_constraints; - mod_retroknowledge = []; - mod_delta = mtb1.typ_delta} env - | _ -> 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 - if mtb1'== mtb2' then () - else check_structure env mtb1' mtb2' equiv subst1 subst2 +and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr 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; + if equiv then + check_signatures env mtb2.typ_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 + 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; + mod_expr = Abstract; + mod_type = body_t1; + mod_type_alg = None; + mod_constraints = mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_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 let check_subtypes env sup super = check_modtypes env (strengthen sup sup.typ_mp) super empty_subst diff --git a/checker/values.ml b/checker/values.ml index 974d3431e..b39d90548 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 43e0b61e2a549058ae0a59bbadbb9d61 checker/cic.mli +MD5 09a4e5d657809e040f50837a78fe6dfe checker/cic.mli *) @@ -248,6 +248,18 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_cstrs; Any|] +let v_with = + Sum ("with_declaration_body",0, + [|[|List v_id;v_mp|]; + [|List v_id;v_constr|]|]) + +let rec v_mae = + Sum ("module_alg_expr",0, + [|[|v_mp|]; (* SEBident *) + [|v_mae;v_mp|]; (* SEBapply *) + [|v_mae;v_with|] (* SEBwith *) + |]) + let rec v_sfb = Sum ("struct_field_body",0, [|[|v_cb|]; (* SFBconst *) @@ -255,27 +267,25 @@ let rec v_sfb = [|v_module|]; (* SFBmodule *) [|v_modtype|] (* SFBmodtype *) |]) -and v_sb = List (Tuple ("label*sfb",[|v_id;v_sfb|])) -and v_seb = - Sum ("struct_expr_body",0, - [|[|v_mp|]; (* SEBident *) - [|v_uid;v_modtype;v_seb|]; (* SEBfunctor *) - [|v_seb;v_seb;v_cstrs|]; (* SEBapply *) - [|v_sb|]; (* SEBstruct *) - [|v_seb;v_with|] (* SEBwith *) - |]) -and v_with = - Sum ("with_declaration_body",0, - [|[|List v_id;v_mp|]; - [|List v_id;v_cb|]|]) +and v_struc = List (Tuple ("label*sfb",[|v_id;v_sfb|])) +and v_sign = + Sum ("module_sign",0, + [|[|v_struc|]; (* NoFunctor *) + [|v_uid;v_modtype;v_sign|]|]) (* MoreFunctor *) +and v_mexpr = + Sum ("module_expr",0, + [|[|v_mae|]; (* NoFunctor *) + [|v_uid;v_modtype;v_mexpr|]|]) (* MoreFunctor *) +and v_impl = + Sum ("module_impl",2, + [|[|v_mexpr|]; (* Algebraic *) + [|v_sign|]|]) (* Struct *) and v_module = Tuple ("module_body", - [|v_mp;Opt v_seb;v_seb; - Opt v_seb;v_cstrs;v_resolver;Any|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_seb;Opt v_seb;v_cstrs;v_resolver|]) - + [|v_mp;v_sign;Opt v_mexpr;v_cstrs;v_resolver|]) (** kernel/safe_typing *) diff --git a/interp/modintern.ml b/interp/modintern.ml index d809f0221..8f8e2df93 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Declarations open Entries open Libnames open Constrexpr @@ -59,34 +60,32 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> - With_Module (fqid,lookup_module qid) + WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> - With_Definition (fqid,interp_constr Evd.empty env c) + WithDef (fqid,interp_constr Evd.empty env c) let loc_of_module = function | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc -let is_path = function - | CMident _ -> true - | CMapply _ | CMwith _ -> false - (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) let rec interp_module_ast env kind = function | CMident qid -> let (mp,kind) = lookup_module_or_modtype kind qid in - (MSEident mp, kind) + (MEident mp, kind) | CMapply (_,me1,me2) -> let me1',kind1 = interp_module_ast env kind me1 in let me2',kind2 = interp_module_ast env ModAny me2 in - if not (is_path me2) then - error_application_to_not_path (loc_of_module me2) me2'; + let mp2 = match me2' with + | MEident mp -> mp + | _ -> error_application_to_not_path (loc_of_module me2) me2' + in if kind2 == ModType then error_application_to_module_type (loc_of_module me2); - (MSEapply (me1',me2'), kind1) + (MEapply (me1',mp2), kind1) | CMwith (loc,me,decl) -> let me,kind = interp_module_ast env kind me in if kind == Module then error_incorrect_with_in_module loc; let decl = transl_with_decl env decl in - (MSEwith(me,decl), kind) + (MEwith(me,decl), kind) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 5cb406ffa..6a5b0dbb2 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -155,8 +155,30 @@ type mutual_inductive_body = { } -(** {6 Modules: signature component specifications, module types, and - module declarations } *) +(** {6 Module declarations } *) + +(** Functor expressions are forced to be on top of other expressions *) + +type ('ty,'a) functorize = + | NoFunctor of 'a + | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize + +(** The fully-algebraic module expressions : names, applications, 'with ...'. + They correspond to the user entries of non-interactive modules. + They will be later expanded into module structures in [Mod_typing], + and won't play any role into the kernel after that : they are kept + only for short module printing and for extraction. *) + +type with_declaration = + | WithMod of Id.t list * module_path + | WithDef of Id.t list * constr + +type module_alg_expr = + | MEident of module_path + | MEapply of module_alg_expr * module_path + | MEwith of module_alg_expr * with_declaration + +(** A component of a module structure *) type structure_field_body = | SFBconst of constant_body @@ -164,47 +186,58 @@ type structure_field_body = | SFBmodule of module_body | SFBmodtype of module_type_body -(** NB: we may encounter now (at most) twice the same label in +(** A module structure is a list of labeled components. + + Note : we may encounter now (at most) twice the same label in a [structure_body], once for a module ([SFBmodule] or [SFBmodtype]) and once for an object ([SFBconst] or [SFBmind]) *) and structure_body = (Label.t * structure_field_body) list -and struct_expr_body = - | SEBident of module_path - | SEBfunctor of MBId.t * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints - | SEBstruct of structure_body - | SEBwith of struct_expr_body * with_declaration_body +(** A module signature is a structure, with possibly functors on top of it *) + +and module_signature = (module_type_body,structure_body) functorize + +(** A module expression is an algebraic expression, possibly functorized. *) -and with_declaration_body = - With_module_body of Id.t list * module_path - | With_definition_body of Id.t list * constant_body +and module_expression = (module_type_body,module_alg_expr) functorize + +and module_implementation = + | Abstract (** no accessible implementation *) + | Algebraic of module_expression (** non-interactive algebraic expression *) + | Struct of module_signature (** interactive body *) + | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) and module_body = - { (** absolute path of the module *) - mod_mp : module_path; - (** Implementation *) - mod_expr : struct_expr_body option; - (** Signature *) - mod_type : struct_expr_body; - (** algebraic structure expression is kept - if it's relevant for extraction *) - mod_type_alg : struct_expr_body option; - (** set of all constraint in the module *) - mod_constraints : Univ.constraints; - (** quotiented set of equivalent constant and inductive name *) - mod_delta : Mod_subst.delta_resolver; - mod_retroknowledge : Retroknowledge.action list} + { mod_mp : module_path; (** absolute path of the module *) + mod_expr : module_implementation; (** implementation *) + mod_type : module_signature; (** expanded type *) + (** algebraic type, kept if it's relevant for extraction *) + mod_type_alg : module_expression option; + (** set of all constraints in the module *) + mod_constraints : Univ.constraints; + (** quotiented set of equivalent constants and inductive names *) + mod_delta : Mod_subst.delta_resolver; + mod_retroknowledge : Retroknowledge.action list } + +(** A [module_type_body] is similar to a [module_body], with + no implementation and retroknowledge fields *) and module_type_body = - { - (** Path of the module type *) - typ_mp : module_path; - typ_expr : struct_expr_body; - (** algebraic structure expression is kept - if it's relevant for extraction *) - typ_expr_alg : struct_expr_body option ; - typ_constraints : Univ.constraints; - (** quotiented set of equivalent constant and inductive name *) - typ_delta : Mod_subst.delta_resolver} + { typ_mp : module_path; (** path of the module type *) + typ_expr : module_signature; (** expanded type *) + (** algebraic expression, kept if it's relevant for extraction *) + typ_expr_alg : module_expression option; + typ_constraints : Univ.constraints; + (** quotiented set of equivalent constants and inductive names *) + typ_delta : Mod_subst.delta_resolver} + +(** Extra invariants : + + - No [MEwith] inside a [mod_expr] implementation : the 'with' syntax + is only supported for module types + + - A module application is atomic, for instance ((M N) P) : + * the head of [MEapply] can only be another [MEapply] or a [MEident] + * the argument of [MEapply] is now directly forced to be a [module_path]. +*) diff --git a/kernel/entries.mli b/kernel/entries.mli index 3b7a2fd19..b78372c0e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -67,16 +67,14 @@ type constant_entry = (** {6 Modules } *) -type module_struct_entry = - MSEident of module_path - | MSEfunctor of MBId.t * module_struct_entry * module_struct_entry - | MSEwith of module_struct_entry * with_declaration - | MSEapply of module_struct_entry * module_struct_entry - -and with_declaration = - With_Module of Id.t list * module_path - | With_Definition of Id.t list * constr - -and module_entry = - { mod_entry_type : module_struct_entry option; - mod_entry_expr : module_struct_entry option} +type module_struct_entry = Declarations.module_alg_expr + +type module_params_entry = + (MBId.t * module_struct_entry) list (** older first *) + +type module_type_entry = module_params_entry * module_struct_entry + +type module_entry = + | MType of module_params_entry * module_struct_entry + | MExpr of + module_params_entry * module_struct_entry * module_struct_entry option diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index d5555c624..7794f19be 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -20,17 +20,13 @@ open Environ open Modops open Mod_subst -exception Not_path - -let path_of_mexpr = function - | MSEident mp -> mp - | _ -> raise Not_path +type 'alg translation = + module_signature * 'alg option * delta_resolver * Univ.constraints let rec mp_from_mexpr = function - | MSEident mp -> mp - | MSEapply (expr,_) -> mp_from_mexpr expr - | MSEfunctor (_,_,expr) -> mp_from_mexpr expr - | MSEwith (expr,_) -> mp_from_mexpr expr + | MEident mp -> mp + | MEapply (expr,_) -> mp_from_mexpr expr + | MEwith (expr,_) -> mp_from_mexpr expr let is_modular = function | SFBmodule _ | SFBmodtype _ -> true @@ -39,7 +35,7 @@ let is_modular = function (** Split a [structure_body] at some label corresponding to a modular definition or not. *) -let split_sign k m struc = +let split_struc k m struc = let rec split rev_before = function | [] -> raise Not_found | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> @@ -48,8 +44,8 @@ let split_sign k m struc = in split [] struc let discr_resolver mtb = match mtb.typ_expr with - | SEBstruct _ -> mtb.typ_delta - | _ -> empty_delta_resolver (* when mp is a functor *) + | NoFunctor _ -> mtb.typ_delta + | MoreFunctor _ -> empty_delta_resolver let rec rebuild_mp mp l = match l with @@ -58,19 +54,15 @@ let rec rebuild_mp mp l = let (+++) = Univ.union_constraints -let rec check_with_def env sign (idl,c) mp equiv = - let sig_b = match sign with - | SEBstruct(sig_b) -> sig_b - | _ -> error_signature_expected sign - in +let rec check_with_def env struc (idl,c) mp equiv = let lab,idl = match idl with | [] -> assert false | id::idl -> Label.of_id id, idl in try let modular = not (List.is_empty idl) in - let before,spec,after = split_sign lab modular sig_b in - let env' = Modops.add_signature mp before equiv env in + let before,spec,after = split_struc lab modular struc in + let env' = Modops.add_structure mp before equiv env in if List.is_empty idl then (* Toplevel definition *) let cb = match spec with @@ -80,27 +72,26 @@ let rec check_with_def env sign (idl,c) mp equiv = (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, as long as they have the right type *) - let def,cst = match cb.const_body with + let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j,cst1 = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in let cst2 = Reduction.conv_leq env' j.uj_type typ in let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in - let def = Def (Lazyconstr.from_val j.uj_val) in - def,cst + j.uj_val,cst | Def cs -> let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in let cst = Future.force cb.const_constraints +++ cst1 in - let def = Def (Lazyconstr.from_val c) in - def,cst + c, cst in + let def = Def (Lazyconstr.from_val c') in let cb' = { cb with const_body = def; const_body_code = Cemitcodes.from_val (compile_constant_body env' def); const_constraints = Future.from_val cst } in - SEBstruct(before@(lab,SFBconst(cb'))::after),cb',cst + before@(lab,SFBconst(cb'))::after, c', cst else (* Definition inside a sub-module *) let mb = match spec with @@ -108,33 +99,30 @@ let rec check_with_def env sign (idl,c) mp equiv = | _ -> error_not_a_module (Label.to_string lab) in begin match mb.mod_expr with - | Some _ -> error_generative_module_expected lab - | None -> - let sign,cb,cst = - check_with_def env' mb.mod_type (idl,c) (MPdot(mp,lab)) mb.mod_delta + | Abstract -> + let struc = Modops.destr_nofunctor mb.mod_type in + let struc',c',cst = + check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta in let mb' = { mb with - mod_type = sign; + mod_type = NoFunctor struc'; mod_type_alg = None } in - SEBstruct(before@(lab,SFBmodule mb')::after),cb,cst + before@(lab,SFBmodule mb')::after, c', cst + | _ -> error_generative_module_expected lab end with | Not_found -> error_no_such_label lab | Reduction.NotConvertible -> error_incorrect_with_constraint lab -let rec check_with_mod env sign (idl,mp1) mp equiv = - let sig_b = match sign with - | SEBstruct(sig_b) -> sig_b - | _ -> error_signature_expected sign - in +let rec check_with_mod env struc (idl,mp1) mp equiv = let lab,idl = match idl with | [] -> assert false | id::idl -> Label.of_id id, idl in try - let before,spec,after = split_sign lab true sig_b in - let env' = Modops.add_signature mp before equiv env in + let before,spec,after = split_struc lab true struc in + let env' = Modops.add_structure mp before equiv env in let old = match spec with | SFBmodule mb -> mb | _ -> error_not_a_module (Label.to_string lab) @@ -142,33 +130,35 @@ let rec check_with_mod env sign (idl,mp1) mp equiv = if List.is_empty idl then (* Toplevel module definition *) let mb_mp1 = lookup_module mp1 env in - let mtb_mp1 = module_type_of_module None mb_mp1 in + let mtb_mp1 = module_type_of_module mb_mp1 in let cst = match old.mod_expr with - | None -> + | Abstract -> begin try - let mtb_old = module_type_of_module None old in + let mtb_old = module_type_of_module old in Subtyping.check_subtypes env' mtb_mp1 mtb_old +++ old.mod_constraints with Failure _ -> error_incorrect_with_constraint lab end - | Some (SEBident(mp')) -> + | Algebraic (NoFunctor (MEident(mp'))) -> check_modpath_equiv env' mp1 mp'; old.mod_constraints - | _ -> error_generative_module_expected lab + | _ -> error_generative_module_expected lab in let mp' = MPdot (mp,lab) in let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in - let new_mb' = {new_mb with - mod_mp = mp'; - mod_expr = Some (SEBident mp1); - mod_constraints = cst } + let new_mb' = + { new_mb with + mod_mp = mp'; + mod_expr = Algebraic (NoFunctor (MEident mp1)); + mod_constraints = cst } in + let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature with the identity substitution accompagned by the new resolver*) let id_subst = map_mp mp' mp' new_mb.mod_delta in - SEBstruct(before@(lab,SFBmodule new_mb')::subst_signature id_subst after), - add_delta_resolver equiv new_mb.mod_delta,cst + let new_after = subst_structure id_subst after in + before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst else (* Module definition of a sub-module *) let mp' = MPdot (mp,lab) in @@ -177,255 +167,163 @@ let rec check_with_mod env sign (idl,mp1) mp equiv = | _ -> error_not_a_module (Label.to_string lab) in begin match old.mod_expr with - | None -> - let sign,equiv',cst = - check_with_mod env' old.mod_type (idl,mp1) mp' old.mod_delta in + | Abstract -> + let struc = destr_nofunctor old.mod_type in + let struc',equiv',cst = + check_with_mod env' struc (idl,mp1) mp' old.mod_delta + in + let new_mb = + { old with + mod_type = NoFunctor struc'; + mod_type_alg = None; + mod_delta = equiv' } + in let new_equiv = add_delta_resolver equiv equiv' in - let new_mb = { old with - mod_type = sign; - mod_type_alg = None; - mod_delta = equiv'} - in let id_subst = map_mp mp' mp' equiv' in - SEBstruct(before@(lab,SFBmodule new_mb)::subst_signature id_subst after), - new_equiv,cst - | Some (SEBident mp0) -> + let new_after = subst_structure id_subst after in + before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst + | Algebraic (NoFunctor (MEident mp0)) -> let mpnew = rebuild_mp mp0 idl in check_modpath_equiv env' mpnew mp; - SEBstruct(before@(lab,spec)::after),equiv,Univ.empty_constraint + before@(lab,spec)::after, equiv, Univ.empty_constraint | _ -> error_generative_module_expected lab end with | Not_found -> error_no_such_label lab | Reduction.NotConvertible -> error_incorrect_with_constraint lab -let check_with env sign with_decl alg_sign mp equiv = - let sign,wd,equiv,cst= match with_decl with - | With_Definition (idl,c) -> - let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in - sign,With_definition_body(idl,cb),equiv,cst - | With_Module (idl,mp1) -> - let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in - sign,With_module_body(idl,mp1),equiv,cst - in - match alg_sign with - | None -> sign, None, equiv, cst - | Some s -> sign, Some (SEBwith(s, wd)), equiv, cst - -let rec translate_module env mp inl me = - match me.mod_entry_expr, me.mod_entry_type with - | None, None -> - Errors.anomaly ~label:"Mod_typing.translate_module" - (Pp.str "empty type and expr in module entry") - | None, Some mte -> - let mtb = translate_module_type env mp inl mte in - { mod_mp = mp; - mod_expr = None; - mod_type = mtb.typ_expr; - mod_type_alg = mtb.typ_expr_alg; - mod_delta = mtb.typ_delta; - mod_constraints = mtb.typ_constraints; - mod_retroknowledge = []} - | Some mexpr, _ -> - let sign,alg_implem,resolver,cst1 = - translate_struct_module_entry env mp inl mexpr in - let sign,alg1,resolver,cst2 = - match me.mod_entry_type with - | None -> - sign,None,resolver,Univ.empty_constraint - | Some mte -> - let mtb = translate_module_type env mp inl mte in - let cst = Subtyping.check_subtypes env - {typ_mp = mp; - typ_expr = sign; - typ_expr_alg = None; - typ_constraints = Univ.empty_constraint; - typ_delta = resolver;} - mtb - in - mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst - in - { mod_mp = mp; - mod_type = sign; - mod_expr = alg_implem; - mod_type_alg = alg1; - mod_constraints = cst1 +++ cst2; - mod_delta = resolver; - mod_retroknowledge = []} - (* spiwack: not so sure about that. It may - cause a bug when closing nested modules. - If it does, I don't really know how to - fix the bug.*) - -and translate_apply env inl ftrans mexpr mkalg = - let sign,alg,resolver,cst1 = ftrans in +let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg + +let check_with env mp (sign,alg,reso,cst) = function + |WithDef(idl,c) -> + let struc = destr_nofunctor sign in + let struc',c',cst' = check_with_def env struc (idl,c) mp reso in + let alg' = mk_alg_with alg (WithDef (idl,c')) in + (NoFunctor struc'),alg',reso, cst+++cst' + |WithMod(idl,mp1) as wd -> + let struc = destr_nofunctor sign in + let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in + let alg' = mk_alg_with alg wd in + (NoFunctor struc'),alg',reso', cst+++cst' + +let mk_alg_app mpo alg arg = match mpo, alg with + | Some _, Some alg -> Some (MEapply (alg,arg)) + | _ -> None + +(** Translation of a module struct entry : + - We translate to a module when a [module_path] is given, + otherwise to a module type. + - The first output is the expanded signature + - The second output is the algebraic expression, kept for the extraction. + It is never None when translating to a module, but for module type + it could not be contain [SEBapply] or [SEBfunctor]. +*) + +let rec translate_mse env mpo inl = function + |MEident mp1 -> + let sign,reso = match mpo with + |Some mp -> + let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in + mb.mod_type, mb.mod_delta + |None -> + let mtb = lookup_modtype mp1 env in + mtb.typ_expr, mtb.typ_delta + in + sign,Some (MEident mp1),reso,Univ.empty_constraint + |MEapply (fe,mp1) -> + translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo) + |MEwith(me, with_decl) -> + assert (mpo == None); (* No 'with' syntax for modules *) + let mp = mp_from_mexpr me in + check_with env mp (translate_mse env None inl me) with_decl + +and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg = let farg_id, farg_b, fbody_b = destr_functor sign in - let mp1 = - try path_of_mexpr mexpr - with Not_path -> error_application_to_not_path mexpr - in - let mtb = module_type_of_module None (lookup_module mp1 env) in + let mtb = module_type_of_module (lookup_module mp1 env) in let cst2 = Subtyping.check_subtypes env mtb farg_b in let mp_delta = discr_resolver mtb in let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in let subst = map_mbid farg_id mp1 mp_delta in - subst_struct_expr subst fbody_b, - mkalg alg mp1 cst2, - subst_codom_delta_resolver subst resolver, - cst1 +++ cst2 - -and translate_functor env inl arg_id arg_e trans mkalg = - let mtb = translate_module_type env (MPbound arg_id) inl arg_e in - let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in - let sign,alg,resolver,cst = trans env' + let body = subst_signature subst fbody_b in + let alg' = mkalg alg mp1 in + let reso' = subst_codom_delta_resolver subst reso in + body,alg',reso', cst1 +++ cst2 + +let mk_alg_funct mpo mbid mtb alg = match mpo, alg with + | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg)) + | _ -> None + +let rec translate_mse_funct env mpo inl mse = function + |[] -> + let sign,alg,reso,cst = translate_mse env mpo inl mse in + sign, Option.map (fun a -> NoFunctor a) alg, reso, cst + |(mbid, ty) :: params -> + let mp_id = MPbound mbid in + let mtb = translate_modtype env mp_id inl ([],ty) in + let env' = add_module_type mp_id mtb env in + let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in + let alg' = mk_alg_funct mpo mbid mtb alg in + MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.typ_constraints + +and translate_modtype env mp inl (params,mte) = + let sign,alg,reso,cst = translate_mse_funct env None inl mte params in + let mtb = + { typ_mp = mp_from_mexpr mte; + typ_expr = sign; + typ_expr_alg = None; + typ_constraints = cst; + typ_delta = reso } in - SEBfunctor (arg_id, mtb, sign), - mkalg alg arg_id mtb, - resolver, - cst +++ mtb.typ_constraints - -and translate_struct_module_entry env mp inl = function - | MSEident mp1 -> - let mb = lookup_module mp1 env in - let mb' = strengthen_and_subst_mb mb mp false in - mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint - | MSEfunctor (arg_id, arg_e, body_expr) -> - let trans env' = translate_struct_module_entry env' mp inl body_expr in - let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in - translate_functor env inl arg_id arg_e trans mkalg - | MSEapply (fexpr,mexpr) -> - let trans = translate_struct_module_entry env mp inl fexpr in - let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in - translate_apply env inl trans mexpr mkalg - | MSEwith(mte, with_decl) -> - let sign,alg,resolve,cst1 = - translate_struct_module_entry env mp inl mte in - let sign,alg,resolve,cst2 = - check_with env sign with_decl alg mp resolve in - sign,alg,resolve, cst1 +++ cst2 - -and translate_struct_type_entry env inl = function - | MSEident mp1 -> - let mtb = lookup_modtype mp1 env in - mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint - | MSEfunctor (arg_id, arg_e, body_expr) -> - let trans env' = translate_struct_type_entry env' inl body_expr in - translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None) - | MSEapply (fexpr,mexpr) -> - let trans = translate_struct_type_entry env inl fexpr in - translate_apply env inl trans mexpr (fun _ _ _ -> None) - | MSEwith(mte, with_decl) -> - let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in - let sign,alg,resolve,cst2 = - check_with env sign with_decl alg (mp_from_mexpr mte) resolve - in - sign,alg,resolve, cst1 +++ cst2 - -and translate_module_type env mp inl mte = - let mp_from = mp_from_mexpr mte in - let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in - let mtb = subst_modtype_and_resolver - {typ_mp = mp_from; - typ_expr = sign; - typ_expr_alg = None; - typ_constraints = cst; - typ_delta = resolve} mp - in {mtb with typ_expr_alg = alg} - -let rec translate_struct_include_module_entry env mp inl = function - | MSEident mp1 -> - let mb = lookup_module mp1 env in - let mb' = strengthen_and_subst_mb mb mp true in - let mb_typ = clean_bounded_mod_expr mb'.mod_type in - mb_typ,None,mb'.mod_delta,Univ.empty_constraint - | MSEapply (fexpr,mexpr) -> - let ftrans = translate_struct_include_module_entry env mp inl fexpr in - translate_apply env inl ftrans mexpr (fun _ _ _ -> None) - | _ -> Modops.error_higher_order_include () - -let rec add_struct_expr_constraints env = function - | SEBident _ -> env - - | SEBfunctor (_,mtb,meb) -> - add_struct_expr_constraints - (add_modtype_constraints env mtb) meb - - | SEBstruct (structure_body) -> - List.fold_left - (fun env (_,item) -> add_struct_elem_constraints env item) - env - structure_body - - | SEBapply (meb1,meb2,cst) -> - Environ.add_constraints cst - (add_struct_expr_constraints - (add_struct_expr_constraints env meb1) - meb2) - | SEBwith(meb,With_definition_body(_,cb))-> - Environ.add_constraints (Future.force cb.const_constraints) - (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_))-> - add_struct_expr_constraints env meb - -and add_struct_elem_constraints env = function - | SFBconst cb -> - Environ.add_constraints (Future.force cb.const_constraints) env - | SFBmind mib -> Environ.add_constraints mib.mind_constraints env - | SFBmodule mb -> add_module_constraints env mb - | SFBmodtype mtb -> add_modtype_constraints env mtb - -and add_module_constraints env mb = - let env = match mb.mod_expr with - | None -> env - | Some meb -> add_struct_expr_constraints env meb - in - let env = - add_struct_expr_constraints env mb.mod_type - in - Environ.add_constraints mb.mod_constraints env - -and add_modtype_constraints env mtb = - Environ.add_constraints mtb.typ_constraints - (add_struct_expr_constraints env mtb.typ_expr) - - -let rec struct_expr_constraints cst = function - | SEBident _ -> cst - - | SEBfunctor (_,mtb,meb) -> - struct_expr_constraints - (modtype_constraints cst mtb) meb - - | SEBstruct (structure_body) -> - List.fold_left - (fun cst (_,item) -> struct_elem_constraints cst item) - cst - structure_body - - | SEBapply (meb1,meb2,cst1) -> - struct_expr_constraints (struct_expr_constraints (cst1 +++ cst) meb1) - meb2 - | SEBwith(meb,With_definition_body(_,cb))-> - struct_expr_constraints ((Future.force cb.const_constraints) +++ cst) meb - | SEBwith(meb,With_module_body(_,_))-> - struct_expr_constraints cst meb - -and struct_elem_constraints cst = function - | SFBconst cb -> cst - | SFBmind mib -> cst - | SFBmodule mb -> module_constraints cst mb - | SFBmodtype mtb -> modtype_constraints cst mtb - -and module_constraints cst mb = - let cst = match mb.mod_expr with - | None -> cst - | Some meb -> struct_expr_constraints cst meb in - let cst = struct_expr_constraints cst mb.mod_type in - mb.mod_constraints +++ cst - -and modtype_constraints cst mtb = - struct_expr_constraints (mtb.typ_constraints +++ cst) mtb.typ_expr - - -let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint -let module_constraints = module_constraints Univ.empty_constraint + let mtb' = subst_modtype_and_resolver mtb mp in + { mtb' with typ_expr_alg = alg } + +(** [finalize_module] : + from an already-translated (or interactive) implementation + and a signature entry, produce a final [module_expr] *) + +let finalize_module env mp (sign,alg,reso,cst) restype = match restype with + |None -> + let impl = match alg with Some e -> Algebraic e | None -> FullStruct in + { mod_mp = mp; + mod_expr = impl; + mod_type = sign; + mod_type_alg = None; + mod_constraints = cst; + mod_delta = reso; + mod_retroknowledge = [] } + |Some (params_mte,inl) -> + let res_mtb = translate_modtype env mp inl params_mte in + let auto_mtb = { + typ_mp = mp; + typ_expr = sign; + typ_expr_alg = None; + typ_constraints = Univ.empty_constraint; + typ_delta = reso } in + let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in + let impl = match alg with Some e -> Algebraic e | None -> Struct sign in + { mod_mp = mp; + mod_expr = impl; + mod_type = res_mtb.typ_expr; + mod_type_alg = res_mtb.typ_expr_alg; + mod_constraints = cst +++ cst'; + mod_delta = res_mtb.typ_delta; + mod_retroknowledge = [] } + +let translate_module env mp inl = function + |MType (params,ty) -> + let mtb = translate_modtype env mp inl (params,ty) in + module_body_of_type mp mtb + |MExpr (params,mse,oty) -> + let t = translate_mse_funct env (Some mp) inl mse params in + let restype = Option.map (fun ty -> ((params,ty),inl)) oty in + finalize_module env mp t restype + +let rec translate_mse_incl env mp inl = function + |MEident mp1 -> + let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in + let sign = clean_bounded_mod_expr mb.mod_type in + sign,None,mb.mod_delta,Univ.empty_constraint + |MEapply (fe,arg) -> + let ftrans = translate_mse_incl env mp inl fe in + translate_apply env inl ftrans arg (fun _ _ -> None) + |_ -> Modops.error_higher_order_include () diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 0990e36c1..21171705d 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -12,40 +12,40 @@ open Entries open Mod_subst open Names +(** Main functions for translating module entries + + Note : [module_body] and [module_type_body] obtained this way + won't have any [MEstruct] in their algebraic fields. +*) val translate_module : env -> module_path -> inline -> module_entry -> module_body -val translate_module_type : - env -> module_path -> inline -> module_struct_entry -> module_type_body +val translate_modtype : + env -> module_path -> inline -> module_type_entry -> module_type_body -val translate_struct_module_entry : - env -> module_path -> inline -> module_struct_entry -> - struct_expr_body (* Signature *) - * struct_expr_body option (* Algebraic expr, in fact never None *) - * delta_resolver - * Univ.constraints - -val translate_struct_type_entry : - env -> inline -> module_struct_entry -> - struct_expr_body - * struct_expr_body option - * delta_resolver - * Univ.constraints - -val translate_struct_include_module_entry : - env -> module_path -> inline -> module_struct_entry -> - struct_expr_body - * struct_expr_body option (* Algebraic expr, always None *) - * delta_resolver - * Univ.constraints +(** Low-level function for translating a module struct entry : + - We translate to a module when a [module_path] is given, + otherwise to a module type. + - The first output is the expanded signature + - The second output is the algebraic expression, kept for the extraction. + It is never None when translating to a module, but for module type + it could not be contain applications or functors. + Moreover algebraic expressions obtained here cannot contain [MEstruct]. +*) -val add_modtype_constraints : env -> module_type_body -> env +type 'alg translation = + module_signature * 'alg option * delta_resolver * Univ.constraints -val add_module_constraints : env -> module_body -> env +val translate_mse : + env -> module_path option -> inline -> module_struct_entry -> + module_alg_expr translation -val add_struct_expr_constraints : env -> struct_expr_body -> env - -val struct_expr_constraints : struct_expr_body -> Univ.constraints +val translate_mse_incl : + env -> module_path -> inline -> module_struct_entry -> + module_alg_expr translation -val module_constraints : module_body -> Univ.constraints +val finalize_module : + env -> module_path -> module_expression translation -> + (module_type_entry * inline) option -> + module_body diff --git a/kernel/modops.ml b/kernel/modops.ml index deff291ec..76feb8498 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -51,12 +51,12 @@ type module_typing_error = Label.t * structure_field_body * signature_mismatch_error | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry - | NotAFunctor of struct_expr_body + | NotAFunctor + | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body | NotEqualModulePaths of module_path * module_path | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t - | SignatureExpected of struct_expr_body | NotAModule of string | NotAModuleType of string | NotAConstant of Label.t @@ -73,8 +73,11 @@ let error_existing_label l = let error_application_to_not_path mexpr = raise (ModuleTypingError (ApplicationToNotPath mexpr)) -let error_not_a_functor mtb = - raise (ModuleTypingError (NotAFunctor mtb)) +let error_not_a_functor () = + raise (ModuleTypingError NotAFunctor) + +let error_is_a_functor () = + raise (ModuleTypingError IsAFunctor) let error_incompatible_modtypes mexpr1 mexpr2 = raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2))) @@ -91,9 +94,6 @@ let error_no_such_label l = let error_incompatible_labels l l' = raise (ModuleTypingError (IncompatibleLabels (l,l'))) -let error_signature_expected mtb = - raise (ModuleTypingError (SignatureExpected mtb)) - let error_not_a_module s = raise (ModuleTypingError (NotAModule s)) @@ -112,24 +112,49 @@ let error_no_such_label_sub l l1 = let error_higher_order_include () = raise (ModuleTypingError HigherOrderInclude) -(** {6 Misc operations } *) +(** {6 Operations on functors } *) + +let is_functor = function + |NoFunctor _ -> false + |MoreFunctor _ -> true let destr_functor = function - | SEBfunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) - | mtb -> error_not_a_functor mtb + |NoFunctor _ -> error_not_a_functor () + |MoreFunctor (mbid,ty,x) -> (mbid,ty,x) -let is_functor = function - | SEBfunctor _ -> true - | _ -> false +let destr_nofunctor = function + |NoFunctor a -> a + |MoreFunctor _ -> error_is_a_functor () + +let rec functor_smartmap fty f0 funct = match funct with + |MoreFunctor (mbid,ty,e) -> + let ty' = fty ty in + let e' = functor_smartmap fty f0 e in + if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e') + |NoFunctor a -> + let a' = f0 a in if a==a' then funct else NoFunctor a' + +let rec functor_iter fty f0 = function + |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e + |NoFunctor a -> f0 a + +(** {6 Misc operations } *) + +let module_type_of_module mb = + { typ_mp = mb.mod_mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta } let module_body_of_type mp mtb = { mod_mp = mp; mod_type = mtb.typ_expr; mod_type_alg = mtb.typ_expr_alg; - mod_expr = None; + mod_expr = Abstract; mod_constraints = mtb.typ_constraints; mod_delta = mtb.typ_delta; - mod_retroknowledge = []} + mod_retroknowledge = [] } let check_modpath_equiv env mp1 mp2 = if ModPath.equal mp1 mp2 then () @@ -139,17 +164,27 @@ let check_modpath_equiv env mp1 mp2 = if ModPath.equal mp1' mp2' then () else error_not_equal_modpaths mp1 mp2 +let implem_smartmap fs fa impl = match impl with + |Struct e -> let e' = fs e in if e==e' then impl else Struct e' + |Algebraic a -> let a' = fa a in if a==a' then impl else Algebraic a' + |Abstract|FullStruct -> impl + +let implem_iter fs fa impl = match impl with + |Struct e -> fs e + |Algebraic a -> fa a + |Abstract|FullStruct -> () + (** {6 Substitutions of modular structures } *) let id_delta x y = x let rec subst_with_body sub = function - |With_module_body(id,mp) as orig -> + |WithMod(id,mp) as orig -> let mp' = subst_mp sub mp in - if mp==mp' then orig else With_module_body(id,mp') - |With_definition_body(id,cb) as orig -> - let cb' = subst_const_body sub cb in - if cb==cb' then orig else With_definition_body(id,cb') + if mp==mp' then orig else WithMod(id,mp') + |WithDef(id,c) as orig -> + let c' = subst_mps sub c in + if c==c' then orig else WithDef(id,c') and subst_modtype sub do_delta mtb= let { typ_mp = mp; typ_expr = ty; typ_expr_alg = aty } = mtb in @@ -158,8 +193,8 @@ and subst_modtype sub do_delta mtb= if ModPath.equal mp mp' then sub else add_mp mp mp' empty_delta_resolver sub in - let ty' = subst_struct_expr sub do_delta ty in - let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in + let ty' = subst_signature sub do_delta ty in + let aty' = Option.smartmap (subst_expression sub id_delta) aty in let delta' = do_delta mtb.typ_delta sub in if mp==mp' && ty==ty' && aty==aty' && delta'==mtb.typ_delta then mtb @@ -172,16 +207,16 @@ and subst_modtype sub do_delta mtb= and subst_structure sub do_delta sign = let subst_body ((l,body) as orig) = match body with - | SFBconst cb -> + |SFBconst cb -> let cb' = subst_const_body sub cb in if cb==cb' then orig else (l,SFBconst cb') - | SFBmind mib -> + |SFBmind mib -> let mib' = subst_mind sub mib in if mib==mib' then orig else (l,SFBmind mib') - | SFBmodule mb -> + |SFBmodule mb -> let mb' = subst_module sub do_delta mb in if mb==mb' then orig else (l,SFBmodule mb') - | SFBmodtype mtb -> + |SFBmodtype mtb -> let mtb' = subst_modtype sub do_delta mtb in if mtb==mtb' then orig else (l,SFBmodtype mtb') in @@ -194,13 +229,12 @@ and subst_module sub do_delta mb = if not (is_functor ty) || ModPath.equal mp mp' then sub else add_mp mp mp' empty_delta_resolver sub in - let ty' = subst_struct_expr sub do_delta ty in - (* Special optim : maintain sharing between [mod_expr] and [mod_type] *) - let me' = match me with - | Some m when m == ty -> if ty == ty' then me else Some ty' - | _ -> Option.smartmap (subst_struct_expr sub id_delta) me + let ty' = subst_signature sub do_delta ty in + let me' = + implem_smartmap + (subst_signature sub id_delta) (subst_expression sub id_delta) me in - let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in + let aty' = Option.smartmap (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta then mb @@ -212,34 +246,35 @@ and subst_module sub do_delta mb = mod_type_alg = aty'; mod_delta = delta' } -and subst_struct_expr sub do_delta seb = match seb with - |SEBident mp -> +and subst_expr sub do_delta seb = match seb with + |MEident mp -> let mp' = subst_mp sub mp in - if mp==mp' then seb else SEBident mp' - |SEBfunctor (mbid, mtb, meb) -> - let mtb' = subst_modtype sub do_delta mtb in - let meb' = subst_struct_expr sub do_delta meb in - if mtb==mtb' && meb==meb' then seb - else SEBfunctor(mbid,mtb',meb') - |SEBstruct str -> - let str' = subst_structure sub do_delta str in - if str==str' then seb else SEBstruct str' - |SEBapply (meb1,meb2,cst) -> - let meb1' = subst_struct_expr sub do_delta meb1 in - let meb2' = subst_struct_expr sub do_delta meb2 in - if meb1==meb1' && meb2==meb2' then seb else SEBapply(meb1',meb2',cst) - |SEBwith (meb,wdb) -> - let meb' = subst_struct_expr sub do_delta meb in + if mp==mp' then seb else MEident mp' + |MEapply (meb1,mp2) -> + let meb1' = subst_expr sub do_delta meb1 in + let mp2' = subst_mp sub mp2 in + if meb1==meb1' && mp2==mp2' then seb else MEapply(meb1',mp2') + |MEwith (meb,wdb) -> + let meb' = subst_expr sub do_delta meb in let wdb' = subst_with_body sub wdb in - if meb==meb' && wdb==wdb' then seb else SEBwith(meb',wdb') + if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb') + +and subst_expression sub do_delta = + functor_smartmap + (subst_modtype sub do_delta) + (subst_expr sub do_delta) + +and subst_signature sub do_delta = + functor_smartmap + (subst_modtype sub do_delta) + (subst_structure sub do_delta) -let subst_signature subst = - subst_structure subst - (fun resolver subst-> subst_codom_delta_resolver subst resolver) +let do_delta_dom reso sub = subst_dom_delta_resolver sub reso +let do_delta_codom reso sub = subst_codom_delta_resolver sub reso +let do_delta_dom_codom reso sub = subst_dom_codom_delta_resolver sub reso -let subst_struct_expr subst = - subst_struct_expr subst - (fun resolver subst-> subst_codom_delta_resolver subst resolver) +let subst_signature subst = subst_signature subst do_delta_codom +let subst_structure subst = subst_structure subst do_delta_codom (** {6 Retroknowledge } *) @@ -247,16 +282,12 @@ let subst_struct_expr subst = the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge mp = - let perform rkaction env = - match rkaction with - | Retroknowledge.RKRegister (f, e) -> - Environ.register env f - (match e with - | Const kn -> kind_of_term (mkConst kn) - | Ind ind -> kind_of_term (mkInd ind) - | _ -> - anomaly ~label:"Modops.add_retroknowledge" - (Pp.str "had to import an unsupported kind of term")) + let perform rkaction env = match rkaction with + |Retroknowledge.RKRegister (f, (Const _ | Ind _ as e)) -> + Environ.register env f e + |_ -> + Errors.anomaly ~label:"Modops.add_retroknowledge" + (Pp.str "had to import an unsupported kind of term") in fun lclrk env -> (* The order of the declaration matters, for instance (and it's at the @@ -271,7 +302,7 @@ let add_retroknowledge mp = (** {6 Adding a module in the environment } *) -let rec add_signature mp sign resolver env = +let rec add_structure mp sign resolver env = let add_one env (l,elem) = match elem with |SFBconst cb -> let c = constant_of_delta_kn resolver (KerName.make2 mp l) in @@ -288,105 +319,71 @@ and add_module mb env = let mp = mb.mod_mp in let env = Environ.shallow_add_module mb env in match mb.mod_type with - | SEBstruct (sign) -> + |NoFunctor struc -> add_retroknowledge mp mb.mod_retroknowledge - (add_signature mp sign mb.mod_delta env) - | SEBfunctor _ -> env - | _ -> - anomaly ~label:"Modops" - (Pp.str "the evaluation of the structure failed ") + (add_structure mp struc mb.mod_delta env) + |MoreFunctor _ -> env + +let add_module_type mp mtb env = + add_module (module_body_of_type mp mtb) env (** {6 Strengtening } *) let strengthen_const mp_from l cb resolver = match cb.const_body with - | Def _ -> cb - | _ -> - let kn = KerName.make2 mp_from l in - let con = constant_of_delta_kn resolver kn in - { cb with - const_body = Def (Lazyconstr.from_val (mkConst con)); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) - } + |Def _ -> cb + |_ -> + let kn = KerName.make2 mp_from l in + let con = constant_of_delta_kn resolver kn in + { cb with + const_body = Def (Lazyconstr.from_val (mkConst con)); + const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) } let rec strengthen_mod mp_from mp_to mb = - if mp_in_delta mb.mod_mp mb.mod_delta then - mb - else - match mb.mod_type with - | SEBstruct (sign) -> - let resolve_out,sign_out = - strengthen_sig mp_from sign mp_to mb.mod_delta - in - { mb with - mod_expr = Some (SEBident mp_to); - mod_type = SEBstruct(sign_out); - mod_type_alg = mb.mod_type_alg; - mod_constraints = mb.mod_constraints; - mod_delta = add_mp_delta_resolver mp_from mp_to - (add_delta_resolver mb.mod_delta resolve_out); - mod_retroknowledge = mb.mod_retroknowledge } - | SEBfunctor _ -> mb - | _ -> - anomaly ~label:"Modops" - (Pp.str "the evaluation of the structure failed ") - -and strengthen_sig mp_from sign mp_to resolver = - match sign with - | [] -> empty_delta_resolver,[] - | (l,SFBconst cb) :: rest -> - let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item'::rest' - | (_,SFBmind _ as item):: rest -> - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item::rest' - | (l,SFBmodule mb) :: rest -> - let mp_from' = MPdot (mp_from,l) in - let mp_to' = MPdot(mp_to,l) in - let mb_out = strengthen_mod mp_from' mp_to' mb in - let item' = l,SFBmodule (mb_out) in - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - add_delta_resolver resolve_out mb.mod_delta, item':: rest' - | (l,SFBmodtype mty as item) :: rest -> - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item::rest' + if mp_in_delta mb.mod_mp mb.mod_delta then mb + else match mb.mod_type with + |NoFunctor struc -> + let reso,struc' = strengthen_sig mp_from struc mp_to mb.mod_delta in + { mb with + mod_expr = Algebraic (NoFunctor (MEident mp_to)); + mod_type = NoFunctor struc'; + mod_delta = + add_mp_delta_resolver mp_from mp_to + (add_delta_resolver mb.mod_delta reso) } + |MoreFunctor _ -> mb + +and strengthen_sig mp_from struc mp_to reso = match struc with + |[] -> empty_delta_resolver,[] + |(l,SFBconst cb) :: rest -> + let item' = l,SFBconst (strengthen_const mp_from l cb reso) in + let reso',rest' = strengthen_sig mp_from rest mp_to reso in + reso',item'::rest' + |(_,SFBmind _ as item):: rest -> + let reso',rest' = strengthen_sig mp_from rest mp_to reso in + reso',item::rest' + |(l,SFBmodule mb) :: rest -> + let mp_from' = MPdot (mp_from,l) in + let mp_to' = MPdot(mp_to,l) in + let mb' = strengthen_mod mp_from' mp_to' mb in + let item' = l,SFBmodule mb' in + let reso',rest' = strengthen_sig mp_from rest mp_to reso in + add_delta_resolver reso' mb.mod_delta, item':: rest' + |(l,SFBmodtype mty as item) :: rest -> + let reso',rest' = strengthen_sig mp_from rest mp_to reso in + reso',item::rest' let strengthen mtb mp = - if mp_in_delta mtb.typ_mp mtb.typ_delta then - (* in this case mtb has already been strengthened*) - mtb - else - match mtb.typ_expr with - | SEBstruct (sign) -> - let resolve_out,sign_out = - strengthen_sig mtb.typ_mp sign mp mtb.typ_delta - in - {mtb with - typ_expr = SEBstruct(sign_out); - typ_delta = add_delta_resolver mtb.typ_delta - (add_mp_delta_resolver mtb.typ_mp mp resolve_out)} - | SEBfunctor _ -> mtb - | _ -> - anomaly ~label:"Modops" - (Pp.str "the evaluation of the structure failed ") - -let module_type_of_module mp mb = - match mp with - Some mp -> - strengthen { - typ_mp = mp; - typ_expr = mb.mod_type; - typ_expr_alg = None; - typ_constraints = mb.mod_constraints; - typ_delta = mb.mod_delta} mp - - | None -> - {typ_mp = mb.mod_mp; - typ_expr = mb.mod_type; - typ_expr_alg = None; - typ_constraints = mb.mod_constraints; - typ_delta = mb.mod_delta} + (* Has mtb already been strengthened ? *) + if mp_in_delta mtb.typ_mp mtb.typ_delta then mtb + else match mtb.typ_expr with + |NoFunctor struc -> + let reso',struc' = strengthen_sig mtb.typ_mp struc mp mtb.typ_delta in + { mtb with + typ_expr = NoFunctor struc'; + typ_delta = + add_delta_resolver mtb.typ_delta + (add_mp_delta_resolver mtb.typ_mp mp reso') } + |MoreFunctor _ -> mtb let inline_delta_resolver env inl mp mbid mtb delta = let constants = inline_of_delta inl mtb.typ_delta in @@ -409,109 +406,97 @@ let inline_delta_resolver env inl mp mbid mtb delta = in make_inline delta constants -let rec strengthen_and_subst_mod mb subst mp_from mp_to resolver = +let rec strengthen_and_subst_mod mb subst mp_from mp_to = match mb.mod_type with - | SEBstruct str -> - let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in - if mb_is_an_alias then - subst_module subst - (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb - else - let resolver,new_sig = - strengthen_and_subst_struct str subst - mp_from mp_from mp_to false false mb.mod_delta - in - {mb with - mod_mp = mp_to; - mod_expr = Some (SEBident mp_from); - mod_type = SEBstruct(new_sig); - mod_delta = add_mp_delta_resolver mp_to mp_from resolver} - | SEBfunctor(arg_id,arg_b,body) -> - let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in - subst_module subst - (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb - | _ -> - anomaly ~label:"Modops" - (Pp.str "the evaluation of the structure failed ") - -and strengthen_and_subst_struct - str subst mp_alias mp_from mp_to alias incl resolver = + |NoFunctor struc -> + let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in + if mb_is_an_alias then subst_module subst do_delta_dom mb + else + let reso',struc' = + strengthen_and_subst_struct struc subst + mp_from mp_to false false mb.mod_delta + in + { mb with + mod_mp = mp_to; + mod_expr = Algebraic (NoFunctor (MEident mp_from)); + mod_type = NoFunctor struc'; + mod_delta = add_mp_delta_resolver mp_to mp_from reso' } + |MoreFunctor _ -> + let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in + subst_module subst do_delta_dom mb + +and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = match str with | [] -> empty_delta_resolver,[] | (l,SFBconst cb) :: rest -> - let item' = if alias then - (* case alias no strengthening needed*) - l,SFBconst (subst_const_body subst cb) - else - l,SFBconst (strengthen_const mp_from l - (subst_const_body subst cb) resolver) - in - let resolve_out,rest' = - strengthen_and_subst_struct rest subst - mp_alias mp_from mp_to alias incl resolver in + let cb' = subst_const_body subst cb in + let cb'' = + if alias then cb' + else strengthen_const mp_from l cb' reso + in + let item' = l, SFBconst cb'' in + let reso',rest' = + strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso + in if incl then - (* If we are performing an inclusion we need to add - the fact that the constant mp_to.l is \Delta-equivalent - to resolver(mp_from.l) *) - let kn_from = KerName.make2 mp_from l in - let kn_to = KerName.make2 mp_to l in - let old_name = kn_of_delta resolver kn_from in - (add_kn_delta_resolver kn_to old_name resolve_out), - item'::rest' + (* If we are performing an inclusion we need to add + the fact that the constant mp_to.l is \Delta-equivalent + to reso(mp_from.l) *) + let kn_from = KerName.make2 mp_from l in + let kn_to = KerName.make2 mp_to l in + let old_name = kn_of_delta reso kn_from in + add_kn_delta_resolver kn_to old_name reso', item'::rest' else - (*In this case the fact that the constant mp_to.l is - \Delta-equivalent to resolver(mp_from.l) is already known - because resolve_out contains mp_to maps to resolver(mp_from)*) - resolve_out,item'::rest' + (* In this case the fact that the constant mp_to.l is + \Delta-equivalent to resolver(mp_from.l) is already known + because reso' contains mp_to maps to reso(mp_from) *) + reso', item'::rest' | (l,SFBmind mib) :: rest -> - (*Same as constant*) let item' = l,SFBmind (subst_mind subst mib) in - let resolve_out,rest' = - strengthen_and_subst_struct rest subst - mp_alias mp_from mp_to alias incl resolver in + let reso',rest' = + strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso + in + (* Same as constant *) if incl then let kn_from = KerName.make2 mp_from l in let kn_to = KerName.make2 mp_to l in - let old_name = kn_of_delta resolver kn_from in - (add_kn_delta_resolver kn_to old_name resolve_out), - item'::rest' + let old_name = kn_of_delta reso kn_from in + add_kn_delta_resolver kn_to old_name reso', item'::rest' else - resolve_out,item'::rest' + reso', item'::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in - let mp_to' = MPdot(mp_to,l) in - let mb_out = if alias then - subst_module subst - (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb + let mp_to' = MPdot (mp_to,l) in + let mb' = if alias then + subst_module subst do_delta_dom mb else - strengthen_and_subst_mod - mb subst mp_from' mp_to' resolver + strengthen_and_subst_mod mb subst mp_from' mp_to' in - let item' = l,SFBmodule (mb_out) in - let resolve_out,rest' = - strengthen_and_subst_struct rest subst - mp_alias mp_from mp_to alias incl resolver in - (* if mb is a functor we should not derive new equivalences - on names, hence we add the fact that the functor can only - be equivalent to itself. If we adopt an applicative - semantic for functor this should be changed.*) - if is_functor mb_out.mod_type then - (add_mp_delta_resolver - mp_to' mp_to' resolve_out),item':: rest' - else - add_delta_resolver resolve_out mb_out.mod_delta, - item':: rest' - | (l,SFBmodtype mty) :: rest -> + let item' = l,SFBmodule mb' in + let reso',rest' = + strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso + in + (* if mb is a functor we should not derive new equivalences + on names, hence we add the fact that the functor can only + be equivalent to itself. If we adopt an applicative + semantic for functor this should be changed.*) + if is_functor mb'.mod_type then + add_mp_delta_resolver mp_to' mp_to' reso', item':: rest' + else + add_delta_resolver reso' mb'.mod_delta, item':: rest' + | (l,SFBmodtype mty) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in - let mty = subst_modtype subst' - (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in - let resolve_out,rest' = strengthen_and_subst_struct rest subst - mp_alias mp_from mp_to alias incl resolver + let mty = subst_modtype subst' + (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver) + mty in - (add_mp_delta_resolver mp_to' mp_to' resolve_out), - (l,SFBmodtype mty)::rest' + let item' = l,SFBmodtype mty in + let reso',rest' = + strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso + in + add_mp_delta_resolver mp_to' mp_to' reso', item'::rest' (** Let P be a module path when we write: @@ -521,7 +506,7 @@ and strengthen_and_subst_struct - The second one is strenghtening. *) let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with - |SEBstruct str -> + |NoFunctor struc -> let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in (* if mb.mod_mp is an alias then the strengthening is useless (i.e. it is already done)*) @@ -529,168 +514,125 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in let new_resolver = add_mp_delta_resolver mp mp_alias - (subst_dom_delta_resolver subst_resolver mb.mod_delta) in + (subst_dom_delta_resolver subst_resolver mb.mod_delta) + in let subst = map_mp mb.mod_mp mp new_resolver in - let resolver_out,new_sig = - strengthen_and_subst_struct str subst - mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta + let reso',struc' = + strengthen_and_subst_struct struc subst + mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta in { mb with mod_mp = mp; - mod_type = SEBstruct(new_sig); - mod_expr = Some (SEBident mb.mod_mp); + mod_type = NoFunctor struc'; + mod_expr = Algebraic (NoFunctor (MEident mb.mod_mp)); mod_delta = - if include_b then resolver_out - else add_delta_resolver new_resolver resolver_out } - |SEBfunctor(arg_id,argb,body) -> + if include_b then reso' + else add_delta_resolver new_resolver reso' } + |MoreFunctor _ -> let subst = map_mp mb.mod_mp mp empty_delta_resolver in - subst_module subst - (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb - | _ -> - anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") - + subst_module subst do_delta_dom_codom mb let subst_modtype_and_resolver mtb mp = - let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in + let subst = map_mp mtb.typ_mp mp empty_delta_resolver in let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in - let full_subst = (map_mp mtb.typ_mp mp new_delta) in - subst_modtype full_subst - (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb + let full_subst = map_mp mtb.typ_mp mp new_delta in + subst_modtype full_subst do_delta_dom_codom mtb + +(** {6 Cleaning a module expression from bounded parts } -(** {6 Cleaning a bounded module expression } *) + For instance: + functor(X:T)->struct module M:=X end) + becomes: + functor(X:T)->struct module M:=<content of T> end) +*) let rec is_bounded_expr l = function - | SEBident mp -> List.mem mp l - | SEBapply (fexpr,mexpr,_) -> - is_bounded_expr l mexpr || is_bounded_expr l fexpr + | MEident (MPbound mbid) -> MBIset.mem mbid l + | MEapply (fexpr,mp) -> + is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr | _ -> false -let rec clean_struct l = function - | (lab,SFBmodule mb) as field -> - let clean_typ = clean_expr l mb.mod_type in - let clean_impl = - begin try - if (is_bounded_expr l (Option.get mb.mod_expr)) then - Some clean_typ - else Some (clean_expr l (Option.get mb.mod_expr)) - with - Option.IsNone -> None - end in - if clean_typ==mb.mod_type && clean_impl==mb.mod_expr then - field - else - (lab,SFBmodule {mb with - mod_type=clean_typ; - mod_expr=clean_impl}) - | field -> field - -and clean_expr l = function - | SEBfunctor (mbid,sigt,str) as s-> - let str_clean = clean_expr l str in - let sig_clean = clean_expr l sigt.typ_expr in - if str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **) - s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean) - | SEBstruct str as s-> - let str_clean = List.smartmap (clean_struct l) str in - if str_clean == str then s else SEBstruct(str_clean) - | str -> str - -let rec collect_mbid l = function - | SEBfunctor (mbid,sigt,str) as s-> - let str_clean = collect_mbid ((MPbound mbid)::l) str in - if str_clean == str then s else - SEBfunctor (mbid,sigt,str_clean) - | SEBstruct str as s-> - let str_clean = List.smartmap (clean_struct l) str in - if str_clean == str then s else SEBstruct(str_clean) - | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") - - -let clean_bounded_mod_expr = function - | SEBfunctor _ as str -> - let str_clean = collect_mbid [] str in - if str_clean == str then str else str_clean - | str -> str +let rec clean_module l mb = + let impl, typ = mb.mod_expr, mb.mod_type in + let typ' = clean_signature l typ in + let impl' = match impl with + | Algebraic (NoFunctor m) when is_bounded_expr l m -> FullStruct + | _ -> implem_smartmap (clean_signature l) (clean_expression l) impl + in + if typ==typ' && impl==impl' then mb + else { mb with mod_type=typ'; mod_expr=impl' } + +and clean_modtype l mt = + let ty = mt.typ_expr in + let ty' = clean_signature l ty in + if ty==ty' then mt else { mt with typ_expr=ty' } + +and clean_field l field = match field with + |(lab,SFBmodule mb) -> + let mb' = clean_module l mb in + if mb==mb' then field else (lab,SFBmodule mb') + |_ -> field + +and clean_structure l = List.smartmap (clean_field l) + +and clean_signature l = + functor_smartmap (clean_modtype l) (clean_structure l) + +and clean_expression l = + functor_smartmap (clean_modtype l) (fun me -> me) + +let rec collect_mbid l sign = match sign with + |MoreFunctor (mbid,ty,m) -> + let m' = collect_mbid (MBIset.add mbid l) m in + if m==m' then sign else MoreFunctor (mbid,ty,m') + |NoFunctor struc -> + let struc' = clean_structure l struc in + if struc==struc' then sign else NoFunctor struc' + +let clean_bounded_mod_expr sign = + if is_functor sign then collect_mbid MBIset.empty sign else sign (** {6 Stm machinery : join and prune } *) -let rec join_module_body mb = - Option.iter join_struct_expr_body mb.mod_expr; - Option.iter join_struct_expr_body mb.mod_type_alg; - join_struct_expr_body mb.mod_type -and join_structure_body struc = - let join_body (l,body) = match body with - | SFBconst sb -> join_constant_body sb - | SFBmind _ -> () - | SFBmodule m -> join_module_body m - | SFBmodtype m -> - join_struct_expr_body m.typ_expr; - Option.iter join_struct_expr_body m.typ_expr_alg in - List.iter join_body struc; -and join_struct_expr_body = function - | SEBfunctor (_,t,e) -> - join_struct_expr_body t.typ_expr; - Option.iter join_struct_expr_body t.typ_expr_alg; - join_struct_expr_body e - | SEBident mp -> () - | SEBstruct s -> join_structure_body s - | SEBapply (mexpr,marg,u) -> - join_struct_expr_body mexpr; - join_struct_expr_body marg - | SEBwith (seb,wdcl) -> - join_struct_expr_body seb; - match wdcl with - | With_module_body _ -> () - | With_definition_body (_, sb) -> join_constant_body sb - -let rec prune_module_body mb = +let rec join_module mb = + implem_iter join_signature join_expression mb.mod_expr; + Option.iter join_expression mb.mod_type_alg; + join_signature mb.mod_type +and join_modtype mt = + Option.iter join_expression mt.typ_expr_alg; + join_signature mt.typ_expr +and join_field (l,body) = match body with + |SFBconst sb -> join_constant_body sb + |SFBmind _ -> () + |SFBmodule m -> join_module m + |SFBmodtype m -> join_modtype m +and join_structure struc = List.iter join_field struc +and join_signature sign = functor_iter join_modtype join_structure sign +and join_expression me = functor_iter join_modtype (fun _ -> ()) me + +let rec prune_module mb = let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in - let me' = Option.smartmap prune_struct_expr_body me in - let mta' = Option.smartmap prune_struct_expr_body mta in - let mt' = prune_struct_expr_body mt in + let mt' = prune_signature mt in + let me' = implem_smartmap prune_signature prune_expression me in + let mta' = Option.smartmap prune_expression mta in if me' == me && mta' == mta && mt' == mt then mb else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'} -and prune_structure_body struc = - let prune_body (l,body as orig) = match body with - | SFBconst sb -> - let sb' = prune_constant_body sb in - if sb == sb' then orig else (l, SFBconst sb') - | SFBmind _ -> orig - | SFBmodule m -> - let m' = prune_module_body m in - if m == m' then orig else (l, SFBmodule m') - | SFBmodtype m -> - let te, te_alg = m.typ_expr, m.typ_expr_alg in - let te' = prune_struct_expr_body te in - let te_alg' = - Option.smartmap prune_struct_expr_body te_alg in - if te' == te && te_alg' == te_alg then orig - else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'}) - in - List.smartmap prune_body struc -and prune_struct_expr_body orig = match orig with - | SEBfunctor (id,t,e) -> - let te, ta = t.typ_expr, t.typ_expr_alg in - let te' = prune_struct_expr_body te in - let ta' = Option.smartmap prune_struct_expr_body ta in - let e' = prune_struct_expr_body e in - if te' == te && ta' == ta && e' == e then orig - else SEBfunctor(id, {t with typ_expr = te'; typ_expr_alg = ta'}, e') - | SEBident _ -> orig - | SEBstruct s -> - let s' = prune_structure_body s in - if s' == s then orig else SEBstruct s' - | SEBapply (mexpr,marg,u) -> - let mexpr' = prune_struct_expr_body mexpr in - let marg' = prune_struct_expr_body marg in - if mexpr' == mexpr && marg' == marg then orig - else SEBapply (mexpr', marg', u) - | SEBwith (seb,wdcl) -> - let seb' = prune_struct_expr_body seb in - let wdcl' = match wdcl with - | With_module_body _ -> wdcl - | With_definition_body (id, sb) -> - let sb' = prune_constant_body sb in - if sb' == sb then wdcl else With_definition_body (id, sb') in - if seb' == seb && wdcl' == wdcl then orig - else SEBwith (seb', wdcl') +and prune_modtype mt = + let te, ta = mt.typ_expr, mt.typ_expr_alg in + let te' = prune_signature te in + let ta' = Option.smartmap prune_expression ta in + if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' } +and prune_field (l,body as orig) = match body with + |SFBconst sb -> + let sb' = prune_constant_body sb in + if sb == sb' then orig else (l, SFBconst sb') + |SFBmind _ -> orig + |SFBmodule m -> + let m' = prune_module m in + if m == m' then orig else (l, SFBmodule m') + |SFBmodtype m -> + let m' = prune_modtype m in + if m == m' then orig else (l, SFBmodtype m') +and prune_structure struc = List.smartmap prune_field struc +and prune_signature sign = functor_smartmap prune_modtype prune_structure sign +and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me diff --git a/kernel/modops.mli b/kernel/modops.mli index e148f9628..6aed95988 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -16,30 +16,43 @@ open Mod_subst (** {6 Various operations on modules and module types } *) -val module_body_of_type : module_path -> module_type_body -> module_body +(** Functors *) -val module_type_of_module : - module_path option -> module_body -> module_type_body +val is_functor : ('ty,'a) functorize -> bool -val destr_functor : - struct_expr_body -> MBId.t * module_type_body * struct_expr_body +val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize + +val destr_nofunctor : ('ty,'a) functorize -> 'a + +(** Conversions between [module_body] and [module_type_body] *) + +val module_type_of_module : module_body -> module_type_body +val module_body_of_type : module_path -> module_type_body -> module_body val check_modpath_equiv : env -> module_path -> module_path -> unit -(** {6 Substitutions } *) +val implem_smartmap : + (module_signature -> module_signature) -> + (module_expression -> module_expression) -> + (module_implementation -> module_implementation) -val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body +(** {6 Substitutions } *) -val subst_signature : substitution -> structure_body -> structure_body +val subst_signature : substitution -> module_signature -> module_signature +val subst_structure : substitution -> structure_body -> structure_body (** {6 Adding to an environment } *) -val add_signature : +val add_structure : module_path -> structure_body -> delta_resolver -> env -> env (** adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env + +(** same, for a module type *) +val add_module_type : module_path -> module_type_body -> env -> env + (** {6 Strengthening } *) val strengthen : module_type_body -> module_path -> module_type_body @@ -53,17 +66,22 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body val subst_modtype_and_resolver : module_type_body -> module_path -> module_type_body -(** {6 Cleaning a bound module expression } *) +(** {6 Cleaning a module expression from bounded parts } -val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body + For instance: + functor(X:T)->struct module M:=X end) + becomes: + functor(X:T)->struct module M:=<content of T> end) +*) + +val clean_bounded_mod_expr : module_signature -> module_signature (** {6 Stm machinery : join and prune } *) -val join_module_body : module_body -> unit -val join_structure_body : structure_body -> unit -val join_struct_expr_body : struct_expr_body -> unit +val join_module : module_body -> unit +val join_structure : structure_body -> unit -val prune_structure_body : structure_body -> structure_body +val prune_structure : structure_body -> structure_body (** {6 Errors } *) @@ -91,12 +109,12 @@ type module_typing_error = Label.t * structure_field_body * signature_mismatch_error | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry - | NotAFunctor of struct_expr_body + | NotAFunctor + | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body | NotEqualModulePaths of module_path * module_path | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t - | SignatureExpected of struct_expr_body | NotAModule of string | NotAModuleType of string | NotAConstant of Label.t @@ -121,8 +139,6 @@ val error_incompatible_labels : Label.t -> Label.t -> 'a val error_no_such_label : Label.t -> 'a -val error_signature_expected : struct_expr_body -> 'a - val error_not_a_module : string -> 'a val error_not_a_constant : Label.t -> 'a diff --git a/kernel/names.ml b/kernel/names.ml index fbd26ca3d..0da8fc5d4 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -234,6 +234,7 @@ struct end module MBImap = Map.Make(MBId) +module MBIset = Set.Make(MBId) (** {6 Names of structure elements } *) diff --git a/kernel/names.mli b/kernel/names.mli index 8022cb199..c05e30b9b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -169,6 +169,7 @@ sig end +module MBIset : Set.S with type elt = MBId.t module MBImap : Map.S with type key = MBId.t (** {6 The module part of the kernel name } *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index acb740cd0..55d348550 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -19,13 +19,11 @@ compiler *) let rec translate_mod prefix mp env mod_expr acc = match mod_expr with - | SEBident mp' -> assert false - | SEBstruct msb -> - let env' = add_signature mp msb empty_delta_resolver env in - List.fold_left (translate_field prefix mp env') acc msb - | SEBfunctor (mbid,mtb,meb) -> acc - | SEBapply (f,x,_) -> assert false - | SEBwith _ -> assert false + | NoFunctor struc -> + let env' = add_structure mp struc empty_delta_resolver env in + List.fold_left (translate_field prefix mp env') acc struc + | MoreFunctor _ -> acc + and translate_field prefix mp env (code, upds as acc) (l,x) = match x with | SFBconst cb -> @@ -41,14 +39,14 @@ and translate_field prefix mp env (code, upds as acc) (l,x) = let dump_library mp dp env mod_expr = if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library..."); match mod_expr with - | SEBstruct msb -> - let env = add_signature mp msb empty_delta_resolver env in + | NoFunctor struc -> + let env = add_structure mp struc empty_delta_resolver env in let prefix = mod_uid_of_dirpath dp ^ "." in - let t0 = Sys.time () in + let t0 = Sys.time () in clear_global_tbl (); clear_symb_tbl (); let mlcode, upds = - List.fold_left (translate_field prefix mp env) ([],empty_updates) msb + List.fold_left (translate_field prefix mp env) ([],empty_updates) struc in let t1 = Sys.time () in let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 7b74b00c5..3f413631c 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -13,7 +13,7 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -val dump_library : module_path -> dir_path -> env -> struct_expr_body -> +val dump_library : module_path -> dir_path -> env -> module_signature -> global list * symbol array * code_location_updates val compile_library : diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c7711b137..5ff619ce1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,8 +194,8 @@ let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false let join_safe_environment e = - Modops.join_structure_body e.revstruct; - List.fold_left + Modops.join_structure e.revstruct; + List.fold_left (fun e fc -> add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst @@ -213,7 +213,7 @@ let prune_env env = let prune_safe_environment e = { e with modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE); - revstruct = Modops.prune_structure_body e.revstruct; + revstruct = Modops.prune_structure e.revstruct; future_cst = []; env = prune_env e.env } @@ -433,9 +433,9 @@ let add_mind dir l mie senv = (** Insertion of module types *) -let add_modtype l mte inl senv = +let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in - let mtb = Mod_typing.translate_module_type senv.env mp inl mte in + let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' @@ -445,16 +445,19 @@ let full_add_module mb senv = let senv = add_constraints (Now mb.mod_constraints) senv in { senv with env = Modops.add_module mb senv.env } +let full_add_module_type mp mt senv = + let senv = add_constraints (Now mt.typ_constraints) senv in + { senv with env = Modops.add_module_type mp mt senv.env } + (** Insertion of modules *) let add_module l me inl senv = let mp = MPdot(senv.modpath, l) in let mb = Mod_typing.translate_module senv.env mp inl me in let senv' = add_field (l,SFBmodule mb) M senv in - let senv'' = match mb.mod_type with - | SEBstruct _ -> - update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv' - | _ -> senv' + let senv'' = + if Modops.is_functor mb.mod_type then senv' + else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv' in (mp,mb.mod_delta),senv'' @@ -489,27 +492,24 @@ let start_modtype l senv = let add_module_parameter mbid mte inl senv = let () = check_empty_struct senv in let mp = MPbound mbid in - let mtb = Mod_typing.translate_module_type senv.env mp inl mte in - let senv = full_add_module (Modops.module_body_of_type mp mtb) senv in + let mtb = Mod_typing.translate_modtype senv.env mp inl ([],mte) in + let senv = full_add_module_type mp mtb senv in let new_variant = match senv.modvariant with | STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv) | SIG (params,oldenv) -> SIG ((mbid,mtb) :: params, oldenv) | _ -> assert false in - let new_paramresolver = match mtb.typ_expr with - | SEBstruct _ -> - Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver - | _ -> senv.paramresolver + let new_paramresolver = + if Modops.is_functor mtb.typ_expr then senv.paramresolver + else Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver in mtb.typ_delta, { senv with modvariant = new_variant; paramresolver = new_paramresolver } -let functorize_struct params seb0 = - List.fold_left - (fun seb (arg_id,arg_b) -> SEBfunctor(arg_id,arg_b,seb)) - seb0 params +let functorize params init = + List.fold_left (fun e (mbid,mt) -> MoreFunctor(mbid,mt,e)) init params let propagate_loads senv = List.fold_left @@ -520,36 +520,22 @@ let propagate_loads senv = (** Build the module body of the current module, taking in account a possible return type (_:T) *) +let functorize_module params mb = + let f x = functorize params x in + { mb with + mod_expr = Modops.implem_smartmap f f mb.mod_expr; + mod_type = f mb.mod_type; + mod_type_alg = Option.map f mb.mod_type_alg } + let build_module_body params restype senv = - let mp = senv.modpath in - let mexpr = SEBstruct (List.rev senv.revstruct) in - let mexpr' = functorize_struct params mexpr in - match restype with - | None -> - { mod_mp = mp; - mod_expr = Some mexpr'; - mod_type = mexpr'; - mod_type_alg = None; - mod_constraints = senv.univ; - mod_delta = senv.modresolver; - mod_retroknowledge = senv.local_retroknowledge } - | Some (res,inl) -> - let res_mtb = Mod_typing.translate_module_type senv.env mp inl res in - let auto_mtb = { - typ_mp = mp; - typ_expr = mexpr; - typ_expr_alg = None; - typ_constraints = Univ.empty_constraint; - typ_delta = Mod_subst.empty_delta_resolver} in - let cst = Subtyping.check_subtypes senv.env auto_mtb res_mtb in - { mod_mp = mp; - mod_expr = Some mexpr'; - mod_type = functorize_struct params res_mtb.typ_expr; - mod_type_alg = - Option.map (functorize_struct params) res_mtb.typ_expr_alg; - mod_constraints = Univ.union_constraints cst senv.univ; - mod_delta = res_mtb.typ_delta; - mod_retroknowledge = senv.local_retroknowledge } + let struc = NoFunctor (List.rev senv.revstruct) in + let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) restype in + let mb = + Mod_typing.finalize_module senv.env senv.modpath + (struc,None,senv.modresolver,senv.univ) restype' + in + let mb' = functorize_module params mb in + { mb' with mod_retroknowledge = senv.local_retroknowledge } (** Returning back to the old pre-interactive-module environment, with one extra component and some updated fields @@ -582,10 +568,9 @@ let end_module l restype senv = let senv'= propagate_loads {senv with env=newenv} in let newenv = Environ.add_constraints mb.mod_constraints senv'.env in let newenv = Modops.add_module mb newenv in - let newresolver = match mb.mod_type with - | SEBstruct _ -> - Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver - | _ -> oldsenv.modresolver + let newresolver = + if Modops.is_functor mb.mod_type then oldsenv.modresolver + else Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver in (mp,mbids,mb.mod_delta), propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv @@ -596,14 +581,14 @@ let end_modtype l senv = let () = check_current_label l mp in let () = check_empty_context senv in let mbids = List.rev_map fst params in - let auto_tb = SEBstruct (List.rev senv.revstruct) in + let auto_tb = NoFunctor (List.rev senv.revstruct) in let newenv = oldsenv.env in let newenv = Environ.add_constraints senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in let senv' = propagate_loads {senv with env=newenv} in let mtb = { typ_mp = mp; - typ_expr = functorize_struct params auto_tb; + typ_expr = functorize params auto_tb; typ_expr_alg = None; typ_constraints = senv'.univ; typ_delta = senv.modresolver } @@ -616,22 +601,21 @@ let end_modtype l senv = (** {6 Inclusion of module or module type } *) let add_include me is_module inl senv = + let open Mod_typing in let mp_sup = senv.modpath in let sign,cst,resolver = if is_module then - let sign,_,resolver,cst = - Mod_typing.translate_struct_include_module_entry senv.env mp_sup inl me - in - sign,cst,resolver + let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in + sign,cst,reso else - let mtb = Mod_typing.translate_module_type senv.env mp_sup inl me in + let mtb = translate_modtype senv.env mp_sup inl ([],me) in mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta in let senv = add_constraints (Now cst) senv in (* Include Self support *) let rec compute_sign sign mb resolver senv = match sign with - | SEBfunctor(mbid,mtb,str) -> + | MoreFunctor(mbid,mtb,str) -> let cst_sub = Subtyping.check_subtypes senv.env mb mtb in let senv = add_constraints (Now cst_sub) senv in let mpsup_delta = @@ -639,21 +623,21 @@ let add_include me is_module inl senv = in let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in - compute_sign (Modops.subst_struct_expr subst str) mb resolver senv + compute_sign (Modops.subst_signature subst str) mb resolver senv | str -> resolver,str,senv in let resolver,sign,senv = let mtb = { typ_mp = mp_sup; - typ_expr = SEBstruct (List.rev senv.revstruct); + typ_expr = NoFunctor (List.rev senv.revstruct); typ_expr_alg = None; typ_constraints = Univ.empty_constraint; typ_delta = senv.modresolver } in compute_sign sign mtb resolver senv in let str = match sign with - | SEBstruct str_l -> str_l - | _ -> Modops.error_higher_order_include () + | NoFunctor struc -> struc + | MoreFunctor _ -> Modops.error_higher_order_include () in let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv in @@ -682,7 +666,7 @@ type compiled_library = { type native_library = Nativecode.global list -let join_compiled_library l = Modops.join_module_body l.comp_mod +let join_compiled_library l = Modops.join_module l.comp_mod let start_library dir senv = check_initial senv; @@ -702,10 +686,10 @@ let export senv dir = in let () = check_current_library dir senv in let mp = senv.modpath in - let str = SEBstruct (List.rev senv.revstruct) in + let str = NoFunctor (List.rev senv.revstruct) in let mb = { mod_mp = mp; - mod_expr = Some str; + mod_expr = FullStruct; mod_type = str; mod_type_alg = None; mod_constraints = senv.univ; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 3d67f6c07..5d1c98de5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -73,7 +73,7 @@ val add_module : Label.t -> Entries.module_entry -> Declarations.inline -> (module_path * Mod_subst.delta_resolver) safe_transformer val add_modtype : - Label.t -> Entries.module_struct_entry -> Declarations.inline -> + Label.t -> Entries.module_type_entry -> Declarations.inline -> module_path safe_transformer (** Adding universe constraints *) @@ -94,6 +94,8 @@ val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer +(** The optional result type is given without its functorial part *) + val end_module : Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 99c1b8483..6cedb6ad2 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -319,10 +319,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = check_conv error cst conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = - let mty1 = module_type_of_module None msb1 in - let mty2 = module_type_of_module None msb2 in - let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in - cst + let mty1 = module_type_of_module msb1 in + let mty2 = module_type_of_module msb2 in + check_modtypes cst env mty1 mty2 subst1 subst2 false and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let map1 = make_labmap mp1 sig1 in @@ -344,67 +343,62 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= | Modtype mtb -> mtb | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected in - let env = add_module (module_body_of_type mtb2.typ_mp mtb2) - (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in - check_modtypes cst env mtb1 mtb2 subst1 subst2 true + let env = + add_module_type mtb2.typ_mp mtb2 + (add_module_type mtb1.typ_mp mtb1 env) + in + check_modtypes cst env mtb1 mtb2 subst1 subst2 true in List.fold_left check_one_body cst sig2 -and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = - if mtb1==mtb2 then cst else - let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in - let rec check_structure cst env str1 str2 equiv subst1 subst2 = - match str1,str2 with - | SEBstruct (list1), - SEBstruct (list2) -> - if equiv then - let subst2 = - add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in - Univ.union_constraints - (check_signatures cst env - mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 - mtb1.typ_delta mtb2.typ_delta) - (check_signatures cst env - mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1 - mtb2.typ_delta mtb1.typ_delta) - else - check_signatures cst env - mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 - mtb1.typ_delta mtb2.typ_delta - | SEBfunctor (arg_id1,arg_t1,body_t1), - SEBfunctor (arg_id2,arg_t2,body_t2) -> - let subst1 = - (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in - let cst = check_modtypes cst env - arg_t2 arg_t1 subst2 subst1 - equiv in - (* contravariant *) - let env = add_module - (module_body_of_type (MPbound arg_id2) arg_t2) env - in - let env = match body_t1 with - SEBstruct str -> - add_module {mod_mp = mtb1.typ_mp; - mod_expr = None; - mod_type = subst_struct_expr subst1 body_t1; - mod_type_alg= None; - mod_constraints=mtb1.typ_constraints; - mod_retroknowledge = []; - mod_delta = mtb1.typ_delta} env - | _ -> env - in - check_structure cst env body_t1 body_t2 equiv - subst1 - subst2 - | _ , _ -> error_incompatible_modtypes mtb1 mtb2 - in - if mtb1'== mtb2' then cst - else check_structure cst env mtb1' mtb2' equiv subst1 subst2 +and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then cst + else + let rec check_structure cst env str1 str2 equiv subst1 subst2 = + match str1,str2 with + |NoFunctor list1, + NoFunctor list2 -> + if equiv then + let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in + let cst1 = check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta + in + let cst2 = check_signatures cst env + mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1 + mtb2.typ_delta mtb1.typ_delta + in + Univ.union_constraints cst1 cst2 + else + check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta + |MoreFunctor (arg_id1,arg_t1,body_t1), + MoreFunctor (arg_id2,arg_t2,body_t2) -> + let mp2 = MPbound arg_id2 in + let subst1 = join (map_mbid arg_id1 mp2 arg_t2.typ_delta) subst1 in + let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in + (* contravariant *) + let env = add_module_type mp2 arg_t2 env in + let env = + if Modops.is_functor body_t1 then env + else add_module + {mod_mp = mtb1.typ_mp; + mod_expr = Abstract; + mod_type = subst_signature subst1 body_t1; + mod_type_alg = None; + mod_constraints = mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + in + check_structure cst env body_t1 body_t2 equiv subst1 subst2 + | _ , _ -> error_incompatible_modtypes mtb1 mtb2 + in + check_structure cst env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2 let check_subtypes env sup super = - let env = add_module - (module_body_of_type sup.typ_mp sup) env in - check_modtypes empty_constraint env + let env = add_module_type sup.typ_mp sup env in + check_modtypes empty_constraint env (strengthen sup sup.typ_mp) super empty_subst (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false diff --git a/library/assumptions.ml b/library/assumptions.ml index 2418f0648..b1f133ac3 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -67,6 +67,23 @@ let rec search_cst_label lab = function | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields +(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: + a) I don't see currently what should be used instead + b) this shouldn't be critical for Print Assumption. At worse some + constants will have a canonical name which is non-canonical, + leading to failures in [Global.lookup_constant], but our own + [lookup_constant] should work. +*) + +let rec fields_of_functor f subs mp0 args = function + |NoFunctor a -> f subs mp0 args a + |MoreFunctor (mbid,_,e) -> + match args with + | [] -> assert false (* we should only encounter applied functors *) + | mpa :: args -> + let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in + fields_of_functor f subs mp0 args e + let rec lookup_module_in_impl mp = try Global.lookup_module mp with Not_found -> @@ -93,43 +110,29 @@ and fields_of_mp mp = if mp_eq inner_mp mp then subs else add_mp inner_mp mp mb.mod_delta subs in - Modops.subst_signature subs fields + Modops.subst_structure subs fields -and fields_of_mb subs mb args = - let seb = match mb.mod_expr with - | None -> mb.mod_type (* cf. Declare Module *) - | Some seb -> seb - in - fields_of_seb subs mb.mod_mp seb args +and fields_of_mb subs mb args = match mb.mod_expr with + |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr + |Struct sign -> fields_of_signature subs mb.mod_mp args sign + |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type -(* TODO: using [empty_delta_resolver] below in [fields_of_seb] - is probably slightly incorrect. But: - a) I don't see currently what should be used instead - b) this shouldn't be critical for Print Assumption. At worse some - constants will have a canonical name which is non-canonical, - leading to failures in [Global.lookup_constant], but our own - [lookup_constant] should work. -*) +(** The Abstract case above corresponds to [Declare Module] *) -and fields_of_seb subs mp0 seb args = match seb with - | SEBstruct l -> - let () = assert (List.is_empty args) in - l, mp0, subs - | SEBident mp -> +and fields_of_signature x = + fields_of_functor + (fun subs mp0 args struc -> + assert (List.is_empty args); + (struc, mp0, subs)) x + +and fields_of_expr subs mp0 args = function + |MEident mp -> let mb = lookup_module_in_impl (subst_mp subs mp) in fields_of_mb subs mb args - | SEBapply (seb1,seb2,_) -> - (match seb2 with - | SEBident mp2 -> fields_of_seb subs mp0 seb1 (mp2::args) - | _ -> assert false) (* only legal application is to module names *) - | SEBfunctor (mbid,mtb,seb) -> - (match args with - | [] -> assert false (* we should only encounter applied functors *) - | mpa :: args -> - let subs = add_mbid mbid mpa empty_delta_resolver subs in - fields_of_seb subs mp0 seb args) - | SEBwith _ -> assert false (* should not appear in a mod_expr - or mod_type field *) + |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1 + |MEwith _ -> assert false (* no 'with' in [mod_expr] *) + +and fields_of_expression x = fields_of_functor fields_of_expr x let lookup_constant_in_impl cst fallback = try diff --git a/library/declaremods.ml b/library/declaremods.ml index 5c0700606..8d332b7df 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -336,15 +336,14 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs (** Turn a chain of [MSEapply] into the head module_path and the list of module_path parameters (deepest param coming first). - Currently, right part of [MSEapply] must be [MSEident], - and left part must be either [MSEident] or another [MSEapply]. *) + The left part of a [MSEapply] must be either [MSEident] or + another [MSEapply]. *) let get_applications mexpr = let rec get params = function - | MSEident mp -> mp, params - | MSEapply (fexpr, MSEident mp) -> get (mp::params) fexpr - | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr - | _ -> error "Application of a non-functor." + | MEident mp -> mp, params + | MEapply (fexpr, mp) -> get (mp::params) fexpr + | MEwith _ -> error "Non-atomic functor application." in get [] mexpr (** Create the substitution corresponding to some functor applications *) @@ -357,10 +356,10 @@ let rec compute_subst env mbids sign mp_l inl = let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mb = Environ.lookup_module mp env in let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = match mb.mod_type with - | SEBstruct _ -> - Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - | _ -> empty_delta_resolver (* case of a functor *) + let resolver = + if Modops.is_functor mb.mod_type then empty_delta_resolver + else + Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta in mbid_left,join (map_mbid mbid mp resolver) subst @@ -386,25 +385,21 @@ let type_of_mod mp env = function |false -> (Environ.lookup_modtype mp env).typ_expr let rec get_module_path = function - |MSEident mp -> mp - |MSEfunctor (_,_,me) -> get_module_path me - |MSEwith (me,_) -> get_module_path me - |MSEapply _ as me -> fst (get_applications me) + |MEident mp -> mp + |MEwith (me,_) -> get_module_path me + |MEapply (me,_) -> get_module_path me (** Substitutive objects of a module expression (or module type) *) let rec get_module_sobjs is_mod env inl = function - |MSEident mp -> + |MEident mp -> begin match ModSubstObjs.get mp with |(mbids,Objs _) when not (ModPath.is_bound mp) -> (mbids,Ref (mp, empty_subst)) (* we create an alias *) |sobjs -> sobjs end - |MSEfunctor (mbid,_,mexpr) -> - let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in - (mbid::mbids, aobjs) - |MSEwith (mty, With_Definition _) -> get_module_sobjs is_mod env inl mty - |MSEwith (mty, With_Module (idl,mp1)) -> + |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty + |MEwith (mty, WithMod (idl,mp1)) -> assert (not is_mod); let sobjs0 = get_module_sobjs is_mod env inl mty in assert (sobjs_no_functor sobjs0); @@ -413,35 +408,27 @@ let rec get_module_sobjs is_mod env inl = function let objs0 = expand_sobjs sobjs0 in let objs1 = expand_sobjs (ModSubstObjs.get mp1) in ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) - |MSEapply _ as me -> + |MEapply _ as me -> let mp1, mp_l = get_applications me in - let mbids, aobjs = get_module_sobjs is_mod env inl (MSEident mp1) in + let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in let typ = type_of_mod mp1 env is_mod in let mbids_left,subst = compute_subst env mbids typ mp_l inl in (mbids_left, subst_aobjs subst aobjs) +let get_functor_sobjs is_mod env inl (params,mexpr) = + let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in + (List.map fst params @ mbids, aobjs) + (** {6 Handling of module parameters} *) (** For printing modules, [process_module_binding] adds names of bound module (and its components) to Nametab. It also loads - objects associated to it. It may raise a [Failure] when the - bound module hasn't an atomic type. *) - -let rec seb2mse = function - | SEBident mp -> MSEident mp - | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s') - | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp)) - | SEBwith (s,With_definition_body(l,cb)) -> - (match cb.const_body with - | Def c -> MSEwith(seb2mse s,With_Definition(l,Lazyconstr.force c)) - | _ -> assert false) - | _ -> failwith "seb2mse: received a non-atomic seb" - -let process_module_binding mbid seb = + objects associated to it. *) + +let process_module_binding mbid me = let dir = DirPath.make [MBId.to_id mbid] in let mp = MPbound mbid in - let me = seb2mse seb in let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in let subst = map_mp (get_module_path me) mp empty_delta_resolver in let sobjs = subst_sobjs subst sobjs in @@ -468,7 +455,7 @@ let intern_arg interp_modast acc (idl,(typ,ann)) = let resolver = Global.add_module_parameter mbid mty inl in let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in do_module false Lib.load_objects 1 dir mp sobjs []; - (mbid,(mty,inl))::acc) + (mbid,mty,inl)::acc) acc idl (** Process a list of declarations of functor parameters @@ -504,7 +491,7 @@ let check_subtypes mp sub_mtb_l = let mb = try Global.lookup_module mp with Not_found -> assert false in - let mtb = Modops.module_type_of_module None mb in + let mtb = Modops.module_type_of_module mb in check_sub mtb sub_mtb_l (** Same for module type [mp] *) @@ -515,24 +502,21 @@ let check_subtypes_mt mp sub_mtb_l = in check_sub mtb sub_mtb_l -(** Create a functor entry. +(** Create a params entry. In [args], the youngest module param now comes first. *) -let mk_funct_entry args entry0 = - List.fold_left - (fun entry (arg_id,(arg_t,_)) -> - MSEfunctor (arg_id,arg_t,entry)) - entry0 args +let mk_params_entry args = + List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args (** Create a functor type struct. In [args], the youngest module param now comes first. *) let mk_funct_type env args seb0 = List.fold_left - (fun seb (arg_id,(arg_t,arg_inl)) -> + (fun seb (arg_id,arg_t,arg_inl) -> let mp = MPbound arg_id in - let arg_t = Mod_typing.translate_module_type env mp arg_inl arg_t in - SEBfunctor(arg_id,arg_t,seb)) + let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in + MoreFunctor(arg_id,arg_t,seb)) seb0 args (** Prepare the module type list for check of subtypes *) @@ -542,7 +526,7 @@ let build_subtypes interp_modast env mp args mtys = (fun (m,ann) -> let inl = inl2intopt ann in let mte,_ = interp_modast env ModType m in - let mtb = Mod_typing.translate_module_type env mp inl mte in + let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in { mtb with typ_expr = mk_funct_type env args mtb.typ_expr }) mtys @@ -583,7 +567,8 @@ let start_module interp_modast export id args res fs = | Enforce (res,ann) -> let inl = inl2intopt ann in let mte,_ = interp_modast env ModType res in - let _ = Mod_typing.translate_struct_type_entry env inl mte in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in Some (mte,inl), [] | Check resl -> None, build_subtypes interp_modast env mp arg_entries_r resl @@ -636,32 +621,31 @@ let declare_module interp_modast id args res mexpr_o fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_module id in - let arg_entries_r = intern_args interp_modast args - in + let arg_entries_r = intern_args interp_modast args in + let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mk_entry k m = mk_funct_entry arg_entries_r (fst (interp_modast env k m)) - in let mty_entry_o, subs, inl_res = match res with | Enforce (mty,ann) -> - Some (mk_entry ModType mty), [], inl2intopt ann + Some (fst (interp_modast env ModType mty)), [], inl2intopt ann | Check mtys -> None, build_subtypes interp_modast env mp arg_entries_r mtys, default_inline () in let mexpr_entry_o, inl_expr = match mexpr_o with | None -> None, default_inline () - | Some (mexpr,ann) -> Some (mk_entry Module mexpr), inl2intopt ann + | Some (mexpr,ann) -> + Some (fst (interp_modast env Module mexpr)), inl2intopt ann in - let entry = - {mod_entry_type = mty_entry_o; - mod_entry_expr = mexpr_entry_o } + let entry = match mexpr_entry_o, mty_entry_o with + | None, None -> assert false (* No body, no type ... *) + | None, Some typ -> MType (params, typ) + | Some body, otyp -> MExpr (params, body, otyp) in let sobjs, mp0 = match entry with - | {mod_entry_type = Some mte} -> - get_module_sobjs false env inl_res mte, get_module_path mte - | {mod_entry_expr = Some me} -> - get_module_sobjs true env inl_expr me, get_module_path me - | _ -> assert false (* No type, no body ... *) + | MType (_,mte) | MExpr (_,_,Some mte) -> + get_functor_sobjs false env inl_res (params,mte), get_module_path mte + | MExpr (_,me,None) -> + get_functor_sobjs true env inl_expr (params,me), get_module_path me in (* Undo the simulated interactive building of the module and declare the module as a whole *) @@ -720,16 +704,13 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in - let arg_entries_r = intern_args interp_modast args - in + let arg_entries_r = intern_args interp_modast args in + let params = mk_params_entry arg_entries_r in let env = Global.env () in - let entry,_ = interp_modast env ModType mty in - let entry = mk_funct_entry arg_entries_r entry in - + let entry = params, fst (interp_modast env ModType mty) in let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in - - let sobjs = get_module_sobjs false env inl entry in - let subst = map_mp (get_module_path entry) mp empty_delta_resolver in + let sobjs = get_functor_sobjs false env inl entry in + let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in let sobjs = subst_sobjs subst sobjs in (* Undo the simulated interactive building of the module type @@ -767,17 +748,17 @@ let rec include_subst env mp reso mbids sign inline = match mbids with let rec decompose_functor mpl typ = match mpl, typ with | [], _ -> typ - | _::mpl, SEBfunctor(_,_,str) -> decompose_functor mpl str + | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str | _ -> error "Application of a functor with too much arguments." exception NoIncludeSelf let type_of_incl env is_mod = function - |MSEident mp -> type_of_mod mp env is_mod - |MSEapply _ as me -> + |MEident mp -> type_of_mod mp env is_mod + |MEapply _ as me -> let mp0, mp_l = get_applications me in decompose_functor mp_l (type_of_mod mp0 env is_mod) - |_ -> raise NoIncludeSelf + |MEwith _ -> raise NoIncludeSelf let declare_one_include interp_modast (me_ast,annot) = let env = Global.env() in diff --git a/library/declaremods.mli b/library/declaremods.mli index f18ed2807..89bcccef3 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -118,4 +118,4 @@ val debug_print_modtab : unit -> Pp.std_ppcmds bound module hasn't an atomic type. *) val process_module_binding : - MBId.t -> Declarations.struct_expr_body -> unit + MBId.t -> Declarations.module_alg_expr -> unit diff --git a/library/global.mli b/library/global.mli index 1bc745bb7..c62f51e16 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,7 +46,7 @@ val add_module : Id.t -> Entries.module_entry -> Declarations.inline -> module_path * Mod_subst.delta_resolver val add_modtype : - Id.t -> Entries.module_struct_entry -> Declarations.inline -> module_path + Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index cc302b95d..7fffc960b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Miniml open Term open Declarations open Names @@ -14,7 +15,6 @@ open Globnames open Pp open Errors open Util -open Miniml open Table open Extraction open Modutil @@ -47,7 +47,7 @@ let toplevel_env () = end | _ -> None in - SEBstruct (List.rev (List.map_filter get_reference (Lib.contents ()))) + List.rev (List.map_filter get_reference (Lib.contents ())) let environment_until dir_opt = @@ -55,11 +55,11 @@ let environment_until dir_opt = | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] | [] -> [] | d :: l -> - match (Global.lookup_module (MPfile d)).mod_expr with - | Some meb -> - if dir_opt = Some d then [MPfile d, meb] - else (MPfile d, meb) :: (parse l) - | _ -> assert false + let meb = + Modops.destr_nofunctor (Global.lookup_module (MPfile d)).mod_type + in + if dir_opt = Some d then [MPfile d, meb] + else (MPfile d, meb) :: (parse l) in parse (Library.loaded_libraries ()) @@ -168,113 +168,106 @@ let factor_fix env l cb msb = labels, recd, msb'' end -(** Expanding a [struct_expr_body] into a version without abbreviations +(** Expanding a [module_alg_expr] into a version without abbreviations or functor applications. This is done via a detour to entries (hack proposed by Elie) *) -let rec seb2mse = function - | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s') - | SEBident mp -> Entries.MSEident mp - | _ -> failwith "seb2mse: received a non-atomic seb" - -let expand_seb env mp seb = - let seb,_,_,_ = - let inl = Some (Flags.get_inline_level()) in - Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb) - in seb - -(** When possible, we use the nicer, shorter, algebraic type structures - instead of the expanded ones. *) - -let my_type_of_mb mb = - let m0 = mb.mod_type in - match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0 - -let my_type_of_mtb mtb = - let m0 = mtb.typ_expr in - match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0 +let expand_mexpr env mp me = + let inl = Some (Flags.get_inline_level()) in + let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in + sign (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) -let rec msid_of_seb = function - | SEBident mp -> mp - | SEBwith (seb,_) -> msid_of_seb seb +let rec mp_of_mexpr = function + | MEident mp -> mp + | MEwith (seb,_) -> mp_of_mexpr seb | _ -> assert false -let env_for_mtb_with_def env mp seb idl = - let sig_b = match seb with - | SEBstruct(sig_b) -> sig_b - | _ -> assert false - in +let env_for_mtb_with_def env mp me idl = + let struc = Modops.destr_nofunctor me in let l = Label.of_id (List.hd idl) in - let spot = function (l',SFBconst _) -> l = l' | _ -> false in - let before = fst (List.split_when spot sig_b) in - Modops.add_signature mp before empty_delta_resolver env + let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in + let before = fst (List.split_when spot struc) in + Modops.add_structure mp before empty_delta_resolver env (* From a [structure_body] (i.e. a list of [structure_field_body]) to specifications. *) -let rec extract_sfb_spec env mp = function +let rec extract_structure_spec env mp = function | [] -> [] | (l,SFBconst cb) :: msig -> let kn = Constant.make2 mp l in let s = extract_constant_spec env kn cb in - let specs = extract_sfb_spec env mp msig in + let specs = extract_structure_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> let mind = MutInd.make2 mp l in let s = Sind (mind, extract_inductive env mind) in - let specs = extract_sfb_spec env mp msig in + let specs = extract_structure_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmodule mb) :: msig -> - let specs = extract_sfb_spec env mp msig in - let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in + let specs = extract_structure_spec env mp msig in + let spec = extract_mb_spec env mb.mod_mp mb in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> - let specs = extract_sfb_spec env mp msig in - let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in + let specs = extract_structure_spec env mp msig in + let spec = extract_mtb_spec env mtb.typ_mp mtb in (l,Smodtype spec) :: specs -(* From [struct_expr_body] to specifications *) +(* From [module_expression] to specifications *) -(* Invariant: the [seb] given to [extract_seb_spec] should either come +(* Invariant: the [me] given to [extract_mexpr_spec] should either come from a [mod_type] or [type_expr] field, or their [_alg] counterparts. - This way, any encountered [SEBident] should be a true module type. + This way, any encountered [MEident] should be a true module type. *) -and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with - | SEBident mp -> Visit.add_mp_all mp; MTident mp - | SEBwith(seb',With_definition_body(idl,cb))-> - let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in - let mt = extract_seb_spec env mp1 (seb,seb') in - (match extract_with_type env' cb with (* cb peut contenir des kn *) +and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with + | MEident mp -> Visit.add_mp_all mp; MTident mp + | MEwith(me',WithDef(idl,c))-> + let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in + let mt = extract_mexpr_spec env mp1 (me_struct,me') in + (match extract_with_type env' c with (* cb may contain some kn *) | None -> mt | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) - | SEBwith(seb',With_module_body(idl,mp))-> + | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; - MTwith(extract_seb_spec env mp1 (seb,seb'), - ML_With_module(idl,mp)) - | SEBfunctor (mbid, mtb, seb_alg') -> - let seb' = match seb with - | SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb' + MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) + | MEapply _ -> extract_msignature_spec env mp1 me_struct + +and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with + | MoreFunctor (mbid, mtb, me_alg') -> + let me_struct' = match me_struct with + | MoreFunctor (mbid',_,me') when MBId.equal mbid' mbid -> me' | _ -> assert false in let mp = MPbound mbid in - let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in - MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb), - extract_seb_spec env' mp1 (seb',seb_alg')) - | SEBstruct (msig) -> - let env' = Modops.add_signature mp1 msig empty_delta_resolver env in - MTsig (mp1, extract_sfb_spec env' mp1 msig) - | SEBapply _ -> - if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb) - else assert false + let env' = Modops.add_module_type mp mtb env in + MTfunsig (mbid, extract_mtb_spec env mp mtb, + extract_mexpression_spec env' mp1 (me_struct',me_alg')) + | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m) + +and extract_msignature_spec env mp1 = function + | NoFunctor struc -> + let env' = Modops.add_structure mp1 struc empty_delta_resolver env in + MTsig (mp1, extract_structure_spec env' mp1 struc) + | MoreFunctor (mbid, mtb, me) -> + let mp = MPbound mbid in + let env' = Modops.add_module_type mp mtb env in + MTfunsig (mbid, extract_mtb_spec env mp mtb, + extract_msignature_spec env' mp1 me) +and extract_mtb_spec env mp mtb = match mtb.typ_expr_alg with + | Some ty -> extract_mexpression_spec env mp (mtb.typ_expr,ty) + | None -> extract_msignature_spec env mp mtb.typ_expr +and extract_mb_spec env mp mb = match mb.mod_type_alg with + | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty) + | None -> extract_msignature_spec env mp mb.mod_type (* From a [structure_body] (i.e. a list of [structure_field_body]) to implementations. @@ -283,13 +276,13 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with important: last to first ensures correct dependencies. *) -let rec extract_sfb env mp all = function +let rec extract_structure env mp all = function | [] -> [] - | (l,SFBconst cb) :: msb -> + | (l,SFBconst cb) :: struc -> (try - let vl,recd,msb = factor_fix env l cb msb in + let vl,recd,struc = factor_fix env l cb struc in let vc = Array.map (Constant.make2 mp) vl in - let ms = extract_sfb env mp all msb in + let ms = extract_structure env mp all struc in let b = Array.exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in @@ -297,7 +290,7 @@ let rec extract_sfb env mp all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_sfb env mp all msb in + let ms = extract_structure env mp all struc in let c = Constant.make2 mp l in let b = Visit.needed_con c in if all || b then @@ -305,8 +298,8 @@ let rec extract_sfb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) - | (l,SFBmind mib) :: msb -> - let ms = extract_sfb env mp all msb in + | (l,SFBmind mib) :: struc -> + let ms = extract_structure env mp all struc in let mind = MutInd.make2 mp l in let b = Visit.needed_ind mind in if all || b then @@ -314,41 +307,54 @@ let rec extract_sfb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms - | (l,SFBmodule mb) :: msb -> - let ms = extract_sfb env mp all msb in + | (l,SFBmodule mb) :: struc -> + let ms = extract_structure env mp all struc in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodule (extract_module env mp true mb)) :: ms else ms - | (l,SFBmodtype mtb) :: msb -> - let ms = extract_sfb env mp all msb in + | (l,SFBmodtype mtb) :: struc -> + let ms = extract_structure env mp all struc in let mp = MPdot (mp,l) in - if all || Visit.needed_mp mp then - (l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms + if all || Visit.needed_mp mp then + (l,SEmodtype (extract_mtb_spec env mp mtb)) :: ms else ms -(* From [struct_expr_body] to implementations *) +(* From [module_expr] and [module_expression] to implementations *) -and extract_seb env mp all = function - | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml -> +and extract_mexpr env mp all = function + | MEwith _ -> assert false (* no 'with' syntax for modules *) + | me when lang () <> Ocaml -> (* in Haskell/Scheme, we expand everything *) - extract_seb env mp all (expand_seb env mp seb) - | SEBident mp -> + extract_msignature env mp all (expand_mexpr env mp me) + | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; - Visit.add_mp_all mp; MEident mp - | SEBapply (meb, meb',_) -> - MEapply (extract_seb env mp true meb, - extract_seb env mp true meb') - | SEBfunctor (mbid, mtb, meb) -> + Visit.add_mp_all mp; Miniml.MEident mp + | MEapply (me, arg) -> + Miniml.MEapply (extract_mexpr env mp true me, + extract_mexpr env mp true (MEident arg)) + +and extract_mexpression env mp all = function + | NoFunctor me -> extract_mexpr env mp all me + | MoreFunctor (mbid, mtb, me) -> let mp1 = MPbound mbid in - let env' = Modops.add_module (Modops.module_body_of_type mp1 mtb) - env in - MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb), - extract_seb env' mp true meb) - | SEBstruct (msb) -> - let env' = Modops.add_signature mp msb empty_delta_resolver env in - MEstruct (mp,extract_sfb env' mp all msb) - | SEBwith (_,_) -> anomaly (Pp.str "Not available yet") + let env' = Modops.add_module_type mp1 mtb env in + Miniml.MEfunctor + (mbid, + extract_mtb_spec env mp1 mtb, + extract_mexpression env' mp true me) + +and extract_msignature env mp all = function + | NoFunctor struc -> + let env' = Modops.add_structure mp struc empty_delta_resolver env in + Miniml.MEstruct (mp,extract_structure env' mp all struc) + | MoreFunctor (mbid, mtb, me) -> + let mp1 = MPbound mbid in + let env' = Modops.add_module_type mp1 mtb env in + Miniml.MEfunctor + (mbid, + extract_mtb_spec env mp1 mtb, + extract_msignature env' mp true me) and extract_module env mp all mb = (* A module has an empty [mod_expr] when : @@ -357,14 +363,14 @@ and extract_module env mp all mb = Since we look at modules from outside, we shouldn't have variables. But a Declare Module at toplevel seems legal (cf #2525). For the moment we don't support this situation. *) - match mb.mod_expr with - | None -> error_no_module_expr mp - | Some me -> - { ml_mod_expr = extract_seb env mp all me; - ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } - - -let unpack = function MEstruct (_,sel) -> sel | _ -> assert false + let impl = match mb.mod_expr with + | Abstract -> error_no_module_expr mp + | Algebraic me -> extract_mexpression env mp all me + | Struct sign -> extract_msignature env mp all sign + | FullStruct -> extract_msignature env mp all mb.mod_type + in + { ml_mod_expr = impl; + ml_mod_type = extract_mb_spec env mp mb } let mono_environment refs mpl = Visit.reset (); @@ -373,7 +379,8 @@ let mono_environment refs mpl = let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m)) + (fun (mp,struc) -> + mp, extract_structure env mp (Visit.needed_mp_all mp) struc) l (**************************************) @@ -620,9 +627,9 @@ let extraction_library is_rec m = Visit.add_mp_all (MPfile dir_m); let env = Global.env () in let l = List.rev (environment_until (Some dir_m)) in - let select l (mp,meb) = + let select l (mp,struc) = if Visit.needed_mp mp - then (mp, unpack (extract_seb env mp true meb)) :: l + then (mp, extract_structure env mp true struc) :: l else l in let struc = List.fold_left select [] l in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 68f832997..6c1be2d36 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1024,17 +1024,12 @@ let extract_constant_spec env kn cb = let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) -let extract_with_type env cb = - let typ = Typeops.type_of_constant_type env cb.const_type in +let extract_with_type env c = + let typ = type_of env c in match flag_of_type env typ with | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in let db = db_from_sign s in - let c = match cb.const_body with - | Def body -> Lazyconstr.force body - (* A "with Definition ..." is necessarily transparent *) - | Undef _ | OpaqueDef _ -> assert false - in let t = extract_type_scheme env db c (List.length s) in Some (vl, t) | _ -> None diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 3a5fc9794..89db50e63 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -19,7 +19,7 @@ val extract_constant : env -> constant -> constant_body -> ml_decl val extract_constant_spec : env -> constant -> constant_body -> ml_spec -val extract_with_type : env -> constant_body -> ( Id.t list * ml_type ) option +val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option val extract_fixpoint : env -> constant array -> (constr, types) prec_declaration -> ml_decl diff --git a/printing/printmod.ml b/printing/printmod.ml index ee4a2db7f..b5d1d8a18 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -114,18 +114,24 @@ let nametab_register_module_body mp struc = nametab_register_dir mp; List.iter (nametab_register_body mp DirPath.empty) struc -let nametab_register_module_param mbid seb = - (* For algebraic seb, we use a Declaremods function that converts into mse *) - try Declaremods.process_module_binding mbid seb - with e when Errors.noncritical e -> - (* Otherwise, for expanded structure, we try to play with the nametab *) - match seb with - | SEBstruct struc -> - let mp = MPbound mbid in - let dir = DirPath.make [MBId.to_id mbid] in - nametab_register_dir mp; - List.iter (nametab_register_body mp dir) struc - | _ -> () +let get_typ_expr_alg mtb = match mtb.typ_expr_alg with + | Some (NoFunctor me) -> me + | _ -> raise Not_found + +let nametab_register_modparam mbid mtb = + match mtb.typ_expr with + | MoreFunctor _ -> () (* functorial param : nothing to register *) + | NoFunctor struc -> + (* We first try to use the algebraic type expression if any, + via a Declaremods function that converts back to module entries *) + try + Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) + with e when Errors.noncritical e -> + (* Otherwise, we try to play with the nametab ourselves *) + let mp = MPbound mbid in + let dir = DirPath.make [MBId.to_id mbid] in + nametab_register_dir mp; + List.iter (nametab_register_body mp dir) struc let print_body is_impl env mp (l,body) = let name = str (Label.to_string l) in @@ -161,71 +167,71 @@ let print_body is_impl env mp (l,body) = let print_struct is_impl env mp struc = prlist_with_sep spc (print_body is_impl env mp) struc +let print_structure is_type env mp locals struc = + let env' = Option.map + (Modops.add_structure mp struc Mod_subst.empty_delta_resolver) env in + nametab_register_module_body mp struc; + let kwd = if is_type then "Sig" else "Struct" in + hv 2 (str kwd ++ spc () ++ print_struct false env' mp struc ++ + brk (1,-2) ++ str "End") + let rec flatten_app mexpr l = match mexpr with - | SEBapply (mexpr, SEBident arg,_) -> flatten_app mexpr (arg::l) - | SEBident mp -> mp::l - | _ -> assert false + | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l) + | MEident mp -> mp::l + | MEwith _ -> assert false -let rec print_modtype env mp locals mty = +let rec print_typ_expr env mp locals mty = match mty with - | SEBident kn -> print_kn locals kn - | SEBfunctor (mbid,mtb1,mtb2) -> - let mp1 = MPbound mbid in - let env' = Option.map - (Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in - let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in - let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals - in - nametab_register_module_param mbid seb1; - hov 2 (str "Funsig" ++ spc () ++ str "(" ++ - pr_id (MBId.to_id mbid) ++ str ":" ++ - print_modtype env mp1 locals seb1 ++ - str ")" ++ spc() ++ print_modtype env' mp locals' mtb2) - | SEBstruct (sign) -> - let env' = Option.map - (Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in - nametab_register_module_body mp sign; - hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++ - brk (1,-2) ++ str "End") - | SEBapply _ -> + | MEident kn -> print_kn locals kn + | MEapply _ -> let lapp = flatten_app mty [] in let fapp = List.hd lapp in let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ prlist_with_sep spc (print_modpath locals) mapp ++ str")") - | SEBwith(seb,With_definition_body(idl,cb))-> + | MEwith(me,WithDef(idl,c))-> let env' = None in (* TODO: build a proper environment if env <> None *) - let s = (String.concat "." (List.map Id.to_string idl)) in - hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++ - str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | SEBwith(seb,With_module_body(idl,mp))-> - let s =(String.concat "." (List.map Id.to_string idl)) in - hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++ - str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - -let rec print_modexpr env mp locals mexpr = match mexpr with - | SEBident mp -> print_modpath locals mp - | SEBfunctor (mbid,mty,mexpr) -> - let mp' = MPbound mbid in - let env' = Option.map - (Modops.add_module (Modops.module_body_of_type mp' mty)) env in - let typ = Option.default mty.typ_expr mty.typ_expr_alg in + let s = String.concat "." (List.map Id.to_string idl) in + hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() + ++ str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + | MEwith(me,WithMod(idl,mp))-> + let s = String.concat "." (List.map Id.to_string idl) in + hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ + str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + +let print_mod_expr env mp locals = function + | MEident mp -> print_modpath locals mp + | MEapply _ as me -> + let lapp = flatten_app me [] in + hov 3 + (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") + | MEwith _ -> assert false (* No 'with' syntax for modules *) + +let rec print_functor fty fatom is_type env mp locals = function + |NoFunctor me -> fatom is_type env mp locals me + |MoreFunctor (mbid,mtb1,me2) -> + nametab_register_modparam mbid mtb1; + let mp1 = MPbound mbid in + let pr_mtb1 = fty env mp1 locals mtb1 in + let env' = Option.map (Modops.add_module_type mp1 mtb1) env in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in - nametab_register_module_param mbid typ; - hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++ - str ":" ++ print_modtype env mp' locals typ ++ - str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr) - | SEBstruct struc -> - let env' = Option.map - (Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in - nametab_register_module_body mp struc; - hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++ - brk (1,-2) ++ str "End") - | SEBapply _ -> - let lapp = flatten_app mexpr [] in - hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") - | SEBwith (_,_)-> anomaly (Pp.str "Not available yet") + let kwd = if is_type then "Funsig" else "Functor" in + hov 2 + (str kwd ++ spc () ++ + str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++ + spc() ++ print_functor fty fatom is_type env' mp locals' me2) + +let rec print_expression x = + print_functor + print_modtype + (function true -> print_typ_expr | false -> print_mod_expr) x + +and print_signature x = + print_functor print_modtype print_structure x +and print_modtype env mp locals mtb = match mtb.typ_expr_alg with + | Some me -> print_expression true env mp locals me + | None -> print_signature true env mp locals mtb.typ_expr let rec printable_body dir = let dir = pop_dirpath dir in @@ -241,23 +247,28 @@ let rec printable_body dir = (** Since we might play with nametab above, we should reset to prior state after the printing *) -let print_modexpr' env mp mexpr = +let print_expression' is_type env mp me = States.with_state_protection - (fun e -> eval_ppcmds (print_modexpr env mp [] e)) mexpr + (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me -let print_modtype' env mp mty = +let print_signature' is_type env mp me = States.with_state_protection - (fun e -> eval_ppcmds (print_modtype env mp [] e)) mty + (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me -let print_module' env mp with_body mb = +let unsafe_print_module env mp with_body mb = let name = print_modpath [] mp in + let pr_equals = spc () ++ str ":= " in let body = match with_body, mb.mod_expr with | false, _ - | true, None -> mt() - | true, Some mexpr -> - spc () ++ str ":= " ++ print_modexpr' env mp mexpr + | true, Abstract -> mt() + | _, Algebraic me -> pr_equals ++ print_expression' false env mp me + | _, Struct sign -> pr_equals ++ print_signature' false env mp sign + | _, FullStruct -> pr_equals ++ print_signature' false env mp mb.mod_type in - let modtype = brk (1,1) ++ str": " ++ print_modtype' env mp mb.mod_type + let modtype = match mb.mod_expr, mb.mod_type_alg with + | FullStruct, _ -> mt () + | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true env mp ty + | _, _ -> brk (1,1) ++ str": " ++ print_signature' true env mp mb.mod_type in hv 0 (str "Module " ++ name ++ modtype ++ body) @@ -267,9 +278,9 @@ let print_module with_body mp = let me = Global.lookup_module mp in try if !short then raise ShortPrinting; - print_module' (Some (Global.env ())) mp with_body me ++ fnl () + unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl () with e when Errors.noncritical e -> - print_module' None mp with_body me ++ fnl () + unsafe_print_module None mp with_body me ++ fnl () let print_modtype kn = let mtb = Global.lookup_modtype kn in @@ -278,6 +289,6 @@ let print_modtype kn = (str "Module Type " ++ name ++ str " =" ++ spc () ++ (try if !short then raise ShortPrinting; - print_modtype' (Some (Global.env ())) kn mtb.typ_expr + print_signature' true (Some (Global.env ())) kn mtb.typ_expr with e when Errors.noncritical e -> - print_modtype' None kn mtb.typ_expr)) + print_signature' true None kn mtb.typ_expr)) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c9090f76e..de77ee131 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -671,8 +671,11 @@ let explain_label_already_declared l = let explain_application_to_not_path _ = str "Application of modules is restricted to paths." -let explain_not_a_functor mtb = - str "Application of not a functor." +let explain_not_a_functor () = + str "Application of a non-functor." + +let explain_is_a_functor () = + str "Illegal use of a functor." let explain_incompatible_module_types mexpr1 mexpr2 = str "Incompatible module types." @@ -687,9 +690,6 @@ let explain_incompatible_labels l l' = str "Opening and closing labels are not the same: " ++ str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!" -let explain_signature_expected mtb = - str "Signature expected." - let explain_not_a_module s = quote (str s) ++ str " is not a module." @@ -719,12 +719,12 @@ let explain_module_error = function | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err | LabelAlreadyDeclared l -> explain_label_already_declared l | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr - | NotAFunctor mtb -> explain_not_a_functor mtb + | NotAFunctor -> explain_not_a_functor () + | IsAFunctor -> explain_is_a_functor () | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2 | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2 | NoSuchLabel l -> explain_no_such_label l | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2 - | SignatureExpected mtb -> explain_signature_expected mtb | NotAModule s -> explain_not_a_module s | NotAModuleType s -> explain_not_a_module_type s | NotAConstant l -> explain_not_a_constant l |