Skip to content

Commit abf0292

Browse files
MirceaSana-pantilierv-jenkins
authored
Use unit and element symbol attributes
* moved Concat, Element and Unit symbol files * added AC symbol fields to Symbol * code refactoring * integrated new functions * added the strict pragma to modules newly introduced * Materialize Nix expressions * updated unparsing function * fixed redundant import issue * fixed error messages * fixed unit tests and refactored some code * Materialize Nix expressions * Materialize Nix expressions * refactoring and redefining of Eq/Ord instances * removed no longer relevant comments and refactored some code * fixed strictness issue * added unit tests for unparsing failures * Materialize Nix expressions * regenerated regression tests * Materialize Nix expressions * updated kore file for tiny test * updated integration test kore files * fixed small error * regenerated regression files again * removed test for issue 2095 * addressed some PR comments * prettified error messages for unit, element and concat mismatch * added HasCallStack to the new partial functions and their callers * Update kore/test/Test/Kore/Step/Simplification/InternalMap.hs Co-authored-by: ana-pantilie <[email protected]> * made some test easier to read * Materialize Nix expressions * fixed merge issue Co-authored-by: MirceaS <[email protected]> Co-authored-by: ana-pantilie <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent 2891334 commit abf0292

File tree

98 files changed

+48444
-95527
lines changed

Some content is hidden

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

98 files changed

+48444
-95527
lines changed

‎kore/kore.cabal

Lines changed: 5 additions & 5 deletions
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: 2702a5d875e9f185a4aedc5fdcafa951249ccd4ef5edab6f1e96689991c8f13f
7+
-- hash: 80d27d36f0343e3b6779aa37ed5fccc747fd7c1b66c7b9bd2fb27c1f6a2d6403
88

99
name: kore
1010
version: 0.41.0.0
@@ -70,7 +70,9 @@ library
7070
Kore.Attribute.Axiom.Symbolic
7171
Kore.Attribute.Axiom.Unit
7272
Kore.Attribute.Comm
73+
Kore.Attribute.Concat
7374
Kore.Attribute.Constructor
75+
Kore.Attribute.Element
7476
Kore.Attribute.Function
7577
Kore.Attribute.Functional
7678
Kore.Attribute.Hook
@@ -101,12 +103,9 @@ library
101103
Kore.Attribute.Smtlib.Smthook
102104
Kore.Attribute.Smtlib.Smtlib
103105
Kore.Attribute.Sort
104-
Kore.Attribute.Sort.Concat
105106
Kore.Attribute.Sort.Constructors
106107
Kore.Attribute.Sort.ConstructorsBuilder
107-
Kore.Attribute.Sort.Element
108108
Kore.Attribute.Sort.HasDomainValues
109-
Kore.Attribute.Sort.Unit
110109
Kore.Attribute.SortInjection
111110
Kore.Attribute.Source
112111
Kore.Attribute.SourceLocation
@@ -120,6 +119,7 @@ library
120119
Kore.Attribute.Synthetic
121120
Kore.Attribute.Trusted
122121
Kore.Attribute.UniqueId
122+
Kore.Attribute.Unit
123123
Kore.BugReport
124124
Kore.Builtin
125125
Kore.Builtin.AssocComm.AssocComm
@@ -916,7 +916,6 @@ test-suite kore-test
916916
Test.Kore.Attribute.Smtlib
917917
Test.Kore.Attribute.Sort.ConstructorsBuilder
918918
Test.Kore.Attribute.Sort.HasDomainValues
919-
Test.Kore.Attribute.Sort.Unit
920919
Test.Kore.Attribute.SortInjection
921920
Test.Kore.Attribute.Subsort
922921
Test.Kore.Attribute.Symbol
@@ -927,6 +926,7 @@ test-suite kore-test
927926
Test.Kore.Attribute.Symbol.SymbolKywd
928927
Test.Kore.Attribute.Trusted
929928
Test.Kore.Attribute.UniqueId
929+
Test.Kore.Attribute.Unit
930930
Test.Kore.BugReport
931931
Test.Kore.Builtin
932932
Test.Kore.Builtin.AssocComm.CeilSimplifier

‎kore/src/Kore/Attribute/Concat.hs

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{-|
2+
Copyright : (c) Runtime Verification, 2021
3+
License : NCSA
4+
-}
5+
6+
{-# LANGUAGE Strict #-}
7+
8+
module Kore.Attribute.Concat
9+
( Concat (..)
10+
, mergeConcat, toConcat, fromConcat
11+
, concatId, concatSymbol, concatAttribute
12+
) where
13+
14+
import Prelude.Kore
15+
16+
import Data.Default
17+
import qualified Generics.SOP as SOP
18+
import qualified Pretty
19+
20+
import Kore.Attribute.Parser
21+
import Kore.Debug
22+
import Kore.Unparser
23+
24+
-- | @Concat@ represents the @concat@ attribute.
25+
newtype Concat symbol = Concat { getConcat :: Maybe symbol }
26+
deriving (Generic, Eq, Ord, Show)
27+
deriving (Foldable, Functor, Traversable)
28+
deriving anyclass (Hashable)
29+
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
30+
deriving anyclass (Debug, Diff)
31+
32+
mergeConcat
33+
:: (Eq symbol , Unparse symbol)
34+
=> Concat symbol
35+
-> Concat symbol
36+
-> Concat symbol
37+
mergeConcat (Concat Nothing) b = b
38+
mergeConcat a (Concat Nothing) = a
39+
mergeConcat a@(Concat (Just aSymbol)) (Concat (Just bSymbol))
40+
| aSymbol == bSymbol = a
41+
| otherwise = (error . show . Pretty.vsep)
42+
[ "Concat symbol mismatch error! Found both"
43+
, Pretty.indent 4 (unparse aSymbol)
44+
, "and"
45+
, Pretty.indent 4 (unparse bSymbol)
46+
, "inside term. This is a bug."
47+
]
48+
49+
instance Default (Concat symbol) where
50+
def = Concat { getConcat = Nothing }
51+
52+
instance NFData symbol => NFData (Concat symbol)
53+
54+
instance ParseAttributes (Concat SymbolOrAlias) where
55+
parseAttribute = withApplication' parseApplication
56+
where
57+
parseApplication params args Concat { getConcat }
58+
| Just _ <- getConcat = failDuplicate'
59+
| otherwise = do
60+
getZeroParams params
61+
arg <- getOneArgument args
62+
symbol <- getSymbolOrAlias arg
63+
return Concat { getConcat = Just symbol }
64+
withApplication' = withApplication concatId
65+
failDuplicate' = failDuplicate concatId
66+
67+
instance From (Concat SymbolOrAlias) Attributes where
68+
from =
69+
maybe def toAttribute . getConcat
70+
where
71+
toAttribute = from @AttributePattern . concatAttribute
72+
73+
toConcat :: symbol -> Concat symbol
74+
toConcat sym = Concat { getConcat = Just sym }
75+
76+
fromConcat :: HasCallStack => Concat symbol -> symbol
77+
fromConcat Concat {getConcat = Just sym} = sym
78+
fromConcat _ = error "There is no concat symbol to extract"
79+
80+
-- | Kore identifier representing the @concat@ attribute symbol.
81+
concatId :: Id
82+
concatId = "concat"
83+
84+
-- | Kore symbol representing the @concat@ attribute.
85+
concatSymbol :: SymbolOrAlias
86+
concatSymbol =
87+
SymbolOrAlias
88+
{ symbolOrAliasConstructor = concatId
89+
, symbolOrAliasParams = []
90+
}
91+
92+
-- | Kore pattern representing the @concat@ attribute.
93+
concatAttribute :: SymbolOrAlias -> AttributePattern
94+
concatAttribute symbol =
95+
attributePattern concatSymbol [attributePattern_ symbol]

‎kore/src/Kore/Attribute/Element.hs

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{-|
2+
Copyright : (c) Runtime Verification, 2021
3+
License : NCSA
4+
-}
5+
6+
{-# LANGUAGE Strict #-}
7+
8+
module Kore.Attribute.Element
9+
( Element (..)
10+
, mergeElement, toElement, fromElement
11+
, elementId, elementSymbol, elementAttribute
12+
) where
13+
14+
import Prelude.Kore
15+
16+
import Data.Default
17+
import qualified Generics.SOP as SOP
18+
import qualified Pretty
19+
20+
import Kore.Attribute.Parser
21+
import Kore.Debug
22+
import Kore.Unparser
23+
24+
-- | @Element@ represents the @element@ attribute.
25+
newtype Element symbol = Element { getElement :: Maybe symbol }
26+
deriving (Generic, Eq, Ord, Show)
27+
deriving (Foldable, Functor, Traversable)
28+
deriving anyclass (Hashable)
29+
deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
30+
deriving anyclass (Debug, Diff)
31+
32+
mergeElement
33+
:: (Eq symbol , Unparse symbol)
34+
=> Element symbol
35+
-> Element symbol
36+
-> Element symbol
37+
mergeElement (Element Nothing) b = b
38+
mergeElement a (Element Nothing) = a
39+
mergeElement a@(Element (Just aSymbol)) (Element (Just bSymbol))
40+
| aSymbol == bSymbol = a
41+
| otherwise = (error . show . Pretty.vsep)
42+
[ "Element symbol mismatch error! Found both"
43+
, Pretty.indent 4 (unparse aSymbol)
44+
, "and"
45+
, Pretty.indent 4 (unparse bSymbol)
46+
, "inside term. This is a bug."
47+
]
48+
49+
instance Default (Element symbol) where
50+
def = Element { getElement = Nothing }
51+
52+
instance NFData symbol => NFData (Element symbol)
53+
54+
-- | Kore identifier representing the @element@ attribute symbol.
55+
elementId :: Id
56+
elementId = "element"
57+
58+
-- | Kore symbol representing the @element@ attribute.
59+
elementSymbol :: SymbolOrAlias
60+
elementSymbol =
61+
SymbolOrAlias
62+
{ symbolOrAliasConstructor = elementId
63+
, symbolOrAliasParams = []
64+
}
65+
66+
-- | Kore pattern representing the @element@ attribute.
67+
elementAttribute :: SymbolOrAlias -> AttributePattern
68+
elementAttribute symbol =
69+
attributePattern elementSymbol [attributePattern_ symbol]
70+
71+
instance ParseAttributes (Element SymbolOrAlias) where
72+
parseAttribute = withApplication' parseApplication
73+
where
74+
parseApplication params args Element { getElement }
75+
| Just _ <- getElement = failDuplicate'
76+
| otherwise = do
77+
getZeroParams params
78+
arg <- getOneArgument args
79+
symbol <- getSymbolOrAlias arg
80+
return Element { getElement = Just symbol }
81+
withApplication' = withApplication elementId
82+
failDuplicate' = failDuplicate elementId
83+
84+
instance From (Element SymbolOrAlias) Attributes where
85+
from =
86+
maybe def toAttribute . getElement
87+
where
88+
toAttribute = from @AttributePattern . elementAttribute
89+
90+
toElement :: symbol -> Element symbol
91+
toElement sym = Element { getElement = Just sym }
92+
93+
fromElement :: HasCallStack => Element symbol -> symbol
94+
fromElement Element {getElement = Just sym} = sym
95+
fromElement _ = error "There is no element symbol to extract"

‎kore/src/Kore/Attribute/Sort.hs

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -18,29 +18,29 @@ import Prelude.Kore hiding
1818
import qualified Control.Monad as Monad
1919
import Data.Generics.Product
2020

21+
import Kore.Attribute.Concat
22+
import Kore.Attribute.Element
2123
import Kore.Attribute.Hook
2224
import Kore.Attribute.Parser hiding
2325
( Sort
2426
)
2527
import Kore.Attribute.Smtlib.Smtlib
26-
import Kore.Attribute.Sort.Concat
27-
import Kore.Attribute.Sort.Element
2828
import Kore.Attribute.Sort.HasDomainValues
2929
( HasDomainValues
3030
)
31-
import Kore.Attribute.Sort.Unit
31+
import Kore.Attribute.Unit
3232

3333
data Sort =
3434
Sort
3535
{ hook :: !Hook
3636
-- ^ The builtin sort hooked to the sort.
3737
, smtlib :: !Smtlib
3838
-- ^ The user-defined translation of the sort for SMT.
39-
, unit :: !Unit
39+
, unit :: !(Unit SymbolOrAlias)
4040
-- ^ The unit symbol associated with the sort.
41-
, element :: !Element
41+
, element :: !(Element SymbolOrAlias)
4242
-- ^ The element symbol associated with the sort.
43-
, concat :: !Concat
43+
, concat :: !(Concat SymbolOrAlias)
4444
-- ^ The concat symbol associated with the sort.
4545
, hasDomainValues :: !HasDomainValues
4646
-- ^ whether the sort has domain values
@@ -68,9 +68,9 @@ instance ParseAttributes Sort where
6868
parseAttribute attr =
6969
typed @Hook (parseAttribute attr)
7070
Monad.>=> typed @Smtlib (parseAttribute attr)
71-
Monad.>=> typed @Unit (parseAttribute attr)
72-
Monad.>=> typed @Element (parseAttribute attr)
73-
Monad.>=> typed @Concat (parseAttribute attr)
71+
Monad.>=> typed @(Unit SymbolOrAlias) (parseAttribute attr)
72+
Monad.>=> typed @(Element SymbolOrAlias) (parseAttribute attr)
73+
Monad.>=> typed @(Concat SymbolOrAlias) (parseAttribute attr)
7474
Monad.>=> typed @HasDomainValues (parseAttribute attr)
7575

7676
instance From Sort Attributes where

‎kore/src/Kore/Attribute/Sort/Concat.hs

Lines changed: 0 additions & 70 deletions
This file was deleted.

0 commit comments

Comments
 (0)