-
Notifications
You must be signed in to change notification settings - Fork 18
/
Struct.scala
222 lines (184 loc) · 6.73 KB
/
Struct.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
/*
* Struct.scala
*
*/
package gapt.proofs.ceres
import gapt.expr._
import gapt.expr.formula.Atom
import gapt.expr.formula.Bottom
import gapt.expr.formula.Formula
import gapt.expr.formula.Top
import gapt.expr.formula.fol.FOLAtom
import gapt.expr.ty.To
import gapt.proofs.Sequent
import scala.math.max
/**
* The superclass for all struct elements: atom, negated atom, junction, times and the neutral elememts for the latter
* two. For details refer to Bruno Woltzenlogel-Paleo's PhD Thesis.
*/
trait Struct {
/**
* Struct equality without taking the additional data into account.
* @param that the struct to compare with
* @return true if the structs are equal modulo data, false otherwise
*/
def formula_equal( that: Struct ): Boolean
/**
* Calculates the size (number of nodes of the tree) of the struct.
* @return the size of the struct
*/
def size(): Int //total number of nodes
/**
* Calculates the maximum number of times-junction alternations of all paths from the root to one of the leaves.
* The alternations are a measure for the complexity of the generated clause/sequent set.
* @return the number of times-junction alternations
*/
def alternations(): Int //number of alternations (includes duals)
/**
* Allows to access the calculus-specific data of the struct
* @return the corresponding data element
*/
def toFormula: Formula
def label: Expr
def children: Seq[Struct]
}
object Times {
//create a series of of times applications and add the same data to each
def apply( structs: Vector[Struct] ): Struct = ( structs: @unchecked ) match {
case Vector() => EmptyTimesJunction()
case EmptyTimesJunction() +: l => apply( l )
case Vector( s1 ) => s1
case s1 +: tail => apply( s1, apply( tail ) )
}
}
case class Times( left: Struct, right: Struct ) extends Struct {
override def toString(): String = "(" + left + " ⊗ " + right + ")"
override def formula_equal( s: Struct ) = s match {
case Times( x, y ) => left.formula_equal( x ) && right.formula_equal( y )
case _ => false
}
override def size() = 1 + left.size() + right.size()
override def alternations() = {
( left, right ) match {
case ( Times( _, _ ), Times( _, _ ) ) => max( left.alternations(), right.alternations() )
case ( Times( _, _ ), _ ) => max( left.alternations(), 1 + right.alternations() )
case ( _, Times( _, _ ) ) => max( 1 + left.alternations(), right.alternations() )
case _ => 1 + max( left.alternations(), right.alternations() )
}
}
def toFormula = left.toFormula | right.toFormula
def label = Const( "⊗", To ->: To ->: To )
def children = Seq( left, right )
}
case class Plus( left: Struct, right: Struct ) extends Struct {
override def toString(): String = "(" + left + " ⊕ " + right + ")"
override def formula_equal( s: Struct ) = s match {
case Plus( x, y ) => left.formula_equal( x ) && right.formula_equal( y )
case _ => false
}
override def size() = 1 + left.size() + right.size()
override def alternations() = {
( left, right ) match {
case ( Plus( _, _ ), Plus( _, _ ) ) => max( left.alternations(), right.alternations() )
case ( Plus( _, _ ), _ ) => max( left.alternations(), 1 + right.alternations() )
case ( _, Plus( _, _ ) ) => max( 1 + left.alternations(), right.alternations() )
case _ => 1 + max( left.alternations(), right.alternations() )
}
}
def toFormula = left.toFormula & right.toFormula
def label = Const( "⊕", To ->: To ->: To )
def children = Seq( left, right )
}
case class Dual( sub: Struct ) extends Struct {
override def toString(): String = "~(" + sub + ")"
override def formula_equal( s: Struct ) = s match {
case Dual( x ) => sub.formula_equal( x )
case _ => false
}
override def size() = 1 + sub.size()
override def alternations() = {
sub match {
case Dual( _ ) => sub.alternations()
case _ => 1 + sub.size()
}
}
def toFormula = -sub.toFormula
def label = Const( "~", To ->: To )
def children = Seq( sub )
}
case class A( fo: Formula ) extends Struct { // Atomic Struct
override def toString(): String = fo.toString
override def formula_equal( s: Struct ) = s match {
case A( x ) => fo syntaxEquals ( x )
case _ => false
}
override def size() = 1
override def alternations() = 0
def toFormula = fo
def label = fo
def children = Seq()
}
case class CLS( proof: Expr, config: Sequent[Boolean] ) extends Struct { // Clause Set Symbol Struct
override def toString(): String = {
val Apps( Const( pn, _, _ ), vs ) = proof
"CLS(" + pn + " , " + config.toString + " , " + vs.toString() + ")"
}
override def formula_equal( s: Struct ) = this == s
override def size() = 1
override def alternations() = 0
def toFormula = {
val Apps( Const( pn, _, _ ), vs ) = proof
Atom( "CL" + "[" + pn + "," + config.toString + "]", vs )
}
def label = {
val Apps( Const( pn, _, _ ), vs ) = proof
Atom( "CL" + "[" + pn + "," + config.toString + "]", vs )
}
def children = Seq()
}
case class EmptyTimesJunction() extends Struct {
override def toString(): String = "ε⊗"
override def formula_equal( s: Struct ) = s match {
case EmptyTimesJunction() => true
case _ => false
}
override def size() = 1
override def alternations() = 0
def toFormula = Bottom()
def label = FOLAtom( "ε⊗" )
def children = Seq()
}
case class EmptyPlusJunction() extends Struct {
override def toString(): String = "ε⊕"
override def formula_equal( s: Struct ) = s match {
case EmptyPlusJunction() => true
case _ => false
}
override def size() = 1
override def alternations() = 0
def toFormula = Top()
def label = FOLAtom( "ε⊕" )
def children = Seq()
}
/* convenience object allowing to create and match a set of plus nodes */
object PlusN {
def apply( l: List[Struct] ): Struct = l match {
case Nil => EmptyPlusJunction()
case x :: Nil => x
case x :: xs => Plus( x, PlusN( xs ) )
}
def unapply( s: Struct ): Option[List[Struct]] = Some( unapply_( s ) )
private def unapply_( s: Struct ): List[Struct] = s match {
case Plus( l, r ) => unapply_( l ) ++ unapply_( r )
case _ => s :: Nil
}
}
//Returns all Schematic Leaves
object SchematicLeafs {
def apply( l: Struct ): Set[Struct] = l match {
case Times( le, r ) => SchematicLeafs( le ) ++ SchematicLeafs( r )
case Plus( le, r ) => SchematicLeafs( le ) ++ SchematicLeafs( r )
case CLS( x, y ) => Set[Struct]( l )
case _ => Set[Struct]()
}
}