add type inference

src/main/scala/de/tum/niwo/ExampleWorkflows.scala

@@ -39,7 +39,7 @@ object ExampleWorkflows extends LazyLogging {
       	logger.error(s"Parsing of $f unsuccessful: $spec")
       	None
       } else {
-        if (!spec.get.checkSanity()) {
+        if (!spec.get.isSane()) {
           logger.error(s"Sanity check of $f failed. Skipping file.")
         	None
         } else {
@@ -60,7 +60,7 @@ object ExampleWorkflows extends LazyLogging {
         logger.error(s"Parsing of $f unsuccessful: $spec")
         name -> None
       } else {
-        if (!spec.get.checkSanity()) {
+        if (!spec.get.isSane()) {
           logger.error(s"Sanity check of $f failed. Skipping file.")
           name -> None
         } else {

src/main/scala/de/tum/niwo/InvariantCLI.scala

@@ -44,7 +44,7 @@ object InvariantCLI extends App with LazyLogging {
       logger.error(s"Parsing of $file unsuccessful: $spec")
       None
     } else {
-      if (!spec.get.checkSanity()) {
+      if (!spec.get.isSane()) {
         logger.error(s"Sanity check of $file failed. Skipping file.")
         None
       } else {

src/main/scala/de/tum/niwo/LTLCLI.scala

@@ -33,7 +33,7 @@ object LTLCLI extends App with LazyLogging {
       logger.error(s"Parsing of $file unsuccessful: $spec")
       None
     } else {
-      if (!spec.get.checkSanity()) {
+      if (!spec.get.isSane()) {
         logger.error(s"Sanity check of $file failed. Skipping file.")
         None
       } else {

src/main/scala/de/tum/niwo/blocks/TransitionSystem.scala

@@ -3,6 +3,7 @@ package de.tum.niwo.blocks;
 import de.tum.niwo.Utils
 import de.tum.niwo.foltl.FOLTL._
 import de.tum.niwo.foltl.Properties
+import de.tum.niwo.parser.ParserUtils
 
 case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun], constants: Set[Var])
 object Signature {
@@ -11,6 +12,15 @@ object Signature {
 
 case class TransitionSystem(sig: Signature, steps: List[TSBlock]) {
   override def toString: String = steps.mkString("\n")
+
+  def isSane() = {
+
+    // check that the steps fit the signature
+    val uses = ParserUtils.allpredicates(steps)
+    val sanesteps = ParserUtils.checkSig(uses)
+
+    true
+  }
 }
 object TransitionSystem {
   val EMPTY = TransitionSystem(Signature.EMPTY, List())
@@ -36,29 +46,24 @@ object InvariantSpec {
 }
 
 abstract class Statement {
-  type This >: this.type <: Statement
-
   def guard: Formula
   def fun: String
   def tuple: List[Var]
-  def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): This
+  def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): this.type
 
   lazy val freeVars: Set[Var] = guard.freeVars ++ tuple
 }
 
 case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
-  type This = Add
   override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
   override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Add(guard, fun, tuple)
 }
 case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
-  type This = Remove
   override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
   override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Remove(guard, fun, tuple)
 
 }
 case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement {
-  type This = SetStmt
   override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";"
   override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = SetStmt(guard, fun, tuple)
 }

src/main/scala/de/tum/niwo/blocks/Workflow.scala

@@ -35,7 +35,7 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axiom
     // TODO: How to check for more constants?
   }
 
-  def checkSanity(): Boolean = {
+  def isSane(): Boolean = {
     var sane = true
 
     // TODO: check all types

src/main/scala/de/tum/niwo/parser/ParserUtils.scala

@@ -3,28 +3,47 @@ package de.tum.niwo.parser
 import com.typesafe.scalalogging.LazyLogging
 import de.tum.niwo.blocks._
 import de.tum.niwo.foltl.FOLTL._
-import de.tum.niwo.parser.WorkflowParser.inferType
 
 import scala.util.parsing.combinator.{PackratParsers, RegexParsers}
 
-trait ParserUtils extends LazyLogging {
+object ParserUtils extends LazyLogging {
 
-  def checkSig(preds: List[Fun]) = {
+  def checkSig(sig:Signature, preds: List[Fun]) = {
+
+    val sigtypes = (sig.constas ++ sig.as ++ sig.bs ++ sig.preds) map
+      (f => f.name -> f.params.map(_.typ)) toMap
+
+    val consttypes = sig.constants.map(c => c.name -> c.typ).toMap
 
     // Filter to just the first
     val grouped = preds groupBy (_.name)
 
-    // Check arities
+    // Check arities and types
     val checks = for ((k, list) <- grouped) yield {
-      val sizes = list map (_.params.size)
-      // all equal
-      (k, sizes.distinct.size == 1)
-    }
+      val sigtype = sigtypes(k)
+      val variables = list.map(_.params)
+      val types = variables.map(_.map(_.typ))
+      val checkTypes = types.forall(_ == sigtype)
+
+      if (!checkTypes) {
+        logger.error(s"Predicate $k appears with conflicting arities or types")
+      }
+
+      val invalidConstants = for (
+        list <- variables;
+        v <- list
+        if consttypes.isDefinedAt(v.name)
+        if consttypes(v.name) != v.typ
+      ) yield {
+        v
+      }
 
-    for ((k, valid) <- checks) {
-      if (!valid) {
-        logger.error(s"Predicate $k appears with conflicting arities")
+      if (invalidConstants.nonEmpty) {
+        logger.error(s"Constant use with wrong type found: $invalidConstants")
       }
+
+      // all equal
+      (k, checkTypes && invalidConstants.isEmpty)
     }
 
     // all valid?
@@ -78,12 +97,7 @@ trait ParserUtils extends LazyLogging {
     })
     val newtup = stmt.tuple.map (inferType(typemap, _))
 
-    // TODO this could be improved
-    stmt match {
-      case s:Add => Add(newguard, stmt.fun, newtup)
-      case s:Remove => Remove(newguard, stmt.fun, newtup)
-      case s:SetStmt => SetStmt(newguard, stmt.fun, newtup)
-    }
+    stmt.update(newguard, stmt.fun, newtup)
   }
 
   // TS Type inference
@@ -91,24 +105,6 @@ trait ParserUtils extends LazyLogging {
     typedpreds.map(v => v.name -> v.params.map(_.typ)).toMap
   }
 
-  def mapStatements(block:Block, pf:T => T) = {
-    block match {
-      case sim:SimpleBlock => {
-        val newsteps = sim.steps.map(pf(_))
-        sim.update(newsteps)
-      }
-      case l:Loop => {
-        val newsteps = l.steps.map(inferTypeFromSig(sig, _))
-        l.update(newsteps)
-      }
-      case c:NondetChoice => {
-        val left = c.left.map(inferTypeFromSig(sig, _))
-        val right = c.right.map(inferTypeFromSig(sig, _))
-        c.update(left, right)
-      }
-    }
-  }
-
   def inferTypeFromSig[B <: Block](sig:Signature, block:B): B = {
     block match {
       case sim:SimpleBlock => {

src/main/scala/de/tum/niwo/parser/TransitionSystemParser.scala

@@ -3,12 +3,12 @@ package de.tum.niwo.parser
 import com.typesafe.scalalogging.LazyLogging
 import de.tum.niwo.blocks._
 import de.tum.niwo.foltl.FOLTL._
-import de.tum.niwo.parser.WorkflowParser.{SPEC, parseAll}
+import ParserUtils._
 
 import scala.util.parsing.combinator.{PackratParsers, RegexParsers}
 
 object TransitionSystemParser extends RegexParsers
-  with PackratParsers with FormulaParser with ParserUtils with LazyLogging {
+  with PackratParsers with FormulaParser with LazyLogging {
 
   private def BLOCKLIST:Parser[List[TSBlock]] = (BLOCK | LOOP | NDCHOICE)+
   private def LOOP: Parser[TSLoop] = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => TSLoop(bs))
@@ -42,11 +42,17 @@ object TransitionSystemParser extends RegexParsers
     ("Signature" ~> SIG) ~
     ("Transition System" ~> BLOCKLIST) ~
     (("Axioms" ~> repsep(TERM, ","))?) ~
-    ("Invariant" ~> repsep(TERM, ",")) ^^ {
-      case sig ~ ts ~ axioms ~ invariants => {
+    ("Invariant" ~> repsep(TERM, ",")) ^? {
+      case sig ~ blocks ~ axioms ~ invariants if {
+        val infered = blocks.map(ParserUtils.inferTypeFromSig(sig, _))
+        val predicates = allpredicates(infered)
+        checkSig(sig, predicates)
+      } => {
         val axiomlist = if (axioms.isDefined) axioms.get else List()
+        val infered = blocks.map(ParserUtils.inferTypeFromSig(sig, _))
+        val ts = TransitionSystem(sig, infered)
         InvariantSpec(
-          TransitionSystem(sig, ts), And.make(axiomlist), And.make(invariants)
+          ts, And.make(axiomlist), And.make(invariants)
         )
       }
     }

src/main/scala/de/tum/niwo/parser/WorkflowParser.scala

@@ -3,6 +3,7 @@ package de.tum.niwo.parser
 import com.typesafe.scalalogging.LazyLogging
 import de.tum.niwo.blocks._
 import de.tum.niwo.foltl.FOLTL._
+import ParserUtils._
 
 import scala.util.parsing.combinator._
 
@@ -42,8 +43,10 @@ object WorkflowParser extends RegexParsers with PackratParsers with ParserUtils
     distinct && unbound.isEmpty
   }
 
-  private def ADD: Parser[Add] = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
-  private def REM: Parser[Remove] = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
+  private def ADD: Parser[Add] = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ {
+    case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
+  private def REM: Parser[Remove] = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ {
+    case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
 
   private def STMT: Parser[Statement] = ADD | REM
 
@@ -69,9 +72,16 @@ object WorkflowParser extends RegexParsers with PackratParsers with ParserUtils
   private def BLOCKLIST: Parser[List[WFBlock]] = (BLOCK | LOOP | NDCHOICE)+
 
   private def WORKFLOW: Parser[Workflow] = BLOCKLIST ^? {
-    case blocks if checkSig(allpredicates(blocks)) => {
+    case blocks if {
       val choiceblocks = addChoicePredicates(blocks)
-      Workflow(buildSig(allpredicates(choiceblocks)), choiceblocks)
+      val predicates = allpredicates(choiceblocks)
+      val sig = buildSig(predicates)
+      checkSig(sig, predicates)
+    } => {
+      val choiceblocks = addChoicePredicates(blocks)
+      val predicates = allpredicates(choiceblocks)
+      val sig = buildSig(predicates)
+      Workflow(sig, choiceblocks)
     }
   }