Skip to content

Commit

Permalink
collect ensures clause in Parser.scala (#838)
Browse files Browse the repository at this point in the history 
Here we add code to the scala codebase to collect into the AxiomInfo the
ensures clause of axioms. This is not actually used by the llvm backend
because the llvm backend does not support `ensures`, but we need to
collect it because this code path is shared with the Maude backend.
  • Loading branch information
Dwight Guth authored Sep 26, 2023
1 parent c64bbbb commit afb8810
Showing 1 changed file with 21 additions and 20 deletions.
41 changes: 21 additions & 20 deletions matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import org.kframework.parser.kore.implementation.{DefaultBuilders => B}
import java.util
import java.util.Optional

case class AxiomInfo(priority: Int, ordinal: Int, rewrite: GeneralizedRewrite, sideCondition: Option[Pattern], source: Optional[Source], location: Optional[Location], att: Attributes) {}
case class AxiomInfo(priority: Int, ordinal: Int, rewrite: GeneralizedRewrite, sideCondition: Option[Pattern], ensures: Option[Pattern], source: Optional[Source], location: Optional[Location], att: Attributes) {}

object Parser {

Expand Down Expand Up @@ -136,7 +136,7 @@ object Parser {
private def location(axiom: AxiomDeclaration): Optional[Location] = location(axiom.att)

private def parseAxiomSentence[T <: GeneralizedRewrite](
split: Pattern => Option[(Option[SymbolOrAlias], T, Option[Pattern])],
split: Pattern => Option[(Option[SymbolOrAlias], T, Option[Pattern], Option[Pattern])],
axiom: (AxiomDeclaration, Int),
simplification: Boolean,
search: Boolean) :
Expand All @@ -147,43 +147,44 @@ object Parser {
if (hasAtt(s, "comm") || hasAtt(s, "assoc") || hasAtt(s, "idem") || hasAtt(s, "unit") || hasAtt(s, "non-executable") || (hasAtt(s, "simplification") && !simplification)) {
Seq()
} else {
Seq((splitted.get._1, AxiomInfo(rulePriority(s, search), axiom._2, splitted.get._2, splitted.get._3, source(s), location(s), s.att)))
Seq((splitted.get._1, AxiomInfo(rulePriority(s, search), axiom._2, splitted.get._2, splitted.get._3, splitted.get._4, source(s), location(s), s.att)))
}
} else {
Seq()
}
}

private def splitTop(topPattern: Pattern): Option[(Option[SymbolOrAlias], Rewrites, Option[Pattern])] = {
private def splitTop(topPattern: Pattern): Option[(Option[SymbolOrAlias], Rewrites, Option[Pattern], Option[Pattern])] = {
topPattern match {
case Rewrites(s, And(_, Equals(_, _, pat, _), l), And(_, _, r)) => Some((None, B.Rewrites(s, l, r), Some(pat)))
case Rewrites(s, And(_, l, Equals(_, _, pat, _)), And(_, r, _)) => Some((None, B.Rewrites(s, l, r), Some(pat)))
case Rewrites(s, And(_, Top(_), l), And(_, _, r)) => Some((None, B.Rewrites(s, l, r), None))
case Rewrites(s, And(_, l, Top(_)), And(_, r, _)) => Some((None, B.Rewrites(s, l, r), None))
case Rewrites(s, And(_, Not(_, _), And(_, Equals(_, _, pat, _), l)), And(_, _, r)) => Some((None, B.Rewrites(s, l, r), Some(pat)))
case Rewrites(s, And(_, Not(_, _), And(_, Top(_), l)), And(_, _, r)) => Some((None, B.Rewrites(s, l, r), None))
case Rewrites(s, And(_, req @ Equals(_, _, _, _), l), And(_, ens, r)) => Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
case Rewrites(s, And(_, req @ Top(_), l), And(_, ens, r)) => Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
case Rewrites(s, And(_, Not(_, _), And(_, req, l)), And(_, ens, r)) => Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
case Rewrites(s, And(_, l, req), And(_, r, ens)) => Some((None, B.Rewrites(s, l, r), splitPredicate(req), splitPredicate(ens)))
case _ => None
}
}

private def splitPredicate(pat: Pattern): Option[Pattern] = {
pat match {
case Top(_) => None
case Equals(_, _, pat, _) => Some(pat)
}
}

private def getPatterns(pat: Pattern): List[Pattern] = {
pat match {
case And(_, Mem(_, _, _, pat), pats) => pat :: getPatterns(pats)
case Top(_) => Nil
}
}

private def splitFunction(topPattern: Pattern): Option[(Option[SymbolOrAlias], Equals, Option[Pattern])] = {
private def splitFunction(topPattern: Pattern): Option[(Option[SymbolOrAlias], Equals, Option[Pattern], Option[Pattern])] = {
topPattern match {
case Implies(_, And(_, Equals(_, _, pat, _), args), Equals(i, o, Application(symbol, _), And(_, rhs, _))) => Some(Some(symbol), B.Equals(i, o, B.Application(symbol, getPatterns(args)), rhs), Some(pat))
case Implies(_, And(_, Not(_, _), And (_, Equals(_, _, pat, _), args)), Equals(i, o, Application(symbol, _), And(_, rhs, _))) => Some(Some(symbol), B.Equals(i, o, B.Application(symbol, getPatterns(args)), rhs), Some(pat))
case Implies(_, And(_, Not(_, _), And (_, Top(_), args)), Equals(i, o, Application(symbol, _), And(_, rhs, _))) => Some(Some(symbol), B.Equals(i, o, B.Application(symbol, getPatterns(args)), rhs), None)
case Implies(_, And(_, Top(_), args), Equals(i, o, Application(symbol, _), And(_, rhs, _))) => Some(Some(symbol), B.Equals(i, o, B.Application(symbol, getPatterns(args)), rhs), None)
case Implies(_, Top(_), Equals(i, o, app @ Application(symbol, _), And(_, rhs, Top(_)))) => Some(Some(symbol), B.Equals(i, o, app, rhs), None)
case Implies(_, Equals(_, _, pat, _), Equals(i, o, app @ Application(symbol, _), And(_, rhs, Top(_)))) => Some(Some(symbol), B.Equals(i, o, app, rhs), Some(pat))
case Implies(_, Top(_), eq @ Equals(_, _, Application(symbol, _), _)) => Some(Some(symbol), eq, None)
case Implies(_, Equals(_, _, pat, _), eq @ Equals(_, _, Application(symbol, _), _)) => Some(Some(symbol), eq, Some(pat))
case eq @ Equals(_, _, Application(symbol, _), _) => Some(Some(symbol), eq, None)
case Implies(_, And(_, Not(_, _), And (_, req, args)), Equals(i, o, Application(symbol, _), And(_, rhs, ens))) => Some(Some(symbol), B.Equals(i, o, B.Application(symbol, getPatterns(args)), rhs), splitPredicate(req), splitPredicate(ens))
case Implies(_, And(_, req, args), Equals(i, o, Application(symbol, _), And(_, rhs, ens))) => Some(Some(symbol), B.Equals(i, o, B.Application(symbol, getPatterns(args)), rhs), splitPredicate(req), splitPredicate(ens))
case Implies(_, req, Equals(i, o, app @ Application(symbol, _), And(_, rhs, ens))) => Some(Some(symbol), B.Equals(i, o, app, rhs), splitPredicate(req), splitPredicate(ens))
case Implies(_, req, eq @ Equals(_, _, Application(symbol, _), _)) => Some(Some(symbol), eq, splitPredicate(req), None)
case eq @ Equals(_, _, Application(symbol, _), _) => Some(Some(symbol), eq, None, None)
case _ => None
}
}
Expand Down

0 comments on commit afb8810

Please sign in to comment.