Skip to content

Commit f42ad2e

Browse files
ttuegelttuegel
committed
[WIP] Add Kore.Internal.Key
1 parent 097885b commit f42ad2e

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
@@ -58,6 +58,7 @@ externalize =
5858
(Syntax.Pattern variable Attribute.Null)
5959
(TermLike variable)
6060
worker termLike =
61+
-- TODO (thomas.tuegel): Make all these cases into classes.
6162
case termLikeF of
6263
InternalBoolF (Const internalBool) ->
6364
(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
@@ -139,12 +139,13 @@ isSymbolList2set = Builtin.isSymbol list2setKey
139139
isSymbolInclusion :: Symbol -> Bool
140140
isSymbolInclusion = Builtin.isSymbol inclusionKey
141141

142+
-- TODO (thomas.tuegel): Rename this function.
142143
{- | Externalizes a 'Domain.InternalSet' as a 'TermLike'.
143144
-}
144145
asTermLike
145146
:: forall variable
146147
. InternalVariable variable
147-
=> InternalSet (TermLike Concrete) (TermLike variable)
148+
=> InternalSet Key (TermLike variable)
148149
-> TermLike variable
149150
asTermLike builtin =
150151
AssocComm.asTermLike
@@ -179,9 +180,9 @@ asTermLike builtin =
179180
NormalizedAc { opaque } = normalizedAc
180181

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

186187
element
187188
:: (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
@@ -61,6 +61,7 @@ module Kore.Internal.TermLike
6161
, mkInternalInt
6262
, mkInternalString
6363
, mkInternalList
64+
, Key
6465
, mkInternalMap
6566
, mkInternalSet
6667
, mkCeil
@@ -206,6 +207,9 @@ import qualified Data.Functor.Foldable as Recursive
206207
import Data.Generics.Product
207208
( field
208209
)
210+
import Data.Map.Strict
211+
( Map
212+
)
209213
import qualified Data.Map.Strict as Map
210214
import Data.Monoid
211215
( Endo (..)
@@ -245,6 +249,9 @@ import Kore.Internal.InternalList
245249
import Kore.Internal.InternalMap
246250
import Kore.Internal.InternalSet
247251
import Kore.Internal.InternalString
252+
import Kore.Internal.Key
253+
( Key
254+
)
248255
import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
249256
( Representation
250257
)
@@ -1095,7 +1102,7 @@ mkInternalList = updateCallStack . synthesize . InternalListF
10951102
mkInternalMap
10961103
:: HasCallStack
10971104
=> InternalVariable variable
1098-
=> InternalMap (TermLike Concrete) (TermLike variable)
1105+
=> InternalMap Key (TermLike variable)
10991106
-> TermLike variable
11001107
mkInternalMap = updateCallStack . synthesize . InternalMapF
11011108

@@ -1104,7 +1111,7 @@ mkInternalMap = updateCallStack . synthesize . InternalMapF
11041111
mkInternalSet
11051112
:: HasCallStack
11061113
=> InternalVariable variable
1107-
=> InternalSet (TermLike Concrete) (TermLike variable)
1114+
=> InternalSet Key (TermLike variable)
11081115
-> TermLike variable
11091116
mkInternalSet = updateCallStack . synthesize . InternalSetF
11101117

@@ -1566,20 +1573,25 @@ mkDefined = worker
15661573
. AcWrapper normalized
15671574
=> Functor (Value normalized)
15681575
=> Functor (Element normalized)
1569-
=> InternalAc (TermLike Concrete) normalized (TermLike variable)
1570-
-> InternalAc (TermLike Concrete) normalized (TermLike variable)
1576+
=> InternalAc Key normalized (TermLike variable)
1577+
-> InternalAc Key normalized (TermLike variable)
15711578
mkDefinedInternalAc internalAc =
15721579
Lens.over (field @"builtinAcChild") mkDefinedNormalized internalAc
15731580
where
1581+
mkDefinedNormalized
1582+
:: normalized Key (TermLike variable)
1583+
-> normalized Key (TermLike variable)
15741584
mkDefinedNormalized =
15751585
unwrapAc
15761586
>>> Lens.over (field @"concreteElements") mkDefinedConcrete
15771587
>>> Lens.over (field @"elementsWithVariables") mkDefinedAbstract
15781588
>>> Lens.over (field @"opaque") mkDefinedOpaque
15791589
>>> wrapAc
1590+
mkDefinedConcrete
1591+
:: Map Key (Value normalized (TermLike variable))
1592+
-> Map Key (Value normalized (TermLike variable))
15801593
mkDefinedConcrete =
15811594
(fmap . fmap) mkDefined
1582-
. Map.mapKeys mkDefined
15831595
mkDefinedAbstract = (fmap . fmap) mkDefined
15841596
mkDefinedOpaque = map mkDefined
15851597

@@ -1765,11 +1777,11 @@ pattern InternalList_
17651777
-> TermLike variable
17661778

17671779
pattern InternalMap_
1768-
:: InternalMap (TermLike Concrete) (TermLike variable)
1780+
:: InternalMap Key (TermLike variable)
17691781
-> TermLike variable
17701782

17711783
pattern InternalSet_
1772-
:: InternalSet (TermLike Concrete) (TermLike variable)
1784+
:: InternalSet Key (TermLike variable)
17731785
-> TermLike variable
17741786

17751787
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
@@ -81,6 +81,11 @@ import Kore.Internal.InternalList
8181
import Kore.Internal.InternalMap
8282
import Kore.Internal.InternalSet
8383
import Kore.Internal.InternalString
84+
import Kore.Internal.Key
85+
( Key
86+
, KeyF
87+
)
88+
import qualified Kore.Internal.Key as Key
8489
import Kore.Internal.Symbol hiding
8590
( isConstructorLike
8691
)
@@ -179,6 +184,7 @@ instance {-# OVERLAPS #-} Synthetic Pattern.Defined Defined where
179184
data TermLikeF variable child
180185
= AndF !(And Sort child)
181186
| ApplySymbolF !(Application Symbol child)
187+
-- TODO (thomas.tuegel): Expand aliases during validation?
182188
| ApplyAliasF !(Application (Alias (TermLike VariableName)) child)
183189
| BottomF !(Bottom Sort child)
184190
| CeilF !(Ceil Sort child)
@@ -205,8 +211,8 @@ data TermLikeF variable child
205211
| InternalIntF !(Const InternalInt child)
206212
| InternalStringF !(Const InternalString child)
207213
| InternalListF !(InternalList child)
208-
| InternalMapF !(InternalMap (TermLike Concrete) child)
209-
| InternalSetF !(InternalSet (TermLike Concrete) child)
214+
| InternalMapF !(InternalMap Key child)
215+
| InternalSetF !(InternalSet Key child)
210216
| VariableF !(Const (SomeVariable variable) child)
211217
| EndiannessF !(Const Endianness child)
212218
| SignednessF !(Const Signedness child)
@@ -500,6 +506,15 @@ instance Synthetic Pattern.ConstructorLike (TermLikeF variable) where
500506
InjF inj -> synthetic inj
501507
DefinedF defined -> synthetic defined
502508

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

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

0 commit comments

Comments
 (0)