Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Emit KoreJson \right-assoc for collections #3651

Closed
wants to merge 13 commits into from
Closed

Emit KoreJson \right-assoc for collections #3651

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
248cace
prune any bottom states from a branch
goodlyrottenapple Sep 6, 2023
ed4d143
Add a custom conversion from TermLike to KoreJson which encodes colle…
goodlyrottenapple Sep 8, 2023
d7e4db6
Format with fourmolu
invalid-email-address Sep 8, 2023
33ba3e1
Format with fourmolu
invalid-email-address Sep 8, 2023
a704ce8
revert kore/src/Kore/Rewrite.hs
goodlyrottenapple Sep 8, 2023
d1053d3
fix retry code in runTests.py
goodlyrottenapple Sep 11, 2023
41b80d4
add rpc test returning a set
goodlyrottenapple Sep 11, 2023
9d1a51b
add .DS_Store to .gitignore
goodlyrottenapple Sep 11, 2023
9a803db
Merge remote-tracking branch 'origin/master' into sam/right-assoc-col…
goodlyrottenapple Sep 11, 2023
17d941f
merge master
goodlyrottenapple Dec 13, 2023
dd56839
cleanup merge
goodlyrottenapple Dec 13, 2023
c94b056
Revert "cleanup merge"
goodlyrottenapple Dec 13, 2023
290012c
Merge branch 'master' into sam/right-assoc-collections
goodlyrottenapple Jan 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,3 +51,4 @@ hie.yaml
.hie/
.direnv
*~
.DS_Store
1 change: 1 addition & 0 deletions kore/src/Kore/Builtin/Endianness/Endianness.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ License : BSD-3-Clause
module Kore.Builtin.Endianness.Endianness (
Endianness (..),
toApplication,
toSymbol,
) where

import Data.Functor.Const
Expand Down
1 change: 1 addition & 0 deletions kore/src/Kore/Builtin/Signedness/Signedness.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ License : BSD-3-Clause
module Kore.Builtin.Signedness.Signedness (
Signedness (..),
toApplication,
toSymbol,
) where

import Data.Functor.Const
Expand Down
8 changes: 4 additions & 4 deletions kore/src/Kore/Syntax/Json.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,8 @@ import Kore.Internal.Substitution qualified as Substitution
import Kore.Internal.TermLike qualified as TermLike
import Kore.Internal.TermLike.TermLike (TermLike)
import Kore.Syntax qualified as Kore
import Kore.Syntax.Json.Internal
import Kore.Syntax.Json.Internal hiding (fromTermLike)
import Kore.Syntax.Json.Internal qualified
import Kore.Syntax.Variable (VariableName (..))
import Prelude.Kore

Expand Down Expand Up @@ -100,15 +101,14 @@ prettyJsonOpts =
fromTermLike :: TermLike VariableName -> KoreJson
fromTermLike =
addHeader
. fromPattern
. from @_ @(Kore.Pattern _ (TermLike.TermAttributes VariableName))
. Kore.Syntax.Json.Internal.fromTermLike
Comment on lines -103 to +104
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should completely delete Internal.fromPattern and rewrite the unit tests to use the new fromTermLike to retain the test coverage.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure what the best way to go about this is tbh. fromPattern is basically unused, but we use the inverse toParsedPattern in a lot of places. The problem is we go from KorePattern to ParsedPattern which at some point gets turned into a TermLike which we then turn back into a KorePattern. Perhaps that path should be added and we keep the other unit tests??


fromPredicate :: Kore.Sort -> Predicate VariableName -> KoreJson
fromPredicate s = fromTermLike . Predicate.fromPredicate s

{- | represent a @'Substitution'@ as a conjunction of equalities, so

'[t1 / X1][t2 / X2]..[tn / Xn'
'[t1 / X1][t2 / X2]..[tn / Xn]'

becomes

Expand Down
Loading
Loading