Groebner extension

Binaries/DafnyPrelude.bpl

@@ -1461,3 +1461,23 @@ axiom (forall x, y, z: int ::
 #endif
 
 // -------------------------------------------------------------------------
+
+// function declaration for _System._default.rank__is__less__than
+function _System.__default.rank__is__less__than(A:Ty, B:Ty, a:Box, b:Box):bool;
+
+axiom (forall A:Ty, B:Ty, a:Box, b:Box ::
+  {_System.__default.rank__is__less__than(A, B, a, b), BoxRank(a)}
+  {_System.__default.rank__is__less__than(A, B, a, b), BoxRank(b)}
+  _System.__default.rank__is__less__than(A, B, a, b) ==> BoxRank(a) < BoxRank(b));
+
+axiom (forall A:Ty, B:Ty, a:Box, b:Seq Box ::
+  {_System.__default.rank__is__less__than(A, B, a, $Box(b)), BoxRank(a)}
+  {_System.__default.rank__is__less__than(A, B, a, $Box(b)), Seq#Rank(b)}
+  _System.__default.rank__is__less__than(A, B, a, $Box(b)) ==> BoxRank(a) < Seq#Rank(b));
+
+axiom (forall A:Ty, B:Ty, a:Seq Box, b:Box ::
+  {_System.__default.rank__is__less__than(A, B, $Box(a), b), Seq#Rank(a)}
+  {_System.__default.rank__is__less__than(A, B, $Box(a), b), BoxRank(b)}
+  _System.__default.rank__is__less__than(A, B, $Box(a), b) ==> Seq#Rank(a) < BoxRank(b));
+
+// -------------------------------------------------------------------------

Binaries/DafnyRuntime.h

@@ -15,6 +15,8 @@
 #include <cstdint>
 #include <variant>
 #include <exception>
+#include <smmintrin.h>
+#include <immintrin.h>
 
 typedef uint8_t  uint8;
 typedef uint16_t uint16;
@@ -97,11 +99,21 @@ struct get_default<unsigned int> {
   static unsigned int call() { return 0; }
 };
 
+template<>
+struct get_default<long> {
+  static long call() { return 0; }
+};
+
 template<>
 struct get_default<unsigned long> {
   static unsigned long call() { return 0; }
 };
 
+template<>
+struct get_default<long long> {
+  static long long call() { return 0; }
+};
+
 template<>
 struct get_default<unsigned long long> {
   static unsigned long long call() { return 0; }
@@ -118,6 +130,8 @@ struct get_default<std::shared_ptr<U>> {
  *  TUPLES                                               *
  *********************************************************/
 
+struct Tuple0 {};
+
 template <typename... Types>
 struct Tuple{
  public:
@@ -287,6 +301,13 @@ struct DafnySequence {
       std::copy(arr.begin(), arr.end(), start);
     }
 
+    DafnySequence(std::vector<T> vec) {
+      len = vec.size();
+      sptr = std::shared_ptr<T> (new T[len], std::default_delete<T[]>());
+      start = &*sptr;
+      std::copy(vec.begin(), vec.end(), start);
+     }
+
     DafnySequence(DafnyArray<T> arr, uint64 lo, uint64 hi) {
       len = hi - lo;
       sptr = std::shared_ptr<T> (new T[len], std::default_delete<T[]>());
@@ -465,6 +486,17 @@ struct std::hash<DafnyArray<U>> {
     }
 };
 
+template<typename U>
+struct std::hash<std::vector<U>> {
+  std::size_t operator()(const std::    vector<U>& x) const {
+    size_t seed = 0;
+    for (size_t i = 0; i < x.size(); i++) {
+      hash_combine<U>(seed, x[i]);
+    }
+    return seed;
+  }
+};
+
 /*********************************************************
  *  SETS                                                 *
  *********************************************************/

Source/Dafny/Compiler-Csharp.cs

@@ -211,7 +211,7 @@ private void EmitTypeDescriptorMethod(TopLevelDecl enclosingTypeDecl, TargetWrit
       Contract.Requires(wr != null);
 
       var type = UserDefinedType.FromTopLevelDecl(enclosingTypeDecl.tok, enclosingTypeDecl);
-      var initializer = TypeInitializationValue(type, wr, enclosingTypeDecl.tok, false, true);
+      var initializer = TypeInitializationValue(type, wr, enclosingTypeDecl.tok, Usage.Ordinary, false, true);
 
       var targetTypeName = TypeName(type, wr, enclosingTypeDecl.tok);
       var typeDescriptorExpr = $"new {DafnyTypeDescriptor}<{targetTypeName}>({initializer})";
@@ -286,7 +286,7 @@ protected override BlockTargetWriter CreateIterator(IteratorDecl iter, TargetWri
       foreach (var member in iter.Members) {
         var f = member as Field;
         if (f != null && !f.IsGhost) {
-          cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, DefaultValue(f.Type, w, f.tok, true), f);
+          cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, DefaultValue(f.Type, w, f.tok, Usage.Ordinary, true), f);
         } else if (member is Constructor) {
           Contract.Assert(ct == null);  // we're expecting just one constructor
           ct = (Constructor)member;
@@ -410,7 +410,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, TargetWriter wr) {
       wDefault.Write(DtCreateName(groundingCtor));
       wDefault.Write("(");
       var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost);
-      wDefault.Write(Util.Comma(nonGhostFormals, f => DefaultValue(f.Type, wDefault, f.tok)));
+      wDefault.Write(Util.Comma(nonGhostFormals, f => DefaultValue(f.Type, wDefault, f.tok, f.Usage)));
       wDefault.Write(")");
 
       EmitTypeDescriptorMethod(dt, wr);
@@ -815,7 +815,7 @@ public BlockTargetWriter Writer(bool isStatic, bool createBody, MemberDecl/*?*/
       public BlockTargetWriter/*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
         return Compiler.CreateMethod(m, typeArgs, createBody, Writer(m.IsStatic, createBody, m), forBodyInheritance, lookasideBody);
       }
-      public BlockTargetWriter/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) {
+      public BlockTargetWriter/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Usage resultUsage, Bpl.IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) {
         return Compiler.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, Writer(isStatic, createBody, member), forBodyInheritance, lookasideBody);
       }
       public BlockTargetWriter/*?*/ CreateGetter(string name, TopLevelDecl enclosingDecl, Type resultType, Bpl.IToken tok, bool isStatic, bool isConst, bool createBody, MemberDecl/*?*/ member, bool forBodyInheritance) {
@@ -866,7 +866,7 @@ public void Finish() { }
       if (customReceiver) {
         var nt = m.EnclosingClass;
         var receiverType = UserDefinedType.FromTopLevelDecl(m.tok, nt);
-        DeclareFormal(sep, "_this", receiverType, m.tok, true, wr);
+        DeclareFormal(sep, "_this", receiverType, m.tok, Usage.Ordinary, true, false, wr);
         nIns++;
         sep = ", ";
       }
@@ -907,7 +907,7 @@ public void Finish() { }
       if (customReceiver) {
         var nt = member.EnclosingClass;
         var receiverType = UserDefinedType.FromTopLevelDecl(tok, nt);
-        DeclareFormal(sep, "_this", receiverType, tok, true, wr);
+        DeclareFormal(sep, "_this", receiverType, tok, Usage.Ordinary, true, false, wr);
         sep = ", ";
       }
       WriteFormals(sep, formals, wr);
@@ -1102,7 +1102,7 @@ public string CommonTypeName(Type a, Type /*?*/ b, TextWriter wr, Bpl.IToken tok
       return "object";
     }
 
-    protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.IToken tok, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
+    protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.IToken tok, Usage usage, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
       var xType = type.NormalizeExpandKeepConstraints();
 
       if (usePlaceboValue) {
@@ -1141,7 +1141,7 @@ protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.
         } else if (td.NativeType != null) {
           return "0";
         } else {
-          return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
+          return TypeInitializationValue(td.BaseType, wr, tok, Usage.Ordinary, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
         }
       } else if (cl is SubsetTypeDecl) {
         var td = (SubsetTypeDecl)cl;
@@ -1153,7 +1153,7 @@ protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.
           if (ArrowType.IsPartialArrowTypeName(td.Name)) {
             return string.Format("(({0})null)", TypeName(xType, wr, udt.tok));
           } else if (ArrowType.IsTotalArrowTypeName(td.Name)) {
-            var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
+            var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, Usage.Ordinary, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
             // return the lambda expression ((Ty0 x0, Ty1 x1, Ty2 x2) => rangeDefaultValue)
             return string.Format("(({0}) => {1})",
               Util.Comma(udt.TypeArgs.Count - 1, i => string.Format("{0} x{1}", TypeName(udt.TypeArgs[i], wr, udt.tok), i)),
@@ -1171,7 +1171,7 @@ protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.
             return string.Format("default({0})", TypeName(xType, wr, udt.tok));
           }
         } else {
-          return TypeInitializationValue(td.RhsWithArgument(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
+          return TypeInitializationValue(td.RhsWithArgument(udt.TypeArgs), wr, tok, Usage.Ordinary, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
         }
       } else if (cl is ClassDecl) {
         bool isHandle = true;
@@ -1186,7 +1186,7 @@ protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.
           s += "<" + TypeNames(udt.TypeArgs, wr, udt.tok) + ">";
         }
         var relevantTypeArgs = UsedTypeParameters(dt, udt.TypeArgs);
-        return string.Format($"{s}.Default({Util.Comma(relevantTypeArgs, ta => DefaultValue(ta.Actual, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors))})");
+        return string.Format($"{s}.Default({Util.Comma(relevantTypeArgs, ta => DefaultValue(ta.Actual, wr, tok, Usage.Ordinary, constructTypeParameterDefaultsFromTypeDescriptors))})");
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
@@ -1366,12 +1366,12 @@ protected void DeclareField(string name, bool isPublic, bool isStatic, bool isCo
       }
     }
 
-    protected override bool DeclareFormal(string prefix, string name, Type type, Bpl.IToken tok, bool isInParam, TextWriter wr) {
+    protected override bool DeclareFormal(string prefix, string name, Type type, Bpl.IToken tok, Usage usage, bool isInParam, bool isInoutParam, TextWriter wr) {
       wr.Write("{0}{1}{2} {3}", prefix, isInParam ? "" : "out ", TypeName(type, wr, tok), name);
       return true;
     }
 
-    protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr) {
+    protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr) {
       wr.Write("{0} {1}", type != null ? TypeName(type, wr, tok) : "var", name);
       if (leaveRoomForRhs) {
         Contract.Assert(rhs == null);  // follows from precondition
@@ -1382,7 +1382,7 @@ protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/
       }
     }
 
-    protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, TargetWriter wr) {
+    protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr) {
       wr.Write("{0} {1} = ", type != null ? TypeName(type, wr, tok) : "var", name);
       var w = wr.Fork();
       wr.WriteLine(";");
@@ -1393,9 +1393,9 @@ protected override void DeclareOutCollector(string collectorVarName, TargetWrite
       wr.Write("var {0} = ", collectorVarName);
     }
 
-    protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
+    protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, Usage usage, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
       if (useReturnStyleOuts) {
-        DeclareLocalVar(name, type, tok, false, rhs, wr);
+        DeclareLocalVar(name, type, tok, usage, false, rhs, wr);
       } else {
         EmitAssignment(name, type, rhs, null, wr);
       }
@@ -1545,7 +1545,7 @@ protected override void EmitNew(Type type, Bpl.IToken tok, CallStmt/*?*/ initCal
           Formal p = ctor.Ins[i];
           if (!p.IsGhost) {
             wr.Write(sep);
-            TrExpr(initCall.Args[i], wr, false);
+            TrExpr(initCall.Args[i].Expr, wr, false);
             sep = ", ";
           }
         }
@@ -1588,7 +1588,7 @@ private List<TargetWriter> EmitNewArray(Type elmtType, Bpl.IToken tok, int dimCo
       } else {
         wr.Write("Dafny.ArrayHelpers.InitNewArray{0}<{1}>", dimCount, TypeName(elmtType, wr, tok));
         wr.Write("(");
-        wr.Write(DefaultValue(elmtType, wr, tok, true));
+        wr.Write(DefaultValue(elmtType, wr, tok, Usage.Ordinary,true));
         for (var d = 0; d < dimCount; d++) {
           wr.Write(", ");
           var w = wr.Fork();
@@ -2248,7 +2248,7 @@ private void EmitSeqConstructionExprFromLambda(Expression lengthExpr, BoundVar b
 
       var indexType = lengthExpr.Type;
       var lengthVar = FreshId("dim");
-      DeclareLocalVar(lengthVar, indexType, lengthExpr.tok, lengthExpr, inLetExprBody, wrLamBody);
+      DeclareLocalVar(lengthVar, indexType, lengthExpr.tok, boundVar.Usage, lengthExpr, inLetExprBody, wrLamBody);
       var arrVar = FreshId("arr");
       wrLamBody.Write("var {0} = ", arrVar);
       var wrDims = EmitNewArray(body.Type, body.tok, dimCount: 1, mustInitialize: false, wr: wrLamBody);
@@ -2699,12 +2699,12 @@ protected override void EmitMapDisplay(MapType mt, Bpl.IToken tok, List<Expressi
     }
 
     protected override void EmitSetBuilder_New(TargetWriter wr, SetComprehension e, string collectionName) {
-      var wrVarInit = DeclareLocalVar(collectionName, null, null, wr);
+      var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
       wrVarInit.Write("new System.Collections.Generic.List<{0}>()", TypeName(e.Type.AsSetType.Arg, wrVarInit, e.tok));
     }
 
     protected override void EmitMapBuilder_New(TargetWriter wr, MapComprehension e, string collectionName) {
-      var wrVarInit = DeclareLocalVar(collectionName, null, null, wr);
+      var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
       var mt = e.Type.AsMapType;
       var domtypeName = TypeName(mt.Domain, wrVarInit, e.tok);
       var rantypeName = TypeName(mt.Range, wrVarInit, e.tok);