Develop.symbolic

src/main/scala/org/kframework/kale/SubstitutionApply.scala

@@ -1,6 +1,7 @@
 package org.kframework.kale
 
 import org.kframework.kale.transformer.Unary
+import org.kframework.kale.transformer.Unary.Apply
 
 object Var {
   def apply(solver: SubstitutionApply)(v: Variable): Term = solver.substitution.get(v).getOrElse(v)
@@ -13,9 +14,14 @@ class SubstitutionApply(val substitution: Substitution)(implicit penv: Environme
   def ExistsSub(solver: SubstitutionApply)(v: Exists): Term =
     substitutionMaker(solver.substitution.remove(v.v))(v.p)
 
+  def HLPF(solver: SubstitutionApply)(t: FreeNode1): Term = {
+    t.copy(solver(t._1))
+  }
+
   override def processingFunctions = definePartialFunction[Term, this.type]({
     case `Variable` => Var.apply _
     case Exists => ExistsSub _
+    case l: HasLabelPredicateFunction => HLPF _
   }) orElse env.unaryProcessingFunctions
 
   override def apply(t: Term): Term = {

src/main/scala/org/kframework/kale/builtin/MAP.scala

@@ -99,7 +99,10 @@ trait MapMixin extends Mixin {
 
 }
 
-case class MapLabel(name: String, indexFunction: Term => Term, identity: Term)(implicit val env: Environment) extends NonPrimitiveMonoidLabel with Constructor {
+case class MapLabel(name: String, indexFunction: Term => Term, identity: Term)
+                   (implicit val env: Environment)
+  extends NonPrimitiveMonoidLabel with Constructor {
+
   override val isPredicate: Option[Boolean] = Some(false)
 
   def isIndexable(t: Term) =

src/main/scala/org/kframework/kale/builtin/SET.scala

@@ -4,7 +4,10 @@ import org.kframework.kale._
 
 import scala.collection.{Iterable, Set}
 
-case class SetLabel(name: String, identity: Term)(implicit val env: Environment with BooleanMixin) extends NonPrimitiveMonoidLabel with Constructor {
+case class SetLabel(name: String, identity: Term)
+                   (implicit val env: Environment with BooleanMixin)
+  extends NonPrimitiveMonoidLabel with Constructor {
+
   override val isPredicate: Option[Boolean] = Some(false)
 
   override def construct(l: Iterable[Term]): Term = SET(this, l.toSet)

src/main/scala/org/kframework/kale/context/pattern.scala

@@ -12,7 +12,8 @@ import scala.collection.Set
 trait PatternContextMixin extends Mixin {
   _: Environment with standard.MatchingLogicMixin with HasMatcher with HolesMixin =>
 
-  case class PatternContextApplicationLabel(name: String)(implicit val env: Environment with standard.MatchingLogicMixin)
+  case class PatternContextApplicationLabel(name: String)
+                                           (implicit val env: Environment with standard.MatchingLogicMixin)
     extends Context1ApplicationLabel with CluelessRoaring {
 
     //  val C = env.Variable("GENERIC_CONTEXT_VAR")

src/main/scala/org/kframework/kale/function.scala

@@ -3,9 +3,6 @@ package org.kframework.kale
 import cats.Monoid
 import org.kframework.kale.highcats._
 import org.kframework.kale.standard.AssocWithIdList
-import org.roaringbitmap.RoaringBitmap
-
-import scala.annotation.switch
 
 trait FunctionLabel extends NodeLabel with CluelessRoaring {
   val name: String
@@ -17,6 +14,12 @@ trait PureFunctionLabel {
   override lazy val isPredicate = Some(false)
 }
 
+trait PredicateFunctionLabel {
+  self: FunctionLabel =>
+
+  override lazy val isPredicate = Some(true)
+}
+
 trait FunctionLabel0 extends Label0 with FunctionLabel {
   def f(): Option[Term]
 
@@ -37,6 +40,10 @@ trait FunctionLabel2 extends Label2 with FunctionLabel {
   override def apply(_1: Term, _2: Term): Term = env.bottomize(_1, _2) {
     f(_1, _2) getOrElse FreeNode2(this, _1, _2)
   }
+  // testing only
+  def applyBuild(_1: Term, _2: Term): Term = env.bottomize(_1, _2) {
+    FreeNode2(this, _1, _2)
+  }
 }
 
 trait FunctionLabel3 extends Label3 with FunctionLabel {
@@ -55,7 +62,9 @@ trait FunctionLabel4 extends Label4 with FunctionLabel {
   }
 }
 
-case class PrimitiveFunction1[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], primitiveF: A => R)(implicit val env: Environment) extends FunctionLabel1 with PureFunctionLabel {
+case class PrimitiveFunction1[A, R]
+(name: String, aLabel: UpDown[A], rLabel: Up[R], primitiveF: A => R)
+(implicit val env: Environment) extends FunctionLabel1 with PureFunctionLabel {
   def f(_1: Term): Option[Term] = _1 match {
     case aLabel.extract(a) => Some(rLabel.up(primitiveF(a)))
     case _ => None
@@ -67,11 +76,51 @@ object PrimitiveFunction1 {
     PrimitiveFunction1(name, aLabel, aLabel, f)
 }
 
-case class PrimitiveFunction2[A, B, R](name: String, aLabel: UpDown[A], bLabel: UpDown[B], rLabel: Up[R], primitiveF: (A, B) => R)(implicit val env: Environment)
+case class HasLabelPredicateFunction(name: String, label: Label)
+                                    (implicit val env: Environment)
+  extends FunctionLabel1 with PredicateFunctionLabel {
+
+  def f(_1: Term): Option[Term] = {
+    if (_1.label.isInstanceOf[VariableLabel]) {
+      None
+    } else if (_1.label == label) {
+      Some(env.Top)
+    } else _1 match {
+      case v: SymbolicVariable if v.givenLabel == label =>
+        Some(env.Top)
+      case _ =>
+        Some(env.Bottom)
+    }
+  }
+}
+
+case class PredicateFunction1(functionLabel: FunctionLabel1)
+                             (implicit val env: Environment)
+  extends FunctionLabel1 with PredicateFunctionLabel {
+  override def f(_1: Term) = {
+    if (_1.label.isInstanceOf[VariableLabel]) {
+      None
+    } else {
+      functionLabel.f(_1)
+    }
+  }
+
+  override val name = "pred" + functionLabel.name
+}
+
+case class PrimitiveFunction2[A, B, R](name: String,
+                                       aLabel: UpDown[A], bLabel: UpDown[B], rLabel: Up[R],
+                                       primitiveF: (A, B) => R)
+                                      (implicit val env: Environment)
   extends FunctionLabel2 with PureFunctionLabel {
 
   def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
     case (aLabel.extract(a), bLabel.extract(b)) => Some(rLabel.up(primitiveF(a, b)))
+    case (_: SymbolicVariable, bLabel.extract(_))
+         |(aLabel.extract(_), _: SymbolicVariable)
+         | (_: SymbolicVariable, _: SymbolicVariable) =>
+      val newVar: SymbolicVariable = env.SymbolicVariable.freshVariable(rLabel.label)
+      Some(env.And(newVar, env.Equality(newVar, FreeNode2(this, _1, _2))))
     case _ => None
   }
 }
@@ -149,10 +198,12 @@ case class PrimitiveMonoid[O: Monoid : UpDown](name: String)(implicit val env: E
 
 
 object PrimitiveFunction2 {
-  def apply[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], f: (A, A) => R)(implicit env: Environment): PrimitiveFunction2[A, A, R] =
+  def apply[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], f: (A, A) => R)
+                 (implicit env: Environment): PrimitiveFunction2[A, A, R] =
     PrimitiveFunction2(name, aLabel, aLabel, rLabel, f)
 
-  def apply[A](name: String, aLabel: UpDown[A], f: (A, A) => A)(implicit env: Environment): PrimitiveFunction2[A, A, A] =
+  def apply[A](name: String, aLabel: UpDown[A], f: (A, A) => A)
+              (implicit env: Environment): PrimitiveFunction2[A, A, A] =
     PrimitiveFunction2(name, aLabel, aLabel, aLabel, f)
 }
 

src/main/scala/org/kframework/kale/highcats/Free.scala

@@ -4,7 +4,7 @@ import cats._
 import cats.implicits._
 import cats.{Apply, Eq}
 import org.kframework.kale.util.LabelNamed
-import org.kframework.kale.{Environment, FreeLabel1, FreeLabel2, FreeLabel3, Term}
+import org.kframework.kale.{Environment, FreeLabel1, FreeLabel2, FreeLabel3, Label, Term}
 
 trait Free {
   _: Environment =>
@@ -21,6 +21,8 @@ trait Free {
         case (a) => a.down[A] map companionObject
       }
       override def up(o: R): Term = apply(split(o))
+
+      override def label: Label = this
     }
 
   def free2[A: UpDown, B: UpDown, R <: Product](companionObject: (A, B) => R) =
@@ -35,6 +37,8 @@ trait Free {
       override def up(o: R) = split(o) match {
         case (a, b) => apply(a, b)
       }
+
+      override def label: Label = this
     }
 
   def free3[A: UpDown, B: UpDown, C: UpDown, R <: Product](companionObject: (A, B, C) => R) =
@@ -51,6 +55,8 @@ trait Free {
           case (a, b, c) => apply(a, b, c)
         }
       }
+
+      override def label: Label = this
     }
 
 }

src/main/scala/org/kframework/kale/highcats/UpDown.scala

@@ -1,9 +1,10 @@
 package org.kframework.kale.highcats
 
-import org.kframework.kale.{LeafLabel, Term}
+import org.kframework.kale.{Label, LeafLabel, Term}
 
 trait Up[O] {
   def up(o: O): Term
+  def label: Label
 }
 
 trait Down[O] {
@@ -17,12 +18,17 @@ trait Down[O] {
 object UpDown {
   final def apply[O](implicit instance: Up[O]): Up[O] = instance
 
-  final def apply[O](f: O => Term): Up[O] = (o: O) => f(o)
+  final def apply[O](f: O => Term, l: LeafLabel[O]): Up[O] = new Up[O] {
+    override def up(o: O) = f(o)
+    override def label: LeafLabel[O] = l
+  }
 
   final implicit def updownFromLeafLabel[O](implicit l: LeafLabel[O]): UpDown[O] = new UpDown[O] {
     override def down(t: Term) = l.unapply(t)
 
     override def up(o: O) = l.apply(o)
+
+    override def label: LeafLabel[O] = l
   }
 }
 

src/main/scala/org/kframework/kale/highcats/liftedCats.scala

@@ -4,7 +4,7 @@ import cats._
 import cats.implicits._
 import org.kframework.kale.standard.ReferenceLabel
 import org.kframework.kale.util.LabelNamed
-import org.kframework.kale.{Environment, FunctionLabel, FunctionLabel1, Label1, Label2, Mixin, MonoidLabel, PrimitiveFunction1, PrimitiveFunction2, PrimitiveFunction3, PrimitiveMonoid, Term, highcats}
+import org.kframework.kale.{Environment, FunctionLabel, FunctionLabel1, Label, Label1, Label2, LeafLabel, Mixin, MonoidLabel, PrimitiveFunction1, PrimitiveFunction2, PrimitiveFunction3, PrimitiveMonoid, Term, highcats}
 
 trait Convert[A, B] {
   def convert(a: A): B
@@ -58,16 +58,18 @@ trait LiftedCatsMixin extends Mixin with highcats.Free {
   implicit def upMonoidLabeled[O[_] : MonoidLabeled : Traverse : Applicative : MonoidK, E: UpDown]: UpDown[O[E]] = new UpDown[O[E]] {
     val eUpDown = implicitly[UpDown[E]]
     val fTraverse = implicitly[Traverse[O]]
-    val label = implicitly[MonoidLabeled[O]].monoidLabel
+    val mLabel = implicitly[MonoidLabeled[O]].monoidLabel
     val oMonoid = implicitly[MonoidK[O]].algebra[E]
     val oApplicative = implicitly[Applicative[O]]
 
+    override def label: Label = mLabel
+
     override def up(o: O[E]): Term = {
-      fTraverse.foldMap(o)(eUpDown.up)(label)
+      fTraverse.foldMap(o)(eUpDown.up)(mLabel)
     }
 
     override def down(t: Term): Option[O[E]] = t match {
-      case label.iterable(seq: Iterable[Term]) =>
+      case mLabel.iterable(seq: Iterable[Term]) =>
         def ff(t: Term) = oApplicative.pure(eUpDown.down(t).get)
 
         Some(implicitly[Traverse[scala.List]].foldMap(seq.toList)(ff)(oMonoid))

src/main/scala/org/kframework/kale/matchingLogic.scala

@@ -1,6 +1,6 @@
 package org.kframework.kale
 
-import org.kframework.kale.standard.{MightBeSolved}
+import org.kframework.kale.standard.MightBeSolved
 import org.kframework.kore.implementation.DefaultBuilders
 import org.kframework.{kale, kore}
 
@@ -15,6 +15,7 @@ trait MatchingLogicMixin extends Mixin {
 
   // Labels
   val Variable: VariableLabel
+  val SymbolicVariable: SymbolicVariableLabel
   val And: AndLabel
   val Or: OrLabel
   val Rewrite: RewriteLabel
@@ -79,6 +80,28 @@ trait VariableLabel extends LeafLabel[(Name, Sort)] {
   def apply(name: kale.Name): Variable = apply((name, standard.Sort.K))
 }
 
+trait SymbolicVariableLabel extends LeafLabel[(Name, Sort, Label)] {
+  def apply(name: String, givenLabel: Label): SymbolicVariable =
+    apply((standard.Name(name), standard.Sort.K, givenLabel))
+
+  def apply(name: String, sort: kale.Sort, givenLabel: Label): SymbolicVariable =
+    apply((standard.Name(name), sort, givenLabel))
+
+  def apply(v: (Name, Sort, Label)): SymbolicVariable
+
+  def apply(name: kale.Name, givenLabel: Label): SymbolicVariable =
+    apply((name, standard.Sort.K, givenLabel))
+
+  private var counter = 0
+
+  def freshVariable(givenLabel: Label): SymbolicVariable = {
+    counter += 1
+    generatedVariable(givenLabel, counter)
+  }
+
+  def generatedVariable(givenLabel: Label, count: Int): SymbolicVariable
+}
+
 trait Name extends kore.Name {
   override def toString = str
 }
@@ -108,6 +131,31 @@ trait Variable extends Leaf[(Name, Sort)] with kore.SortedVariable {
   override val variables: Set[Variable] = Set(this)
 }
 
+trait SymbolicVariable extends Leaf[(Name, Sort, Label)] {
+  val name: Name
+  val givenLabel: Label  // TODO: Should use the sort instead.
+
+  val label: SymbolicVariableLabel
+  override val isGround = true
+  override val sort: Sort
+  override lazy val data: (Name, Sort, Label) = (name, sort, givenLabel)
+  override lazy val isPredicate: Boolean = false
+
+  override def toString: String = name.str + (
+    if (sort.name == "K")
+      ""
+    else
+      ":" + sort.name
+    ) + ":" + givenLabel.name
+
+  override def canEqual(o: Any): Boolean = o.isInstanceOf[SymbolicVariable]
+
+  override def equals(o: Any): Boolean = o match {
+    case v: SymbolicVariable => v.name == this.name
+    case _ => false
+  }
+}
+
 trait TruthLabel extends LeafLabel[Boolean] {
   override protected[this] def internalInterpret(s: String): Boolean = s.toBoolean
 }

src/main/scala/org/kframework/kale/standard/ac.scala

@@ -141,7 +141,9 @@ case class CollectionSize(collectionLabel: CollectionLabel)(implicit env: Enviro
   override val isPredicate: Option[Boolean] = Some(false)
 }
 
-private[standard] class MonoidListLabel(val name: String, val identity: Term)(implicit val env: Environment with IntMixin) extends NonPrimitiveMonoidLabel with Constructor {
+private[standard] class MonoidListLabel(val name: String, val identity: Term)
+                                       (implicit val env: Environment with IntMixin)
+  extends NonPrimitiveMonoidLabel with Constructor {
 
   val size = CollectionSize(this)
 

src/main/scala/org/kframework/kale/standard/function.scala

@@ -83,7 +83,10 @@ trait FunctionDefinedByRewriting extends FunctionLabel with PureFunctionLabel wi
     }
 }
 
-case class FunctionDefinedByRewritingLabel0(name: String)(implicit val env: StandardEnvironment) extends FunctionDefinedByRewriting with FunctionLabel0 {
+case class FunctionDefinedByRewritingLabel0(name: String)
+                                           (implicit val env: StandardEnvironment)
+  extends FunctionDefinedByRewriting with FunctionLabel0 {
+
   def f(): Option[Term] = tryToApply(FreeNode0(this))
 }