Skip to content

Commit e87dac7

Browse files
Fix uninterpreted functions in keys of Maps and Sets (#2323)
* Prelude.Kore: Export NFData * Kore.Step.Function.Memo: Rename Key to CacheKey * From: Add into * Add instance From [a] (Seq a) * Add Kore.Internal.Key * InternalBytes: Rename fields for uniformity * test: make golden Co-authored-by: ttuegel <ttuegel@users.noreply.github.com> Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com>
1 parent d0412b7 commit e87dac7

File tree

130 files changed

+994
-803
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

130 files changed

+994
-803
lines changed

kore/kore.cabal

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ cabal-version: 2.2
44
--
55
-- see: https://github.com/sol/hpack
66
--
7-
-- hash: 3a3209955e7db4f112e2b2c2ab073b1d479448d68f21f84c4a14ce8f5f2293d9
7+
-- hash: 1eb807e1a58c0a657f51fd08934c8a7e171988a07bcd9e0e4c098055595b6ac4
88

99
name: kore
1010
version: 0.38.0.0
@@ -183,6 +183,7 @@ library
183183
Kore.Internal.InternalMap
184184
Kore.Internal.InternalSet
185185
Kore.Internal.InternalString
186+
Kore.Internal.Key
186187
Kore.Internal.MultiAnd
187188
Kore.Internal.MultiOr
188189
Kore.Internal.NormalizedAc
@@ -962,6 +963,7 @@ test-suite kore-test
962963
Test.Kore.IndexedModule.SortGraph
963964
Test.Kore.Internal.ApplicationSorts
964965
Test.Kore.Internal.Condition
966+
Test.Kore.Internal.Key
965967
Test.Kore.Internal.MultiAnd
966968
Test.Kore.Internal.OrCondition
967969
Test.Kore.Internal.OrPattern

kore/src/Data/Sup.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,6 @@ module Data.Sup
1313

1414
import Prelude.Kore
1515

16-
import Control.DeepSeq
17-
( NFData
18-
)
1916
import Data.Data
2017
( Data
2118
)

kore/src/From.hs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,13 @@ License : NCSA
66

77
module From
88
( From (..)
9+
, into
910
) where
1011

12+
import Data.Sequence
13+
( Seq
14+
)
15+
import qualified Data.Sequence as Seq
1116
import Data.Void
1217

1318
{- | Convert type @from@ into @to@.
@@ -43,8 +48,17 @@ let b = let a :: A = _ in from @_ @B a
4348
class From from to where
4449
from :: from -> to
4550

51+
{- | @into@ is 'from' with the type parameters in reverse order.
52+
-}
53+
into :: forall to from. From from to => from -> to
54+
into = from @from @to
55+
4656
{- | This instance implements the principle /ex falso quodlibet/.
4757
-}
4858
instance From Void any where
4959
from = absurd
5060
{-# INLINE from #-}
61+
62+
instance From [a] (Seq a) where
63+
from = Seq.fromList
64+
{-# INLINE from #-}

kore/src/Kore/Attribute/Attributes.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,6 @@ module Kore.Attribute.Attributes
1717

1818
import Prelude.Kore
1919

20-
import Control.DeepSeq
21-
( NFData
22-
)
2320
import Data.Default
2421
( Default (..)
2522
)

kore/src/Kore/Attribute/Axiom.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,9 +37,6 @@ module Kore.Attribute.Axiom
3737

3838
import Prelude.Kore
3939

40-
import Control.DeepSeq
41-
( NFData
42-
)
4340
import qualified Control.Lens as Lens
4441
import qualified Control.Monad as Monad
4542
import Data.Default

kore/src/Kore/Attribute/Null.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,6 @@ module Kore.Attribute.Null
2121

2222
import Prelude.Kore
2323

24-
import Control.DeepSeq
25-
( NFData
26-
)
2724
import Data.Default
2825
import qualified Generics.SOP as SOP
2926
import qualified GHC.Generics as GHC

kore/src/Kore/Attribute/Parser.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,9 +68,6 @@ module Kore.Attribute.Parser
6868

6969
import Prelude.Kore
7070

71-
import Control.DeepSeq
72-
( NFData
73-
)
7471
import Control.Lens
7572
( Getter
7673
, Iso'

kore/src/Kore/Attribute/Pattern.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,6 @@ module Kore.Attribute.Pattern
2828

2929
import Prelude.Kore
3030

31-
import Control.DeepSeq
32-
( NFData
33-
)
3431
import qualified Control.Lens as Lens
3532
import Data.Generics.Product
3633
import qualified Generics.SOP as SOP

kore/src/Kore/Attribute/Pattern/ConstructorLike.hs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ module Kore.Attribute.Pattern.ConstructorLike
1515

1616
import Prelude.Kore
1717

18-
import Control.DeepSeq
1918
import qualified Generics.SOP as SOP
2019
import qualified GHC.Generics as GHC
2120

kore/src/Kore/Attribute/Pattern/Created.hs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ module Kore.Attribute.Pattern.Created
1111

1212
import Prelude.Kore
1313

14-
import Control.DeepSeq
1514
import qualified Generics.SOP as SOP
1615
import qualified GHC.Generics as GHC
1716
import GHC.Stack

0 commit comments

Comments
 (0)