From 4e90d6d144df100d98bff366c2c2c188b375ff12 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 2 Jul 2010 13:36:06 +0000 Subject: Extraction: better support of modules - For Haskell, modules abbreviations and applied functors are expanded. The only remaining sitation that isn't supported is extracting functors and applying them after extraction. - Add a module extraction for Scheme with the same capabilities as for Haskell (with no Extraction Library, though). - Nicer extracted module types (use of the mb.mod_type_alg if present) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13236 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/common.ml | 2 +- plugins/extraction/extract_env.ml | 22 ++++++++++++---------- plugins/extraction/haskell.ml | 7 ++++--- plugins/extraction/scheme.ml | 16 +++++++++++----- 4 files changed, 28 insertions(+), 19 deletions(-) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index afa674e9d..0941ed50f 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -304,7 +304,7 @@ and mp_renaming = let ref_renaming_fun (k,r) = let mp = modpath_of_r r in let l = mp_renaming mp in - let l = if lang () = Haskell && not (modular ()) then [""] else l in + let l = if lang () <> Ocaml && not (modular ()) then [""] else l in let s = if l = [""] (* this happens only at toplevel of the monolithic case *) then diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index a426b2274..2fca8016c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,17 +137,8 @@ let factor_fix env l cb msb = labels, recd, msb'' end -let build_mb mp expr typ_opt = - { mod_mp = mp; - mod_expr = Some expr; - mod_type = typ_opt; - mod_type_alg = None; - mod_constraints = Univ.Constraint.empty; - mod_delta = Mod_subst.empty_delta_resolver; - mod_retroknowledge = [] } - let my_type_of_mb env mb = - mb.mod_type + match mb.mod_type_alg with Some m -> m | None -> mb.mod_type (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) @@ -282,6 +273,17 @@ let rec extract_sfb env mp all = function (* 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 | SEBident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp mp; MEident mp diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 333bdcddd..ce9fab735 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -319,9 +319,10 @@ let rec pp_structure_elem = function and pp_module_expr = function | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel - | MEident _ -> failwith "Not Implemented: Module Ident" - | MEfunctor _ -> failwith "Not Implemented: Module Functor" - | MEapply _ -> failwith "Not Implemented: Module Application" + | MEfunctor _ -> mt () + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) let pp_struct = let pp_sel (mp,sel) = diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 097df6a61..9c600760f 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -180,12 +180,18 @@ let pp_decl = function hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () -let pp_structure_elem = function +let rec pp_structure_elem = function | (l,SEdecl d) -> pp_decl d - | (l,SEmodule m) -> - failwith "TODO: Scheme extraction of modules not implemented yet" - | (l,SEmodtype m) -> - failwith "TODO: Scheme extraction of modules not implemented yet" + | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr + | (l,SEmodtype m) -> mt () + (* for the moment we simply discard module type *) + +and pp_module_expr = function + | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel + | MEfunctor _ -> mt () + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) let pp_struct = let pp_sel (mp,sel) = -- cgit v1.2.3