FOLTL.scala 5.66 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
    def opsize() = TermFunctions.opsize(this)
18
19
20
21
22
23
24
25

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

    def pretty(): String = {
      val s = this.toString
Christian Müller's avatar
Christian Müller committed
26
      val broken = s replace ("∧ ", "∧\n") replace ("∨ ", "∨\n")
27
28
29
30
31
32
33
34
35
36
37
38
39

      // 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
40
41
42
43
44
45
    }
  }

  case object True extends Term
  case object False extends Term

46
47
48
49
50
  object Var {
    val DEFAULT_TYPE = "T"
  }
  case class Var(name: String, typ:String = Var.DEFAULT_TYPE) extends Term {
    override def toString() = s"$name"
Christian Müller's avatar
Christian Müller committed
51
    def withType() = s"$name:$typ"
Christian Müller's avatar
Christian Müller committed
52
  }
53

Christian Müller's avatar
Christian Müller committed
54
  object Fun {
55
    def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
Christian Müller's avatar
Christian Müller committed
56
  }
57
  case class Fun(name: String, ind: Option[String], params: List[Var]) extends Term {
58
    override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.map(_.name).mkString("(", ",", ")")
Christian Müller's avatar
Christian Müller committed
59
    def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p)) 
60
    def updatedParams(list: List[Var]) = Fun(name, ind, list) 
Christian Müller's avatar
Christian Müller committed
61
62
63
64
65
66
67
  }

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

Christian Müller's avatar
Christian Müller committed
69
    override def toString() = {
70
      // show types only in quantifiers
Christian Müller's avatar
Christian Müller committed
71
      qname + " " + vars.map(_.withType()).mkString(",") + ". " + t.bracketed()
Christian Müller's avatar
Christian Müller committed
72
73
    }
  }
74

Christian Müller's avatar
Christian Müller committed
75
76
77
78
79
80
81
82
83
84
85
86
  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 _
  }
Christian Müller's avatar
Christian Müller committed
87
88
89
90
91
92
93
  case class ForallOtherThan(vars: List[Var], otherthan:List[Var], t: Term) extends Quantifier {
    val qname = "∀"
    val qmake = ForallOtherThan.apply(_:List[Var], otherthan, _:Term)
    override def toString() = {
       s"$qname ${vars.map(_.withType()).mkString(",")} ∉ {${otherthan.map(_.withType()).mkString(",")}}. ${t.bracketed()}"
    }
  }
Christian Müller's avatar
Christian Müller committed
94
95
96

  trait TemporalTerm extends Term

97
  case class Next(t: Term) extends TemporalTerm with UnOp {
Christian Müller's avatar
Christian Müller committed
98
99
    val make = Next.apply _
    val opname = "X"
Christian Müller's avatar
Christian Müller committed
100
  }
Christian Müller's avatar
Christian Müller committed
101
102
103
  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
104
  }
Christian Müller's avatar
Christian Müller committed
105
106
107
108

  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
109
  }
110

Christian Müller's avatar
Christian Müller committed
111
112
113
114
  case class Until(t1: Term, t2: Term) extends TemporalTerm with BinOp {
    val make = Until.apply _
    val opname = "U"
  }
Christian Müller's avatar
Christian Müller committed
115
116
117
118
  
  object WUntil {
    def apply(t1: Term, t2: Term) = Or(Until(t1, t2), Globally(t1)) 
  }
119

Christian Müller's avatar
Christian Müller committed
120
  trait UnOp extends Term {
121
    def make: Term => UnOp
Christian Müller's avatar
Christian Müller committed
122
123
    def opname: String
    def t: Term
124

Christian Müller's avatar
Christian Müller committed
125
126
    override def toString() = opname + " " + t.bracketed()
  }
127

Christian Müller's avatar
Christian Müller committed
128
129
130
  object UnOp {
    def unapply(unop: UnOp) = {
      Some((unop.make, unop.t))
Christian Müller's avatar
Christian Müller committed
131
132
133
134
    }
  }

  trait BinOp extends Term {
135
    def make: (Term, Term) => BinOp
Christian Müller's avatar
Christian Müller committed
136
137
    def opname: String
    def t1: Term
138
139
    def t2: Term

Christian Müller's avatar
Christian Müller committed
140
141
    override def toString() = {
      (t1, t2) match {
142
        case (t1: BinOp, t2: BinOp) if (opname == t1.opname && opname == t2.opname) => t1 + " " + opname + " " + t2
Christian Müller's avatar
Christian Müller committed
143
        case (t1: BinOp, _) if (opname == t1.opname) => t1 + " " + opname + " " + t2.bracketed()
144
        case (_, t2: BinOp) if (opname == t2.opname) => t1.bracketed() + " " + opname + " " + t2
Christian Müller's avatar
Christian Müller committed
145
146
147
148
        case _ => t1.bracketed() + " " + opname + " " + t2.bracketed()
      }
    }
  }
149

Christian Müller's avatar
Christian Müller committed
150
151
152
153
  object BinOp {
    def unapply(binop: BinOp) = {
      Some((binop.make, binop.t1, binop.t2))
    }
154
155

    def makeL(make: (Term, Term) => Term, l: Seq[Term], Empty: Term): Term = {
Christian Müller's avatar
Christian Müller committed
156
      l.toList match {
157
158
159
160
        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
161
162
163
      }
    }
  }
164
  
165
166
  object Or {
    def make(terms: List[Term]) = {
Christian Müller's avatar
Christian Müller committed
167
168
169
      BinOp.makeL(Or.apply _, terms, True)
    }
    def make(terms: Term*) = {
170
171
172
      BinOp.makeL(Or.apply _, terms, False)
    }
  }
173
  
Christian Müller's avatar
Christian Müller committed
174
175
176
177
  case class Or(t1: Term, t2: Term) extends BinOp {
    val opname = "∨"
    val make = Or.apply _
  }
178
  
179
180
181
182
  object And {
    def make(terms: List[Term]) = {
      BinOp.makeL(And.apply _, terms, True)
    }
Christian Müller's avatar
Christian Müller committed
183
184
185
    def make(terms: Term*) = {
      BinOp.makeL(And.apply _, terms, True)
    }
186
  }
187
  
Christian Müller's avatar
Christian Müller committed
188
189
190
191
  case class And(t1: Term, t2: Term) extends BinOp {
    val opname = "∧"
    val make = And.apply _
  }
192
193
  
  case class Eq(t1: Term, t2: Term) extends BinOp {
Christian Müller's avatar
Christian Müller committed
194
195
196
    val opname = "↔"
    val make = Eq.apply _
  }
197
  
Christian Müller's avatar
Christian Müller committed
198
199
200
201
202
203
  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
204
    val make = Neg.apply _
Christian Müller's avatar
Christian Müller committed
205
206
207
208
    val opname = "¬"
  }

}