From 36a4f8a3f8be8e769f198c401f1b7b92ae7d67f6 Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 9 Sep 2014 19:14:19 -0700 Subject: Print system module (in a comment) with /rprint. Cleaner printing of .reads and .requires members of the built-in arrow "classes". --- Source/Dafny/DafnyAst.cs | 31 +++++++++++++------------------ Source/Dafny/Printer.cs | 47 ++++++++++++++++++++++++++++++----------------- 2 files changed, 43 insertions(+), 35 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 598b53da..9a519ec1 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -156,12 +156,12 @@ namespace Microsoft.Dafny { if (!arrowTypeDecls.ContainsKey(arity)) { IToken tok = Token.NoToken; var tps = Util.Map(Enumerable.Range(0, arity + 1), - x => new TypeParameter(tok, "_Fn" + x)); + x => new TypeParameter(tok, "T" + x)); var tys = tps.ConvertAll(tp => (Type)(new UserDefinedType(tp))); - var args = tys.GetRange(0, arity).ConvertAll(t => new Formal(tok, "x", t, true, false)); + var args = Util.Map(Enumerable.Range(0, arity), i => new Formal(tok, "x" + i, tys[i], true, false)); var argExprs = args.ConvertAll(a => (Expression)new IdentifierExpr(tok, a.Name) { Var = a, Type = a.Type }); - var readsIS = new IdentifierSequence(new List { tok }, tok, argExprs) { + var readsIS = new FunctionCallExpr(tok, "reads", new ImplicitThisExpr(tok), tok, argExprs) { Type = new SetType(new ObjectType()), }; var readsFrame = new List { new FrameExpression(tok, readsIS, null) }; @@ -169,20 +169,15 @@ namespace Microsoft.Dafny { new List(), args, Type.Bool, new List(), readsFrame, new List(), new Specification(new List(), null), - null, new Attributes("axiom", new List(), null), null); + null, null, null); var reads = new Function(tok, "reads", false, true, new List(), args, new SetType(new ObjectType()), new List(), readsFrame, new List(), new Specification(new List(), null), - null, new Attributes("axiom", new List(), null), null); - var readsFexp = - new FunctionCallExpr(tok, "reads", new ThisExpr(tok), tok, argExprs) { - Function = reads, - Type = readsIS.Type, - TypeArgumentSubstitutions = Util.Dict(tps, tys) - }; - readsIS.ResolvedExpression = readsFexp; - var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule); + null, null, null); + readsIS.Function = reads; // just so we can really claim the member declarations are resolved + readsIS.TypeArgumentSubstitutions = Util.Dict(tps, tys); // ditto + var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule, DontCompile()); arrowTypeDecls.Add(arity, arrowDecl); SystemModule.TopLevelDecls.Add(arrowDecl); } @@ -693,12 +688,12 @@ namespace Microsoft.Dafny { } public static string ArrowTypeName(int arity) { - return "_Func" + arity; + return "_#Func" + arity; } [Pure] public static bool IsArrowTypeName(string s) { - return s.StartsWith("_Func"); + return s.StartsWith("_#Func"); } public override string TypeName(ModuleDefinition context) { @@ -1742,9 +1737,9 @@ namespace Microsoft.Dafny { public readonly Function Requires; public readonly Function Reads; - public ArrowTypeDecl(List tps, Function req, Function reads, ModuleDefinition module) - : base(Token.NoToken, "_Func" + (tps.Count - 1), module, tps, - new List { req, reads }, null, null) { + public ArrowTypeDecl(List tps, Function req, Function reads, ModuleDefinition module, Attributes attributes) + : base(Token.NoToken, "_#Func" + (tps.Count - 1), module, tps, + new List { req, reads }, attributes, null) { Contract.Requires(tps != null && 1 <= tps.Count); Contract.Requires(req != null); Contract.Requires(reads != null); diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 56722543..6ec05a50 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -124,6 +124,12 @@ namespace Microsoft.Dafny { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment); } wr.WriteLine("// {0}", prog.Name); + if (DafnyOptions.O.DafnyPrintResolvedFile != null) { + wr.WriteLine(); + wr.WriteLine("/*"); + PrintModuleDefinition(prog.BuiltIns.SystemModule, 0); + wr.WriteLine("*/"); + } wr.WriteLine(); PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0); } @@ -204,23 +210,7 @@ namespace Microsoft.Dafny { Indent(indent); if (d is LiteralModuleDecl) { ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef; - if (module.IsAbstract) { - wr.Write("abstract "); - } - wr.Write("module"); - PrintAttributes(module.Attributes); - wr.Write(" {0} ", module.Name); - if (module.RefinementBaseName != null) { - wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val)); - } - if (module.TopLevelDecls.Count == 0) { - wr.WriteLine("{ }"); - } else { - wr.WriteLine("{"); - PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount); - Indent(indent); - wr.WriteLine("}"); - } + PrintModuleDefinition(module, indent); } else if (d is AliasModuleDecl) { wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((AliasModuleDecl)d).Name); @@ -230,12 +220,35 @@ namespace Microsoft.Dafny { wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name); wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); } + } else { Contract.Assert(false); // unexpected TopLevelDecl } } } + void PrintModuleDefinition(ModuleDefinition module, int indent) { + Contract.Requires(module != null); + Contract.Requires(0 <= indent); + if (module.IsAbstract) { + wr.Write("abstract "); + } + wr.Write("module"); + PrintAttributes(module.Attributes); + wr.Write(" {0} ", module.Name); + if (module.RefinementBaseName != null) { + wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val)); + } + if (module.TopLevelDecls.Count == 0) { + wr.WriteLine("{ }"); + } else { + wr.WriteLine("{"); + PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount); + Indent(indent); + wr.WriteLine("}"); + } + } + void PrintIteratorSignature(IteratorDecl iter, int indent) { Indent(indent); PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs); -- cgit v1.2.3