summaryrefslogtreecommitdiff
path: root/kernel/mod_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_typing.ml')
-rw-r--r--kernel/mod_typing.ml699
1 files changed, 290 insertions, 409 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 55fdf1ab..97c1d1fd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -14,432 +14,313 @@
open Util
open Names
-open Univ
open Declarations
open Entries
open Environ
-open Term_typing
open Modops
-open Subtyping
open Mod_subst
-exception Not_path
-
-let path_of_mexpr = function
- | MSEident mp -> mp
- | _ -> raise Not_path
+type 'alg translation =
+ module_signature * 'alg option * delta_resolver * Univ.constraints
let rec mp_from_mexpr = function
- | MSEident mp -> mp
- | MSEapply (expr,_) -> mp_from_mexpr expr
- | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
- | MSEwith (expr,_) -> mp_from_mexpr expr
+ | MEident mp -> mp
+ | MEapply (expr,_) -> mp_from_mexpr expr
+ | MEwith (expr,_) -> mp_from_mexpr expr
let is_modular = function
| SFBmodule _ | SFBmodtype _ -> true
| SFBconst _ | SFBmind _ -> false
-let rec list_split_assoc ((k,m) as km) rev_before = function
- | [] -> raise Not_found
- | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
- | h::tail -> list_split_assoc km (h::rev_before) tail
+(** Split a [structure_body] at some label corresponding to
+ a modular definition or not. *)
-let discr_resolver env mtb =
- match mtb.typ_expr with
- SEBstruct _ ->
- mtb.typ_delta
- | _ -> (*case mp is a functor *)
- empty_delta_resolver
-
-let rec rebuild_mp mp l =
- match l with
- []-> mp
- | i::r -> rebuild_mp (MPdot(mp,i)) r
-
-let rec check_with env sign with_decl alg_sign mp equiv =
- let sign,wd,equiv,cst= match with_decl with
- | With_Definition (idl,c) ->
- let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
- sign,With_definition_body(idl,cb),equiv,cst
- | With_Module (idl,mp1) ->
- let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
- sign,With_module_body(idl,mp1),equiv,cst
- in
- if alg_sign = None then
- sign,None,equiv,cst
- else
- sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
-
-and check_with_def env sign (idl,c) mp equiv =
- let sig_b = match sign with
- | SEBstruct(sig_b) -> sig_b
- | _ -> error_signature_expected sign
- in
- let id,idl = match idl with
- | [] -> assert false
- | id::idl -> id,idl
- in
- let l = label_of_id id in
- try
- let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
- let before = List.rev rev_before in
- let env' = Modops.add_signature mp before equiv env in
- if idl = [] then
- (* Toplevel definition *)
- let cb = match spec with
- | SFBconst cb -> cb
- | _ -> error_not_a_constant l
- in
- (* In the spirit of subtyping.check_constant, we accept
- any implementations of parameters and opaques terms,
- as long as they have the right type *)
- let def,cst = match cb.const_body with
- | Undef _ | OpaqueDef _ ->
- let (j,cst1) = Typeops.infer env' c in
- let typ = Typeops.type_of_constant_type env' cb.const_type in
- let cst2 = Reduction.conv_leq env' j.uj_type typ in
- let cst =
- union_constraints
- (union_constraints cb.const_constraints cst1)
- cst2
- in
- let def = Def (Declarations.from_val j.uj_val) in
- def,cst
- | Def cs ->
- let cst1 = Reduction.conv env' c (Declarations.force cs) in
- let cst = union_constraints cb.const_constraints cst1 in
- let def = Def (Declarations.from_val c) in
- def,cst
- in
- let cb' =
- { cb with
- const_body = def;
- const_body_code =
- Cemitcodes.from_val (compile_constant_body env' def);
- const_constraints = cst }
- in
- SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
- else
- (* Definition inside a sub-module *)
- let old = match spec with
- | SFBmodule msb -> msb
- | _ -> error_not_a_module (string_of_label l)
- in
- begin
- match old.mod_expr with
- | None ->
- let sign,cb,cst =
- check_with_def env' old.mod_type (idl,c)
- (MPdot(mp,l)) old.mod_delta in
- let new_spec = SFBmodule({old with
- mod_type = sign;
- mod_type_alg = None}) in
- SEBstruct(before@(l,new_spec)::after),cb,cst
- | Some msb ->
- error_generative_module_expected l
- end
- with
- | Not_found -> error_no_such_label l
- | Reduction.NotConvertible -> error_incorrect_with_constraint l
+let split_struc k m struc =
+ let rec split rev_before = function
+ | [] -> raise Not_found
+ | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) ->
+ List.rev rev_before,b,after
+ | h::tail -> split (h::rev_before) tail
+ in split [] struc
-and check_with_mod env sign (idl,mp1) mp equiv =
- let sig_b = match sign with
- | SEBstruct(sig_b) ->sig_b
- | _ -> error_signature_expected sign
- in
- let id,idl = match idl with
- | [] -> assert false
- | id::idl -> id,idl
- in
- let l = label_of_id id in
- try
- let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
- let before = List.rev rev_before in
- let env' = Modops.add_signature mp before equiv env in
- if idl = [] then
- (* Toplevel module definition *)
- let old = match spec with
- SFBmodule msb -> msb
- | _ -> error_not_a_module (string_of_label l)
- in
- let mb_mp1 = (lookup_module mp1 env) in
- let mtb_mp1 =
- module_type_of_module None mb_mp1 in
- let cst =
- match old.mod_expr with
- None ->
- begin
- try union_constraints
- (check_subtypes env' mtb_mp1
- (module_type_of_module None old))
- old.mod_constraints
- with Failure _ -> error_incorrect_with_constraint (label_of_id id)
- end
- | Some (SEBident(mp')) ->
- check_modpath_equiv env' mp1 mp';
- old.mod_constraints
- | _ -> error_generative_module_expected l
- in
- let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false
- in
- let new_spec = SFBmodule {new_mb with
- mod_mp = MPdot(mp,l);
- mod_expr = Some (SEBident mp1);
- mod_constraints = cst} in
- (* we propagate the new equality in the rest of the signature
- with the identity substitution accompagned by the new resolver*)
- let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
- SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
- add_delta_resolver equiv new_mb.mod_delta,cst
- else
- (* Module definition of a sub-module *)
- let old = match spec with
- SFBmodule msb -> msb
- | _ -> error_not_a_module (string_of_label l)
- in
- begin
- match old.mod_expr with
- None ->
- let sign,equiv',cst =
- check_with_mod env'
- old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
- let new_equiv = add_delta_resolver equiv equiv' in
- let new_spec = SFBmodule {old with
- mod_type = sign;
- mod_type_alg = None;
- mod_delta = equiv'}
- in
- let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) equiv' in
- SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
- new_equiv,cst
- | Some (SEBident(mp')) ->
- let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
- check_modpath_equiv env' mpnew mp;
- SEBstruct(before@(l,spec)::after)
- ,equiv,empty_constraint
- | _ ->
- error_generative_module_expected l
- end
- with
- Not_found -> error_no_such_label l
- | Reduction.NotConvertible -> error_incorrect_with_constraint l
+let discr_resolver mtb = match mtb.mod_type with
+ | NoFunctor _ -> mtb.mod_delta
+ | MoreFunctor _ -> empty_delta_resolver
-and translate_module env mp inl me =
- match me.mod_entry_expr, me.mod_entry_type with
- | None, None ->
- anomaly "Mod_typing.translate_module: empty type and expr in module entry"
- | None, Some mte ->
- let mtb = translate_module_type env mp inl mte in
- { mod_mp = mp;
- mod_expr = None;
- mod_type = mtb.typ_expr;
- mod_type_alg = mtb.typ_expr_alg;
- mod_delta = mtb.typ_delta;
- mod_constraints = mtb.typ_constraints;
- mod_retroknowledge = []}
- | Some mexpr, _ ->
- let sign,alg_implem,resolver,cst1 =
- translate_struct_module_entry env mp inl mexpr in
- let sign,alg1,resolver,cst2 =
- match me.mod_entry_type with
- | None ->
- sign,None,resolver,empty_constraint
- | Some mte ->
- let mtb = translate_module_type env mp inl mte in
- let cst = check_subtypes env
- {typ_mp = mp;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = empty_constraint;
- typ_delta = resolver;}
- mtb
- in
- mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst
- in
- { mod_mp = mp;
- mod_type = sign;
- mod_expr = alg_implem;
- mod_type_alg = alg1;
- mod_constraints = Univ.union_constraints cst1 cst2;
- mod_delta = resolver;
- 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
- fix the bug.*)
+let rec rebuild_mp mp l =
+ match l with
+ | []-> mp
+ | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
-and translate_apply env inl ftrans mexpr mkalg =
- let sign,alg,resolver,cst1 = ftrans in
- let farg_id, farg_b, fbody_b = destr_functor env sign in
- let mp1 =
- try path_of_mexpr mexpr
- with Not_path -> error_application_to_not_path mexpr
- in
- let mtb = module_type_of_module None (lookup_module mp1 env) in
- let cst2 = check_subtypes env mtb farg_b in
- let mp_delta = discr_resolver env mtb in
- let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
- let subst = map_mbid farg_id mp1 mp_delta
- in
- subst_struct_expr subst fbody_b,
- mkalg alg mp1 cst2,
- subst_codom_delta_resolver subst resolver,
- Univ.union_constraints cst1 cst2
+let (+++) = Univ.Constraint.union
-and translate_functor env inl arg_id arg_e trans mkalg =
- let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
- let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
- let sign,alg,resolver,cst = trans env'
+let rec check_with_def env struc (idl,c) mp equiv =
+ let lab,idl = match idl with
+ | [] -> assert false
+ | id::idl -> Label.of_id id, idl
in
- SEBfunctor (arg_id, mtb, sign),
- mkalg alg arg_id mtb,
- resolver,
- Univ.union_constraints cst mtb.typ_constraints
-
-and translate_struct_module_entry env mp inl = function
- | MSEident mp1 ->
- let mb = lookup_module mp1 env in
- let mb' = strengthen_and_subst_mb mb mp false in
- mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
- | MSEfunctor (arg_id, arg_e, body_expr) ->
- let trans env' = translate_struct_module_entry env' mp inl body_expr in
- let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in
- translate_functor env inl arg_id arg_e trans mkalg
- | MSEapply (fexpr,mexpr) ->
- let trans = translate_struct_module_entry env mp inl fexpr in
- let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in
- translate_apply env inl trans mexpr mkalg
- | MSEwith(mte, with_decl) ->
- let sign,alg,resolve,cst1 =
- translate_struct_module_entry env mp inl mte in
- let sign,alg,resolve,cst2 =
- check_with env sign with_decl alg mp resolve in
- sign,alg,resolve,Univ.union_constraints cst1 cst2
-
-and translate_struct_type_entry env inl = function
- | MSEident mp1 ->
- let mtb = lookup_modtype mp1 env in
- mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint
- | MSEfunctor (arg_id, arg_e, body_expr) ->
- let trans env' = translate_struct_type_entry env' inl body_expr in
- translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None)
- | MSEapply (fexpr,mexpr) ->
- let trans = translate_struct_type_entry env inl fexpr in
- translate_apply env inl trans mexpr (fun _ _ _ -> None)
- | MSEwith(mte, with_decl) ->
- let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in
- let sign,alg,resolve,cst2 =
- check_with env sign with_decl alg (mp_from_mexpr mte) resolve
+ try
+ let modular = not (List.is_empty idl) in
+ let before,spec,after = split_struc lab modular struc in
+ let env' = Modops.add_structure mp before equiv env in
+ if List.is_empty idl then
+ (* Toplevel definition *)
+ let cb = match spec with
+ | SFBconst cb -> cb
+ | _ -> error_not_a_constant lab
in
- sign,alg,resolve,Univ.union_constraints cst1 cst2
-
-and translate_module_type env mp inl mte =
- let mp_from = mp_from_mexpr mte in
- let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in
- let mtb = subst_modtype_and_resolver
- {typ_mp = mp_from;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = cst;
- typ_delta = resolve} mp
- in {mtb with typ_expr_alg = alg}
-
-let rec translate_struct_include_module_entry env mp inl = function
- | MSEident mp1 ->
- let mb = lookup_module mp1 env in
- let mb' = strengthen_and_subst_mb mb mp true in
- let mb_typ = clean_bounded_mod_expr mb'.mod_type in
- mb_typ,None,mb'.mod_delta,Univ.empty_constraint
- | MSEapply (fexpr,mexpr) ->
- let ftrans = translate_struct_include_module_entry env mp inl fexpr in
- translate_apply env inl ftrans mexpr (fun _ _ _ -> None)
- | _ -> error ("You cannot Include a high-order structure.")
-
-let rec add_struct_expr_constraints env = function
- | SEBident _ -> env
-
- | SEBfunctor (_,mtb,meb) ->
- add_struct_expr_constraints
- (add_modtype_constraints env mtb) meb
-
- | SEBstruct (structure_body) ->
- List.fold_left
- (fun env (_,item) -> add_struct_elem_constraints env item)
- env
- structure_body
-
- | SEBapply (meb1,meb2,cst) ->
- Environ.add_constraints cst
- (add_struct_expr_constraints
- (add_struct_expr_constraints env meb1)
- meb2)
- | SEBwith(meb,With_definition_body(_,cb))->
- Environ.add_constraints cb.const_constraints
- (add_struct_expr_constraints env meb)
- | SEBwith(meb,With_module_body(_,_))->
- add_struct_expr_constraints env meb
-
-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
- | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb =
- let env = match mb.mod_expr with
- | None -> env
- | Some meb -> add_struct_expr_constraints env meb
- in
- let env =
- add_struct_expr_constraints env mb.mod_type
+ (* In the spirit of subtyping.check_constant, we accept
+ any implementations of parameters and opaques terms,
+ as long as they have the right type *)
+ let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
+ let env' = Environ.add_constraints ccst env' in
+ let c',cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let cst = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ j.uj_val,cst
+ | Def cs ->
+ let cst = Reduction.infer_conv env' (Environ.universes env') c
+ (Mod_subst.force_constr cs) in
+ let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
+ if cb.const_polymorphic then cst
+ else ccst +++ cst
+ in
+ c, cst
+ in
+ let def = Def (Mod_subst.from_val c') in
+ let cb' =
+ { cb with
+ const_body = def;
+ const_body_code = Cemitcodes.from_val (compile_constant_body env' def) }
+ (* const_universes = Future.from_val cst } *)
+ in
+ before@(lab,SFBconst(cb'))::after, c', cst
+ else
+ (* Definition inside a sub-module *)
+ let mb = match spec with
+ | SFBmodule mb -> mb
+ | _ -> error_not_a_module (Label.to_string lab)
+ in
+ begin match mb.mod_expr with
+ | Abstract ->
+ let struc = Modops.destr_nofunctor mb.mod_type in
+ let struc',c',cst =
+ check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
+ in
+ let mb' = { mb with
+ mod_type = NoFunctor struc';
+ mod_type_alg = None }
+ in
+ before@(lab,SFBmodule mb')::after, c', cst
+ | _ -> error_generative_module_expected lab
+ end
+ with
+ | Not_found -> error_no_such_label lab
+ | Reduction.NotConvertible -> error_incorrect_with_constraint lab
+
+let rec check_with_mod env struc (idl,mp1) mp equiv =
+ let lab,idl = match idl with
+ | [] -> assert false
+ | id::idl -> Label.of_id id, idl
in
- Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb =
- Environ.add_constraints mtb.typ_constraints
- (add_struct_expr_constraints env mtb.typ_expr)
-
-
-let rec struct_expr_constraints cst = function
- | SEBident _ -> cst
-
- | SEBfunctor (_,mtb,meb) ->
- struct_expr_constraints
- (modtype_constraints cst mtb) meb
-
- | SEBstruct (structure_body) ->
- List.fold_left
- (fun cst (_,item) -> struct_elem_constraints cst item)
- cst
- structure_body
-
- | SEBapply (meb1,meb2,cst1) ->
- struct_expr_constraints
- (struct_expr_constraints (Univ.union_constraints cst1 cst) meb1)
- meb2
- | SEBwith(meb,With_definition_body(_,cb))->
- struct_expr_constraints
- (Univ.union_constraints cb.const_constraints cst) meb
- | SEBwith(meb,With_module_body(_,_))->
- struct_expr_constraints cst meb
-
-and struct_elem_constraints cst = function
- | SFBconst cb -> cst
- | SFBmind mib -> cst
- | SFBmodule mb -> module_constraints cst mb
- | SFBmodtype mtb -> modtype_constraints cst mtb
-
-and module_constraints cst mb =
- let cst = match mb.mod_expr with
- | None -> cst
- | Some meb -> struct_expr_constraints cst meb in
- let cst =
- struct_expr_constraints cst mb.mod_type in
- Univ.union_constraints mb.mod_constraints cst
-
-and modtype_constraints cst mtb =
- struct_expr_constraints (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr
-
-
-let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
-let module_constraints = module_constraints Univ.empty_constraint
+ try
+ let before,spec,after = split_struc lab true struc in
+ let env' = Modops.add_structure mp before equiv env in
+ let old = match spec with
+ | SFBmodule mb -> mb
+ | _ -> error_not_a_module (Label.to_string lab)
+ in
+ if List.is_empty idl then
+ (* Toplevel module definition *)
+ let mb_mp1 = lookup_module mp1 env in
+ let mtb_mp1 = module_type_of_module mb_mp1 in
+ let cst = match old.mod_expr with
+ | Abstract ->
+ begin
+ try
+ let mtb_old = module_type_of_module old in
+ Subtyping.check_subtypes env' mtb_mp1 mtb_old
+ +++ old.mod_constraints
+ with Failure _ -> error_incorrect_with_constraint lab
+ end
+ | Algebraic (NoFunctor (MEident(mp'))) ->
+ check_modpath_equiv env' mp1 mp';
+ old.mod_constraints
+ | _ -> error_generative_module_expected lab
+ in
+ let mp' = MPdot (mp,lab) in
+ let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
+ let new_mb' =
+ { new_mb with
+ mod_mp = mp';
+ mod_expr = Algebraic (NoFunctor (MEident mp1));
+ mod_constraints = cst }
+ in
+ let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
+ (* we propagate the new equality in the rest of the signature
+ with the identity substitution accompagned by the new resolver*)
+ let id_subst = map_mp mp' mp' new_mb.mod_delta in
+ let new_after = subst_structure id_subst after in
+ before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
+ else
+ (* Module definition of a sub-module *)
+ let mp' = MPdot (mp,lab) in
+ let old = match spec with
+ | SFBmodule msb -> msb
+ | _ -> error_not_a_module (Label.to_string lab)
+ in
+ begin match old.mod_expr with
+ | Abstract ->
+ let struc = destr_nofunctor old.mod_type in
+ let struc',equiv',cst =
+ check_with_mod env' struc (idl,mp1) mp' old.mod_delta
+ in
+ let new_mb =
+ { old with
+ mod_type = NoFunctor struc';
+ mod_type_alg = None;
+ mod_delta = equiv' }
+ in
+ let new_equiv = add_delta_resolver equiv equiv' in
+ let id_subst = map_mp mp' mp' equiv' in
+ let new_after = subst_structure id_subst after in
+ before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
+ | Algebraic (NoFunctor (MEident mp0)) ->
+ let mpnew = rebuild_mp mp0 idl in
+ check_modpath_equiv env' mpnew mp;
+ before@(lab,spec)::after, equiv, Univ.Constraint.empty
+ | _ -> error_generative_module_expected lab
+ end
+ with
+ | Not_found -> error_no_such_label lab
+ | Reduction.NotConvertible -> error_incorrect_with_constraint lab
+
+let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
+
+let check_with env mp (sign,alg,reso,cst) = function
+ |WithDef(idl,c) ->
+ let struc = destr_nofunctor sign in
+ let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
+ let alg' = mk_alg_with alg (WithDef (idl,c')) in
+ (NoFunctor struc'),alg',reso, cst+++cst'
+ |WithMod(idl,mp1) as wd ->
+ let struc = destr_nofunctor sign in
+ let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
+ let alg' = mk_alg_with alg wd in
+ (NoFunctor struc'),alg',reso', cst+++cst'
+
+let mk_alg_app mpo alg arg = match mpo, alg with
+ | Some _, Some alg -> Some (MEapply (alg,arg))
+ | _ -> None
+
+(** Translation of a module struct entry :
+ - We translate to a module when a [module_path] is given,
+ otherwise to a module type.
+ - The first output is the expanded signature
+ - 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 [SEBapply] or [SEBfunctor].
+*)
+
+let rec translate_mse env mpo inl = function
+ |MEident mp1 ->
+ let sign,reso = match mpo with
+ |Some mp ->
+ let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
+ mb.mod_type, mb.mod_delta
+ |None ->
+ let mtb = lookup_modtype mp1 env in
+ mtb.mod_type, mtb.mod_delta
+ in
+ sign,Some (MEident mp1),reso,Univ.Constraint.empty
+ |MEapply (fe,mp1) ->
+ translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+ |MEwith(me, with_decl) ->
+ assert (mpo == None); (* No 'with' syntax for modules *)
+ let mp = mp_from_mexpr me in
+ check_with env mp (translate_mse env None inl me) with_decl
+
+and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
+ let farg_id, farg_b, fbody_b = destr_functor sign in
+ let mtb = module_type_of_module (lookup_module mp1 env) in
+ let cst2 = Subtyping.check_subtypes env mtb farg_b in
+ let mp_delta = discr_resolver mtb in
+ let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
+ let subst = map_mbid farg_id mp1 mp_delta in
+ let body = subst_signature subst fbody_b in
+ let alg' = mkalg alg mp1 in
+ let reso' = subst_codom_delta_resolver subst reso in
+ body,alg',reso', cst1 +++ cst2
+
+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
+ sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+ |(mbid, ty) :: params ->
+ let mp_id = MPbound mbid in
+ let mtb = translate_modtype env mp_id inl ([],ty) in
+ 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.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 = mk_modtype (mp_from_mexpr mte) sign cst reso in
+ let mtb' = subst_modtype_and_resolver mtb mp in
+ { mtb' with mod_type_alg = alg }
+
+(** [finalize_module] :
+ from an already-translated (or interactive) implementation
+ and a signature entry, produce a final [module_expr] *)
+
+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
+ 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 = 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
+ { res_mtb with
+ mod_mp = mp;
+ mod_expr = impl;
+ mod_constraints = cst +++ cst' }
+
+let translate_module env mp inl = function
+ |MType (params,ty) ->
+ let mtb = translate_modtype env mp inl (params,ty) in
+ module_body_of_type mp mtb
+ |MExpr (params,mse,oty) ->
+ let t = translate_mse_funct env (Some mp) inl mse params in
+ let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
+ finalize_module env mp t restype
+
+let rec translate_mse_incl env mp inl = function
+ |MEident mp1 ->
+ let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
+ let sign = clean_bounded_mod_expr mb.mod_type in
+ sign,None,mb.mod_delta,Univ.Constraint.empty
+ |MEapply (fe,arg) ->
+ let ftrans = translate_mse_incl env mp inl fe in
+ translate_apply env inl ftrans arg (fun _ _ -> None)
+ |_ -> Modops.error_higher_order_include ()