From bea62cec16ae455c2644a82d6425749f2eac0184 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Wed, 23 Sep 2015 11:51:26 -0700 Subject: fixed bugs related to identifying newtypes as types of integers and reals. --- Source/Dafny/DafnyAst.cs | 21 ++++++++++++----- Source/Dafny/Resolver.cs | 60 +++++++++++++++++++++++++----------------------- 2 files changed, 46 insertions(+), 35 deletions(-) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 600f7473..116b9004 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -5223,7 +5223,9 @@ namespace Microsoft.Dafny { public static Expression CreateAdd(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType)); + Contract.Requires( + (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) || + (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real))); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add; // resolve here @@ -5265,8 +5267,12 @@ namespace Microsoft.Dafny { /// public static Expression CreateSubtract(Expression e0, Expression e1) { Contract.Requires(e0 != null); + Contract.Requires(e0.Type != null); Contract.Requires(e1 != null); - Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType)); + Contract.Requires(e1.Type != null); + Contract.Requires( + (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) || + (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real))); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub; // resolve here @@ -5279,7 +5285,8 @@ namespace Microsoft.Dafny { /// public static Expression CreateIncrement(Expression e, int n) { Contract.Requires(e != null); - Contract.Requires(e.Type.IsIntegerType); + Contract.Requires(e.Type != null); + Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuation.Int)); Contract.Requires(0 <= n); Contract.Ensures(Contract.Result() != null); if (n == 0) { @@ -5294,7 +5301,7 @@ namespace Microsoft.Dafny { /// public static Expression CreateDecrement(Expression e, int n) { Contract.Requires(e != null); - Contract.Requires(e.Type.IsIntegerType); + Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuation.Int)); Contract.Requires(0 <= n); Contract.Ensures(Contract.Result() != null); if (n == 0) { @@ -5353,7 +5360,7 @@ namespace Microsoft.Dafny { public static Expression CreateLess(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires(e0.Type.IsIntegerType && e1.Type.IsIntegerType); + Contract.Requires(e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt; // resolve here @@ -5367,7 +5374,9 @@ namespace Microsoft.Dafny { public static Expression CreateAtMost(Expression e0, Expression e1) { Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType)); + Contract.Requires( + (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) || + (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real))); Contract.Ensures(Contract.Result() != null); var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1); s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le; // resolve here diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a2ae401a..210cd4ac 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -7305,41 +7305,43 @@ namespace Microsoft.Dafny } eIter = ei.Seq; } - var e0 = eIter; - - // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)" - // Wrapping it in a let expr avoids exponential growth in the size of the expression - // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" to - // "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)" - - // Create a unique name for d', the variable we introduce in the let expression - string tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext); - IdentifierExpr tmpVarIdExpr = new IdentifierExpr(e0.tok, tmpName); - BoundVar tmpVarBv = new BoundVar(e0.tok, tmpName, e0.Type); - - // Build the arguments to the datatype constructor, using the updated value in the appropriate slot - List ctor_args = new List(); - foreach (Formal d in ctor.Formals) { - Expression v = null; - foreach (var dvPair in IndexToValue.Values) { - var destructor = dvPair.Item1; - if (d == destructor.CorrespondingFormal) { - Contract.Assert(v == null); - v = dvPair.Item2; + if (ctor != null) { + var e0 = eIter; + + // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)" + // Wrapping it in a let expr avoids exponential growth in the size of the expression + // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" to + // "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)" + + // Create a unique name for d', the variable we introduce in the let expression + string tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext); + IdentifierExpr tmpVarIdExpr = new IdentifierExpr(e0.tok, tmpName); + BoundVar tmpVarBv = new BoundVar(e0.tok, tmpName, e0.Type); + + // Build the arguments to the datatype constructor, using the updated value in the appropriate slot + List ctor_args = new List(); + foreach (Formal d in ctor.Formals) { + Expression v = null; + foreach (var dvPair in IndexToValue.Values) { + var destructor = dvPair.Item1; + if (d == destructor.CorrespondingFormal) { + Contract.Assert(v == null); + v = dvPair.Item2; + } } + ctor_args.Add(v ?? new ExprDotName(expr.tok, tmpVarIdExpr, d.Name, null)); } - ctor_args.Add(v ?? new ExprDotName(expr.tok, tmpVarIdExpr, d.Name, null)); - } - DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args); + DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args); - CasePattern tmpVarPat = new CasePattern(e0.tok, tmpVarBv); - LetExpr let = new LetExpr(e0.tok, new List() { tmpVarPat }, new List() { e0 }, ctor_call, true); + CasePattern tmpVarPat = new CasePattern(e0.tok, tmpVarBv); + LetExpr let = new LetExpr(e0.tok, new List() { tmpVarPat }, new List() { e0 }, ctor_call, true); - ResolveExpression(let, opts); - e.ResolvedUpdateExpr = let; + ResolveExpression(let, opts); + e.ResolvedUpdateExpr = let; - expr.Type = e0.Type; + expr.Type = e0.Type; + } } else { reporter.Error(MessageSource.Resolver, expr, "update requires a sequence, map, or datatype (got {0})", e.Seq.Type); } -- cgit v1.2.3