Chalice: put classes and objects into package "chalice"

10 files changed, 14 insertions, 4 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index bad1292c..53c2093d 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 import scala.util.parsing.input.Position

 import scala.util.parsing.input.NoPosition

 import scala.util.parsing.input.Positional

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 63e4281c..2c872349 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 import scala.util.parsing.input.Position

 import scala.util.parsing.input.NoPosition

 

@@ -271,12 +272,13 @@ object Boogie {
      ")"

    case Ite(con, then, els) =>

      "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")"

+   case Trigger(ts) => Print(ts,", ", PrintExpr)

    case Forall(ts, xs, triggers, body) =>

      "(forall" +

      (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +

      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +

      " :: " +

-     Print(triggers , "", { t: Trigger => "{" + Print(t.ts,", ", PrintExpr) + "} " }) +

+     Print(triggers , "", { t: Trigger => "{" +  PrintExpr(t) + "} " }) +

      PrintExpr(body) +

      ")"

    case Exists(ts, xs, triggers, body) =>

@@ -284,7 +286,7 @@ object Boogie {
      (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +     

      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +

      " :: " +

-     Print(triggers , "", { t: Trigger => "{" + Print(t.ts,", ", PrintExpr) + "} " }) +

+     Print(triggers , "", { t: Trigger => "{" + PrintExpr(t) + "} " }) +

      PrintExpr(body) +

      ")"

    case Lambda(ts, xs, body) =>

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 0466ecc5..0342964b 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 import java.io.BufferedReader

 import java.io.InputStreamReader

 import java.io.File

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 63aecf14..67f6585b 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 class ChaliceToCSharp {

     

   def convertProgram(decls: List[TopLevelDecl]): String = {

diff --git a/Chalice/src/Graph.scala b/Chalice/src/Graph.scala
index 0e809c29..0d4bae4a 100644
--- a/Chalice/src/Graph.scala
+++ b/Chalice/src/Graph.scala
@@ -7,7 +7,7 @@
 /**

  * Graph algorithms

  */

-

+package chalice;

 import scala.collection.mutable;

 import scala.collection.immutable;

 

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index c427afe3..8999add9 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 import scala.util.parsing.combinator.syntactical.StandardTokenParsers

 import scala.util.parsing.input.PagedSeqReader

 import scala.collection.immutable.PagedSeq

diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index b4994889..f5f4861d 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -3,7 +3,8 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

-object TranslatorPrelude { 

+package chalice;

+object TranslatorPrelude {

 

   val P =

 """// Copyright (c) 2008, Microsoft

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 413a4b29..3e8798f4 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 object PrintProgram {

   def P(prog: List[TopLevelDecl]) =

     for (decl <- prog) decl match {

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index e69b1776..7365bfc8 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 import scala.util.parsing.input.Position

 import scala.util.parsing.input.Positional

 

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 2ef41de1..45d875f0 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -3,6 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

+package chalice;

 import scala.util.parsing.input.Position

 import scala.util.parsing.input.NoPosition