diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 100 | ||||
| -rw-r--r-- | checker/declarations.ml | 99 | ||||
| -rw-r--r-- | checker/declarations.mli | 4 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 373 | ||||
| -rw-r--r-- | checker/modops.ml | 127 | ||||
| -rw-r--r-- | checker/modops.mli | 22 | ||||
| -rw-r--r-- | checker/subtyping.ml | 91 | ||||
| -rw-r--r-- | checker/values.ml | 46 |
8 files changed, 305 insertions, 557 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index fd33516748..0b732e4b99 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 0981cfd1a8..eec76ba396 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 64234e8cdc..ab74114d55 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 66f1194d34..b0f20da70a 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 20f330812b..89ffcb50b3 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 0b94edb545..396eb8e7cf 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 150e99bc9b..7903c33c56 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 974d3431e0..b39d905487 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 *) |