From fad74b96e5d9367960358b1c4cc9c2cce79e961a Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Wed, 8 Jul 2015 11:01:11 -0700 Subject: added unit tests for exclusive refinement. --- Test/irondafny0/xrefine1.dfy | 77 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 Test/irondafny0/xrefine1.dfy (limited to 'Test/irondafny0/xrefine1.dfy') diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy new file mode 100644 index 00000000..10d25f53 --- /dev/null +++ b/Test/irondafny0/xrefine1.dfy @@ -0,0 +1,77 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +abstract module ProtocolSpec { + type ProtoT + + predicate Init(p:ProtoT) +} + +abstract module HostSpec { + type HostT + import P as ProtocolSpec + + function method foo(h:HostT) : P.ProtoT +} + +module ProtocolImpl exclusively refines ProtocolSpec { + type ProtoT = bool + + predicate Init(p:ProtoT) { !p } + + method orange(i:nat) returns (j:nat) + { + j := i + 1; + } +} + +module HostImpl exclusively refines HostSpec { + import P = ProtocolImpl + + type HostT = int + + function method foo(h:HostT) : P.ProtoT + { + h > 0 + } + + method apple(i:nat) returns (j:nat) + { + j := i + 1; + } +} + +abstract module MainSpec { + import HI as HostSpec + import PI as ProtocolSpec + + method Test(h1:HI.HostT, h2:HI.HostT) + requires HI.foo(h1) == HI.foo(h2); + requires PI.Init(HI.foo(h1)) +} + +module MainImpl exclusively refines MainSpec { + import HI = HostImpl + import PI = ProtocolImpl + + method Test(h1:HI.HostT, h2:HI.HostT) + { + var a := HI.foo(h1); + print "HI.foo(h1) => ", a, "\n"; + var b := HI.foo(h2); + print "HI.foo(h2) => ", b, "\n"; + var i := PI.orange(1); + print "PI.orange(1) => ", i, "\n"; + var j := HI.apple(2); + print "PI.apple(2) => ", j, "\n"; + } + + method Main() + { + Test(-1, 1); + } +} + + + + -- cgit v1.2.3 From fe501d243c0413db8ae85bda174d0761da00d330 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Mon, 13 Jul 2015 10:40:35 -0700 Subject: [IronDafny] implemented workaround for "import opened" bug(s). --- Source/Dafny/Cloner.cs | 8 ++-- Source/Dafny/Dafny.atg | 16 ++++---- Source/Dafny/DafnyAst.cs | 52 +++++++++++++++++++----- Source/Dafny/DafnyOptions.cs | 27 +++++++++++- Source/Dafny/Parser.cs | 16 ++++---- Source/Dafny/Resolver.cs | 61 ++++++++++++++++++++-------- Test/irondafny0/FIFO.dfy | 2 +- Test/irondafny0/LIFO.dfy | 2 +- Test/irondafny0/opened_workaround.dfy | 21 ++++++++++ Test/irondafny0/opened_workaround.dfy.expect | 3 ++ Test/irondafny0/xrefine0.dfy | 2 +- Test/irondafny0/xrefine1.dfy | 2 +- Test/irondafny0/xrefine2.dfy | 2 +- Test/irondafny0/xrefine3.dfy | 2 +- 14 files changed, 161 insertions(+), 55 deletions(-) create mode 100644 Test/irondafny0/opened_workaround.dfy create mode 100644 Test/irondafny0/opened_workaround.dfy.expect (limited to 'Test/irondafny0/xrefine1.dfy') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 6e64c7ec..fe9795d3 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -44,9 +44,9 @@ namespace Microsoft.Dafny } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes)); + return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes), dd); } else { - return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes)); + return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes), dd); } } else if (d is TupleTypeDecl) { var dd = (TupleTypeDecl)d; @@ -55,7 +55,7 @@ namespace Microsoft.Dafny var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes)); + var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes), dd); return dt; } else if (d is CoDatatypeDecl) { var dd = (CoDatatypeDecl)d; @@ -108,7 +108,7 @@ namespace Microsoft.Dafny if (d is DefaultClassDecl) { return new DefaultClassDecl(m, mm); } else { - return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType)); + return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd); } } else if (d is ModuleDecl) { if (d is LiteralModuleDecl) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 7b51fb5e..6e939968 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -515,7 +515,7 @@ Dafny | OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .) | IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) | TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .) - | ClassMemberDecl + | ClassMemberDecl } (. // find the default class in the default module, then append membersDefaultClass to its member list DefaultClassDecl defaultClass = null; @@ -561,7 +561,7 @@ SubModuleDecl | NewtypeDecl (. module.TopLevelDecls.Add(td); .) | OtherTypeDecl (. module.TopLevelDecls.Add(td); .) | IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | ClassMemberDecl + | ClassMemberDecl } "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); @@ -618,7 +618,7 @@ ClassDecl {"," Type (. traits.Add(trait); .) } ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -642,7 +642,7 @@ ClassDecl NoUSIdent [ GenericParameters ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -651,7 +651,7 @@ ClassDecl .) . -ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl.> +ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl.> = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -685,7 +685,7 @@ ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDe mmod.IsProtected = false; } .) - MethodDecl (. mm.Add(m); .) + MethodDecl (. mm.Add(m); .) ) . DatatypeDecl @@ -937,7 +937,7 @@ GenericParameters<.List/*!*/ typeArgs.> ">" . /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1018,7 +1018,7 @@ MethodDecl [ BlockStmt ] (. - if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { + if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d14d82a3..c90755a3 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1777,6 +1777,14 @@ namespace Microsoft.Dafny { this.refinementBase = null; Includes = new List(); IsBuiltinName = isBuiltinName; + + if (isExclusiveRefinement && !DafnyOptions.O.IronDafny) { + parser.errors.SynErr( + tok.filename, + tok.line, + tok.col, + "The exclusively keyword is experimental and only available when IronDafny features are enabled (/ironDafny)."); + } } public virtual bool IsDefaultModule { get { @@ -1990,8 +1998,8 @@ namespace Microsoft.Dafny { } public ClassDecl(IToken tok, string name, ModuleDefinition module, - List typeArgs, [Captured] List members, Attributes attributes, List traits) - : base(tok, name, module, typeArgs, attributes) { + List typeArgs, [Captured] List members, Attributes attributes, List traits, ClassDecl clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2005,6 +2013,12 @@ namespace Microsoft.Dafny { return false; } } + + public new ClassDecl ClonedFrom { + get { + return (ClassDecl)base.ClonedFrom; + } + } } public class DefaultClassDecl : ClassDecl { @@ -2067,8 +2081,8 @@ namespace Microsoft.Dafny { } public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, - [Captured] List ctors, Attributes attributes) - : base(tok, name, module, typeArgs, attributes) { + [Captured] List ctors, Attributes attributes, DatatypeDecl clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2082,6 +2096,12 @@ namespace Microsoft.Dafny { return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0)); } } + + public new DatatypeDecl ClonedFrom { + get { + return (DatatypeDecl)base.ClonedFrom; + } + } } public class IndDatatypeDecl : DatatypeDecl @@ -2094,8 +2114,8 @@ namespace Microsoft.Dafny { public ES EqualitySupport = ES.NotYetComputed; public IndDatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, - [Captured] List ctors, Attributes attributes) - : base(tok, name, module, typeArgs, ctors, attributes) { + [Captured] List ctors, Attributes attributes, IndDatatypeDecl clonedFrom = null) + : base(tok, name, module, typeArgs, ctors, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2103,6 +2123,12 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(ctors)); Contract.Requires(1 <= ctors.Count); } + + public new IndDatatypeDecl ClonedFrom { + get { + return (IndDatatypeDecl)base.ClonedFrom; + } + } } public class TupleTypeDecl : IndDatatypeDecl @@ -2578,16 +2604,16 @@ namespace Microsoft.Dafny { 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) { + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes, NewtypeDecl clonedFrom = null) + : base(tok, name, module, new List(), attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(baseType != null); BaseType = baseType; } - public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes) - : base(tok, name, module, new List(), attributes) { + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes, NewtypeDecl clonedFrom = null) + : base(tok, name, module, new List(), attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2618,6 +2644,12 @@ namespace Microsoft.Dafny { get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases } + + public new NewtypeDecl ClonedFrom { + get { + return (NewtypeDecl)base.ClonedFrom; + } + } } public class TypeSynonymDecl : TopLevelDecl, RedirectingTypeDecl diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index a3b26f2a..978525f3 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -15,7 +15,11 @@ namespace Microsoft.Dafny public override string VersionNumber { get { - return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion; + return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion +#if ENABLE_IRONDAFNY + + "[IronDafny]" +#endif + ; } } public override string VersionSuffix { @@ -59,6 +63,13 @@ namespace Microsoft.Dafny public bool PrintStats = false; public bool PrintFunctionCallGraph = false; public bool WarnShadowing = false; + public bool IronDafny = +#if ENABLE_IRONDAFNY + true +#else + false +#endif + ; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -201,6 +212,16 @@ namespace Microsoft.Dafny return true; } + case "noIronDafny": { + IronDafny = false; + return true; + } + + case "ironDafny": { + IronDafny = true; + return true; + } + default: break; } @@ -301,6 +322,10 @@ namespace Microsoft.Dafny /funcCallGraph Print out the function call graph. Format is: func,mod=callee* /warnShadowing Emits a warning if the name of a declared variable caused another variable to be shadowed + /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of + these features may cause your code to become incompatible with future + releases of Dafny. + /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default. "); base.Usage(); // also print the Boogie options } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a90e650a..0c88cc22 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -576,7 +576,7 @@ bool IsType(ref IToken pt) { break; } case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { - ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals); + ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false); break; } } @@ -672,7 +672,7 @@ bool IsType(ref IToken pt) { break; } case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { - ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals); + ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, true); break; } } @@ -750,7 +750,7 @@ bool IsType(ref IToken pt) { Expect(45); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, true, false); + ClassMemberDecl(members, true, false, false); } Expect(46); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -961,7 +961,7 @@ bool IsType(ref IToken pt) { Expect(45); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, true, false); + ClassMemberDecl(members, true, false, false); } Expect(46); trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -970,7 +970,7 @@ bool IsType(ref IToken pt) { } - void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl) { + void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -1015,7 +1015,7 @@ bool IsType(ref IToken pt) { mmod.IsProtected = false; } - MethodDecl(mmod, allowConstructors, out m); + MethodDecl(mmod, allowConstructors, permitAbstractDecl, out m); mm.Add(m); } else SynErr(151); } @@ -1273,7 +1273,7 @@ bool IsType(ref IToken pt) { } - void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) { + void MethodDecl(MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl, out Method/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1393,7 +1393,7 @@ bool IsType(ref IToken pt) { if (la.kind == 45) { BlockStmt(out body, out bodyStart, out bodyEnd); } - if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { + if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 3e308e76..460859db 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -919,20 +919,27 @@ namespace Microsoft.Dafny sig.IsGhost = moduleDef.IsAbstract; List declarations = moduleDef.TopLevelDecls; - if (useImports) { - // First go through and add anything from the opened imports - foreach (var im in declarations) { - if (im is ModuleDecl && ((ModuleDecl)im).Opened) { - var s = GetSignature(((ModuleDecl)im).Signature); + // First go through and add anything from the opened imports + foreach (var im in declarations) { + if (im is ModuleDecl && ((ModuleDecl)im).Opened) { + var s = GetSignature(((ModuleDecl)im).Signature); + + if (useImports || DafnyOptions.O.IronDafny) { // classes: foreach (var kv in s.TopLevels) { - TopLevelDecl d; - if (sig.TopLevels.TryGetValue(kv.Key, out d)) { - sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); - } else { - sig.TopLevels.Add(kv.Key, kv.Value); + // IronDafny: we need to pull the members of the opened module's _default class in so that they can be merged. + if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) { + TopLevelDecl d; + if (sig.TopLevels.TryGetValue(kv.Key, out d)) { + sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); + } else { + sig.TopLevels.Add(kv.Key, kv.Value); + } } } + } + + if (useImports) { // constructors: foreach (var kv in s.Ctors) { Tuple pair; @@ -948,6 +955,9 @@ namespace Microsoft.Dafny sig.Ctors.Add(kv.Key, kv.Value); } } + } + + if (useImports || DafnyOptions.O.IronDafny) { // static members: foreach (var kv in s.StaticMembers) { MemberDecl md; @@ -957,7 +967,7 @@ namespace Microsoft.Dafny // add new sig.StaticMembers.Add(kv.Key, kv.Value); } - } + } } } } @@ -4406,8 +4416,23 @@ namespace Microsoft.Dafny return false; } var aa = (UserDefinedType)a; + var rca = aa.ResolvedClass; var bb = (UserDefinedType)b; - if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) { + var rcb = bb.ResolvedClass; + if (DafnyOptions.O.IronDafny) + { + while (rca != null && rca.Module.IsAbstract && rca.ClonedFrom != null) + { + // todo: should ClonedFrom be a TopLevelDecl? + // todo: should ClonedFrom be moved to TopLevelDecl? + rca = (TopLevelDecl)rca.ClonedFrom; + } + while (rcb != null && rcb.Module.IsAbstract && rcb.ClonedFrom != null) + { + rcb = (TopLevelDecl)rcb.ClonedFrom; + } + } + if (rca != null && rca == rcb) { // these are both resolved class/datatype types Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count); bool successSoFar = true; @@ -4416,12 +4441,12 @@ namespace Microsoft.Dafny } return successSoFar; } - else if ((bb.ResolvedClass is TraitDecl) && (aa.ResolvedClass is TraitDecl)) { - return ((TraitDecl)bb.ResolvedClass).FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName; - } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) { - return ((ClassDecl)bb.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName); - } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) { - return ((ClassDecl)aa.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName); + else if ((rcb is TraitDecl) && (rca is TraitDecl)) { + return ((TraitDecl)rcb).FullCompileName == ((TraitDecl)rca).FullCompileName; + } else if ((rcb is ClassDecl) && (rca is TraitDecl)) { + return ((ClassDecl)rcb).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rca).FullCompileName); + } else if ((rca is ClassDecl) && (rcb is TraitDecl)) { + return ((ClassDecl)rca).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rcb).FullCompileName); } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) { // type parameters if (aa.TypeArgs.Count != bb.TypeArgs.Count) { diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy index 1256b55d..ded8f567 100644 --- a/Test/irondafny0/FIFO.dfy +++ b/Test/irondafny0/FIFO.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "Queue.dfyi" diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy index bac08fba..8c0a08e8 100644 --- a/Test/irondafny0/LIFO.dfy +++ b/Test/irondafny0/LIFO.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "Queue.dfyi" diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy new file mode 100644 index 00000000..7464c346 --- /dev/null +++ b/Test/irondafny0/opened_workaround.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module A { + + predicate P() + + class C + { + static method{:axiom} M() + ensures P(); + } +} + +abstract module B { + import opened A +} + +abstract module C { + import Bee as B // Works +} diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect new file mode 100644 index 00000000..0be94b4c --- /dev/null +++ b/Test/irondafny0/opened_workaround.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Compilation error: Function _0_A_Compile._default.P has no body diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy index 35993ce8..b849111c 100644 --- a/Test/irondafny0/xrefine0.dfy +++ b/Test/irondafny0/xrefine0.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module Delicious {} diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy index 10d25f53..4b085e6b 100644 --- a/Test/irondafny0/xrefine1.dfy +++ b/Test/irondafny0/xrefine1.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module ProtocolSpec { diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy index 7578b424..1de4e201 100644 --- a/Test/irondafny0/xrefine2.dfy +++ b/Test/irondafny0/xrefine2.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module ProtocolSpec { diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy index 69c5bc27..44add7cc 100644 --- a/Test/irondafny0/xrefine3.dfy +++ b/Test/irondafny0/xrefine3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module AlphaSpec { -- cgit v1.2.3 From 2be514ca20e1478b6df02ef2b4c2725c319ac934 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Tue, 2 Feb 2016 12:40:07 -0800 Subject: Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B" --- Source/Dafny/Dafny.atg | 2 +- Source/Dafny/Parser.cs | 2 +- Test/dafny0/Compilation.dfy | 8 ++++---- Test/dafny0/Modules1.dfy | 2 +- Test/dafny0/Modules2.dfy | 2 +- Test/dafny0/OpaqueFunctions.dfy | 4 ++-- Test/dafny3/CachedContainer.dfy.expect | 1 + Test/dafny3/GenericSort.dfy | 2 +- Test/dafny4/Bug110.dfy | 2 +- Test/dafny4/Bug117.dfy | 4 ++-- Test/irondafny0/Queue.dfyi | 2 +- Test/irondafny0/opened_workaround.dfy | 2 +- Test/irondafny0/xrefine1.dfy | 6 +++--- Test/irondafny0/xrefine2.dfy | 6 +++--- Test/irondafny0/xrefine3.dfy | 6 +++--- 15 files changed, 26 insertions(+), 25 deletions(-) (limited to 'Test/irondafny0/xrefine1.dfy') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index e3696c5b..80792ce2 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -727,7 +727,7 @@ SubModuleDecl [IF(IsDefaultImport()) "default" QualifiedModuleName ] (. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); - //errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\""); + errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\""); .) | ":" QualifiedModuleName (. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .) diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index c7955dc8..8a1da161 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -835,7 +835,7 @@ bool IsDefaultImport() { QualifiedModuleName(out idAssignment); } submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); - //errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\""); + errors.Warning(t, "\"import A as B\" has been deprecated; in the new syntax, it is \"import A:B\""); } else if (la.kind == 21) { Get(); diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 965f0787..7a443e47 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -109,8 +109,8 @@ module T refines S { } } module A { - import X as S default T - import Y as S default T + import X : T + import Y : T import Z = T method run() { var x := new X.C; @@ -128,7 +128,7 @@ method NotMain() { abstract module S1 { - import B as S default T + import B : T method do() } @@ -138,7 +138,7 @@ module T1 refines S1 { } } module A1 { - import X as S1 default T1 + import X : T1 method run() { X.do(); var x := new X.B.C; diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index 3ffa5a23..3025cc00 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -130,6 +130,6 @@ abstract module Regression { abstract module B { - import X as A + import X : A } } diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy index a8dde8ce..beb80546 100644 --- a/Test/dafny0/Modules2.dfy +++ b/Test/dafny0/Modules2.dfy @@ -31,7 +31,7 @@ module Test { } module Test2 { - import opened B as A + import opened B : A method m() { var c := new C; // fine, as A was opened var c' := new B.C;// also fine, as A is bound diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index e1c0756c..b3cde309 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -44,7 +44,7 @@ module A' refines A { } module B { - import X as A + import X : A method Main() { var c := new X.C(); c.M(); // fine @@ -68,7 +68,7 @@ module B { } } module B_direct { - import X as A' + import X : A' method Main() { var c := new X.C(); c.M(); // fine diff --git a/Test/dafny3/CachedContainer.dfy.expect b/Test/dafny3/CachedContainer.dfy.expect index c6c90498..0185aacd 100644 --- a/Test/dafny3/CachedContainer.dfy.expect +++ b/Test/dafny3/CachedContainer.dfy.expect @@ -1,2 +1,3 @@ +CachedContainer.dfy(120,25): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B" Dafny program verifier finished with 47 verified, 0 errors diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index ea75c196..7555817c 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -17,7 +17,7 @@ abstract module TotalOrder { } abstract module Sort { - import O as TotalOrder // let O denote some module that has the members of TotalOrder + import O : TotalOrder // let O denote some module that has the members of TotalOrder predicate Sorted(a: array, low: int, high: int) requires a != null && 0 <= low <= high <= a.Length diff --git a/Test/dafny4/Bug110.dfy b/Test/dafny4/Bug110.dfy index 239f18d3..aa808669 100644 --- a/Test/dafny4/Bug110.dfy +++ b/Test/dafny4/Bug110.dfy @@ -27,5 +27,5 @@ abstract module Host { } abstract module Main { - import H as Host + import H : Host } diff --git a/Test/dafny4/Bug117.dfy b/Test/dafny4/Bug117.dfy index 2ae4bc70..418746cb 100644 --- a/Test/dafny4/Bug117.dfy +++ b/Test/dafny4/Bug117.dfy @@ -8,14 +8,14 @@ abstract module AbstractModule1 abstract module AbstractModule2 { - import opened AM1 as AbstractModule1 + import opened AM1 : AbstractModule1 datatype AbstractType2 = AbstractType2(x:AbstractType1) } abstract module AbstractModule3 { - import AM1 as AbstractModule1 + import AM1 : AbstractModule1 datatype AbstractType2 = AbstractType2(x:AM1.AbstractType1) } diff --git a/Test/irondafny0/Queue.dfyi b/Test/irondafny0/Queue.dfyi index 9f7eb534..06f4b29e 100644 --- a/Test/irondafny0/Queue.dfyi +++ b/Test/irondafny0/Queue.dfyi @@ -17,6 +17,6 @@ abstract module Queue { } abstract module MainSpec { - import Q as Queue + import Q : Queue } diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy index 7464c346..6d44ccfd 100644 --- a/Test/irondafny0/opened_workaround.dfy +++ b/Test/irondafny0/opened_workaround.dfy @@ -17,5 +17,5 @@ abstract module B { } abstract module C { - import Bee as B // Works + import Bee : B // Works } diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy index 4b085e6b..1b835649 100644 --- a/Test/irondafny0/xrefine1.dfy +++ b/Test/irondafny0/xrefine1.dfy @@ -9,7 +9,7 @@ abstract module ProtocolSpec { abstract module HostSpec { type HostT - import P as ProtocolSpec + import P : ProtocolSpec function method foo(h:HostT) : P.ProtoT } @@ -42,8 +42,8 @@ module HostImpl exclusively refines HostSpec { } abstract module MainSpec { - import HI as HostSpec - import PI as ProtocolSpec + import HI : HostSpec + import PI : ProtocolSpec method Test(h1:HI.HostT, h2:HI.HostT) requires HI.foo(h1) == HI.foo(h2); diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy index 1de4e201..9c33391b 100644 --- a/Test/irondafny0/xrefine2.dfy +++ b/Test/irondafny0/xrefine2.dfy @@ -9,7 +9,7 @@ abstract module ProtocolSpec { abstract module HostSpec { type HostT - import P as ProtocolSpec + import P : ProtocolSpec function method foo(h:HostT) : P.ProtoT } @@ -42,8 +42,8 @@ module HostImpl exclusively refines HostSpec { } abstract module MainSpec { - import HI as HostSpec - import PI as ProtocolSpec + import HI : HostSpec + import PI : ProtocolSpec method Test(h1:HI.HostT, h2:HI.HostT) requires HI.foo(h1) == HI.foo(h2); diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy index 44add7cc..86dbd957 100644 --- a/Test/irondafny0/xrefine3.dfy +++ b/Test/irondafny0/xrefine3.dfy @@ -12,7 +12,7 @@ abstract module AlphaSpec { abstract module BetaSpec { type Beta - import A as AlphaSpec + import A : AlphaSpec predicate IsValid(b:Beta) @@ -49,8 +49,8 @@ module BetaImpl exclusively refines BetaSpec { } abstract module MainSpec { - import A as AlphaSpec - import B as BetaSpec + import A : AlphaSpec + import B : BetaSpec method Main() { -- cgit v1.2.3