Skip to content

Commit bb6b37f

Browse files
robby-phdrobby-phd
committed
Rewriting system.
1 parent 69ae3d9 commit bb6b37f

File tree

3 files changed

+101
-18
lines changed

3 files changed

+101
-18
lines changed

‎jvm/src/test/scala/org/sireum/logika/example/list.sc

+81-12
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ object List {
118118
//@formatter:off
119119
1 ( l ≡ List.Cons[T](value, next) ) by Premise, // auto-generated
120120
2 ( next.length >= 0 ) by Premise, // auto-generated
121-
3 ( l.length ≡ (1 + next.length) ) by Simpl,
121+
3 ( l.length ≡ (1 + next.length) ) by Simpl, // Auto,
122122
4 ( l.length >= 0 ) by Auto and (2, 3)
123123
//@formatter:on
124124
)
@@ -128,7 +128,7 @@ object List {
128128
Deduce(
129129
//@formatter:off
130130
1 ( l ≡ List.Nil[T]() ) by Premise, // auto-generated
131-
2 ( l.length >= 0 ) by Simpl
131+
2 ( l.length >= 0 ) by Simpl // Auto
132132
//@formatter:on
133133
)
134134
return
@@ -329,6 +329,75 @@ object List {
329329
}
330330
}
331331

332+
@pure def lookupUpdateNeInduct[K, V](map: Map[K, V], key1: K, key2: K, value: V): Unit = {
333+
Contract(
334+
Requires(key1 ≢ key2),
335+
Ensures(lookup(update(map, key1, value), key2) ≡ lookup(map, key2))
336+
)
337+
(map: @induct) match {
338+
case Cons(p, next) => {
339+
340+
if (p._1 ≡ key1) {
341+
342+
Deduce(
343+
//@formatter:off
344+
1 ( map ≡ Cons(p, next) ) by Premise, // auto-generated
345+
2 ( key1 ≢ key2 ) by Premise,
346+
3 ( p._1 ≡ key1 ) by Premise,
347+
4 ( p._1 ≢ key2 ) by Auto,
348+
5 ( update(map, key1, value) ≡ Cons(key1 ~> value, next) ) by RSimpl(RS(update _)), //Auto,
349+
6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _)) //Auto
350+
//@formatter:on
351+
)
352+
return
353+
354+
} else {
355+
356+
if (p._1 ≡ key2) {
357+
Deduce(
358+
//@formatter:off
359+
1 ( map ≡ Cons(p, next) ) by Premise, // Auto-generated
360+
2 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by Premise, // Auto-generated
361+
3 ( key1 ≢ key2 ) by Premise,
362+
4 ( !(p._1 ≡ key1) ) by Premise,
363+
5 ( p._1 ≡ key2 ) by Premise,
364+
6 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
365+
7 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
366+
//@formatter:on
367+
)
368+
} else {
369+
Deduce(
370+
//@formatter:off
371+
1 ( map ≡ Cons(p, next) ) by Premise, // Auto-generated
372+
2 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by Premise, // Auto-generated
373+
3 ( key1 ≢ key2 ) by Premise,
374+
4 ( !(p._1 ≡ key1) ) by Premise,
375+
5 ( !(p._1 ≡ key2) ) by Premise,
376+
6 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
377+
7 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
378+
//@formatter:on
379+
)
380+
}
381+
return
382+
383+
}
384+
385+
}
386+
case Nil() => {
387+
Deduce(
388+
//@formatter:off
389+
1 ( map ≡ Nil[(K, V)]() ) by Premise, // Auto-generated
390+
2 ( key1 ≢ key2 ) by Premise,
391+
3 ( update(map, key1, value) ≡ Cons(key1 ~> value, Nil[(K, V)]()) ) by RSimpl(RS(update _)), //Auto,
392+
4 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _)) //Auto,
393+
//@formatter:on
394+
)
395+
return
396+
397+
}
398+
}
399+
}
400+
332401
}
333402

334403
@strictpure def make[T](value: T): List[T] = Cons(value, Nil())
@@ -541,12 +610,12 @@ object List {
541610
)
542611
)
543612

544-
q.strategy match {
613+
(q.strategy: @induct) match {
545614
case Queue.Strategy.DropEarliest => {
546615
if (q.length < q.capacity) {
547616
Deduce(
548617
//@formatter:off
549-
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise,
618+
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, // Auto-generated
550619
2 ( q.length < q.capacity ) by Premise,
551620
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
552621
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -556,7 +625,7 @@ object List {
556625
} else {
557626
Deduce(
558627
//@formatter:off
559-
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise,
628+
1 ( q.strategy ≡ List.Queue.Strategy.DropEarliest ) by Premise, // Auto-generated
560629
2 ( !(q.length < q.capacity) ) by Premise,
561630
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
562631
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -569,7 +638,7 @@ object List {
569638
if (q.length < q.capacity) {
570639
Deduce(
571640
//@formatter:off
572-
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise,
641+
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, // Auto-generated
573642
2 ( q.length < q.capacity ) by Premise,
574643
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
575644
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -579,7 +648,7 @@ object List {
579648
} else {
580649
Deduce(
581650
//@formatter:off
582-
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise,
651+
1 ( q.strategy ≡ List.Queue.Strategy.DropLatest ) by Premise, // Auto-generated
583652
2 ( !(q.length < q.capacity) ) by Premise,
584653
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
585654
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -592,7 +661,7 @@ object List {
592661
if (q.length < q.capacity) {
593662
Deduce(
594663
//@formatter:off
595-
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise,
664+
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, // Auto-generated
596665
2 ( q.length < q.capacity ) by Premise,
597666
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
598667
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -602,7 +671,7 @@ object List {
602671
} else {
603672
Deduce(
604673
//@formatter:off
605-
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise,
674+
1 ( q.strategy ≡ List.Queue.Strategy.Error ) by Premise, // Auto-generated
606675
2 ( !(q.length < q.capacity) ) by Premise,
607676
3 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
608677
4 ( q.push(a).strategy ≡ q.strategy ) by Simpl
@@ -614,7 +683,7 @@ object List {
614683
case Queue.Strategy.Unbounded => {
615684
Deduce(
616685
//@formatter:off
617-
1 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise,
686+
1 ( q.strategy ≡ List.Queue.Strategy.Unbounded ) by Premise, // Auto-generated
618687
2 ( q.push(a).capacity ≡ q.capacity ) by Simpl,
619688
3 ( q.push(a).strategy ≡ q.strategy ) by Simpl
620689
//@formatter:on
@@ -630,7 +699,7 @@ object List {
630699
Ensures(q.push(a).buffer ≡ (q.buffer ++ List.make(a)))
631700
)
632701

633-
q.strategy match {
702+
(q.strategy: @induct) match {
634703
case Queue.Strategy.DropEarliest => {
635704
Deduce(
636705
//@formatter:off
@@ -683,7 +752,7 @@ object List {
683752

684753
framePush(q, a)
685754

686-
q.strategy match {
755+
(q.strategy: @induct) match {
687756
case Queue.Strategy.DropEarliest => {
688757
if (q.length < q.capacity) {
689758

‎shared/src/main/scala/org/sireum/logika/RewritingSystem.scala

+9-5
Original file line numberDiff line numberDiff line change
@@ -598,7 +598,7 @@ object RewritingSystem {
598598
}
599599
val patterns2: ISZ[Rewriter.Pattern.Claim] =
600600
(for (k <- 0 until apcs.size; apc <- toCondEquiv(th, apcs(k)._2)) yield
601-
r2l(Rewriter.Pattern.Claim(pattern.name :+ s"Assumption$k", F, isPermutative(apc), HashSSet.empty, apc))) ++
601+
r2l(Rewriter.Pattern.Claim(pattern.isInObject, pattern.name :+ s"Assumption$k", F, isPermutative(apc), HashSSet.empty, apc))) ++
602602
patterns
603603
val o2 = Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F,
604604
maxUnfolding, F, F, F, ISZ()).transformCoreExpBase(cache, o).getOrElse(o)
@@ -650,11 +650,14 @@ object RewritingSystem {
650650
@pure def toRightToLeft: Rewriter.Pattern = {
651651
return this
652652
}
653+
@pure def isInObject: B
654+
@pure def name: ISZ[String]
653655
}
654656

655657
object Pattern {
656658

657-
@datatype class Claim(val name: ISZ[String],
659+
@datatype class Claim(val isInObject: B,
660+
val name: ISZ[String],
658661
val rightToLeft: B,
659662
val isPermutative: B,
660663
val localPatternSet: LocalPatternSet,
@@ -680,6 +683,7 @@ object RewritingSystem {
680683
val id: String,
681684
val params: ISZ[(String, AST.Typed)],
682685
val exp: AST.CoreExp.Base) extends Pattern {
686+
@strictpure def name: ISZ[String] = owner :+ id
683687
@memoize def toFun: AST.CoreExp.Fun = {
684688
val context = owner :+ id
685689
var map = HashMap.empty[AST.CoreExp, AST.CoreExp.ParamVarRef]
@@ -2832,7 +2836,7 @@ object RewritingSystem {
28322836
case c => RewritingSystem.translateExp(th, T, c)
28332837
}
28342838
return for (c <- RewritingSystem.toCondEquiv(th, claim)) yield
2835-
Rewriter.Pattern.Claim(name, F, isPermutative(c), localPatternSet, c)
2839+
Rewriter.Pattern.Claim(T, name, F, isPermutative(c), localPatternSet, c)
28362840
case info: Info.Fact =>
28372841
var localPatternSet: RewritingSystem.LocalPatternSet = HashSSet.empty
28382842
var r = ISZ[Rewriter.Pattern]()
@@ -2846,7 +2850,7 @@ object RewritingSystem {
28462850
case c => RewritingSystem.translateExp(th, T, c)
28472851
}
28482852
for (c <- RewritingSystem.toCondEquiv(th, claim)) {
2849-
r = r :+ Rewriter.Pattern.Claim(name, F, isPermutative(c), localPatternSet, c)
2853+
r = r :+ Rewriter.Pattern.Claim(T, name, F, isPermutative(c), localPatternSet, c)
28502854
}
28512855
}
28522856
return r
@@ -2887,7 +2891,7 @@ object RewritingSystem {
28872891
exp = AST.CoreExp.Arrow(translateExp(th, T, requires(i)), exp)
28882892
}
28892893
for (e <- toCondEquiv(th, exp)) {
2890-
r = r :+ Rewriter.Pattern.Claim(minfo.name :+ title, F, isPermutative(exp), localPatternSet, e)
2894+
r = r :+ Rewriter.Pattern.Claim(minfo.isInObject, minfo.name :+ title, F, isPermutative(exp), localPatternSet, e)
28912895
}
28922896
}
28932897

‎shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala

+11-1
Original file line numberDiff line numberDiff line change
@@ -70,9 +70,19 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
7070
} else {
7171
var r1 = ISZ[Rewriter.Pattern.Claim]()
7272
var r2 = HashSMap.empty[(ISZ[String], B), Rewriter.Pattern.Method]
73+
val (currIsInObject, currMethodName): (B, ISZ[String]) = logika.context.methodOpt match {
74+
case Some(m) => (m.receiverTypeOpt.isEmpty, m.name)
75+
case _ => (F, ISZ())
76+
}
7377
for (p <- RewritingSystem.retrievePatterns(logika.th, cache, justArgs(0), HashSet.empty)) {
78+
if (p.isInObject == currIsInObject && (p.name == currMethodName :+ "contract" || p.name == currMethodName)) {
79+
val n: Z = if (p.name(p.name.size - 1) == "contract") 2 else 1
80+
reporter.error(step.just.id.attr.posOpt, Logika.kind, s"Cannot use ${p.name(p.name.size - n)} as a rewrite in itself")
81+
return err
82+
}
7483
p match {
75-
case p: Rewriter.Pattern.Claim => r1 = r1 :+ p
84+
case p: Rewriter.Pattern.Claim =>
85+
r1 = r1 :+ p
7686
case p: Rewriter.Pattern.Method =>
7787
if (p.isAbs) {
7888
r2 = r2 + (p.owner :+ p.id, p.isInObject) ~> p

0 commit comments

Comments
 (0)