aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli17
-rw-r--r--checker/declarations.ml17
-rw-r--r--checker/mod_checking.ml26
-rw-r--r--checker/modops.ml75
-rw-r--r--checker/subtyping.ml26
-rw-r--r--checker/values.ml7
-rw-r--r--kernel/declarations.mli16
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/mod_typing.ml53
-rw-r--r--kernel/mod_typing.mli7
-rw-r--r--kernel/modops.ml88
-rw-r--r--kernel/nativelibrary.ml4
-rw-r--r--kernel/safe_typing.ml43
-rw-r--r--kernel/subtyping.ml36
-rw-r--r--library/declaremods.ml4
-rw-r--r--plugins/extraction/extract_env.ml41
-rw-r--r--printing/printmod.ml12
17 files changed, 191 insertions, 283 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index c8b7c9e66..75ce98e90 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -365,7 +365,7 @@ and module_signature = (module_type_body,structure_body) functorize
and module_expression = (module_type_body,module_alg_expr) functorize
and module_implementation =
- | Abstract (** no accessible implementation *)
+ | Abstract (** no accessible implementation (keep this constructor first!) *)
| Algebraic of module_expression (** non-interactive algebraic expression *)
| Struct of module_signature (** interactive body *)
| FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
@@ -382,18 +382,11 @@ and module_body =
mod_delta : delta_resolver;
mod_retroknowledge : action list }
-(** A [module_type_body] is similar to a [module_body], with
- no implementation and retroknowledge fields *)
-
-and module_type_body =
- { typ_mp : module_path; (** path of the module type *)
- typ_expr : module_signature; (** expanded type *)
- (** algebraic expression, kept if it's relevant for extraction *)
- typ_expr_alg : module_expression option;
- typ_constraints : Univ.constraints;
- (** quotiented set of equivalent constants and inductive names *)
- typ_delta : delta_resolver}
+(** A [module_type_body] is just a [module_body] with no
+ implementation ([mod_expr] always [Abstract]) and also
+ an empty [mod_retroknowledge] *)
+and module_type_body = module_body
(*************************************************************************)
(** {4 From safe_typing.ml} *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index d38df793f..c6709a785 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -591,23 +591,17 @@ let rec subst_expr sub = function
| MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd)
let rec subst_expression sub me =
- functor_map (subst_modtype sub) (subst_expr sub) me
+ functor_map (subst_module sub) (subst_expr sub) me
and subst_signature sub sign =
- functor_map (subst_modtype sub) (subst_structure sub) sign
-
-and subst_modtype sub mtb=
- { mtb with
- typ_mp = subst_mp sub mtb.typ_mp;
- typ_expr = subst_signature sub mtb.typ_expr;
- typ_expr_alg = Option.smartmap (subst_expression sub) mtb.typ_expr_alg }
+ functor_map (subst_module sub) (subst_structure sub) sign
and subst_structure sub struc =
let subst_body = function
| SFBconst cb -> SFBconst (subst_const_body sub cb)
| SFBmind mib -> SFBmind (subst_mind sub mib)
- | SFBmodule mb -> SFBmodule (subst_module sub mb)
- | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb)
+ | SFBmodule mb -> SFBmodule (subst_module sub mb)
+ | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb)
in
List.map (fun (l,b) -> (l,subst_body b)) struc
@@ -617,5 +611,4 @@ and subst_module sub mb =
mod_expr =
implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
mod_type = subst_signature sub mb.mod_type;
- mod_type_alg = Option.map (subst_expression sub) mb.mod_type_alg }
-
+ mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9e61d3491..998e23c6e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -64,6 +64,15 @@ let lookup_module mp env =
with Not_found ->
failwith ("Unknown module: "^string_of_mp mp)
+let mk_mtb mp sign delta =
+ { mod_mp = mp;
+ mod_expr = Abstract;
+ mod_type = sign;
+ mod_type_alg = None;
+ mod_constraints = Univ.Constraint.empty;
+ mod_delta = delta;
+ mod_retroknowledge = []; }
+
let rec check_module env mp mb =
let (_:module_signature) =
check_signature env mb.mod_type mb.mod_mp mb.mod_delta
@@ -76,25 +85,14 @@ let rec check_module env mp mb =
match optsign with
|None -> ()
|Some sign ->
- let mtb1 =
- {typ_mp=mp;
- typ_expr=sign;
- typ_expr_alg=None;
- typ_constraints=Univ.Constraint.empty;
- typ_delta = mb.mod_delta;}
- and mtb2 =
- {typ_mp=mp;
- typ_expr=mb.mod_type;
- typ_expr_alg=None;
- typ_constraints=Univ.Constraint.empty;
- typ_delta = mb.mod_delta;}
- in
+ let mtb1 = mk_mtb mp sign mb.mod_delta
+ and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in
let env = add_module_type mp mtb1 env in
Subtyping.check_subtypes env mtb1 mtb2
and check_module_type env mty =
let (_:module_signature) =
- check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in
+ check_signature env mty.mod_type mty.mod_mp mty.mod_delta in
()
and check_structure_field env mp lab res = function
diff --git a/checker/modops.ml b/checker/modops.ml
index c27c5d598..1e5cd4347 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,13 +49,7 @@ let destr_functor = function
| NoFunctor _ -> error_not_a_functor ()
let module_body_of_type mp mtb =
- { mod_mp = mp;
- mod_type = mtb.typ_expr;
- mod_type_alg = mtb.typ_expr_alg;
- mod_expr = Abstract;
- mod_constraints = mtb.typ_constraints;
- mod_delta = mtb.typ_delta;
- mod_retroknowledge = []}
+ { mtb with mod_mp = mp; mod_expr = Abstract }
let rec add_structure mp sign resolver env =
let add_one env (l,elem) =
@@ -71,7 +65,7 @@ let rec add_structure mp sign resolver env =
Environ.add_mind mind mib env
| SFBmodule mb -> add_module mb env
(* adds components as well *)
- | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
+ | SFBmodtype mtb -> Environ.add_modtype mtb.mod_mp mtb env
in
List.fold_left add_one env sign
@@ -97,23 +91,20 @@ let strengthen_const mp_from l cb resolver =
{ cb with const_body = Def (Declarations.from_val (Const (con,u))) }
let rec strengthen_mod mp_from mp_to mb =
- if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
- mb
- else
- match mb.mod_type with
- | NoFunctor (sign) ->
- let resolve_out,sign_out =
- strengthen_sig mp_from sign mp_to mb.mod_delta
- in
- { mb with
- mod_expr = Algebraic (NoFunctor (MEident mp_to));
- mod_type = NoFunctor sign_out;
- mod_type_alg = mb.mod_type_alg;
- mod_constraints = mb.mod_constraints;
- mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to
- (add_delta_resolver mb.mod_delta resolve_out)*);
- mod_retroknowledge = mb.mod_retroknowledge}
- | MoreFunctor _ -> mb
+ if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
+ else strengthen_body true mp_from mp_to mb
+
+and strengthen_body is_mod mp_from mp_to mb =
+ match mb.mod_type with
+ | MoreFunctor _ -> mb
+ | NoFunctor sign ->
+ let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
+ in
+ { mb with
+ mod_expr =
+ (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract);
+ mod_type = NoFunctor sign_out;
+ mod_delta = resolve_out }
and strengthen_sig mp_from sign mp_to resolver =
match sign with
@@ -137,33 +128,19 @@ and strengthen_sig mp_from sign mp_to resolver =
let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
resolve_out,item::rest'
-let strengthen mtb mp = match mtb.typ_expr with
- | NoFunctor sign ->
- let resolve_out,sign_out =
- strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
- in
- { mtb with
- typ_expr = NoFunctor sign_out;
- typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
- (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
- | MoreFunctor _ -> mtb
+let strengthen mtb mp =
+ strengthen_body false mtb.mod_mp mp mtb
let subst_and_strengthen mb mp =
strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
-
let module_type_of_module mp mb =
+ let mtb =
+ { mb with
+ mod_expr = Abstract;
+ mod_type_alg = None;
+ mod_retroknowledge = [] }
+ in
match mp with
- | Some mp ->
- strengthen {
- typ_mp = mp;
- typ_expr = mb.mod_type;
- typ_expr_alg = None;
- typ_constraints = mb.mod_constraints;
- typ_delta = mb.mod_delta} mp
- | None ->
- { typ_mp = mb.mod_mp;
- typ_expr = mb.mod_type;
- typ_expr_alg = None;
- typ_constraints = mb.mod_constraints;
- typ_delta = mb.mod_delta}
+ | Some mp -> strengthen {mtb with mod_mp = mp} mp
+ | None -> mtb
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0144580bc..fe88a5071 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -354,52 +354,52 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
| _ -> error_not_match l spec2
in
let env =
- add_module_type mtb2.typ_mp mtb2
- (add_module_type mtb1.typ_mp mtb1 env)
+ add_module_type mtb2.mod_mp mtb2
+ (add_module_type mtb1.mod_mp mtb1 env)
in
check_modtypes env mtb1 mtb2 subst1 subst2 true
in
List.iter check_one_body sig2
and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
- if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then ()
+ if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type then ()
else
let rec check_structure env str1 str2 equiv subst1 subst2 =
match str1,str2 with
| NoFunctor (list1),
NoFunctor (list2) ->
- check_signatures env mtb1.typ_mp list1 list2 subst1 subst2;
+ check_signatures env mtb1.mod_mp list1 list2 subst1 subst2;
if equiv then
- check_signatures env mtb2.typ_mp list2 list1 subst1 subst2
+ check_signatures env mtb2.mod_mp list2 list1 subst1 subst2
else
()
| MoreFunctor (arg_id1,arg_t1,body_t1),
MoreFunctor (arg_id2,arg_t2,body_t2) ->
check_modtypes env
arg_t2 arg_t1
- (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+ (map_mp arg_t1.mod_mp arg_t2.mod_mp) subst2
equiv;
(* contravariant *)
let env = add_module_type (MPbound arg_id2) arg_t2 env in
let env =
if is_functor body_t1 then env
else
- let env = shallow_remove_module mtb1.typ_mp env in
- add_module {mod_mp = mtb1.typ_mp;
+ let env = shallow_remove_module mtb1.mod_mp env in
+ add_module {mod_mp = mtb1.mod_mp;
mod_expr = Abstract;
mod_type = body_t1;
mod_type_alg = None;
- mod_constraints = mtb1.typ_constraints;
+ mod_constraints = mtb1.mod_constraints;
mod_retroknowledge = [];
- mod_delta = mtb1.typ_delta} env
+ mod_delta = mtb1.mod_delta} env
in
check_structure env body_t1 body_t2 equiv
(join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
subst2
| _ , _ -> error_incompatible_modtypes mtb1 mtb2
in
- check_structure env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
+ check_structure env mtb1.mod_type mtb2.mod_type equiv subst1 subst2
let check_subtypes env sup super =
- check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
- (map_mp super.typ_mp sup.typ_mp) false
+ check_modtypes env (strengthen sup sup.mod_mp) super empty_subst
+ (map_mp super.mod_mp sup.mod_mp) false
diff --git a/checker/values.ml b/checker/values.ml
index 0ac8bf78c..5c4876e59 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 27f35ee65fef280d5a7a80bb11b31837 checker/cic.mli
+MD5 f4d390282966a3fbd22a9e384046d231 checker/cic.mli
*)
@@ -296,15 +296,16 @@ and v_mexpr =
[|[|v_mae|]; (* NoFunctor *)
[|v_uid;v_modtype;v_mexpr|]|]) (* MoreFunctor *)
and v_impl =
- Sum ("module_impl",2,
+ Sum ("module_impl",2, (* Abstract, FullStruct *)
[|[|v_mexpr|]; (* Algebraic *)
[|v_sign|]|]) (* Struct *)
+and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
and v_module =
Tuple ("module_body",
[|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
and v_modtype =
Tuple ("module_type_body",
- [|v_mp;v_sign;Opt v_mexpr;v_cstrs;v_resolver|])
+ [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
(** kernel/safe_typing *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 4f1672884..2d5468ff1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -251,17 +251,11 @@ and module_body =
mod_delta : Mod_subst.delta_resolver;
mod_retroknowledge : Retroknowledge.action list }
-(** A [module_type_body] is similar to a [module_body], with
- no implementation and retroknowledge fields *)
-
-and module_type_body =
- { typ_mp : module_path; (** path of the module type *)
- typ_expr : module_signature; (** expanded type *)
- (** algebraic expression, kept if it's relevant for extraction *)
- typ_expr_alg : module_expression option;
- typ_constraints : Univ.constraints;
- (** quotiented set of equivalent constants and inductive names *)
- typ_delta : Mod_subst.delta_resolver}
+(** A [module_type_body] is just a [module_body] with no
+ implementation ([mod_expr] always [Abstract]) and also
+ an empty [mod_retroknowledge] *)
+
+and module_type_body = module_body
(** Extra invariants :
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 45dfb22d3..6e5491c0b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -436,7 +436,7 @@ let keep_hyps env needed =
(* Modules *)
let add_modtype mtb env =
- let mp = mtb.typ_mp in
+ let mp = mtb.mod_mp in
let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in
let new_globals = { env.env_globals with env_modtypes = new_modtypes } in
{ env with env_globals = new_globals }
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 7a9b12c43..39dfa9aa3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -43,8 +43,8 @@ let split_struc k m struc =
| h::tail -> split (h::rev_before) tail
in split [] struc
-let discr_resolver mtb = match mtb.typ_expr with
- | NoFunctor _ -> mtb.typ_delta
+let discr_resolver mtb = match mtb.mod_type with
+ | NoFunctor _ -> mtb.mod_delta
| MoreFunctor _ -> empty_delta_resolver
let rec rebuild_mp mp l =
@@ -233,7 +233,7 @@ let rec translate_mse env mpo inl = function
mb.mod_type, mb.mod_delta
|None ->
let mtb = lookup_modtype mp1 env in
- mtb.typ_expr, mtb.typ_delta
+ mtb.mod_type, mtb.mod_delta
in
sign,Some (MEident mp1),reso,Univ.Constraint.empty
|MEapply (fe,mp1) ->
@@ -259,6 +259,17 @@ let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
| Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
| _ -> None
+let mk_mod mp e ty ty' cst reso =
+ { mod_mp = mp;
+ mod_expr = e;
+ mod_type = ty;
+ mod_type_alg = ty';
+ mod_constraints = cst;
+ mod_delta = reso;
+ mod_retroknowledge = [] }
+
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+
let rec translate_mse_funct env mpo inl mse = function
|[] ->
let sign,alg,reso,cst = translate_mse env mpo inl mse in
@@ -269,19 +280,13 @@ let rec translate_mse_funct env mpo inl mse = function
let env' = add_module_type mp_id mtb env in
let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
let alg' = mk_alg_funct mpo mbid mtb alg in
- MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.typ_constraints
+ MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
and translate_modtype env mp inl (params,mte) =
let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
- let mtb =
- { typ_mp = mp_from_mexpr mte;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = cst;
- typ_delta = reso }
- in
+ let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
let mtb' = subst_modtype_and_resolver mtb mp in
- { mtb' with typ_expr_alg = alg }
+ { mtb' with mod_type_alg = alg }
(** [finalize_module] :
from an already-translated (or interactive) implementation
@@ -290,30 +295,16 @@ and translate_modtype env mp inl (params,mte) =
let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
|None ->
let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
- { mod_mp = mp;
- mod_expr = impl;
- mod_type = sign;
- mod_type_alg = None;
- mod_constraints = cst;
- mod_delta = reso;
- mod_retroknowledge = [] }
+ mk_mod mp impl sign None cst reso
|Some (params_mte,inl) ->
let res_mtb = translate_modtype env mp inl params_mte in
- let auto_mtb = {
- typ_mp = mp;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = Univ.Constraint.empty;
- typ_delta = reso } in
+ let auto_mtb = mk_modtype mp sign Univ.Constraint.empty reso in
let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
- { mod_mp = mp;
+ { res_mtb with
+ mod_mp = mp;
mod_expr = impl;
- mod_type = res_mtb.typ_expr;
- mod_type_alg = res_mtb.typ_expr_alg;
- mod_constraints = cst +++ cst';
- mod_delta = res_mtb.typ_delta;
- mod_retroknowledge = [] }
+ mod_constraints = cst +++ cst' }
let translate_module env mp inl = function
|MType (params,ty) ->
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 21171705d..2e629a3b5 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -12,11 +12,7 @@ open Entries
open Mod_subst
open Names
-(** Main functions for translating module entries
-
- Note : [module_body] and [module_type_body] obtained this way
- won't have any [MEstruct] in their algebraic fields.
-*)
+(** Main functions for translating module entries *)
val translate_module :
env -> module_path -> inline -> module_entry -> module_body
@@ -31,7 +27,6 @@ val translate_modtype :
- The second output is the algebraic expression, kept for the extraction.
It is never None when translating to a module, but for module type
it could not be contain applications or functors.
- Moreover algebraic expressions obtained here cannot contain [MEstruct].
*)
type 'alg translation =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 05eac6221..dcf026caf 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -145,20 +145,11 @@ let rec functor_iter fty f0 = function
(** {6 Misc operations } *)
let module_type_of_module mb =
- { typ_mp = mb.mod_mp;
- typ_expr = mb.mod_type;
- typ_expr_alg = None;
- typ_constraints = mb.mod_constraints;
- typ_delta = mb.mod_delta }
+ { mb with mod_expr = Abstract; mod_type_alg = None }
let module_body_of_type mp mtb =
- { mod_mp = mp;
- mod_type = mtb.typ_expr;
- mod_type_alg = mtb.typ_expr_alg;
- mod_expr = Abstract;
- mod_constraints = mtb.typ_constraints;
- mod_delta = mtb.typ_delta;
- mod_retroknowledge = [] }
+ assert (mtb.mod_expr == Abstract);
+ { mtb with mod_mp = mp }
let check_modpath_equiv env mp1 mp2 =
if ModPath.equal mp1 mp2 then ()
@@ -182,7 +173,7 @@ let implem_iter fs fa impl = match impl with
let id_delta x y = x
-let rec subst_with_body sub = function
+let subst_with_body sub = function
|WithMod(id,mp) as orig ->
let mp' = subst_mp sub mp in
if mp==mp' then orig else WithMod(id,mp')
@@ -190,26 +181,7 @@ let rec subst_with_body sub = function
let c' = subst_mps sub c in
if c==c' then orig else WithDef(id,c')
-and subst_modtype sub do_delta mtb=
- let { typ_mp = mp; typ_expr = ty; typ_expr_alg = aty } = mtb in
- 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
- let ty' = subst_signature sub do_delta ty in
- let aty' = Option.smartmap (subst_expression sub id_delta) aty in
- let delta' = do_delta mtb.typ_delta sub in
- if mp==mp' && ty==ty' && aty==aty' && delta'==mtb.typ_delta
- then mtb
- else
- { mtb with
- typ_mp = mp';
- typ_expr = ty';
- typ_expr_alg = aty';
- typ_delta = delta' }
-
-and subst_structure sub do_delta sign =
+let rec 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
@@ -226,11 +198,12 @@ and subst_structure sub do_delta sign =
in
List.smartmap subst_body sign
-and subst_module sub do_delta mb =
+and subst_body is_mod sub do_delta mb =
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
+ if ModPath.equal mp mp' then sub
+ else if is_mod && not (is_functor ty) then sub
else add_mp mp mp' empty_delta_resolver sub
in
let ty' = subst_signature sub do_delta ty in
@@ -250,6 +223,10 @@ and subst_module sub do_delta mb =
mod_type_alg = aty';
mod_delta = delta' }
+and subst_module sub do_delta mb = subst_body true sub do_delta mb
+
+and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb
+
and subst_expr sub do_delta seb = match seb with
|MEident mp ->
let mp' = subst_mp sub mp in
@@ -397,19 +374,19 @@ and strengthen_sig mp_from struc mp_to reso = match struc with
let strengthen mtb mp =
(* Has mtb already been strengthened ? *)
- if mp_in_delta mtb.typ_mp mtb.typ_delta then mtb
- else match mtb.typ_expr with
+ if mp_in_delta mtb.mod_mp mtb.mod_delta then mtb
+ else match mtb.mod_type with
|NoFunctor struc ->
- let reso',struc' = strengthen_sig mtb.typ_mp struc mp mtb.typ_delta in
+ let reso',struc' = strengthen_sig mtb.mod_mp struc mp mtb.mod_delta in
{ mtb with
- typ_expr = NoFunctor struc';
- typ_delta =
- add_delta_resolver mtb.typ_delta
- (add_mp_delta_resolver mtb.typ_mp mp reso') }
+ mod_type = NoFunctor struc';
+ mod_delta =
+ add_delta_resolver mtb.mod_delta
+ (add_mp_delta_resolver mtb.mod_mp mp reso') }
|MoreFunctor _ -> mtb
let inline_delta_resolver env inl mp mbid mtb delta =
- let constants = inline_of_delta inl mtb.typ_delta in
+ let constants = inline_of_delta inl mtb.mod_delta in
let rec make_inline delta = function
| [] -> delta
| (lev,kn)::r ->
@@ -556,9 +533,9 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
subst_module subst do_delta_dom_codom mb
let subst_modtype_and_resolver mtb mp =
- let subst = map_mp mtb.typ_mp mp empty_delta_resolver in
- let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
- let full_subst = map_mp mtb.typ_mp mp new_delta in
+ let subst = map_mp mtb.mod_mp mp empty_delta_resolver in
+ let new_delta = subst_dom_codom_delta_resolver subst mtb.mod_delta in
+ let full_subst = map_mp mtb.mod_mp mp new_delta in
subst_modtype full_subst do_delta_dom_codom mtb
(** {6 Cleaning a module expression from bounded parts }
@@ -585,11 +562,6 @@ let rec clean_module l mb =
if typ==typ' && impl==impl' then mb
else { mb with mod_type=typ'; mod_expr=impl' }
-and clean_modtype l mt =
- let ty = mt.typ_expr in
- let ty' = clean_signature l ty in
- if ty==ty' then mt else { mt with typ_expr=ty' }
-
and clean_field l field = match field with
|(lab,SFBmodule mb) ->
let mb' = clean_module l mb in
@@ -599,10 +571,10 @@ and clean_field l field = match field with
and clean_structure l = List.smartmap (clean_field l)
and clean_signature l =
- functor_smartmap (clean_modtype l) (clean_structure l)
+ functor_smartmap (clean_module l) (clean_structure l)
and clean_expression l =
- functor_smartmap (clean_modtype l) (fun me -> me)
+ functor_smartmap (clean_module l) (fun me -> me)
let rec collect_mbid l sign = match sign with
|MoreFunctor (mbid,ty,m) ->
@@ -630,17 +602,13 @@ let join_structure except otab s =
implem_iter join_signature join_expression mb.mod_expr;
Option.iter join_expression mb.mod_type_alg;
join_signature mb.mod_type
- and join_modtype mt =
- Option.iter join_expression mt.typ_expr_alg;
- join_signature mt.typ_expr
and join_field (l,body) = match body with
|SFBconst sb -> join_constant_body except otab sb
|SFBmind _ -> ()
- |SFBmodule m -> join_module m
- |SFBmodtype m -> join_modtype m
+ |SFBmodule m |SFBmodtype m -> join_module m
and join_structure struc = List.iter join_field struc
and join_signature sign =
- functor_iter join_modtype join_structure sign
- and join_expression me = functor_iter join_modtype (fun _ -> ()) me in
+ functor_iter join_module join_structure sign
+ and join_expression me = functor_iter join_module (fun _ -> ()) me in
join_structure s
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index f33e1eaa6..ddd795917 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -47,13 +47,13 @@ and translate_field prefix mp env acc (l,x) =
Pp.msg_debug (Pp.str msg));
translate_mod prefix mp env md.mod_type acc
| SFBmodtype mdtyp ->
- let mp = mdtyp.typ_mp in
+ let mp = mdtyp.mod_mp in
(if !Flags.debug then
let msg =
Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
in
Pp.msg_debug (Pp.str msg));
- translate_mod prefix mp env mdtyp.typ_expr acc
+ translate_mod prefix mp env mdtyp.mod_type acc
let dump_library mp dp env mod_expr =
if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index af154afd4..27f94972a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -386,7 +386,7 @@ let constraints_of_sfb env sfb =
match sfb with
| SFBconst cb -> globalize_constant_universes env cb
| SFBmind mib -> globalize_mind_universes mib
- | SFBmodtype mtb -> [Now mtb.typ_constraints]
+ | SFBmodtype mtb -> [Now mtb.mod_constraints]
| SFBmodule mb -> [Now mb.mod_constraints]
(** A generic function for adding a new field in a same environment.
@@ -396,7 +396,7 @@ type generic_name =
| C of constant
| I of mutual_inductive
| M (** name already known, cf the mod_mp field *)
- | MT (** name already known, cf the typ_mp field *)
+ | MT (** name already known, cf the mod_mp field *)
let add_field ((l,sfb) as field) gn senv =
let mlabs,olabs = match sfb with
@@ -494,7 +494,7 @@ let full_add_module mb senv =
{ senv with env = Modops.add_module mb senv.env }
let full_add_module_type mp mt senv =
- let senv = add_constraints (Now mt.typ_constraints) senv in
+ let senv = add_constraints (Now mt.mod_constraints) senv in
{ senv with env = Modops.add_module_type mp mt senv.env }
(** Insertion of modules *)
@@ -548,10 +548,10 @@ let add_module_parameter mbid mte inl senv =
| _ -> assert false
in
let new_paramresolver =
- if Modops.is_functor mtb.typ_expr then senv.paramresolver
- else Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver
+ if Modops.is_functor mtb.mod_type then senv.paramresolver
+ else Mod_subst.add_delta_resolver mtb.mod_delta senv.paramresolver
in
- mtb.typ_delta,
+ mtb.mod_delta,
{ senv with
modvariant = new_variant;
paramresolver = new_paramresolver }
@@ -628,24 +628,27 @@ let end_module l restype senv =
(mp,mbids,mb.mod_delta),
propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv
+let build_mtb mp sign cst delta =
+ { mod_mp = mp;
+ mod_expr = Abstract;
+ mod_type = sign;
+ mod_type_alg = None;
+ mod_constraints = cst;
+ mod_delta = delta;
+ mod_retroknowledge = [] }
+
let end_modtype l senv =
let mp = senv.modpath in
let params, oldsenv = check_sig senv.modvariant in
let () = check_current_label l mp in
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
- let auto_tb = NoFunctor (List.rev senv.revstruct) in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
let newenv = Environ.add_constraints senv.univ newenv in
let newenv = set_engagement_opt newenv senv.engagement in
let senv' = {senv with env=newenv} in
- let mtb =
- { typ_mp = mp;
- typ_expr = functorize params auto_tb;
- typ_expr_alg = None;
- typ_constraints = senv'.univ;
- typ_delta = senv.modresolver }
- in
+ let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
+ let mtb = build_mtb mp auto_tb senv'.univ senv.modresolver in
let newenv = Environ.add_modtype mtb senv'.env in
let newresolver = oldsenv.modresolver in
(mp,mbids),
@@ -662,7 +665,7 @@ let add_include me is_module inl senv =
sign,cst,reso
else
let mtb = translate_modtype senv.env mp_sup inl ([],me) in
- mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
+ mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
in
let senv = add_constraints (Now cst) senv in
(* Include Self support *)
@@ -672,7 +675,7 @@ let add_include me is_module inl senv =
let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
let senv = add_constraints (Now cst_sub) senv in
let mpsup_delta =
- Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
+ Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
in
let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
@@ -680,12 +683,8 @@ let add_include me is_module inl senv =
| str -> resolver,str,senv
in
let resolver,sign,senv =
- let mtb =
- { typ_mp = mp_sup;
- typ_expr = NoFunctor (List.rev senv.revstruct);
- typ_expr_alg = None;
- typ_constraints = Univ.Constraint.empty;
- typ_delta = senv.modresolver } in
+ let struc = NoFunctor (List.rev senv.revstruct) in
+ let mtb = build_mtb mp_sup struc Univ.Constraint.empty senv.modresolver in
compute_sign sign mtb resolver senv
in
let str = match sign with
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 857f577a8..1cf1e8936 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -401,61 +401,61 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
| _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
in
let env =
- add_module_type mtb2.typ_mp mtb2
- (add_module_type mtb1.typ_mp mtb1 env)
+ add_module_type mtb2.mod_mp mtb2
+ (add_module_type mtb1.mod_mp mtb1 env)
in
check_modtypes cst env mtb1 mtb2 subst1 subst2 true
in
List.fold_left check_one_body cst sig2
and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
- if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then cst
+ if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type then cst
else
let rec check_structure cst env str1 str2 equiv subst1 subst2 =
match str1,str2 with
|NoFunctor list1,
NoFunctor list2 ->
if equiv then
- let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
+ let subst2 = add_mp mtb2.mod_mp mtb1.mod_mp mtb1.mod_delta subst2 in
let cst1 = check_signatures cst env
- mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
- mtb1.typ_delta mtb2.typ_delta
+ mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
+ mtb1.mod_delta mtb2.mod_delta
in
let cst2 = check_signatures cst env
- mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
- mtb2.typ_delta mtb1.typ_delta
+ mtb2.mod_mp list2 mtb1.mod_mp list1 subst2 subst1
+ mtb2.mod_delta mtb1.mod_delta
in
Univ.Constraint.union cst1 cst2
else
check_signatures cst env
- mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
- mtb1.typ_delta mtb2.typ_delta
+ mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
+ mtb1.mod_delta mtb2.mod_delta
|MoreFunctor (arg_id1,arg_t1,body_t1),
MoreFunctor (arg_id2,arg_t2,body_t2) ->
let mp2 = MPbound arg_id2 in
- let subst1 = join (map_mbid arg_id1 mp2 arg_t2.typ_delta) subst1 in
+ let subst1 = join (map_mbid arg_id1 mp2 arg_t2.mod_delta) subst1 in
let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in
(* contravariant *)
let env = add_module_type mp2 arg_t2 env in
let env =
if Modops.is_functor body_t1 then env
else add_module
- {mod_mp = mtb1.typ_mp;
+ {mod_mp = mtb1.mod_mp;
mod_expr = Abstract;
mod_type = subst_signature subst1 body_t1;
mod_type_alg = None;
- mod_constraints = mtb1.typ_constraints;
+ mod_constraints = mtb1.mod_constraints;
mod_retroknowledge = [];
- mod_delta = mtb1.typ_delta} env
+ mod_delta = mtb1.mod_delta} env
in
check_structure cst env body_t1 body_t2 equiv subst1 subst2
| _ , _ -> error_incompatible_modtypes mtb1 mtb2
in
- check_structure cst env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
+ check_structure cst env mtb1.mod_type mtb2.mod_type equiv subst1 subst2
let check_subtypes env sup super =
- let env = add_module_type sup.typ_mp sup env in
+ let env = add_module_type sup.mod_mp sup env in
check_modtypes Univ.Constraint.empty env
- (strengthen sup sup.typ_mp) super empty_subst
- (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
+ (strengthen sup sup.mod_mp) super empty_subst
+ (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5c245064f..68cb81f1a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -382,7 +382,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
let type_of_mod mp env = function
|true -> (Environ.lookup_module mp env).mod_type
- |false -> (Environ.lookup_modtype mp env).typ_expr
+ |false -> (Environ.lookup_modtype mp env).mod_type
let rec get_module_path = function
|MEident mp -> mp
@@ -527,7 +527,7 @@ let build_subtypes interp_modast env mp args mtys =
let inl = inl2intopt ann in
let mte,_ = interp_modast env ModType m in
let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in
- { mtb with typ_expr = mk_funct_type env args mtb.typ_expr })
+ { mtb with mod_type = mk_funct_type env args mtb.mod_type })
mtys
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a11d73469..04ce9800a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -213,11 +213,11 @@ let rec extract_structure_spec env mp = function
else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
| (l,SFBmodule mb) :: msig ->
let specs = extract_structure_spec env mp msig in
- let spec = extract_mb_spec env mb.mod_mp mb in
+ let spec = extract_mbody_spec env mb.mod_mp mb in
(l,Smodule spec) :: specs
| (l,SFBmodtype mtb) :: msig ->
let specs = extract_structure_spec env mp msig in
- let spec = extract_mtb_spec env mtb.typ_mp mtb in
+ let spec = extract_mbody_spec env mtb.mod_mp mtb in
(l,Smodtype spec) :: specs
(* From [module_expression] to specifications *)
@@ -248,7 +248,7 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
in
let mp = MPbound mbid in
let env' = Modops.add_module_type mp mtb env in
- MTfunsig (mbid, extract_mtb_spec env mp mtb,
+ MTfunsig (mbid, extract_mbody_spec env mp mtb,
extract_mexpression_spec env' mp1 (me_struct',me_alg'))
| NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
@@ -259,14 +259,10 @@ and extract_msignature_spec env mp1 = function
| MoreFunctor (mbid, mtb, me) ->
let mp = MPbound mbid in
let env' = Modops.add_module_type mp mtb env in
- MTfunsig (mbid, extract_mtb_spec env mp mtb,
+ MTfunsig (mbid, extract_mbody_spec env mp mtb,
extract_msignature_spec env' mp1 me)
-and extract_mtb_spec env mp mtb = match mtb.typ_expr_alg with
- | Some ty -> extract_mexpression_spec env mp (mtb.typ_expr,ty)
- | None -> extract_msignature_spec env mp mtb.typ_expr
-
-and extract_mb_spec env mp mb = match mb.mod_type_alg with
+and extract_mbody_spec env mp mb = match mb.mod_type_alg with
| Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
| None -> extract_msignature_spec env mp mb.mod_type
@@ -319,32 +315,32 @@ let rec extract_structure env mp ~all = function
let ms = extract_structure env mp ~all struc in
let mp = MPdot (mp,l) in
if all || Visit.needed_mp mp then
- (l,SEmodtype (extract_mtb_spec env mp mtb)) :: ms
+ (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms
else ms
(* From [module_expr] and [module_expression] to implementations *)
-and extract_mexpr env mp ~all = function
+and extract_mexpr env mp = function
| MEwith _ -> assert false (* no 'with' syntax for modules *)
| me when lang () != Ocaml ->
(* in Haskell/Scheme, we expand everything *)
- extract_msignature env mp ~all (expand_mexpr env mp me)
+ extract_msignature env mp ~all:true (expand_mexpr env mp me)
| MEident mp ->
if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
Visit.add_mp_all mp; Miniml.MEident mp
| MEapply (me, arg) ->
- Miniml.MEapply (extract_mexpr env mp ~all:true me,
- extract_mexpr env mp ~all:true (MEident arg))
+ Miniml.MEapply (extract_mexpr env mp me,
+ extract_mexpr env mp (MEident arg))
-and extract_mexpression env mp ~all = function
- | NoFunctor me -> extract_mexpr env mp ~all me
+and extract_mexpression env mp = function
+ | NoFunctor me -> extract_mexpr env mp me
| MoreFunctor (mbid, mtb, me) ->
let mp1 = MPbound mbid in
let env' = Modops.add_module_type mp1 mtb env in
Miniml.MEfunctor
(mbid,
- extract_mtb_spec env mp1 mtb,
- extract_mexpression env' mp ~all:true me)
+ extract_mbody_spec env mp1 mtb,
+ extract_mexpression env' mp me)
and extract_msignature env mp ~all = function
| NoFunctor struc ->
@@ -355,7 +351,7 @@ and extract_msignature env mp ~all = function
let env' = Modops.add_module_type mp1 mtb env in
Miniml.MEfunctor
(mbid,
- extract_mtb_spec env mp1 mtb,
+ extract_mbody_spec env mp1 mtb,
extract_msignature env' mp ~all:true me)
and extract_module env mp ~all mb =
@@ -367,15 +363,18 @@ and extract_module env mp ~all mb =
moment we don't support this situation. *)
let impl = match mb.mod_expr with
| Abstract -> error_no_module_expr mp
- | Algebraic me -> extract_mexpression env mp ~all:true me
+ | Algebraic me -> extract_mexpression env mp me
| Struct sign -> extract_msignature env mp ~all:true sign
| FullStruct -> extract_msignature env mp ~all mb.mod_type
in
+ (* Slight optimization: for modules without explicit signatures
+ ([FullStruct] case), we build the type out of the extracted
+ implementation *)
let typ = match mb.mod_expr with
| FullStruct ->
assert (Option.is_empty mb.mod_type_alg);
mtyp_of_mexpr impl
- | _ -> extract_mb_spec env mp mb
+ | _ -> extract_mbody_spec env mp mb
in
{ ml_mod_expr = impl;
ml_mod_type = typ }
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 84d4208f9..6b8bdea40 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -234,12 +234,12 @@ let nametab_register_module_body mp struc =
nametab_register_dir mp;
List.iter (nametab_register_body mp DirPath.empty) struc
-let get_typ_expr_alg mtb = match mtb.typ_expr_alg with
+let get_typ_expr_alg mtb = match mtb.mod_type_alg with
| Some (NoFunctor me) -> me
| _ -> raise Not_found
let nametab_register_modparam mbid mtb =
- match mtb.typ_expr with
+ match mtb.mod_type with
| MoreFunctor _ -> () (* functorial param : nothing to register *)
| NoFunctor struc ->
(* We first try to use the algebraic type expression if any,
@@ -355,9 +355,9 @@ let rec print_expression x =
and print_signature x =
print_functor print_modtype print_structure x
-and print_modtype env mp locals mtb = match mtb.typ_expr_alg with
+and print_modtype env mp locals mtb = match mtb.mod_type_alg with
| Some me -> print_expression true env mp locals me
- | None -> print_signature true env mp locals mtb.typ_expr
+ | None -> print_signature true env mp locals mtb.mod_type
let rec printable_body dir =
let dir = pop_dirpath dir in
@@ -415,9 +415,9 @@ let print_modtype kn =
(keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++
(try
if !short then raise ShortPrinting;
- print_signature' true (Some (Global.env ())) kn mtb.typ_expr
+ print_signature' true (Some (Global.env ())) kn mtb.mod_type
with e when Errors.noncritical e ->
- print_signature' true None kn mtb.typ_expr))
+ print_signature' true None kn mtb.mod_type))
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:38:08 +0000