Comparisons and well-founded order of char

11 files changed, 186 insertions, 42 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 4cdb21e9..9b410b1e 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -79,6 +79,9 @@ axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
 type char;

 function char#FromInt(int): char;

 function char#ToInt(char): int;  // inverse of char#FromInt

+axiom (forall ch: char ::

+  { char#ToInt(ch) } 

+  char#FromInt(char#ToInt(ch)) == ch);

 axiom (forall n: int ::

   { char#FromInt(n) }

   0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 84066c0e..0d77ecc6 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -191,7 +191,7 @@ namespace Microsoft.Dafny
         return new InferredTypeProxy();

       } else if (t is OperationTypeProxy) {

         var p = (OperationTypeProxy)t;

-        return new OperationTypeProxy(p.AllowInts, p.AllowReals, p.AllowSeq, p.AllowSetVarieties);

+        return new OperationTypeProxy(p.AllowInts, p.AllowReals, p.AllowChar, p.AllowSeq, p.AllowSetVarieties);

       } else if (t is ParamTypeProxy) {

         return new ParamTypeProxy(CloneTypeParam(((ParamTypeProxy)t).orig));

       } else {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index b7568f54..9d2cad2f 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2367,13 +2367,17 @@ namespace Microsoft.Dafny {
           }

 

           case BinaryExpr.ResolvedOpcode.Lt:

-            opString = "<";  break;

+          case BinaryExpr.ResolvedOpcode.LtChar:

+            opString = "<"; break;

           case BinaryExpr.ResolvedOpcode.Le:

-            opString = "<=";  break;

+          case BinaryExpr.ResolvedOpcode.LeChar:

+            opString = "<="; break;

           case BinaryExpr.ResolvedOpcode.Ge:

-            opString = ">=";  break;

+          case BinaryExpr.ResolvedOpcode.GeChar:

+            opString = ">="; break;

           case BinaryExpr.ResolvedOpcode.Gt:

-            opString = ">";  break;

+          case BinaryExpr.ResolvedOpcode.GtChar:

+            opString = ">"; break;

           case BinaryExpr.ResolvedOpcode.Add:

             opString = "+";  break;

           case BinaryExpr.ResolvedOpcode.Sub:

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f9ffa5c7..2903d471 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -489,7 +489,7 @@ NewtypeDecl<ModuleDefinition module, out TopLevelDecl td>
   "="

   ( IF(IsIdentColonOrBar())

     NoUSIdent<out bvId>

-    [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false); } .)

+    [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } .)

     "|"

     Expression<out wh, false, true>  (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)

   | Type<out baseType>               (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ab59dc34..834e6aba 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -387,7 +387,7 @@ namespace Microsoft.Dafny {
       var t = NormalizeExpand();

       var opProxy = t as OperationTypeProxy;

       if (opProxy != null) {

-        return (opProxy.AllowInts || opProxy.AllowReals) && !opProxy.AllowSeq && !opProxy.AllowSetVarieties;

+        return (opProxy.AllowInts || opProxy.AllowReals) && !opProxy.AllowChar && !opProxy.AllowSeq && !opProxy.AllowSetVarieties;

       }

       return t.IsIntegerType || t.IsRealType || t.AsNewtype != null;

     }

@@ -1185,18 +1185,21 @@ namespace Microsoft.Dafny {
   public class OperationTypeProxy : RestrictedTypeProxy {

     public readonly bool AllowInts;

     public readonly bool AllowReals;

+    public readonly bool AllowChar;

     public readonly bool AllowSeq;

     public readonly bool AllowSetVarieties;

     public bool JustInts {

-      get { return AllowInts && !AllowReals && !AllowSeq && !AllowSetVarieties; }

+      get { return AllowInts && !AllowReals && !AllowChar && !AllowSeq && !AllowSetVarieties; }

     }

     public bool JustReals {

-      get { return !AllowInts && AllowReals && !AllowSeq && !AllowSetVarieties; }

+      get { return !AllowInts && AllowReals && !AllowChar && !AllowSeq && !AllowSetVarieties; }

     }

-    public OperationTypeProxy(bool allowInts, bool allowReals, bool allowSeq, bool allowSetVarieties) {

-      Contract.Requires(allowInts || allowReals || allowSeq || allowSetVarieties);  // don't allow unsatisfiable constraint

+    public OperationTypeProxy(bool allowInts, bool allowReals, bool allowChar, bool allowSeq, bool allowSetVarieties) {

+      Contract.Requires(allowInts || allowReals || allowChar || allowSeq || allowSetVarieties);  // don't allow unsatisfiable constraint

+      Contract.Requires(!(!allowInts && !allowReals && allowChar && !allowSeq && !allowSetVarieties));  // to constrain to just char, don't use a proxy

       AllowInts = allowInts;

       AllowReals = allowReals;

+      AllowChar = allowChar;

       AllowSeq = allowSeq;

       AllowSetVarieties = allowSetVarieties;

     }

@@ -5707,6 +5710,11 @@ namespace Microsoft.Dafny {
       Mul,

       Div,

       Mod,

+      // char

+      LtChar,

+      LeChar,

+      GeChar,

+      GtChar,

       // sets

       SetEq,

       SetNeq,

@@ -5801,6 +5809,7 @@ namespace Microsoft.Dafny {
           return Opcode.Neq;

 

         case ResolvedOpcode.Lt:

+        case ResolvedOpcode.LtChar:

         case ResolvedOpcode.ProperSubset:

         case ResolvedOpcode.ProperMultiSuperset:

         case ResolvedOpcode.ProperPrefix:

@@ -5808,17 +5817,20 @@ namespace Microsoft.Dafny {
           return Opcode.Lt;

 

         case ResolvedOpcode.Le:

+        case ResolvedOpcode.LeChar:

         case ResolvedOpcode.Subset:

         case ResolvedOpcode.MultiSubset:

         case ResolvedOpcode.Prefix:

           return Opcode.Le;

 

         case ResolvedOpcode.Ge:

+        case ResolvedOpcode.GeChar:

         case ResolvedOpcode.Superset:

         case ResolvedOpcode.MultiSuperset:

           return Opcode.Ge;

 

         case ResolvedOpcode.Gt:

+        case ResolvedOpcode.GtChar:

         case ResolvedOpcode.ProperSuperset:

         case ResolvedOpcode.ProperMultiSubset:

         case ResolvedOpcode.RankGt:

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 7a617a6c..8755d275 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -560,7 +560,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				Get();

 				Type(out baseType);

 			}

-			if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false); } 

+			if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false); } 

 			Expect(9);

 			Expression(out wh, false, true);

 			td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2932b4b7..1486f403 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4088,6 +4088,8 @@ namespace Microsoft.Dafny
           // fine

         } else if (opProxy.AllowReals && t.IsNumericBased(Type.NumericPersuation.Real)) {

           // fine

+        } else if (opProxy.AllowChar && t is CharType) {

+          // fine

         } else if (opProxy.AllowSetVarieties && (t is SetType || t is MultiSetType)) {

           // fine

         } else if (opProxy.AllowSeq && t is SeqType) {

@@ -4099,7 +4101,7 @@ namespace Microsoft.Dafny
       } else if (proxy is IndexableTypeProxy) {

         var iProxy = (IndexableTypeProxy)proxy;

         if (t is SeqType) {

-          if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false))) {

+          if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false, false))) {

             return false;

           } else if (!UnifyTypes(iProxy.Range, ((SeqType)t).Arg)) {

             return false;

@@ -4108,7 +4110,7 @@ namespace Microsoft.Dafny
           }

         } else if (iProxy.AllowArray && t.IsArrayType && t.AsArrayType.Dims == 1) {

           Type elType = UserDefinedType.ArrayElementType(t);

-          if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false))) {

+          if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false, false))) {

             return false;

           } else if (!UnifyTypes(iProxy.Range, elType)) {

             return false;

@@ -4126,7 +4128,7 @@ namespace Microsoft.Dafny
         } else if (t is MultiSetType) {

           if (!UnifyTypes(iProxy.Domain, ((MultiSetType)t).Arg)) {

             return false;

-          } else if (!UnifyTypes(iProxy.Range, new OperationTypeProxy(true, false, false, false))) {

+          } else if (!UnifyTypes(iProxy.Range, new OperationTypeProxy(true, false, false, false, false))) {

             return false;

           } else if (!UnifyTypes(iProxy.Arg, iProxy.Domain)) {

             return false;

@@ -4225,24 +4227,25 @@ namespace Microsoft.Dafny
           var pb = (OperationTypeProxy)b;

           var i = pa.AllowInts && pb.AllowInts;

           var r = pa.AllowReals && pb.AllowReals;

+          var h = pa.AllowChar && pb.AllowChar;

           var q = pa.AllowSeq && pb.AllowSeq;

           var s = pa.AllowSetVarieties && pb.AllowSetVarieties;

-          if (!i && !r && !q && !s) {

+          if (!i && !r && !h && !q && !s) {

             // over-constrained

             return false;

-          } else if (i == pa.AllowInts && r == pa.AllowReals && q == pa.AllowSeq && s == pa.AllowSetVarieties) {

+          } else if (i == pa.AllowInts && r == pa.AllowReals && h == pa.AllowChar && q == pa.AllowSeq && s == pa.AllowSetVarieties) {

             b.T = a;  // a has the stronger requirement

-          } else if (i == pb.AllowInts && r == pb.AllowReals && q == pb.AllowSeq && s == pb.AllowSetVarieties) {

+          } else if (i == pb.AllowInts && r == pb.AllowReals && h == pb.AllowChar && q == pb.AllowSeq && s == pb.AllowSetVarieties) {

             a.T = b;  // b has the stronger requirement

           } else {

-            var c = new OperationTypeProxy(i, r, q, s);

+            Type c = !i && !r && h && !q && !s ? new CharType() : (Type)new OperationTypeProxy(i, r, h, q, s);

             a.T = c;

             b.T = c;

           }

           return true;

         } else {

           var ib = (IndexableTypeProxy)b;  // cast justification:  else we have unexpected restricted-proxy type

-          // a is:  possibly numeric, possibly seq, possibly set or multiset

+          // a is:  possibly numeric, possibly char, possibly seq, possibly set or multiset

           // b is:  seq, multiset, possibly map, possibly array -- with some constraints about the type parameterization

           // So, the intersection could include multiset and seq.

           if (pa.AllowSetVarieties && !pa.AllowSeq) {

@@ -4262,10 +4265,11 @@ namespace Microsoft.Dafny
             Contract.Assert(pa.AllowSeq && pa.AllowSetVarieties);  // the only case left

             if (ib.AllowMap || ib.AllowArray) {

               var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, false, false);

+              a.T = c;

               b.T = c;

-              b = c;

+            } else {

+              a.T = b;

             }

-            a.T = b;

             return true;

           }

         }

@@ -5778,7 +5782,7 @@ namespace Microsoft.Dafny
           foreach (Expression dim in rr.ArrayDimensions) {

             Contract.Assert(dim != null);

             ResolveExpression(dim, new ResolveOpts(codeContext, true));

-            if (!UnifyTypes(dim.Type, new OperationTypeProxy(true, false, false, false))) {

+            if (!UnifyTypes(dim.Type, new OperationTypeProxy(true, false, false, false, false))) {

               Error(stmt, "new must use an integer-based expression for the array size (got {0} for index {1})", dim.Type, i);

             }

             i++;

@@ -6186,9 +6190,9 @@ namespace Microsoft.Dafny
           if (e.Value == null) {

             e.Type = new ObjectTypeProxy();

           } else if (e.Value is BigInteger) {

-            e.Type = new OperationTypeProxy(true, false, false, false);

+            e.Type = new OperationTypeProxy(true, false, false, false, false);

           } else if (e.Value is Basetypes.BigDec) {

-            e.Type = new OperationTypeProxy(false, true, false, false);

+            e.Type = new OperationTypeProxy(false, true, false, false, false);

           } else if (e.Value is bool) {

             e.Type = Type.Bool;

           } else if (e is CharLiteralExpr) {

@@ -6349,7 +6353,7 @@ namespace Microsoft.Dafny
           Contract.Assert(idx != null);

           ResolveExpression(idx, opts);

           Contract.Assert(idx.Type != null);  // follows from postcondition of ResolveExpression

-          if (!UnifyTypes(idx.Type, new OperationTypeProxy(true, false, false, false))) {

+          if (!UnifyTypes(idx.Type, new OperationTypeProxy(true, false, false, false, false))) {

             Error(idx, "array selection requires integer-based numeric indices (got {0} for index {1})", idx.Type, i);

           }

           i++;

@@ -6391,7 +6395,7 @@ namespace Microsoft.Dafny
             Error(e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);

           }

           ResolveExpression(e.Value, opts);

-          if (!UnifyTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false))) {

+          if (!UnifyTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false, false))) {

             Error(e.Value, "multiset update requires integer-based numeric value (got {0})", e.Value.Type);

           }

           expr.Type = e.Seq.Type;

@@ -6534,11 +6538,11 @@ namespace Microsoft.Dafny
         ResolveType(e.tok, e.ToType, opts.codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);

         ResolveExpression(e.E, opts);

         if (e.ToType.IsNumericBased(Type.NumericPersuation.Int)) {

-          if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false))) {

+          if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false))) {

             Error(expr, "type conversion to an int-based type is allowed only from numeric types (got {0})", e.E.Type);

           }

         } else if (e.ToType.IsNumericBased(Type.NumericPersuation.Real)) {

-          if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false))) {

+          if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false))) {

             Error(expr, "type conversion to a real-based type is allowed only from numeric types (got {0})", e.E.Type);

           }

         } else {

@@ -6620,15 +6624,17 @@ namespace Microsoft.Dafny
                 expr.Type = Type.Bool;

               } else {

                 bool err = false;

-                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, true, true))) {

-                  Error(expr, "arguments to {0} must be of a numeric type or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

+                bool isComparison = e.Op != BinaryExpr.Opcode.Add;

+                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, true, true))) {

+                  Error(expr, "arguments to {0} must be of a numeric type{2} or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type,

+                    isComparison ? ", char," : "");

                   err = true;

                 }

                 if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

                   Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);

                   err = true;

                 }

-                if (e.Op != BinaryExpr.Opcode.Add) {

+                if (isComparison) {

                   expr.Type = Type.Bool;

                 } else if (!err) {

                   expr.Type = e.E0.Type;

@@ -6657,15 +6663,17 @@ namespace Microsoft.Dafny
                 expr.Type = Type.Bool;

               } else {

                 bool err = false;

-                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, true))) {

-                  Error(expr, "arguments to {0} must be of a numeric type or set type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

+                bool isComparison = e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge;

+                if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, false, true))) {

+                  Error(expr, "arguments to {0} must be of a numeric type{2} or a set type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type,

+                    isComparison ? ", char, " : "");

                   err = true;

                 }

                 if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

                   Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);

                   err = true;

                 }

-                if (e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge) {

+                if (isComparison) {

                   expr.Type = Type.Bool;

                 } else if (!err) {

                   expr.Type = e.E0.Type;

@@ -6683,7 +6691,7 @@ namespace Microsoft.Dafny
             break;

 

           case BinaryExpr.Opcode.Div:

-            if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false))) {

+            if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false, false))) {

               Error(expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

             }

             if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

@@ -6693,7 +6701,7 @@ namespace Microsoft.Dafny
             break;

 

           case BinaryExpr.Opcode.Mod:

-            if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false))) {

+            if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false, false))) {

               Error(expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);

             }

             if (!UnifyTypes(e.E1.Type, e.E0.Type)) {

@@ -8408,7 +8416,7 @@ namespace Microsoft.Dafny
       if (e.E1 != null) {

         ResolveExpression(e.E1, opts);

         Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression

-        var domType = e.E0 == null ? domainType : new OperationTypeProxy(true, false, false, false);  // reuse 'domainType' if .E0 did not use it; otherwise, create a new proxy to allow .E1 to be any integer-based numeric type, independent of the integer-based numeric type used by .E0

+        var domType = e.E0 == null ? domainType : new OperationTypeProxy(true, false, false, false, false);  // reuse 'domainType' if .E0 did not use it; otherwise, create a new proxy to allow .E1 to be any integer-based numeric type, independent of the integer-based numeric type used by .E0

         if (!UnifyTypes(e.E1.Type, domType)) {

           Error(e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domType);

         }

@@ -8476,6 +8484,8 @@ namespace Microsoft.Dafny
             return BinaryExpr.ResolvedOpcode.ProperMultiSubset;

           } else if (operandType is SeqType) {

             return BinaryExpr.ResolvedOpcode.ProperPrefix;

+          } else if (operandType is CharType) {

+            return BinaryExpr.ResolvedOpcode.LtChar;

           } else {

             return BinaryExpr.ResolvedOpcode.Lt;

           }

@@ -8486,6 +8496,8 @@ namespace Microsoft.Dafny
             return BinaryExpr.ResolvedOpcode.MultiSubset;

           } else if (operandType is SeqType) {

             return BinaryExpr.ResolvedOpcode.Prefix;

+          } else if (operandType is CharType) {

+            return BinaryExpr.ResolvedOpcode.LeChar;

           } else {

             return BinaryExpr.ResolvedOpcode.Le;

           }

@@ -8524,6 +8536,8 @@ namespace Microsoft.Dafny
             return BinaryExpr.ResolvedOpcode.ProperSuperset;

           } else if (operandType is MultiSetType) {

             return BinaryExpr.ResolvedOpcode.ProperMultiSuperset;

+          } else if (operandType is CharType) {

+            return BinaryExpr.ResolvedOpcode.GtChar;

           } else {

             return BinaryExpr.ResolvedOpcode.Gt;

           }

@@ -8532,6 +8546,8 @@ namespace Microsoft.Dafny
             return BinaryExpr.ResolvedOpcode.Superset;

           } else if (operandType is MultiSetType) {

             return BinaryExpr.ResolvedOpcode.MultiSuperset;

+          } else if (operandType is CharType) {

+            return BinaryExpr.ResolvedOpcode.GeChar;

           } else {

             return BinaryExpr.ResolvedOpcode.Ge;

           }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 6f86f4d1..1086a79b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -8711,7 +8711,7 @@ namespace Microsoft.Dafny {
 

       int N = types0.Count;

 

-      // compute eq and less for each component of the lexicographic pair

+      // compute eq and less for each component of the lexicographic tuple

       List<Bpl.Expr> Eq = new List<Bpl.Expr>(N);

       List<Bpl.Expr> Less = new List<Bpl.Expr>(N);

       for (int i = 0; i < N; i++) {

@@ -8839,8 +8839,10 @@ namespace Microsoft.Dafny {
         atmost = Bpl.Expr.Imp(e0, e1);

       } else if (ty0 is CharType) {

         eq = Bpl.Expr.Eq(e0, e1);

-        less = Bpl.Expr.False;

-        atmost = eq;  // less || eq

+        var operand0 = FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, e0);

+        var operand1 = FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, e1);

+        less = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Lt, operand0, operand1);

+        atmost = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Le, operand0, operand1);

       } else if (ty0.IsNumericBased(Type.NumericPersuation.Int) || ty0 is SeqType || ty0.IsDatatype) {

         Bpl.Expr b0, b1;

         if (ty0.IsNumericBased(Type.NumericPersuation.Int)) {

@@ -10710,6 +10712,26 @@ namespace Microsoft.Dafny {
               typ = Bpl.Type.Int;

               bOpcode = BinaryOperator.Opcode.Mod; break;

 

+            case BinaryExpr.ResolvedOpcode.LtChar:

+            case BinaryExpr.ResolvedOpcode.LeChar:

+            case BinaryExpr.ResolvedOpcode.GeChar:

+            case BinaryExpr.ResolvedOpcode.GtChar: {

+                // work off the original operands (that is, allow them to be lit-wrapped)

+                var operand0 = translator.FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, oe0);

+                var operand1 = translator.FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, oe1);

+                BinaryOperator.Opcode bOp;

+                switch (e.ResolvedOp) {

+                  case BinaryExpr.ResolvedOpcode.LtChar:  bOp = BinaryOperator.Opcode.Lt; break;

+                  case BinaryExpr.ResolvedOpcode.LeChar: bOp = BinaryOperator.Opcode.Le; break;

+                  case BinaryExpr.ResolvedOpcode.GeChar: bOp = BinaryOperator.Opcode.Ge; break;

+                  case BinaryExpr.ResolvedOpcode.GtChar: bOp = BinaryOperator.Opcode.Gt; break;

+                  default:

+                    Contract.Assert(false);  // unexpected case

+                    throw new cce.UnreachableException();  // to please compiler

+                }

+                return Bpl.Expr.Binary(expr.tok, bOp, operand0, operand1);

+              }

+

             case BinaryExpr.ResolvedOpcode.SetEq:

               return translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1);

             case BinaryExpr.ResolvedOpcode.SetNeq:

@@ -11364,6 +11386,7 @@ namespace Microsoft.Dafny {
       LitReal,

       LayerSucc,

       CharFromInt,

+      CharToInt,

       

       Is, IsBox,

       IsAlloc, IsAllocBox,

@@ -11520,6 +11543,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "char#FromInt", predef.CharType, args);

+        case BuiltinFunction.CharToInt:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "char#ToInt", predef.CharType, args);

 

         case BuiltinFunction.Is:

           Contract.Assert(args.Length == 2);

diff --git a/Test/dafny0/Char.dfy b/Test/dafny0/Char.dfy
new file mode 100644
index 00000000..0abfbec5
--- /dev/null
+++ b/Test/dafny0/Char.dfy
@@ -0,0 +1,66 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+class CharChar {

+  var c: char;

+  var d: char;

+

+  method Order()

+    modifies this;

+    ensures c <= d;

+  {

+    if d < c {

+      c, d := d, c;

+    }

+  }

+

+  function Recurse(ch: char): bool

+    reads this;

+  {

+    if c < ch then Recurse(c)

+    else if d < ch then Recurse(d)

+    else ch == ' '

+  }

+

+  function MinChar(s: string): char

+    requires s != "";

+  {

+    var ch := s[0];

+    if |s| == 1 then ch else

+    var m := MinChar(s[1..]);

+    if m < ch then m else ch

+  }

+  lemma MinCharLemma(s: string)

+    requires |s| != 0;

+    ensures forall i :: 0 <= i < |s| ==> MinChar(s) <= s[i];

+  {

+    if 2 <= |s| {

+      var m := MinChar(s[1..]);

+      assert forall i :: 1 <= i < |s| ==> m <= s[1..][i-1] == s[i];

+    }

+  }

+

+  method CharEq(s: string) {

+    if "hello Dafny" <= s {

+      assert s[6] == 'D';

+      assert s[7] == '\u0061';

+      if * {

+        assert s[9] == '\n';  // error

+      } else if * {

+        assert s[1] < s[2] <= s[3];

+      } else {

+        assert s[0] <= s[5];  // error

+      }

+    }

+  }

+  method CharInbetween(ch: char)

+    requires 'B' < ch;

+  {

+    if ch < 'D' {

+      assert 'C' <= ch <= 'C';

+      assert ch == 'C';

+    } else {

+      assert ch <= 'M';  // error

+    }

+  }

+}

diff --git a/Test/dafny0/Char.dfy.expect b/Test/dafny0/Char.dfy.expect
new file mode 100644
index 00000000..55418934
--- /dev/null
+++ b/Test/dafny0/Char.dfy.expect
@@ -0,0 +1,16 @@
+Char.dfy(48,21): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+    (0,0): anon10_Then

+Char.dfy(52,21): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+    (0,0): anon11_Else

+Char.dfy(63,17): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+

+Dafny program verifier finished with 8 verified, 3 errors

diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy
index f56f36e1..9e5c6a8f 100644
--- a/Test/dafny0/Strings.dfy
+++ b/Test/dafny0/Strings.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%2.dprint" "%s" > "%t"

+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 method Char(a: char, s: string, i: int) returns (b: char)