Skip to content

Issue 2100 follow up #2574

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

Merged
merged 1 commit into from
Apr 26, 2021
Merged

Issue 2100 follow up #2574

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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 kore/src/Kore/ASTVerifier/SentenceVerifier.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ import Kore.ASTVerifier.PatternVerifier as PatternVerifier
import Kore.ASTVerifier.SortVerifier
import Kore.ASTVerifier.Verifier
import qualified Kore.Attribute.Axiom as Attribute (
Axiom (..),
Axiom,
parseAxiomAttributes,
)
import qualified Kore.Attribute.Hook as Attribute
Expand Down
40 changes: 32 additions & 8 deletions kore/src/Kore/Equation/Sentence.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,14 +65,38 @@ data MatchEquationError variable
deriving anyclass (Debug)

instance InternalVariable variable => Pretty (MatchEquationError variable) where
pretty (NotEquation term) = "The given term is not an equation:\n" <> unparse term
pretty (RequiresError notPred) = "The equation's requires clause is not a predicate:\n" <> pretty notPred
pretty (ArgumentError notPred) = "The equation's argument clause is not a predicate:\n" <> pretty notPred
pretty (AntiLeftError notPred) = "The equation's anti-left clause is not a predicate:\n" <> pretty notPred
pretty (EnsuresError notPred) = "The equation's ensures clause is not a predicate:\n" <> pretty notPred
pretty FunctionalAxiom = "The term is a functional axiom"
pretty ConstructorAxiom = "The term is a constructor axiom"
pretty SubsortAxiom = "The term is a subsort axiom"
pretty (NotEquation term) =
Pretty.vsep
[ "The given term is not an equation:"
, unparse term
]
pretty (RequiresError notPred) =
Pretty.vsep
[ "The equation's requires clause is not a predicate:"
, pretty notPred
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
]
pretty (ArgumentError notPred) =
Pretty.vsep
[ "The equation's argument clause is not a predicate:"
, pretty notPred
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
]
pretty (AntiLeftError notPred) =
Pretty.vsep
[ "The equation's anti-left clause is not a predicate:"
, pretty notPred
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
]
pretty (EnsuresError notPred) =
Pretty.vsep
[ "The equation's ensures clause is not a predicate:"
, pretty notPred
, "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
]
pretty FunctionalAxiom = "The term is a functional axiom."
pretty ConstructorAxiom = "The term is a constructor axiom."
pretty SubsortAxiom = "The term is a subsort axiom."

matchEquation ::
forall variable.
Expand Down
35 changes: 18 additions & 17 deletions kore/src/Kore/Equation/Validate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,14 +113,14 @@ validateAxiom attrs verified =
pack $
show $
Pretty.vsep
[ "Head of LHS of Not Simplification axiom is not a non-constructor function symbol. This is the LHS symbol:"
[ "Expected function symbol, but found constructor symbol:"
, unparse sym
]

checkVarFunctionArguments =
failOnJust
eq
"LHS of NotSimplification axiom contains non-variable:"
"Expected variable, but found:"
$ asum $ getNotVar <$> termLikeF

getNotVar (TermLike.Var_ _) = Nothing
Expand All @@ -129,7 +129,7 @@ validateAxiom attrs verified =
checkArg _ Nothing = return ()
checkArg eq (Just arg) =
traverse_
( failOnJust eq "Found invalid subterm of Axiom equation argument:"
( failOnJust eq "Found invalid subterm in argument of function equation:"
. checkArgIn
)
$ Predicate.getMultiAndPredicate arg
Expand All @@ -144,20 +144,7 @@ validateAxiom attrs verified =
_
| TermLike.isConstructorLike term -> descend
TermLike.App_ sym _
| or
[ Symbol.isConstructorLike sym
, Symbol.isAnywhere sym && Symbol.isInjective sym
, Map.isSymbolConcat sym
, Map.isSymbolElement sym
, Map.isSymbolUnit sym
, Set.isSymbolConcat sym
, Set.isSymbolElement sym
, Set.isSymbolUnit sym
, List.isSymbolConcat sym
, List.isSymbolElement sym
, List.isSymbolUnit sym
] ->
descend
| isGoodSymbol sym -> descend
| otherwise -> Just term
TermLike.InternalBytes_ _ _ -> Nothing
TermLike.InternalBool_ _ -> Nothing
Expand All @@ -170,6 +157,20 @@ validateAxiom attrs verified =
_ -> Just term
where
_ :< termF = Recursive.project term
isGoodSymbol sym =
or
[ Symbol.isConstructorLike sym
, Symbol.isAnywhere sym && Symbol.isInjective sym
, Map.isSymbolConcat sym
, Map.isSymbolElement sym
, Map.isSymbolUnit sym
, Set.isSymbolConcat sym
, Set.isSymbolElement sym
, Set.isSymbolUnit sym
, List.isSymbolConcat sym
, List.isSymbolElement sym
, List.isSymbolUnit sym
]
descend = asum $ findBadArgSubterm <$> termF

failOnJust _ _ Nothing = return ()
Expand Down