From b008f8401ec8f3e71e2c8a0d422d3c94f74ea5e6 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 19 Dec 2024 16:27:50 +0100 Subject: [PATCH] move more defines out of CoreToLogic --- .../Haskell/Liquid/GHC/CoreToLogic.hs | 30 ------------------- src/Data/Set_LHAssumptions.hs | 21 +++++++++++++ src/GHC/CString_LHAssumptions.hs | 2 ++ src/GHC/Real_LHAssumptions.hs | 5 ++++ 4 files changed, 28 insertions(+), 30 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs index af3189eab..2a74678fc 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs +++ b/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)" ] diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs index f95db559d..22e7dc97d 100644 --- a/src/Data/Set_LHAssumptions.hs +++ b/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) + @-} diff --git a/src/GHC/CString_LHAssumptions.hs b/src/GHC/CString_LHAssumptions.hs index d41a028b9..0f7ef6f04 100644 --- a/src/GHC/CString_LHAssumptions.hs +++ b/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 @-} diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs index 0e9e1389b..18a05479f 100644 --- a/src/GHC/Real_LHAssumptions.hs +++ b/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) + @-}