Merge pull request #2430 from ucsd-progsys/fd/no-ghc-internal

Eliminate explicit dependency on ghc-internal

Author: facundominguez

liquidhaskell.cabal

@@ -55,14 +55,6 @@ library
                       GHC.ForeignPtr_LHAssumptions
                       GHC.Int_LHAssumptions
                       GHC.IO.Handle_LHAssumptions
-                      GHC.Internal.Base_LHAssumptions
-                      GHC.Internal.Data.Foldable_LHAssumptions
-                      GHC.Internal.Data.Maybe_LHAssumptions
-                      GHC.Internal.Float_LHAssumptions
-                      GHC.Internal.Int_LHAssumptions
-                      GHC.Internal.List_LHAssumptions
-                      GHC.Internal.Num_LHAssumptions
-                      GHC.Internal.Word_LHAssumptions
                       GHC.List_LHAssumptions
                       GHC.Num_LHAssumptions
                       GHC.Num.Integer_LHAssumptions
@@ -89,8 +81,6 @@ library
                       liquidhaskell-boot   == 0.9.10.1,
                       bytestring           == 0.12.1.0,
                       containers           == 0.7,
-                      ghc-bignum,
-                      ghc-internal,
                       ghc-prim
   default-language:   Haskell98
   ghc-options:        -Wall

src/Data/Foldable_LHAssumptions.hs

@@ -1,4 +1,12 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
 module Data.Foldable_LHAssumptions where
 
-import GHC.Internal.Data.Foldable_LHAssumptions()
+import Data.Foldable
+import GHC.Types_LHAssumptions()
+import Prelude hiding (length, null)
+
+{-@
+assume length :: Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}
+assume null   :: Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}
+@-}

src/Data/List_LHAssumptions.hs

@@ -1,4 +1,9 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
 module Data.List_LHAssumptions where
 
-import GHC.Internal.List_LHAssumptions()
+-- TODO: For some reason, the specifications of GHC.List have
+-- a role when verifying functions from Data.List. e.g
+-- basic/pos/AssmReflFilter.hs
+--
+-- Needs to be investigated.
+import GHC.List_LHAssumptions()

src/Data/Maybe_LHAssumptions.hs

@@ -2,4 +2,20 @@
 {-# OPTIONS_GHC -Wno-unused-imports #-}
 module Data.Maybe_LHAssumptions where
 
-import GHC.Internal.Data.Maybe_LHAssumptions
+import Data.Maybe
+import GHC.Types_LHAssumptions ()
+
+{-@
+assume maybe :: v:b -> (a -> b) -> u:(Maybe a) -> {w:b | not (isJust u) => w == v}
+assume isNothing :: v:(Maybe a) -> {b:Bool | not (isJust v) == b}
+assume fromMaybe :: v:a -> u:(Maybe a) -> {x:a | not (isJust u) => x == v}
+
+assume isJust :: v:(Maybe a) -> {b:Bool | b == isJust v}
+measure isJust :: Maybe a -> Bool
+  isJust (Just x)  = true
+  isJust (Nothing) = false
+
+assume fromJust :: {v:(Maybe a) | isJust v} -> a
+measure fromJust :: Maybe a -> a
+  fromJust (Just x) = x
+@-}

src/Data/Word_LHAssumptions.hs

@@ -1,4 +1,4 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
 module Data.Word_LHAssumptions where
 
-import GHC.Internal.Word_LHAssumptions()
+import GHC.Word_LHAssumptions()

src/GHC/Base_LHAssumptions.hs

@@ -1,4 +1,55 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
 module GHC.Base_LHAssumptions where
 
-import GHC.Internal.Base_LHAssumptions()
+import GHC.Base (assert)
+import GHC.CString_LHAssumptions()
+import GHC.Exts_LHAssumptions()
+import GHC.Types_LHAssumptions()
+import Data.Tuple_LHAssumptions()
+
+{-@
+
+assume . :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.
+                   {xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}
+                   (ycmp:b -> c<p ycmp>)
+                -> (zcmp:a -> b<q zcmp>)
+                ->  xcmp:a -> c<r xcmp>
+
+measure autolen :: forall a. a -> Int
+
+//  Useless as compiled into GHC primitive, which is ignored
+assume assert :: {v:Bool | v } -> a -> a
+
+instance measure len :: forall a. [a] -> Int
+  len []     = 0
+  len (y:ys) = 1 + len ys
+
+invariant {v: [a] | len v >= 0 }
+assume map       :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}
+assume ++        :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}
+
+assume $         :: (a -> b) -> a -> b
+assume id        :: x:a -> {v:a | v = x}
+
+qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0))
+qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0))
+
+qualif ListZ(v: [a])          : (len v =  0)
+qualif ListZ(v: [a])          : (len v >= 0)
+qualif ListZ(v: [a])          : (len v >  0)
+
+qualif CmpLen(v:[a], xs:[b])  : (len v  =  len xs )
+qualif CmpLen(v:[a], xs:[b])  : (len v  >= len xs )
+qualif CmpLen(v:[a], xs:[b])  : (len v  >  len xs )
+qualif CmpLen(v:[a], xs:[b])  : (len v  <= len xs )
+qualif CmpLen(v:[a], xs:[b])  : (len v  <  len xs )
+
+qualif EqLen(v:int, xs: [a])  : (v = len xs )
+qualif LenEq(v:[a], x: int)   : (x = len v )
+
+qualif LenDiff(v:[a], x:int)  : (len v  = x + 1)
+qualif LenDiff(v:[a], x:int)  : (len v  = x - 1)
+qualif LenAcc(v:int, xs:[a], n: int): (v = len xs  + n)
+
+@-}

src/GHC/Float_LHAssumptions.hs

@@ -1,5 +1,31 @@
 {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
 {-# OPTIONS_GHC -Wno-unused-imports #-}
-module GHC.Float_LHAssumptions where
+module GHC.Float_LHAssumptions(Floating(..)) where
 
-import GHC.Internal.Float_LHAssumptions
+import GHC.Float
+
+{-@
+class Fractional a => Floating a where
+  pi       :: a
+  exp      :: a -> {y:a | y > 0}
+  log      :: {x:a | x > 0} -> a
+  sqrt     :: {x:a | x >= 0} -> {y:a | y >= 0}
+  (**)     :: x:a -> {y:a | x = 0 => y >= 0} -> a
+  logBase  :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a
+  sin      :: a -> {y:a | -1 <= y && y <= 1}
+  cos      :: a -> {y:a | -1 <= y && y <= 1}
+  tan      :: a -> a
+  asin     :: {x:a | -1 <= x && x <= 1} -> a
+  acos     :: {x:a | -1 <= x && x <= 1} -> a
+  atan     :: a -> a
+  sinh     :: a -> a
+  cosh     :: a -> {y:a | y >= 1}
+  tanh     :: a -> {y:a | -1 < y && y < 1}
+  asinh    :: a -> a
+  acosh    :: {y:a | y >= 1} -> a
+  atanh    :: {y:a | -1 < y && y < 1} -> a
+  log1p    :: a -> a
+  expm1    :: a -> a
+  log1pexp :: a -> a
+  log1mexp :: a -> a
+@-}