diff options
| -rw-r--r-- | plugins/extraction/extract_env.ml | 55 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/modutil.mli | 2 |
3 files changed, 38 insertions, 24 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index a10d9904d..a11d73469 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -277,13 +277,13 @@ and extract_mb_spec env mp mb = match mb.mod_type_alg with important: last to first ensures correct dependencies. *) -let rec extract_structure env mp all = function +let rec extract_structure env mp ~all = function | [] -> [] | (l,SFBconst cb) :: struc -> (try let vl,recd,struc = factor_fix env l cb struc in let vc = Array.map (Constant.make2 mp) vl in - let ms = extract_structure env mp all struc in + let ms = extract_structure env mp ~all struc in let b = Array.exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in @@ -291,7 +291,7 @@ let rec extract_structure env mp all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_structure env mp all struc in + let ms = extract_structure env mp ~all struc in let c = Constant.make2 mp l in let b = Visit.needed_con c in if all || b then @@ -300,7 +300,7 @@ let rec extract_structure env mp all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) | (l,SFBmind mib) :: struc -> - let ms = extract_structure env mp all struc in + let ms = extract_structure env mp ~all struc in let mind = MutInd.make2 mp l in let b = Visit.needed_ind mind in if all || b then @@ -309,13 +309,14 @@ let rec extract_structure env mp all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms | (l,SFBmodule mb) :: struc -> - let ms = extract_structure env mp all struc in + let ms = extract_structure env mp ~all struc in let mp = MPdot (mp,l) in - if all || Visit.needed_mp mp then - (l,SEmodule (extract_module env mp true mb)) :: ms + let all' = all || Visit.needed_mp_all mp in + if all' || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp ~all:all' mb)) :: ms else ms | (l,SFBmodtype mtb) :: struc -> - let ms = extract_structure env mp all struc in + 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 @@ -323,41 +324,41 @@ let rec extract_structure env mp all = function (* From [module_expr] and [module_expression] to implementations *) -and extract_mexpr env mp all = function +and extract_mexpr env mp ~all = 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 (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 true me, - extract_mexpr env mp true (MEident arg)) + Miniml.MEapply (extract_mexpr env mp ~all:true me, + extract_mexpr env mp ~all:true (MEident arg)) -and extract_mexpression env mp all = function - | NoFunctor me -> extract_mexpr env mp all me +and extract_mexpression env mp ~all = function + | NoFunctor me -> extract_mexpr env mp ~all 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 true me) + extract_mexpression env' mp ~all:true me) -and extract_msignature env mp all = function +and extract_msignature env mp ~all = function | NoFunctor struc -> let env' = Modops.add_structure mp struc empty_delta_resolver env in - Miniml.MEstruct (mp,extract_structure env' mp all struc) + Miniml.MEstruct (mp,extract_structure env' mp ~all struc) | 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_msignature env' mp true me) + extract_msignature env' mp ~all:true me) -and extract_module env mp all mb = +and extract_module env mp ~all mb = (* A module has an empty [mod_expr] when : - it is a module variable (for instance X inside a Module F [X:SIG]) - it is a module assumption (Declare Module). @@ -366,12 +367,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 me - | Struct sign -> extract_msignature env mp all sign - | FullStruct -> extract_msignature env mp all mb.mod_type + | Algebraic me -> extract_mexpression env mp ~all:true me + | Struct sign -> extract_msignature env mp ~all:true sign + | FullStruct -> extract_msignature env mp ~all mb.mod_type + in + 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 in { ml_mod_expr = impl; - ml_mod_type = extract_mb_spec env mp mb } + ml_mod_type = typ } let mono_environment refs mpl = Visit.reset (); @@ -381,7 +388,7 @@ let mono_environment refs mpl = let l = List.rev (environment_until None) in List.rev_map (fun (mp,struc) -> - mp, extract_structure env mp (Visit.needed_mp_all mp) struc) + mp, extract_structure env mp ~all:(Visit.needed_mp_all mp) struc) l (**************************************) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index e6bcefe22..94f6f52cb 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -197,6 +197,11 @@ let rec msig_of_ms = function let signature_of_structure s = List.map (fun (mp,ms) -> mp,msig_of_ms ms) s +let rec mtyp_of_mexpr = function + | MEfunctor (id,ty,e) -> MTfunsig (id,ty, mtyp_of_mexpr e) + | MEstruct (mp,str) -> MTsig (mp, msig_of_ms str) + | _ -> assert false + (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 88ead482b..d09820c37 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -23,6 +23,8 @@ val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit val signature_of_structure : ml_structure -> ml_signature +val mtyp_of_mexpr : ml_module_expr -> ml_module_type + val msid_of_mt : ml_module_type -> module_path val get_decl_in_structure : global_reference -> ml_structure -> ml_decl |