use Hooking mechanism in develop

src/main/scala/org/kframework/backend/skala/SkalaBackend.scala

@@ -62,35 +62,7 @@ object Encodings {
 object Hook {
   def apply(s: kore.SymbolDeclaration)(implicit env: StandardEnvironment): Option[Label] = {
     s.att.getSymbolValue(Encodings.hook) match {
-      case Some(v) => v.str match {
-        case "INT.Int" => Some(env.INT)
-        case "INT.add" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x + y))
-        case "INT.sub" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x - y))
-        case "INT.ediv" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x / y))
-        case "INT.tmod" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x % y))
-        case "INT.abs" => Some(PrimitiveFunction1(s.symbol.str, env.INT, env.INT, (x: Int) => math.abs(x)))
-        case "INT.shr" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x >> y))
-        case "INT.not" => Some(PrimitiveFunction1(s.symbol.str, env.INT, env.INT, (x: Int) => ~x))
-        case "INT.xor" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x ^ y))
-        case "INT.ne" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x != y))
-        case "INT.gt" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x > y))
-        case "INT.ge" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x >= y))
-        case "INT.lt" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x < y))
-        case "INT.le" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x <= y))
-        case "BOOL.or" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x || y))
-        case "BOOL.and" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x && y))
-        case "BOOL.xor" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x ^ y))
-        case "BOOL.ne" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x != y))
-        case "BOOL.not" => Some(PrimitiveFunction1(s.symbol.str, env.BOOLEAN, (x: Boolean) => !x))
-        case "BOOL.eq" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x == y))
-        case "BOOL.implies" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => !x || y))
-        //Todo: How to handle these?
-        case "BOOL.orElse" => Some(SimpleFreeLabel2(s.symbol.str))
-        case "BOOL.andThen" => Some(SimpleFreeLabel2(s.symbol.str))
-        case "KString" => Some(SimpleFreeLabel1(s.symbol.str))
-        case "#KRewrite" => Some(FunctionDefinedByRewritingLabel2(s.symbol.str))
-        case _ => None
-      }
+      case Some(kore.Value(v)) => env.uniqueLabels.get(v)
       case None => None
     }
   }

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

@@ -7,6 +7,8 @@ import scala.collection._
 
 trait Environment extends KORELabels with Bottomize {
 
+  implicit protected val env: this.type = this
+
   trait HasEnvironment {
     val env = Environment.this
   }
@@ -31,7 +33,7 @@ trait Environment extends KORELabels with Bottomize {
   protected val unifier: MatcherOrUnifier
 
   def register(label: Label): Int = {
-    assert(!isSealed, "The environment is sealed")
+    assert(!isSealed, "Cannot register label " + label + " because the environment is sealed")
     assert(label != null)
 
     if (uniqueLabels.contains(label.name))
@@ -52,6 +54,15 @@ trait Environment extends KORELabels with Bottomize {
   override def toString = {
     "nextId: " + uniqueLabels.size + "\n" + uniqueLabels.mkString("\n")
   }
+
+  def SMTName(l: Label): String
+
+  def isZ3Builtin(l: Label): Boolean
+
+  implicit class WithSMTname(l: Label) {
+    def smtName: String = SMTName(l)
+  }
+
 }
 
 trait KORELabels {

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

@@ -1,12 +1,20 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.Environment
+import org.kframework.kale.{DomainValue, Environment, Label, builtin}
 import org.kframework.kale.standard.ReferenceLabel
 
-trait HasBOOLEAN {
-  self: Environment =>
-
-  val BOOLEAN = new ReferenceLabel[Boolean]("Boolean")(this) {
+case class BOOLEAN()(implicit penv: Environment) extends Module("BOOLEAN") {
+  val Boolean = new ReferenceLabel[Boolean]("Boolean") {
     override protected[this] def internalInterpret(s: String): Boolean = s.toBoolean
   }
+
+  override val all: Set[Label] = Set(Boolean)
+}
+
+trait importBOOLEAN {
+  protected val env: Environment
+
+  val BOOLEAN = builtin.BOOLEAN()(env)
+
+  implicit def toBoolean(b: Boolean): DomainValue[Boolean] = BOOLEAN.Boolean(b)
 }

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

@@ -1,27 +1,28 @@
 package org.kframework.kale.builtin
 
 import org.kframework.kale.standard.ReferenceLabel
-import org.kframework.kale.{Environment, FunctionLabel2, Term}
+import org.kframework.kale.util.Named
+import org.kframework.kale.{FunctionLabel2, _}
 
-trait HasDOUBLE {
-  self: Environment =>
-
-  val DOUBLE = new ReferenceLabel[Double]("Double")(this) {
+case class DOUBLE()(implicit protected val penv: Environment) extends Module("DOUBLE") {
+  val Double = new ReferenceLabel[Double]("Double")(penv) {
     override protected[this] def internalInterpret(s: String): Double = s.toDouble
   }
-}
 
-trait HasDOUBLEdiv {
-  self: Environment with HasDOUBLE =>
-
-  val DOUBLEdiv = new HasEnvironment with FunctionLabel2 {
+  val div = new Named("_/Double_") with FunctionLabel2 {
     def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (_, DOUBLE(0)) => None
-      case (DOUBLE(0), b) if b.isGround => Some(DOUBLE(0))
-      case (DOUBLE(a), DOUBLE(b)) => Some(DOUBLE(a / b))
+      case (_, Double(0)) => None
+      case (Double(0), b) if b.isGround => Some(Double(0))
+      case (Double(a), Double(b)) => Some(Double(a / b))
       case _ => None
     }
-
-    override val name: String = "_/Double_"
   }
+
+  override lazy val all: Set[Label] = Set(Double)
+}
+
+trait importDOUBLE {
+  protected val env: Environment
+
+  val DOUBLE = builtin.DOUBLE()(env)
 }

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

@@ -1,14 +1,21 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.{DomainValue, Environment}
+import org.kframework.kale.{DomainValue, Environment, Label}
 import org.kframework.kale.standard.ReferenceLabel
+import org.kframework.kale.builtin
 
-trait HasID {
-  self: Environment =>
-
-  val ID = new ReferenceLabel[Symbol]("ID")(this) {
+case class ID()(implicit protected val penv: Environment) extends Module("ID")   {
+  val Id = new ReferenceLabel[Symbol]("Id")(penv) {
     override protected[this] def internalInterpret(s: String): Symbol = Symbol(s)
   }
+  override val all: Set[Label] = Set(Id)
+}
+
+trait importID {
+  protected val env: Environment
+
+  val ID = builtin.ID()(env)
+
+  implicit def toID(s: Symbol): DomainValue[Symbol] = ID.Id(s)
 
-  implicit def toID(s: Symbol): DomainValue[Symbol] = ID(s)
 }

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

@@ -1,111 +1,34 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.standard.ReferenceLabel
-import org.kframework.kale.util.Named
 import org.kframework.kale._
+import org.kframework.kale.standard.ReferenceLabel
 
-trait HasINT {
-  self: Environment =>
-
-  val INT = new ReferenceLabel[Int]("Int")(this) {
-    override protected[this] def internalInterpret(s: String): Int = s.toInt
-  }
-
-  implicit def toINT(i: Int): DomainValue[Int] = INT(i)
-}
-
-trait HasINTbop extends HasINTplus with HasINTminus with HasINTmult with HasINTdiv with HasINTmod { self: Environment => }
-
-trait HasINTplus extends HasINT { self: Environment =>
-  val intPlus = new Named("_+Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a + b))
-      case _ => None
-    }
-    override def smtName: String = "+"
-  }
-}
-
-trait HasINTminus extends HasINT { self: Environment =>
-  val intMinus = new Named("_-Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a + b))
-      case _ => None
-    }
-    override def smtName: String = "-"
-  }
-}
-
-trait HasINTmult extends HasINT { self: Environment =>
-  val intMult = new Named("_*Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a * b))
-      case _ => None
-    }
-    override def smtName: String = "*"
-  }
-}
+case class INT(implicit protected val penv: Environment with importBOOLEAN) extends Module("INT") {
 
-trait HasINTdiv extends HasINT { self: Environment =>
-  val intDiv = new Named("_/Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-    //case (_, INT(0)) => None
-    //case (INT(0), b) if b.isGround => Some(INT(0))
-      case (INT(a), INT(b)) => Some(INT(a / b))
-      case _ => None
-    }
-    override def smtName: String = "div" // integer division, while "/" is real division.
-  }
-}
+  import penv._
 
-trait HasINTmod extends HasINT { self: Environment =>
-  val intMod = new Named("_%Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a % b))
-      case _ => None
-    }
-    override def smtName: String = "mod" // z3 also has "rem", remainder.
+  val Int = new ReferenceLabel[Int]("Int") {
+    override protected[this] def internalInterpret(s: String): Int = s.toInt
   }
-}
 
-trait HasINTcmp extends HasINTlt with HasINTle with HasINTgt with HasINTge { self: Environment => }
+  val plus = PrimitiveFunction2[Int]("_+Int_", Int, _ + _)
+  val minus = PrimitiveFunction2[Int]("_-Int_", Int, _ - _)
+  val mult = PrimitiveFunction2[Int]("_*Int_", Int, _ * _)
+  val div = PrimitiveFunction2[Int]("_/Int_", Int, _ / _)
+  val mod = PrimitiveFunction2[Int]("_%Int_", Int, _ / _)
+  val lt = PrimitiveFunction2[Int, Boolean]("_<Int_", Int, BOOLEAN.Boolean, _ < _)
+  val le = PrimitiveFunction2[Int, Boolean]("_<=Int_", Int, BOOLEAN.Boolean, _ <= _)
+  val gt = PrimitiveFunction2[Int, Boolean]("_>Int_", Int, BOOLEAN.Boolean, _ > _)
+  val ge = PrimitiveFunction2[Int, Boolean]("_>=Int_", Int, BOOLEAN.Boolean, _ >= _)
 
-trait HasINTlt extends HasINT with HasBOOLEAN { self: Environment =>
-  val intLt = new Named("_<Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a < b))
-      case _ => None
-    }
-    override def smtName: String = "<"
-  }
+  lazy val all = Set(Int, plus, minus, mult, div, mod, lt, le, gt, ge)
 }
 
-trait HasINTle extends HasINT with HasBOOLEAN { self: Environment =>
-  val intLe = new Named("_<=Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a <= b))
-      case _ => None
-    }
-    override def smtName: String = "<="
-  }
-}
+trait importINT {
+  protected val env: Environment with importBOOLEAN
+  val BOOLEAN: builtin.BOOLEAN
 
-trait HasINTgt extends HasINT with HasBOOLEAN { self: Environment =>
-  val intGt = new Named("_>Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a > b))
-      case _ => None
-    }
-    override def smtName: String = ">"
-  }
-}
+  val INT = builtin.INT()(env)
 
-trait HasINTge extends HasINT with HasBOOLEAN { self: Environment =>
-  val intGe = new Named("_>=Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a >= b))
-      case _ => None
-    }
-    override def smtName: String = ">="
-  }
+  implicit def toINT(i: Int): DomainValue[Int] = INT.Int(i)
 }

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

@@ -0,0 +1,16 @@
+package org.kframework.kale.builtin
+
+import org.kframework.kale.{Environment, Label, util}
+
+abstract class Module(val moduleName: String)(implicit val env: Environment) {
+
+  private def fullname(localName: String): String = localName + "@" + moduleName
+
+  protected abstract class LocalName[E <: Environment](val localName: String) extends util.Named(fullname(localName))
+
+  val all: Set[Label]
+
+  private lazy val labelName2Label = all.map(l => (l.name, l)).toMap
+
+  def apply(localName: String): Label = labelName2Label(fullname(localName))
+}

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

@@ -4,7 +4,7 @@ import org.kframework.kale._
 
 import scala.collection.{Iterable, Set}
 
-case class SetLabel(name: String, identity: Term)(implicit val env: Environment with HasBOOLEAN) extends AssocWithIdLabel {
+case class SetLabel(name: String, identity: Term)(implicit val env: Environment with importBOOLEAN) extends AssocWithIdLabel {
   override def construct(l: Iterable[Term]): Term = SET(this, l.toSet)
 
   trait HasEnvironment {
@@ -23,7 +23,7 @@ case class SetLabel(name: String, identity: Term)(implicit val env: Environment
     val name = SetLabel.this.name + ".in"
   } with HasEnvironment with FunctionLabel2 {
     def f(s: Term, key: Term) = s match {
-      case set(elements) => Some(env.BOOLEAN(elements.contains(key)))
+      case set(elements) => Some(env.BOOLEAN.Boolean(elements.contains(key)))
     }
   }
 

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

@@ -1,14 +1,21 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.{DomainValue, Environment}
+import org.kframework.kale.{DomainValue, Environment, Label}
 import org.kframework.kale.standard.ReferenceLabel
+import org.kframework.kale.builtin
 
-trait HasSTRING {
-  self: Environment =>
-
-  val STRING = new ReferenceLabel[String]("String")(this) {
+case class STRING()(implicit protected val penv: Environment) extends Module("STRING")   {
+  val String = new ReferenceLabel[String]("String")(penv) {
     override protected[this] def internalInterpret(s: String): String = s
   }
+  override val all: Set[Label] = Set(String)
+}
+
+trait importSTRING {
+  protected val env: Environment
+
+  val STRING = builtin.STRING()(env)
+
+  implicit def toSTRING(s: String): DomainValue[String] = STRING.String(s)
 
-  implicit def toSTRING(s: String): DomainValue[String] = STRING(s)
 }