Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
63491ca
Update resolver to lts-18.18
andreiburdusa Nov 24, 2021
90a85e7
Update haskell.nix
andreiburdusa Dec 3, 2021
f29fa63
Update ghc_version in test.yml
andreiburdusa Dec 6, 2021
5557f7f
Update fourmolu in sources.json
andreiburdusa Dec 6, 2021
27dcd28
Merge remote-tracking branch 'origin/master' into update-resolver-lts…
andreiburdusa Dec 9, 2021
b307dc2
Update fourmolu and hlint files
andreiburdusa Dec 10, 2021
261588e
Materialize Nix expressions
invalid-email-address Dec 10, 2021
0565e24
Merge remote-tracking branch 'origin/master' into update-resolver-lts…
andreiburdusa Dec 10, 2021
a7e033a
Format with fourmolu
invalid-email-address Dec 10, 2021
bef7036
Empty commit
andreiburdusa Dec 10, 2021
42f8d6a
Merge branch 'update-resolver-lts-18.18' of github.com:kframework/kor…
andreiburdusa Dec 10, 2021
6cd743f
Update index-state in default.nix
andreiburdusa Dec 10, 2021
8ceb92a
Update haskell-hls-nix in sources.json
andreiburdusa Dec 13, 2021
1c678e3
Revert "Update fourmolu in sources.json"
andreiburdusa Dec 13, 2021
13e3d85
Merge remote-tracking branch 'origin/master' into update-resolver-lts…
andreiburdusa Dec 13, 2021
cb0de5d
Materialize Nix expressions
invalid-email-address Dec 13, 2021
8d6de5f
Empty commit
andreiburdusa Dec 13, 2021
1a9c5bb
Merge branch 'update-resolver-lts-18.18' of github.com:kframework/kor…
andreiburdusa Dec 13, 2021
e9f9dbd
Format with fourmolu
invalid-email-address Dec 13, 2021
256674c
Empty commit
andreiburdusa Dec 13, 2021
83bcfd6
Give ghcVersion instead of compiler-nix-name to haskell-hls-nix
andreiburdusa Dec 13, 2021
ac308e8
Update hlint in sources.json and rematerialize
andreiburdusa Dec 13, 2021
eb02c94
Update hlint version in sources.json
andreiburdusa Dec 13, 2021
1f191dd
Empty commir to restart Cabal tests
andreiburdusa Dec 13, 2021
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
2 changes: 1 addition & 1 deletion .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ jobs:
name: 'Cabal'
runs-on: ubuntu-latest
env:
ghc_version: "8.10.4"
ghc_version: "8.10.7"
steps:
- name: Install prerequisites
run: |
Expand Down
5 changes: 3 additions & 2 deletions default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,9 @@ let
};

# Change the compiler when updating our own resolver.
compiler-nix-name = "ghc8104";
index-state = "2021-02-09T00:00:00Z";
compiler-nix-name = "ghc8107";
ghcVersion = "8.10.7";
index-state = "2021-12-03T00:00:00Z";
};

in default
2 changes: 1 addition & 1 deletion kore/kore.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ common library
build-depends: aeson >=1.4
build-depends: bytestring >=0.10
build-depends: clock >=0.8
build-depends: co-log >=0.3
build-depends: co-log >=0.4
build-depends: comonad >=5.0
build-depends: containers >=0.5.8
build-depends: cryptonite >=0.25
Expand Down
4 changes: 2 additions & 2 deletions kore/src/Kore/Builtin/AssociativeCommutative.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1358,9 +1358,9 @@ unifyEqualsElementLists
return (result, [])
where
unifyWithPermutations ::
-- | First structure elements
-- First structure elements
[ConcreteOrWithVariable normalized variable] ->
-- | Second structure elements
-- Second structure elements
[ConcreteOrWithVariable normalized variable] ->
unifier
( Conditional
Expand Down
6 changes: 3 additions & 3 deletions kore/src/Kore/Internal/TermLike/TermLike.hs
Original file line number Diff line number Diff line change
Expand Up @@ -847,11 +847,11 @@ instance InternalVariable variable => Substitute (TermLike variable) where
either extractFreeVariables (Set.singleton . variableName)

renaming ::
-- | Original variable
-- Original variable
SomeVariable variable ->
-- | Renamed variable
-- Renamed variable
Maybe (SomeVariable variable) ->
-- | Substitution
-- Substitution
Map
(SomeVariableName variable)
(Either (TermLike variable) (SomeVariable variable)) ->
Expand Down
6 changes: 3 additions & 3 deletions kore/src/Kore/Repl/Interpreter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1346,7 +1346,7 @@ performStepNoBranching =
-- Loop branch
(n, SingleResult _) -> do
res <- runStepper
pure $ Left (n -1, res)
pure $ Left (n - 1, res)
-- Early exit when there is a branch or there is no next.
(n, res) -> pure $ Right (n, res)

Expand All @@ -1366,8 +1366,8 @@ recursiveForcedStep n node
updateExecutionGraph graph
case result of
NoResult -> pure ()
SingleResult sr -> (recursiveForcedStep $ n -1) sr
BranchResult xs -> traverse_ (recursiveForcedStep (n -1)) xs
SingleResult sr -> (recursiveForcedStep $ n - 1) sr
BranchResult xs -> traverse_ (recursiveForcedStep (n - 1)) xs

-- | Display a rule as a String.
showRewriteRule ::
Expand Down
2 changes: 1 addition & 1 deletion kore/src/Kore/Rewrite/Strategy.hs
Original file line number Diff line number Diff line change
Expand Up @@ -339,7 +339,7 @@ executionHistoryStep transit prim exe@ExecutionGraph{graph} node
nodeIsNotLeaf = Graph.outdeg graph node > 0

mkChildNode ::
-- | Child node identifier and configuration
-- Child node identifier and configuration
(config, Seq rule) ->
ChildNode config rule
mkChildNode (config, rules) =
Expand Down
8 changes: 4 additions & 4 deletions kore/test/Test/Kore/Builtin/InternalBytes.hs
Original file line number Diff line number Diff line change
Expand Up @@ -265,9 +265,9 @@ test_substr =
testSubstrBytes ::
HasCallStack =>
TestName ->
-- | arguments of @substrBytes@ symbol
-- arguments of @substrBytes@ symbol
[TermLike RewritingVariableName] ->
-- | expected result
-- expected result
OrPattern RewritingVariableName ->
TestTree
testSubstrBytes testName = testBytes testName substrBytesSymbol
Expand Down Expand Up @@ -589,9 +589,9 @@ int2bytesData =
, (128, True, "\x80")
, (-128, True, "\x80")
, (2, True, "\x02")
, (- 2, True, "\xfe")
, (-2, True, "\xfe")
, (16, True, "\x10")
, (- 16, True, "\xf0")
, (-16, True, "\xf0")
, (128, True, "\x00\x80")
, (-128, True, "\xff\x80")
, (128, False, "\x80\x00")
Expand Down
10 changes: 5 additions & 5 deletions kore/test/Test/Kore/Builtin/Map.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1309,9 +1309,9 @@ test_renormalize =
becomes ::
HasCallStack =>
TestName ->
-- | original, (possibly) de-normalized map
-- original, (possibly) de-normalized map
NormalizedMap Key (TermLike RewritingVariableName) ->
-- | expected normalized map
-- expected normalized map
NormalizedMap Key (TermLike RewritingVariableName) ->
TestTree
becomes name origin expect =
Expand All @@ -1333,11 +1333,11 @@ test_renormalize =
testCase name $ assertEqual "" Nothing (Ac.renormalize origin)

mkMap' ::
-- | abstract elements
-- abstract elements
[(TermLike RewritingVariableName, TermLike RewritingVariableName)] ->
-- | concrete elements
-- concrete elements
[(Key, TermLike RewritingVariableName)] ->
-- | opaque terms
-- opaque terms
[NormalizedMap Key (TermLike RewritingVariableName)] ->
NormalizedMap Key (TermLike RewritingVariableName)
mkMap' abstract concrete opaque =
Expand Down
4 changes: 2 additions & 2 deletions kore/test/Test/Kore/Builtin/Set.hs
Original file line number Diff line number Diff line change
Expand Up @@ -508,9 +508,9 @@ test_difference_symbolic =

evalDifference ::
HasCallStack =>
-- | expected result
-- expected result
Maybe (Pattern RewritingVariableName) ->
-- | arguments of 'differenceSet'
-- arguments of 'differenceSet'
[TermLike RewritingVariableName] ->
Assertion
evalDifference expect args = do
Expand Down
18 changes: 9 additions & 9 deletions kore/test/Test/Kore/Reachability/MockAllPath.hs
Original file line number Diff line number Diff line change
Expand Up @@ -170,9 +170,9 @@ test_transitionRule_ApplyClaims =
unmodified state = run [Rule (A, B)] state `equals_` [(state, mempty)]
derives ::
HasCallStack =>
-- | rules to apply in parallel
-- rules to apply in parallel
[MockRule] ->
-- | transitions
-- transitions
[(MockClaimState, Seq MockAppliedRule)] ->
TestTree
derives rules = equals_ (run rules $ ClaimState.Claimed (MockClaim (A, C)))
Expand Down Expand Up @@ -201,9 +201,9 @@ test_transitionRule_ApplyAxioms =
unmodified state = run [Rule (A, B)] state `equals_` [(state, mempty)]
derives ::
HasCallStack =>
-- | rules to apply in parallel
-- rules to apply in parallel
[MockRule] ->
-- | transitions
-- transitions
[(MockClaimState, Seq MockAppliedRule)] ->
TestTree
derives rules =
Expand Down Expand Up @@ -242,11 +242,11 @@ test_runStrategy =
(ClaimState.Claimed . MockClaim . unRule $ goal)
disproves ::
HasCallStack =>
-- | Axioms
-- Axioms
[MockRule] ->
-- | Proof goal
-- Proof goal
MockClaim ->
-- | Unproven goals
-- Unproven goals
[MockClaim] ->
TestTree
disproves axioms (MockClaim goal) unproven =
Expand All @@ -256,9 +256,9 @@ test_runStrategy =
(show axioms ++ " disproves " ++ show goal)
proves ::
HasCallStack =>
-- | Axioms
-- Axioms
[MockRule] ->
-- | Proof goal
-- Proof goal
MockClaim ->
TestTree
proves axioms (MockClaim goal) =
Expand Down
2 changes: 1 addition & 1 deletion kore/test/Test/Kore/Rewrite/Rule/Simplify.hs
Original file line number Diff line number Diff line change
Expand Up @@ -432,7 +432,7 @@ test_simplifyClaimRule =
test ::
HasCallStack =>
TestName ->
-- | replacements
-- replacements
[(TermLike RewritingVariableName, TermLike RewritingVariableName)] ->
ClaimPattern ->
[ClaimPattern] ->
Expand Down
4 changes: 2 additions & 2 deletions kore/test/Test/Kore/Simplify/SubstitutionSimplifier.hs
Original file line number Diff line number Diff line change
Expand Up @@ -218,12 +218,12 @@ test_SubstitutionSimplifier =
test ::
HasCallStack =>
TestName ->
-- | Test input
-- Test input
[ ( SomeVariable RewritingVariableName
, TermLike RewritingVariableName
)
] ->
-- | Expected normalized, denormalized outputs
-- Expected normalized, denormalized outputs
[Normalization RewritingVariableName] ->
TestTree
test
Expand Down
2 changes: 1 addition & 1 deletion kore/test/Test/Kore/Simplify/TermLike.hs
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@ test_simplifyOnly =
HasCallStack =>
TestName ->
TermLike RewritingVariableName ->
-- | Expected output, if simplified.
-- Expected output, if simplified.
Maybe (OrPattern RewritingVariableName) ->
TestTree
test testName input maybeExpect =
Expand Down
6 changes: 3 additions & 3 deletions kore/test/Test/Kore/Unification/SubstitutionNormalization.hs
Original file line number Diff line number Diff line change
Expand Up @@ -338,9 +338,9 @@ test_normalize =
test ::
HasCallStack =>
TestName ->
-- | Test input
-- Test input
Map (SomeVariable VariableName) (TermLike VariableName) ->
-- | Expected output
-- Expected output
Normalization VariableName ->
TestTree
test testName input normalization =
Expand All @@ -352,7 +352,7 @@ test_normalize =
testBottom ::
HasCallStack =>
TestName ->
-- | Test input
-- Test input
Map (SomeVariable VariableName) (TermLike VariableName) ->
TestTree
testBottom testName input =
Expand Down
Loading