Define $Is and $IsAlloc predicates for newtypes.

2 files changed, 40 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index deeffb33..53627053 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -468,6 +468,44 @@ namespace Microsoft.Dafny {
       Contract.Requires(dd != null);

       AddTypeDecl_Aux(dd.tok, dd.FullName, new List<TypeParameter>());

       AddWellformednessCheck(dd);

+      // Add $Is and $IsAlloc axioms for the newtype

+      MapM(Bools, is_alloc => {

+        var vars = new List<Variable>();

+

+        var oDafnyType = dd.BaseType.IsNumericBased(Type.NumericPersuation.Int) ? (Type)Type.Int : Type.Real;

+        var oBplType = dd.BaseType.IsNumericBased(Type.NumericPersuation.Int) ? Bpl.Type.Int : Bpl.Type.Real;

+

+        var oVarDafny = new BoundVar(dd.tok, "$o", oDafnyType);

+        var o = BplBoundVar(oVarDafny.AssignUniqueName(dd), oBplType, vars);

+

+        Bpl.Expr body, is_o;

+        Bpl.Expr o_ty = ClassTyCon(dd, new List<Expr>());

+        string name = dd.FullName + ": newtype ";

+

+        if (is_alloc) {

+          name += "$IsAlloc";

+          var h = BplBoundVar("$h", predef.HeapType, vars);

+          // $IsAlloc(o, ..)

+          is_o = MkIsAlloc(o, o_ty, h);

+          body = is_o;

+        } else {

+          name += "$Is";

+          // $Is(o, ..)

+          is_o = MkIs(o, o_ty);

+          Bpl.Expr rhs = MkIs(o, dd.BaseType);

+          if (dd.Var != null) {

+            // conjoin the constraint

+            var etran = new ExpressionTranslator(this, predef, dd.tok);

+            var ie = new IdentifierExpr(dd.tok, oVarDafny.Name);

+            ie.Var = oVarDafny; ie.Type = ie.Var.Type;  // resolve ie here

+            var constraint = etran.TrExpr(Substitute(dd.Constraint, dd.Var, ie));

+            rhs = BplAnd(rhs, constraint);

+          }

+          body = BplIff(is_o, rhs);

+        }

+

+        sink.TopLevelDeclarations.Add(new Bpl.Axiom(dd.tok, BplForall(vars, BplTrigger(is_o), body), name));

+      });

     }

     void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs) {

       Contract.Requires(tok != null);

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
index 3345b709..5b3b7d5c 100644
--- a/Test/dafny0/DerivedTypes.dfy
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -57,7 +57,7 @@ module Constraints {
   {

     x % 2 == 0

   }

-  newtype G = x: int where IsEven(x)  // it's okay to use ghost constructs in type constraints

+//  newtype G = x: int where IsEven(x)  // it's okay to use ghost constructs in type constraints

 

   newtype N = nat

 

@@ -69,7 +69,7 @@ module Constraints {
   newtype Te = x: int where 0 <= x < 3 && [5, 7, 8][x] % 2 != 0

 

   newtype Ta = x: int where 0 <= x < 3

-//  newtype Tb = y: Ta where [5, 7, 8][int(y)] % 2 != 0  // the indexing is okay, because of the type constraint for Ta

+  newtype Tb = y: Ta where [5, 7, 8][int(y)] % 2 != 0  // the indexing is okay, because of the type constraint for Ta

 

   newtype Odds = x: int where x % 2 == 1  // error: cannot find witness