From 1c340cc5309cffd91025b3f4960c14f9c383bcdd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 10:56:58 +0000 Subject: [PATCH 1/8] Eliminate GHC.Internal.Float_LHAssumptions and GHC.Internal.Int_LHAssumptions --- liquidhaskell.cabal | 2 -- src/GHC/Float_LHAssumptions.hs | 30 +++++++++++++++++++++-- src/GHC/Internal/Float_LHAssumptions.hs | 32 ------------------------- src/GHC/Internal/Int_LHAssumptions.hs | 12 ---------- 4 files changed, 28 insertions(+), 48 deletions(-) delete mode 100644 src/GHC/Internal/Float_LHAssumptions.hs delete mode 100644 src/GHC/Internal/Int_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 26506d85b2..260e004935 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -58,8 +58,6 @@ library 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 diff --git a/src/GHC/Float_LHAssumptions.hs b/src/GHC/Float_LHAssumptions.hs index 6630622c6d..e9fb1e0445 100644 --- a/src/GHC/Float_LHAssumptions.hs +++ b/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 +@-} diff --git a/src/GHC/Internal/Float_LHAssumptions.hs b/src/GHC/Internal/Float_LHAssumptions.hs deleted file mode 100644 index 515fdb417f..0000000000 --- a/src/GHC/Internal/Float_LHAssumptions.hs +++ /dev/null @@ -1,32 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Float_LHAssumptions(Floating(..)) where - -import GHC.Internal.Float -import GHC.Internal.Real - -{-@ -class (GHC.Internal.Real.Fractional a) => GHC.Internal.Float.Floating a where - GHC.Internal.Float.pi :: a - GHC.Internal.Float.exp :: a -> {y:a | y > 0} - GHC.Internal.Float.log :: {x:a | x > 0} -> a - GHC.Internal.Float.sqrt :: {x:a | x >= 0} -> {y:a | y >= 0} - (GHC.Internal.Float.**) :: x:a -> {y:a | x = 0 => y >= 0} -> a - GHC.Internal.Float.logBase :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a - GHC.Internal.Float.sin :: a -> {y:a | -1 <= y && y <= 1} - GHC.Internal.Float.cos :: a -> {y:a | -1 <= y && y <= 1} - GHC.Internal.Float.tan :: a -> a - GHC.Internal.Float.asin :: {x:a | -1 <= x && x <= 1} -> a - GHC.Internal.Float.acos :: {x:a | -1 <= x && x <= 1} -> a - GHC.Internal.Float.atan :: a -> a - GHC.Internal.Float.sinh :: a -> a - GHC.Internal.Float.cosh :: a -> {y:a | y >= 1} - GHC.Internal.Float.tanh :: a -> {y:a | -1 < y && y < 1} - GHC.Internal.Float.asinh :: a -> a - GHC.Internal.Float.acosh :: {y:a | y >= 1} -> a - GHC.Internal.Float.atanh :: {y:a | -1 < y && y < 1} -> a - GHC.Internal.Float.log1p :: a -> a - GHC.Internal.Float.expm1 :: a -> a - GHC.Internal.Float.log1pexp :: a -> a - GHC.Internal.Float.log1mexp :: a -> a -@-} diff --git a/src/GHC/Internal/Int_LHAssumptions.hs b/src/GHC/Internal/Int_LHAssumptions.hs deleted file mode 100644 index d0ca2d4743..0000000000 --- a/src/GHC/Internal/Int_LHAssumptions.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Int_LHAssumptions where - -import GHC.Internal.Int - -{-@ -embed Int8 as int -embed Int16 as int -embed Int32 as int -embed Int64 as int -@-} From 3f6949335e80af8a68ce8967645d4baa69dc7158 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 10:59:53 +0000 Subject: [PATCH 2/8] Eliminate GHC.Internal.Num_LHAssumptions --- liquidhaskell.cabal | 1 - src/GHC/Internal/Num_LHAssumptions.hs | 19 ------------------- src/GHC/Num_LHAssumptions.hs | 17 ++++++++++++++++- 3 files changed, 16 insertions(+), 21 deletions(-) delete mode 100644 src/GHC/Internal/Num_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 260e004935..b97d1570d8 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -59,7 +59,6 @@ library GHC.Internal.Data.Foldable_LHAssumptions GHC.Internal.Data.Maybe_LHAssumptions GHC.Internal.List_LHAssumptions - GHC.Internal.Num_LHAssumptions GHC.Internal.Word_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions diff --git a/src/GHC/Internal/Num_LHAssumptions.hs b/src/GHC/Internal/Num_LHAssumptions.hs deleted file mode 100644 index 33c233af66..0000000000 --- a/src/GHC/Internal/Num_LHAssumptions.hs +++ /dev/null @@ -1,19 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Num_LHAssumptions where - -import GHC.Internal.Num -import GHC.Num.Integer_LHAssumptions() - -{-@ -assume GHC.Internal.Num.fromInteger :: x:Integer -> {v:a | v = x } - -assume GHC.Internal.Num.negate :: (Num a) - => x:a - -> {v:a | v = -x} - -assume GHC.Internal.Num.abs :: (Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) } - -assume GHC.Internal.Num.+ :: x:a -> y:a -> {v:a | v = x + y } -assume GHC.Internal.Num.- :: (Num a) => x:a -> y:a -> {v:a | v = x - y } -@-} diff --git a/src/GHC/Num_LHAssumptions.hs b/src/GHC/Num_LHAssumptions.hs index 1b31725813..bcb3859a8c 100644 --- a/src/GHC/Num_LHAssumptions.hs +++ b/src/GHC/Num_LHAssumptions.hs @@ -1,4 +1,19 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Num_LHAssumptions where -import GHC.Internal.Num_LHAssumptions() +import GHC.Num +import GHC.Num.Integer_LHAssumptions() + +{-@ +assume fromInteger :: x:Integer -> {v:a | v = x } + +assume negate :: (Num a) + => x:a + -> {v:a | v = -x} + +assume abs :: (Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) } + +assume + :: x:a -> y:a -> {v:a | v = x + y } +assume - :: (Num a) => x:a -> y:a -> {v:a | v = x - y } +@-} From ab8022c943fd91f9f48a873f6781805061b37167 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 11:32:25 +0000 Subject: [PATCH 3/8] Eliminate GHC.Internal.List_LHAssumptions --- liquidhaskell.cabal | 1 - src/Data/List_LHAssumptions.hs | 7 ++- src/GHC/Internal/List_LHAssumptions.hs | 70 -------------------------- src/GHC/List_LHAssumptions.hs | 68 ++++++++++++++++++++++++- 4 files changed, 73 insertions(+), 73 deletions(-) delete mode 100644 src/GHC/Internal/List_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index b97d1570d8..0fbc3b463a 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -58,7 +58,6 @@ library GHC.Internal.Base_LHAssumptions GHC.Internal.Data.Foldable_LHAssumptions GHC.Internal.Data.Maybe_LHAssumptions - GHC.Internal.List_LHAssumptions GHC.Internal.Word_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions diff --git a/src/Data/List_LHAssumptions.hs b/src/Data/List_LHAssumptions.hs index 42bd6933cd..29b35f8e6c 100644 --- a/src/Data/List_LHAssumptions.hs +++ b/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() diff --git a/src/GHC/Internal/List_LHAssumptions.hs b/src/GHC/Internal/List_LHAssumptions.hs deleted file mode 100644 index c3fb5fc466..0000000000 --- a/src/GHC/Internal/List_LHAssumptions.hs +++ /dev/null @@ -1,70 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.List_LHAssumptions where - -import GHC.Internal.List -import GHC.Types_LHAssumptions() -import Prelude hiding (foldr1, length, null) - -{-@ -assume head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs} -assume tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs} - -assume last :: xs:{v: [a] | len v > 0} -> a -assume init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1} -assume null :: xs:[a] -> {v: Bool | ((v) <=> len(xs) = 0) } -assume length :: xs:[a] -> {v: Int | v = len(xs)} -assume filter :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} -assume scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) } -assume scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) } -assume foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a -assume scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) } -assume scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) } - -lazy GHC.Internal.List.iterate -assume iterate :: (a -> a) -> a -> [a] - -assume repeat :: a -> [a] -lazy GHC.Internal.List.repeat - -assume replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n} - -assume cycle :: {v: [a] | len(v) > 0 } -> [a] -lazy GHC.Internal.List.cycle - -assume takeWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} -assume dropWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} - -assume take :: n:Int - -> xs:[a] - -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)} -assume drop :: n:Int - -> xs:[a] - -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))} - -assume splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}> -assume span :: (a -> Bool) - -> xs:[a] - -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))}) - -assume break :: (a -> Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}> - -assume reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)} - -// Copy-pasted from len.hquals -qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys])) -qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys])) - -assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a - - -assume zip :: xs : [a] -> ys:[b] - -> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys))) - && (((len xs) = (len ys)) => ((len v) = (len xs))) )} - -assume zipWith :: (a -> b -> c) - -> xs : [a] -> ys:[b] - -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))} - -assume errorEmptyList :: {v: _ | false} -> a -@-} diff --git a/src/GHC/List_LHAssumptions.hs b/src/GHC/List_LHAssumptions.hs index ad30a0da00..cd59b24ae0 100644 --- a/src/GHC/List_LHAssumptions.hs +++ b/src/GHC/List_LHAssumptions.hs @@ -1,4 +1,70 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.List_LHAssumptions where -import GHC.Internal.List_LHAssumptions() +import GHC.List +import GHC.Types_LHAssumptions() +import Prelude hiding (foldr1, length, null) + +{-@ +assume head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs} +assume tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs} + +assume last :: xs:{v: [a] | len v > 0} -> a +assume init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1} +assume null :: xs:[a] -> {v: Bool | ((v) <=> len(xs) = 0) } +assume length :: xs:[a] -> {v: Int | v = len(xs)} +assume filter :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} +assume scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) } +assume scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) } +assume foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a +assume scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) } +assume scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) } + +lazy iterate +assume iterate :: (a -> a) -> a -> [a] + +assume repeat :: a -> [a] +lazy repeat + +assume replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n} + +assume cycle :: {v: [a] | len(v) > 0 } -> [a] +lazy cycle + +assume takeWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} +assume dropWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} + +assume take :: n:Int + -> xs:[a] + -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)} +assume drop :: n:Int + -> xs:[a] + -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))} + +assume splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}> +assume span :: (a -> Bool) + -> xs:[a] + -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))}) + +assume break :: (a -> Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}> + +assume reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)} + +// Copy-pasted from len.hquals +qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys])) +qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys])) + +assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a + + +assume zip :: xs : [a] -> ys:[b] + -> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys))) + && (((len xs) = (len ys)) => ((len v) = (len xs))) )} + +assume zipWith :: (a -> b -> c) + -> xs : [a] -> ys:[b] + -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))} + +assume errorEmptyList :: {v: _ | false} -> a +@-} From 1c68a5738ba359c9a93276089a7ef141b20c5f4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 11:35:15 +0000 Subject: [PATCH 4/8] Eliminate GHC.Internal.Word_LHAssumptions --- liquidhaskell.cabal | 1 - src/Data/Word_LHAssumptions.hs | 2 +- src/GHC/Internal/Word_LHAssumptions.hs | 16 ---------------- src/GHC/Word_LHAssumptions.hs | 14 +++++++++++++- 4 files changed, 14 insertions(+), 19 deletions(-) delete mode 100644 src/GHC/Internal/Word_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 0fbc3b463a..00bbadd304 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -58,7 +58,6 @@ library GHC.Internal.Base_LHAssumptions GHC.Internal.Data.Foldable_LHAssumptions GHC.Internal.Data.Maybe_LHAssumptions - GHC.Internal.Word_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions GHC.Num.Integer_LHAssumptions diff --git a/src/Data/Word_LHAssumptions.hs b/src/Data/Word_LHAssumptions.hs index c240956964..b7441ee4b2 100644 --- a/src/Data/Word_LHAssumptions.hs +++ b/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() diff --git a/src/GHC/Internal/Word_LHAssumptions.hs b/src/GHC/Internal/Word_LHAssumptions.hs deleted file mode 100644 index 44cf8e6695..0000000000 --- a/src/GHC/Internal/Word_LHAssumptions.hs +++ /dev/null @@ -1,16 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Word_LHAssumptions where - -import GHC.Internal.Word - -{-@ -embed Word as int -embed Word8 as int -embed Word16 as int -embed Word32 as int -embed Word64 as int - -invariant {v : Word32 | 0 <= v } -invariant {v : Word16 | 0 <= v } -@-} diff --git a/src/GHC/Word_LHAssumptions.hs b/src/GHC/Word_LHAssumptions.hs index 2c6fba4139..41228dbf8a 100644 --- a/src/GHC/Word_LHAssumptions.hs +++ b/src/GHC/Word_LHAssumptions.hs @@ -1,4 +1,16 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Word_LHAssumptions where -import GHC.Internal.Word_LHAssumptions() +import GHC.Word + +{-@ +embed Word as int +embed Word8 as int +embed Word16 as int +embed Word32 as int +embed Word64 as int + +invariant {v : Word32 | 0 <= v } +invariant {v : Word16 | 0 <= v } +@-} From 7ea6f00b1c84faf72a55e5e87e3b679b954ab005 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 12:04:46 +0000 Subject: [PATCH 5/8] Eliminate GHC.Internal.Data.Maybe_LHAssumptions --- liquidhaskell.cabal | 1 - src/Data/Maybe_LHAssumptions.hs | 18 +++++++++++++++- src/GHC/Internal/Data/Maybe_LHAssumptions.hs | 22 -------------------- 3 files changed, 17 insertions(+), 24 deletions(-) delete mode 100644 src/GHC/Internal/Data/Maybe_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 00bbadd304..387045efd5 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -57,7 +57,6 @@ library GHC.IO.Handle_LHAssumptions GHC.Internal.Base_LHAssumptions GHC.Internal.Data.Foldable_LHAssumptions - GHC.Internal.Data.Maybe_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions GHC.Num.Integer_LHAssumptions diff --git a/src/Data/Maybe_LHAssumptions.hs b/src/Data/Maybe_LHAssumptions.hs index 0cdb97e810..cf8bafa7b0 100644 --- a/src/Data/Maybe_LHAssumptions.hs +++ b/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 +@-} diff --git a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs b/src/GHC/Internal/Data/Maybe_LHAssumptions.hs deleted file mode 100644 index 80c1771f0e..0000000000 --- a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs +++ /dev/null @@ -1,22 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Data.Maybe_LHAssumptions where - -import GHC.Types_LHAssumptions() -import GHC.Internal.Data.Maybe -import GHC.Internal.Maybe - -{-@ -assume GHC.Internal.Data.Maybe.maybe :: v:b -> (a -> b) -> u:(Maybe a) -> {w:b | not (isJust u) => w == v} -assume GHC.Internal.Data.Maybe.isNothing :: v:(Maybe a) -> {b:Bool | not (isJust v) == b} -assume GHC.Internal.Data.Maybe.fromMaybe :: v:a -> u:(Maybe a) -> {x:a | not (isJust u) => x == v} - -assume GHC.Internal.Data.Maybe.isJust :: v:(Maybe a) -> {b:Bool | b == isJust v} -measure isJust :: Maybe a -> Bool - isJust (Just x) = true - isJust (Nothing) = false - -assume GHC.Internal.Data.Maybe.fromJust :: {v:(Maybe a) | isJust v} -> a -measure fromJust :: Maybe a -> a - fromJust (Just x) = x -@-} From a5efcd68b1c3858e0757ca4f7cd489dcd651a49e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 12:09:46 +0000 Subject: [PATCH 6/8] Eliminate GHC.Internal.Data.Foldable_LHAssumptions --- liquidhaskell.cabal | 1 - src/Data/Foldable_LHAssumptions.hs | 10 +++++++++- src/GHC/Internal/Data/Foldable_LHAssumptions.hs | 11 ----------- 3 files changed, 9 insertions(+), 13 deletions(-) delete mode 100644 src/GHC/Internal/Data/Foldable_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 387045efd5..9e35d7d1ee 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -56,7 +56,6 @@ library GHC.Int_LHAssumptions GHC.IO.Handle_LHAssumptions GHC.Internal.Base_LHAssumptions - GHC.Internal.Data.Foldable_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions GHC.Num.Integer_LHAssumptions diff --git a/src/Data/Foldable_LHAssumptions.hs b/src/Data/Foldable_LHAssumptions.hs index bdc310a44b..d2d936ad29 100644 --- a/src/Data/Foldable_LHAssumptions.hs +++ b/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)} +@-} diff --git a/src/GHC/Internal/Data/Foldable_LHAssumptions.hs b/src/GHC/Internal/Data/Foldable_LHAssumptions.hs deleted file mode 100644 index 771be54c00..0000000000 --- a/src/GHC/Internal/Data/Foldable_LHAssumptions.hs +++ /dev/null @@ -1,11 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Data.Foldable_LHAssumptions where - -import GHC.Internal.Data.Foldable -import GHC.Types_LHAssumptions() - -{-@ -assume GHC.Internal.Data.Foldable.length :: Foldable f => forall a. xs:f a -> {v:Nat | v = len xs} -assume GHC.Internal.Data.Foldable.null :: Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)} -@-} From c1285f4110f9d1dba1f2a3aa0bb4469fcd68f34c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 12:12:05 +0000 Subject: [PATCH 7/8] Eliminate GHC.Internal.Base_LHAssumptions --- liquidhaskell.cabal | 1 - src/GHC/Base_LHAssumptions.hs | 53 ++++++++++++++++++++++++- src/GHC/Internal/Base_LHAssumptions.hs | 55 -------------------------- 3 files changed, 52 insertions(+), 57 deletions(-) delete mode 100644 src/GHC/Internal/Base_LHAssumptions.hs diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 9e35d7d1ee..6b675a9f5f 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -55,7 +55,6 @@ library GHC.ForeignPtr_LHAssumptions GHC.Int_LHAssumptions GHC.IO.Handle_LHAssumptions - GHC.Internal.Base_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions GHC.Num.Integer_LHAssumptions diff --git a/src/GHC/Base_LHAssumptions.hs b/src/GHC/Base_LHAssumptions.hs index 7da1888e87..d648e1ca34 100644 --- a/src/GHC/Base_LHAssumptions.hs +++ b/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

c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. + {xcmp::a, wcmp::b |- c

<: c} + (ycmp:b -> c

) + -> (zcmp:a -> b) + -> xcmp:a -> c + +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) + +@-} diff --git a/src/GHC/Internal/Base_LHAssumptions.hs b/src/GHC/Internal/Base_LHAssumptions.hs deleted file mode 100644 index fb8bbe4ebc..0000000000 --- a/src/GHC/Internal/Base_LHAssumptions.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} -{-# OPTIONS_GHC -Wno-unused-imports #-} -module GHC.Internal.Base_LHAssumptions where - -import GHC.Base (assert) -import GHC.CString_LHAssumptions() -import GHC.Exts_LHAssumptions() -import GHC.Types_LHAssumptions() -import Data.Tuple_LHAssumptions() - -{-@ - -assume . :: forall

c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. - {xcmp::a, wcmp::b |- c

<: c} - (ycmp:b -> c

) - -> (zcmp:a -> b) - -> xcmp:a -> c - -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) - -@-} From cd819b13383626e93952328a5ed6c1f0ff1c9d1b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 8 Nov 2024 12:21:09 +0000 Subject: [PATCH 8/8] Eliminate dependencies on ghc-internal and ghc-bignum --- liquidhaskell.cabal | 2 -- src/GHC/Ptr_LHAssumptions.hs | 16 +++++++------- src/GHC/Real_LHAssumptions.hs | 28 +++++++++++------------- src/Liquid/Prelude/Real_LHAssumptions.hs | 4 +--- 4 files changed, 22 insertions(+), 28 deletions(-) diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 6b675a9f5f..f950f53d4e 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -81,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 diff --git a/src/GHC/Ptr_LHAssumptions.hs b/src/GHC/Ptr_LHAssumptions.hs index 74210fbd53..3ab4fe3e3a 100644 --- a/src/GHC/Ptr_LHAssumptions.hs +++ b/src/GHC/Ptr_LHAssumptions.hs @@ -2,24 +2,24 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Ptr_LHAssumptions where -import GHC.Internal.Ptr +import GHC.Ptr import GHC.Types_LHAssumptions() {-@ -measure pbase :: GHC.Internal.Ptr.Ptr a -> Int -measure plen :: GHC.Internal.Ptr.Ptr a -> Int -measure isNullPtr :: GHC.Internal.Ptr.Ptr a -> Bool +measure pbase :: Ptr a -> Int +measure plen :: Ptr a -> Int +measure isNullPtr :: Ptr a -> Bool type PtrN a N = {v: PtrV a | plen v == N } -type PtrV a = {v: GHC.Internal.Ptr.Ptr a | 0 <= plen v } +type PtrV a = {v: Ptr a | 0 <= plen v } -assume GHC.Internal.Ptr.castPtr :: p:(PtrV a) -> (PtrN b (plen p)) +assume castPtr :: p:(PtrV a) -> (PtrN b (plen p)) -assume GHC.Internal.Ptr.plusPtr :: base:(PtrV a) +assume plusPtr :: base:(PtrV a) -> off:{v:Int | v <= plen base } -> {v:(PtrV b) | pbase v = pbase base && plen v = plen base - off} -assume GHC.Internal.Ptr.minusPtr :: q:(PtrV a) +assume minusPtr :: q:(PtrV a) -> p:{v:(PtrV b) | pbase v == pbase q && plen v >= plen q} -> {v:Nat | v == plen p - plen q} diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs index 49901f66bd..0e9e1389bf 100644 --- a/src/GHC/Real_LHAssumptions.hs +++ b/src/GHC/Real_LHAssumptions.hs @@ -3,9 +3,7 @@ -- Reexports are necessary for LH to expose specs of type classes module GHC.Real_LHAssumptions(Integral(..), Fractional(..)) where -import GHC.Internal.Enum -import GHC.Internal.Num -import GHC.Internal.Real +import GHC.Real import GHC.Types_LHAssumptions() {-@ @@ -13,19 +11,19 @@ assume (^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 & assume fromIntegral :: x:a -> {v:b|v=x} -class (GHC.Internal.Num.Num a) => GHC.Internal.Real.Fractional a where - (GHC.Internal.Real./) :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y} - GHC.Internal.Real.recip :: a -> a - GHC.Internal.Real.fromRational :: GHC.Internal.Real.Ratio Integer -> a +class Num a => Fractional a where + (/) :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y} + recip :: a -> a + fromRational :: Ratio Integer -> a -class (GHC.Internal.Real.Real a, GHC.Internal.Enum.Enum a) => GHC.Internal.Real.Integral a where - GHC.Internal.Real.quot :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) && +class (Real a, Enum a) => Integral a where + quot :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) } - GHC.Internal.Real.rem :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v >= 0) && (v < y))} - GHC.Internal.Real.mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))} + rem :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v >= 0) && (v < y))} + mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))} - GHC.Internal.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = div x y) && + div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = div x y) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) && ((1 < y && x >= 0) => v < x) && @@ -35,16 +33,16 @@ class (GHC.Internal.Real.Real a, GHC.Internal.Enum.Enum a) => GHC.Internal.Real. ((x > 0 && y < 0) => v <= 0) && ((x < 0 && y < 0) => v >= 0) } - GHC.Internal.Real.quotRem :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) && + quotRem :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x)} , {v:a | ((v >= 0) && (v < y))}) - GHC.Internal.Real.divMod :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) && + divMod :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) && ((x >= 0 && y >= 0) => v >= 0) && ((x >= 0 && y >= 1) => v <= x) } , {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))} ) - GHC.Internal.Real.toInteger :: x:a -> {v:Integer | v = x} + toInteger :: x:a -> {v:Integer | v = x} // 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) } diff --git a/src/Liquid/Prelude/Real_LHAssumptions.hs b/src/Liquid/Prelude/Real_LHAssumptions.hs index b316d5a32c..4b304b1ffe 100644 --- a/src/Liquid/Prelude/Real_LHAssumptions.hs +++ b/src/Liquid/Prelude/Real_LHAssumptions.hs @@ -2,8 +2,6 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Liquid.Prelude.Real_LHAssumptions where -import GHC.Internal.Num - {-@ -assume GHC.Internal.Num.* :: Num a => x:a -> y:a -> {v:a | v = x * y} +assume * :: Num a => x:a -> y:a -> {v:a | v = x * y} @-}