aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/declareops.ml188
-rw-r--r--kernel/declareops.mli1
-rw-r--r--kernel/modops.ml327
-rw-r--r--kernel/modops.mli26
4 files changed, 310 insertions, 232 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 76d9876c4..da945b67b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -14,7 +14,7 @@ open Util
(** Operations concernings types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
-(** Constants *)
+(** {6 Constants } *)
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
@@ -29,40 +29,54 @@ let is_opaque cb = match cb.const_body with
| OpaqueDef _ -> true
| Undef _ | Def _ -> false
-(** Constant substitutions *)
+(** {7 Constant substitutions } *)
let subst_rel_declaration sub (id,copt,t as x) =
let copt' = Option.smartmap (subst_mps sub) copt in
let t' = subst_mps sub t in
- if copt == copt' & t == t' then x else (id,copt',t')
+ if copt == copt' && t == t' then x else (id,copt',t')
let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
-(* TODO: these substitution functions could avoid duplicating things
- when the substitution have preserved all the fields *)
+let subst_const_type sub arity = match arity with
+ | NonPolymorphicType s ->
+ let s' = subst_mps sub s in
+ if s==s' then arity else NonPolymorphicType s'
+ | PolymorphicArity (ctx,s) ->
+ let ctx' = subst_rel_context sub ctx in
+ if ctx==ctx' then arity else PolymorphicArity (ctx',s)
-let subst_const_type sub arity =
- if is_empty_subst sub then arity
- else match arity with
- | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
- | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+(** No need here to check for physical equality after substitution,
+ at least for Def due to the delayed substitution [subst_constr_subst]. *)
-let subst_const_def sub = function
- | Undef inl -> Undef inl
+let subst_const_def sub def = match def with
+ | Undef _ -> def
| Def c -> Def (subst_constr_subst sub c)
| OpaqueDef lc ->
- OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
-
-let subst_const_body sub cb = {
- const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
- const_body = subst_const_def sub cb.const_body;
- const_type = subst_const_type sub cb.const_type;
- const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
- const_constraints = cb.const_constraints;
- const_native_name = ref NotLinked;
- const_inline_code = cb.const_inline_code }
-
-(** Hash-consing of constants *)
+ OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
+
+let subst_const_body sub cb =
+ assert (List.is_empty cb.const_hyps); (* we're outside sections *)
+ if is_empty_subst sub then cb
+ else
+ let body' = subst_const_def sub cb.const_body in
+ let type' = subst_const_type sub cb.const_type in
+ if body' == cb.const_body && type' == cb.const_type then cb
+ else
+ { const_hyps = [];
+ const_body = body';
+ const_type = type';
+ const_body_code =
+ Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+ const_constraints = cb.const_constraints;
+ const_native_name = ref NotLinked;
+ const_inline_code = cb.const_inline_code }
+
+(** {7 Hash-consing of constants } *)
+
+(** This hash-consing is currently quite partial : we only
+ share internal fields (e.g. constr), and not the records
+ themselves. But would it really bring substantial gains ? *)
let hcons_rel_decl ((n,oc,t) as d) =
let n' = Names.Name.hcons n
@@ -103,7 +117,7 @@ let hcons_const_body cb =
(Univ.hcons_constraints (Future.force cb.const_constraints))
else cb.const_constraints }
-(** Inductive types *)
+(** {6 Inductive types } *)
let eq_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> true
@@ -113,10 +127,12 @@ let eq_recarg r1 r2 = match r1, r2 with
let subst_recarg sub r = match r with
| Norec -> r
- | Mrec (kn,i) -> let kn' = subst_ind sub kn in
- if kn==kn' then r else Mrec (kn',i)
- | Imbr (kn,i) -> let kn' = subst_ind sub kn in
- if kn==kn' then r else Imbr (kn',i)
+ | Mrec (kn,i) ->
+ let kn' = subst_ind sub kn in
+ if kn==kn' then r else Mrec (kn',i)
+ | Imbr (kn,i) ->
+ let kn' = subst_ind sub kn in
+ if kn==kn' then r else Imbr (kn',i)
let mk_norec = Rtree.mk_node Norec [||]
@@ -142,61 +158,79 @@ let recarg_length p j =
let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
-(** Substitution of inductive declarations *)
-
-let subst_indarity sub = function
-| Monomorphic s ->
- Monomorphic {
- mind_user_arity = subst_mps sub s.mind_user_arity;
- mind_sort = s.mind_sort;
- }
-| Polymorphic s as x -> x
-
-let subst_mind_packet sub mbp =
- { mind_consnames = mbp.mind_consnames;
- mind_consnrealdecls = mbp.mind_consnrealdecls;
- mind_typename = mbp.mind_typename;
- mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
- mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
- mind_arity = subst_indarity sub mbp.mind_arity;
- mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
- mind_nrealargs = mbp.mind_nrealargs;
- mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
- mind_kelim = mbp.mind_kelim;
- mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
- mind_nb_constant = mbp.mind_nb_constant;
- mind_nb_args = mbp.mind_nb_args;
- mind_reloc_tbl = mbp.mind_reloc_tbl }
+(** {7 Substitution of inductive declarations } *)
+
+let subst_indarity sub ar = match ar with
+ | Monomorphic s ->
+ let uar' = subst_mps sub s.mind_user_arity in
+ if uar' == s.mind_user_arity then ar
+ else Monomorphic { mind_user_arity = uar'; mind_sort = s.mind_sort }
+ | Polymorphic _ -> ar
+
+let subst_mind_packet sub mip =
+ let { mind_nf_lc = nf;
+ mind_user_lc = user;
+ mind_arity_ctxt = ctxt;
+ mind_arity = ar;
+ mind_recargs = ra } = mip
+ in
+ let nf' = Array.smartmap (subst_mps sub) nf in
+ let user' =
+ (* maintain sharing of [mind_user_lc] and [mind_nf_lc] *)
+ if user==nf then nf'
+ else Array.smartmap (subst_mps sub) user
+ in
+ let ctxt' = subst_rel_context sub ctxt in
+ let ar' = subst_indarity sub ar in
+ let ra' = subst_wf_paths sub ra in
+ if nf==nf' && user==user' && ctxt==ctxt' && ar==ar' && ra==ra'
+ then mip
+ else
+ { mip with
+ mind_nf_lc = nf';
+ mind_user_lc = user';
+ mind_arity_ctxt = ctxt';
+ mind_arity = ar';
+ mind_recargs = ra' }
let subst_mind sub mib =
- { mind_record = mib.mind_record ;
- mind_finite = mib.mind_finite ;
- mind_ntypes = mib.mind_ntypes ;
- mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
- mind_nparams = mib.mind_nparams;
- mind_nparams_rec = mib.mind_nparams_rec;
- mind_params_ctxt =
- Context.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_native_name = ref NotLinked }
-
-(** Hash-consing of inductive declarations *)
+ assert (List.is_empty mib.mind_hyps); (* we're outside sections *)
+ if is_empty_subst sub then mib
+ else
+ let params = mib.mind_params_ctxt in
+ let params' = Context.map_rel_context (subst_mps sub) params in
+ let packets = mib.mind_packets in
+ let packets' = Array.smartmap (subst_mind_packet sub) packets in
+ if params==params' && packets==packets' then mib
+ else
+ { mib with
+ mind_params_ctxt = params';
+ mind_packets = packets';
+ mind_native_name = ref NotLinked }
+
+(** {6 Hash-consing of inductive declarations } *)
+
+(** Just as for constants, this hash-consing is quite partial *)
let hcons_indarity = function
| Monomorphic a ->
- Monomorphic { mind_user_arity = Term.hcons_constr a.mind_user_arity;
- mind_sort = Term.hcons_sorts a.mind_sort }
+ Monomorphic
+ { mind_user_arity = Term.hcons_constr a.mind_user_arity;
+ mind_sort = Term.hcons_sorts a.mind_sort }
| Polymorphic a -> Polymorphic (hcons_polyarity a)
let hcons_mind_packet oib =
- { oib with
- mind_typename = Names.Id.hcons oib.mind_typename;
- mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
- mind_arity = hcons_indarity oib.mind_arity;
- mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
- mind_user_lc = Array.smartmap Term.hcons_types oib.mind_user_lc;
- mind_nf_lc = Array.smartmap Term.hcons_types oib.mind_nf_lc }
+ let user = Array.smartmap Term.hcons_types oib.mind_user_lc in
+ let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in
+ (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
+ let nf = if Array.equal (==) user nf then user else nf in
+ { oib with
+ mind_typename = Names.Id.hcons oib.mind_typename;
+ mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
+ mind_arity = hcons_indarity oib.mind_arity;
+ mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
+ mind_user_lc = user;
+ mind_nf_lc = nf }
let hcons_mind mib =
{ mib with
@@ -204,6 +238,8 @@ let hcons_mind mib =
mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
mind_constraints = Univ.hcons_constraints mib.mind_constraints }
+(** {6 Stm machinery } *)
+
let join_constant_body cb =
ignore(Future.join cb.const_constraints);
match cb.const_body with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 0da7c85c7..54eed5ea6 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -14,7 +14,6 @@ open Mod_subst
(** {6 Constants} *)
-val subst_const_def : substitution -> constant_def -> constant_def
val subst_const_body : substitution -> constant_body -> constant_body
(** Is there a actual body in const_body ? *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d431fdfdd..deff291ec 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -25,6 +25,8 @@ open Environ
open Entries
open Mod_subst
+(** {6 Errors } *)
+
type signature_mismatch_error =
| InductiveFieldExpected of mutual_inductive_body
| DefinitionFieldExpected
@@ -45,7 +47,8 @@ type signature_mismatch_error =
| NoTypeConstraintExpected
type module_typing_error =
- | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error
+ | SignatureMismatch of
+ Label.t * structure_field_body * signature_mismatch_error
| LabelAlreadyDeclared of Label.t
| ApplicationToNotPath of module_struct_entry
| NotAFunctor of struct_expr_body
@@ -109,17 +112,17 @@ let error_no_such_label_sub l l1 =
let error_higher_order_include () =
raise (ModuleTypingError HigherOrderInclude)
-let destr_functor mtb =
- match mtb with
- | SEBfunctor (arg_id,arg_t,body_t) ->
- (arg_id,arg_t,body_t)
- | _ -> error_not_a_functor mtb
+(** {6 Misc operations } *)
+
+let destr_functor = function
+ | SEBfunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
+ | mtb -> error_not_a_functor mtb
let is_functor = function
- | SEBfunctor (arg_id,arg_t,body_t) -> true
- | _ -> false
+ | SEBfunctor _ -> true
+ | _ -> false
-let module_body_of_type mp mtb =
+let module_body_of_type mp mtb =
{ mod_mp = mp;
mod_type = mtb.typ_expr;
mod_type_alg = mtb.typ_expr_alg;
@@ -128,103 +131,119 @@ let module_body_of_type mp mtb =
mod_delta = mtb.typ_delta;
mod_retroknowledge = []}
-let check_modpath_equiv env mp1 mp2 =
- if mp_eq mp1 mp2 then () else
- let mb1=lookup_module mp1 env in
- let mb2=lookup_module mp2 env in
- if mp_eq (mp_of_delta mb1.mod_delta mp1) (mp_of_delta mb2.mod_delta mp2)
- then ()
- else error_not_equal_modpaths mp1 mp2
-
+let check_modpath_equiv env mp1 mp2 =
+ if ModPath.equal mp1 mp2 then ()
+ else
+ let mp1' = mp_of_delta (lookup_module mp1 env).mod_delta mp1 in
+ let mp2' = mp_of_delta (lookup_module mp2 env).mod_delta mp2 in
+ if ModPath.equal mp1' mp2' then ()
+ else error_not_equal_modpaths mp1 mp2
+
+(** {6 Substitutions of modular structures } *)
+
+let id_delta x y = x
+
let rec subst_with_body sub = function
- | With_module_body(id,mp) ->
- With_module_body(id,subst_mp sub mp)
- | With_definition_body(id,cb) ->
- With_definition_body( id,subst_const_body sub cb)
+ |With_module_body(id,mp) as orig ->
+ let mp' = subst_mp sub mp in
+ if mp==mp' then orig else With_module_body(id,mp')
+ |With_definition_body(id,cb) as orig ->
+ let cb' = subst_const_body sub cb in
+ if cb==cb' then orig else With_definition_body(id,cb')
and subst_modtype sub do_delta mtb=
- let mp = subst_mp sub mtb.typ_mp in
- let sub = add_mp mtb.typ_mp mp empty_delta_resolver sub in
- let typ_expr' = subst_struct_expr sub do_delta mtb.typ_expr in
- let typ_alg' =
- Option.smartmap
- (subst_struct_expr sub (fun x y-> x)) mtb.typ_expr_alg in
- let mtb_delta = do_delta mtb.typ_delta sub in
- if typ_expr'==mtb.typ_expr &&
- typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
- mtb
- else
- {mtb with
- typ_mp = mp;
- typ_expr = typ_expr';
- typ_expr_alg = typ_alg';
- typ_delta = mtb_delta}
-
-and subst_structure sub do_delta sign =
- 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 do_delta mb)
- | SFBmodtype mtb ->
- SFBmodtype (subst_modtype sub do_delta mtb)
+ let { typ_mp = mp; typ_expr = ty; typ_expr_alg = aty } = mtb in
+ let mp' = subst_mp sub mp in
+ let sub =
+ if ModPath.equal mp mp' then sub
+ else add_mp mp mp' empty_delta_resolver sub
in
- List.map (fun (l,b) -> (l,subst_body b)) sign
+ let ty' = subst_struct_expr sub do_delta ty in
+ let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in
+ let delta' = do_delta mtb.typ_delta sub in
+ if mp==mp' && ty==ty' && aty==aty' && delta'==mtb.typ_delta
+ then mtb
+ else
+ { mtb with
+ typ_mp = mp';
+ typ_expr = ty';
+ typ_expr_alg = aty';
+ typ_delta = delta' }
+
+and subst_structure sub do_delta sign =
+ let subst_body ((l,body) as orig) = match body with
+ | SFBconst cb ->
+ let cb' = subst_const_body sub cb in
+ if cb==cb' then orig else (l,SFBconst cb')
+ | SFBmind mib ->
+ let mib' = subst_mind sub mib in
+ if mib==mib' then orig else (l,SFBmind mib')
+ | SFBmodule mb ->
+ let mb' = subst_module sub do_delta mb in
+ if mb==mb' then orig else (l,SFBmodule mb')
+ | SFBmodtype mtb ->
+ let mtb' = subst_modtype sub do_delta mtb in
+ if mtb==mtb' then orig else (l,SFBmodtype mtb')
+ in
+ List.smartmap subst_body sign
and subst_module sub do_delta mb =
- let mp = subst_mp sub mb.mod_mp in
- let sub = if is_functor mb.mod_type && not (mp_eq mp mb.mod_mp) then
- add_mp mb.mod_mp mp
- empty_delta_resolver sub else sub in
- let id_delta = (fun x y-> x) in
- let mtb',me' =
- let mtb = subst_struct_expr sub do_delta mb.mod_type in
- match mb.mod_expr with
- None -> mtb,None
- | Some me -> if me==mb.mod_type then
- mtb,Some mtb
- else mtb,Option.smartmap
- (subst_struct_expr sub id_delta) mb.mod_expr
+ let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in
+ let mp' = subst_mp sub mp in
+ let sub =
+ if not (is_functor ty) || ModPath.equal mp mp' then sub
+ else add_mp mp mp' empty_delta_resolver sub
+ in
+ let ty' = subst_struct_expr sub do_delta ty in
+ (* Special optim : maintain sharing between [mod_expr] and [mod_type] *)
+ let me' = match me with
+ | Some m when m == ty -> if ty == ty' then me else Some ty'
+ | _ -> Option.smartmap (subst_struct_expr sub id_delta) me
in
- let typ_alg' = Option.smartmap
- (subst_struct_expr sub id_delta) mb.mod_type_alg in
- let mb_delta = do_delta mb.mod_delta sub in
- if mtb'==mb.mod_type && mb.mod_expr == me'
- && mb_delta == mb.mod_delta && mp == mb.mod_mp
- then mb else
- { mb with
- mod_mp = mp;
- mod_expr = me';
- mod_type_alg = typ_alg';
- mod_type=mtb';
- mod_delta = mb_delta}
-
-and subst_struct_expr sub do_delta = function
- | SEBident mp -> SEBident (subst_mp sub mp)
- | SEBfunctor (mbid, mtb, meb') ->
- SEBfunctor(mbid,subst_modtype sub do_delta mtb
- ,subst_struct_expr sub do_delta meb')
- | SEBstruct (str)->
- SEBstruct( subst_structure sub do_delta str)
- | SEBapply (meb1,meb2,cst)->
- SEBapply(subst_struct_expr sub do_delta meb1,
- subst_struct_expr sub do_delta meb2,
- cst)
- | SEBwith (meb,wdb)->
- SEBwith(subst_struct_expr sub do_delta meb,
- subst_with_body sub wdb)
+ let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in
+ let delta' = do_delta mb.mod_delta sub in
+ if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
+ then mb
+ else
+ { mb with
+ mod_mp = mp';
+ mod_expr = me';
+ mod_type = ty';
+ mod_type_alg = aty';
+ mod_delta = delta' }
+
+and subst_struct_expr sub do_delta seb = match seb with
+ |SEBident mp ->
+ let mp' = subst_mp sub mp in
+ if mp==mp' then seb else SEBident mp'
+ |SEBfunctor (mbid, mtb, meb) ->
+ let mtb' = subst_modtype sub do_delta mtb in
+ let meb' = subst_struct_expr sub do_delta meb in
+ if mtb==mtb' && meb==meb' then seb
+ else SEBfunctor(mbid,mtb',meb')
+ |SEBstruct str ->
+ let str' = subst_structure sub do_delta str in
+ if str==str' then seb else SEBstruct str'
+ |SEBapply (meb1,meb2,cst) ->
+ let meb1' = subst_struct_expr sub do_delta meb1 in
+ let meb2' = subst_struct_expr sub do_delta meb2 in
+ if meb1==meb1' && meb2==meb2' then seb else SEBapply(meb1',meb2',cst)
+ |SEBwith (meb,wdb) ->
+ let meb' = subst_struct_expr sub do_delta meb in
+ let wdb' = subst_with_body sub wdb in
+ if meb==meb' && wdb==wdb' then seb else SEBwith(meb',wdb')
let subst_signature subst =
- subst_structure subst
+ subst_structure subst
(fun resolver subst-> subst_codom_delta_resolver subst resolver)
-let subst_struct_expr subst =
+let subst_struct_expr subst =
subst_struct_expr subst
(fun resolver subst-> subst_codom_delta_resolver subst resolver)
-(* spiwack: here comes the function which takes care of importing
+(** {6 Retroknowledge } *)
+
+(* spiwack: here comes the function which takes care of importing
the retroknowledge declared in the library *)
(* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
let add_retroknowledge mp =
@@ -235,7 +254,9 @@ let add_retroknowledge mp =
(match e with
| Const kn -> kind_of_term (mkConst kn)
| Ind ind -> kind_of_term (mkInd ind)
- | _ -> anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term"))
+ | _ ->
+ anomaly ~label:"Modops.add_retroknowledge"
+ (Pp.str "had to import an unsupported kind of term"))
in
fun lclrk env ->
(* The order of the declaration matters, for instance (and it's at the
@@ -243,23 +264,25 @@ let add_retroknowledge mp =
int31 type registration absolutely needs int31 bits to be registered.
Since the local_retroknowledge is stored in reverse order (each new
registration is added at the top of the list) we need a fold_right
- for things to go right (the pun is not intented). So we lose
+ for things to go right (the pun is not intented). So we lose
tail recursivity, but the world will have exploded before any module
imports 10 000 retroknowledge registration.*)
List.fold_right perform lclrk env
-let rec add_signature mp sign resolver env =
- let add_one env (l,elem) =
- let kn = KerName.make2 mp l in
- match elem with
- | SFBconst cb ->
- Environ.add_constant (constant_of_delta_kn resolver kn) cb env
- | SFBmind mib ->
- Environ.add_mind (mind_of_delta_kn resolver kn) mib env
- | SFBmodule mb -> add_module mb env (* adds components as well *)
- | SFBmodtype mtb -> Environ.add_modtype mtb env
+(** {6 Adding a module in the environment } *)
+
+let rec add_signature mp sign resolver env =
+ let add_one env (l,elem) = match elem with
+ |SFBconst cb ->
+ let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
+ Environ.add_constant c cb env
+ |SFBmind mib ->
+ let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+ Environ.add_mind mind mib env
+ |SFBmodule mb -> add_module mb env (* adds components as well *)
+ |SFBmodtype mtb -> Environ.add_modtype mtb env
in
- List.fold_left add_one env sign
+ List.fold_left add_one env sign
and add_module mb env =
let mp = mb.mod_mp in
@@ -273,6 +296,8 @@ and add_module mb env =
anomaly ~label:"Modops"
(Pp.str "the evaluation of the structure failed ")
+(** {6 Strengtening } *)
+
let strengthen_const mp_from l cb resolver =
match cb.const_body with
| Def _ -> cb
@@ -489,48 +514,54 @@ and strengthen_and_subst_struct
(l,SFBmodtype mty)::rest'
-(* Let P be a module path when we write "Module M:=P." or "Module M. Include P. End M."
- we need to perform two operations to compute the body of M. The first one is applying
- the substitution {P <- M} on the type of P and the second one is strenghtening. *)
-let strengthen_and_subst_mb mb mp include_b =
- match mb.mod_type with
- SEBstruct str ->
- let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
- (*if mb.mod_mp is an alias then the strengthening is useless
- (i.e. it is already done)*)
- let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in
- let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
- let new_resolver =
- add_mp_delta_resolver mp mp_alias
- (subst_dom_delta_resolver subst_resolver mb.mod_delta) in
- let subst = map_mp mb.mod_mp mp new_resolver in
- let resolver_out,new_sig =
- strengthen_and_subst_struct str subst
- mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
- in
- {mb with
- mod_mp = mp;
- mod_type = SEBstruct(new_sig);
- mod_expr = Some (SEBident mb.mod_mp);
- mod_delta = if include_b then resolver_out
- else add_delta_resolver new_resolver resolver_out}
- | SEBfunctor(arg_id,argb,body) ->
- let subst = map_mp mb.mod_mp mp empty_delta_resolver in
- subst_module subst
- (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb
- | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+(** Let P be a module path when we write:
+ "Module M:=P." or "Module M. Include P. End M."
+ We need to perform two operations to compute the body of M.
+ - The first one is applying the substitution {P <- M} on the type of P
+ - The second one is strenghtening. *)
+
+let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
+ |SEBstruct str ->
+ let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
+ (* if mb.mod_mp is an alias then the strengthening is useless
+ (i.e. it is already done)*)
+ let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in
+ let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
+ let new_resolver =
+ add_mp_delta_resolver mp mp_alias
+ (subst_dom_delta_resolver subst_resolver mb.mod_delta) in
+ let subst = map_mp mb.mod_mp mp new_resolver in
+ let resolver_out,new_sig =
+ strengthen_and_subst_struct str subst
+ mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
+ in
+ { mb with
+ mod_mp = mp;
+ mod_type = SEBstruct(new_sig);
+ mod_expr = Some (SEBident mb.mod_mp);
+ mod_delta =
+ if include_b then resolver_out
+ else add_delta_resolver new_resolver resolver_out }
+ |SEBfunctor(arg_id,argb,body) ->
+ let subst = map_mp mb.mod_mp mp empty_delta_resolver in
+ subst_module subst
+ (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb
+ | _ ->
+ anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
let subst_modtype_and_resolver mtb mp =
let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in
- let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
+ let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
let full_subst = (map_mp mtb.typ_mp mp new_delta) in
- subst_modtype full_subst
- (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb
+ subst_modtype full_subst
+ (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb
+
+(** {6 Cleaning a bounded module expression } *)
let rec is_bounded_expr l = function
| SEBident mp -> List.mem mp l
- | SEBapply (fexpr,mexpr,_) ->
+ | SEBapply (fexpr,mexpr,_) ->
is_bounded_expr l mexpr || is_bounded_expr l fexpr
| _ -> false
@@ -560,9 +591,9 @@ and clean_expr l = function
if str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **)
s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
| SEBstruct str as s->
- let str_clean = Util.List.smartmap (clean_struct l) str in
- if str_clean == str then s else SEBstruct(str_clean)
- | str -> str
+ let str_clean = List.smartmap (clean_struct l) str in
+ if str_clean == str then s else SEBstruct(str_clean)
+ | str -> str
let rec collect_mbid l = function
| SEBfunctor (mbid,sigt,str) as s->
@@ -570,8 +601,8 @@ let rec collect_mbid l = function
if str_clean == str then s else
SEBfunctor (mbid,sigt,str_clean)
| SEBstruct str as s->
- let str_clean = Util.List.smartmap (clean_struct l) str in
- if str_clean == str then s else SEBstruct(str_clean)
+ let str_clean = List.smartmap (clean_struct l) str in
+ if str_clean == str then s else SEBstruct(str_clean)
| _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
@@ -581,6 +612,8 @@ let clean_bounded_mod_expr = function
if str_clean == str then str else str_clean
| str -> str
+(** {6 Stm machinery : join and prune } *)
+
let rec join_module_body mb =
Option.iter join_struct_expr_body mb.mod_expr;
Option.iter join_struct_expr_body mb.mod_type_alg;
@@ -632,8 +665,9 @@ and prune_structure_body struc =
let te_alg' =
Option.smartmap prune_struct_expr_body te_alg in
if te' == te && te_alg' == te_alg then orig
- else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'}) in
- CList.smartmap prune_body struc
+ else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'})
+ in
+ List.smartmap prune_body struc
and prune_struct_expr_body orig = match orig with
| SEBfunctor (id,t,e) ->
let te, ta = t.typ_expr, t.typ_expr_alg in
@@ -660,4 +694,3 @@ and prune_struct_expr_body orig = match orig with
if sb' == sb then wdcl else With_definition_body (id, sb') in
if seb' == seb && wdcl' == wdcl then orig
else SEBwith (seb', wdcl')
-
diff --git a/kernel/modops.mli b/kernel/modops.mli
index ea92c45ea..e148f9628 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -14,28 +14,33 @@ open Declarations
open Entries
open Mod_subst
-(** Various operations on modules and module types *)
+(** {6 Various operations on modules and module types } *)
+val module_body_of_type : module_path -> module_type_body -> module_body
-val module_body_of_type : module_path -> module_type_body -> module_body
-
-val module_type_of_module : module_path option -> module_body ->
- module_type_body
+val module_type_of_module :
+ module_path option -> module_body -> module_type_body
val destr_functor :
struct_expr_body -> MBId.t * module_type_body * struct_expr_body
+val check_modpath_equiv : env -> module_path -> module_path -> unit
+
+(** {6 Substitutions } *)
+
val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body
val subst_signature : substitution -> structure_body -> structure_body
+(** {6 Adding to an environment } *)
+
val add_signature :
module_path -> structure_body -> delta_resolver -> env -> env
(** adds a module and its components, but not the constraints *)
val add_module : module_body -> env -> env
-val check_modpath_equiv : env -> module_path -> module_path -> unit
+(** {6 Strengthening } *)
val strengthen : module_type_body -> module_path -> module_type_body
@@ -48,15 +53,19 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
val subst_modtype_and_resolver : module_type_body -> module_path ->
module_type_body
+(** {6 Cleaning a bound module expression } *)
+
val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
+(** {6 Stm machinery : join and prune } *)
+
val join_module_body : module_body -> unit
val join_structure_body : structure_body -> unit
val join_struct_expr_body : struct_expr_body -> unit
val prune_structure_body : structure_body -> structure_body
-(** Errors *)
+(** {6 Errors } *)
type signature_mismatch_error =
| InductiveFieldExpected of mutual_inductive_body
@@ -78,7 +87,8 @@ type signature_mismatch_error =
| NoTypeConstraintExpected
type module_typing_error =
- | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error
+ | SignatureMismatch of
+ Label.t * structure_field_body * signature_mismatch_error
| LabelAlreadyDeclared of Label.t
| ApplicationToNotPath of module_struct_entry
| NotAFunctor of struct_expr_body
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 16:13:05 +0000