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(-) 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