From ac659e1ffa8d3f664daaa9f5394e007ca75cb3d1 Mon Sep 17 00:00:00 2001 From: chrishaw Date: Tue, 9 Dec 2014 14:36:12 -0800 Subject: Add nativeType attribute for newtype declarations. Change Compiler.cs to use native C# representation of small integer newtypes. Examples: newtype{:nativeType "byte"} byte = i:int | 0 <= i < 0x100 newtype{:nativeType "sbyte"} sbyte = i:int | -0x80 <= i < 0x80 newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000 newtype{:nativeType "short"} int16 = i:int | -0x8000 <= i < 0x8000 newtype{:nativeType "uint"} uint32 = i:int | 0 <= i < 0x100000000 newtype{:nativeType "int"} int32 = i:int | -0x80000000 <= i < 0x80000000 newtype{:nativeType "ulong"} uint64 = i:int | 0 <= i < 0x10000000000000000 newtype{:nativeType "long"} int64 = i:int | -0x8000000000000000 <= i < 0x8000000000000000 newtype month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise BigInteger newtype{:nativeType} month = i:int | 0 <= i < 12 // same as {:nativeType true} newtype{:nativeType true} month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise error newtype{:nativeType false} month = i:int | 0 <= i < 12 // use BigInteger newtype{:nativeType "uint"} month = i:int | 0 <= i < 12 // use C# uint type if possible, otherwise error newtype{:nativeType} even20 = i:int | 0 <= i < 20 && (i % 2 == 0) // nativeTypes need not be contiguous newtype{:nativeType} even10 = i:even20 | i < 10 // nativeTypes can inherit constraints from other nativeTypes --- Binaries/DafnyRuntime.cs | 129 +++++++++++++++++++++++++++++++++++++++++++---- Source/Dafny/Compiler.cs | 85 ++++++++++++++++++++++++++----- Source/Dafny/DafnyAst.cs | 87 ++++++++++++++++++++++++++++++++ Source/Dafny/Resolver.cs | 101 +++++++++++++++++++++++++++++++++++++ 4 files changed, 379 insertions(+), 23 deletions(-) diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 661666ef..a1d9037d 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -437,8 +437,11 @@ namespace Dafny public static Sequence FromString(string s) { return new Sequence(s.ToCharArray()); } - public BigInteger Length { - get { return new BigInteger(elmts.Length); } + public int Length { + get { return elmts.Length; } + } + public long LongLength { + get { return elmts.LongLength; } } public T[] Elements { get { @@ -451,14 +454,32 @@ namespace Dafny return st.Elements; } } + public T Select(ulong index) { + return elmts[index]; + } + public T Select(long index) { + return elmts[index]; + } + public T Select(uint index) { + return elmts[index]; + } + public T Select(int index) { + return elmts[index]; + } public T Select(BigInteger index) { return elmts[(int)index]; } - public Sequence Update(BigInteger index, T t) { + public Sequence Update(long index, T t) { T[] a = (T[])elmts.Clone(); - a[(int)index] = t; + a[index] = t; return new Sequence(a); } + public Sequence Update(ulong index, T t) { + return Update((long)index, t); + } + public Sequence Update(BigInteger index, T t) { + return Update((long)index, t); + } public bool Equals(Sequence other) { int n = elmts.Length; return n == other.elmts.Length && EqualUntil(other, n); @@ -519,22 +540,34 @@ namespace Dafny } return false; } - public Sequence Take(BigInteger n) { - int m = (int)n; - if (elmts.Length == m) + public Sequence Take(long m) { + if (elmts.LongLength == m) return this; T[] a = new T[m]; System.Array.Copy(elmts, a, m); return new Sequence(a); } - public Sequence Drop(BigInteger n) { - if (n.IsZero) + public Sequence Take(ulong n) { + return Take((long)n); + } + public Sequence Take(BigInteger n) { + return Take((long)n); + } + public Sequence Drop(long m) { + if (m == 0) return this; - int m = (int)n; T[] a = new T[elmts.Length - m]; System.Array.Copy(elmts, m, a, 0, elmts.Length - m); return new Sequence(a); } + public Sequence Drop(ulong n) { + return Drop((long)n); + } + public Sequence Drop(BigInteger n) { + if (n.IsZero) + return this; + return Drop((long)n); + } } public struct Pair { @@ -604,6 +637,50 @@ namespace Dafny } // pre: b != 0 // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) + public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) { + return (sbyte)EuclideanDivision(a, b); + } + public static short EuclideanDivision_short(short a, short b) { + return (short)EuclideanDivision(a, b); + } + public static int EuclideanDivision_int(int a, int b) { + if (0 <= a) { + if (0 <= b) { + // +a +b: a/b + return (int)(((uint)(a)) / ((uint)(b))); + } else { + // +a -b: -(a/(-b)) + return -((int)(((uint)(a)) / ((uint)(unchecked(-b))))); + } + } else { + if (0 <= b) { + // -a +b: -((-a-1)/b) - 1 + return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1; + } + } + } + public static long EuclideanDivision_long(long a, long b) { + if (0 <= a) { + if (0 <= b) { + // +a +b: a/b + return (long)(((ulong)(a)) / ((ulong)(b))); + } else { + // +a -b: -(a/(-b)) + return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b))))); + } + } else { + if (0 <= b) { + // -a +b: -((-a-1)/b) - 1 + return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1; + } + } + } public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) { if (0 <= a.Sign) { if (0 <= b.Sign) { @@ -625,6 +702,38 @@ namespace Dafny } // pre: b != 0 // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) + public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) { + return (sbyte)EuclideanModulus(a, b); + } + public static short EuclideanModulus_short(short a, short b) { + return (short)EuclideanModulus(a, b); + } + public static int EuclideanModulus_int(int a, int b) { + uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b)); + if (0 <= a) { + // +a: a % b' + return (int)(((uint)a) % bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + uint c = ((uint)(unchecked(-a))) % bp; + return (int)(c == 0 ? c : bp - c); + } + } + public static long EuclideanModulus_long(long a, long b) { + ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b)); + if (0 <= a) { + // +a: a % b' + return (long)(((ulong)a) % bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + ulong c = ((ulong)(unchecked(-a))) % bp; + return (long)(c == 0 ? c : bp - c); + } + } public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) { var bp = BigInteger.Abs(b); if (0 <= a.Sign) { diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index a4541414..485fe661 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -953,6 +953,14 @@ namespace Microsoft.Dafny { readonly string DafnySeqClass = "Dafny.Sequence"; readonly string DafnyMapClass = "Dafny.Map"; + NativeType AsNativeType(Type typ) { + Contract.Requires(typ != null); + if (typ.AsNewtype != null) { + return typ.AsNewtype.NativeType; + } + return null; + } + string TypeName(Type type) { Contract.Requires(type != null); @@ -973,6 +981,10 @@ namespace Microsoft.Dafny { } else if (type is RealType) { return "Dafny.BigRational"; } else if (type.AsNewtype != null) { + NativeType nativeType = type.AsNewtype.NativeType; + if (nativeType != null) { + return nativeType.Name; + } return TypeName(type.AsNewtype.BaseType); } else if (type is ObjectType) { return "object"; @@ -1070,6 +1082,9 @@ namespace Microsoft.Dafny { } else if (type is RealType) { return "Dafny.BigRational.ZERO"; } else if (type.AsNewtype != null) { + if (type.AsNewtype.NativeType != null) { + return "0"; + } return DefaultValue(type.AsNewtype.BaseType); } else if (type.IsRefType) { return string.Format("({0})null", TypeName(type)); @@ -2057,6 +2072,8 @@ namespace Microsoft.Dafny { } else if (e is StringLiteralExpr) { var str = (StringLiteralExpr)e; wr.Write("{0}.FromString({1}\"{2}\")", DafnySeqClass, str.IsVerbatim ? "@" : "", (string)e.Value); + } else if (AsNativeType(e.Type) != null) { + wr.Write((BigInteger)e.Value + AsNativeType(e.Type).Suffix); } else if (e.Value is BigInteger) { BigInteger i = (BigInteger)e.Value; if (new BigInteger(int.MinValue) <= i && i <= new BigInteger(int.MaxValue)) { @@ -2291,14 +2308,9 @@ namespace Microsoft.Dafny { TrParenExpr(e.E); break; case UnaryOpExpr.Opcode.Cardinality: - if (e.E.Type.IsArrayType) { - wr.Write("new BigInteger("); - TrParenExpr(e.E); - wr.Write(".Length)"); - } else { - TrParenExpr(e.E); - wr.Write(".Length"); - } + wr.Write("new BigInteger("); + TrParenExpr(e.E); + wr.Write(".Length)"); break; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression @@ -2310,17 +2322,54 @@ namespace Microsoft.Dafny { Contract.Assert(fromInt || e.E.Type.IsNumericBased(Type.NumericPersuation.Real)); var toInt = e.ToType.IsNumericBased(Type.NumericPersuation.Int); Contract.Assert(toInt || e.ToType.IsNumericBased(Type.NumericPersuation.Real)); + Action fromIntAsBigInteger = () => { + Contract.Assert(fromInt); + if (AsNativeType(e.E.Type) != null) { + wr.Write("new BigInteger"); + } + TrParenExpr(e.E); + }; + Action toIntCast = () => { + Contract.Assert(toInt); + if (AsNativeType(e.ToType) != null) { + wr.Write("(" + AsNativeType(e.ToType).Name + ")"); + } + }; if (fromInt && !toInt) { // int -> real wr.Write("new Dafny.BigRational("); - TrExpr(e.E); + fromIntAsBigInteger(); wr.Write(", BigInteger.One)"); } else if (!fromInt && toInt) { // real -> int + toIntCast(); TrParenExpr(e.E); wr.Write(".ToBigInteger()"); + } else if (AsNativeType(e.ToType) != null) { + toIntCast(); + LiteralExpr lit = e.E.Resolved as LiteralExpr; + UnaryOpExpr u = e.E.Resolved as UnaryOpExpr; + MemberSelectExpr m = e.E.Resolved as MemberSelectExpr; + if (lit != null && lit.Value is BigInteger) { + // Optimize constant to avoid intermediate BigInteger + wr.Write("(" + (BigInteger)lit.Value + AsNativeType(e.ToType).Suffix + ")"); + } else if ((u != null && u.Op == UnaryOpExpr.Opcode.Cardinality) || (m != null && m.MemberName == "Length" && m.Obj.Type.IsArrayType)) { + // Optimize .Length to avoid intermediate BigInteger + TrParenExpr((u != null) ? u.E : m.Obj); + if (AsNativeType(e.ToType).UpperBound <= new BigInteger(0x80000000U)) { + wr.Write(".Length"); + } else { + wr.Write(".LongLength"); + } + } else { + TrParenExpr(e.E); + } + } else if (e.ToType.IsIntegerType && AsNativeType(e.E.Type) != null) { + fromIntAsBigInteger(); } else { Contract.Assert(fromInt == toInt); + Contract.Assert(AsNativeType(e.ToType) == null); + Contract.Assert(AsNativeType(e.E.Type) == null); TrParenExpr(e.E); } @@ -2387,8 +2436,9 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.Mul: opString = "*"; break; case BinaryExpr.ResolvedOpcode.Div: - if (expr.Type.IsIntegerType) { - wr.Write("Dafny.Helpers.EuclideanDivision("); + if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) { + string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : ""; + wr.Write("Dafny.Helpers.EuclideanDivision" + suffix + "("); TrParenExpr(e.E0); wr.Write(", "); TrExpr(e.E1); @@ -2398,8 +2448,9 @@ namespace Microsoft.Dafny { } break; case BinaryExpr.ResolvedOpcode.Mod: - if (expr.Type.IsIntegerType) { - wr.Write("Dafny.Helpers.EuclideanModulus("); + if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) { + string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : ""; + wr.Write("Dafny.Helpers.EuclideanModulus" + suffix + "("); TrParenExpr(e.E0); wr.Write(", "); TrExpr(e.E1); @@ -2485,10 +2536,18 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression } if (opString != null) { + NativeType nativeType = AsNativeType(e.Type); + bool needsCast = nativeType != null && nativeType.NeedsCastAfterArithmetic; + if (needsCast) { + wr.Write("(" + nativeType.Name + ")("); + } wr.Write(preOpString); TrParenExpr(e.E0); wr.Write(" {0} ", opString); TrParenExpr(e.E1); + if (needsCast) { + wr.Write(")"); + } } else if (callString != null) { wr.Write(preOpString); TrParenExpr(e.E0); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 9e5c1c7f..c028fe10 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -298,6 +298,72 @@ namespace Microsoft.Dafny { return false; } + + /// + /// Returns list of expressions if "nm" is a specified attribute: + /// - if the attribute is {:nm e1,...,en}, then returns (e1,...,en) + /// Otherwise, returns null. + /// + public static List FindExpressions(Attributes attrs, string nm) { + Contract.Requires(nm != null); + for (; attrs != null; attrs = attrs.Prev) { + if (attrs.Name == nm) { + return attrs.Args; + } + } + return null; + } + + /// + /// Returns true if "nm" is a specified attribute whose arguments match the "allowed" parameter. + /// - if "nm" is not found in attrs, return false and leave value unmodified. Otherwise, + /// - if "allowed" contains Empty and the Args contains zero elements, return true and leave value unmodified. Otherwise, + /// - if "allowed" contains Bool and Args contains one bool literal, return true and set value to the bool literal. Otherwise, + /// - if "allowed" contains Int and Args contains one BigInteger literal, return true and set value to the BigInteger literal. Otherwise, + /// - if "allowed" contains String and Args contains one string literal, return true and set value to the string literal. Otherwise, + /// - if "allowed" contains Expression and Args contains one element, return true and set value to the one element (of type Expression). Otherwise, + /// - return false, leave value unmodified, and call errorReporter with an error string. + /// + public enum MatchingValueOption { Empty, Bool, Int, String, Expression } + public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object value, IEnumerable allowed, Action errorReporter) { + Contract.Requires(nm != null); + Contract.Requires(allowed != null); + Contract.Requires(errorReporter != null); + List args = FindExpressions(attrs, nm); + if (args == null) { + return false; + } else if (args.Count == 0) { + if (allowed.Contains(MatchingValueOption.Empty)) { + return true; + } else { + errorReporter("Attribute " + nm + " requires one argument"); + return false; + } + } else if (args.Count == 1) { + Expression arg = args[0]; + StringLiteralExpr stringLiteral = arg as StringLiteralExpr; + LiteralExpr literal = arg as LiteralExpr; + if (literal != null && literal.Value is bool && allowed.Contains(MatchingValueOption.Bool)) { + value = literal.Value; + return true; + } else if (literal != null && literal.Value is BigInteger && allowed.Contains(MatchingValueOption.Int)) { + value = literal.Value; + return true; + } else if (stringLiteral != null && (stringLiteral.Value as string) != null && allowed.Contains(MatchingValueOption.String)) { + value = stringLiteral.Value; + return true; + } else if (allowed.Contains(MatchingValueOption.Expression)) { + value = arg; + return true; + } else { + errorReporter("Attribute " + nm + " expects an argument in one of the following categories: " + String.Join(", ", allowed)); + return false; + } + } else { + errorReporter("Attribute " + nm + " cannot have more than one argument"); + return false; + } + } } // ------------------------------------------------------------------------------------------------------ @@ -2281,11 +2347,32 @@ namespace Microsoft.Dafny { string Name { get; } } + public class NativeType + { + public readonly string Name; + public readonly BigInteger LowerBound; + public readonly BigInteger UpperBound; + public readonly string Suffix; + public readonly bool NeedsCastAfterArithmetic; + public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, string Suffix, bool NeedsCastAfterArithmetic) { + Contract.Requires(Name != null); + Contract.Requires(LowerBound != null); + Contract.Requires(UpperBound != null); + Contract.Requires(Suffix != null); + this.Name = Name; + this.LowerBound = LowerBound; + this.UpperBound = UpperBound; + this.Suffix = Suffix; + this.NeedsCastAfterArithmetic = NeedsCastAfterArithmetic; + } + } + public class NewtypeDecl : TopLevelDecl, RedirectingTypeDecl { public readonly Type BaseType; public readonly BoundVar Var; // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType)) public readonly Expression Constraint; // is null iff Var is + public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers) public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes) : base(tok, name, module, new List(), attributes) { Contract.Requires(tok != null); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d38076fd..79421d0f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1205,6 +1205,17 @@ namespace Microsoft.Dafny private readonly List needFiniteBoundsChecks = new List(); public int NFBC_Count { get { return needFiniteBoundsChecks.Count; } } // provided just for the purpose of conveniently writing contracts for ResolveTopLevelDecl_Meat + static readonly List NativeTypes = new List() { + new NativeType("byte", 0, 0x100, "", true), + new NativeType("sbyte", -0x80, 0x80, "", true), + new NativeType("ushort", 0, 0x10000, "", true), + new NativeType("short", -0x8000, 0x8000, "", true), + new NativeType("uint", 0, 0x100000000, "U", false), + new NativeType("int", -0x80000000, 0x80000000, "", false), + new NativeType("ulong", 0, new BigInteger(0x100000000) * new BigInteger(0x100000000), "UL", false), + new NativeType("long", Int64.MinValue, 0x8000000000000000, "L", false), + }; + public void ResolveTopLevelDecls_Meat(List/*!*/ declarations, Graph/*!*/ datatypeDependencies, Graph/*!*/ codatatypeDependencies) { Contract.Requires(declarations != null); Contract.Requires(cce.NonNullElements(datatypeDependencies)); @@ -1288,6 +1299,11 @@ namespace Microsoft.Dafny } needFiniteBoundsChecks.Clear(); + Dictionary nativeTypeMap = new Dictionary(); + foreach (var nativeType in NativeTypes) { + nativeTypeMap.Add(nativeType.Name, nativeType); + } + if (ErrorCount == prevErrorCount) { // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions foreach (TopLevelDecl d in declarations) { @@ -1302,9 +1318,94 @@ namespace Microsoft.Dafny cl.Members.Iter(CheckTypeInference_Member); } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; + bool? boolNativeType = null; + NativeType stringNativeType = null; + object nativeTypeAttr = true; + bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr, + new Attributes.MatchingValueOption[] { + Attributes.MatchingValueOption.Empty, + Attributes.MatchingValueOption.Bool, + Attributes.MatchingValueOption.String }, + err => Error(dd, err)); + if (hasNativeTypeAttr) { + if (nativeTypeAttr is bool) { + boolNativeType = (bool)nativeTypeAttr; + } else { + string keyString = (string)nativeTypeAttr; + if (nativeTypeMap.ContainsKey(keyString)) { + stringNativeType = nativeTypeMap[keyString]; + } else { + Error(dd, "Unsupported nativeType {0}", keyString); + } + } + } + if (stringNativeType != null || boolNativeType == true) { + if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) { + Error(dd, "nativeType can only be used on integral types"); + } + if (dd.Var == null) { + Error(dd, "nativeType can only be used if newtype specifies a constraint"); + } + } if (dd.Var != null) { Contract.Assert(dd.Constraint != null); CheckTypeInference(dd.Constraint); + + Func GetConst = null; + GetConst = (Expression e) => { + int m = 1; + BinaryExpr bin = e as BinaryExpr; + if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) { + m = -1; + e = bin.E1; + } + LiteralExpr l = e as LiteralExpr; + if (l != null && l.Value is BigInteger) { + return m * (BigInteger)l.Value; + } + return null; + }; + var missingBounds = new List(); + var bounds = DiscoverBounds(dd.Constraint.tok, new List { dd.Var }, dd.Constraint, + true, true, missingBounds); + List potentialNativeTypes = + (stringNativeType != null) ? new List { stringNativeType } : + (boolNativeType == false) ? new List() : + NativeTypes; + foreach (var nt in potentialNativeTypes) { + if (missingBounds.Count == 0) { + bool lowerOk = false; + bool upperOk = false; + foreach (var bound in bounds) { + if (bound is ComprehensionExpr.IntBoundedPool) { + var bnd = (ComprehensionExpr.IntBoundedPool)bound; + if (bnd.LowerBound != null) { + BigInteger? lower = GetConst(bnd.LowerBound); + if (lower != null && nt.LowerBound <= lower) { + lowerOk = true; + } + } + if (bnd.UpperBound != null) { + BigInteger? upper = GetConst(bnd.UpperBound); + if (upper != null && upper <= nt.UpperBound) { + upperOk = true; + } + } + } + } + if (lowerOk && upperOk) { + dd.NativeType = nt; + break; + } + } + } + if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) { + Error(dd, "Dafny's heuristics cannot find a compatible native type. " + + "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'"); + } + if (dd.NativeType != null && stringNativeType == null) { + ReportAdditionalInformation(dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}", dd.tok.val.Length); + } } } } -- cgit v1.2.3