diff options
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 715 |
1 files changed, 478 insertions, 237 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 0066e7848..3211cc28f 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -31,60 +31,241 @@ let val_cst_type = type substitution_domain = - MSI of mod_self_id | MBI of mod_bound_id | MPI of module_path let val_subst_dom = - val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|] + val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|] module Umap = Map.Make(struct type t = substitution_domain let compare = Pervasives.compare end) -type resolver -type substitution = (module_path * resolver option) Umap.t +type delta_hint = + Inline of constr option + | Equiv of kernel_name + | Prefix_equiv of module_path + +type delta_key = + KN of kernel_name + | MP of module_path + +module Deltamap = Map.Make(struct + type t = delta_key + let compare = Pervasives.compare + end) + +type delta_resolver = delta_hint Deltamap.t + +let empty_delta_resolver = Deltamap.empty + +type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a -let val_res = val_opt no_val +let val_res_dom = no_val + (*val_sum "resolver_domain" 0 [|[|val_kn|];[|val_mp|]|]*) + +let val_res = no_val + (* val_map ~name:"delta_resolver" + val_res_dom + (val_sum "resolver_codomain" 0 [|[|val_opt val_constr||];[|val_kn|];[|val_mp|]|])*) let val_subst = val_map ~name:"substitution" val_subst_dom (val_tuple "substition range" [|val_mp;val_res|]) -let fold_subst fs fb fp = +let fold_subst fb fp = Umap.fold (fun k (mp,_) acc -> match k with - MSI msid -> fs msid mp acc | MBI mbid -> fb mbid mp acc | MPI mp1 -> fp mp1 mp acc) let empty_subst = Umap.empty -let add_msid msid mp = - Umap.add (MSI msid) (mp,None) let add_mbid mbid mp = - Umap.add (MBI mbid) (mp,None) + Umap.add (MBI mbid) (mp,empty_delta_resolver) let add_mp mp1 mp2 = - Umap.add (MPI mp1) (mp2,None) + Umap.add (MPI mp1) (mp2,empty_delta_resolver) -let map_msid msid mp = add_msid msid mp empty_subst let map_mbid mbid mp = add_mbid mbid mp empty_subst let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst +let add_inline_delta_resolver con = + Deltamap.add (KN(user_con con)) (Inline None) + +let add_inline_constr_delta_resolver con cstr = + Deltamap.add (KN(user_con con)) (Inline (Some cstr)) + +let add_constant_delta_resolver con = + Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) + +let add_mind_delta_resolver mind = + Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind)) + +let add_mp_delta_resolver mp1 mp2 = + Deltamap.add (MP mp1) (Prefix_equiv mp2) + +let mp_in_delta mp = + Deltamap.mem (MP mp) + +let con_in_delta con resolver = +try + match Deltamap.find (KN(user_con con)) resolver with + | Inline _ | Prefix_equiv _ -> false + | Equiv _ -> true +with + Not_found -> false + +let mind_in_delta mind resolver = +try + match Deltamap.find (KN(user_mind mind)) resolver with + | Inline _ | Prefix_equiv _ -> false + | Equiv _ -> true +with + Not_found -> false + +let delta_of_mp resolve mp = + try + match Deltamap.find (MP mp) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly "mod_subst: bad association in delta_resolver" + with + Not_found -> mp + +let delta_of_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> kn + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found -> kn + +let remove_mp_delta_resolver resolver mp = + Deltamap.remove (MP mp) resolver + +exception Inline_kn + +let rec find_prefix resolve mp = + let rec sub_mp = function + | MPdot(mp,l) as mp_sup -> + (try + match Deltamap.find (MP mp_sup) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found -> MPdot(sub_mp mp,l)) + | p -> + match Deltamap.find (MP p) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + in + try + sub_mp mp + with + Not_found -> mp + +let solve_delta_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> raise Inline_kn + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found | Inline_kn -> + let mp,dir,l = repr_kn kn in + let new_mp = find_prefix resolve mp in + if mp == new_mp then + kn + else + make_kn new_mp dir l + + +let constant_of_delta resolve con = + let kn = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn new_kn + +let constant_of_delta2 resolve con = + let kn = canonical_con con in + let kn1 = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn1 new_kn + +let mind_of_delta resolve mind = + let kn = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn new_kn + +let mind_of_delta2 resolve mind = + let kn = canonical_mind mind in + let kn1 = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn1 new_kn + + + +let inline_of_delta resolver = + let extract key hint l = + match key,hint with + |KN kn, Inline _ -> kn::l + | _,_ -> l + in + Deltamap.fold extract resolver [] + +exception Not_inline + +let constant_of_delta_with_inline resolve con = + let kn1,kn2 = canonical_con con,user_con con in + try + match Deltamap.find (KN kn2) resolve with + | Inline None -> None + | Inline (Some const) -> Some const + | _ -> raise Not_inline + with + Not_found | Not_inline -> + try match Deltamap.find (KN kn1) resolve with + | Inline None -> None + | Inline (Some const) -> Some const + | _ -> raise Not_inline + with + Not_found | Not_inline -> None + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPself sid -> - let mp',resolve = Umap.find (MSI sid) sub in + | MPfile sid -> + let mp',resolve = Umap.find (MPI (MPfile sid)) sub in mp',resolve | MPbound bid -> - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve + begin + try + let mp',resolve = Umap.find (MBI bid) sub in + mp',resolve + with Not_found -> + let mp',resolve = Umap.find (MPI mp) sub in + mp',resolve + end | MPdot (mp1,l) as mp2 -> begin try @@ -94,59 +275,135 @@ let subst_mp0 sub mp = (* 's like subst *) let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end - | _ -> raise Not_found in try Some (aux mp) with Not_found -> None - - -let subst_mp0 sub mp = (* 's like subst *) - let rec aux mp = - match mp with - | MPself sid -> fst (Umap.find (MSI sid) sub) - | MPbound bid -> fst (Umap.find (MBI bid) sub) - | MPdot (mp1,l) as mp2 -> - begin - try fst (Umap.find (MPI mp2) sub) - with Not_found -> MPdot (aux mp1,l) - end - - | _ -> raise Not_found - in - try Some (aux mp) with Not_found -> None - let subst_mp sub mp = match subst_mp0 sub mp with None -> mp - | Some mp' -> mp' + | Some (mp',_) -> mp' -let subst_kn0 sub kn = +let subst_kn_delta sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with - Some mp' -> - Some (make_kn mp' dir l) - | None -> None + Some (mp',resolve) -> + solve_delta_kn resolve (make_kn mp' dir l) + | None -> kn let subst_kn sub kn = - match subst_kn0 sub kn with - None -> kn - | Some kn' -> kn' + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',_) -> + make_kn mp' dir l + | None -> kn + +exception No_subst + +type sideconstantsubst = + | User + | Canonical + +let subst_ind sub mind = + let kn1,kn2 = user_mind mind,canonical_mind mind in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,mind',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_mind_equiv mp1' mp2' dir l), resolve2 + in + match side with + |User -> + let mind = mind_of_delta resolve mind' in + mind + |Canonical -> + let mind = mind_of_delta2 resolve mind' in + mind + with + No_subst -> mind + +let subst_mind0 sub mind = + let kn1,kn2 = user_mind mind,canonical_mind mind in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,mind',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_mind_equiv mp1' mp2' dir l), resolve2 + in + match side with + |User -> + let mind = mind_of_delta resolve mind' in + Some mind + |Canonical -> + let mind = mind_of_delta2 resolve mind' in + Some mind + with + No_subst -> Some mind let subst_con sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> con - | Some mp' -> make_con mp' dir l + let kn1,kn2 = user_con con,canonical_con con in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,con',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_con_equiv mp1' mp2' dir l), resolve2 + in + match constant_of_delta_with_inline resolve con' with + None -> begin + match side with + |User -> + let con = constant_of_delta resolve con' in + con,Const con + |Canonical -> + let con = constant_of_delta2 resolve con' in + con,Const con + end + | Some t -> con',t + with No_subst -> con , Const con + let subst_con0 sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> None - | Some mp' -> - let con' = make_con mp' dir l in - Some (Const con') + let kn1,kn2 = user_con con,canonical_con con in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,con',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_con_equiv mp1' mp2' dir l), resolve2 + in + match constant_of_delta_with_inline resolve con' with + None ->begin + match side with + |User -> + let con = constant_of_delta resolve con' in + Some (Const con) + |Canonical -> + let con = constant_of_delta2 resolve con' in + Some (Const con) + end + | t -> t + with No_subst -> Some (Const con) + let rec map_kn f f' c = let func = map_kn f f' in @@ -220,22 +477,8 @@ let rec map_kn f f' c = | _ -> c let subst_mps sub = - map_kn (subst_kn0 sub) (subst_con0 sub) + map_kn (subst_mind0 sub) (subst_con0 sub) -let rec replace_mp_in_mp mpfrom mpto mp = - match mp with - | _ when mp = mpfrom -> mpto - | MPdot (mp1,l) -> - let mp1' = replace_mp_in_mp mpfrom mpto mp1 in - if mp1==mp1' then mp - else MPdot (mp1',l) - | _ -> mp - -let replace_mp_in_con mpfrom mpto kn = - let mp,dir,l = kn in - let mp'' = replace_mp_in_mp mpfrom mpto mp in - if mp==mp'' then kn - else (mp'', dir, l) type 'a lazy_subst = | LSval of 'a @@ -253,117 +496,115 @@ let force fsubst r = r := LSval a'; a' - - -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,_) = - match subst_mp0 sub mp with - None -> mp,None - | Some mp' -> mp',None in - let subst = Umap.mapi (apply_subst subst2) subst1 in - (Umap.fold Umap.add subst2 subst) - -let subst_key subst1 subst2 = - let replace_in_key key mp 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 sub - | Some mpi -> Umap.add mpi mp sub +let mp_in_key mp key = + let rec mp_rec mp1 = + match mp1 with + | _ when mp1 = mp -> true + | MPdot (mp2,l) -> mp_rec mp2 + | _ -> false + in + match key with + | MP mp1 -> + mp_rec mp1 + | KN kn -> + let mp1,dir,l = repr_kn kn in + mp_rec mp1 + +let subset_prefixed_by mp resolver = + let prefixmp key hint resolv = + if mp_in_key mp key then + Deltamap.add key hint resolv + else + resolv in - Umap.fold replace_in_key subst2 empty_subst - -let update_subst_alias subst1 subst2 = - let subst_inv key (mp,_) 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 + Deltamap.fold prefixmp resolver empty_delta_resolver + +let subst_dom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match key with + (MP mp) -> + Deltamap.add (MP (subst_mp subst mp)) hint resolver + | (KN kn) -> + Deltamap.add (KN (subst_kn subst kn)) hint resolver in - let subst_mbi = Umap.fold subst_inv subst2 empty_subst in - let alias_subst key (mp,_) 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,None) sub - | Some mpi -> Umap.add mpi (mp,None) sub - in - Umap.fold alias_subst subst1 empty_subst + Deltamap.fold apply_subst resolver empty_delta_resolver -let join_alias (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,_) = - match subst_mp0 sub mp with - None -> mp,None - | Some mp' -> mp',None in - Umap.mapi (apply_subst subst2) subst1 - - -let update_subst subst1 subst2 = - let subst_inv key (mp,_) l = - let newmp = - match key with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - match mp with - | MPbound mbid -> ((MBI mbid),newmp)::l - | MPself msid -> ((MSI msid),newmp)::l - | _ -> ((MPI mp),newmp)::l +let subst_mp_delta sub mp key= + match subst_mp0 sub mp with + None -> empty_delta_resolver,mp + | Some (mp',resolve) -> + let mp1 = find_prefix resolve mp' in + let resolve1 = subset_prefixed_by mp1 resolve in + match key with + MP mpk -> + (subst_dom_delta_resolver + (map_mp mp1 mpk) resolve1),mp1 + | _ -> anomaly "Mod_subst: Bad association in resolver" + +let subst_codom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match hint with + Prefix_equiv mp -> + let derived_resolve,mpnew = subst_mp_delta subst mp key in + Deltamap.fold Deltamap.add derived_resolve + (Deltamap.add key (Prefix_equiv mpnew) resolver) + | (Equiv kn) -> + Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver + | Inline None -> + Deltamap.add key hint resolver + | Inline (Some t) -> + Deltamap.add key (Inline (Some (subst_mps subst t))) resolver in - let subst_mbi = Umap.fold subst_inv subst2 [] in - let alias_subst key (mp,_) sub= - let newsetkey = - match key with - | MPI mp1 -> - let compute_set_newkey l (k,mp') = - let mp_from_key = match k with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1)::l - in - begin - match List.fold_left compute_set_newkey [] subst_mbi with - | [] -> None - | l -> Some (l) - end - | _ -> None + Deltamap.fold apply_subst resolver empty_delta_resolver + +let subst_dom_codom_delta_resolver subst resolver = + subst_dom_delta_resolver subst + (subst_codom_delta_resolver subst resolver) + +let update_delta_resolver resolver1 resolver2 = + let apply_res key hint res = + try + match hint with + Prefix_equiv mp -> + let new_hint = + Prefix_equiv (find_prefix resolver2 mp) + in Deltamap.add key new_hint res + | Equiv kn -> + let new_hint = + Equiv (solve_delta_kn resolver2 kn) + in Deltamap.add key new_hint res + | _ -> Deltamap.add key hint res + with not_found -> + Deltamap.add key hint res in - match newsetkey with - | None -> sub - | Some l -> - List.fold_left (fun s k -> Umap.add k (mp,None) s) - sub l - in - Umap.fold alias_subst subst1 empty_subst + Deltamap.fold apply_res resolver1 empty_delta_resolver + +let add_delta_resolver resolver1 resolver2 = + if resolver1 == resolver2 then + resolver2 + else + Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) + resolver2 +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' + ,Some resolve' in + let resolve'' : delta_resolver = + match resolve' with + Some res -> + add_delta_resolver + (subst_dom_codom_delta_resolver sub resolve) + res + | None -> + subst_codom_delta_resolver sub resolve + in + mp',resolve'' in + let subst = Umap.mapi (apply_subst subst2) subst1 in + (Umap.fold Umap.add subst2 subst) let subst_substituted s r = match !r with @@ -414,7 +655,7 @@ let val_recarg = val_sum "recarg" 1 (* Norec *) let subst_recarg sub r = match r with | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_kn sub kn in + | Imbr (kn,i) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) type wf_paths = recarg Rtree.t @@ -547,8 +788,6 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } let val_ind_pack = val_tuple "mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; @@ -605,8 +844,7 @@ let subst_mind sub mib = mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints ; - mind_equiv = Option.map (subst_kn sub) mib.mind_equiv } + mind_constraints = mib.mind_constraints } (* Modules *) @@ -616,7 +854,6 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -624,116 +861,120 @@ and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path | 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 - * Univ.constraints + | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * - struct_expr_body option * Univ.constraints + With_module_body of identifier list * module_path | With_definition_body of identifier list * constant_body and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : Univ.constraints; - mod_alias : substitution; + mod_delta : delta_resolver; mod_retroknowledge : action list} and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : Univ.constraints; + typ_delta :delta_resolver} (* the validation functions: *) let rec val_sfb o = val_sum "struct_field_body" 0 [|[|val_cb|]; (* SFBconst *) [|val_ind_pack|]; (* SFBmind *) [|val_module|]; (* SFBmodule *) - [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *) [|val_modtype|] (* SFBmodtype *) |] o and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o and val_seb o = val_sum "struct_expr_body" 0 [|[|val_mp|]; (* SEBident *) [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *) - [|val_uid;val_sb|]; (* SEBstruct *) + [|val_sb|]; (* SEBstruct *) [|val_seb;val_seb;val_cstrs|]; (* SEBapply *) [|val_seb;val_with|] (* SEBwith *) |] o and val_with o = val_sum "with_declaration_body" 0 - [|[|val_list val_id;val_mp;val_cstrs|]; + [|[|val_list val_id;val_mp|]; [|val_list val_id;val_cb|]|] o and val_module o = val_tuple "module_body" - [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o + [|val_mp;val_opt val_seb;val_opt val_seb; + val_seb;val_cstrs;val_res;no_val|] o and val_modtype o = val_tuple "module_type_body" - [|val_seb;val_opt val_mp;val_subst|] o + [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o let rec subst_with_body sub = function - | With_module_body(id,mp,typ_opt,cst) -> - With_module_body(id,subst_mp sub mp, - Option.smartmap (subst_struct_expr sub) typ_opt,cst) + | 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) -and subst_modtype sub mtb = +and subst_modtype sub mtb= let typ_expr' = subst_struct_expr sub mtb.typ_expr in - if typ_expr'==mtb.typ_expr then - mtb + 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_expr = typ_expr'} - -and subst_structure sub sign = - let subst_body = function - SFBconst cb -> + {mtb with + typ_mp = mp; + typ_expr = typ_expr'; + typ_expr_alg = typ_alg'} + +and subst_structure sub sign = + let subst_body = function + SFBconst cb -> SFBconst (subst_const_body sub cb) - | SFBmind mib -> + | SFBmind mib -> SFBmind (subst_mind sub mib) - | SFBmodule mb -> - SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> + | SFBmodule mb -> + SFBmodule (subst_module sub mb) + | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb) - | SFBalias (mp,typ_opt ,cst) -> - SFBalias (subst_mp sub mp, - Option.smartmap (subst_struct_expr sub) typ_opt,cst) in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub mb = - 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 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_constraints=mb.mod_constraints; - mod_alias = mb_alias; - mod_retroknowledge=mb.mod_retroknowledge} +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 (msid, mtb, meb') -> - SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') - | SEBstruct (msid,str)-> - SEBstruct(msid, subst_structure sub str) + | 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 (meb,wdb)-> SEBwith(subst_struct_expr sub meb, subst_with_body sub wdb) -let subst_signature_msid msid mp = - subst_structure (map_msid msid mp) |