Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"

13 files changed, 24 insertions, 23 deletions

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<O.T>, 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()

     {