develop

.gitignore

@@ -1,3 +1,6 @@
 target
 .idea
-
+/z3
+.DS_Store
+/src/test/scala/org/kframework/test.sc
+/npm-debug.log

DEVELOPER_GUIDE.md

@@ -0,0 +1,50 @@
+## Building
+
+Clone the repository (recursively to include submodules) and then build using
+`sbt`. Use the `develop` branch if you intend to create pull requests: 
+
+```
+git clone --recurse-submodules https://github.com/kframework/kale --branch develop
+sbt compile
+```
+
+These git configuration settings smoothen out working with submodules:
+
+```
+git config --global push.recurseSubmodules check
+git config --global fetch.recurseSubmodules true
+```
+
+If you intend to push to the `kore` repository too, using you SSH adding:
+
+```
+[url "[email protected].:"]
+    pushInsteadOf = https://github.com/
+```
+
+to your `~/.gitconfig` will let you do that.
+
+
+## Guide on adding a new feature to terms/labels
+
+In an `if-then-elseif-...` style:
+
+#### Is it very specific to your use/project?
+
+Leave it in your project / out of the Scala backend.
+
+#### It it only invoked occasionally, performance is not critical?
+
+Put it in Rich* (`org.kframework.kale` package object)
+
+#### Performance is important?
+
+Create an `Environment` `Mixin` and use `Unary` or `Binary`.  
+
+#### Do you think the feature is extremely important and should be in the main trait hierarchy, not a mixin?
+
+**Talk with a few other developers before putting it there!!!**
+
+#### Do you an idea of how we could move functionality out of the main trait hierarchy into a Mixin?
+
+**Let's talk about it!**

LICENSE.md

@@ -0,0 +1,61 @@
+<!-- Copyright (c) 2010-2016 K Team. All Rights Reserved. -->
+==============================================================================
+The K Release License
+==============================================================================
+University of Illinois/NCSA
+Open Source License
+
+Copyright (c) 2009-2015 University of Illinois at Urbana-Champaign.
+All rights reserved.
+
+Developed by:
+
+    K Team
+
+    University of Illinois at Urbana-Champaign
+    Runtime Verification, Inc.
+    Iuvo AI, Inc.
+
+    http://kframework.org
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal with
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+* Redistributions of source code must retain the above copyright notice,
+      this list of conditions and the following disclaimers.
+
+* Redistributions in binary form must reproduce the above copyright notice,
+      this list of conditions and the following disclaimers in the
+      documentation and/or other materials provided with the distribution.
+
+* Neither the names of the K Team, the University of Illinois at
+      Urbana-Champaign, the University Alexandru-Ioan Cuza, nor the names of
+      its contributors may be used to endorse or promote products derived from
+      this Software without specific prior written permission.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE
+SOFTWARE.
+
+==============================================================================
+Copyrights and Licenses for Third Party Software Distributed with K:
+==============================================================================
+The K software contains code written by third parties. Such software will have
+its own individual LICENSE file in the directory in which it appears. This
+file will describe the copyrights, license, and restrictions which apply to
+that code.
+
+The disclaimer of warranty in the University of Illinois Open Source License
+applies to all code in the K Distribution, and nothing in any of the other
+licenses gives permission to use the names of the K Team, the
+University of Illinois, or the University Alexandru-Ioan Cuza to endorse or
+promote products derived from this Software.
+

README.md

@@ -0,0 +1,9 @@
+[ ![Codeship Status for kframework/kale](https://app.codeship.com/projects/8a5162d0-1588-0135-d42f-6a6f9a84ad3f/status?branch=develop)](https://app.codeship.com/projects/217943)
+
+# K Scala Backend
+
+# Install
+
+# Use
+
+# Contribute

build.sbt

@@ -3,18 +3,37 @@ organization := "org.kframework"
 
 name := "kale"
 
-scalaVersion := "2.12.2"
+scalaVersion := "2.12.4"
 
 resolvers += "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
 
-resolvers += "Local Maven Repository" at "file://" + Path.userHome.absolutePath + "/.m2/repository"
+resolvers += Resolver.mavenLocal
+
+lazy val kale = project.in(file("."))
 
 libraryDependencies ++= Seq(
-  "org.scalatest" %% "scalatest" % "3.0.1" % "test",
+  "org.typelevel" %% "discipline" % "0.7.+" % "test",
+  "org.scalatest" %% "scalatest" % "3.0.+" % "test",
+
+  "org.typelevel" %% "cats-core" % "1.0.+",
+  "org.typelevel" %% "cats-laws" % "1.0.+" % "test",
+  "org.typelevel" %% "kittens" % "1.0.+",
 
-  "io.circe" %% "circe-core" % "0.7.0",
-  "io.circe" %% "circe-generic" % "0.7.0",
-  "io.circe" %% "circe-parser" % "0.7.0",
+  "org.typelevel"  %% "squants"  % "1.3.0",
 
-  "org.kframework.k" %% "kore" % "1.0-SNAPSHOT"
+  "org.roaringbitmap" % "RoaringBitmap" % "0.6.+",
+
+  "io.circe" %% "circe-core" % "0.9.+",
+  "io.circe" %% "circe-parser" % "0.9.+"
 )
+
+lazy val installZ3 = taskKey[Unit]("Install Z3 theorem prover")
+
+installZ3 := {
+  "./installZ3.sh" !
+}
+
+(test in Test) := (test in Test).dependsOn(installZ3).value
+
+// Your profile name of the sonatype account. The default is the same with the organization value
+sonatypeProfileName := "org.kframework.kale"

installZ3.sh

@@ -0,0 +1,18 @@
+#!/bin/sh
+
+if [ ! -d ./z3 ]; then
+
+    URL="https://github.com/Z3Prover/z3/releases/download/z3-4.5.0/"
+    FORMAT=".zip"
+
+    if [ `uname` = "Linux" ]; then
+        EXECUTABLE="z3-4.5.0-x64-ubuntu-14.04"
+
+
+    elif [ `uname` = "Darwin" ]; then
+        EXECUTABLE="z3-4.5.0-x64-osx-10.11.6"
+    fi
+
+    curl -OL $URL$EXECUTABLE$FORMAT && unzip $EXECUTABLE$FORMAT && mv $EXECUTABLE"/" z3 && rm $EXECUTABLE$FORMAT
+
+fi

project/build.properties

@@ -0,0 +1 @@
+sbt.version=0.13.15

sonatype.sbt

@@ -1,5 +1,3 @@
-// Your profile name of the sonatype account. The default is the same with the organization value
-sonatypeProfileName := "org.kframework.kale"
 
 // To sync with Maven central, you need to supply the following information:
 pomExtra in Global := {

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

@@ -1,30 +1,50 @@
 package org.kframework.kale
 
-import org.kframework.kale.standard.{Bottomize, Name, Sort}
-import org.kframework.kore
+import org.kframework.kale.highcats.LiftedCatsMixin
+import org.kframework.kale.standard.BottomizeMixin
+import org.kframework.kale.transformer.Binary.{Apply, ProcessingFunctions}
+import org.kframework.kale.transformer.{Binary, Unary}
 
-import scala.collection._
+trait Environment extends Foundation with RoaringMixin with HasMatcher with MatchingLogicMixin with LiftedCatsMixin with BottomizeMixin
 
-trait Environment extends KORELabels with Bottomize {
+trait Foundation {
+  _: Environment =>
 
-  trait HasEnvironment {
-    val env = Environment.this
-  }
+  implicit protected val env: this.type = this
 
-  val uniqueLabels = mutable.Map[String, Label]()
+  val uniqueLabels = collection.mutable.Map[String, Label]()
 
-  def labels = uniqueLabels.values.toSet
+  def labels: Set[Label] = if (isSealed) {
+    labelSet
+  } else {
+    uniqueLabels.values.toSet
+  }
 
+  private lazy val labelSet = uniqueLabels.values.toSet
   private var pisSealed = false
 
-  def seal(): Unit = pisSealed = true
+  var _matcher: Binary.Apply = _
+
+  def seal(): Unit = {
+    pisSealed = true
+  }
 
   def isSealed = pisSealed
 
+  def unaryProcessingFunctions: Unary.ProcessingFunctions = Unary.processingFunctions
+
   val substitutionMaker: Substitution => SubstitutionApply
 
+  final val unify: Label2 = lift("unify", {
+    (a: Term, b: Term) =>
+      assert(this.isSealed)
+      unifier(a, b)
+  })
+
+  def unifier: Binary.Apply
+
   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))
@@ -36,29 +56,52 @@ trait Environment extends KORELabels with Bottomize {
 
   def label(labelName: String): Label = uniqueLabels(labelName)
 
-  def sort(l: Label, children: Seq[Term]): Sort
-
-  def sortArgs(l: Label): Seq[Sort]
-
-  def sortTarget(l: Label): Sort
+  lazy val labelForIndex: Map[Int, Label] = labels map { l => (l.id, l) } toMap
 
   override def toString = {
     "nextId: " + uniqueLabels.size + "\n" + uniqueLabels.mkString("\n")
   }
-}
 
-trait KORELabels {
-  // Constants
-  val Bottom: Truth with kore.Bottom
-  val Top: Truth with Substitution with kore.Top
-
-  // Labels
-  val Variable: VariableLabel
-  val And: AndLabel
-  val Or: OrLabel
-  val Rewrite: RewriteLabel
-  val Equality: EqualityLabel
-  val Truth: TruthLabel
-  val Not: NotLabel
+  def rewrite(rule: Term, obj: Term): Term
+
 }
 
+trait HasMatcher extends Mixin {
+  env: Environment =>
+
+  case class NoMatch(solver: Apply) extends Binary.F({ (a: Term, b: Term) => Bottom })
+
+  case class LeaveAlone(solver: Apply) extends Binary.F({ (a: Term, b: Term) => And(a, b) })
+
+  case class AssertNotPossible(solver: Apply) extends Binary.F({ (a: Term, b: Term) => throw new AssertionError("Should not try to match " + a + " with " + b) })
+
+  private var _registeredMatchers: Map[Binary.ProcessingFunctions, Int] = collection.immutable.ListMap()
+
+  object Priority {
+    val low = 30
+    val medium = 50
+    val high = 80
+    val ultimate = 200
+  }
+
+  def registeredMatchers = _registeredMatchers
+
+  def registerInner(matcher: Binary.ProcessingFunctions, priority: Int) {
+    _registeredMatchers = _registeredMatchers + (matcher -> priority)
+  }
+
+  def registerMatcher[Process <: Apply, A <: Term, B <: Term](f: PartialFunction[(Label, Label), Process => (A, B) => Term], priority: Int) = {
+    registerInner(Binary.definePartialFunction(f), priority)
+  }
+
+  final lazy val makeMatcher: Binary.ProcessingFunctions = {
+    registeredMatchers
+      .groupBy(_._2)
+      .mapValues(_.keySet)
+      .toList
+      .sortBy(-_._1)
+      .map(_._2)
+      .map(_.reduce(_ orElse _))
+      .reduceLeft(_ orElse _)
+  }
+}