diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 3 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 12 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 22 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 68 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 33 | ||||
| -rw-r--r-- | Test/dafny0/Char.dfy | 66 | ||||
| -rw-r--r-- | Test/dafny0/Char.dfy.expect | 16 | ||||
| -rw-r--r-- | Test/dafny0/Strings.dfy | 2 |
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)
|