Skip to content

Commit 04d6b6c

Browse files
ttuegelttuegel
committed
[WIP] Add Kore.Internal.Key
1 parent 3a159d7 commit 04d6b6c

File tree

6 files changed

+202
-12
lines changed

6 files changed

+202
-12
lines changed

‎kore/kore.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,7 @@ library
180180
Kore.Internal.InternalMap
181181
Kore.Internal.InternalSet
182182
Kore.Internal.InternalString
183+
Kore.Internal.Key
183184
Kore.Internal.MultiAnd
184185
Kore.Internal.MultiOr
185186
Kore.Internal.NormalizedAc

‎kore/src/Kore/Builtin/External.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ externalize =
5555
(Syntax.Pattern variable Attribute.Null)
5656
(TermLike variable)
5757
worker termLike =
58+
-- TODO (thomas.tuegel): Make all these cases into classes.
5859
case termLikeF of
5960
InternalBoolF (Const internalBool) ->
6061
(toPatternF . Recursive.project) (Bool.asTermLike internalBool)

‎kore/src/Kore/Builtin/Set/Set.hs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -137,12 +137,13 @@ isSymbolList2set = Builtin.isSymbol list2setKey
137137
isSymbolInclusion :: Symbol -> Bool
138138
isSymbolInclusion = Builtin.isSymbol inclusionKey
139139

140+
-- TODO (thomas.tuegel): Rename this function.
140141
{- | Externalizes a 'Domain.InternalSet' as a 'TermLike'.
141142
-}
142143
asTermLike
143144
:: forall variable
144145
. InternalVariable variable
145-
=> InternalSet (TermLike Concrete) (TermLike variable)
146+
=> InternalSet Key (TermLike variable)
146147
-> TermLike variable
147148
asTermLike builtin =
148149
AssocComm.asTermLike
@@ -177,9 +178,9 @@ asTermLike builtin =
177178
NormalizedAc { opaque } = normalizedAc
178179

179180
concreteElement
180-
:: (TermLike Concrete, SetValue (TermLike variable))
181+
:: (Key, SetValue (TermLike variable))
181182
-> TermLike variable
182-
concreteElement (key, value) = element (TermLike.fromConcrete key, value)
183+
concreteElement (key, value) = element (from @Key key, value)
183184

184185
element
185186
:: (TermLike variable, SetValue (TermLike variable))

‎kore/src/Kore/Internal/Key.hs

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2018
3+
License : NCSA
4+
-}
5+
6+
module Kore.Internal.Key
7+
( Key (..)
8+
, KeyF (..)
9+
) where
10+
11+
import Prelude.Kore
12+
13+
import Data.Functor.Const
14+
( Const
15+
)
16+
import Data.Functor.Foldable
17+
( Base
18+
, Corecursive
19+
, Recursive
20+
)
21+
import qualified Data.Functor.Foldable as Recursive
22+
import qualified Generics.SOP as SOP
23+
import qualified GHC.Generics as GHC
24+
25+
import qualified Kore.Attribute.Pattern as Attribute
26+
( Pattern
27+
)
28+
import Kore.Attribute.Pattern.ConstructorLike
29+
import Kore.Debug
30+
import Kore.Internal.Inj
31+
( Inj
32+
)
33+
import Kore.Internal.InternalBool
34+
( InternalBool
35+
)
36+
import Kore.Internal.InternalInt
37+
( InternalInt
38+
)
39+
import Kore.Internal.InternalString
40+
( InternalString
41+
)
42+
import Kore.Internal.Symbol
43+
( Symbol
44+
)
45+
import Kore.Sort
46+
( Sort
47+
)
48+
import Kore.Syntax.Application
49+
( Application (..)
50+
)
51+
import Kore.Syntax.DomainValue
52+
( DomainValue (..)
53+
)
54+
import Kore.Syntax.Variable
55+
( Concrete
56+
)
57+
import Kore.Unparser
58+
59+
{- | @Key@ is the type of patterns that may be keys of maps and sets.
60+
-}
61+
newtype Key =
62+
Key { getKey :: CofreeF KeyF (Attribute.Pattern Concrete) Key }
63+
deriving (Show)
64+
deriving (GHC.Generic)
65+
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
66+
deriving anyclass (Debug)
67+
68+
type instance Base Key =
69+
CofreeF KeyF (Attribute.Pattern Concrete)
70+
71+
-- This instance implements all class functions for the TermLike newtype
72+
-- because the their implementations for the inner type may be specialized.
73+
instance Recursive Key where
74+
project = getKey
75+
{-# INLINE project #-}
76+
77+
-- This instance implements all class functions for the TermLike newtype
78+
-- because the their implementations for the inner type may be specialized.
79+
instance Corecursive Key where
80+
embed = Key
81+
{-# INLINE embed #-}
82+
83+
instance Diff Key where
84+
diffPrec
85+
key1@(Recursive.project -> attrs1 :< keyF1)
86+
key2@(Recursive.project -> _ :< keyF2)
87+
=
88+
-- If the patterns differ, do not display the difference in the
89+
-- attributes, which would overload the user with redundant information.
90+
diffPrecGeneric
91+
(Recursive.embed (attrs1 :< keyF1))
92+
(Recursive.embed (attrs1 :< keyF2))
93+
<|> diffPrecGeneric key1 key2
94+
95+
{- | This instance ignores the difference in attributes.
96+
-}
97+
instance Eq Key where
98+
(==) (Recursive.project -> _ :< keyF1) (Recursive.project -> _ :< keyF2) =
99+
keyF1 == keyF2
100+
101+
{- | This instance ignores the difference in attributes.
102+
-}
103+
instance Ord Key where
104+
compare
105+
(Recursive.project -> _ :< pat1)
106+
(Recursive.project -> _ :< pat2)
107+
= compare pat1 pat2
108+
109+
{- | This instance ignores the difference in attributes.
110+
-}
111+
instance Hashable Key where
112+
hashWithSalt salt (Recursive.project -> _ :< pat) = hashWithSalt salt pat
113+
{-# INLINE hashWithSalt #-}
114+
115+
instance NFData Key where
116+
rnf (Recursive.project -> annotation :< pat) =
117+
rnf annotation `seq` rnf pat
118+
119+
instance Unparse Key where
120+
unparse (Recursive.project -> _ :< keyF) = unparse keyF
121+
{-# INLINE unparse #-}
122+
123+
unparse2 (Recursive.project -> _ :< keyF) = unparse2 keyF
124+
{-# INLINE unparse2 #-}
125+
126+
instance HasConstructorLike Key where
127+
extractConstructorLike (Recursive.project -> attrs :< _) =
128+
extractConstructorLike attrs
129+
{-# INLINE extractConstructorLike #-}
130+
131+
{- | The base functor of 'Key'; the branching structure of the syntax tree.
132+
-}
133+
data KeyF child
134+
= ApplySymbolF !(Application Symbol child)
135+
| InjF !(Inj child)
136+
| DomainValueF !(DomainValue Sort child)
137+
| InternalBoolF !(Const InternalBool child)
138+
| InternalIntF !(Const InternalInt child)
139+
| InternalStringF !(Const InternalString child)
140+
deriving (Eq, Ord, Show)
141+
deriving (Foldable, Functor, Traversable)
142+
deriving (GHC.Generic)
143+
deriving anyclass (Hashable, NFData)
144+
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
145+
deriving anyclass (Debug, Diff)
146+
147+
instance Unparse child => Unparse (KeyF child) where
148+
unparse = unparseGeneric
149+
unparse2 = unparse2Generic

‎kore/src/Kore/Internal/TermLike.hs

Lines changed: 19 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ module Kore.Internal.TermLike
6060
, mkInternalInt
6161
, mkInternalString
6262
, mkBuiltinList
63+
, Key
6364
, mkBuiltinMap
6465
, mkBuiltinSet
6566
, mkCeil
@@ -205,6 +206,9 @@ import qualified Data.Functor.Foldable as Recursive
205206
import Data.Generics.Product
206207
( field
207208
)
209+
import Data.Map.Strict
210+
( Map
211+
)
208212
import qualified Data.Map.Strict as Map
209213
import Data.Monoid
210214
( Endo (..)
@@ -244,6 +248,9 @@ import Kore.Internal.InternalList
244248
import Kore.Internal.InternalMap
245249
import Kore.Internal.InternalSet
246250
import Kore.Internal.InternalString
251+
import Kore.Internal.Key
252+
( Key
253+
)
247254
import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
248255
( Representation
249256
)
@@ -1094,7 +1101,7 @@ mkBuiltinList = updateCallStack . synthesize . InternalListF
10941101
mkBuiltinMap
10951102
:: HasCallStack
10961103
=> InternalVariable variable
1097-
=> InternalMap (TermLike Concrete) (TermLike variable)
1104+
=> InternalMap Key (TermLike variable)
10981105
-> TermLike variable
10991106
mkBuiltinMap = updateCallStack . synthesize . InternalMapF
11001107

@@ -1103,7 +1110,7 @@ mkBuiltinMap = updateCallStack . synthesize . InternalMapF
11031110
mkBuiltinSet
11041111
:: HasCallStack
11051112
=> InternalVariable variable
1106-
=> InternalSet (TermLike Concrete) (TermLike variable)
1113+
=> InternalSet Key (TermLike variable)
11071114
-> TermLike variable
11081115
mkBuiltinSet = updateCallStack . synthesize . InternalSetF
11091116

@@ -1565,20 +1572,25 @@ mkDefined = worker
15651572
. AcWrapper normalized
15661573
=> Functor (Value normalized)
15671574
=> Functor (Element normalized)
1568-
=> InternalAc (TermLike Concrete) normalized (TermLike variable)
1569-
-> InternalAc (TermLike Concrete) normalized (TermLike variable)
1575+
=> InternalAc Key normalized (TermLike variable)
1576+
-> InternalAc Key normalized (TermLike variable)
15701577
mkDefinedInternalAc internalAc =
15711578
Lens.over (field @"builtinAcChild") mkDefinedNormalized internalAc
15721579
where
1580+
mkDefinedNormalized
1581+
:: normalized Key (TermLike variable)
1582+
-> normalized Key (TermLike variable)
15731583
mkDefinedNormalized =
15741584
unwrapAc
15751585
>>> Lens.over (field @"concreteElements") mkDefinedConcrete
15761586
>>> Lens.over (field @"elementsWithVariables") mkDefinedAbstract
15771587
>>> Lens.over (field @"opaque") mkDefinedOpaque
15781588
>>> wrapAc
1589+
mkDefinedConcrete
1590+
:: Map Key (Value normalized (TermLike variable))
1591+
-> Map Key (Value normalized (TermLike variable))
15791592
mkDefinedConcrete =
15801593
(fmap . fmap) mkDefined
1581-
. Map.mapKeys mkDefined
15821594
mkDefinedAbstract = (fmap . fmap) mkDefined
15831595
mkDefinedOpaque = map mkDefined
15841596

@@ -1764,11 +1776,11 @@ pattern InternalList_
17641776
-> TermLike variable
17651777

17661778
pattern InternalMap_
1767-
:: InternalMap (TermLike Concrete) (TermLike variable)
1779+
:: InternalMap Key (TermLike variable)
17681780
-> TermLike variable
17691781

17701782
pattern InternalSet_
1771-
:: InternalSet (TermLike Concrete) (TermLike variable)
1783+
:: InternalSet Key (TermLike variable)
17721784
-> TermLike variable
17731785

17741786
pattern InternalString_ :: InternalString -> TermLike variable

‎kore/src/Kore/Internal/TermLike/TermLike.hs

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,11 @@ import Kore.Internal.InternalList
8080
import Kore.Internal.InternalMap
8181
import Kore.Internal.InternalSet
8282
import Kore.Internal.InternalString
83+
import Kore.Internal.Key
84+
( Key
85+
, KeyF
86+
)
87+
import qualified Kore.Internal.Key as Key
8388
import Kore.Internal.Symbol hiding
8489
( isConstructorLike
8590
)
@@ -178,6 +183,7 @@ instance {-# OVERLAPS #-} Synthetic Pattern.Defined Defined where
178183
data TermLikeF variable child
179184
= AndF !(And Sort child)
180185
| ApplySymbolF !(Application Symbol child)
186+
-- TODO (thomas.tuegel): Expand aliases during validation?
181187
| ApplyAliasF !(Application (Alias (TermLike VariableName)) child)
182188
| BottomF !(Bottom Sort child)
183189
| CeilF !(Ceil Sort child)
@@ -204,8 +210,8 @@ data TermLikeF variable child
204210
| InternalIntF !(Const InternalInt child)
205211
| InternalStringF !(Const InternalString child)
206212
| InternalListF !(InternalList child)
207-
| InternalMapF !(InternalMap (TermLike Concrete) child)
208-
| InternalSetF !(InternalSet (TermLike Concrete) child)
213+
| InternalMapF !(InternalMap Key child)
214+
| InternalSetF !(InternalSet Key child)
209215
| VariableF !(Const (SomeVariable variable) child)
210216
| EndiannessF !(Const Endianness child)
211217
| SignednessF !(Const Signedness child)
@@ -499,6 +505,15 @@ instance Synthetic Pattern.ConstructorLike (TermLikeF variable) where
499505
InjF inj -> synthetic inj
500506
DefinedF defined -> synthetic defined
501507

508+
instance From (KeyF child) (TermLikeF variable child) where
509+
from (Key.ApplySymbolF app) = ApplySymbolF app
510+
from (Key.InjF inj) = InjF inj
511+
from (Key.DomainValueF domainValue) = DomainValueF domainValue
512+
from (Key.InternalBoolF internalBool) = InternalBoolF internalBool
513+
from (Key.InternalIntF internalInt) = InternalIntF internalInt
514+
from (Key.InternalStringF internalString) = InternalStringF internalString
515+
{-# INLINE from #-}
516+
502517
{- | @TermLike@ is a term-like Kore pattern.
503518
504519
@TermLike@ is the common internal representation of patterns, especially terms.
@@ -685,6 +700,17 @@ instance
685700
from = mapVariables (pure $ from @Concrete)
686701
{-# INLINE from #-}
687702

703+
instance From Key (TermLike variable) where
704+
from = Recursive.unfold worker
705+
where
706+
worker key =
707+
attrs' :< from @(KeyF _) keyF
708+
where
709+
attrs :< keyF = Recursive.project key
710+
attrs' :: Attribute.Pattern variable
711+
attrs' = Attribute.mapVariables (pure coerceVariable) attrs
712+
coerceVariable = from @Concrete @variable
713+
688714
instance
689715
( AstWithLocation variable
690716
, AstWithLocation child

0 commit comments

Comments
 (0)