diff options
| -rw-r--r-- | plugins/extraction/extract_env.ml | 104 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 16 |
2 files changed, 66 insertions, 54 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3210f2f16..b1195b4be 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,14 +137,42 @@ let factor_fix env l cb msb = labels, recd, msb'' end -let my_type_of_mb env mb = - match mb.mod_type_alg with Some m -> m | None -> mb.mod_type +(** Expanding a [struct_expr_body] into a version without abbreviations + or functor applications. This is done via a detour to entries + (hack proposed by Elie) +*) + +let rec seb2mse = function + | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s') + | SEBident mp -> Entries.MSEident mp + | _ -> failwith "seb2mse: received a non-atomic seb" + +let expand_seb env mp seb = + let seb,_,_,_ = + Mod_typing.translate_struct_module_entry env mp true (seb2mse seb) + in seb + +(** When possible, we use the nicer, shorter, algebraic type structures + instead of the expanded ones. *) + +let my_type_of_mb mb = + let m0 = mb.mod_type in + match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0 + +let my_type_of_mtb mtb = + let m0 = mtb.typ_expr in + match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) -let env_for_mtb_with env mp mtb idl = - let sig_b = match mtb with +let rec msid_of_seb = function + | SEBident mp -> mp + | SEBwith (seb,_) -> msid_of_seb seb + | _ -> assert false + +let env_for_mtb_with env mp seb idl = + let sig_b = match seb with | SEBstruct(sig_b) -> sig_b | _ -> assert false in @@ -172,49 +200,47 @@ let rec extract_sfb_spec env mp = function else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmodule mb) :: msig -> let specs = extract_sfb_spec env mp msig in - let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb env mb) in + let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> let specs = extract_sfb_spec env mp msig in - (l,Smodtype (extract_seb_spec env mtb.typ_mp mtb.typ_expr)) :: specs + let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in + (l,Smodtype spec) :: specs (* From [struct_expr_body] to specifications *) -(* Invariant: the [seb] given to [extract_seb_spec] should either come: - - from a [mod_type] or [type_expr] field - - from the output of [Modops.eval_struct]. +(* Invariant: the [seb] given to [extract_seb_spec] should either come + from a [mod_type] or [type_expr] field, or their [_alg] counterparts. This way, any encountered [SEBident] should be a true module type. - For instance, [my_type_of_mb] ensures this invariant. *) -and extract_seb_spec env mp1 = function +and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with | SEBident mp -> Visit.add_mp mp; MTident mp - | SEBwith(mtb',With_definition_body(idl,cb))-> - let env' = env_for_mtb_with env mp1 mtb' idl in - let mtb''= extract_seb_spec env mp1 mtb' in + | SEBwith(seb',With_definition_body(idl,cb))-> + let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in + let mt = extract_seb_spec env mp1 (seb,seb') in (match extract_with_type env' cb with (* cb peut contenir des kn *) - | None -> mtb'' - | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) - | SEBwith(mtb',With_module_body(idl,mp))-> + | None -> mt + | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) + | SEBwith(seb',With_module_body(idl,mp))-> Visit.add_mp mp; - MTwith(extract_seb_spec env mp1 mtb', + MTwith(extract_seb_spec env mp1 (seb,seb'), ML_With_module(idl,mp)) -(* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre: - | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_)) - when mbid = mbid2 -> extract_seb_spec env m - (* faudrait alors ajouter un test de non-apparition de mbid dans mb *) -*) - | SEBfunctor (mbid, mtb, mtb') -> + | SEBfunctor (mbid, mtb, seb_alg') -> + let seb' = match seb with + | SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb' + | _ -> assert false + in let mp = MPbound mbid in - let env' = Modops.add_module (Modops.module_body_of_type mp mtb) - env in - MTfunsig (mbid, extract_seb_spec env mp mtb.typ_expr, - extract_seb_spec env' mp1 mtb') + let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in + MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb), + extract_seb_spec env' mp1 (seb',seb_alg')) | SEBstruct (msig) -> let env' = Modops.add_signature mp1 msig empty_delta_resolver env in - MTsig (mp1, extract_sfb_spec env' mp1 msig) + MTsig (mp1, extract_sfb_spec env' mp1 msig) | SEBapply _ -> - assert false + if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb) + else assert false @@ -267,23 +293,15 @@ let rec extract_sfb env mp all = function let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then - (l,SEmodtype (extract_seb_spec env mp mtb.typ_expr)) :: ms + (l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms else ms (* From [struct_expr_body] to implementations *) and extract_seb env mp all = function | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml -> - (* in Haskell/Scheme, we expanse everything *) - let rec seb2mse = function - | SEBident mp -> Entries.MSEident mp - | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s') - | _ -> assert false - in - let seb,_,_,_ = - Mod_typing.translate_struct_module_entry env mp true (seb2mse seb) - in - extract_seb env mp all seb + (* in Haskell/Scheme, we expand everything *) + extract_seb env mp all (expand_seb env mp seb) | SEBident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp mp; MEident mp @@ -294,7 +312,7 @@ and extract_seb env mp all = function let mp1 = MPbound mbid in let env' = Modops.add_module (Modops.module_body_of_type mp1 mtb) env in - MEfunctor (mbid, extract_seb_spec env mp1 mtb.typ_expr, + MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb), extract_seb env' mp true meb) | SEBstruct (msb) -> let env' = Modops.add_signature mp msb empty_delta_resolver env in @@ -305,7 +323,7 @@ and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr); - ml_mod_type = extract_seb_spec env mp (my_type_of_mb env mb) } + ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ceb2246ad..baec2eae4 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -646,26 +646,20 @@ and pp_module_type params = function let mp_w = List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) - in + let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in push_visible mp_mt []; - let s = - pp_module_type [] mt ++ str " with type " ++ - pp_global Type r ++ ids - in + let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); - s ++ str "=" ++ spc () ++ pp_type false vl typ + pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_type false vl typ | MTwith(mt,ML_With_module(idl,mp)) -> let mp_mt = msid_of_mt mt in let mp_w = List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl in push_visible mp_mt []; - let s = - pp_module_type [] mt ++ str " with module " ++ pp_modname mp_w - in + let pp_w = str " with module " ++ pp_modname mp_w in pop_visible (); - s ++ str " = " ++ pp_modname mp + pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_modname mp let is_short = function MEident _ | MEapply _ -> true | _ -> false |