FOLTL.scala 4.82 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
package de.tum.workflows.foltl

Christian Müller's avatar
Christian Müller committed
3
import de.tum.workflows.Utils
4
5
import scala.annotation.tailrec

Christian Müller's avatar
Christian Müller committed
6
7
8
9
10
11
12
13
//import de.tum.workflows.foltl.TermFunctions._

object FOLTL {
  abstract class Term {
    def simplify() = TermFunctions.simplify(this)
    def freeVars() = TermFunctions.freeVars(this)
    def everywhere(trans: PartialFunction[Term, Term]) = TermFunctions.everywhere(trans, this)
    def assumeEmpty(name: String) = TermFunctions.assumeEmpty(this, name)
14
15
    def in(name: String) = TermFunctions.annotate(this, name)
    def in(name: String, ignore: Set[String]) = TermFunctions.annotate(this, name, ignore)
16
    def collect[T](coll: PartialFunction[Term, List[T]]) = TermFunctions.collect(coll, this)
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

    def bracketed(): String = this match {
      case _: BinOp => "(" + this + ")"
      case _        => this.toString()
    }

    def pretty(): String = {
      val s = this.toString
      val broken = s replace ("∧ ", "∧ \n")

      // indent
      var opens = 0;

      val indented = for (line <- broken.lines) yield {
        val indent = " " * (opens * 2)
        val ret = indent + line
        opens += line.count(_ == '(')
        opens -= line.count(_ == ')')

        ret
      }
      indented.reduce(_ + "\n" + _)
Christian Müller's avatar
Christian Müller committed
39
40
41
42
43
44
45
46
47
    }
  }

  case object True extends Term
  case object False extends Term

  case class Var(name: String) extends Term {
    override def toString() = name
  }
48

Christian Müller's avatar
Christian Müller committed
49
  object Fun {
50
    def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
Christian Müller's avatar
Christian Müller committed
51
  }
52
  case class Fun(name: String, ind: Option[String], params: List[Var]) extends Term {
Christian Müller's avatar
Christian Müller committed
53
    override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.mkString("(", ",", ")")
Christian Müller's avatar
Christian Müller committed
54
55
56
57
58
59
60
  }

  trait Quantifier extends Term {
    def qmake: (List[Var], Term) => Quantifier
    def qname: String
    def vars: List[Var]
    def t: Term
61

Christian Müller's avatar
Christian Müller committed
62
63
64
65
    override def toString() = {
      qname + " " + vars.mkString(",") + ". " + t.bracketed()
    }
  }
66

Christian Müller's avatar
Christian Müller committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
  object Quantifier {
    def unapply(q: Quantifier) = Some((q.qmake, q.vars, q.t))
  }

  case class Exists(vars: List[Var], t: Term) extends Quantifier {
    val qname = "∃"
    val qmake = Exists.apply _
  }
  case class Forall(vars: List[Var], t: Term) extends Quantifier {
    val qname = "∀"
    val qmake = Forall.apply _
  }

  trait TemporalTerm extends Term

82
  case class Next(t: Term) extends TemporalTerm with UnOp {
Christian Müller's avatar
Christian Müller committed
83
84
    val make = Next.apply _
    val opname = "X"
Christian Müller's avatar
Christian Müller committed
85
  }
Christian Müller's avatar
Christian Müller committed
86
87
88
  case class Globally(t: Term) extends TemporalTerm with UnOp {
    val make = Globally.apply _
    val opname = "G"
Christian Müller's avatar
Christian Müller committed
89
  }
Christian Müller's avatar
Christian Müller committed
90
91
92
93

  case class Finally(t: Term) extends TemporalTerm with UnOp {
    val make = Finally.apply _
    val opname = "F"
Christian Müller's avatar
Christian Müller committed
94
  }
95

Christian Müller's avatar
Christian Müller committed
96
97
98
99
  case class Until(t1: Term, t2: Term) extends TemporalTerm with BinOp {
    val make = Until.apply _
    val opname = "U"
  }
100

Christian Müller's avatar
Christian Müller committed
101
  trait UnOp extends Term {
102
    def make: Term => UnOp
Christian Müller's avatar
Christian Müller committed
103
104
    def opname: String
    def t: Term
105

Christian Müller's avatar
Christian Müller committed
106
107
    override def toString() = opname + " " + t.bracketed()
  }
108

Christian Müller's avatar
Christian Müller committed
109
110
111
  object UnOp {
    def unapply(unop: UnOp) = {
      Some((unop.make, unop.t))
Christian Müller's avatar
Christian Müller committed
112
113
114
115
    }
  }

  trait BinOp extends Term {
116
    def make: (Term, Term) => BinOp
Christian Müller's avatar
Christian Müller committed
117
118
    def opname: String
    def t1: Term
119
120
    def t2: Term

Christian Müller's avatar
Christian Müller committed
121
122
    override def toString() = {
      (t1, t2) match {
123
        case (t1: BinOp, t2: BinOp) if (opname == t1.opname && opname == t2.opname) => t1 + " " + opname + " " + t2
Christian Müller's avatar
Christian Müller committed
124
        case (t1: BinOp, _) if (opname == t1.opname) => t1 + " " + opname + " " + t2.bracketed()
125
        case (_, t2: BinOp) if (opname == t2.opname) => t1.bracketed() + " " + opname + " " + t2
Christian Müller's avatar
Christian Müller committed
126
127
128
129
        case _ => t1.bracketed() + " " + opname + " " + t2.bracketed()
      }
    }
  }
130

Christian Müller's avatar
Christian Müller committed
131
132
133
134
  object BinOp {
    def unapply(binop: BinOp) = {
      Some((binop.make, binop.t1, binop.t2))
    }
135
136

    def makeL(make: (Term, Term) => Term, l: Seq[Term], Empty: Term): Term = {
Christian Müller's avatar
Christian Müller committed
137
      l.toList match {
138
139
140
141
        case List(x)     => x
        case Empty :: xs => makeL(make, xs, Empty)
        case x :: xs     => make(x, makeL(make, xs, Empty))
        case List()      => Empty
Christian Müller's avatar
Christian Müller committed
142
143
144
      }
    }
  }
145
  
146
147
  object Or {
    def make(terms: List[Term]) = {
Christian Müller's avatar
Christian Müller committed
148
149
150
      BinOp.makeL(Or.apply _, terms, True)
    }
    def make(terms: Term*) = {
151
152
153
      BinOp.makeL(Or.apply _, terms, False)
    }
  }
154
  
Christian Müller's avatar
Christian Müller committed
155
156
157
158
  case class Or(t1: Term, t2: Term) extends BinOp {
    val opname = "∨"
    val make = Or.apply _
  }
159
  
160
161
162
163
  object And {
    def make(terms: List[Term]) = {
      BinOp.makeL(And.apply _, terms, True)
    }
Christian Müller's avatar
Christian Müller committed
164
165
166
    def make(terms: Term*) = {
      BinOp.makeL(And.apply _, terms, True)
    }
167
  }
168
  
Christian Müller's avatar
Christian Müller committed
169
170
171
172
  case class And(t1: Term, t2: Term) extends BinOp {
    val opname = "∧"
    val make = And.apply _
  }
173
174
  
  case class Eq(t1: Term, t2: Term) extends BinOp {
Christian Müller's avatar
Christian Müller committed
175
176
177
    val opname = "↔"
    val make = Eq.apply _
  }
178
  
Christian Müller's avatar
Christian Müller committed
179
180
181
182
183
184
  case class Implies(t1: Term, t2: Term) extends BinOp {
    val opname = "→"
    val make = Implies.apply _
  }

  case class Neg(t: Term) extends UnOp {
Christian Müller's avatar
Christian Müller committed
185
    val make = Neg.apply _
Christian Müller's avatar
Christian Müller committed
186
187
188
189
    val opname = "¬"
  }

}