Skip to content
Snippets Groups Projects
Commit 7ec123d2 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

ScalaPrinter prints subsetOf correctly

parent 7cedd12d
No related branches found
No related tags found
No related merge requests found
...@@ -3,7 +3,6 @@ ...@@ -3,7 +3,6 @@
package leon package leon
package purescala package purescala
import Constructors._
import Extractors._ import Extractors._
import PrinterHelpers._ import PrinterHelpers._
import Common._ import Common._
...@@ -27,15 +26,18 @@ class ScalaPrinter(opts: PrinterOptions, ...@@ -27,15 +26,18 @@ class ScalaPrinter(opts: PrinterOptions,
})) }))
case Not(Equals(l, r)) => optP { p"$l != $r" } case Not(Equals(l, r)) => optP { p"$l != $r" }
case Choose(pred) => p"choose($pred)" case Choose(pred) => p"choose($pred)"
case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})" case s @ FiniteSet(rss, t) => p"Set[$t](${rss.toSeq})"
case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
case ElementOfSet(e,s) => p"$s.contains(e)" case ElementOfSet(e,s) => p"$s.contains(e)"
case SetUnion(l,r) => optP { p"$l ++ $r" } case SetUnion(l,r) => optP { p"$l ++ $r" }
case MapUnion(l,r) => optP { p"$l ++ $r" }
case SetDifference(l,r) => optP { p"$l -- $r" } case SetDifference(l,r) => optP { p"$l -- $r" }
case SetIntersection(l,r) => optP { p"$l & $r" } case SetIntersection(l,r) => optP { p"$l & $r" }
case SetCardinality(s) => p"$s.size" case SetCardinality(s) => p"$s.size"
case SubsetOf(subset,superset) => p"$subset.subsetOf($superset)"
case MapUnion(l,r) => optP { p"$l ++ $r" }
case m @ FiniteMap(els, k, v) => p"Map[$k,$v]($els)"
case InfiniteIntegerLiteral(v) => p"BigInt($v)" case InfiniteIntegerLiteral(v) => p"BigInt($v)"
case a@FiniteArray(elems, oDef, size) => case a@FiniteArray(elems, oDef, size) =>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment