Merge branch 'develop'

.gitignore

@@ -11,3 +11,5 @@
 *.smt2
 /report/
 /build/
+/modules/wycs/src/wycs/core/Types.java
+/modules/wycs/src/wycs/solver/Solver.java

.travis.yml

@@ -7,4 +7,4 @@ jdk:
 
 #
 script:
-    ant build-all
+    ant build-all test-all

CONTRIBUTING.md

@@ -61,3 +61,5 @@ Signed-off-by: Daniel Gibbs <[email protected]>
 Signed-off-by: Min-Hsien Weng <[email protected]>
 Signed-off-by: Henry J. Wylde <[email protected]>
 Signed-off-by: Mark Utting <[email protected]>
+Signed-off-by: Drew Stratford <[email protected]>
+Signed-off-by: Rich Dougherty <[email protected]>

README

@@ -7,7 +7,19 @@
                             |___/             |___/
 
 ======================================================================
-Introduction
+Contents
+======================================================================
+
+1. Introduction
+
+2. Installation
+
+3. Building from Source
+
+4. Making a Contribution
+
+======================================================================
+1. Introduction
 ======================================================================
 
 Whiley is a programming language particularly suited to
@@ -25,36 +37,32 @@ for more on this.
 To find out more, visit http://whiley.org
 
 ======================================================================
-Installation
+2. Installation
 ======================================================================
 
 There are several ways to get started with Whiley:
 
-1) You can install the Eclipse Plugin.
+1) You can run it directly in your web browser.
 
 2) Or, you can download and run the executable Jar.
 
 3) Or, you can download and setup the Whiley Development Kit.
 
+4) You can install the Eclipse Plugin.
+
 The Eclipse plugin is the easiest way to get started with Whiley (see
 instructions below).  If you don't use Eclipse, another simple option
 is to download and run the executable Jar.  Finally, developers may
 like to download the Whiley Development Kit (WDK), which includes the
 source code for the compiler/runtime and various scripts to simplify
 compiling and running Whiley programs from the command-line.
 
-1. Whiley Eclipse Plugin (Wyclipse)
+2.1 Whiley Play
 ----------------------------------------------------------------------
-To install the Whiley Eclipse plugin start Eclipse and select "Install
-New Software" (normally found under "Help").  Then, add
-http://whiley.org/eclipse as a "software site", afterwhich you should
-find the "Whiley Eclipse Plugin" becomes an option to install.  At
-this point, "select all" and follow the instructions to install the
-plugin.
 
-For more info on Wyclipse, see http://whiley.org/tools/wyclipse/
+To run Whiley in your web-browser, goto http://whiley.org/play/
 
-2. Whiley Executable Jar
+2.2 Whiley Executable Jar
 ----------------------------------------------------------------------
 If you're running on a Windows system without cygwin, or you're having
 trouble getting the wyjc scripts to work, then a useful alternative is
@@ -74,7 +82,7 @@ Hello World
 
 (note: under Mac OS and UNIX you will want to replace the ';' with a ':')
 
-3. Whiley Development Kit (WDK)
+2.3 Whiley Development Kit (WDK)
 ----------------------------------------------------------------------
 To install the Whiley Development Kit, first download it from
 http://whiley.org/downloads.  Then, unpack the tarball into an
@@ -114,8 +122,50 @@ Hello World
 
 (note: under Mac OS and UNIX you will want to replace the ';' with a ':')
 
+2.4 Whiley Eclipse Plugin (Wyclipse)
+----------------------------------------------------------------------
+
+*** NOTE: the Eclipse plugin is out-of-date and not recommended
+
+To install the Whiley Eclipse plugin start Eclipse and select "Install
+New Software" (normally found under "Help").  Then, add
+http://whiley.org/eclipse as a "software site", afterwhich you should
+find the "Whiley Eclipse Plugin" becomes an option to install.  At
+this point, "select all" and follow the instructions to install the
+plugin.
+
+For more info on Wyclipse, see http://whiley.org/tools/wyclipse/
+
+============================================================================
+3. Building from Source
+============================================================================
+
+You can build the Whiley compiler from scratch by cloning this
+repository.  Then build all the projects simply by running 'ant'
+at the top level (You need to have Apache Ant installed to do this).
+
+If you wish to use an IDE, here are a few notes about setting up
+under an IDE such as Eclipse or IntelliJ:
+
+* The repository should not be setup as a single project!  Rather,
+  each module in the modules/ directory is intended to be its own
+  project.
+
+* Appropriate .classpath and .project files for each module are
+  included for use with Eclipse.  This should make it easy to setup
+  under Eclipse.
+
+* The .classpath Eclipse files refer to the libraries "WyRL" and
+  "Jasm".  Under Eclipse (Preferences/Java/Build Path/User Libraries),
+  you should set these up as "User-Defined Libraries" and point them
+  to the appropriate jar files in the lib/ directory (the "config.xml"
+  file will tell you which version of each .jar file you should use).
+  You should also create a user-defined library called "Ant" and add
+  to it at least the lib/ant.jar file in your Apache Ant installation.
+
+
 ============================================================================
-Making a Contribution
+4. Making a Contribution
 ============================================================================
 
 When making a contribution to the Whiley project, you will need to

build.xml

@@ -1,23 +1,33 @@
 <project name="whiley" default="build-all">
   <import file="config.xml"/>
 
+  <!-- ============================================== -->
+  <!-- Configuration -->
+  <!-- ============================================== -->
+
+  <!-- The set of build files in the order they should be built. -->
+  <filelist id="module.build.files" dir="modules">
+    <file name="wybs/build.xml"/>
+    <file name="wycs/build.xml"/>
+    <file name="wyil/build.xml"/>
+    <file name="wyc/build.xml"/>
+    <file name="wyrt/build.xml"/>
+    <file name="wyjc/build.xml"/>
+  </filelist>
+
+
   <!-- ============================================== -->
   <!-- Build Commands -->
   <!-- ============================================== -->
 
   <target name="build-all">
     <subant failonerror="true" target="build">
-      <fileset dir="modules" includes="wybs/build.xml"/>
-      <fileset dir="modules" includes="wycs/build.xml"/>
-      <fileset dir="modules" includes="wyil/build.xml"/>
-      <fileset dir="modules" includes="wyc/build.xml"/>
-      <fileset dir="modules" includes="wyrt/build.xml"/>
-      <fileset dir="modules" includes="wyjc/build.xml"/>
+      <filelist refid="module.build.files"/>
     </subant>
   </target>
 
   <!-- ============================================== -->
-  <!-- Documenation -->
+  <!-- Documentation -->
   <!-- ============================================== -->
 
   <target name="doc">
@@ -73,13 +83,7 @@
 
   <target name="distjars" depends="build-all">
     <subant failonerror="false" target="dist">
-      <fileset dir="modules" includes="wybs/build.xml"/>
-      <fileset dir="modules" includes="wycs/build.xml"/>
-      <fileset dir="modules" includes="wyil/build.xml"/>
-      <fileset dir="modules" includes="wyc/build.xml"/>
-      <fileset dir="modules" includes="wyrt/build.xml"/>
-      <fileset dir="modules" includes="wyjc/build.xml"/>
-
+      <filelist refid="module.build.files"/>
     </subant>
   </target>
 
@@ -110,6 +114,7 @@
       <include name="lib/*-v${version}.jar"/>
       <include name="lib/wyrl-v*.jar"/>
       <include name="lib/jasm-v*.jar"/>
+      <include name="lib/maven-ant-tasks*.jar"/>      
     </fileset>
   </copy>
   <tar destfile="dist/wdk-src-v${version}.tar" longfile="gnu">
@@ -133,9 +138,15 @@
   <!-- Misc Commands -->
   <!-- ============================================== -->
 
+  <target name="test-all" depends="build-all">
+    <subant failonerror="true" target="test">
+      <filelist refid="module.build.files"/>
+    </subant>
+  </target>
+
   <target name="clean">
     <subant failonerror="false" target="clean">
-      <fileset dir="modules" includes="*/build.xml"/>
+      <filelist refid="module.build.files"/>
     </subant>
     <delete includeEmptyDirs="true" failonerror="false">
       <fileset file="*~"/>

config.xml

@@ -1,5 +1,19 @@
-<project name="BuildConfig">
-  <property name="version" value="0.3.37"/>
+<project name="BuildConfig" xmlns:maven="urn:maven-ant">
+  <!-- Get the root directory of the project by looking at the directory enclosing this file. -->
+  <dirname property="rootdir" file="${ant.file.BuildConfig}"/>
+  <!-- Set the current Whiley version -->
+  <property name="version" value="0.3.38"/>
+  <!-- Load the Maven Ant tasks so that we can work with Maven repositories. -->
+  <typedef uri="urn:maven-ant"
+           classpath="${rootdir}/lib/maven-ant-tasks-2.1.3.jar"
+           resource="org/apache/maven/artifact/ant/antlib.xml"/>
+
+  <!-- Paths to common JARs -->
   <property name="JASM_JAR" value="lib/jasm-v0.1.7.jar"/>
-  <property name="WYRL_JAR" value="lib/wyrl-v0.4.3.jar"/>
+  <property name="WYRL_JAR" value="lib/wyrl-v0.4.4.jar"/>
+
+  <!-- Set the classpath for Junit and its dependencies -->
+  <maven:dependencies pathId="junit.classpath">
+    <dependency groupId="junit" artifactId="junit" version="4.12"/>
+  </maven:dependencies>
 </project>

examples/TicTacToe.whiley

@@ -15,13 +15,13 @@ type Square is (int x) where x == BLANK || x == CIRCLE || x == CROSS
 // ==================================================================
 // A board consists of 9 squares, and a move counter
 // ==================================================================
-type Board is {
+type Board is ({
     nat move,
     Square[] pieces // 3 x 3
-} where |pieces| == 9 && move <= 9 &&
-    countOf(pieces,BLANK) == (9 - move) &&
-    (countOf(pieces,CIRCLE) == countOf(pieces,CROSS) ||
-     countOf(pieces,CIRCLE) == countOf(pieces,CROSS)+1)
+} this)
+where |this.pieces| == 9 && this.move <= 9
+where countOf(this.pieces,BLANK) == (9 - this.move)
+where (countOf(this.pieces,CIRCLE) == countOf(this.pieces,CROSS) || countOf(this.pieces,CIRCLE) == countOf(this.pieces,CROSS)+1)
 
 // ==================================================================
 // An empty board is one where all pieces are blank

examples/TrafficLights.whiley

@@ -1,14 +1,13 @@
 import whiley.lang.*
 
 // the British interpretation of traffic lights!
-type TrafficLights is {
+type TrafficLights is ({
     bool red,
     bool amber,
     bool green
-} where (!red && !amber && green) ||
-        (!red && amber && !green) || // ignoring flashing
-        (red && !amber && !green) ||
-        (red && amber && !green)
+} this)
+// Red or Amber are on iff Green is off
+where (this.red || this.amber) <==> !this.green
 
 function TrafficLights() -> TrafficLights:
     return {

examples/matrix-multiply.whiley

@@ -23,11 +23,11 @@ import whiley.io.File
 
 type nat is (int x) where x >= 0
 
-type Matrix is {
+type Matrix is ({
     int width,
     int height,
     int[][] data
-} where |data| == height && no { i in 0..height | |data[i]| != width }
+} this) where |this.data| == this.height && no { i in 0..this.height | |this.data[i]| != this.width }
 
 function Matrix(nat width, nat height, int[][] data) -> (Matrix r)
 // Input array must match matrix height
@@ -74,27 +74,25 @@ ensures C.width == B.width && C.height == A.height:
 // Parser Code
 // ========================================================
 
-function parseFile(ASCII.string input) -> (Matrix,Matrix) | null:
+function parseFile(ASCII.string input) -> (Matrix|null a,Matrix|null b):
     Matrix|null A // 1st result
     Matrix|null B // 2nd result
-    int[]|null data, int pos = parseLine(2,0,input)
+    int[]|null data
+    int pos
+    data,pos = parseLine(2,0,input)
     // santity check    
     if data != null:
         int nrows = data[0]
         int ncols = data[1]
         pos = skipBreak(pos,input)
         A,pos = parseMatrix(nrows,ncols,pos,input)
-        // sanity check
-        if A != null:
-            pos = skipBreak(pos,input)
-            B,pos = parseMatrix(nrows,ncols,pos,input)
-            // sanity check
-            if B != null:
-                return A,B
+        pos = skipBreak(pos,input)
+        B,pos = parseMatrix(nrows,ncols,pos,input)
+        return A,B
     //
-    return null
+    return null,null
 
-function parseMatrix(nat height, nat width, int pos, ASCII.string input) -> (Matrix|null,int):
+function parseMatrix(nat height, nat width, int pos, ASCII.string input) -> (Matrix|null m, int npos):
     //
     int[][] rows = [[0;0];height]
     int[]|null row
@@ -110,7 +108,7 @@ function parseMatrix(nat height, nat width, int pos, ASCII.string input) -> (Mat
     //
     return Matrix(width,height,rows),pos
 
-function parseLine(int count, int pos, ASCII.string input) -> (int[]|null,int):
+function parseLine(int count, int pos, ASCII.string input) -> (int[]|null data,int npos):
     //
     pos = skipWhiteSpace(pos,input)
     int[] ints = [0;0]
@@ -129,7 +127,7 @@ function parseLine(int count, int pos, ASCII.string input) -> (int[]|null,int):
     else:
         return ints,pos
 
-function parseInt(int pos, ASCII.string input) -> (int|null,int):
+function parseInt(int pos, ASCII.string input) -> (int|null data,int npos):
     //
     int start = pos
     // check for negative input
@@ -183,13 +181,14 @@ method main(System.Console sys):
         // first, read data
         ASCII.string input = ASCII.fromBytes(file.readAll())
         // second, build the matrices
-        null|(Matrix, Matrix) AxB = parseFile(input)
+        null|Matrix A
+        null|Matrix B
+        //
+        A,B = parseFile(input)
         // third, sanity check we succeeded
-        if AxB is null:
+        if A is null || B is null:
             sys.out.println_s("error parsing input")
         else:
-            //
-            Matrix A, Matrix B = AxB
             // fourth, run the benchmark
             Matrix C = multiply(A,B)
             // finally, print the result!

modules/wybs/build.xml

@@ -25,6 +25,8 @@
     <echo message="============================================="/>
   </target>
 
+  <target name="test"/>
+
   <target name="dist">
     <mkdir dir="tmp"/>
     <manifest file="tmp/MANIFEST.MF">