move more defines out of CoreToLogic

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs

@@ -3,42 +3,12 @@ module Language.Haskell.Liquid.GHC.CoreToLogic where
 coreToLogic :: String
 coreToLogic = unlines
   [ "define GHC.Types.True                   = (true)"
-  , "define GHC.Internal.Real.div x y        = (x / y)"
-  , "define GHC.Internal.Real.mod x y        = (x mod y)"
-  , "define GHC.Internal.Real.fromIntegral x = (x)"
-
   , "define GHC.Classes.not x                = (~ x)"
   , "define GHC.Internal.Base.$ f x          = (f x)"
-  , ""
-  , "define GHC.CString.unpackCString# x = x"
-  , ""
   , "define Main.mempty       = (mempty)"
-  , ""
   , "define Control.Parallel.Strategies.withStrategy s x = (x)"
-  , ""
   , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
-
   , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
   , "define Liquid.ProofCombinators.cast x y = (y)"
   , "define ProofCombinators.cast x y = (y)"
-  , ""
-  , "define Data.Set.Base.singleton x      = (Set_sng x)"
-  , "define Data.Set.Base.union x y        = (Set_cup x y)"
-  , "define Data.Set.Base.intersection x y = (Set_cap x y)"
-  , "define Data.Set.Base.difference x y   = (Set_dif x y)"
-  , "define Data.Set.Base.empty            = (Set_empty 0)"
-  , "define Data.Set.Base.null x           = (Set_emp x)"
-  , "define Data.Set.Base.member x xs      = (Set_mem x xs)"
-  , "define Data.Set.Base.isSubsetOf x y   = (Set_sub x y)"
-  , "define Data.Set.Base.fromList xs      = (listElts xs)"
-  , ""
-  , "define Data.Set.Internal.singleton x      = (Set_sng x)"
-  , "define Data.Set.Internal.union x y        = (Set_cup x y)"
-  , "define Data.Set.Internal.intersection x y = (Set_cap x y)"
-  , "define Data.Set.Internal.difference x y   = (Set_dif x y)"
-  , "define Data.Set.Internal.empty            = (Set_empty 0)"
-  , "define Data.Set.Internal.null x           = (Set_emp x)"
-  , "define Data.Set.Internal.member x xs      = (Set_mem x xs)"
-  , "define Data.Set.Internal.isSubsetOf x y   = (Set_sub x y)"
-  , "define Data.Set.Internal.fromList xs      = (Data.Set_LHAssumptions.listElts xs)"
   ]

src/Data/Set_LHAssumptions.hs

@@ -3,6 +3,7 @@
 module Data.Set_LHAssumptions where
 
 import Data.Set
+import Data.Set.Internal as I
 import GHC.Types_LHAssumptions()
 import Prelude hiding (null)
 
@@ -38,4 +39,24 @@ measure listElts :: [a] -> Set a
   listElts []     = {v | (Set_emp v)}
   listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }
 
+define singleton x      = (Set_sng x)
+define union x y        = (Set_cup x y)
+define intersection x y = (Set_cap x y)
+define difference x y   = (Set_dif x y)
+define empty            = (Set_empty 0)
+define null x           = (Set_emp x)
+define member x xs      = (Set_mem x xs)
+define isSubsetOf x y   = (Set_sub x y)
+define fromList xs      = (Data.Set_LHAssumptions.listElts xs)
+
+define I.singleton x      = (Set_sng x)
+define I.union x y        = (Set_cup x y)
+define I.intersection x y = (Set_cap x y)
+define I.difference x y   = (Set_dif x y)
+define I.empty            = (Set_empty 0)
+define I.null x           = (Set_emp x)
+define I.member x xs      = (Set_mem x xs)
+define I.isSubsetOf x y   = (Set_sub x y)
+define I.fromList xs      = (Data.Set_LHAssumptions.listElts xs)
+
 @-}

src/GHC/CString_LHAssumptions.hs

@@ -14,4 +14,6 @@ _f = unpackCString#
 assume GHC.CString.unpackCString#
   :: x:Addr#
   -> {v:[Char] | v ~~ x && len v == strLen x}
+
+define GHC.CString.unpackCString# x = x
 @-}

src/GHC/Real_LHAssumptions.hs

@@ -46,4 +46,9 @@ class (Real a, Enum a) => Integral a where
 
 //  fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
 //  mod :: x:a -> y:a -> {v:a | v = (x mod y) }
+
+define div x y        = (x / y)
+define mod x y        = (x mod y)
+define fromIntegral x = (x)
+
 @-}