File: Extraction_Haskell_String_12258.out

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (80 lines) | stat: -rw-r--r-- 1,807 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
{-# 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
#if __GLASGOW_HASKELL__ >= 900
import qualified GHC.Exts
#endif
#else
-- HUGS
import qualified IOExts
#endif

#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
#if __GLASGOW_HASKELL__ >= 900
unsafeCoerce = GHC.Exts.unsafeCoerce#
#else
unsafeCoerce = GHC.Base.unsafeCoerce#
#endif
#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 ()))