ParserUtils.scala 5.33 KB
Newer Older
1 2 3 4 5 6 7 8
package de.tum.niwo.parser

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._

import scala.util.parsing.combinator.{PackratParsers, RegexParsers}

Christian Müller's avatar
Christian Müller committed
9
object ParserUtils extends LazyLogging {
10

11 12 13 14 15 16 17 18 19
  def checkSig(sig:Signature, form:Formula):Boolean = {
    val uses = form.collect {
      case f:Fun => List(f)
    }
    // TODO: we might add checking equal types for (a = b)
    checkSig(sig, uses)
  }

  def checkSig(sig:Signature, preds: List[Fun]): Boolean = {
Christian Müller's avatar
Christian Müller committed
20 21 22 23 24

    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
25 26 27 28

    // Filter to just the first
    val grouped = preds groupBy (_.name)

Christian Müller's avatar
Christian Müller committed
29
    // Check arities and types
30
    val checks = for ((k, list) <- grouped) yield {
Christian Müller's avatar
Christian Müller committed
31 32 33 34
      val sigtype = sigtypes(k)
      val variables = list.map(_.params)
      val types = variables.map(_.map(_.typ))
      val checkTypes = types.forall(_ == sigtype)
35

Christian Müller's avatar
Christian Müller committed
36 37
      if (!checkTypes) {
        logger.error(s"Predicate $k appears with conflicting arities or types")
38
        logger.error(s"Usage: ${list.map(_.toTypedString)}")
39
      }
Christian Müller's avatar
Christian Müller committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55

      val invalidConstants = for (
        list <- variables;
        v <- list
        if consttypes.isDefinedAt(v.name)
        if consttypes(v.name) != v.typ
      ) yield {
        v
      }

      if (invalidConstants.nonEmpty) {
        logger.error(s"Constant use with wrong type found: $invalidConstants")
      }

      // all equal
      (k, checkTypes && invalidConstants.isEmpty)
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
    }

    // all valid?
    checks.forall(x => x._2)
  }

  def buildSig(preds: List[Fun]) = {
    // Filter to just the first
    val filtered = preds.groupBy(_.name).map(_._2.head).toSet
    val oracles = filtered.filter(_.isOracle)
    val constinputs = filtered.filter(_.isConstInput)
    val bs = filtered.filter(_.isB)
    val rels = filtered -- oracles -- constinputs -- bs
    Signature(oracles, constinputs, bs, rels, Set())
  }

  def typeMap(typedvars: List[Var]) = {
    typedvars.map(v => v.name -> v.typ).toMap
  }

  def inferType(typemap: Map[String, String], v:Var) = {
    Var(v.name, typemap(v.name))
  }

  def allpredicates(list: List[Block]): List[Fun] = {
81
    def predicatesStmt(s: Statement[_]):Set[Fun] = {
82 83 84 85
      // collect from guard
      val inguard = s.guard.collect({
        case f:Fun => List(f)
      })
86
      // function to be updated
87
      val ch = Fun(s.fun, s.tuple)
88
      (ch :: inguard).toSet
89 90 91 92
    }

    def predicates(b: Block): Set[Fun] = {
      b match {
93 94 95
        case b:SimpleBlock[_, _] => b.steps.flatMap(predicatesStmt).toSet
        case l:Loop[_, _] => l.steps.flatMap(predicates).toSet
        case c:NondetChoice[_, _] => (c.left.flatMap(predicates) ++ c.right.flatMap(predicates)).toSet
96 97 98 99 100 101
      }
    }

    list flatMap predicates
  }

102
  def inferTypes(typemap: Map[String, String], stmt: Statement[_]): Statement[_] = {
103 104 105 106 107 108

    val newguard = stmt.guard.everywhere({
      case Fun(n, tr, params) => Fun(n, tr, params map (inferType(typemap, _)))
    })
    val newtup = stmt.tuple.map (inferType(typemap, _))

Christian Müller's avatar
Christian Müller committed
109
    stmt.update(newguard, stmt.fun, newtup)
110 111 112 113 114 115 116
  }

  // TS Type inference
  def predtypeMap(typedpreds: Set[Fun]) = {
    typedpreds.map(v => v.name -> v.params.map(_.typ)).toMap
  }

117 118 119 120
  def inferBlockTypeFromSig[B <: Block](sig:Signature, block:B): B = {
    val b = block match {
      case sim:SimpleBlock[_,_] => {
        val newsteps = sim.steps.map(inferStmtTypeFromSig(sig, _))
Christian Müller's avatar
stuff  
Christian Müller committed
121 122
        sim.update(newsteps)
      }
123 124
      case l:Loop[_, a] => {
        val newsteps = l.steps.map(inferBlockTypeFromSig(sig, _))
Christian Müller's avatar
stuff  
Christian Müller committed
125 126
        l.update(newsteps)
      }
127 128 129
      case c:NondetChoice[_, a] => {
        val left = c.left.map(inferBlockTypeFromSig(sig, _))
        val right = c.right.map(inferBlockTypeFromSig(sig, _))
Christian Müller's avatar
stuff  
Christian Müller committed
130 131 132
        c.update(left, right)
      }
    }
133 134
    // FIXME: sigh ... is there a way to do type preservation here?
    b.asInstanceOf[B]
Christian Müller's avatar
stuff  
Christian Müller committed
135 136
  }

137
  def inferStmtTypeFromSig[T <: Statement[_]](sig:Signature, stmt:T): T = {
138 139 140

    val map = predtypeMap(sig.preds ++ sig.as ++ sig.constas ++ sig.bs)

141 142 143 144 145 146 147
    val repl = (stmt.tuple.map(_.name).zip(map(stmt.fun)) ++ sig.constants.map(v => (v.name, v.typ))).toMap

    def addTypes(tuple: List[Var]): List[Var] = {
      if (tuple.exists(v => !repl.isDefinedAt(v.name))) {
        logger.error(s"Variables from $tuple not defined in type inference map $repl")
      }
      tuple.map(v => Var(v.name, repl(v.name)))
148
    }
149

150
    val newguard = stmt.guard.everywhere {
151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
      case Fun(n, tr, params) => Fun(n, tr, addTypes(params))
      case v:Var => addTypes(List(v)).head
    }
    val newtup = addTypes(stmt.tuple)

    val s = stmt.update(guard = newguard, tuple = newtup)

    // FIXME: sigh ... is there a way to do type preservation here?
    s.asInstanceOf[T]
  }

  def inferFormulaTypes(sig:Signature, f:Formula):Formula = {

    def infer(g:Formula, map:Map[String, String]):Formula = {
      g everywhere {
        case Quantifier(make, vars, inner) =>
          val newmap = map ++ vars.map(v => v.name -> v.typ)
          make(vars, infer(inner, newmap))
        case fun:Fun => fun.updatedParams(fun.params.map(v => Var(v.name, map(v.name))))
        case v:Var => Var(v.name, map(v.name))
      }
172 173
    }

174 175 176
    // start with constant map, fill map along quantifiers
    val map = sig.constants.map(v => v.name -> v.typ).toMap
    infer(f, map)
177 178
  }
}