edits

# Avoid module name puns, as it confuses Coq’s code extraction
rename module Data.Semigroup.Internal Data.SemigroupInternal

skip module GHC.Arr
skip module GHC.Generics
skip module GHC.Types
skip module GHC.CString
skip module GHC.Classes
skip module GHC.Magic
skip module GHC.IO
skip module GHC.Integer
skip module GHC.Show
skip module Data.Data


## Not yet translated or manually implemented
skip module GHC.Int
skip module GHC.Word
skip module GHC.Integer.Type

## Classes that are generally not interesting
# or where we don’t want any interfaces translated
# automatically
skip class Data.Data.Data
skip class GHC.Show.Show
skip class GHC.Read.Read
skip class GHC.Generics.Generic
skip class GHC.Generics.Generic1
skip class GHC.Exception.Exception
skip class GHC.Arr.Ix
skip class Data.Bits.Bits
skip class Data.Bits.FiniteBits
skip class GHC.Float.Floating
skip class GHC.Real.Fractional
skip class GHC.Real.Integral
skip class GHC.Real.Real
skip class GHC.Real.RealFrac
skip class GHC.Float.RealFloat
skip class Foreign.Storable.Storable
skip class Control.Monad.Fix.MonadFix
skip class GHC.Base.Alternative
skip class GHC.Base.MonadPlus
skip class Control.DeepSeq.NFData
skip class Data.Functor.Classes.Show1
skip class Data.Functor.Classes.Read1
skip class Data.Functor.Classes.Read2
skip class Data.Functor.Classes.Show2
skip class GHC.Exts.IsList

## Classes that we define manually -- we need a better story for this.
skip class GHC.Num.Num
skip class GHC.Enum.Bounded
skip class GHC.Enum.Enum

rename type GHC.IO.FilePath = GHC.Base.String

# Work around the fact that build is higher rank, so the generator
# expects a non-implicit type argument.
rewrite forall g, (GHC.Base.build g) = GHC.Base.build' (fun _ => g)

# Much prettier
rewrite forall f x, (f GHC.Base.$ x) = f x
rewrite forall f x, (f GHC.Base.$! x) = f x

rename type  GHC.Tuple.() = unit
rename value GHC.Tuple.() = tt

rename type GHC.Tuple.(,) = GHC.Tuple.pair_type
rename type GHC.Tuple.(,,) = GHC.Tuple.triple_type
rename type GHC.Tuple.(,,,) = GHC.Tuple.quad_type
rename type GHC.Tuple.(,,,,) = GHC.Tuple.quint_type
rename type GHC.Tuple.(,,,,,) = GHC.Tuple.sext_type
rename type GHC.Tuple.(,,,,,,) = GHC.Tuple.sept_type

rename value GHC.Tuple.(,) = GHC.Tuple.pair2
rename value GHC.Tuple.(,,) = GHC.Tuple.pair3
rename value GHC.Tuple.(,,,) = GHC.Tuple.pair4
rename value GHC.Tuple.(,,,,) = GHC.Tuple.pair5
rename value GHC.Tuple.(,,,,,) = GHC.Tuple.pair6
rename value GHC.Tuple.(,,,,,,) = GHC.Tuple.pair7

rename type  GHC.Types.[]  = list
rename value GHC.Types.[]  = nil
rename value GHC.Types.:   = cons

rename value GHC.Base.++         = Coq.Init.Datatypes.app
rename value GHC.List.concatMap  = Coq.Lists.List.flat_map

rename value GHC.List.foldl      = GHC.Base.foldl
rename value GHC.List.foldl'     = GHC.Base.foldl'

# rename value GHC.Magic.oneShot   = GHC.Base.oneShot
rewrite forall x, GHC.Magic.lazy x = x
#rewrite forall x y, GHC.Prim.seq x y = y
rewrite forall x y, Data.Functor.Utils.hash_compose x y = Coq.Program.Basics.compose x y
rewrite forall x, GHC.Magic.oneShot x = x

rename type GHC.Types.Ordering = comparison
rename value GHC.Types.EQ = Eq
rename value GHC.Types.LT = Lt
rename value GHC.Types.GT = Gt

rename type GHC.Types.* = Type
rename type GHC.Types.Word = GHC.Num.Word
rename type GHC.Types.Int = GHC.Num.Int
rename type GHC.Types.Char = GHC.Char.Char

rename type GHC.Types.Coercible = GHC.Prim.Coercible

rename type  GHC.Classes.Eq = GHC.Base.Eq_
rename value GHC.Classes.== = GHC.Base.op_zeze__
rename value GHC.Classes./= = GHC.Base.op_zsze__

rename type  GHC.Classes.Ord     = GHC.Base.Ord
rename value GHC.Classes.<       = GHC.Base.<
rename value GHC.Classes.<=      = GHC.Base.<=
rename value GHC.Classes.>       = GHC.Base.>
rename value GHC.Classes.>=      = GHC.Base.>=
rename value GHC.Classes.max     = GHC.Base.max
rename value GHC.Classes.min     = GHC.Base.min
rename value GHC.Classes.compare = GHC.Base.compare

rename type  GHC.Types.Bool    = bool
rename value GHC.Types.True    = true
rename value GHC.Types.False   = false
rename value GHC.Classes.not   = negb
rename value GHC.Classes.||    = orb
rename value GHC.Classes.&&    = andb

rename type  GHC.Base.Maybe   = option
rename value GHC.Base.Just    = Some
rename value GHC.Base.Nothing = None

skip method GHC.Base.Monad fail
skip method GHC.Enum.Enum enumFromThen
skip method GHC.Enum.Enum enumFromThenTo
skip method GHC.Base.Semigroup stimes
skip method GHC.Base.Semigroup sconcat

# deprecated
skip method Data.Bits.Bits bitSize

# default definition cannot be used
skip method GHC.Base.Applicative op_zlzt__
skip method Data.Foldable.Foldable elem

# partial methods
skip method Data.Foldable.Foldable foldl1
skip method Data.Foldable.Foldable foldr1
skip method Data.Foldable.Foldable maximum
skip method Data.Foldable.Foldable minimum

# workarounds for partial functions
rewrite forall x y, Data.Foldable.minimum (cons x y) = Data.Foldable.foldr GHC.Base.min x y
rewrite forall x y, Data.Foldable.maximum (cons x y) = Data.Foldable.foldr GHC.Base.max x y
rewrite forall n tys, enumFrom n = (GHC.Enum.enumFromTo n (GHC.List.length tys))  

# add Default constraint
rewrite forall , GHC.List.head = GHC.Err.head


# We do not create notation for constructors yet
# (but it would not be hard)
rename value GHC.Base.:| = GHC.Base.NEcons

# Avoid clashing with Coq’s <> notation
rename value GHC.Base.<> = GHC.Base.<<>>

# Punned constructors
rename value Control.Arrow.ArrowMonad        = Control.Arrow.Mk_ArrowMonad
rename value Control.Arrow.Kleisli           = Control.Arrow.Mk_Kleisli
rename value Data.Foldable.Max               = Data.Foldable.Mk_Max
rename value Data.Foldable.Min               = Data.Foldable.Mk_Min
rename value Data.Functor.Const.Const        = Data.Functor.Const.Mk_Const
rename value Data.Functor.Identity.Identity  = Data.Functor.Identity.Mk_Identity
rename value Data.Semigroup.Internal.All     = Data.SemigroupInternal.Mk_All
rename value Data.Semigroup.Internal.Alt     = Data.SemigroupInternal.Mk_Alt
rename value Data.Semigroup.Internal.Any     = Data.SemigroupInternal.Mk_Any
rename value Data.Semigroup.Internal.Dual    = Data.SemigroupInternal.Mk_Dual
rename value Data.Semigroup.Internal.Endo    = Data.SemigroupInternal.Mk_Endo
rename value Data.Semigroup.Internal.Product = Data.SemigroupInternal.Mk_Product
rename value Data.Semigroup.Internal.Sum     = Data.SemigroupInternal.Mk_Sum
rename value Data.Monoid.First               = Data.Monoid.Mk_First
rename value Data.Monoid.Last                = Data.Monoid.Mk_Last
rename value Data.OldList.SnocBuilder        = Data.OldList.Mk_SnocBuilder
rename value Data.Ord.Down                   = Data.Ord.Mk_Down
rename value Data.Proxy.KProxy               = Data.Proxy.Mk_KProxy
rename value Data.Proxy.Proxy                = Data.Proxy.Mk_Proxy
rename value Data.Semigroup.Arg              = Data.Semigroup.Mk_Arg
rename value Data.Semigroup.First            = Data.Semigroup.Mk_First
rename value Data.Semigroup.Last             = Data.Semigroup.Mk_Last
rename value Data.Semigroup.Max              = Data.Semigroup.Mk_Max
rename value Data.Semigroup.Min              = Data.Semigroup.Mk_Min
rename value Data.Semigroup.Option           = Data.Semigroup.Mk_Option
rename value Data.Traversable.Id             = Data.Traversable.Mk_Id
rename value Data.Traversable.StateL         = Data.Traversable.Mk_StateL
rename value Data.Traversable.StateR         = Data.Traversable.Mk_StateR
rename value Data.Functor.Utils.StateR       = Data.Functor.Utils.Mk_StateR
rename value Data.Functor.Utils.StateL       = Data.Functor.Utils.Mk_StateL
rename value Data.Functor.Utils.Min          = Data.Functor.Utils.Mk_Min
rename value Data.Functor.Utils.Max          = Data.Functor.Utils.Mk_Max
rename value Data.Functor.Compose.Compose    = Data.Functor.Compose.Mk_Compose