Merge branch 'develop'

build.xml

@@ -62,17 +62,10 @@
 	<include name="wyjvm/**"/>
 	<exclude name="wyjc/testing/**"/>
       </packageset>
-      <!--
-      <packageset dir="modules/wycc/src">
-	<include name="wycc/**"/>
-	<exclude name="wycc/testing/**"/>
-      </packageset>
-      -->
       <group title="Whiley Build System (WYBS)" packages="wybs:wyfs.*:wybs.*:wycc.*"/>
       <group title="Whiley Compiler (WYC)" packages="wyc:wyc.*"/>
       <group title="Whiley Intermediate Language (WYIL)" packages="wyil:wyil.*"/>
       <group title="Whiley-2-Java Compiler (WYJC)" packages="wyjc:wyjc.*:wyjvm.*"/>
-      <!--<group title="Whiley-2-C Compiler (WYCC)" packages="wycc:wycc.*"/>-->
       <group title="Whiley Constraint Solver (WYCS)" packages="wycs:wycs.*"/>
       </javadoc>
   </target>

config.xml

@@ -2,15 +2,25 @@
   <!-- 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.40"/>
+  <property name="version" value="0.4.0-SNAPSHOT"/>
   <!-- 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 DIRs -->
+  <property name="LIB_DIR" value="${rootdir}/lib/"/>
+  <property name="DIST_DIR" value="${rootdir}/dist/"/>
+
+  <property name="WYBS_DIR" value="${rootdir}/modules/wybs/"/>
+  <property name="WYC_DIR"  value="${rootdir}/modules/wyc/"/>
+  <property name="WYIL_DIR" value="${rootdir}/modules/wyil/"/>
+  <property name="WYCS_DIR" value="${rootdir}/modules/wycs/"/>
+  <property name="WYRT_DIR" value="${rootdir}/modules/wyrt/"/>
+
   <!-- Paths to common JARs -->
-  <property name="JASM_JAR" value="lib/jasm-v0.1.7.jar"/>
-  <property name="WYRL_JAR" value="lib/wyrl-v0.4.4.jar"/>
+  <property name="JASM_JAR" value="${LIB_DIR}/jasm-v0.1.7.jar"/>
+  <property name="WYRL_JAR" value="${LIB_DIR}/wyrl-v0.4.4.jar"/>
 
   <!-- Set the classpath for Junit and its dependencies -->
   <maven:dependencies pathId="junit.classpath">

examples/TicTacToe.whiley

@@ -18,10 +18,10 @@ type Square is (int x) where x == BLANK || x == CIRCLE || x == CROSS
 type Board is ({
     nat move,
     Square[] pieces // 3 x 3
-} 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)
+} b)
+where |b.pieces| == 9 && b.move <= 9
+where countOf(b.pieces,BLANK) == (9 - b.move)
+where (countOf(b.pieces,CIRCLE) == countOf(b.pieces,CROSS) || countOf(b.pieces,CIRCLE) == countOf(b.pieces,CROSS)+1)
 
 // ==================================================================
 // An empty board is one where all pieces are blank

examples/matrix-multiply.whiley

@@ -27,13 +27,13 @@ type Matrix is ({
     int width,
     int height,
     int[][] data
-} this) where |this.data| == this.height && no { i in 0..this.height | |this.data[i]| != this.width }
+} m) where |m.data| == m.height && all { i in 0..m.height | |m.data[i]| == m.width }
 
 function Matrix(nat width, nat height, int[][] data) -> (Matrix r)
 // Input array must match matrix height
 requires |data| == height
 // Elements of input array must match matrix width
-requires no { i in 0..height | |data[i]| != width }
+requires all { i in 0..height | |data[i]| == width }
 //
 ensures r.width == width && r.height == height && r.data == data:
     //

misc/emacs/whiley.el

@@ -34,7 +34,7 @@ For detail, see `comment-dwim'."
      (comment-dwim arg)))
 
 (defvar whiley-keywords
-  '("native" "export" "extern" "null" "return" "if" "is" "throw" "throws" "try" "catch" "switch" "case" "default" "break" "skip" "do" "while" "for" "else" "define" "assume" "assert" "assume" "package" "import" "function" "method" "type" "constant" "from" "debug" "where" "ensures" "requires" "public" "protected" "private" "this" "str" "new" "in" "no" "some" "all" "false" "true")
+  '("native" "export" "extern" "null" "return" "if" "is" "throw" "throws" "try" "catch" "switch" "case" "default" "break" "continue" "skip" "do" "while" "for" "else" "define" "assume" "assert" "assume" "package" "import" "function" "method" "type" "constant" "from" "debug" "where" "ensures" "requires" "public" "protected" "private" "this" "str" "new" "in" "no" "some" "all" "false" "true")
     "Whiley keywords.")
 
 (defvar whiley-types

misc/emacs/wyal.el

@@ -34,7 +34,7 @@ For detail, see `comment-dwim'."
      (comment-dwim arg)))
 
 (defvar wyal-keywords
-  '("import" "define" "function" "type" "assert" "assume" "ensures" "requires" "forall" "where" "some" "not" "if" "in" "is" "then" "false" "true")
+  '("import" "define" "function" "type" "assert" "assume" "ensures" "requires" "forall" "where" "some" "not" "if" "either" "or" "in" "is" "then" "false" "true")
     "Wyal keywords.")
 
 (defvar wyal-types

misc/emacs/wyrl.el

@@ -34,7 +34,7 @@ For detail, see `comment-dwim'."
      (comment-dwim arg)))
 
 (defvar wyrl-keywords
-  '("include" "term" "define" "reduce" "infer" "requires" "name" "rank" "function" "if" "in" "let" "as" "false" "true")
+  '("include" "term" "define" "reduce" "infer" "requires" "name" "rank" "function" "if" "in" "let" "as" "false" "true" "package")
     "Wyrl keywords.")
 
 (defvar wyrl-types

modules/wybs/build.xml

@@ -1,6 +1,14 @@
 <project name="wybs" default="build">
+
+  <!-- ================================================================== -->
+  <!-- Configuration -->
+  <!-- ================================================================== -->
   <import file="../../config.xml"/>
 
+  <!-- ================================================================== -->
+  <!-- Compile -->
+  <!-- ================================================================== -->
+
   <target name="compile-wybs">
     <javac memoryMaximumSize="2048m" fork="true" debug="true" debuglevel="vars,lines,source" source="1.7" target="1.7" includeantruntime="true">
       <src path="src"/>
@@ -9,14 +17,24 @@
     </javac>
   </target>
 
+  <!-- ================================================================== -->
+  <!-- Test -->
+  <!-- ================================================================== -->
+
+  <target name="test"/>
+
+  <!-- ================================================================== -->
+  <!-- Build -->
+  <!-- ================================================================== -->
+
   <target name="build" depends="compile-wybs">
     <mkdir dir="tmp"/>
     <manifest file="tmp/MANIFEST.MF">
       <attribute name="Built-By" value="${user.name}"/>
       <attribute name="Implementation-Version" value="${version}"/>
       <attribute name="Implementation-Title" value="wybs-v${version}.jar"/>
     </manifest>
-    <jar destfile="../../lib/wybs-v${version}.jar" manifest="tmp/MANIFEST.MF">
+    <jar destfile="${LIB_DIR}/wybs-v${version}.jar" manifest="tmp/MANIFEST.MF">
       <fileset dir="src" includes="*/**/*.class"/>
     </jar>
     <delete dir="tmp"/>
@@ -25,7 +43,9 @@
     <echo message="============================================="/>
   </target>
 
-  <target name="test"/>
+  <!-- ================================================================== -->
+  <!-- Dist -->
+  <!-- ================================================================== -->
 
   <target name="dist">
     <mkdir dir="tmp"/>
@@ -34,7 +54,7 @@
       <attribute name="Implementation-Version" value="${version}"/>
       <attribute name="Implementation-Title" value="wybs-v${version}.jar"/>
     </manifest>
-    <jar destfile="../../dist/wybs-all-v${version}.jar" manifest="tmp/MANIFEST.MF">
+    <jar destfile="${DIST_DIR}/wybs-all-v${version}.jar" manifest="tmp/MANIFEST.MF">
       <fileset dir="src">
 	<include name="wyfs/**/*.class"/>
 	<include name="wybs/**/*.class"/>
@@ -47,13 +67,17 @@
     <echo message="============================================="/>
   </target>
 
- <target name="clean">
-   <delete includeEmptyDirs="true" failonerror="false">
-     <fileset dir="." includes="**/*.class,**/*.wyil,**/*.wyasm"/>
-   </delete>
+  <!-- ================================================================== -->
+  <!-- Clean -->
+  <!-- ================================================================== -->
+
+  <target name="clean">
+    <delete includeEmptyDirs="true" failonerror="false">
+      <fileset dir="." includes="**/*.class,**/*.wyil,**/*.wyasm"/>
+    </delete>
     <echo message="============================================="/>
     <echo message="CLEANED: ${ant.project.name}"/>
     <echo message="============================================="/>
- </target>
+  </target>
 
 </project>

modules/wybs/src/wybs/lang/Build.java

@@ -61,8 +61,7 @@ public interface Project {
 		 * @throws IOException
 		 *             --- in case of some I/O failure.
 		 */
-		public boolean exists(Path.ID id, Content.Type<?> ct)
-				throws IOException;
+		public boolean exists(Path.ID id, Content.Type<?> ct) throws IOException;
 
 		/**
 		 * Get the entry corresponding to a given ID and content type. If no
@@ -73,8 +72,7 @@ public boolean exists(Path.ID id, Content.Type<?> ct)
 		 * @throws IOException
 		 *             --- in case of some I/O failure.
 		 */
-		public <T> Path.Entry<T> get(Path.ID id, Content.Type<T> ct)
-				throws IOException;
+		public <T> Path.Entry<T> get(Path.ID id, Content.Type<T> ct) throws IOException;
 
 		/**
 		 * Get all objects matching a given content filter stored in this root.
@@ -86,8 +84,7 @@ public <T> Path.Entry<T> get(Path.ID id, Content.Type<T> ct)
 		 * @param ct
 		 * @return
 		 */
-		public <T> List<Path.Entry<T>> get(Content.Filter<T> ct)
-				throws IOException;
+		public <T> List<Path.Entry<T>> get(Content.Filter<T> ct) throws IOException;
 
 		/**
 		 * Identify all entries matching a given content filter stored in this
@@ -100,8 +97,7 @@ public <T> List<Path.Entry<T>> get(Content.Filter<T> ct)
 		 *            --- filter to match entries with.
 		 * @return
 		 */
-		public <T> Set<Path.ID> match(Content.Filter<T> filter)
-				throws IOException;
+		public <T> Set<Path.ID> match(Content.Filter<T> filter) throws IOException;
 	}
 
 	/**
@@ -143,13 +139,57 @@ public interface Rule {
 		 * not match against any source file in the group.
 		 * </p>
 		 *
-		 * @param The
-		 *            set of files currently being compiled.
+		 * @param group
+		 *            The set of files currently being compiled.
+		 * @param graph
+		 *            The build graph being constructed
 		 * @return The set of files generated by this rule (which may be empty,
 		 *         but cannot be <code>null</code>).
 		 * @throws IOException
 		 */
-		public Set<Path.Entry<?>> apply(Collection<? extends Path.Entry<?>> group)
+		public Set<Path.Entry<?>> apply(Collection<? extends Path.Entry<?>> group, Build.Graph graph)
 				throws IOException;
 	}
+
+	/**
+	 * <p>
+	 * A build graph captures the relationships between compilation units. There
+	 * are two relationships of interest: <i>vertical</i> and <i>horizontal</i>
+	 * dependencies. For example one (or more) files being compiled to produce a
+	 * generated or <i>derived</i> file corresponds to a vertical dependency
+	 * between the original and the derived files. Horizontal dependencies
+	 * correspond to situations where one file at the same level uses symbols
+	 * from another.
+	 * </p>
+	 * 
+	 * @author David J. Pearce
+	 *
+	 */
+	public interface Graph {
+		/**
+		 * Determine the entry (the parent) that a given entry (the child) is
+		 * derived from, or null if no such entry exists. An entry is said to
+		 * derive from another if it generated from the other during the
+		 * compilation process. For example, a source file is compiled into a
+		 * binary or intermediate file. The latter is said to be derived from
+		 * the former.
+		 * 
+		 * @param child
+		 *            The child entry which is derived from zero or more parent
+		 *            entries.
+		 * @return
+		 */
+		Path.Entry<?> parent(Path.Entry<?> child);
+
+		/**
+		 * Register a derivation from one file (the parent) to another (the
+		 * child). A derivation indicates that one file (e.g. a source file)
+		 * generated another (e.g. a binary file) during the compilation
+		 * process.
+		 * 
+		 * @param parent
+		 * @param child
+		 */
+		void registerDerivation(Path.Entry<?> parent, Path.Entry<?> child);
+	}
 }

modules/wybs/src/wybs/lang/Builder.java

@@ -60,8 +60,10 @@ public interface Builder {
 	 *
 	 * @param delta
 	 *            --- the set of files to be built.
+	 * @param graph
+	 *            --- The build graph being constructed
 	 * @return --- the set of files generated or modified.
 	 */
 	public Set<Path.Entry<?>> build(
-			Collection<Pair<Path.Entry<?>, Path.Root>> delta) throws IOException;
+			Collection<Pair<Path.Entry<?>, Path.Root>> delta, Build.Graph graph) throws IOException;
 }

modules/wybs/src/wybs/util/StdBuildGraph.java

@@ -0,0 +1,31 @@
+package wybs.util;
+
+import java.util.HashMap;
+
+import wybs.lang.Build;
+import wyfs.lang.Path;
+import wyfs.lang.Path.Entry;
+
+/**
+ * Provides a straightforward implementation of the Build.Graph interface.
+ * 
+ * @author David J. Pearce
+ *
+ */
+public class StdBuildGraph implements Build.Graph {
+	/**
+	 * The derived from relation maps child entries to the parents they are
+	 * derived from.
+	 */
+	private HashMap<Path.Entry<?>, Path.Entry<?>> derivedFrom = new HashMap<>();
+
+	@Override
+	public Entry<?> parent(Entry<?> child) {
+		return derivedFrom.get(child);
+	}
+
+	@Override
+	public void registerDerivation(Path.Entry<?> parent, Path.Entry<?> child) {
+		derivedFrom.put(child, parent);
+	}
+}

modules/wybs/src/wybs/util/StdBuildRule.java

@@ -31,7 +31,7 @@ public class StdBuildRule implements Build.Rule {
 	/**
 	 * The builder used to build files using this rule.
 	 */
-	private final Builder builder;
+	final Builder builder;
 
 	/**
 	 * The source root containing all files which might be built using this
@@ -89,8 +89,7 @@ public StdBuildRule(Builder builder, Path.Root srcRoot,
 	}
 
 	@Override
-	public Set<Path.Entry<?>> apply(Collection<? extends Path.Entry<?>> group)
-			throws IOException {
+	public Set<Path.Entry<?>> apply(Collection<? extends Path.Entry<?>> group, Build.Graph graph) throws IOException {
 		ArrayList<Pair<Path.Entry<?>, Path.Root>> matches = new ArrayList<Pair<Path.Entry<?>, Path.Root>>();
 
 		// First, determine the set of matching files
@@ -106,7 +105,7 @@ public Set<Path.Entry<?>> apply(Collection<? extends Path.Entry<?>> group)
 
 		// Second, build all matching files
 		if (matches.size() > 0) {
-			return builder.build(matches);
+			return builder.build(matches, graph);
 		} else {
 			return Collections.EMPTY_SET;
 		}

modules/wybs/src/wybs/util/StdProject.java

@@ -66,7 +66,6 @@ public class StdProject implements Build.Project {
 	 */
 	protected final ArrayList<Build.Rule> rules;
 
-
 	public StdProject(Collection<Path.Root> roots) {
 		this.roots = new ArrayList<Path.Root>(roots);
 		this.rules = new ArrayList<Build.Rule>();
@@ -246,14 +245,15 @@ public void refresh() throws IOException {
 	 * @throws Exception
 	 */
 	public void build(Collection<? extends Path.Entry<?>> sources) throws Exception {
-
+		Build.Graph graph = new StdBuildGraph();
+
 		// Continue building all source files until there are none left. This is
 		// actually quite a naive implementation, as it ignores the potential
 		// need for staging dependencies.
 		do {
 			HashSet<Path.Entry<?>> generated = new HashSet<Path.Entry<?>>();
 			for (Build.Rule r : rules) {
-				generated.addAll(r.apply(sources));
+				generated.addAll(r.apply(sources,graph));
 			}
 			sources = generated;
 		} while (sources.size() > 0);