From f9daa0d73a9642d2d7780d268ef0e0f1d1ea7e60 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 26 Oct 2016 19:41:01 +0200
Subject: [PATCH] Ordering on characters
---
src/main/scala/inox/ast/Expressions.scala | 16 ++++++++++++----
src/main/scala/inox/ast/Printers.scala | 1 +
2 files changed, 13 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 3d6d4064d..9c87a1acb 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -466,25 +466,33 @@ trait Expressions { self: Trees =>
/** $encodingof `... < ...`*/
case class LessThan(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type =
- if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
+ if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+ else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+ else Untyped
}
/** $encodingof `... > ...`*/
case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr with CachingTyped{
protected def computeType(implicit s: Symbols): Type =
- if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
+ if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+ else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+ else Untyped
}
/** $encodingof `... <= ...`*/
case class LessEquals(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type =
- if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
+ if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+ else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+ else Untyped
}
/** $encodingof `... >= ...`*/
case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
protected def computeType(implicit s: Symbols): Type =
- if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType else Untyped
+ if (numericType(lhs.getType, rhs.getType) != Untyped) BooleanType
+ else if (lhs.getType == CharType && rhs.getType == CharType) BooleanType
+ else Untyped
}
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index bd013e591..e180bc0f3 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -254,6 +254,7 @@ trait Printers {
case BagAdd(b, e) => p"$b + $e"
case MultiplicityInBag(e, b) => p"$b($e)"
case MapApply(m, k) => p"$m($k)"
+ case MapUpdated(m, k, v) => p"$m.updated($k, $v)"
case Not(expr) => p"\u00AC$expr"
--
GitLab