summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl24
-rw-r--r--Source/Dafny/DafnyAst.cs11
-rw-r--r--Source/Dafny/DafnyMain.cs12
-rw-r--r--Source/Dafny/DafnyOptions.cs10
-rw-r--r--Source/Dafny/RefinementTransformer.cs97
-rw-r--r--Source/Dafny/Resolver.cs1
-rw-r--r--Source/Dafny/Translator.cs28
7 files changed, 148 insertions, 35 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index c954c019..b3fc7e24 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -317,7 +317,7 @@ axiom (forall<T> s, t: Seq T ::
function Seq#FromArray(h: HeapType, a: ref): Seq BoxType;
axiom (forall h: HeapType, a: ref ::
{ Seq#Length(Seq#FromArray(h,a)) }
- Seq#Length(Seq#FromArray(h, a)) == array.Length(a));
+ Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType }
(forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
@@ -325,11 +325,11 @@ axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );
axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::
{ Seq#FromArray(update(h, a, IndexField(i), v), a) }
- 0 <= i && i < array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );
+ 0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );
/**** Someday:
axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }
$IsGoodHeap(h) &&
- a != null && read(h, a, alloc) && dtype(a) == class.array && TypeParams(a, 0) == class.bool
+ a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.bool
==>
(forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }
0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));
@@ -351,7 +351,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
// Extension axiom, triggers only on Takes from arrays.
axiom (forall h: HeapType, a: ref, n0, n1: int ::
{ Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) }
- n0 + 1 == n1 && 0 <= n0 && n1 <= array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );
+ n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );
// drop commutes with build.
axiom (forall<T> s: Seq T, v: T, n: int ::
{ Seq#Drop(Seq#Build(s, v), n) }
@@ -382,12 +382,12 @@ axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box(
// ---------------------------------------------------------------
type ClassName;
-const unique class.int: ClassName;
-const unique class.bool: ClassName;
-const unique class.set: ClassName;
-const unique class.seq: ClassName;
-const unique class.multiset: ClassName;
-const unique class.array: ClassName;
+const unique class._System.int: ClassName;
+const unique class._System.bool: ClassName;
+const unique class._System.set: ClassName;
+const unique class._System.seq: ClassName;
+const unique class._System.multiset: ClassName;
+const unique class._System.array: ClassName;
function /*{:never_pattern true}*/ dtype(ref): ClassName;
function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
@@ -495,8 +495,8 @@ axiom (forall r: ref, h: HeapType ::
// -- Arrays -----------------------------------------------------
// ---------------------------------------------------------------
-function array.Length(a: ref): int;
-axiom (forall o: ref :: 0 <= array.Length(o));
+function _System.array.Length(a: ref): int;
+axiom (forall o: ref :: 0 <= _System.array.Length(o));
// ---------------------------------------------------------------
// -- The heap ---------------------------------------------------
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 7884b40c..357b2b60 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -570,7 +570,6 @@ namespace Microsoft.Dafny {
[Pure]
public override string ToString() {
Contract.Ensures(Contract.Result<string>() != null);
-
return Name;
}
}
@@ -668,6 +667,12 @@ namespace Microsoft.Dafny {
Module = module;
TypeArgs = typeArgs;
}
+
+ public string FullName {
+ get {
+ return Module.Name + "." + Name;
+ }
+ }
}
public class ClassDecl : TopLevelDecl {
@@ -776,7 +781,7 @@ namespace Microsoft.Dafny {
Contract.Requires(EnclosingDatatype != null);
Contract.Ensures(Contract.Result<string>() != null);
- return "#" + EnclosingDatatype.Name + "." + Name;
+ return "#" + EnclosingDatatype.FullName + "." + Name;
}
}
}
@@ -799,7 +804,7 @@ namespace Microsoft.Dafny {
Contract.Requires(EnclosingClass != null);
Contract.Ensures(Contract.Result<string>() != null);
- return EnclosingClass.Name + "." + Name;
+ return EnclosingClass.FullName + "." + Name;
}
}
}
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 1d075415..62facb31 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -66,6 +66,18 @@ namespace Microsoft.Dafny {
Dafny.Resolver r = new Dafny.Resolver(program);
r.ResolveProgram(program);
+ if (DafnyOptions.O.DafnyPrintResolvedFile != null) {
+ string filename = DafnyOptions.O.DafnyPrintResolvedFile;
+ if (filename == "-") {
+ Printer pr = new Printer(System.Console.Out);
+ pr.PrintProgram(program);
+ } else {
+ using (TextWriter writer = new System.IO.StreamWriter(filename)) {
+ Printer pr = new Printer(writer);
+ pr.PrintProgram(program);
+ }
+ }
+ }
if (r.ErrorCount != 0) {
return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, programName);
}
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index eb01ac12..34fa0487 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -29,6 +29,7 @@ namespace Microsoft.Dafny
public int InductionHeuristic = 6;
public string DafnyPrelude = null;
public string DafnyPrintFile = null;
+ public string DafnyPrintResolvedFile = null;
public bool Compile = true;
public bool ForceCompile = false;
public bool SpillTargetCode = false;
@@ -49,6 +50,12 @@ namespace Microsoft.Dafny
}
return true;
+ case "rprint":
+ if (ps.ConfirmArgumentCount(1)) {
+ DafnyPrintResolvedFile = args[ps.i];
+ }
+ return true;
+
case "compile": {
int compile = 0;
if (ps.GetNumericArgument(ref compile, 3)) {
@@ -113,6 +120,9 @@ namespace Microsoft.Dafny
/dprint:<file>
print Dafny program after parsing it
(use - as <file> to print to console)
+ /rprint:<file>
+ print Dafny program after resolving it
+ (use - as <file> to print to console)
/compile:<n> 0 - do not compile Dafny program
1 (default) - upon successful verification of the Dafny
program, compile Dafny program to C# program out.cs
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 0f3d473a..a13a4dae 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -13,6 +13,7 @@ using System;
using System.Collections.Generic;
using System.Numerics;
using System.Diagnostics.Contracts;
+using IToken = Microsoft.Boogie.IToken;
namespace Microsoft.Dafny {
public class RefinementTransformer
@@ -57,7 +58,7 @@ namespace Microsoft.Dafny {
foreach (var d in prev.TopLevelDecls) {
int index;
if (!declaredNames.TryGetValue(d.Name, out index)) {
- m.TopLevelDecls.Add(CreateRefinementCopy(d, m));
+ m.TopLevelDecls.Add(CloneDeclaration(d, m));
} else {
var nw = m.TopLevelDecls[index];
if (d is ArbitraryTypeDecl) {
@@ -82,20 +83,32 @@ namespace Microsoft.Dafny {
}
}
- TopLevelDecl CreateRefinementCopy(TopLevelDecl d, ModuleDecl m) {
+ IToken Tok(IToken tok) {
+ // TODO: do something that makes it clear that this token is from a copy
+ return tok;
+ }
+
+ // -------------------------------------------------- Cloning ---------------------------------------------------------------
+
+ TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDecl m) {
Contract.Requires(d != null);
Contract.Requires(m != null);
+ // top-level declarations clone their tokens
if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(dd.tok, dd.Name, m, null);
+ return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
} else if (d is DatatypeDecl) {
var dd = (DatatypeDecl)d;
- var dt = new DatatypeDecl(dd.tok, dd.Name, m, dd.TypeArgs/*TODO*/, dd.Ctors/*TODO*/, null);
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var ctors = dd.Ctors.ConvertAll(CloneCtor);
+ var dt = new DatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
return dt;
} else if (d is ClassDecl) {
var dd = (ClassDecl)d;
- var cl = new ClassDecl(dd.tok, dd.Name, m, dd.TypeArgs/*TODO*/, dd.Members/*TODO*/, null);
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
+ var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);
return cl;
} else {
Contract.Assert(false); // unexpected declaration
@@ -103,6 +116,80 @@ namespace Microsoft.Dafny {
}
}
+ DatatypeCtor CloneCtor(DatatypeCtor ct) {
+ // datatype constructors clone their tokens
+ return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
+ }
+
+ TypeParameter CloneTypeParam(TypeParameter tp) {
+ return new TypeParameter(tp.tok, tp.Name);
+ }
+
+ MemberDecl CloneMember(MemberDecl member) {
+ // members clone their tokens
+ if (member is Field) {
+ var f = (Field)member;
+ return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
+ } else if (member is Function) {
+ var f = (Function)member;
+ var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
+ return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.Formals.ConvertAll(CloneFormal), CloneType(f.ResultType),
+ f.Req.ConvertAll(CloneExpr), f.Reads.ConvertAll(CloneFrameExpr), f.Ens.ConvertAll(CloneExpr), CloneSpecExpr(f.Decreases), CloneExpr(f.Body), null);
+ } else {
+ var m = (Method)member;
+ var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
+ return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, m.Ins.ConvertAll(CloneFormal), m.Outs.ConvertAll(CloneFormal),
+ m.Req.ConvertAll(CloneMayBeFreeExpr), CloneSpecFrameExpr(m.Mod), m.Ens.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(m.Decreases), CloneBlockStmt(m.Body), null);
+ }
+ }
+
+ Type CloneType(Type t) {
+ // TODO
+ return t;
+ }
+
+ Formal CloneFormal(Formal formal) {
+ // TODO
+ return formal;
+ }
+
+ Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
+ // TODO
+ return spec;
+ }
+
+ Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
+ // TODO
+ return frame;
+ }
+
+ FrameExpression CloneFrameExpr(FrameExpression frame) {
+ // TODO
+ return frame;
+ }
+
+ MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
+ // TODO
+ return expr;
+ }
+
+ Expression CloneExpr(Expression expr) {
+ // TODO
+ return expr;
+ }
+
+ BlockStmt CloneBlockStmt(BlockStmt stmt) {
+ // TODO
+ return stmt;
+ }
+
+ Statement CloneStmt(Statement stmt) {
+ // TODO
+ return stmt;
+ }
+
+ // -------------------------------------------------- Merging ---------------------------------------------------------------
+
DatatypeDecl MergeDatatype(DatatypeDecl nw, DatatypeDecl prev) {
// TODO
return nw;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 93c11ceb..c9b877c9 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -103,7 +103,6 @@ namespace Microsoft.Dafny {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(builtIns != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(classes));
Contract.Invariant(cce.NonNullElements(importGraph));
Contract.Invariant(cce.NonNullDictionaryAndValues(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullDictionaryAndValues(v)));
Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index da0607e0..4f597519 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -208,7 +208,7 @@ namespace Microsoft.Dafny {
Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
allocField = c;
- } else if (c.Name == "class.array") {
+ } else if (c.Name == "class._System.array") {
classDotArray = c;
}
} else if (d is Bpl.GlobalVariable) {
@@ -218,7 +218,7 @@ namespace Microsoft.Dafny {
}
} else if (d is Bpl.Function) {
var f = (Bpl.Function)d;
- if (f.Name == "array.Length")
+ if (f.Name == "_System.array.Length")
arrayLength = f;
}
}
@@ -229,7 +229,7 @@ namespace Microsoft.Dafny {
} else if (multiSetTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet");
} else if (arrayLength == null) {
- Console.WriteLine("Error: Dafny prelude is missing declaration of function array.Length");
+ Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length");
} else if (fieldNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
@@ -249,7 +249,7 @@ namespace Microsoft.Dafny {
} else if (allocField == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
} else if (classDotArray == null) {
- Console.WriteLine("Error: Dafny prelude is missing declaration of class.array");
+ Console.WriteLine("Error: Dafny prelude is missing declaration of class._System.array");
} else {
return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
@@ -505,7 +505,7 @@ namespace Microsoft.Dafny {
cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj);
}
var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.Name, new Bpl.VariableSeq(cases_dBv), cases_resType);
+ var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullName, new Bpl.VariableSeq(cases_dBv), cases_resType);
cases_fn.Body = cases_body;
sink.TopLevelDeclarations.Add(cases_fn);
}
@@ -1073,7 +1073,7 @@ namespace Microsoft.Dafny {
foreach (var inFormal in m.Ins) {
var dt = inFormal.Type.AsDatatype;
if (dt != null) {
- var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.Name, Bpl.Type.Bool));
+ var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullName, Bpl.Type.Bool));
var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));
builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));
}
@@ -2646,7 +2646,7 @@ namespace Microsoft.Dafny {
if (classes.TryGetValue(cl, out cc)) {
Contract.Assert(cc != null);
} else {
- cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.Name, predef.ClassNameType), true);
+ cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullName, predef.ClassNameType), true);
classes.Add(cl, cc);
}
return cc;
@@ -2671,18 +2671,18 @@ namespace Microsoft.Dafny {
}
if (type is BoolType) {
- return new Bpl.IdentifierExpr(tok, "class.bool", predef.ClassNameType);
+ return new Bpl.IdentifierExpr(tok, "class._System.bool", predef.ClassNameType);
} else if (type is IntType) {
- return new Bpl.IdentifierExpr(tok, "class.int", predef.ClassNameType);
+ return new Bpl.IdentifierExpr(tok, "class._System.int", predef.ClassNameType);
} else if (type is ObjectType) {
- return new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType);
+ return new Bpl.IdentifierExpr(tok, "class._System.object", predef.ClassNameType);
} else if (type is CollectionType) {
CollectionType ct = (CollectionType)type;
Bpl.Expr a = GetTypeExpr(tok, ct.Arg);
if (a == null) {
return null;
}
- Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : (ct is SeqType ? "class.seq" : "class.multiset"), predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class._System.set" : (ct is SeqType ? "class._System.seq" : "class._System.multiset"), predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
} else {
UserDefinedType ct = (UserDefinedType)type;
@@ -4785,9 +4785,9 @@ namespace Microsoft.Dafny {
// array allocation
List<Type> typeArgs = new List<Type>();
typeArgs.Add(tRhs.EType);
- rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class." + BuiltIns.ArrayClassName(tRhs.ArrayDimensions.Count), predef.ClassNameType), typeArgs, true);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class._System." + BuiltIns.ArrayClassName(tRhs.ArrayDimensions.Count), predef.ClassNameType), typeArgs, true);
} else if (tRhs.EType is ObjectType) {
- rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType), new List<Type>(), true);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class._System.object", predef.ClassNameType), new List<Type>(), true);
} else {
rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);
}
@@ -6204,7 +6204,7 @@ namespace Microsoft.Dafny {
Contract.Requires(1 <= totalDims);
Contract.Requires(0 <= dim && dim < totalDims);
- string name = BuiltIns.ArrayClassName(totalDims) + ".Length";
+ string name = "_System." + BuiltIns.ArrayClassName(totalDims) + ".Length";
if (totalDims != 1) {
name += dim;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 04:22:47 +0000