diff options
| -rw-r--r-- | contrib/extraction/extract_env.ml | 29 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 61 | ||||
| -rw-r--r-- | kernel/declarations.ml | 12 | ||||
| -rw-r--r-- | kernel/declarations.mli | 17 | ||||
| -rw-r--r-- | kernel/entries.ml | 1 | ||||
| -rw-r--r-- | kernel/entries.mli | 1 | ||||
| -rw-r--r-- | kernel/environ.ml | 24 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 244 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 10 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 145 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 8 | ||||
| -rw-r--r-- | kernel/modops.ml | 214 | ||||
| -rw-r--r-- | kernel/modops.mli | 20 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 6 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 152 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 123 | ||||
| -rw-r--r-- | kernel/subtyping.mli | 2 | ||||
| -rw-r--r-- | library/declaremods.ml | 204 | ||||
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | library/nametab.ml | 5 | ||||
| -rw-r--r-- | parsing/printmod.ml | 20 |
25 files changed, 902 insertions, 412 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index dabea0f3c..445a26c72 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -35,7 +35,7 @@ let toplevel_env () = | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) | "MODULE TYPE" -> - SFBmodtype (fst (Global.lookup_modtype (MPdot (mp,l)))) + SFBmodtype (Global.lookup_modtype (MPdot (mp,l))) | _ -> failwith "caught" in l,seb | _ -> failwith "caught" @@ -164,10 +164,18 @@ let rec extract_sfb_spec env mp = function (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> let specs = extract_sfb_spec env mp msig in - (l,Smodtype (extract_seb_spec env true(*?*) mtb)) :: specs + (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs + | (l,SFBalias(mp1,_))::msig -> + extract_sfb_spec env mp + ((l,SFBmodule {mod_expr = Some (SEBident mp1); + mod_type = None; + mod_constraints = Univ.Constraint.empty; + mod_alias = Mod_subst.empty_subst; + mod_retroknowledge = []})::msig) (* From [struct_expr_body] to specifications *) + and extract_seb_spec env truetype = function | SEBident kn when truetype -> Visit.add_mp kn; MTident kn | SEBwith(mtb',With_definition_body(idl,cb))-> @@ -182,7 +190,7 @@ and extract_seb_spec env truetype = function | SEBfunctor (mbid, mtb, mtb') -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_seb_spec env true mtb, + MTfunsig (mbid, extract_seb_spec env true mtb.typ_expr, extract_seb_spec env' truetype mtb') | SEBstruct (msid, msig) -> let mp = MPself msid in @@ -240,7 +248,18 @@ let rec extract_sfb env mp all = function let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then - (l,SEmodtype (extract_seb_spec env true(*?*) mtb)) :: ms + (l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms + else ms + | (l,SFBalias (mp1,cst)) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true + {mod_expr = Some (SEBident mp1); + mod_type = None; + mod_constraints= Univ.Constraint.empty; + mod_alias = empty_subst; + mod_retroknowledge = []})) :: ms else ms (* From [struct_expr_body] to implementations *) @@ -255,7 +274,7 @@ and extract_seb env mpo all = function | SEBfunctor (mbid, mtb, meb) -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_seb_spec env true mtb, + MEfunctor (mbid, extract_seb_spec env true mtb.typ_expr, extract_seb env' None true meb) | SEBstruct (msid, msb) -> let mp,msb = match mpo with diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index dca56efae..87f918734 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -20,6 +20,67 @@ open Mod_subst (*S Functions upon modules missing in [Modops]. *) +(*<<<<<<< .mine +(*s Add _all_ direct subobjects of a module, not only those exported. + Build on the [Modops.add_signature] model. *) + +let add_structure mp msb env = + let add_one env (l,elem) = + let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in + match elem with + | SFBconst cb -> Environ.add_constant con cb env + | SFBmind mib -> Environ.add_mind kn mib env + | SFBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env + | SFBmodtype mtb -> Environ.add_modtype (MPdot (mp,l)) mtb env + | SFBalias (mp1,_) -> Environ.register_alias (MPdot (mp,l)) mp1 env + in List.fold_left add_one env msb + +(*s Apply a module path substitution on a module. + Build on the [Modops.subst_modtype] model. *) + +let rec subst_module sub mb = + let mtb' = Option.smartmap (Modops.subst_struct_expr sub) mb.mod_type + and meb' = Option.smartmap (subst_meb sub) mb.mod_expr in + if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) + then mb + else { mod_expr= meb'; + mod_type=mtb'; + mod_constraints=mb.mod_constraints; + mod_alias = mb.mod_alias; + mod_retroknowledge=[] } (* spiwack: since I'm lazy and it's unused at + this point. I forget about retroknowledge, + this may need a change later *) + +and subst_meb sub = function + | SEBident mp -> SEBident (subst_mp sub mp) + | SEBfunctor (mbid, mtb, meb) -> + assert (not (occur_mbid mbid sub)); + SEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb) + | SEBstruct (msid, msb) -> + assert (not (occur_msid msid sub)); + SEBstruct (msid, subst_msb sub msb) + | SEBapply (meb, meb', c) -> + SEBapply (subst_meb sub meb, subst_meb sub meb', c) + | SEBwith (meb,With_module_body(id,mp,cst))-> + SEBwith(subst_meb sub meb, + With_module_body(id,Mod_subst.subst_mp sub mp,cst)) + | SEBwith (meb,With_definition_body(id,cb))-> + SEBwith(subst_meb sub meb, + With_definition_body(id,Declarations.subst_const_body sub cb)) + + +and subst_msb sub msb = + 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 (Modops.subst_modtype sub mtb) + | SFBalias (mp,cst) -> SFBalias(subst_mp sub mp,cst) + in List.map (fun (l,b) -> (l,subst_body b)) msb + +======= +>>>>>>> .r10624 *) (*s Change a msid in a module type, to follow a module expr. Because of the "with" construct, the module type of a module can be a [MTBsig] with a msid different from the one of the module. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 63c690d48..475ef042d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -251,13 +251,14 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBmodtype of struct_expr_body + | SFBalias of module_path * constraints option + | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body | SEBstruct of mod_self_id * structure_body | SEBapply of struct_expr_body * struct_expr_body * constraints @@ -270,8 +271,11 @@ and with_declaration_body = and module_body = { mod_expr : struct_expr_body option; mod_type : struct_expr_body option; - mod_equiv : module_path option; mod_constraints : constraints; + mod_alias : substitution; mod_retroknowledge : Retroknowledge.action list} -type module_type_body = struct_expr_body * module_path option +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 544cea246..03f9be710 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -181,13 +181,14 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBmodtype of struct_expr_body + | SFBalias of module_path * constraints option + | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body | SEBstruct of mod_self_id * structure_body | SEBapply of struct_expr_body * struct_expr_body * constraints @@ -195,14 +196,16 @@ and struct_expr_body = and with_declaration_body = With_module_body of identifier list * module_path * constraints - | With_definition_body of identifier list * constant_body - + | With_definition_body of identifier list * constant_body + and module_body = { mod_expr : struct_expr_body option; mod_type : struct_expr_body option; - mod_equiv : module_path option; mod_constraints : constraints; + mod_alias : substitution; mod_retroknowledge : Retroknowledge.action list} - -type module_type_body = struct_expr_body * module_path option +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} diff --git a/kernel/entries.ml b/kernel/entries.ml index 89e444a74..8dde8fb3e 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -74,6 +74,7 @@ type specification_entry = SPEconst of constant_entry | SPEmind of mutual_inductive_entry | SPEmodule of module_entry + | SPEalias of module_path | SPEmodtype of module_struct_entry and module_struct_entry = diff --git a/kernel/entries.mli b/kernel/entries.mli index b757032f8..6de90d29c 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -73,6 +73,7 @@ type specification_entry = SPEconst of constant_entry | SPEmind of mutual_inductive_entry | SPEmodule of module_entry + | SPEalias of module_path | SPEmodtype of module_struct_entry and module_struct_entry = diff --git a/kernel/environ.ml b/kernel/environ.ml index 64bb3a666..13ef7386f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -287,15 +287,33 @@ let shallow_add_module mp mb env = env_modules = new_mods } in { env with env_globals = new_globals } +let rec scrape_alias mp env = + try + let mp1 = MPmap.find mp env.env_globals.env_alias in + scrape_alias mp1 env + with + Not_found -> mp + let lookup_module mp env = - MPmap.find mp env.env_globals.env_modules + let mp = scrape_alias mp env in + MPmap.find mp env.env_globals.env_modules let lookup_modtype ln env = - MPmap.find ln env.env_globals.env_modtypes + let mp = scrape_alias ln env in + MPmap.find mp env.env_globals.env_modtypes + +let register_alias mp1 mp2 env = + let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in + let new_globals = + { env.env_globals with + env_alias = new_alias } in + { env with env_globals = new_globals } +let lookup_alias mp env = + MPmap.find mp env.env_globals.env_alias (*s Judgments. *) - + type unsafe_judgment = { uj_val : constr; uj_type : types } diff --git a/kernel/environ.mli b/kernel/environ.mli index 19c67435c..c5b4800d5 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -155,6 +155,10 @@ val shallow_add_module : module_path -> module_body -> env -> env val lookup_module : module_path -> env -> module_body val lookup_modtype : module_path -> env -> module_type_body +val register_alias : module_path -> module_path -> env -> env +val lookup_alias : module_path -> env -> module_path +val scrape_alias : module_path -> env -> module_path + (************************************************************************) (*s Universe constraints *) val set_universes : Univ.universes -> env -> env diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index a1e15e3c2..ea477d6a1 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -27,11 +27,15 @@ let apply_opt_resolver resolve kn = | Some resolve -> try List.assoc kn resolve with Not_found -> None -type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id +type substitution_domain = + MSI of mod_self_id + | MBI of mod_bound_id + | MPI of module_path let string_of_subst_domain = function MSI msid -> debug_string_of_msid msid | MBI mbid -> debug_string_of_mbid mbid + | MPI mp -> string_of_mp mp module Umap = Map.Make(struct type t = substitution_domain @@ -46,9 +50,13 @@ let add_msid msid mp = Umap.add (MSI msid) (mp,None) let add_mbid mbid mp resolve = Umap.add (MBI mbid) (mp,resolve) +let add_mp mp1 mp2 = + Umap.add (MPI mp1) (mp2,None) + let map_msid msid mp = add_msid msid mp empty_subst let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst +let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst let list_contents sub = let one_pair uid (mp,_) l = @@ -66,6 +74,7 @@ let debug_pr_subst sub = in str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with @@ -74,13 +83,21 @@ let subst_mp0 sub mp = (* 's like subst *) mp',resolve | MPbound bid -> let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve - | MPdot (mp1,l) -> - let mp1',resolve = aux mp1 in - MPdot (mp1',l),resolve + mp',resolve + | MPdot (mp1,l) as mp2 -> + begin + try + let mp',resolve = Umap.find (MPI mp2) sub in + mp',resolve + with Not_found -> + let mp1',resolve = aux mp1 in + MPdot (mp1',l),resolve + end | _ -> raise Not_found in - try Some (aux mp) with Not_found -> None + try + Some (aux mp) + with Not_found -> None let subst_mp sub mp = match subst_mp0 sub mp with @@ -223,60 +240,173 @@ let replace_mp_in_con mpfrom mpto kn = exception BothSubstitutionsAreIdentitySubstitutions exception ChangeDomain of resolver -let join (subst1 : substitution) (subst2 : substitution) = +let join (subst1 : substitution) (subst2 : substitution) = let apply_subst (sub : substitution) key (mp,resolve) = - let mp',resolve' = - match subst_mp0 sub mp with - None -> mp, None - | Some (mp',resolve') -> mp',resolve' in - let resolve'' : resolver option = - try - let res = - match resolve with - Some res -> res - | None -> - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) - in - Some - (List.map - (fun (kn,topt) -> - kn, - match topt with - None -> - (match key with - MSI msid -> - let kn' = replace_mp_in_con (MPself msid) mp kn in - apply_opt_resolver resolve' kn' - | MBI mbid -> - let kn' = replace_mp_in_con (MPbound mbid) mp kn in - apply_opt_resolver resolve' kn') - | Some t -> Some (subst_mps sub t)) res) - with - BothSubstitutionsAreIdentitySubstitutions -> None - | ChangeDomain res -> - let rec changeDom = function - | [] -> [] - | (kn,topt)::r -> - let key' = - match key with - MSI msid -> MPself msid - | MBI mbid -> MPbound mbid in - let kn' = replace_mp_in_con mp key' kn in - if kn==kn' then - (*the key does not appear in kn, we remove it - from the resolver that we are building*) - changeDom r - else - (kn',topt)::(changeDom r) - in - Some (changeDom res) - in - mp',resolve'' in + let mp',resolve' = + match subst_mp0 sub mp with + None -> mp, None + | Some (mp',resolve') -> mp',resolve' in + let resolve'' : resolver option = + try + let res = + match resolve with + Some res -> res + | None -> + match resolve' with + None -> raise BothSubstitutionsAreIdentitySubstitutions + | Some res -> raise (ChangeDomain res) + in + Some + (List.map + (fun (kn,topt) -> + kn, + match topt with + None -> + (match key with + MSI msid -> + let kn' = replace_mp_in_con (MPself msid) mp kn in + apply_opt_resolver resolve' kn' + | MBI mbid -> + let kn' = replace_mp_in_con (MPbound mbid) mp kn in + apply_opt_resolver resolve' kn' + | MPI mp1 -> + let kn' = replace_mp_in_con mp1 mp kn in + apply_opt_resolver resolve' kn') + | Some t -> Some (subst_mps sub t)) res) + with + BothSubstitutionsAreIdentitySubstitutions -> None + | ChangeDomain res -> + let rec changeDom = function + | [] -> [] + | (kn,topt)::r -> + let key' = + match key with + MSI msid -> MPself msid + | MBI mbid -> MPbound mbid + | MPI mp1 -> mp1 in + let kn' = replace_mp_in_con mp key' kn in + if kn==kn' then + (*the key does not appear in kn, we remove it + from the resolver that we are building*) + changeDom r + else + (kn',topt)::(changeDom r) + in + Some (changeDom res) + in + mp',resolve'' in let subst = Umap.mapi (apply_subst subst2) subst1 in - Umap.fold Umap.add subst2 subst + (Umap.fold Umap.add subst2 subst) +let subst_key subst1 subst2 = + let replace_in_key key (mp,resolve) sub= + let newkey = + match key with + | MPI mp1 -> + begin + match subst_mp0 subst1 mp1 with + | None -> None + | Some (mp2,_) -> Some (MPI mp2) + end + | _ -> None + in + match newkey with + | None -> Umap.add key (mp,resolve) sub + | Some mpi -> Umap.add mpi (mp,resolve) sub + in + Umap.fold replace_in_key subst2 empty_subst + +let update_subst_alias subst1 subst2 = + let subst_inv key (mp,resolve) sub = + let newmp = + match key with + | MBI msid -> Some (MPbound msid) + | MSI msid -> Some (MPself msid) + | _ -> None + in + match newmp with + | None -> sub + | Some mpi -> match mp with + | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub + | MPself msid -> Umap.add (MSI msid) (mpi,None) sub + | _ -> Umap.add (MPI mp) (mpi,None) sub + in + let subst_mbi = Umap.fold subst_inv subst2 empty_subst in + let alias_subst key (mp,resolve) sub= + let newkey = + match key with + | MPI mp1 -> + begin + match subst_mp0 subst_mbi mp1 with + | None -> None + | Some (mp2,_) -> Some (MPI mp2) + end + | _ -> None + in + match newkey with + | None -> Umap.add key (mp,resolve) sub + | Some mpi -> Umap.add mpi (mp,resolve) sub + in + Umap.fold alias_subst subst1 empty_subst + +let join_alias (subst1 : substitution) (subst2 : substitution) = + let apply_subst (sub : substitution) key (mp,resolve) = + let mp',resolve' = + match subst_mp0 sub mp with + None -> mp, None + | Some (mp',resolve') -> mp',resolve' in + let resolve'' : resolver option = + try + let res = + match resolve with + Some res -> res + | None -> + match resolve' with + None -> raise BothSubstitutionsAreIdentitySubstitutions + | Some res -> raise (ChangeDomain res) + in + Some + (List.map + (fun (kn,topt) -> + kn, + match topt with + None -> + (match key with + MSI msid -> + let kn' = replace_mp_in_con (MPself msid) mp kn in + apply_opt_resolver resolve' kn' + | MBI mbid -> + let kn' = replace_mp_in_con (MPbound mbid) mp kn in + apply_opt_resolver resolve' kn' + | MPI mp1 -> + let kn' = replace_mp_in_con mp1 mp kn in + apply_opt_resolver resolve' kn') + | Some t -> Some (subst_mps sub t)) res) + with + BothSubstitutionsAreIdentitySubstitutions -> None + | ChangeDomain res -> + let rec changeDom = function + | [] -> [] + | (kn,topt)::r -> + let key' = + match key with + MSI msid -> MPself msid + | MBI mbid -> MPbound mbid + | MPI mp1 -> mp1 in + let kn' = replace_mp_in_con mp key' kn in + if kn==kn' then + (*the key does not appear in kn, we remove it + from the resolver that we are building*) + changeDom r + else + (kn',topt)::(changeDom r) + in + Some (changeDom res) + in + mp',resolve'' in + Umap.mapi (apply_subst subst2) subst1 + + let rec occur_in_path uid path = match uid,path with | MSI sid,MPself sid' -> sid = sid' diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 0a3220293..b54ae6f3b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -24,11 +24,15 @@ val add_msid : mod_self_id -> module_path -> substitution -> substitution val add_mbid : mod_bound_id -> module_path -> resolver option -> substitution -> substitution +val add_mp : + module_path -> module_path -> substitution -> substitution val map_msid : mod_self_id -> module_path -> substitution val map_mbid : mod_bound_id -> module_path -> resolver option -> substitution +val map_mp : + module_path -> module_path -> substitution (* sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] @@ -78,3 +82,9 @@ val subst_mps : substitution -> constr -> constr val occur_msid : mod_self_id -> substitution -> bool val occur_mbid : mod_bound_id -> substitution -> bool + +val update_subst_alias : substitution -> substitution -> substitution + +val subst_key : substitution -> substitution -> substitution + +val join_alias : substitution -> substitution -> substitution diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 201835c10..3ae9293c7 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -22,7 +22,7 @@ open Mod_subst exception Not_path let path_of_mexpr = function - | MSEident mb -> mb + | MSEident mp -> mp | _ -> raise Not_path let rec list_split_assoc k rev_before = function @@ -41,10 +41,10 @@ let rec check_with env mtb with_decl = match with_decl with | With_Definition (id,_) -> let cb = check_with_aux_def env mtb with_decl in - SEBwith(mtb,With_definition_body(id,cb)) + SEBwith(mtb,With_definition_body(id,cb)),empty_subst | With_Module (id,mp) -> - let cst = check_with_aux_mod env mtb with_decl in - SEBwith(mtb,With_module_body(id,mp,cst)) + let cst,sub = check_with_aux_mod env mtb with_decl in + SEBwith(mtb,With_module_body(id,mp,cst)),sub and check_with_aux_def env mtb with_decl = let msid,sig_b = match (eval_struct env mtb) with @@ -102,13 +102,13 @@ and check_with_aux_def env mtb with_decl = | _ -> error_not_a_module (string_of_label l) in begin - match old.mod_equiv with + match old.mod_expr with | None -> let new_with_decl = match with_decl with With_Definition (_,c) -> With_Definition (idl,c) | With_Module (_,c) -> With_Module (idl,c) in check_with_aux_def env' (type_of_mb env old) new_with_decl - | Some mp -> + | Some msb -> error_a_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" @@ -117,9 +117,9 @@ and check_with_aux_def env mtb with_decl = | Reduction.NotConvertible -> error_with_incorrect l and check_with_aux_mod env mtb with_decl = - let msid,sig_b = match (eval_struct env mtb) with + let initmsid,msid,sig_b = match (eval_struct env mtb) with | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in - msid',(subst_signature_msid msid (MPself(msid')) sig_b) + msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b) | _ -> error_signature_expected mtb in let id,idl = match with_decl with @@ -130,39 +130,56 @@ and check_with_aux_mod env mtb with_decl = try let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in + let rec mp_rec = function + | [] -> MPself initmsid + | i::r -> MPdot(mp_rec r,label_of_id i) + in let env' = Modops.add_signature (MPself msid) before env in match with_decl with | With_Module ([],_) -> assert false | With_Module ([id], mp) -> - let old = match spec with - SFBmodule msb -> msb + let old,alias = match spec with + SFBmodule msb -> Some msb,None + | SFBalias (mp',cst) -> None,Some (mp',cst) | _ -> error_not_a_module (string_of_label l) in - let mtb' = eval_struct env' (SEBident mp) in + let mtb' = lookup_modtype mp env' in let cst = - try check_subtypes env' mtb' (type_of_mb env old) - with Failure _ -> error_with_incorrect (label_of_id id) in - let _ = - match old.mod_equiv with - | None -> Some mp - | Some mp' -> - check_modpath_equiv env' mp mp'; - Some mp + match old,alias with + Some msb,None -> + begin + try Constraint.union + (check_subtypes env' mtb' (module_type_of_module None msb)) + msb.mod_constraints + with Failure _ -> error_with_incorrect (label_of_id id) + end + | None,Some (mp',None) -> + check_modpath_equiv env' mp mp'; + Constraint.empty + | None,Some (mp',Some cst) -> + check_modpath_equiv env' mp mp'; + cst + | _,_ -> + anomaly "Mod_typing:no implementation and no alias" in - cst - | With_Module (_::_,_) -> + cst,join (map_mp (mp_rec [id]) mp) mtb'.typ_alias + | With_Module (_::_,mp) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) in begin - match old.mod_equiv with + match old.mod_expr with None -> let new_with_decl = match with_decl with - With_Definition (_,c) -> With_Definition (idl,c) + With_Definition (_,c) -> + With_Definition (idl,c) | With_Module (_,c) -> With_Module (idl,c) in - check_with_aux_mod env' (type_of_mb env old) new_with_decl - | Some mp -> + let cst,sub = + check_with_aux_mod env' + (type_of_mb env old) new_with_decl in + cst,(join (map_mp (mp_rec idl) mp) sub) + | Some msb -> error_a_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" @@ -175,35 +192,33 @@ and translate_module env me = | None, None -> anomaly "Mod_typing.translate_module: empty type and expr in module entry" | None, Some mte -> - let mtb = translate_struct_entry env mte in + let mtb,sub = translate_struct_entry env mte in { mod_expr = None; mod_type = Some mtb; - mod_equiv = None; + mod_alias = sub; mod_constraints = Constraint.empty; mod_retroknowledge = []} | Some mexpr, _ -> - let meq_o = - try (* TODO: transparent field in module_entry *) - match me.mod_entry_type with - | None -> Some (path_of_mexpr mexpr) - | Some _ -> None - with - | Not_path -> None - in - let meb = translate_struct_entry env mexpr in - let mod_typ, cst = + let meb,sub1 = translate_struct_entry env mexpr in + let mod_typ,sub,cst = match me.mod_entry_type with - | None -> None, Constraint.empty + | None -> None,sub1,Constraint.empty | Some mte -> - let mtb1 = translate_struct_entry env mte in - let cst = check_subtypes env (eval_struct env meb) - mtb1 in - Some mtb1, cst + let mtb2,sub2 = translate_struct_entry env mte in + let cst = check_subtypes env + {typ_expr = meb; + typ_strength = None; + typ_alias = sub1;} + {typ_expr = mtb2; + typ_strength = None; + typ_alias = sub2;} + in + Some mtb2,sub2,cst in { mod_type = mod_typ; mod_expr = Some meb; - mod_equiv = meq_o; mod_constraints = cst; + mod_alias = sub; 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 @@ -211,31 +226,39 @@ and translate_module env me = and translate_struct_entry env mse = match mse with - | MSEident mp -> - SEBident mp + | MSEident mp -> + let mtb = lookup_modtype mp env in + SEBident mp,mtb.typ_alias | MSEfunctor (arg_id, arg_e, body_expr) -> - let arg_b = translate_struct_entry env arg_e in - let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in - let body_b = translate_struct_entry env' body_expr in - SEBfunctor (arg_id, arg_b, body_b) + let arg_b,sub = translate_struct_entry env arg_e in + let mtb = + {typ_expr = arg_b; + typ_strength = None; + typ_alias = sub} in + let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in + let body_b,sub = translate_struct_entry env' body_expr in + SEBfunctor (arg_id, mtb, body_b),sub | MSEapply (fexpr,mexpr) -> - let feb = translate_struct_entry env fexpr in + let feb,sub1 = translate_struct_entry env fexpr in let feb'= eval_struct env feb in let farg_id, farg_b, fbody_b = destr_functor env feb' in - let _ = + let mtb = try - path_of_mexpr mexpr + lookup_modtype (path_of_mexpr mexpr) env with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) in - let meb= translate_struct_entry env mexpr in - let cst = check_subtypes env (eval_struct env meb) farg_b in - SEBapply(feb,meb,cst) + let meb,sub2= translate_struct_entry env mexpr in + let sub = join sub1 sub2 in + let sub = join_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in + let sub = update_subst_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in + let cst = check_subtypes env mtb farg_b in + SEBapply(feb,meb,cst),sub | MSEwith(mte, with_decl) -> - let mtb = translate_struct_entry env mte in - let mtb' = check_with env mtb with_decl in - mtb' + let mtb,sub1 = translate_struct_entry env mte in + let mtb',sub2 = check_with env mtb with_decl in + mtb',join sub1 sub2 let rec add_struct_expr_constraints env = function @@ -267,6 +290,8 @@ 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 = @@ -277,10 +302,10 @@ and add_module_constraints env mb = let env = match mb.mod_type with | None -> env | Some mtb -> - add_modtype_constraints env mtb + add_struct_expr_constraints env mtb in Environ.add_constraints mb.mod_constraints env and add_modtype_constraints env mtb = - add_struct_expr_constraints env mtb + add_struct_expr_constraints env mtb.typ_expr diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 124cb89c4..e3045555f 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -12,16 +12,18 @@ open Declarations open Environ open Entries +open Mod_subst (*i*) val translate_module : env -> module_entry -> module_body -val translate_struct_entry : env -> module_struct_entry -> struct_expr_body +val translate_struct_entry : env -> module_struct_entry -> + struct_expr_body * substitution -val add_modtype_constraints : env -> struct_expr_body -> env +val add_modtype_constraints : env -> module_type_body -> env val add_module_constraints : env -> module_body -> env - +val add_struct_expr_constraints : env -> struct_expr_body -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index c5b8e15b5..dc339af52 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -93,7 +93,7 @@ let rec list_split_assoc k rev_before = function | h::tail -> list_split_assoc k (h::rev_before) tail let path_of_seb = function - | SEBident mb -> mb + | SEBident mp -> mp | _ -> anomaly "Modops: evaluation failed." @@ -106,24 +106,32 @@ let destr_functor env mtb = (* the constraints are not important here *) let module_body_of_type mtb = - { mod_type = Some mtb; - mod_equiv = None; + { mod_type = Some mtb.typ_expr; mod_expr = None; mod_constraints = Constraint.empty; + mod_alias = mtb.typ_alias; mod_retroknowledge = []} +let module_type_of_module mp mb = + {typ_expr = + (match mb.mod_type with + | Some expr -> expr + | None -> (match mb.mod_expr with + | Some expr -> expr + | None -> + anomaly "Modops: empty expr and type")); + typ_alias = mb.mod_alias; + typ_strength = mp + } let rec check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else - let mb1 = lookup_module mp1 env in - match mb1.mod_equiv with - | None -> - let mb2 = lookup_module mp2 env in - (match mb2.mod_equiv with - | None -> error_not_equal mp1 mp2 - | Some mp2' -> check_modpath_equiv env mp2' mp1) - | Some mp1' -> check_modpath_equiv env mp2 mp1' - + let mp1 = scrape_alias mp1 env in + let mp2 = scrape_alias mp2 env in + if mp1=mp2 then () + else + error_not_equal mp1 mp2 + let subst_with_body sub = function | With_module_body(id,mp,cst) -> With_module_body(id,subst_mp sub mp,cst) @@ -131,8 +139,13 @@ let subst_with_body sub = function With_definition_body( id,subst_const_body sub cb) let rec subst_modtype sub mtb = - subst_struct_expr sub mtb - + let typ_expr' = subst_struct_expr sub mtb.typ_expr in + if typ_expr'==mtb.typ_expr then + mtb + else + { mtb with + typ_expr = typ_expr'} + and subst_structure sub sign = let subst_body = function SFBconst cb -> @@ -143,23 +156,26 @@ and subst_structure sub sign = SFBmodule (subst_module sub mb) | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb) + | SFBalias (mp,cst) -> + SFBalias (subst_mp sub mp,cst) in List.map (fun (l,b) -> (l,subst_body b)) sign and subst_module sub mb = - let mtb' = Option.smartmap (subst_modtype sub) mb.mod_type in + let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in (* This is similar to the previous case. In this case we have a module M in a signature that is knows to be equivalent to a module M' (because the signature is "K with Module M := M'") and we are substituting M' with some M''. *) let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in - let mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in - if mtb'==mb.mod_type && mpo'==mb.mod_equiv && mb.mod_expr == me' + let mb_alias = join_alias mb.mod_alias sub in + if mtb'==mb.mod_type && mb.mod_expr == me' + && mb_alias == mb.mod_alias then mb else { mod_expr = me'; mod_type=mtb'; - mod_equiv=mpo'; mod_constraints=mb.mod_constraints; + mod_alias = mb_alias; mod_retroknowledge=mb.mod_retroknowledge} @@ -230,7 +246,8 @@ let strengthen_mind env mp l mib = match mib.mind_equiv with let rec eval_struct env = function | SEBident mp -> begin - match (lookup_modtype mp env) with + let mtb =lookup_modtype mp env in + match mtb.typ_expr,mtb.typ_strength with mtb,None -> eval_struct env mtb | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb) end @@ -238,10 +255,26 @@ let rec eval_struct env = function let svb1 = eval_struct env seb1 in let farg_id, farg_b, fbody_b = destr_functor env svb1 in let mp = path_of_seb seb2 in - let resolve = resolver_of_environment farg_id farg_b mp env in - eval_struct env (subst_modtype - (map_mbid farg_id mp (Some resolve)) fbody_b) - | SEBwith (mtb,wdb) -> merge_with env mtb wdb + let mp = scrape_alias mp env in + let sub_alias = (lookup_modtype mp env).typ_alias in + let sub_alias = match eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias + | _ -> sub_alias in + let sub_alias = update_subst_alias sub_alias + (map_mbid farg_id mp (None)) in + let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + eval_struct env (subst_struct_expr + (join sub_alias + (map_mbid farg_id mp (Some resolve))) fbody_b) + | SEBwith (mtb,(With_definition_body _ as wdb)) -> + merge_with env mtb wdb empty_subst + | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) -> + let alias_in_mp = + (lookup_modtype mp env).typ_alias in + merge_with env mtb wdb alias_in_mp +(* | SEBfunctor(mbid,mtb,body) -> + let env = add_module (MPbound mbid) (module_body_of_type mtb) env in + SEBfunctor(mbid,mtb,eval_struct env body) *) | mtb -> mtb and type_of_mb env mb = @@ -251,7 +284,7 @@ and type_of_mb env mb = | _,_ -> anomaly "Modops: empty type and empty expr" -and merge_with env mtb with_decl = +and merge_with env mtb with_decl alias= let msid,sig_b = match (eval_struct env mtb) with | SEBstruct(msid,sig_b) -> msid,sig_b | _ -> error_signature_expected mtb @@ -264,50 +297,50 @@ and merge_with env mtb with_decl = try let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in - let new_spec = match with_decl with + let rec mp_rec = function + | [] -> MPself msid + | i::r -> MPdot(mp_rec r,label_of_id i) + in + let new_spec,subst = match with_decl with | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false | With_definition_body ([id],c) -> - SFBconst c + SFBconst c,None | With_module_body ([id], mp,cst) -> - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module (string_of_label l) - in - let mtb' = eval_struct env (SEBident mp) in - let msb = - {mod_expr = Some (SEBident mp); - mod_type = Some mtb'; - mod_equiv = Some mp; - mod_constraints = cst; - mod_retroknowledge = old.mod_retroknowledge } - in - (SFBmodule msb) + let mp' = scrape_alias mp env in + SFBalias (mp,Some cst), + Some(join (map_mp (mp_rec [id]) mp') alias) | With_definition_body (_::_,_) | With_module_body (_::_,_,_) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) in - let new_with_decl = match with_decl with - With_definition_body (_,c) -> With_definition_body (idl,c) - | With_module_body (_,c,cst) -> With_module_body (idl,c,cst) in + let new_with_decl,subst1 = + match with_decl with + With_definition_body (_,c) -> With_definition_body (idl,c),None + | With_module_body (idc,mp,cst) -> + With_module_body (idl,mp,cst), + Some(map_mp (mp_rec idc) mp) + in + let subst = Option.fold_right join subst1 alias in let modtype = - merge_with env (type_of_mb env old) new_with_decl in - let msb = - { mod_expr = None; - mod_type = Some modtype; - mod_equiv = None; - mod_constraints = old.mod_constraints; - mod_retroknowledge = old.mod_retroknowledge} - in - (SFBmodule msb) + merge_with env (type_of_mb env old) new_with_decl alias in + let msb = + { mod_expr = None; + mod_type = Some modtype; + mod_constraints = old.mod_constraints; + mod_alias = subst; + mod_retroknowledge = old.mod_retroknowledge} + in + (SFBmodule msb),Some subst in - SEBstruct(msid, before@(l,new_spec)::after) + SEBstruct(msid, before@(l,new_spec):: + (Option.fold_right subst_structure subst after)) with Not_found -> error_no_such_label l -and add_signature mp sign env = +and add_signature mp sign env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in let con = make_con mp empty_dirpath l in @@ -316,20 +349,19 @@ and add_signature mp sign env = | SFBmind mib -> Environ.add_mind kn mib env | SFBmodule mb -> add_module (MPdot (mp,l)) mb env - (* adds components as well *) + (* adds components as well *) + | SFBalias (mp1,cst) -> + Environ.register_alias (MPdot(mp,l)) mp1 env | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) - (mtb,None) env + mtb env in List.fold_left add_one env sign and add_module mp mb env = let env = Environ.shallow_add_module mp mb env in - let env = match mb.mod_type,mb.mod_expr with - | Some mt, _ -> - Environ.add_modtype mp (mt,Some mp) env - | None, Some me -> - Environ.add_modtype mp (me,Some mp) env - | _,_ -> anomaly "Modops:Empty expr and type" in + let env = + Environ.add_modtype mp (module_type_of_module (Some mp) mb) env + in let mod_typ = type_of_mb env mb in match mod_typ with | SEBstruct (msid,sign) -> @@ -346,9 +378,13 @@ and constants_of_specification env mp sign = | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res | SFBmind _ -> env,res | SFBmodule mb -> - let new_env = add_module (MPdot (mp,l)) mb env in + let new_env = add_module (MPdot (mp,l)) mb env in new_env,(constants_of_modtype env (MPdot (mp,l)) (type_of_mb env mb)) @ res + | SFBalias (mp1,cst) -> + let new_env = register_alias (MPdot (mp,l)) mp1 env in + new_env,(constants_of_modtype env (MPdot (mp,l)) + (eval_struct env (SEBident mp1))) @ res | SFBmodtype mtb -> (* module type dans un module type. Il faut au moins mettre mtb dans l'environnement (avec le bon @@ -365,27 +401,29 @@ and constants_of_specification env mp sign = si on ne rajoute pas T2 dans l'environement de typage on va exploser au moment du Declare Module *) - let new_env = Environ.add_modtype (MPdot(mp,l)) (mtb,None) env in - new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res + let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in + new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res in snd (List.fold_left aux (env,[]) sign) and constants_of_modtype env mp modtype = - match (eval_struct env modtype) with - SEBstruct (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | SEBfunctor _ -> [] - | _ -> anomaly "Modops:the evaluation of the structure failed " + match (eval_struct env modtype) with + SEBstruct (msid,sign) -> + constants_of_specification env mp + (subst_signature_msid msid mp sign) + | SEBfunctor _ -> [] + | _ -> anomaly "Modops:the evaluation of the structure failed " (* returns a resolver for kn that maps mbid to mp. We only keep constants that have the inline flag *) -and resolver_of_environment mbid modtype mp env = - let constants = constants_of_modtype env (MPbound mbid) modtype in +and resolver_of_environment mbid modtype mp alias env = + let constants = constants_of_modtype env (MPbound mbid) modtype.typ_expr in + let constants = List.map (fun (l,cb) -> (l,subst_const_body alias cb)) constants in let rec make_resolve = function | [] -> [] | (con,expecteddef)::r -> - let con' = replace_mp_in_con (MPbound mbid) mp con in + let con',_ = subst_con alias con in + let con' = replace_mp_in_con (MPbound mbid) mp con' in try if expecteddef.Declarations.const_inline then let constant = lookup_constant con' env in @@ -413,11 +451,8 @@ and strengthen_mod env mp mb = let mod_typ = type_of_mb env mb in { mod_expr = mb.mod_expr; mod_type = Some (strengthen_mtb env mp mod_typ); - mod_equiv = begin match mb.mod_equiv with - | Some _ -> mb.mod_equiv - | None -> Some mp - end ; mod_constraints = mb.mod_constraints; + mod_alias = mb.mod_alias; mod_retroknowledge = mb.mod_retroknowledge} and strengthen_sig env msid sign mp = match sign with @@ -432,18 +467,19 @@ and strengthen_sig env msid sign mp = match sign with item'::rest' | (l,SFBmodule mb) :: rest -> let mp' = MPdot (mp,l) in - let item' = l,SFBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) - mb - env - in + let item' = l,SFBmodule (strengthen_mod env mp' mb) in + let env' = add_module + (MPdot (MPself msid,l)) mb env in + let rest' = strengthen_sig env' msid rest mp in + item':: rest' + | ((l,SFBalias (mp1,cst)) as item) :: rest -> + let env' = register_alias (MPdot(MPself msid,l)) mp1 env in let rest' = strengthen_sig env' msid rest mp in - item'::rest' + item::rest' | (l,SFBmodtype mty as item) :: rest -> let env' = add_modtype (MPdot((MPself msid),l)) - (mty,None) + mty env in let rest' = strengthen_sig env' msid rest mp in @@ -451,5 +487,11 @@ and strengthen_sig env msid sign mp = match sign with let strengthen env mtb mp = strengthen_mtb env mp mtb - + +let update_subst env mb mp = + match type_of_mb env mb with + | SEBstruct(msid,str) -> false, join_alias + (subst_key (map_msid msid mp) mb.mod_alias) + (map_msid msid mp) + | _ -> true, mb.mod_alias diff --git a/kernel/modops.mli b/kernel/modops.mli index a35e887ea..11f0ddd17 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -21,19 +21,25 @@ open Mod_subst (* Various operations on modules and module types *) (* make the environment entry out of type *) -val module_body_of_type : struct_expr_body -> module_body +val module_body_of_type : module_type_body -> module_body +val module_type_of_module : module_path option -> module_body -> + module_type_body val destr_functor : - env -> struct_expr_body -> mod_bound_id * struct_expr_body * struct_expr_body + env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body -val subst_modtype : substitution -> struct_expr_body -> struct_expr_body +val subst_modtype : substitution -> module_type_body -> module_type_body val subst_structure : substitution -> structure_body -> structure_body +val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body + val subst_signature_msid : mod_self_id -> module_path -> structure_body -> structure_body +val subst_structure : substitution -> structure_body -> structure_body + (* Evaluation functions *) val eval_struct : env -> struct_expr_body -> struct_expr_body @@ -53,6 +59,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body +val update_subst : env -> module_body -> module_path -> bool * substitution + val error_existing_label : label -> 'a val error_declaration_not_path : module_struct_entry -> 'a @@ -62,7 +70,7 @@ val error_application_to_not_path : module_struct_entry -> 'a val error_not_a_functor : module_struct_entry -> 'a val error_incompatible_modtypes : - struct_expr_body -> struct_expr_body -> 'a + module_type_body -> module_type_body -> 'a val error_not_equal : module_path -> module_path -> 'a @@ -97,4 +105,6 @@ val error_local_context : label option -> 'a val error_no_such_label_sub : label->string->string->'a val resolver_of_environment : - mod_bound_id -> struct_expr_body -> module_path -> env -> resolver + mod_bound_id -> module_type_body -> module_path -> substitution + -> env -> resolver + diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 2b41e5a36..8d45bb9e3 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -26,7 +26,8 @@ type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t } + env_modtypes : module_type_body MPmap.t; + env_alias : module_path MPmap.t } type stratification = { env_universes : universes; @@ -60,7 +61,8 @@ let empty_env = { env_constants = Cmap.empty; env_inductives = KNmap.empty; env_modules = MPmap.empty; - env_modtypes = MPmap.empty }; + env_modtypes = MPmap.empty; + env_alias = MPmap.empty }; env_named_context = empty_named_context; env_named_vals = []; env_rel_context = empty_rel_context; diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index b6d83b918..518c6330d 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -26,7 +26,8 @@ type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t } + env_modtypes : module_type_body MPmap.t; + env_alias : module_path MPmap.t } type stratification = { env_universes : universes; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 28e6fb8c7..b1eea3bbd 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -25,11 +25,12 @@ open Term_typing open Modops open Subtyping open Mod_typing +open Mod_subst type modvariant = | NONE - | SIG of (* funsig params *) (mod_bound_id * struct_expr_body) list - | STRUCT of (* functor params *) (mod_bound_id * struct_expr_body) list + | SIG of (* funsig params *) (mod_bound_id * module_type_body) list + | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list | LIBRARY of dir_path type module_info = @@ -37,7 +38,8 @@ type module_info = modpath : module_path; seed : dir_path; (* the "seed" of unique identifier generator *) label : label; - variant : modvariant} + variant : modvariant; + alias_subst : substitution} let check_label l labset = if Labset.mem l labset then error_existing_label l @@ -81,7 +83,8 @@ let rec empty_environment = modpath = initial_path; seed = initial_dir; label = mk_label "_"; - variant = NONE}; + variant = NONE; + alias_subst = empty_subst}; labset = Labset.empty; revstruct = []; univ = Univ.Constraint.empty; @@ -253,10 +256,13 @@ let add_mind dir l mie senv = let add_modtype l mte senv = check_label l senv.labset; - let mtb = translate_struct_entry senv.env mte in + let mtb_expr,sub = translate_struct_entry senv.env mte in + let mtb = { typ_expr = mtb_expr; + typ_strength = None; + typ_alias = sub} in let env' = add_modtype_constraints senv.env mtb in let mp = MPdot(senv.modinfo.modpath, l) in - let env'' = Environ.add_modtype mp (mtb,None) env' in + let env'' = Environ.add_modtype mp mtb env' in mp, { old = senv.old; env = env''; modinfo = senv.modinfo; @@ -281,10 +287,16 @@ let add_module l me senv = check_label l senv.labset; let mb = translate_module senv.env me in let mp = MPdot(senv.modinfo.modpath, l) in + let is_functor,sub = Modops.update_subst senv.env mb mp in let env' = full_add_module mp mb senv.env in mp, { old = senv.old; env = env'; - modinfo = senv.modinfo; + modinfo = + if is_functor then + senv.modinfo + else + {senv.modinfo with + alias_subst = join senv.modinfo.alias_subst sub}; labset = Labset.add l senv.labset; revstruct = (l,SFBmodule mb)::senv.revstruct; univ = senv.univ; @@ -293,6 +305,26 @@ let add_module l me senv = loads = senv.loads; local_retroknowledge = senv.local_retroknowledge } +let add_alias l mp senv = + check_label l senv.labset; + let mp' = MPdot(senv.modinfo.modpath, l) in + (* we get all alias substitutions that comes from mp *) + let _,sub = translate_struct_entry senv.env (MSEident mp) in + (* we add the new one *) + let sub = join (map_mp mp' mp) sub in + let env' = register_alias mp' mp senv.env in + mp', { old = senv.old; + env = env'; + modinfo = { senv.modinfo with + alias_subst = join + senv.modinfo.alias_subst sub}; + labset = Labset.add l senv.labset; + revstruct = (l,SFBalias (mp,None))::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads; + local_retroknowledge = senv.local_retroknowledge } (* Interactive modules *) @@ -304,7 +336,8 @@ let start_module l senv = modpath = mp; seed = senv.modinfo.seed; label = l; - variant = STRUCT [] } + variant = STRUCT []; + alias_subst = empty_subst} in mp, { old = senv; env = senv.env; @@ -322,10 +355,10 @@ let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in let restype = Option.map (translate_struct_entry senv.env) restype in - let params = + let params,is_functor = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () - | STRUCT params -> params + | STRUCT params -> params, (List.length params > 0) in if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; @@ -339,21 +372,27 @@ let end_module l restype senv = let auto_tb = SEBstruct (modinfo.msid, List.rev senv.revstruct) in - let mod_typ, cst = + let mod_typ,subst,cst = match restype with - | None -> None, Constraint.empty - | Some res_tb -> - let cst = check_subtypes senv.env auto_tb res_tb in + | None -> None,modinfo.alias_subst,Constraint.empty + | Some (res_tb,subst) -> + let cst = check_subtypes senv.env + {typ_expr = auto_tb; + typ_strength = None; + typ_alias = modinfo.alias_subst} + {typ_expr = res_tb; + typ_strength = None; + typ_alias = subst} in let mtb = functorize_struct res_tb in - Some mtb, cst + Some mtb,subst,cst in let mexpr = functorize_struct auto_tb in let cst = Constraint.union cst senv.univ in let mb = { mod_expr = Some mexpr; mod_type = mod_typ; - mod_equiv = None; mod_constraints = cst; + mod_alias = subst; mod_retroknowledge = senv.local_retroknowledge } in let mp = MPdot (oldsenv.modinfo.modpath, l) in @@ -368,9 +407,19 @@ let end_module l restype senv = let newenv = full_add_module mp mb newenv in - mp, { old = oldsenv.old; + let is_functor,subst = Modops.update_subst newenv mb mp in + let newmodinfo = + if is_functor then + oldsenv.modinfo + else + { oldsenv.modinfo with + alias_subst = join + oldsenv.modinfo.alias_subst + subst }; + in + mp, { old = oldsenv.old; env = newenv; - modinfo = oldsenv.modinfo; + modinfo = newmodinfo; labset = Labset.add l oldsenv.labset; revstruct = (l,SFBmodule mb)::oldsenv.revstruct; univ = oldsenv.univ; @@ -383,8 +432,8 @@ let end_module l restype senv = (* Include for module and module type*) let add_include me senv = - let struct_expr = translate_struct_entry senv.env me in - let senv = { senv with env = add_modtype_constraints senv.env struct_expr } in + let struct_expr,_ = translate_struct_entry senv.env me in + let senv = { senv with env = add_struct_expr_constraints senv.env struct_expr } in let msid,str = match (eval_struct senv.env struct_expr) with | SEBstruct(msid,str_l) -> msid,str_l | _ -> error ("You cannot Include a higher-order Module or Module Type" ) @@ -426,21 +475,42 @@ let end_module l restype senv = | SFBmodule mb -> let mp = MPdot(senv.modinfo.modpath, l) in + let is_functor,sub = Modops.update_subst senv.env mb mp in let env' = full_add_module mp mb senv.env in { old = senv.old; env = env'; - modinfo = senv.modinfo; + modinfo = + if is_functor then + senv.modinfo + else + {senv.modinfo with + alias_subst = join senv.modinfo.alias_subst sub}; labset = Labset.add l senv.labset; revstruct = (l,SFBmodule mb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads; + local_retroknowledge = senv.local_retroknowledge } + | SFBalias (mp',cst) -> + let env' = Option.fold_right + Environ.add_constraints cst senv.env in + let mp = MPdot(senv.modinfo.modpath, l) in + let env' = register_alias mp mp' env' in + { old = senv.old; + env = env'; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revstruct = (l,SFBalias (mp,cst))::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; loads = senv.loads; - local_retroknowledge = senv.local_retroknowledge } + local_retroknowledge = senv.local_retroknowledge } | SFBmodtype mtb -> let env' = add_modtype_constraints senv.env mtb in let mp = MPdot(senv.modinfo.modpath, l) in - let env'' = Environ.add_modtype mp (mtb,None) env' in + let env'' = Environ.add_modtype mp mtb env' in { old = senv.old; env = env''; modinfo = senv.modinfo; @@ -459,7 +529,10 @@ let end_module l restype senv = let add_module_parameter mbid mte senv = if senv.revstruct <> [] or senv.loads <> [] then anomaly "Cannot add a module parameter to a non empty module"; - let mtb = translate_struct_entry senv.env mte in + let mtb_expr,sub = translate_struct_entry senv.env mte in + let mtb = {typ_expr = mtb_expr; + typ_strength = None; + typ_alias = sub} in let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env in let new_variant = match senv.modinfo.variant with @@ -490,7 +563,8 @@ let start_modtype l senv = modpath = mp; seed = senv.modinfo.seed; label = l; - variant = SIG [] } + variant = SIG []; + alias_subst = empty_subst } in mp, { old = senv; env = senv.env; @@ -517,7 +591,7 @@ let end_modtype l senv = let auto_tb = SEBstruct (modinfo.msid, List.rev senv.revstruct) in - let mtb = + let mtb_expr = List.fold_left (fun mtb (arg_id,arg_b) -> SEBfunctor(arg_id,arg_b,mtb)) @@ -536,11 +610,15 @@ let end_modtype l senv = newenv (List.rev senv.loads) in + let subst = senv.modinfo.alias_subst in + let mtb = {typ_expr = mtb_expr; + typ_strength = None; + typ_alias = subst} in let newenv = - add_modtype_constraints newenv mtb + add_modtype_constraints newenv mtb in let newenv = - Environ.add_modtype mp (mtb,None) newenv + Environ.add_modtype mp mtb newenv in mp, { old = oldsenv.old; env = newenv; @@ -607,7 +685,8 @@ let start_library dir senv = modpath = mp; seed = dir; label = l; - variant = LIBRARY dir } + variant = LIBRARY dir; + alias_subst = empty_subst } in mp, { old = senv; env = senv.env; @@ -637,8 +716,8 @@ let export senv dir = let mb = { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct)); mod_type = None; - mod_equiv = None; mod_constraints = senv.univ; + mod_alias = senv.modinfo.alias_subst; mod_retroknowledge = senv.local_retroknowledge} in modinfo.msid, (dir,mb,senv.imports,engagement senv.env) @@ -692,15 +771,20 @@ let import (dp,mb,depends,engmt) digest senv = and lighten_struct struc = let lighten_body (l,body) = (l,match body with | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _) as x -> x + | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x | SFBmodule m -> SFBmodule (lighten_module m) - | SFBmodtype m -> SFBmodtype (lighten_modexpr m)) + | SFBmodtype m -> SFBmodtype + ({m with + typ_expr = lighten_modexpr m.typ_expr})) in List.map lighten_body struc and lighten_modexpr = function | SEBfunctor (mbid,mty,mexpr) -> - SEBfunctor (mbid,lighten_modexpr mty,lighten_modexpr mexpr) + SEBfunctor (mbid, + ({mty with + typ_expr = lighten_modexpr mty.typ_expr}), + lighten_modexpr mexpr) | SEBident mp as x -> x | SEBstruct (msid, struc) -> SEBstruct (msid, lighten_struct struc) @@ -708,7 +792,7 @@ and lighten_modexpr = function SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) | SEBwith (seb,wdcl) -> SEBwith (lighten_modexpr seb,wdcl) - + let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index e764312b5..07f82876f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,6 +57,10 @@ val add_module : label -> module_entry -> safe_environment -> module_path * safe_environment +(* Adding a module alias*) +val add_alias : + label -> module_path -> safe_environment + -> module_path * safe_environment (* Adding a module type *) val add_modtype : label -> module_struct_entry -> safe_environment diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 3db187a0b..e4b1f7045 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -32,7 +32,8 @@ type namedobject = | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body | Module of module_body - | Modtype of struct_expr_body + | Modtype of module_type_body + | Alias of module_path (* adds above information about one mutual inductive: all types and constructors *) @@ -63,6 +64,7 @@ let make_label_map mp list = add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) + | SFBalias (mp,cst) -> add_map (Alias mp) in List.fold_right add_one list Labmap.empty @@ -289,43 +291,59 @@ let check_constant cst env msid1 l info1 cb2 spec2 = let rec check_modules cst env msid1 l msb1 msb2 = let mp = (MPdot(MPself msid1,l)) in - let mty1 = strengthen env (type_of_mb env msb1) mp in - let cst = check_modtypes cst env mty1 (type_of_mb env msb2) false in - begin - match msb1.mod_equiv, msb2.mod_equiv with - | _, None -> () - | None, Some mp2 -> - check_modpath_equiv env mp mp2 - | Some mp1, Some mp2 -> - check_modpath_equiv env mp1 mp2 - end; - cst + let mty1 = module_type_of_module (Some mp) msb1 in + let mty2 = module_type_of_module None msb2 in + let cst = check_modtypes cst env mty1 mty2 false in + cst -and check_signatures cst env (msid1,sig1) (msid2,sig2') = +and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = let mp1 = MPself msid1 in let env = add_signature mp1 sig1 env in - let sig2 = subst_signature_msid msid2 mp1 sig2' in + let alias = update_subst_alias alias (map_msid msid2 mp1) in + let sig2 = subst_structure alias sig2' in + let sig2 = subst_signature_msid msid2 mp1 sig2 in let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = try Labmap.find l map1 with - Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2) + Not_found -> error_no_such_label_sub l + (string_of_msid msid1) (string_of_msid msid2) in match spec2 with | SFBconst cb2 -> check_constant cst env msid1 l info1 cb2 spec2 | SFBmind mib2 -> check_inductive cst env msid1 l info1 mib2 spec2 - | SFBmodule msb2 -> - let msb1 = + | SFBmodule msb2 -> + begin match info1 with - | Module msb -> msb + | Module msb -> check_modules cst env msid1 l msb msb2 + | Alias mp ->let msb = + {mod_expr = Some (SEBident mp); + mod_type = Some (eval_struct env (SEBident mp)); + mod_constraints = Constraint.empty; + mod_alias = (lookup_modtype mp env).typ_alias; + mod_retroknowledge = []} in + check_modules cst env msid1 l msb msb2 | _ -> error_not_match l spec2 - in - check_modules cst env msid1 l msb1 msb2 + end + | SFBalias (mp,_) -> + begin + match info1 with + | Alias mp1 -> check_modpath_equiv env mp mp1; cst + | Module msb -> + let msb1 = + {mod_expr = Some (SEBident mp); + mod_type = Some (eval_struct env (SEBident mp)); + mod_constraints = Constraint.empty; + mod_alias = (lookup_modtype mp env).typ_alias; + mod_retroknowledge = []} in + check_modules cst env msid1 l msb msb1 + | _ -> error_not_match l spec2 + end | SFBmodtype mtb2 -> let mtb1 = match info1 with @@ -336,35 +354,46 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') = in List.fold_left check_one_body cst sig2 + and check_modtypes cst env mtb1 mtb2 equiv = if mtb1==mtb2 then cst else (* just in case :) *) - let mtb1' = eval_struct env mtb1 in - let mtb2' = eval_struct env mtb2 in - if mtb1'==mtb2' then cst else - match mtb1', mtb2' with - | SEBstruct (msid1,list1), - SEBstruct (msid2,list2) -> - let cst = check_signatures cst env (msid1,list1) (msid2,list2) in - if equiv then - check_signatures cst env (msid2,list2) (msid1,list1) - else - cst - | SEBfunctor (arg_id1,arg_t1,body_t1), - SEBfunctor (arg_id2,arg_t2,body_t2) -> - let cst = check_modtypes cst env arg_t2 arg_t1 equiv in - (* contravariant *) - let env = - add_module (MPbound arg_id2) (module_body_of_type arg_t2) env - in - let body_t1' = - (* since we are just checking well-typedness we do not need - to expand any constant. Hence the identity resolver. *) - subst_modtype - (map_mbid arg_id1 (MPbound arg_id2) None) - body_t1 - in - check_modtypes cst env body_t1' body_t2 equiv - | _ , _ -> error_incompatible_modtypes mtb1 mtb2 + let mtb1',mtb2'= + (match mtb1.typ_strength with + None -> eval_struct env mtb1.typ_expr, + eval_struct env mtb2.typ_expr + | Some mp -> strengthen env mtb1.typ_expr mp, + eval_struct env mtb2.typ_expr) in + let rec check_structure cst env str1 str2 equiv = + match str1, str2 with + | SEBstruct (msid1,list1), + SEBstruct (msid2,list2) -> + let cst = check_signatures cst env + (msid1,list1) mtb1.typ_alias (msid2,list2) in + if equiv then + check_signatures cst env + (msid2,list2) mtb2.typ_alias (msid1,list1) + else + cst + | SEBfunctor (arg_id1,arg_t1,body_t1), + SEBfunctor (arg_id2,arg_t2,body_t2) -> + let cst = check_modtypes cst env arg_t2 arg_t1 equiv in + (* contravariant *) + let env = + add_module (MPbound arg_id2) (module_body_of_type arg_t2) env + in + let body_t1' = + (* since we are just checking well-typedness we do not need + to expand any constant. Hence the identity resolver. *) + subst_struct_expr + (map_mbid arg_id1 (MPbound arg_id2) None) + body_t1 + in + check_structure cst env (eval_struct env body_t1') + (eval_struct env body_t2) equiv + | _ , _ -> error_incompatible_modtypes mtb1 mtb2 + in + if mtb1'== mtb2' then cst + else check_structure cst env mtb1' mtb2' equiv let check_subtypes env sup super = check_modtypes Constraint.empty env sup super false diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index d7288fc06..c0b1ee5d3 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -14,6 +14,6 @@ open Declarations open Environ (*i*) -val check_subtypes : env -> struct_expr_body -> struct_expr_body -> constraints +val check_subtypes : env -> module_type_body -> module_type_body -> constraints diff --git a/library/declaremods.ml b/library/declaremods.ml index dffdb9e6f..6074bac9c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -122,19 +122,19 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) -let rec scrape_alias mp = - match (Environ.lookup_module mp - (Global.env())) with - | {mod_expr = Some (SEBident mp1); - mod_type = None} -> scrape_alias mp1 - | _ -> mp +let scrape_alias mp = + Environ.scrape_alias mp (Global.env()) (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) let check_subtypes mp sub_mtb = let env = Global.env () in - let mtb = Modops.eval_struct env (SEBident mp) in + let mtb = Environ.lookup_modtype mp env in + let sub_mtb = + {typ_expr = sub_mtb; + typ_strength = None; + typ_alias = empty_subst} in let _ = Environ.add_constraints (Subtyping.check_subtypes env mtb sub_mtb) in @@ -221,15 +221,15 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = | Some mte -> Some (Mod_typing.translate_struct_entry (Global.env()) mte) in - + let mp = Global.add_module (basename sp) me in - if mp <> mp_of_kn kn then - anomaly "Kernel and Library names do not match"; + if mp <> mp_of_kn kn then + anomaly "Kernel and Library names do not match"; - match sub_mtb_o with - None -> () - | Some sub_mtb -> - check_subtypes mp sub_mtb + match sub_mtb_o with + None -> () + | Some (sub_mtb,sub) -> + check_subtypes mp sub_mtb in conv_names_do_module false "cache" load_objects 1 oname substobjs substituted @@ -246,13 +246,18 @@ let cache_module_alias ((sp,kn),(entry,substobjs,substituted)) = (Global.env()) mte) in - let mp' = Global.add_module (basename sp) me in + let mp' = match me with + | {mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + Global.add_alias (basename sp) mp + | _ -> anomaly "cache module alias" + in if mp' <> mp_of_kn kn then anomaly "Kernel and Library names do not match"; let _ = match sub_mtb_o with None -> () - | Some sub_mtb -> + | Some (sub_mtb,sub) -> check_subtypes mp' sub_mtb in match me with | {mod_entry_type = None; @@ -278,6 +283,13 @@ let load_module i (oname,(entry,substobjs,substituted)) = check_empty "load_module" entry; conv_names_do_module false "load" load_objects i oname substobjs substituted +let subst_substobjs dir mp (subst,mbids,msid,objs) = + match mbids with + | [] -> + let prefix = dir,(mp,empty_dirpath) in + Some (subst_objects prefix (join (map_msid msid mp) subst) objs) + | _ -> None + let load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = let dir,mp,alias= match entry with @@ -287,9 +299,9 @@ let load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = |{mod_entry_type = None; mod_entry_expr = Some (MSEident mp)} -> dir_of_sp sp,mp_of_kn kn,scrape_alias mp - | _ -> anomaly "tata" + | _ -> anomaly "Modops: Not an alias" end - | None -> anomaly "toujours" + | None -> anomaly "Modops: Empty info" in do_module_alias false "load" load_objects i dir mp alias substobjs substituted @@ -307,24 +319,19 @@ let open_module_alias i ((sp,kn),(entry,substobjs,substituted)) = |{mod_entry_type = None; mod_entry_expr = Some (MSEident mp)} -> dir_of_sp sp,mp_of_kn kn,scrape_alias mp - | _ -> anomaly "tata" + | _ -> anomaly "Modops: Not an alias" end - | None -> anomaly "toujours" + | None -> anomaly "Modops: Empty info" in do_module_alias true "open" open_objects i dir mp alias substobjs substituted -let subst_substobjs dir mp (subst,mbids,msid,objs) = - match mbids with - | [] -> - let prefix = dir,(mp,empty_dirpath) in - Some (subst_objects prefix (add_msid msid mp subst) objs) - | _ -> None - let subst_module ((sp,kn),subst,(entry,substobjs,_)) = check_empty "subst_module" entry; let dir,mp = dir_of_sp sp, mp_of_kn kn in let (sub,mbids,msid,objs) = substobjs in + let sub' = update_subst_alias subst sub in + let sub = join sub' sub in let subst' = join sub subst in (* substitutive_objects get the new substitution *) let substobjs = (subst',mbids,msid,objs) in @@ -342,21 +349,25 @@ let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = let substobjs = (subst',mbids,msid,objs) in (* if we are not a functor - calculate substitued. We add "msid |-> mp" to the substitution *) - let substituted = subst_substobjs dir mp substobjs in - match entry with - | Some (me,sub)-> + let prefix = dir,(mp,empty_dirpath) in + match entry with + | Some (me,sub)-> begin match me with |{mod_entry_type = None; mod_entry_expr = Some (MSEident mp)} -> + let mp = subst_mp subst' mp in (Some ({mod_entry_type = None; mod_entry_expr = - Some (MSEident (subst_mp subst' mp))},sub), - substobjs,substituted) + Some (MSEident mp)},sub), + substobjs, match mbids with + | [] -> + Some (subst_objects prefix (join (map_msid msid mp) subst) objs) + | _ -> None) - | _ -> anomaly "tata" + | _ -> anomaly "Modops: Not an alias" end - | None -> anomaly "toujours" + | None -> anomaly "Modops: Empty info" let classify_module (_,(_,substobjs,_)) = Substitute (None,substobjs,None) @@ -499,28 +510,32 @@ let (in_modtype,out_modtype) = let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = - if mbids<>[] then + let rec mp_rec = function + | [] -> MPself msid + | i::r -> MPdot(mp_rec r,label_of_id i) + in + if mbids<>[] then error "Unexpected functor objects" - else - let rec replace_idl = function - | _,[] -> [] - | id::idl,(id',obj)::tail when id = id' -> - if object_tag obj = "MODULE" then - (match idl with - [] -> (id, in_module_alias (Some - ({mod_entry_type = None; - mod_entry_expr = Some (MSEident mp)},None) - ,modobjs,None))::tail - | _ -> - let (_,substobjs,_) = out_module obj in - let substobjs' = replace_module_object idl substobjs modobjs mp in - (id, in_module (None,substobjs',None))::tail - ) - else error "MODULE expected!" - | idl,lobj::tail -> lobj::replace_idl (idl,tail) - in - (subst, mbids, msid, replace_idl (idl,lib_stack)) - + else + let rec replace_idl = function + | _,[] -> [] + | id::idl,(id',obj)::tail when id = id' -> + if object_tag obj = "MODULE" then + (match idl with + [] -> (id, in_module_alias (Some + ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)},None) + ,modobjs,None))::tail + | _ -> + let (_,substobjs,_) = out_module obj in + let substobjs' = replace_module_object idl substobjs modobjs mp in + (id, in_module (None,substobjs',None))::tail + ) + else error "MODULE expected!" + | idl,lobj::tail -> lobj::replace_idl (idl,tail) + in + (join (map_mp (mp_rec idl) mp) subst, mbids, msid, replace_idl (idl,lib_stack)) + let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) @@ -535,17 +550,26 @@ let rec get_modtype_substobjs env = function let modobjs = MPmap.find mp !modtab_substobjs in replace_module_object idl substobjs modobjs mp | MSEapply (mexpr, MSEident mp) -> - let ftb = Mod_typing.translate_struct_entry env mexpr in + let ftb,_ = Mod_typing.translate_struct_entry env mexpr in let farg_id, farg_b, fbody_b = Modops.destr_functor env (Modops.eval_struct env ftb) in + let mp = Environ.scrape_alias mp env in + let sub_alias = (Environ.lookup_modtype mp env).typ_alias in + let sub_alias = match Modops.eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias + | _ -> sub_alias in + let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in + let sub_alias = update_subst_alias sub_alias + (map_mbid farg_id mp (None)) in let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in (match mbids with | mbid::mbids -> let resolve = - Modops.resolver_of_environment farg_id farg_b mp env in + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) - (join subst (add_mbid mbid mp (Some resolve) empty_subst), mbids, msid, objs) + (join (join (map_mbid mbid mp (Some resolve)) subst ) sub_alias + , mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -565,19 +589,6 @@ let process_module_bindings argids args = in List.iter2 process_arg argids args -(* Dead code *) -(* -let replace_module mtb id mb = todo "replace module after with"; mtb - -let rec get_some_body mty env = match mty with - MTEident kn -> Environ.lookup_modtype kn env - | MTEfunsig _ -> anomaly "anonymous module types not supported" - | MTEwith (mty,With_Definition _) -> get_some_body mty env - | MTEwith (mty,With_Module (id,mp)) -> - replace_module (get_some_body mty env) id (Environ.lookup_module mp env) -*) -(* Dead code *) - let intern_args interp_modtype (idl,arg) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in @@ -592,6 +603,7 @@ let intern_args interp_modtype (idl,arg) = do_module false "interp" load_objects 1 dir mp substobjs substituted; (mbid,mty)) dirs mbids + let start_module interp_modtype export id args res_o = let fs = Summary.freeze_summaries () in @@ -606,12 +618,16 @@ let start_module interp_modtype export id args res_o = if restricted then Some mte, None else - let mtb = Mod_typing.translate_struct_entry (Global.env()) mte in + let mtb,_ = Mod_typing.translate_struct_entry (Global.env()) mte in let sub_mtb = List.fold_right (fun (arg_id,arg_t) mte -> - let arg_t = Mod_typing.translate_struct_entry (Global.env()) arg_t - in SEBfunctor(arg_id,arg_t,mte)) + let arg_t,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t + in + let arg_t = {typ_expr = arg_t; + typ_strength = None; + typ_alias = sub} in + SEBfunctor(arg_id,arg_t,mte)) arg_entries mtb in None, Some sub_mtb @@ -656,7 +672,7 @@ let end_module id = Not_found -> anomaly "Module objects not found..." in - (* must be called after get_modtype_substobjs, because of possible + (* must be called after get_modtype_substobjs, because of possible dependencies on functor arguments *) Summary.module_unfreeze_summaries fs; @@ -839,17 +855,28 @@ let rec get_module_substobjs env = function let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) | MSEapply (mexpr, MSEident mp) -> - let ftb = Mod_typing.translate_struct_entry env mexpr in + let ftb,_ = Mod_typing.translate_struct_entry env mexpr in let farg_id, farg_b, fbody_b = Modops.destr_functor env (Modops.eval_struct env ftb) in + let mp = Environ.scrape_alias mp env in + let sub_alias = (Environ.lookup_modtype mp env).typ_alias in + let sub_alias = match Modops.eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias + | _ -> sub_alias in + let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in + let sub_alias = update_subst_alias sub_alias + (map_mbid farg_id mp (None)) in let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> - let resolve = - Modops.resolver_of_environment farg_id farg_b mp env in - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - (join subst (add_mbid mbid mp (Some resolve) empty_subst), mbids, msid, objs) + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join (map_mbid mbid mp (Some resolve)) subst) + sub_alias) + , mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -909,8 +936,15 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = match entry with |{mod_entry_type = None; mod_entry_expr = Some (MSEident mp) } -> - let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let substituted = subst_substobjs dir mp substobjs in + let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let (sub,mbids,msid,objs) = substobjs in + let prefix = dir,(mp',empty_dirpath) in + let substituted = + match mbids with + | [] -> + Some (subst_objects prefix + (join sub (join (map_msid msid mp') (map_mp mp' mp))) objs) + | _ -> None in ignore (add_leaf id (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))) @@ -920,11 +954,11 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = ignore (add_leaf id (in_module (Some (entry, mty_sub_o), substobjs, substituted))) - + with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e - + (* Include *) let rec subst_inc_expr subst me = diff --git a/library/global.ml b/library/global.ml index 4de4029b2..4f3a40a8a 100644 --- a/library/global.ml +++ b/library/global.ml @@ -68,6 +68,7 @@ let add_constant = add_thing add_constant let add_mind = add_thing add_mind let add_modtype = add_thing (fun _ -> add_modtype) () let add_module = add_thing (fun _ -> add_module) () +let add_alias = add_thing (fun _ -> add_alias) () let add_constraints c = global_env := add_constraints c !global_env diff --git a/library/global.mli b/library/global.mli index 71617f5a1..f0daef0ac 100644 --- a/library/global.mli +++ b/library/global.mli @@ -51,6 +51,8 @@ val add_mind : val add_module : identifier -> module_entry -> module_path val add_modtype : identifier -> module_struct_entry -> module_path +val add_include : module_struct_entry -> unit +val add_alias : identifier -> module_path -> module_path val add_constraints : constraints -> unit @@ -71,7 +73,7 @@ val add_module_parameter : mod_bound_id -> module_struct_entry -> unit val start_modtype : identifier -> module_path val end_modtype : identifier -> module_path -val add_include : module_struct_entry -> unit + (* Queries *) val lookup_named : variable -> named_declaration diff --git a/library/nametab.ml b/library/nametab.ml index 536c9605a..ac6c61116 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -318,7 +318,10 @@ let push_xref visibility sp xref = the_ccitab := SpTab.push visibility sp xref !the_ccitab; match visibility with | Until _ -> - the_globrevtab := Globrevtab.add xref sp !the_globrevtab + if Globrevtab.mem xref !the_globrevtab then + () + else + the_globrevtab := Globrevtab.add xref sp !the_globrevtab | _ -> () let push_cci visibility sp ref = diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 69c596093..0bdae7c77 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -52,12 +52,11 @@ let rec flatten_app mexpr l = match mexpr with | mexpr -> mexpr::l let rec print_module name locals with_body mb = - let body = match mb.mod_equiv, with_body, mb.mod_expr with - | None, false, _ - | None, true, None -> mt() - | None, true, Some mexpr -> + let body = match with_body, mb.mod_expr with + | false, _ + | true, None -> mt() + | true, Some mexpr -> spc () ++ str ":= " ++ print_modexpr locals mexpr - | Some mp, _, _ -> str " == " ++ print_modpath locals mp in let modtype = match mb.mod_type with None -> str "" @@ -77,7 +76,7 @@ and print_modtype locals mty = ::locals in hov 2 (str "Funsig" ++ spc () ++ str "(" ++ pr_id (id_of_mbid mbid) ++ str " : " ++ - print_modtype locals mtb1 ++ + print_modtype locals mtb1.typ_expr ++ str ")" ++ spc() ++ print_modtype locals' mtb2) | SEBstruct (msid,sign) -> hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End") @@ -103,6 +102,7 @@ and print_sig locals msid sign = | SFBconst {const_opaque=true} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " + | SFBalias (mp,_) -> str "Module" | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign @@ -114,6 +114,7 @@ and print_struct locals msid struc = | SFBconst {const_body=None} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " + | SFBalias (mp,_) -> str "Module" | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc @@ -125,7 +126,7 @@ and print_modexpr locals mexpr = match mexpr with in *) let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ - str ":" ++ print_modtype locals mty ++ + str ":" ++ print_modtype locals mty.typ_expr ++ str "]" ++ spc () ++ print_modexpr locals' mexpr) | SEBstruct (msid, struc) -> hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End") @@ -152,8 +153,7 @@ let print_module with_body mp = print_module name [] with_body (Global.lookup_module mp) ++ fnl () let print_modtype kn = - let mtb = match Global.lookup_modtype kn with - | mtb,_ -> mtb in + let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in str "Module Type " ++ name ++ str " = " ++ - print_modtype [] mtb ++ fnl () + print_modtype [] mtb.typ_expr ++ fnl () |