HaskellExtr: Add type annotations to Prelude.==

Also `Export ExtrHaskellBasic` in `ExtrHaskellString`.

Fixes #12257
Fixes #12258

3 files changed, 128 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12257.v b/test-suite/bugs/closed/bug_12257.v
new file mode 100644
index 0000000000..4962048a42
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12257.v
@@ -0,0 +1,3 @@
+(* Test that ExtrHaskellString transitively requires ExtrHaskellBasic *)
+Require Coq.extraction.ExtrHaskellString.
+Import Coq.extraction.ExtrHaskellBasic.
diff --git a/test-suite/output/Extraction_Haskell_String_12258.out b/test-suite/output/Extraction_Haskell_String_12258.out
new file mode 100644
index 0000000000..615abaa3e8
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.out
@@ -0,0 +1,73 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+{- IMPORTANT: If you change this file, make sure that running [cp
+   Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs &&
+   ghc -o test Extraction_Haskell_String_12258.hs] succeeds -}
+
+module Main where
+
+import qualified Prelude
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+#else
+-- HUGS
+import qualified IOExts
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Base.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+data Output_type_code =
+   Ascii_dec
+ | Ascii_eqb
+ | String_dec
+ | String_eqb
+ | Byte_eqb
+ | Byte_eq_dec
+
+type Output_type = Any
+
+output :: Output_type_code -> Output_type
+output c =
+  case c of {
+   Ascii_dec ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+   Ascii_eqb ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+   String_dec ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+   String_eqb ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+   Byte_eqb ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+   Byte_eq_dec ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)}
+
+type Coq__IO a = GHC.Base.IO a
+
+main :: GHC.Base.IO ()
+main =
+   ((Prelude.>>=) (GHC.Base.return output) (\_ -> GHC.Base.return ()))
+
+
diff --git a/test-suite/output/Extraction_Haskell_String_12258.v b/test-suite/output/Extraction_Haskell_String_12258.v
new file mode 100644
index 0000000000..063ff64337
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.v
@@ -0,0 +1,52 @@
+Require Import Coq.extraction.Extraction.
+Require Import Coq.extraction.ExtrHaskellString.
+Extraction Language Haskell.
+Set Extraction File Comment "IMPORTANT: If you change this file, make sure that running [cp Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs && ghc -o test Extraction_Haskell_String_12258.hs] succeeds".
+Inductive output_type_code :=
+| ascii_dec
+| ascii_eqb
+| string_dec
+| string_eqb
+| byte_eqb
+| byte_eq_dec
+.
+
+Definition output_type_sig (c : output_type_code) : { T : Type & T }
+  := existT (fun T => T)
+            _
+            match c return match c with ascii_dec => _ | _ => _ end with
+            | ascii_dec => Ascii.ascii_dec
+            | ascii_eqb => Ascii.eqb
+            | string_dec => String.string_dec
+            | string_eqb => String.eqb
+            | byte_eqb => Byte.eqb
+            | byte_eq_dec => Byte.byte_eq_dec
+            end.
+
+Definition output_type (c : output_type_code)
+  := Eval cbv [output_type_sig projT1 projT2] in
+      projT1 (output_type_sig c).
+Definition output (c : output_type_code) : output_type c
+  := Eval cbv [output_type_sig projT1 projT2] in
+      match c return output_type c with
+      | ascii_dec as c
+      | _ as c
+        => projT2 (output_type_sig c)
+      end.
+
+Axiom IO_unit : Set.
+Axiom _IO : Set -> Set.
+Axiom _IO_bind : forall {A B}, _IO A -> (A -> _IO B) -> _IO B.
+Axiom _IO_return : forall {A : Set}, A -> _IO A.
+Axiom cast_io : _IO unit -> IO_unit.
+Extract Constant _IO "a" => "GHC.Base.IO a".
+Extract Inlined Constant _IO_bind => "(Prelude.>>=)".
+Extract Inlined Constant _IO_return => "GHC.Base.return".
+Extract Inlined Constant IO_unit => "GHC.Base.IO ()".
+Extract Inlined Constant cast_io => "".
+
+Definition main : IO_unit
+  := cast_io (_IO_bind (_IO_return output)
+                       (fun _ => _IO_return tt)).
+
+Recursive Extraction main.