From ec5455d7351c05a58ae99d5a300dc8576f8c9360 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 4 Dec 2015 18:39:47 +0100 Subject: Extraction: nicer implementation of Implicits Instead of the original hacks (embedding implicits in string msg in MLexn !) we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use of the i-th argument of constant or constructor r when this argument has been declared as implicit. A new option Set/Unset Extraction SafeImplicits controls what happens when some implicits still occur after an extraction : fail in safe mode, or otherwise produce some code nonetheless. This code is probably buggish if the implicits are actually used to do anything relevant (match, function call, etc), but it might also be fine if the implicits are just passed along. And anyway, this unsafe mode could help figure what's going on. Note: the MLdummy now expected a kill_reason, just as Tdummy. These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit. Some minor refactoring on the fly. --- plugins/extraction/haskell.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'plugins/extraction/haskell.ml') diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 37b4142073..530eb2ff89 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -200,8 +200,11 @@ let rec pp_expr par env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "Prelude.error" ++ spc () ++ qs s) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ pp_bracket_comment (str s)) | MLmagic a -> pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") -- cgit v1.2.3 From 123cbdfef1733a1786109bd1b97ccfa3f62c0d1c Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 14 Dec 2015 00:33:29 +0100 Subject: Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase") --- plugins/extraction/haskell.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/extraction/haskell.ml') diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 530eb2ff89..dd66a6a98f 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -334,7 +334,8 @@ let pp_decl = function prvecti (fun i r -> let void = is_inline_custom r || - (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom r) && + match defs.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then mt () else -- cgit v1.2.3 From a2a81cec811a8257e47ceb1b9ea3de6d1c2607ee Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 14 Dec 2015 09:57:50 +0100 Subject: Extraction: also get rid of explicit '\n' for haskell --- plugins/extraction/haskell.ml | 71 ++++++++++++++++++++++--------------------- 1 file changed, 37 insertions(+), 34 deletions(-) (limited to 'plugins/extraction/haskell.ml') diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index dd66a6a98f..00259750d6 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -35,56 +35,59 @@ let keywords = let pp_comment s = str "-- " ++ s ++ fnl () let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}" +(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"], + the '\n' character interacts badly with the Format boxing mechanism *) + let preamble mod_name comment used_modules usf = - let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") + let pp_import mp = str ("import qualified "^ string_of_modfile mp) ++ fnl () in (if not (usf.magic || usf.tunknown) then mt () else str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++ - str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}") - ++ fnl () ++ fnl () + str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}" ++ fnl2 ()) ++ (match comment with | None -> mt () - | Some com -> pp_bracket_comment com ++ fnl () ++ fnl ()) + | Some com -> pp_bracket_comment com ++ fnl2 ()) ++ str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++ str "import qualified Prelude" ++ fnl () ++ - prlist pp_import used_modules ++ fnl () ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ + prlist pp_import used_modules ++ fnl () + ++ (if not (usf.magic || usf.tunknown) then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\nimport qualified GHC.Base\ -\nimport qualified GHC.Prim\ -\n#else\ -\n-- HUGS\ -\nimport qualified IOExts\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "import qualified GHC.Base" ++ fnl () ++ + str "import qualified GHC.Prim" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "import qualified IOExts" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.magic then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\nunsafeCoerce :: a -> b\ -\nunsafeCoerce = GHC.Base.unsafeCoerce#\ -\n#else\ -\n-- HUGS\ -\nunsafeCoerce :: a -> b\ -\nunsafeCoerce = IOExts.unsafeCoerce\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "unsafeCoerce :: a -> b" ++ fnl () ++ + str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "unsafeCoerce :: a -> b" ++ fnl () ++ + str "unsafeCoerce = IOExts.unsafeCoerce" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.tunknown then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\ntype Any = GHC.Prim.Any\ -\n#else\ -\n-- HUGS\ -\ntype Any = ()\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "type Any = ()" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.mldummy then mt () - else str "__ :: any" ++ fnl () ++ - str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) + else + str "__ :: any" ++ fnl () ++ + str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) let pp_abst = function | [] -> (mt ()) @@ -120,7 +123,7 @@ let rec pp_type par vl t = (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy _ -> str "()" | Tunknown -> str "Any" - | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" + | Taxiom -> str "() -- AXIOM TO BE REALIZED" ++ fnl () in hov 0 (pp_rec par t) @@ -323,7 +326,7 @@ let pp_decl = function prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s with Not_found -> prlist (fun id -> pr_id id ++ str " ") l ++ - if t == Taxiom then str "= () -- AXIOM TO BE REALIZED\n" + if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () else str "=" ++ spc () ++ pp_type false l t in hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () -- cgit v1.2.3