diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/common.ml | 24 | ||||
| -rw-r--r-- | plugins/extraction/haskell.ml | 17 |
2 files changed, 30 insertions, 11 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bde54e1d80..ebaa05b532 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -68,6 +68,12 @@ let rec dottify = function | s::[""] -> s | s::l -> (dottify l)^"."^s +let rec pseudo_qualify up = function + | [] -> assert false + | [s] -> s + | s::[""] -> s + | s::l -> (if up then "" else "_")^(pseudo_qualify true l)^"__"^s + (*s Uppercase/lowercase renamings. *) let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false @@ -303,6 +309,7 @@ and mp_renaming = let ref_renaming_fun (k,r) = let mp = subst_mp (modpath_of_r r) in let l = mp_renaming mp in + let l = if lang () = Haskell && not (modular ()) then [""] else l in let s = if l = [""] (* this happens only at toplevel of the monolithic case *) then @@ -370,7 +377,7 @@ let opened_libraries () = contains the label of the reference to print. Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *) -let pp_gen k mp ls olab = +let pp_ocaml_gen k mp ls olab = try (* what is the largest prefix of [mp] that belongs to [visible]? *) let prefix = common_prefix_from_list mp (get_visible_mps ()) in let delta = mp_length mp - mp_length prefix in @@ -411,6 +418,14 @@ let pp_gen k mp ls olab = error_module_clash base_s else dottify ls +let pp_haskell_gen k mp ls = + if not (modular ()) then List.hd ls + else match List.rev ls with + | [] -> assert false + | s::ls' -> + (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^ + (pseudo_qualify (upperkind k) (List.rev ls')) + let pp_global k r = let ls = ref_renaming (k,r) in assert (List.length ls > 1); @@ -422,9 +437,8 @@ let pp_global k r = (add_visible (k,s); unquote s) else match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) - | Haskell -> if modular () then dottify ls else s - (* for the moment we always qualify in modular Haskell... *) - | Ocaml -> pp_gen k mp ls (Some (label_of_r r)) + | Haskell -> pp_haskell_gen k mp ls + | Ocaml -> pp_ocaml_gen k mp ls (Some (label_of_r r)) (* The next function is used only in Ocaml extraction...*) let pp_module mp = @@ -437,6 +451,6 @@ let pp_module mp = (* we update the visible environment *) let s = List.hd ls in add_visible (Mod,s); s - | _ -> pp_gen Mod mp ls None + | _ -> pp_ocaml_gen Mod mp ls None diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index c1ed62b340..c199225e4c 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -251,7 +251,7 @@ let pp_one_ind ip pl cv = if Array.length cv = 0 then str "= () -- empty inductive" else (v 0 (str "= " ++ - prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor + prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) let rec pp_ind first kn i ind = @@ -311,12 +311,17 @@ let pp_decl = function else hov 0 (pp_function (empty_env ()) e a ++ fnl2 ()) -let pp_structure_elem = function +let rec pp_structure_elem = function | (l,SEdecl d) -> pp_decl d - | (l,SEmodule m) -> - failwith "TODO: Haskell extraction of modules not implemented yet" - | (l,SEmodtype m) -> - failwith "TODO: Haskell 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 + | MEident _ -> failwith "Not Implemented: Module Ident" + | MEfunctor _ -> failwith "Not Implemented: Module Functor" + | MEapply _ -> failwith "Not Implemented: Module Application" let pp_struct = let pp_sel (mp,sel) = |