diff --git a/.gitignore b/.gitignore
index 49bb2c2b2..15da593af 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,3 +37,4 @@ enroute.zip
.idea
*.iml
+languageServers-log/AlloyLanguageServer.log
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 000000000..7b016a89f
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,3 @@
+{
+ "java.compile.nullAnalysis.mode": "automatic"
+}
\ No newline at end of file
diff --git a/README.md b/README.md
index 4eaf33cef..db8fc6338 100644
--- a/README.md
+++ b/README.md
@@ -78,12 +78,12 @@ Bndtools will continuously create the final executable. The projects are setup t
Ensure you have the [Osmorc] plugin is enabled, as this plugin is needed for
Bndtools support. It should be enabled by default.
-1. Choose "Import Project"
-2. Select the `org.alloytools.alloy` directory.
+1. Choose `Import project from existing Sources` by using `Ctrl + Shift + a`.
+2. Select the root folder (default folder name is `org.alloytools.alloy`).
3. Choose "Import project from external model: Bnd/Bndtools" and click "Next"
-4. For "Select Bnd/Bndtools project to import", all projects should be checked
- by default, click "Next"
+4. For "Select Bnd/Bndtools project to import", all projects should be checked by default, click "Next"
5. For project SDK, Choose "1.8", Click Finish
+6. Select folder `org/alloytools/kodkod/nativesat/jni` as `Resource Folder` by selecting module `org.alloytools.kodkod.nativesat`, selecting folder `jni` -> `right click` -> `Mark Directory As` -> `Resource Root`.
Note: do *not* link the Gradle project, as this will prevent you from running
Alloy within IDEA.
diff --git a/cnf/.project b/cnf/.project
index 0b7164229..b0d9ea35d 100644
--- a/cnf/.project
+++ b/cnf/.project
@@ -5,6 +5,11 @@
+
+ org.eclipse.buildship.core.gradleprojectbuilder
+
+
+ org.eclipse.jdt.core.javabuilder
@@ -13,5 +18,17 @@
org.eclipse.jdt.core.javanature
+ org.eclipse.buildship.core.gradleprojectnature
+
+
+ 1687449709131
+
+ 30
+
+ org.eclipse.core.resources.regexFilterMatcher
+ node_modules|\.git|__CREATED_BY_JAVA_LANGUAGE_SERVER__
+
+
+
diff --git a/cnf/.settings/org.eclipse.buildship.core.prefs b/cnf/.settings/org.eclipse.buildship.core.prefs
new file mode 100644
index 000000000..b1886adb4
--- /dev/null
+++ b/cnf/.settings/org.eclipse.buildship.core.prefs
@@ -0,0 +1,2 @@
+connection.project.dir=..
+eclipse.preferences.version=1
diff --git a/cnf/build.bnd b/cnf/build.bnd
index 21510a285..4ca8bea32 100644
--- a/cnf/build.bnd
+++ b/cnf/build.bnd
@@ -12,6 +12,7 @@ javac.source: 1.8
javac.target: 1.8
javac.compliance: 1.8
javac.debug: on
+-sources false
Git-Descriptor: ${system-allow-fail;git describe --dirty --always}
Git-SHA: ${system-allow-fail;git rev-list -1 HEAD}
@@ -27,6 +28,7 @@ Bundle-Version: ${base.version}.${tstamp}
# Remove -SNAPSHOT for release version
-pom: version=${base.version}-SNAPSHOT
-groupid: org.alloytools
+-includepackage *;from:=classes
#
@@ -61,8 +63,4 @@ usr = ${env;REPOSITORY_USERNAME;}
-connection-settings: ${if;${pwd};server;-dummy};id=https://oss.sonatype.org;username=${usr};password=${pwd}, -bnd
-#
-# Install a copy in the local Maven repository (~/.m2/repository)
-#
-
-
+-includepackage *;from:=classes
diff --git a/cnf/central.mvn b/cnf/central.mvn
index 37dea4666..f3fa8700b 100644
--- a/cnf/central.mvn
+++ b/cnf/central.mvn
@@ -1,12 +1,30 @@
+biz.aQute.bnd:aQute.libg:6.0.0
+biz.aQute:biz.aQute.wrapper.hamcrest:1.3
+biz.aQute:biz.aQute.wrapper.junit:4.13.1
+com.google.code.gson:gson:2.8.9
+com.google.code.gson:gson:2.8.9
+commons-io:commons-io:jar:2.6
+commons-io:commons-io:jar:2.6
+de.jflex:jflex:1.6.1
+org.alloytools:pardinus.core:1.3.0
+org.alloytools:pardinus.nativesat:1.3.0
+org.eclipse.equinox:org.eclipse.equinox.common:jar:3.6.0
+org.eclipse.equinox:org.eclipse.equinox.common:jar:3.6.0
org.eclipse.jdt:org.eclipse.jdt.annotation:2.1.100
+org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.4.1
+org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.4.1
+org.eclipse.lsp4j:org.eclipse.lsp4j:0.4.1
+org.eclipse.lsp4j:org.eclipse.lsp4j:0.4.1
org.sat4j:org.sat4j.core:2.3.1
org.sat4j:org.sat4j.maxsat:2.3.1
org.sat4j:org.sat4j.pb:2.3.1
-de.jflex:jflex:1.6.1
org.slf4j:slf4j-api:1.7.28
org.slf4j:slf4j-simple:1.7.5
org.alloytools:pardinus.core:1.3.0
org.alloytools:pardinus.nativesat:1.3.0
biz.aQute:biz.aQute.wrapper.hamcrest:1.3
biz.aQute:biz.aQute.wrapper.junit:4.13.1
-biz.aQute.bnd:aQute.libg:6.0.0
\ No newline at end of file
+biz.aQute.bnd:aQute.libg:6.1.0
+org.osgi:org.osgi.annotation.bundle:1.1.1
+org.osgi:osgi.annotation:8.0.1
+com.io7m.jpplib:io7m-jpplib-core:0.7.4
diff --git a/org.alloytools.alloy.application/.classpath b/org.alloytools.alloy.application/.classpath
index bcafe71e5..ae30f860a 100644
--- a/org.alloytools.alloy.application/.classpath
+++ b/org.alloytools.alloy.application/.classpath
@@ -1,12 +1,19 @@
-
-
-
-
+
+
+
+
+
+
+
+
+
-
+
+
+
diff --git a/org.alloytools.alloy.application/.project b/org.alloytools.alloy.application/.project
index 2f98f1715..1d348fb1e 100644
--- a/org.alloytools.alloy.application/.project
+++ b/org.alloytools.alloy.application/.project
@@ -10,6 +10,11 @@
+
+ org.eclipse.buildship.core.gradleprojectbuilder
+
+
+ bndtools.core.bndbuilder
@@ -19,5 +24,17 @@
org.eclipse.jdt.core.javanaturebndtools.core.bndnature
+ org.eclipse.buildship.core.gradleprojectnature
+
+
+ 1687449709165
+
+ 30
+
+ org.eclipse.core.resources.regexFilterMatcher
+ node_modules|\.git|__CREATED_BY_JAVA_LANGUAGE_SERVER__
+
+
+
diff --git a/org.alloytools.alloy.application/.settings/org.eclipse.buildship.core.prefs b/org.alloytools.alloy.application/.settings/org.eclipse.buildship.core.prefs
new file mode 100644
index 000000000..b1886adb4
--- /dev/null
+++ b/org.alloytools.alloy.application/.settings/org.eclipse.buildship.core.prefs
@@ -0,0 +1,2 @@
+connection.project.dir=..
+eclipse.preferences.version=1
diff --git a/org.alloytools.alloy.application/.settings/org.eclipse.jdt.core.prefs b/org.alloytools.alloy.application/.settings/org.eclipse.jdt.core.prefs
index 2f809de6d..978ab1820 100644
--- a/org.alloytools.alloy.application/.settings/org.eclipse.jdt.core.prefs
+++ b/org.alloytools.alloy.application/.settings/org.eclipse.jdt.core.prefs
@@ -26,9 +26,9 @@ org.eclipse.jdt.core.compiler.annotation.nullable=org.eclipse.jdt.annotation.Nul
org.eclipse.jdt.core.compiler.annotation.nullanalysis=disabled
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=17
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
-org.eclipse.jdt.core.compiler.compliance=1.8
+org.eclipse.jdt.core.compiler.compliance=17
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
@@ -91,7 +91,7 @@ org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=warning
org.eclipse.jdt.core.compiler.problem.overridingPackageDefaultMethod=warning
org.eclipse.jdt.core.compiler.problem.parameterAssignment=ignore
org.eclipse.jdt.core.compiler.problem.possibleAccidentalBooleanAssignment=warning
-org.eclipse.jdt.core.compiler.problem.potentialNullReference=warning
+org.eclipse.jdt.core.compiler.problem.potentialNullReference=ignore
org.eclipse.jdt.core.compiler.problem.potentiallyUnclosedCloseable=ignore
org.eclipse.jdt.core.compiler.problem.rawTypeReference=warning
org.eclipse.jdt.core.compiler.problem.redundantNullAnnotation=warning
@@ -134,7 +134,7 @@ org.eclipse.jdt.core.compiler.problem.unusedWarningToken=ignore
org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
org.eclipse.jdt.core.compiler.processAnnotations=disabled
org.eclipse.jdt.core.compiler.release=disabled
-org.eclipse.jdt.core.compiler.source=1.8
+org.eclipse.jdt.core.compiler.source=17
org.eclipse.jdt.core.compiler.taskCaseSensitive=enabled
org.eclipse.jdt.core.compiler.taskPriorities=NORMAL,NORMAL
org.eclipse.jdt.core.compiler.taskTags=TODO,FIXME
@@ -143,6 +143,7 @@ org.eclipse.jdt.core.formatter.align_fields_grouping_blank_lines=4
org.eclipse.jdt.core.formatter.align_type_members_on_columns=true
org.eclipse.jdt.core.formatter.align_variable_declarations_on_columns=false
org.eclipse.jdt.core.formatter.align_with_spaces=false
+org.eclipse.jdt.core.formatter.alignment_for_additive_operator=2
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=2
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_annotation=51
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=50
@@ -150,21 +151,24 @@ org.eclipse.jdt.core.formatter.alignment_for_arguments_in_explicit_constructor_c
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_method_invocation=2
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_expression=2
org.eclipse.jdt.core.formatter.alignment_for_assignment=2
-org.eclipse.jdt.core.formatter.alignment_for_binary_expression=2
+org.eclipse.jdt.core.formatter.alignment_for_bitwise_operator=2
org.eclipse.jdt.core.formatter.alignment_for_compact_if=2
org.eclipse.jdt.core.formatter.alignment_for_compact_loops=16
org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=2
org.eclipse.jdt.core.formatter.alignment_for_enum_constants=51
org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=2
org.eclipse.jdt.core.formatter.alignment_for_expressions_in_for_loop_header=2
+org.eclipse.jdt.core.formatter.alignment_for_logical_operator=2
org.eclipse.jdt.core.formatter.alignment_for_method_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_module_statements=16
org.eclipse.jdt.core.formatter.alignment_for_multiple_fields=16
+org.eclipse.jdt.core.formatter.alignment_for_multiplicative_operator=2
org.eclipse.jdt.core.formatter.alignment_for_parameterized_type_references=0
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_constructor_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_method_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_resources_in_try=2
org.eclipse.jdt.core.formatter.alignment_for_selector_in_method_invocation=2
+org.eclipse.jdt.core.formatter.alignment_for_string_concatenation=2
org.eclipse.jdt.core.formatter.alignment_for_superclass_in_type_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_enum_declaration=50
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_type_declaration=2
@@ -256,11 +260,12 @@ org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert
+org.eclipse.jdt.core.formatter.insert_space_after_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation_type_declaration=do not insert
-org.eclipse.jdt.core.formatter.insert_space_after_binary_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_after_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_brace_in_block=insert
@@ -291,6 +296,8 @@ org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_ellipsis=insert
org.eclipse.jdt.core.formatter.insert_space_after_lambda_arrow=insert
+org.eclipse.jdt.core.formatter.insert_space_after_logical_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_after_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_parameters=do not insert
@@ -315,13 +322,17 @@ org.eclipse.jdt.core.formatter.insert_space_after_postfix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_wildcard=insert
+org.eclipse.jdt.core.formatter.insert_space_after_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_for=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_try_resources=insert
+org.eclipse.jdt.core.formatter.insert_space_after_shift_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_after_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_after_unary_operator=do not insert
+org.eclipse.jdt.core.formatter.insert_space_before_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_before_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_at_in_annotation_type_declaration=insert
-org.eclipse.jdt.core.formatter.insert_space_before_binary_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_before_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_parameters=do not insert
@@ -369,6 +380,8 @@ org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_arguments=do no
org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_parameters=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_ellipsis=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_lambda_arrow=insert
+org.eclipse.jdt.core.formatter.insert_space_before_logical_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_before_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_parameters=do not insert
@@ -405,9 +418,12 @@ org.eclipse.jdt.core.formatter.insert_space_before_postfix_operator=do not inser
org.eclipse.jdt.core.formatter.insert_space_before_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_wildcard=insert
+org.eclipse.jdt.core.formatter.insert_space_before_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_for=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_try_resources=do not insert
+org.eclipse.jdt.core.formatter.insert_space_before_shift_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_before_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_before_unary_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_brackets_in_array_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_empty_braces_in_array_initializer=do not insert
@@ -446,10 +462,14 @@ org.eclipse.jdt.core.formatter.tabulation.char=space
org.eclipse.jdt.core.formatter.tabulation.size=4
org.eclipse.jdt.core.formatter.use_on_off_tags=true
org.eclipse.jdt.core.formatter.use_tabs_only_for_leading_indentations=true
+org.eclipse.jdt.core.formatter.wrap_before_additive_operator=true
org.eclipse.jdt.core.formatter.wrap_before_assignment_operator=false
-org.eclipse.jdt.core.formatter.wrap_before_binary_operator=true
+org.eclipse.jdt.core.formatter.wrap_before_bitwise_operator=true
org.eclipse.jdt.core.formatter.wrap_before_conditional_operator=true
+org.eclipse.jdt.core.formatter.wrap_before_logical_operator=true
+org.eclipse.jdt.core.formatter.wrap_before_multiplicative_operator=true
org.eclipse.jdt.core.formatter.wrap_before_or_operator_multicatch=true
+org.eclipse.jdt.core.formatter.wrap_before_string_concatenation=true
org.eclipse.jdt.core.formatter.wrap_outer_expressions_when_nested=true
org.eclipse.jdt.core.incompatibleJDKLevel=ignore
org.eclipse.jdt.core.incompleteClasspath=error
diff --git a/org.alloytools.alloy.application/bnd.bnd b/org.alloytools.alloy.application/bnd.bnd
index ff7ee2679..d22a42e87 100644
--- a/org.alloytools.alloy.application/bnd.bnd
+++ b/org.alloytools.alloy.application/bnd.bnd
@@ -5,7 +5,9 @@
lib/apple-osx-ui.jar;version=file,\
org.alloytools:pardinus.core;version='1.3.0',\
org.alloytools.alloy.core;version=latest,\
- aQute.libg
+ org.alloytools.alloy.dash;version=latest,\
+ aQute.libg,\
+ org.alloytools.api
-testpath: \
biz.aQute.wrapper.junit, \
biz.aQute.wrapper.hamcrest, \
@@ -15,3 +17,4 @@ Private-Package: \
edu.mit.csail.sdg.alloy4graph,\
edu.mit.csail.sdg.alloy4viz,\
edu.mit.csail.sdg.alloy4whole,\
+ ca.uwaterloo.watform.dash4whole,\
\ No newline at end of file
diff --git a/org.alloytools.alloy.application/src/main/java/ca/uwaterloo/watform/dash4whole/Dash.java b/org.alloytools.alloy.application/src/main/java/ca/uwaterloo/watform/dash4whole/Dash.java
new file mode 100644
index 000000000..19edc69b9
--- /dev/null
+++ b/org.alloytools.alloy.application/src/main/java/ca/uwaterloo/watform/dash4whole/Dash.java
@@ -0,0 +1,271 @@
+package ca.uwaterloo.watform.dash4whole;
+
+import java.util.*;
+
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.nio.file.Files;
+
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+
+import edu.mit.csail.sdg.alloy4.Version;
+
+import edu.mit.csail.sdg.alloy4.A4Reporter;
+import edu.mit.csail.sdg.alloy4viz.VizGUI;
+import edu.mit.csail.sdg.ast.Command;
+import edu.mit.csail.sdg.parser.CompModule;
+import edu.mit.csail.sdg.translator.A4Options;
+import edu.mit.csail.sdg.translator.A4Solution;
+import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
+
+import ca.uwaterloo.watform.core.DashOptions;
+import ca.uwaterloo.watform.core.DashErrors;
+import ca.uwaterloo.watform.parser.DashUtil;
+import ca.uwaterloo.watform.core.DashUtilFcns;
+import ca.uwaterloo.watform.parser.DashModule;
+import ca.uwaterloo.watform.mainfunctions.MainFunctions;
+
+
+
+
+public class Dash {
+
+ @SuppressWarnings("resource" )
+
+ public static void executeCommands(CompModule c, Integer commandNumber, A4Reporter rep) {
+ // Choose some default options for how you want to execute the commands
+ A4Options options = new A4Options();
+
+ List commands = c.getAllCommands();
+ // this is an annoying way to convert a list to an array
+ Integer i = 1;
+ for (Command cmd : commands) {
+ if (i == commandNumber | commandNumber == 0) {
+ System.out.println("Executing command: " + cmd);
+ A4Solution ans = null;
+ try {
+ ans = MainFunctions.executeCommand(cmd,c,rep, options);
+ } catch (Exception e) {
+ DashUtilFcns.handleException(e);
+ }
+ if (ans.satisfiable()) {
+ if (cmd.expects == 1)
+ System.out.println("Result: SAT (CORRECT)");
+ else if (cmd.expects == 0)
+ System.out.println("Result: SAT (INCORRECT)");
+ else
+ System.out.println("Result: SAT (nothing expected)");
+ } else {
+ if (cmd.expects == 0)
+ System.out.println("Result: UNSAT (CORRECT)");
+ else if (cmd.expects == 1)
+ System.out.println("Result: UNSAT (INCORRECT)");
+ else
+ System.out.println("Result: UNSAT (nothing expected)");
+ }
+
+ }
+ i++;
+ }
+ if (commandNumber >= i) {
+ System.err.println("Command number: " + commandNumber + " does not exist in file");
+ }
+ }
+
+ public static void main(String args[]) throws Exception {
+
+ if(args.length == 0) {
+ System.out.println("Arguments: (-m traces|tcmc|electrum) (-single) (-reach) (-c #) (-p) (-t) (-tla) (-r) filename(s)");
+ System.out.println("-m traces|tcmc|electrum is verification method");
+ System.out.println("-single includes single event input fact");
+ System.out.println("-reach includes reachability fact (for tcmc only)");
+ System.out.println("-enough includes enoughOperations pred");
+ System.out.println("-c # is commandNumber to execute");
+ System.out.println("-t is translateOnly");
+ System.out.println("-r is resolveOnly");
+ System.out.println("-e is echo file from internal parsed data");
+ System.out.println("-tla translates the file to TLA+, translated file has the same path and name unless otherwise specified");
+ System.out.println("expects .dsh or .als file");
+ System.out.println("if given a .als files, it ignores other options and runs all its commands");
+ System.exit(0);
+ }
+
+ // simple roll-our-own argument parser
+ // to avoid having to import an external package
+
+ List filelist = new ArrayList<>();
+
+ // default values
+ String method = "traces";
+ int commandNumber = 0;
+ boolean translateOnly = false;
+ boolean printOnly = false;
+ boolean resolveOnly = false;
+ boolean translateTLA = false;
+
+ for (int i=0; i 0) // if the file has a dot and no "dsh" after it, it is assumed to be a different type of file
+ {
+ System.err.println("Expected a Dash file with 'dsh' or 'als' extension: "+filename);
+ break;
+ }
+ else filename = filename + ".dsh"; // if there is no dot, it is assumed that the user forgot to add .dsh
+ }
+
+ Path f = Paths.get(filename);
+
+ if (Files.notExists(f)) {
+ System.err.println(filename + " : does not exist");
+ return;
+ }
+
+ Path directory = f.toAbsolutePath().getParent();
+ if (directory.toString() != null)
+ DashOptions.dashModelLocation = directory.toString();
+
+
+ System.out.println("Reading: " + filename );
+
+ A4Reporter rep = new A4Reporter();
+
+ if (filename.endsWith(".als")) {
+ try {
+ CompModule c = MainFunctions.parseAlloyFileAndResolveAll(filename, rep);
+ System.out.println("Parsed Alloy file");
+ // will raise an exception if problems
+ System.out.println("Resolved Alloy file");
+ executeCommands(c,commandNumber,rep);
+ } catch (Exception e) {
+ DashUtilFcns.handleException(e);
+ }
+ } else {
+ try {
+ DashModule d = MainFunctions.parseDashFile(filename, rep);
+ System.out.println("Parsed Dash file");
+ if (d == null) DashErrors.emptyFile(filename);
+
+ if (printOnly) {
+ System.out.println(d.toStringAlloy());
+ } else if(translateTLA)
+ {
+ d = MainFunctions.resolveDash(d, rep);
+ String moduleWithExtension = f.getFileName().toString();
+ String moduleName = moduleWithExtension.substring(0, moduleWithExtension.length()-4);
+ String contents = MainFunctions.translateTLA(d,moduleName);
+
+ // by default, the target is a file in the same folder as the source
+ String TLAfilename = filename.substring(0,filename.length()-4)+".tla";
+
+ // allow user to specify the target right next to the source if they want
+ try
+ {
+ String target = filelist.get(i+1);
+ if(target.endsWith(".tla"))
+ {
+ i++; // if an explicit target is mentioned, it is skipped over in the next iteration
+ TLAfilename = target;
+ }
+ }
+ catch(ArrayIndexOutOfBoundsException e){}
+
+ System.out.println("Translating "+filename+" to TLA+ and writing to "+TLAfilename);
+
+ File out = new File(TLAfilename);
+ if (!out.exists()) out.createNewFile();
+ System.out.println("Creating: " + TLAfilename);
+ FileWriter fw = new FileWriter(out.getAbsoluteFile());
+ BufferedWriter bw = new BufferedWriter(fw);
+ bw.write(contents);
+ bw.close();
+ }
+ else {
+ d = MainFunctions.resolveDash(d, rep);
+ System.out.println("Resolved Dash");
+ CompModule c = MainFunctions.translate(d, rep);
+ System.out.println("Translated Dash to Alloy");
+ // if problem exception would be raised
+ if (translateOnly) {
+ String outfilename = filename.substring(0,filename.length()-4) + "-" + method + ".als";
+ File out = new File(outfilename);
+ if (!out.exists()) out.createNewFile();
+ System.out.println("Creating: " + outfilename);
+ FileWriter fw = new FileWriter(out.getAbsoluteFile());
+ BufferedWriter bw = new BufferedWriter(fw);
+ bw.write(d.toStringAlloy());
+ bw.close();
+ } else {
+ c = MainFunctions.resolveAlloy(c,rep);
+ System.out.println("Resolved Alloy");
+ if (!resolveOnly) {
+ executeCommands(c,commandNumber,rep);
+ }
+ }
+ }
+ } catch (Exception e) {
+ DashUtilFcns.handleException(e);
+ }
+ }
+ }
+ }
+}
+
diff --git a/org.alloytools.alloy.application/src/main/java/ca/uwaterloo/watform/dash4whole/DashMainTest.java b/org.alloytools.alloy.application/src/main/java/ca/uwaterloo/watform/dash4whole/DashMainTest.java
new file mode 100644
index 000000000..57d235bf4
--- /dev/null
+++ b/org.alloytools.alloy.application/src/main/java/ca/uwaterloo/watform/dash4whole/DashMainTest.java
@@ -0,0 +1,66 @@
+/*
+ The purpose of this code is to help
+ with debugging
+*/
+
+package ca.uwaterloo.watform.dash4whole;
+
+import java.util.*;
+
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.nio.file.Files;
+
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+
+import edu.mit.csail.sdg.alloy4.A4Reporter;
+import edu.mit.csail.sdg.alloy4viz.VizGUI;
+import edu.mit.csail.sdg.ast.Command;
+import edu.mit.csail.sdg.parser.CompModule;
+import edu.mit.csail.sdg.translator.A4Options;
+import edu.mit.csail.sdg.translator.A4Solution;
+import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
+
+import ca.uwaterloo.watform.core.DashOptions;
+import ca.uwaterloo.watform.core.DashFQN;
+import ca.uwaterloo.watform.parser.DashUtil;
+import ca.uwaterloo.watform.parser.DashModule;
+import ca.uwaterloo.watform.mainfunctions.MainFunctions;
+
+
+
+
+public class DashMainTest {
+
+
+
+
+ public static void main(String args[]) {
+
+ System.out.println("Starting DashMainTest");
+ A4Reporter rep = new A4Reporter();
+ if(args.length != 0) {
+ // first arg is filename
+ String fname = args[0];
+ DashModule d =
+ MainFunctions.parseAndResolveDashFile(fname,rep);
+ if (args.length == 2) {
+ // transition name
+ d.debug(args[1]);
+ } else d.debug();
+ }
+ /*
+ DashModule d =
+ MainFunctions.parseAndResolveDashFile(
+ "/Users/nday/UW/github/org.alloytools.alloy/org.alloytools.alloy.dash/src/test/resources/wfffail/noTrans1.dsh",rep);
+ */
+ //List p = DashFQN.allPrefixes("A/B/C");
+ //List k = (new String[]{"A", "A/B", "A/B/C"} ;
+ //System.out.println("all prefixes: " + p);
+ //assert(p.equals());
+ System.out.println("Finish DashMainTest");
+ }
+}
+
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/GraphViewer.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/GraphViewer.java
index e6ef4cdf6..a074b07f3 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/GraphViewer.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/GraphViewer.java
@@ -615,7 +615,7 @@ public void actionPerformed(ActionEvent e) {
}
Util.setCurrentDirectory(filename.getParentFile());
} catch (Throwable ex) {
- OurDialog.alert(parent, "An error has occured in writing the output file:\n" + ex);
+ OurDialog.alert(parent, "An error has occurred in writing the output file:\n" + ex);
}
}
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/AlloyModel.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/AlloyModel.java
index 4b696e846..8294b0fbc 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/AlloyModel.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/AlloyModel.java
@@ -58,8 +58,8 @@ public final class AlloyModel {
* If A extends B, then "(A,B)" will be in this map.
*
* AlloyModel's constructor ensures the following:
- * (1) hierachy.keySet() is always a subset of this.types
- * (2) hierachy.valueSet() is always a subset of this.types
+ * (1) hierarchy.keySet() is always a subset of this.types
+ * (2) hierarchy.valueSet() is always a subset of this.types
* (3) "univ" is never in the keySet
* (4) null is never in the keySet nor valueSet
* (5) there is no cycle in this relation
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/MagicLayout.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/MagicLayout.java
index 3e1fdbbd7..48d9fa42a 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/MagicLayout.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/MagicLayout.java
@@ -191,7 +191,7 @@ private final boolean hasLikelyProjectionTypeName(final String n) {
*
*
interesting example: 2d game grid
*
ex: toplogical sort -- layout tree and list, not cnxn between them
- *
look for homogenius binary relation (a -> a)
+ *
look for homogeneous binary relation (a -> a)
*
may be several relations defining the spine
*
*/
@@ -210,7 +210,7 @@ private void spine() {
if (!enumerationTypes.contains(targetType)) {
spines.add(r);
}
- // however, binary relations named parent should be layed
+ // however, binary relations named parent should be laid
// out backwards
if (r.getName().equals("parent")) {
vizState.layoutBack.put(r, true);
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java
index 713516543..19ad35595 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java
@@ -66,7 +66,7 @@ public final class StaticInstanceReader {
private final LinkedHashMap sig2type = new LinkedHashMap();
/**
- * This maps each Sig ot its corresponding unique VIsualizer AlloyAtom (if
+ * This maps each Sig to its corresponding unique VIsualizer AlloyAtom (if
* isMeta is true).
*/
private final LinkedHashMap sig2atom = new LinkedHashMap();
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/CLIFacade.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/CLIFacade.java
new file mode 100644
index 000000000..f344f5586
--- /dev/null
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/CLIFacade.java
@@ -0,0 +1,30 @@
+package edu.mit.csail.sdg.alloy4whole;
+
+import javax.swing.SwingUtilities;
+
+import org.alloytools.alloy.infrastructure.api.AlloyMain;
+
+import aQute.lib.getopt.Options;
+
+
+@AlloyMain(
+ name = "gui",
+ isDefault = true )
+public class CLIFacade {
+
+ interface GuiOptions extends Options {
+
+ }
+
+ public void _gui(GuiOptions options) {
+ SwingUtilities.invokeLater(new Runnable() {
+
+ @Override
+ public void run() {
+ new SimpleGUI(options._arguments().toArray(new String[0]));
+ }
+ });
+
+ }
+}
+
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/DemoFileSystem.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/DemoFileSystem.java
index 9d9b598e3..3e5dd6d27 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/DemoFileSystem.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/DemoFileSystem.java
@@ -21,6 +21,7 @@
import java.util.Set;
import edu.mit.csail.sdg.alloy4.Err;
+import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.ast.Attr;
import edu.mit.csail.sdg.ast.Command;
import edu.mit.csail.sdg.ast.Decl;
@@ -54,14 +55,14 @@ PrimSig makeSig(String name, boolean isAbstract, boolean isOne) throws Err {
}
PrimSig makeSig(PrimSig parent, String name, boolean isAbstract, boolean isOne) throws Err {
- PrimSig ans = new PrimSig(name, parent, (isAbstract ? Attr.ABSTRACT : null), (isOne ? Attr.ONE : null));
+ PrimSig ans = new PrimSig(null, name, Pos.UNKNOWN, parent, (isAbstract ? Attr.ABSTRACT : null), (isOne ? Attr.ONE : null));
sigs.add(ans);
return ans;
}
void runFor3(Expr expr) throws Err {
A4Options opt = new A4Options();
- Command cmd = new Command(false, 3, 3, 3, expr.and(fact));
+ Command cmd = new Command(false, 3, 3, 3, null, expr.and(fact));
A4Solution sol = TranslateAlloyToKodkod.execute_command(NOP, sigs, cmd, opt);
System.out.println(sol.toString().trim());
if (sol.satisfiable()) {
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/ExampleUsingTheAPI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/ExampleUsingTheAPI.java
index 29cbf8276..1a1930629 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/ExampleUsingTheAPI.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/ExampleUsingTheAPI.java
@@ -22,6 +22,7 @@
import java.util.List;
import edu.mit.csail.sdg.alloy4.Err;
+import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.ast.Attr;
import edu.mit.csail.sdg.ast.Command;
@@ -54,10 +55,10 @@ public static void main(String[] args) throws Err {
PrimSig B = new PrimSig("B");
// one sig A1 extends A {}
- PrimSig A1 = new PrimSig("A1", A, Attr.ONE);
+ PrimSig A1 = new PrimSig(null, "A1", Pos.UNKNOWN, A, Attr.ONE);
// one sig A2 extends A {}
- PrimSig A2 = new PrimSig("A2", A, Attr.ONE);
+ PrimSig A2 = new PrimSig(null, "A2", Pos.UNKNOWN, A, Attr.ONE);
// A { f: B lone->lone B }
Expr f = A.addField("f", B.lone_arrow_lone(B));
@@ -71,13 +72,13 @@ public static void main(String[] args) throws Err {
// If you want "setOf", you need: A.addField(null, "g", B.setOf())
// pred someG { some g }
- Func someG = new Func(null, "SomeG", null, null, g.some());
+ Func someG = new Func(null, Pos.UNKNOWN, "SomeG", null, null, g.some());
// pred atMostThree[x:univ, y:univ] { #(x+y) >= 3 }
Decl x = UNIV.oneOf("x");
Decl y = UNIV.oneOf("y");
Expr body = x.get().plus(y.get()).cardinality().lte(ExprConstant.makeNUMBER(3));
- Func atMost3 = new Func(null, "atMost3", Util.asList(x, y), null, body);
+ Func atMost3 = new Func(null, Pos.UNKNOWN, "atMost3", Util.asList(x, y), null, body);
List sigs = Arrays.asList(new Sig[] {
A, B, A1, A2
@@ -85,14 +86,14 @@ public static void main(String[] args) throws Err {
// run { some A && atMostThree[B,B] } for 3 but 3 int, 3 seq
Expr expr1 = A.some().and(atMost3.call(B, B));
- Command cmd1 = new Command(false, 3, 3, 3, expr1);
+ Command cmd1 = new Command(false, 3, 3, 3, null, expr1);
A4Solution sol1 = TranslateAlloyToKodkod.execute_command(NOP, sigs, cmd1, opt);
System.out.println("[Solution1]:");
System.out.println(sol1.toString());
// run { some f && SomeG[] } for 3 but 2 int, 1 seq, 5 A, exactly 6 B
Expr expr2 = f.some().and(someG.call());
- Command cmd2 = new Command(false, 3, 2, 1, expr2);
+ Command cmd2 = new Command(false, 3, 2, 1, null, expr2);
cmd2 = cmd2.change(A, false, 1);
cmd2 = cmd2.change(B, true, 1);
A4Solution sol2 = TranslateAlloyToKodkod.execute_command(NOP, sigs, cmd2, opt);
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java
index 499f47bb0..04c3af904 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java
@@ -10,6 +10,7 @@
import static edu.mit.csail.sdg.alloy4.A4Preferences.ImplicitThis;
import static edu.mit.csail.sdg.alloy4.A4Preferences.InferPartialInstance;
import static edu.mit.csail.sdg.alloy4.A4Preferences.LAF;
+import static edu.mit.csail.sdg.alloy4.A4Preferences.LineNumbers;
import static edu.mit.csail.sdg.alloy4.A4Preferences.NoOverflow;
import static edu.mit.csail.sdg.alloy4.A4Preferences.RecordKodkod;
import static edu.mit.csail.sdg.alloy4.A4Preferences.SkolemDepth;
@@ -345,13 +346,17 @@ private static boolean staticLibrary(String name) {
}
}
// check if in system path
- for (String str : (System.getenv("PATH")).split(Pattern.quote(File.pathSeparator))) {
+ for (String str : (System.getenv("PATH")).split(Pattern.quote(File.pathSeparator)))
+ try {
Path pth = Paths.get(str);
if (Files.exists(pth.resolve(name))) {
if (isDebug)
System.out.println("Loaded: " + name + " at " + pth);
return true;
}
+ } catch (java.nio.file.InvalidPathException e) {
+ if (isDebug)
+ System.out.println("Invalid file path on PATH: " + str + ", ignoring");
}
if (isDebug)
@@ -420,6 +425,7 @@ protected Component initEditorPane() {
JPanel p = OurUtil.makeGrid(2, gbc().make(), mkCombo(FontName), mkCombo(FontSize), mkCombo(TabSize));
addToGrid(p, mkCheckBox(SyntaxDisabled), gbc().pos(0, 3).gridwidth(2));
addToGrid(p, mkCheckBox(AntiAlias), gbc().pos(0, 4).gridwidth(2));
+ addToGrid(p, mkCheckBox(LineNumbers), gbc().pos(0, 5).gridwidth(2));
// JPanel p = new JPanel(new GridBagLayout());
// addToGrid(p, mkCheckBox(SyntaxDisabled), gbc().pos(0,
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java
index 5de8c4ebd..0871426b1 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java
@@ -235,9 +235,9 @@ public static void main(String[] args) throws Exception {
x.b.toString(sb, 4);
rep.flush();
}
- for (Pair x : m.getAllAssertions()) {
- sb.append("\nAssertion ").append(x.a).append("\n");
- x.b.toString(sb, 4);
+ for (edu.mit.csail.sdg.ast.Assert x : m.getAllAssertions()) {
+ sb.append("\nAssertion ").append(x.label).append("\n");
+ x.expr.toString(sb, 4);
rep.flush();
}
if (m == world)
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java
index 2fc53db2c..29dc8a8cf 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java
@@ -29,6 +29,7 @@
import static edu.mit.csail.sdg.alloy4.A4Preferences.ImplicitThis;
import static edu.mit.csail.sdg.alloy4.A4Preferences.InferPartialInstance;
import static edu.mit.csail.sdg.alloy4.A4Preferences.LAF;
+import static edu.mit.csail.sdg.alloy4.A4Preferences.LineNumbers;
import static edu.mit.csail.sdg.alloy4.A4Preferences.Model0;
import static edu.mit.csail.sdg.alloy4.A4Preferences.Model1;
import static edu.mit.csail.sdg.alloy4.A4Preferences.Model2;
@@ -123,6 +124,8 @@
import org.alloytools.alloy.core.AlloyCore;
+import aQute.lib.io.IO;
+
//import com.apple.eawt.Application;
//import com.apple.eawt.ApplicationAdapter;
//import com.apple.eawt.ApplicationEvent;
@@ -597,7 +600,7 @@ public void run() {
* Find a temporary directory to store Alloy files; it's guaranteed to be a
* canonical absolute path.
*/
- private static synchronized String alloyHome(JFrame parent) {
+ public static synchronized String alloyHome(JFrame parent) {
if (alloyHome != null)
return alloyHome;
String temp = System.getProperty("java.io.tmpdir");
@@ -626,7 +629,7 @@ private static synchronized String alloyHome(JFrame parent) {
* Create an empty temporary directory for use, designate it "deleteOnExit",
* then return it. It is guaranteed to be a canonical absolute path.
*/
- private static String maketemp(JFrame parent) {
+ public static String maketemp(JFrame parent) {
Random r = new Random(new Date().getTime());
while (true) {
int i = r.nextInt(1000000);
@@ -1440,6 +1443,7 @@ private Runner doRefreshOption() {
else
addToMenu(optmenu, AntiAlias);
addToMenu(optmenu, A4Preferences.LAF);
+ addToMenu(optmenu, LineNumbers);
optmenu.addSeparator();
@@ -1493,6 +1497,14 @@ private Runner doOptRefreshFont() {
return null;
}
+ private Runner doOptRefreshLineNumbers() {
+ if ( wrap ) {
+ return wrapMe();
+ }
+ text.enableLineNumbers(LineNumbers.get());
+ return null;
+ }
+
/** This method toggles the "antialias" checkbox. */
private Runner doOptAntiAlias() {
if (!wrap) {
@@ -1841,7 +1853,7 @@ private static SimTupleset convert(Object object) throws Err {
}
/** Converts an A4Solution into a SimInstance object. */
- private static SimInstance convert(Module root, A4Solution ans) throws Err {
+ public static SimInstance convert(Module root, A4Solution ans) throws Err {
SimInstance ct = new SimInstance(root, ans.getBitwidth(), ans.getMaxSeq());
for (Sig s : ans.getAllReachableSigs()) {
if (!s.builtin)
@@ -2003,7 +2015,7 @@ public void run() {
* The constructor; this method will be called by the AWT event thread, using
* the "invokeLater" method.
*/
- private SimpleGUI(final String[] args) {
+ SimpleGUI(final String[] args) {
UIManager.put("ToolTip.font", new FontUIResource("Courier New", Font.PLAIN, 14));
@@ -2220,7 +2232,7 @@ private void finishInit(String[] args, int width) {
PreferencesDialog.logOnChange(log, A4Preferences.allUserPrefs().toArray(new Pref< ? >[0]));
// Create the text area
- text = new OurTabbedSyntaxWidget(fontName, fontSize, TabSize.get(), frame);
+ text = new OurTabbedSyntaxWidget(fontName, fontSize, TabSize.get(), LineNumbers.get(), frame);
text.listeners.add(this);
text.enableSyntax(!SyntaxDisabled.get());
@@ -2282,6 +2294,7 @@ private void finishInit(String[] args, int width) {
prefDialog.addChangeListener(wrapToChangeListener(doOptAntiAlias()), AntiAlias);
prefDialog.addChangeListener(wrapToChangeListener(doOptSyntaxHighlighting()), SyntaxDisabled);
prefDialog.addChangeListener(wrapToChangeListener(doLookAndFeel()), LAF);
+ prefDialog.addChangeListener(wrapToChangeListener(doOptRefreshLineNumbers()), LineNumbers);
} finally {
wrap = false;
}
@@ -2312,12 +2325,11 @@ private void finishInit(String[] args, int width) {
frame.setJMenuBar(bar);
// Open the given file, if a filename is given in the command line
- for (String f : args)
- if (f.toLowerCase(Locale.US).endsWith(".als")) {
- File file = new File(f);
- if (file.exists() && file.isFile())
- doOpenFile(file.getPath());
- }
+ for (String f : args) {
+ File file = IO.getFile(f);
+ if (file.isFile())
+ doOpenFile(file.getPath());
+ }
// Update the title and status bar
notifyChange();
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java
index 113692e8d..9c19e83e2 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java
@@ -78,7 +78,7 @@
* parallel problem)
*/
-final class SimpleReporter extends A4Reporter {
+public final class SimpleReporter extends A4Reporter {
public static final class SimpleCallback1 implements WorkerCallback {
@@ -601,7 +601,7 @@ private static void writeXML(A4Reporter rep, Module mod, String filename, A4Solu
private int warn = 0;
/** Task that performs solution enumeration. */
- static final class SimpleTask2 implements WorkerTask {
+ public static final class SimpleTask2 implements WorkerTask {
private static final long serialVersionUID = 0;
public int index = -1; // [electrum] registers which iteration operation to perform
@@ -683,7 +683,7 @@ private static void validate(String filename) throws Exception {
}
/** Task that perform one command. */
- static final class SimpleTask1 implements WorkerTask {
+ public static final class SimpleTask1 implements WorkerTask {
private static final long serialVersionUID = 0;
public A4Options options;
@@ -762,38 +762,40 @@ else if (ai.highLevelCore().a.size() > 0)
rep.cb("", " #" + (i + 1) + ": Unknown.\n");
continue;
}
+ StringBuilder sb = new StringBuilder();
if (result.get(i).endsWith(".xml")) {
rep.cb("", " #" + (i + 1) + ": ");
rep.cb("link", r.check ? "Counterexample found. " : "Instance found. ", "XML: " + result.get(i));
- rep.cb("", r.label + (r.check ? " is invalid" : " is consistent"));
+ sb.append(r.label + (r.check ? " is invalid" : " is consistent"));
if (r.expects == 0)
- rep.cb("", ", contrary to expectation");
+ sb.append(", contrary to expectation");
else if (r.expects == 1)
- rep.cb("", ", as expected");
+ sb.append(", as expected");
} else if (result.get(i).endsWith(".core")) {
rep.cb("", " #" + (i + 1) + ": ");
rep.cb("link", r.check ? "No counterexample found. " : "No instance found. ", "CORE: " + result.get(i));
- rep.cb("", r.label + (r.check ? " may be valid" : " may be inconsistent"));
+ sb.append(r.label + (r.check ? " may be valid" : " may be inconsistent"));
if (r.expects == 1)
- rep.cb("", ", contrary to expectation");
+ sb.append(", contrary to expectation");
else if (r.expects == 0)
- rep.cb("", ", as expected");
+ sb.append(", as expected");
} else {
if (r.check)
- rep.cb("", " #" + (i + 1) + ": No counterexample found. " + r.label + " may be valid");
+ sb.append(" #" + (i + 1) + ": No counterexample found. " + r.label + " may be valid");
else
- rep.cb("", " #" + (i + 1) + ": No instance found. " + r.label + " may be inconsistent");
+ sb.append(" #" + (i + 1) + ": No instance found. " + r.label + " may be inconsistent");
if (r.expects == 1)
- rep.cb("", ", contrary to expectation");
+ sb.append(", contrary to expectation");
else if (r.expects == 0)
- rep.cb("", ", as expected");
+ sb.append(", as expected");
}
- rep.cb("", ".\n");
+ sb.append(".\n");
+ rep.cb("", sb.toString());
}
rep.cb("", "\n");
}
if (rep.warn > 1)
- rep.cb("bold", "Note: There were " + rep.warn + " compilation warnings. Please scroll up to see them.\n");
+ rep.cb("bold", "Note: There were " + rep.warn + " compilation warnings.\n");
if (rep.warn == 1)
rep.cb("bold", "Note: There was 1 compilation warning. Please scroll up to see it.\n");
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SwingLogPanel.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SwingLogPanel.java
index ae0a6a30d..3f9c1c149 100644
--- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SwingLogPanel.java
+++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SwingLogPanel.java
@@ -453,7 +453,7 @@ public void copy() {
log.copy();
}
- /** Removes any messages writtin in "red" style. */
+ /** Removes any messages written in "red" style. */
public void clearError() {
if (log == null)
return;
diff --git a/org.alloytools.alloy.core/.classpath b/org.alloytools.alloy.core/.classpath
index 133ceaf5e..7854e99ab 100644
--- a/org.alloytools.alloy.core/.classpath
+++ b/org.alloytools.alloy.core/.classpath
@@ -1,17 +1,25 @@
-
-
-
-
+
+
+
+
+
+
+
+
+
-
+
-
+
+
-
+
+
+
diff --git a/org.alloytools.alloy.core/.project b/org.alloytools.alloy.core/.project
index 36737ffb6..fc4184230 100644
--- a/org.alloytools.alloy.core/.project
+++ b/org.alloytools.alloy.core/.project
@@ -10,6 +10,11 @@
+
+ org.eclipse.buildship.core.gradleprojectbuilder
+
+
+ bndtools.core.bndbuilder
@@ -19,5 +24,17 @@
org.eclipse.jdt.core.javanaturebndtools.core.bndnature
+ org.eclipse.buildship.core.gradleprojectnature
+
+
+ 1687449709176
+
+ 30
+
+ org.eclipse.core.resources.regexFilterMatcher
+ node_modules|\.git|__CREATED_BY_JAVA_LANGUAGE_SERVER__
+
+
+
diff --git a/org.alloytools.alloy.core/.settings/org.eclipse.buildship.core.prefs b/org.alloytools.alloy.core/.settings/org.eclipse.buildship.core.prefs
new file mode 100644
index 000000000..b1886adb4
--- /dev/null
+++ b/org.alloytools.alloy.core/.settings/org.eclipse.buildship.core.prefs
@@ -0,0 +1,2 @@
+connection.project.dir=..
+eclipse.preferences.version=1
diff --git a/org.alloytools.alloy.core/.settings/org.eclipse.jdt.core.prefs b/org.alloytools.alloy.core/.settings/org.eclipse.jdt.core.prefs
index 2f809de6d..fee4ef9bf 100644
--- a/org.alloytools.alloy.core/.settings/org.eclipse.jdt.core.prefs
+++ b/org.alloytools.alloy.core/.settings/org.eclipse.jdt.core.prefs
@@ -23,12 +23,12 @@ org.eclipse.jdt.core.compiler.annotation.missingNonNullByDefaultAnnotation=ignor
org.eclipse.jdt.core.compiler.annotation.nonnull=org.eclipse.jdt.annotation.NonNull
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.eclipse.jdt.annotation.NonNullByDefault
org.eclipse.jdt.core.compiler.annotation.nullable=org.eclipse.jdt.annotation.Nullable
-org.eclipse.jdt.core.compiler.annotation.nullanalysis=disabled
+org.eclipse.jdt.core.compiler.annotation.nullanalysis=enabled
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=17
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
-org.eclipse.jdt.core.compiler.compliance=1.8
+org.eclipse.jdt.core.compiler.compliance=17
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
@@ -84,9 +84,9 @@ org.eclipse.jdt.core.compiler.problem.noEffectAssignment=warning
org.eclipse.jdt.core.compiler.problem.noImplicitStringConversion=warning
org.eclipse.jdt.core.compiler.problem.nonExternalizedStringLiteral=ignore
org.eclipse.jdt.core.compiler.problem.nonnullParameterAnnotationDropped=warning
-org.eclipse.jdt.core.compiler.problem.nullAnnotationInferenceConflict=error
+org.eclipse.jdt.core.compiler.problem.nullAnnotationInferenceConflict=warning
org.eclipse.jdt.core.compiler.problem.nullReference=warning
-org.eclipse.jdt.core.compiler.problem.nullSpecViolation=error
+org.eclipse.jdt.core.compiler.problem.nullSpecViolation=warning
org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=warning
org.eclipse.jdt.core.compiler.problem.overridingPackageDefaultMethod=warning
org.eclipse.jdt.core.compiler.problem.parameterAssignment=ignore
@@ -134,7 +134,7 @@ org.eclipse.jdt.core.compiler.problem.unusedWarningToken=ignore
org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
org.eclipse.jdt.core.compiler.processAnnotations=disabled
org.eclipse.jdt.core.compiler.release=disabled
-org.eclipse.jdt.core.compiler.source=1.8
+org.eclipse.jdt.core.compiler.source=17
org.eclipse.jdt.core.compiler.taskCaseSensitive=enabled
org.eclipse.jdt.core.compiler.taskPriorities=NORMAL,NORMAL
org.eclipse.jdt.core.compiler.taskTags=TODO,FIXME
@@ -143,6 +143,7 @@ org.eclipse.jdt.core.formatter.align_fields_grouping_blank_lines=4
org.eclipse.jdt.core.formatter.align_type_members_on_columns=true
org.eclipse.jdt.core.formatter.align_variable_declarations_on_columns=false
org.eclipse.jdt.core.formatter.align_with_spaces=false
+org.eclipse.jdt.core.formatter.alignment_for_additive_operator=2
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=2
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_annotation=51
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_enum_constant=50
@@ -150,21 +151,24 @@ org.eclipse.jdt.core.formatter.alignment_for_arguments_in_explicit_constructor_c
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_method_invocation=2
org.eclipse.jdt.core.formatter.alignment_for_arguments_in_qualified_allocation_expression=2
org.eclipse.jdt.core.formatter.alignment_for_assignment=2
-org.eclipse.jdt.core.formatter.alignment_for_binary_expression=2
+org.eclipse.jdt.core.formatter.alignment_for_bitwise_operator=2
org.eclipse.jdt.core.formatter.alignment_for_compact_if=2
org.eclipse.jdt.core.formatter.alignment_for_compact_loops=16
org.eclipse.jdt.core.formatter.alignment_for_conditional_expression=2
org.eclipse.jdt.core.formatter.alignment_for_enum_constants=51
org.eclipse.jdt.core.formatter.alignment_for_expressions_in_array_initializer=2
org.eclipse.jdt.core.formatter.alignment_for_expressions_in_for_loop_header=2
+org.eclipse.jdt.core.formatter.alignment_for_logical_operator=2
org.eclipse.jdt.core.formatter.alignment_for_method_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_module_statements=16
org.eclipse.jdt.core.formatter.alignment_for_multiple_fields=16
+org.eclipse.jdt.core.formatter.alignment_for_multiplicative_operator=2
org.eclipse.jdt.core.formatter.alignment_for_parameterized_type_references=0
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_constructor_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_parameters_in_method_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_resources_in_try=2
org.eclipse.jdt.core.formatter.alignment_for_selector_in_method_invocation=2
+org.eclipse.jdt.core.formatter.alignment_for_string_concatenation=2
org.eclipse.jdt.core.formatter.alignment_for_superclass_in_type_declaration=2
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_enum_declaration=50
org.eclipse.jdt.core.formatter.alignment_for_superinterfaces_in_type_declaration=2
@@ -256,11 +260,12 @@ org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_constant=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_enum_declaration=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_method_body=insert
org.eclipse.jdt.core.formatter.insert_new_line_in_empty_type_declaration=insert
+org.eclipse.jdt.core.formatter.insert_space_after_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_after_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_at_in_annotation_type_declaration=do not insert
-org.eclipse.jdt.core.formatter.insert_space_after_binary_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_after_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_angle_bracket_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_closing_brace_in_block=insert
@@ -291,6 +296,8 @@ org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_arguments=insert
org.eclipse.jdt.core.formatter.insert_space_after_comma_in_type_parameters=insert
org.eclipse.jdt.core.formatter.insert_space_after_ellipsis=insert
org.eclipse.jdt.core.formatter.insert_space_after_lambda_arrow=insert
+org.eclipse.jdt.core.formatter.insert_space_after_logical_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_after_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_opening_angle_bracket_in_type_parameters=do not insert
@@ -315,13 +322,17 @@ org.eclipse.jdt.core.formatter.insert_space_after_postfix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_after_question_in_wildcard=insert
+org.eclipse.jdt.core.formatter.insert_space_after_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_for=insert
org.eclipse.jdt.core.formatter.insert_space_after_semicolon_in_try_resources=insert
+org.eclipse.jdt.core.formatter.insert_space_after_shift_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_after_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_after_unary_operator=do not insert
+org.eclipse.jdt.core.formatter.insert_space_before_additive_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_and_in_type_parameter=insert
org.eclipse.jdt.core.formatter.insert_space_before_assignment_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_at_in_annotation_type_declaration=insert
-org.eclipse.jdt.core.formatter.insert_space_before_binary_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_before_bitwise_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_closing_angle_bracket_in_type_parameters=do not insert
@@ -369,6 +380,8 @@ org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_arguments=do no
org.eclipse.jdt.core.formatter.insert_space_before_comma_in_type_parameters=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_ellipsis=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_lambda_arrow=insert
+org.eclipse.jdt.core.formatter.insert_space_before_logical_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_before_multiplicative_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_parameterized_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_arguments=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_opening_angle_bracket_in_type_parameters=do not insert
@@ -405,9 +418,12 @@ org.eclipse.jdt.core.formatter.insert_space_before_postfix_operator=do not inser
org.eclipse.jdt.core.formatter.insert_space_before_prefix_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_conditional=insert
org.eclipse.jdt.core.formatter.insert_space_before_question_in_wildcard=insert
+org.eclipse.jdt.core.formatter.insert_space_before_relational_operator=insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_for=do not insert
org.eclipse.jdt.core.formatter.insert_space_before_semicolon_in_try_resources=do not insert
+org.eclipse.jdt.core.formatter.insert_space_before_shift_operator=insert
+org.eclipse.jdt.core.formatter.insert_space_before_string_concatenation=insert
org.eclipse.jdt.core.formatter.insert_space_before_unary_operator=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_brackets_in_array_type_reference=do not insert
org.eclipse.jdt.core.formatter.insert_space_between_empty_braces_in_array_initializer=do not insert
@@ -446,10 +462,14 @@ org.eclipse.jdt.core.formatter.tabulation.char=space
org.eclipse.jdt.core.formatter.tabulation.size=4
org.eclipse.jdt.core.formatter.use_on_off_tags=true
org.eclipse.jdt.core.formatter.use_tabs_only_for_leading_indentations=true
+org.eclipse.jdt.core.formatter.wrap_before_additive_operator=true
org.eclipse.jdt.core.formatter.wrap_before_assignment_operator=false
-org.eclipse.jdt.core.formatter.wrap_before_binary_operator=true
+org.eclipse.jdt.core.formatter.wrap_before_bitwise_operator=true
org.eclipse.jdt.core.formatter.wrap_before_conditional_operator=true
+org.eclipse.jdt.core.formatter.wrap_before_logical_operator=true
+org.eclipse.jdt.core.formatter.wrap_before_multiplicative_operator=true
org.eclipse.jdt.core.formatter.wrap_before_or_operator_multicatch=true
+org.eclipse.jdt.core.formatter.wrap_before_string_concatenation=true
org.eclipse.jdt.core.formatter.wrap_outer_expressions_when_nested=true
org.eclipse.jdt.core.incompatibleJDKLevel=ignore
org.eclipse.jdt.core.incompleteClasspath=error
diff --git a/org.alloytools.alloy.core/bnd.bnd b/org.alloytools.alloy.core/bnd.bnd
index 00b1a105b..164412e55 100644
--- a/org.alloytools.alloy.core/bnd.bnd
+++ b/org.alloytools.alloy.core/bnd.bnd
@@ -3,11 +3,14 @@
-includeresource: \
src/main/resources, \
@${repo;slf4j.api}, \
-
+
-buildpath: \
- org.alloytools:pardinus.core;version=1.3.0,\
- org.alloytools:pardinus.nativesat;version=1.3.0,\
- org.eclipse.jdt.annotation
+ org.alloytools:pardinus.core;version='1.3.0',\
+ org.alloytools:pardinus.nativesat;version='1.3.0',\
+ org.eclipse.jdt.annotation,\
+ aQute.libg,\
+ org.alloytools.api,\
+ slf4j.api
-testpath: \
biz.aQute.wrapper.junit, \
@@ -24,7 +27,9 @@ Export-Package: \
edu.mit.csail.sdg.sim,\
edu.mit.csail.sdg.translator,\
org.alloytools.util.table,\
- org.alloytools.alloy.core
+ org.alloytools.alloy.core, \
+ org.alloytools.alloy.core.util, \
+ com.io7m.jpplib.core, \
Private-Package: \
java_cup.runtime
diff --git a/org.alloytools.alloy.core/parser/Alloy.cup b/org.alloytools.alloy.core/parser/Alloy.cup
index 7d4f26005..12e02e32b 100644
--- a/org.alloytools.alloy.core/parser/Alloy.cup
+++ b/org.alloytools.alloy.core/parser/Alloy.cup
@@ -26,6 +26,7 @@ package edu.mit.csail.sdg.parser;
import java.util.Stack;
import java.util.List;
import java.util.ArrayList;
+import java.util.Locale;
import java.util.TreeSet;
import java.util.Map;
import java.util.LinkedHashMap;
@@ -164,7 +165,6 @@ parser code {:
ch.put(CompSym.ENUM, "enum");
ch.put(CompSym.EQUALS, "=");
ch.put(CompSym.EXACTLY, "exactly");
- ch.put(CompSym.EXH, "exh");
ch.put(CompSym.EXPECT, "expect");
ch.put(CompSym.EXTENDS, "extends");
ch.put(CompSym.FACT, "fact");
@@ -202,7 +202,6 @@ parser code {:
ch.put(CompSym.ONE, "one");
ch.put(CompSym.OPEN, "open");
ch.put(CompSym.OR, "||");
- ch.put(CompSym.PART, "part");
ch.put(CompSym.PLUS, "+");
ch.put(CompSym.PLUSPLUS, "++");
ch.put(CompSym.PRED, "pred");
@@ -298,7 +297,7 @@ parser code {:
if (content==null && loaded!=null) content = loaded.get(filename);
if (content==null) content = Util.readAll(filename);
if (loaded!=null) loaded.put(filename,content);
- content = MarkdownHandler.strip(content);
+ if (content.startsWith("---") || filename.toLowerCase(Locale.ROOT).endsWith(".md")) content = MarkdownHandler.strip(content);
content = Util.convertLineBreak(content);
isr = new StringReader(content);
CompFilter s = new CompFilter(u, seenDollar, filename, lineOffset, new BufferedReader(isr));
@@ -378,9 +377,9 @@ action code {:
}
}
if (n!=null)
- parser.alloymodule.addCommand(follow, p, n, o.label.equals("c"), overall, bitwidth, maxseq, mintime, maxtime, expects, s, x);
+ parser.alloymodule.addCommand(follow, p, n, o, overall, bitwidth, maxseq, mintime, maxtime, expects, s, x);
else
- parser.alloymodule.addCommand(follow, p, e, o.label.equals("c"), overall, bitwidth, maxseq, mintime, maxtime, expects, s, x);
+ parser.alloymodule.addCommand(follow, p, e, o, overall, bitwidth, maxseq, mintime, maxtime, expects, s, x);
}
private Expr t(Pos pos, Pos oldClosing, Expr left, Expr right, Pos close) throws Err {
if (right instanceof ExprVar) {
@@ -446,7 +445,6 @@ terminal Pos ELSE; // else
terminal Pos ENUM; // enum
terminal Pos EQUALS; // = ==
terminal Pos EXACTLY; // exactly
-terminal Pos EXH; // exh exhaustive
terminal Pos EXPECT; // expect
terminal Pos EXTENDS; // extends
terminal Pos FACT; // fact
@@ -484,7 +482,6 @@ terminal Pos ONE2; // one // The filter enables us to di
terminal Pos ONE; // one // The filter enables us to disambiguate
terminal Pos OPEN; // open
terminal Pos OR; // || or
-terminal Pos PART; // part partition
terminal Pos PLUS; // +
terminal Pos PLUSPLUS; // ++
terminal Pos PRED; // pred
@@ -648,9 +645,9 @@ Spec ::= Spec Vis:p ENUM:o Name:a LBRACE RBRACE:c {
Spec ::= Spec FACT:o Super:e {: parser.alloymodule.addFact (o , "" , e); :};
Spec ::= Spec FACT:o Name:n Super:e {: nod(n); parser.alloymodule.addFact (o , n.label , e); :};
Spec ::= Spec FACT:o STR:n Super:e {: parser.alloymodule.addFact (o , n.string , e); :};
-Spec ::= Spec ASSERT:o Super:e {: parser.alloymodule.addAssertion (o , "" , e); :};
-Spec ::= Spec ASSERT:o Name:n Super:e {: nod(n); parser.alloymodule.addAssertion (o , n.label , e); :};
-Spec ::= Spec ASSERT:o STR:n Super:e {: parser.alloymodule.addAssertion (o , n.string , e); :};
+Spec ::= Spec ASSERT:o Super:e {: parser.alloymodule.addAssertion (o , null , "" , e); :};
+Spec ::= Spec ASSERT:o Name:n Super:e {: nod(n); parser.alloymodule.addAssertion (o , n.pos, n.label , e); :};
+Spec ::= Spec ASSERT:o STR:n Super:e {: parser.alloymodule.addAssertion (o , null, n.string , e); :};
Spec ::= Spec Sig ;
Spec ::= Spec Function ;
Spec ::= Spec Predicate ;
@@ -673,8 +670,8 @@ Command ::= Command IMPLIES CommandPrefix:o Name:n Scope:s Expects:c {
Expects ::= {: RESULT=null; :};
Expects ::= EXPECT NUMBER:a {: RESULT=a; :};
-Scope ::= FOR NUMBER:a {: RESULT=new ArrayList(); RESULT.add(new CommandScope(a.pos, new PrimSig("univ", AttrType.WHERE.make(a.pos)), true, a.num, a.num, 1)); :};
-Scope ::= FOR NUMBER:a BUT Typescopes:b {: RESULT=b; b.add(new CommandScope(a.pos, new PrimSig("univ", AttrType.WHERE.make(a.pos)), true, a.num, a.num, 1)); :};
+Scope ::= FOR NUMBER:a {: RESULT=new ArrayList(); RESULT.add(new CommandScope(a.pos, Pos.UNKNOWN, new PrimSig("univ", AttrType.WHERE.make(a.pos)), true, a.num, a.num, 1)); :};
+Scope ::= FOR NUMBER:a BUT Typescopes:b {: RESULT=b; b.add(new CommandScope(a.pos, Pos.UNKNOWN, new PrimSig("univ", AttrType.WHERE.make(a.pos)), true, a.num, a.num, 1)); :};
Scope ::= FOR Typescopes:b {: RESULT=b; :};
Scope ::= {: RESULT=new ArrayList(); :};
@@ -683,7 +680,7 @@ Typescopes ::= Typescopes:a COMMA Typescope:b {: RESULT=a; a.add(b);
Typescope ::= TypeNumber:a Name:b {:
nod(b);
- RESULT = new CommandScope(a.pos.merge(b.pos), new PrimSig(b.label, AttrType.WHERE.make(a.pos.merge(b.pos))), a.isExact, a.startingScope, a.endingScope, a.increment);
+ RESULT = new CommandScope(a.pos.merge(b.pos), b.pos, new PrimSig(b.label, AttrType.WHERE.make(a.pos.merge(b.pos))), a.isExact, a.startingScope, a.endingScope, a.increment);
:};
//[AM]: INT -> SIGINT
@@ -691,31 +688,31 @@ Typescope ::= TypeNumber:a SIGINT:b {:
Pos p = a.pos.merge(b);
if (a.endingScope>a.startingScope) throw new ErrorSyntax(p, "Cannot specify a growing scope for \"Int\"");
if (a.isExact) throw new ErrorSyntax(p, "The exactly keyword is redundant here since the integer bitwidth must be exact.");
- RESULT = new CommandScope(p, new PrimSig("int", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.startingScope, 1);
+ RESULT = new CommandScope(p, b, new PrimSig("int", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.startingScope, 1);
:};
Typescope ::= TypeNumber:a INT:b {:
Pos p = a.pos.merge(b);
if (a.endingScope>a.startingScope) throw new ErrorSyntax(p, "Cannot specify a growing scope for \"Int\"");
if (a.isExact) throw new ErrorSyntax(p, "The exactly keyword is redundant here since the integer bitwidth must be exact.");
- RESULT = new CommandScope(p, new PrimSig("int", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.startingScope, 1);
+ RESULT = new CommandScope(p, b, new PrimSig("int", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.startingScope, 1);
:};
Typescope ::= TypeNumber:a SEQ:b {:
Pos p = a.pos.merge(b);
if (a.endingScope>a.startingScope) throw new ErrorSyntax(p, "Cannot specify a growing scope for \"seq\"");
if (a.isExact) throw new ErrorSyntax(p, "The exactly keyword is redundant here since the number of sequence index has to be exact.");
- RESULT = new CommandScope(p, new PrimSig("seq", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.startingScope, 1);
+ RESULT = new CommandScope(p, b, new PrimSig("seq", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.startingScope, 1);
:};
Typescope ::= TypeNumber:e UNIV:f {: if (1==1) throw new ErrorSyntax(e.pos.merge(f), "You cannot set a scope on univ."); :};
-Typescope ::= TypeNumber:a STRING:b {: RESULT = new CommandScope(a.pos.merge(b), new PrimSig("String", AttrType.WHERE.make(a.pos.merge(b))), a.isExact, a.startingScope, a.endingScope, a.increment); :};
+Typescope ::= TypeNumber:a STRING:b {: RESULT = new CommandScope(a.pos.merge(b), b, new PrimSig("String", AttrType.WHERE.make(a.pos.merge(b))), a.isExact, a.startingScope, a.endingScope, a.increment); :};
// [electrum] scope on Time
Typescope ::= TypeNumber:a TIME:b {:
Pos p = a.pos.merge(b);
- RESULT = new CommandScope(p, new PrimSig("steps", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.endingScope, a.increment);
+ RESULT = new CommandScope(p, Pos.UNKNOWN, new PrimSig("steps", AttrType.WHERE.make(p)), a.isExact, a.startingScope, a.endingScope, a.increment);
:};
//[AM] Typescope ::= TypeNumber:e SIGINT:f {: if (1==1) throw new ErrorSyntax(e.pos.merge(f), "You can no longer set a scope on Int; the number of Int atoms is always exactly equal to 2^(integer bitwidth).\n"); :};
@@ -723,39 +720,39 @@ Typescope ::= TypeNumber:a TIME:b {:
Typescope ::= TypeNumber:e NONE:f {: if (1==1) throw new ErrorSyntax(e.pos.merge(f), "You cannot set a scope on none."); :};
// [electrum] distinguish between "n" and "n..n", the latter become exact; open ended scopes "n.."
-TypeNumber ::= EXACTLY:e NUMBER:a {: RESULT = new CommandScope( e.merge(a.pos), Sig.NONE, true, a.num, a.num, 1 ); :};
-TypeNumber ::= EXACTLY:e NUMBER:a DOT DOT NUMBER:b {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e.merge(b.pos), Sig.NONE, true, a.num, b.num, 1 ); :};
-TypeNumber ::= EXACTLY:e NUMBER:a DOT DOT {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e , Sig.NONE, true, a.num, Integer.MAX_VALUE, 1 ); :};
-TypeNumber ::= EXACTLY:e NUMBER:a DOT DOT NUMBER:b COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e.merge(i.pos), Sig.NONE, true, a.num, b.num, i.num); :};
-TypeNumber ::= EXACTLY:e NUMBER:a COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e.merge(i.pos), Sig.NONE, true, a.num, Integer.MAX_VALUE, i.num); :};
-TypeNumber ::= NUMBER:a {: RESULT = new CommandScope(a.pos , Sig.NONE, false, a.num, a.num, 1 ); :};
-TypeNumber ::= NUMBER:a DOT DOT NUMBER:b {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos.merge(b.pos), Sig.NONE, a.num == b.num, a.num, b.num, 1 ); :};
-TypeNumber ::= NUMBER:a DOT DOT {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos , Sig.NONE, false, a.num, Integer.MAX_VALUE, 1 ); :};
-TypeNumber ::= NUMBER:a DOT DOT NUMBER:b COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos.merge(i.pos), Sig.NONE, a.num == b.num, a.num, b.num, i.num); :};
-TypeNumber ::= NUMBER:a COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos.merge(i.pos), Sig.NONE, false, a.num, Integer.MAX_VALUE, i.num); :};
-
-Macro ::= Vis:p LET:o Name:n LPAREN Names:d RPAREN MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.label, d , v); :};
-Macro ::= Vis:p LET:o Name:n LPAREN RPAREN MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.label, null , v); :};
-Macro ::= Vis:p LET:o Name:n LBRACKET Names:d RBRACKET MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.label, d , v); :};
-Macro ::= Vis:p LET:o Name:n LBRACKET RBRACKET MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.label, null , v); :};
-Macro ::= Vis:p LET:o Name:n MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.label, null , v); :};
+TypeNumber ::= EXACTLY:e NUMBER:a {: RESULT = new CommandScope( e.merge(a.pos), Pos.UNKNOWN, Sig.NONE, true, a.num, a.num, 1 ); :};
+TypeNumber ::= EXACTLY:e NUMBER:a DOT DOT NUMBER:b {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e.merge(b.pos), Pos.UNKNOWN, Sig.NONE, true, a.num, b.num, 1 ); :};
+TypeNumber ::= EXACTLY:e NUMBER:a DOT DOT {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e , Pos.UNKNOWN, Sig.NONE, true, a.num, Integer.MAX_VALUE, 1 ); :};
+TypeNumber ::= EXACTLY:e NUMBER:a DOT DOT NUMBER:b COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e.merge(i.pos), Pos.UNKNOWN, Sig.NONE, true, a.num, b.num, i.num); :};
+TypeNumber ::= EXACTLY:e NUMBER:a COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope( e.merge(i.pos), Pos.UNKNOWN, Sig.NONE, true, a.num, Integer.MAX_VALUE, i.num); :};
+TypeNumber ::= NUMBER:a {: RESULT = new CommandScope(a.pos , Pos.UNKNOWN, Sig.NONE, false, a.num, a.num, 1 ); :};
+TypeNumber ::= NUMBER:a DOT DOT NUMBER:b {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos.merge(b.pos), Pos.UNKNOWN, Sig.NONE, a.num == b.num, a.num, b.num, 1 ); :};
+TypeNumber ::= NUMBER:a DOT DOT {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos , Pos.UNKNOWN, Sig.NONE, false, a.num, Integer.MAX_VALUE, 1 ); :};
+TypeNumber ::= NUMBER:a DOT DOT NUMBER:b COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos.merge(i.pos), Pos.UNKNOWN, Sig.NONE, a.num == b.num, a.num, b.num, i.num); :};
+TypeNumber ::= NUMBER:a COLON NUMBER:i {: if (!Version.experimental) throw new ErrorSyntax(a.pos, "Syntax error here."); RESULT = new CommandScope(a.pos.merge(i.pos), Pos.UNKNOWN, Sig.NONE, false, a.num, Integer.MAX_VALUE, i.num); :};
+
+Macro ::= Vis:p LET:o Name:n LPAREN Names:d RPAREN MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.pos, n.label, d , v); :};
+Macro ::= Vis:p LET:o Name:n LPAREN RPAREN MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.pos, n.label, null , v); :};
+Macro ::= Vis:p LET:o Name:n LBRACKET Names:d RBRACKET MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.pos, n.label, d , v); :};
+Macro ::= Vis:p LET:o Name:n LBRACKET RBRACKET MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.pos, n.label, null , v); :};
+Macro ::= Vis:p LET:o Name:n MacroBody:v {: nod(n); parser.alloymodule.addMacro(o.merge(v.span()), p, n.pos, n.label, null , v); :};
MacroBody ::= Super:a {: RESULT=a; :};
MacroBody ::= EQUALS Expr:a {: RESULT=a; :};
-Function ::= Vis:p FUN:o Name:n LPAREN Decls:d RPAREN COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, null, d , mult(r), v); :};
-Function ::= Vis:p FUN:o Name:n LBRACKET Decls:d RBRACKET COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, null, d , mult(r), v); :};
-Function ::= Vis:p FUN:o Name:n COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, null, null , mult(r), v); :};
-Function ::= Vis:p FUN:o SigRef:f DOT Name:n LPAREN Decls:d RPAREN COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, f , d , mult(r), v); :};
-Function ::= Vis:p FUN:o SigRef:f DOT Name:n LBRACKET Decls:d RBRACKET COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, f , d , mult(r), v); :};
-Function ::= Vis:p FUN:o SigRef:f DOT Name:n COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, f , null , mult(r), v); :};
+Function ::= Vis:p FUN:o Name:n LPAREN Decls:d RPAREN COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, null, d , mult(r), v); :};
+Function ::= Vis:p FUN:o Name:n LBRACKET Decls:d RBRACKET COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, null, d , mult(r), v); :};
+Function ::= Vis:p FUN:o Name:n COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, null, null , mult(r), v); :};
+Function ::= Vis:p FUN:o SigRef:f DOT Name:n LPAREN Decls:d RPAREN COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, f , d , mult(r), v); :};
+Function ::= Vis:p FUN:o SigRef:f DOT Name:n LBRACKET Decls:d RBRACKET COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, f , d , mult(r), v); :};
+Function ::= Vis:p FUN:o SigRef:f DOT Name:n COLON Expr:r Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, f , null , mult(r), v); :};
-Predicate ::= Vis:p PRED:o Name:n LPAREN Decls:d RPAREN Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, null, d , null, v); :};
-Predicate ::= Vis:p PRED:o Name:n LBRACKET Decls:d RBRACKET Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, null, d , null, v); :};
-Predicate ::= Vis:p PRED:o Name:n Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, null, null , null, v); :};
-Predicate ::= Vis:p PRED:o SigRef:f DOT Name:n LPAREN Decls:d RPAREN Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, f , d , null, v); :};
-Predicate ::= Vis:p PRED:o SigRef:f DOT Name:n LBRACKET Decls:d RBRACKET Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, f , d , null, v); :};
-Predicate ::= Vis:p PRED:o SigRef:f DOT Name:n Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n.label, f , null , null, v); :};
+Predicate ::= Vis:p PRED:o Name:n LPAREN Decls:d RPAREN Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, null, d , null, v); :};
+Predicate ::= Vis:p PRED:o Name:n LBRACKET Decls:d RBRACKET Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, null, d , null, v); :};
+Predicate ::= Vis:p PRED:o Name:n Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, null, null , null, v); :};
+Predicate ::= Vis:p PRED:o SigRef:f DOT Name:n LPAREN Decls:d RPAREN Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, f , d , null, v); :};
+Predicate ::= Vis:p PRED:o SigRef:f DOT Name:n LBRACKET Decls:d RBRACKET Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, f , d , null, v); :};
+Predicate ::= Vis:p PRED:o SigRef:f DOT Name:n Super:v {: nod(n); parser.alloymodule.addFunc(o.merge(v.span()), p, n, f , null , null, v); :};
Vis ::= {: RESULT=null; :};
Vis ::= PRIVATE:p {: RESULT=p; :};
@@ -765,7 +762,7 @@ Sig ::= SigQuals:a Names:b SigIn:c LBRACE Decls:d RBRACE:o SuperOpt:e
if (e==null) e = ExprConstant.Op.TRUE.make(o, 0);
ExprVar cc = (c!=null && c.size()>0) ? c.remove(c.size()-1) : null;
for(ExprVar bb:b) {
- parser.alloymodule.addSig(bb.label, cc, c, d, e,
+ parser.alloymodule.addSig(bb.pos, bb.label, cc, c, d, e,
AttrType.WHERE .makenull(bb.pos.merge(e==null ? o : e.span())),
AttrType.ABSTRACT.makenull(a.get(0)),
AttrType.LONE .makenull(a.get(1)),
@@ -785,7 +782,7 @@ SigQual ::= PRIVATE:x {: RESULT=new ArrayList(6); RESULT.ad
SigQual ::= VAR:x {: RESULT=new ArrayList(6); RESULT.add(null); RESULT.add(null); RESULT.add(null); RESULT.add(null); RESULT.add(null); RESULT.add(x); :};
SigQuals ::= SIG {: RESULT=new ArrayList(6); RESULT.add(null); RESULT.add(null); RESULT.add(null); RESULT.add(null); RESULT.add(null); RESULT.add(null); :};
-SigQuals ::= SigQual:a SigQuals:b {: RESULT=a; for(int i=0;i<6;i++) if (a.get(i)==null) a.set(i,b.get(i)); else if (b.get(i)!=null) throw new ErrorSyntax(b.get(i), "The same qualifer cannot be specified more than once for the same sig."); :};
+SigQuals ::= SigQual:a SigQuals:b {: RESULT=a; for(int i=0;i<6;i++) if (a.get(i)==null) a.set(i,b.get(i)); else if (b.get(i)!=null) throw new ErrorSyntax(b.get(i), "The same qualifier cannot be specified more than once for the same sig."); :};
SigIn ::= EXTENDS:a SigRef:x {: RESULT=new ArrayList(2); RESULT.add(x); RESULT.add(ExprVar.make(a, "extends")); :};
SigIn ::= IN:a SigRefu:x {: RESULT=x; x.add(ExprVar.make(a,"in")); :};
@@ -825,8 +822,6 @@ Namex ::= Namex:a COMMA Name:b {: nod(b); a.add(b); RESULT=
Namex ::= Namex:a COMMA EXACTLY Name:b {: nod(b); a.add(null); a.add(b); RESULT=a; :};
// [electrum] additional parameter for variable declarations (for fields)
-Decla ::= PART:k Names COLON Expr {: if (1==1) throw CompModule.hint(k, "part"); :};
-Decla ::= EXH:k Names COLON Expr {: if (1==1) throw CompModule.hint(k, "exh"); :};
Decla ::= DISJ:k Names:a COLON Expr:b {: RESULT=new Decl(null, k, null, null, a, mult(b)); :};
Decla ::= PRIVATE:p DISJ:k Names:a COLON Expr:b {: RESULT=new Decl(p, k, null, null, a, mult(b)); :};
Decla ::= PRIVATE:p Names:a COLON Expr:b {: RESULT=new Decl(p, null, null, null, a, mult(b)); :};
@@ -837,8 +832,6 @@ Decla ::= VAR:v PRIVATE:p DISJ:k Names:a COLON Expr:b {: RESULT
Decla ::= VAR:v PRIVATE:p Names:a COLON Expr:b {: RESULT=new Decl(p, null, null, v, a, mult(b)); :};
Decla ::= VAR:v Names:a COLON Expr:b {: RESULT=new Decl(null, null, null, v, a, mult(b)); :};
-Decla ::= PART:k Names COLON DISJ Expr {: if (1==1) throw CompModule.hint(k, "part"); :};
-Decla ::= EXH:k Names COLON DISJ Expr {: if (1==1) throw CompModule.hint(k, "exh"); :};
Decla ::= DISJ:k Names:a COLON DISJ:d Expr:b {: RESULT=new Decl(null, k, d, null, a, mult(b)); :};
Decla ::= PRIVATE:p DISJ:k Names:a COLON DISJ:d Expr:b {: RESULT=new Decl(p, k, d, null, a, mult(b)); :};
Decla ::= PRIVATE:p Names:a COLON DISJ:d Expr:b {: RESULT=new Decl(p, null, d, null, a, mult(b)); :};
@@ -851,15 +844,11 @@ Decla ::= VAR:v Names:a COLON DISJ:d Expr:b {: RESULT
Declb ::= Decla:x {: RESULT=x; :};
-Declb ::= PART:k Names EQUALS Expr {: if (1==1) throw CompModule.hint(k, "part"); :};
-Declb ::= EXH:k Names EQUALS Expr {: if (1==1) throw CompModule.hint(k, "exh"); :};
Declb ::= DISJ:d Names EQUALS Expr {: if (1==1) throw new ErrorSyntax(d, "Defined fields cannot be disjoint."); :};
Declb ::= PRIVATE DISJ:d Names EQUALS Expr {: if (1==1) throw new ErrorSyntax(d, "Defined fields cannot be disjoint."); :};
Declb ::= PRIVATE:p Names:a EQUALS Expr:b {: RESULT=new Decl(p, null, null, null, a, ExprUnary.Op.EXACTLYOF.make(null, b)); :};
Declb ::= Names:a EQUALS Expr:b {: RESULT=new Decl(null, null, null, null, a, ExprUnary.Op.EXACTLYOF.make(null, b)); :};
-Declb ::= PART:k Names EQUALS DISJ Expr {: if (1==1) throw CompModule.hint(k, "part"); :};
-Declb ::= EXH:k Names EQUALS DISJ Expr {: if (1==1) throw CompModule.hint(k, "exh"); :};
Declb ::= DISJ Names EQUALS DISJ:d Expr {: if (1==1) throw new ErrorSyntax(d, "Defined fields cannot be disjoint."); :};
Declb ::= PRIVATE DISJ Names EQUALS DISJ:d Expr {: if (1==1) throw new ErrorSyntax(d, "Defined fields cannot be disjoint."); :};
Declb ::= PRIVATE Names EQUALS DISJ:d Expr {: if (1==1) throw new ErrorSyntax(d, "Defined fields cannot be disjoint."); :};
diff --git a/org.alloytools.alloy.core/parser/Alloy.lex b/org.alloytools.alloy.core/parser/Alloy.lex
index 4ec7c4cac..f0f8f2a65 100644
--- a/org.alloytools.alloy.core/parser/Alloy.lex
+++ b/org.alloytools.alloy.core/parser/Alloy.lex
@@ -186,8 +186,6 @@ import java_cup.runtime.*;
"else" { return alloy_sym(yytext(), CompSym.ELSE );}
"enum" { return alloy_sym(yytext(), CompSym.ENUM );}
"exactly" { return alloy_sym(yytext(), CompSym.EXACTLY );}
-"exhaustive" { return alloy_sym(yytext(), CompSym.EXH );}
-"exh" { return alloy_sym(yytext(), CompSym.EXH );}
"expect" { return alloy_sym(yytext(), CompSym.EXPECT );}
"extends" { return alloy_sym(yytext(), CompSym.EXTENDS );}
"fact" { return alloy_sym(yytext(), CompSym.FACT );}
@@ -208,8 +206,6 @@ import java_cup.runtime.*;
"one" { return alloy_sym(yytext(), CompSym.ONE );}
"open" { return alloy_sym(yytext(), CompSym.OPEN );}
"or" { return alloy_sym(yytext(), CompSym.OR );}
-"partition" { return alloy_sym(yytext(), CompSym.PART );}
-"part" { return alloy_sym(yytext(), CompSym.PART );}
"pred" { return alloy_sym(yytext(), CompSym.PRED );}
"private" { return alloy_sym(yytext(), CompSym.PRIVATE );}
"run" { return alloy_sym(yytext(), CompSym.RUN );}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/A4Preferences.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/A4Preferences.java
index 75365e8fc..52268d447 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/A4Preferences.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/A4Preferences.java
@@ -21,6 +21,7 @@
import java.util.Arrays;
import java.util.Collections;
import java.util.List;
+import java.util.Optional;
import java.util.prefs.Preferences;
import javax.swing.AbstractAction;
@@ -572,6 +573,9 @@ public void actionPerformed(ActionEvent e) {
/** The latest tab distance of the Alloy Analyzer. */
public static final IntChoicePref TabSize = IntChoicePref.range("TabSize", "Tab size", 1, 1, 16, 4);
+ /** The latest line-number mode selection of the Alloy Analyzer. */
+ public static final BooleanPref LineNumbers = new BooleanPref("Line-numbers", "Show line numbers in editors");
+
/** The latest welcome screen that the user has seen. */
public static final BooleanPref Welcome = new BooleanPref("Welcome", "Show welcome message at start up");
@@ -804,14 +808,28 @@ public final String toString() {
return ans;
}
- // /** The visualization algorithm */
- // public static final StringChoicePref VisualizationAlgorithm = new
- // StringChoicePref("VizAlg", "Visualization algorightm",
- // Arrays.asList("Sugiyama", "Circle", "Grid"), "Sugiyama");
- //
- // public static final IntPref GridLayoutRows = new
- // IntPref("GridLayoutRows", 1, 5, 100);
- // public static final IntPref GridLayoutCols = new
- // IntPref("GridLayoutCols", 1, 5, 100);
+ /**
+ * Convenience method to set a value by string
+ *
+ * @param id the id of the preference
+ * @param value the value in string form
+ * @return an error message or null if all ok
+ */
+
+ public static String set(String id, String value) {
+ Optional> pref = allPrefs().stream().filter(p -> p.id.equals(id)).findAny();
+ if (pref.isPresent()) {
+ try {
+ Pref p = (Pref) pref.get();
+ T parsed = (T) pref.get().parse(value);
+ p.set(parsed);
+ } catch (Exception e) {
+ return e.getMessage();
+ }
+ } else {
+ return "no such preference";
+ }
+ return null;
+ }
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurLineNumberWidget.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurLineNumberWidget.java
new file mode 100644
index 000000000..4301aaa10
--- /dev/null
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurLineNumberWidget.java
@@ -0,0 +1,277 @@
+package edu.mit.csail.sdg.alloy4;
+
+import javax.swing.*;
+import javax.swing.event.CaretEvent;
+import javax.swing.event.CaretListener;
+import javax.swing.event.DocumentEvent;
+import javax.swing.event.DocumentListener;
+import javax.swing.text.BadLocationException;
+import javax.swing.text.Element;
+import javax.swing.text.Utilities;
+import java.awt.*;
+import java.awt.event.ComponentEvent;
+import java.awt.event.ComponentListener;
+import java.awt.font.FontRenderContext;
+import java.util.Collections;
+import java.util.Objects;
+
+public class OurLineNumberWidget extends JComponent implements DocumentListener, CaretListener, ComponentListener {
+
+ /**
+ * combine the two submitted objects with a new OurLineNumberWidget and return
+ * that widget. We assume that other code has already connected these components appropriately.
+ *
+ * While callers could send any fontName and size that they wanted, here in Allow in the context of
+ * the editor the assumption is that the font preference set by the user for the whole app is
+ * applying here as well, so OurSyntaxWidget will be sending the same font that it receives to use.
+ *
+ * @param textPane the text pane that has the lines we want to draw numbers for
+ * @param scrollPane the scroll pane we will set a header row for to draw the line numbers for textPane
+ * @param display line numbers should display if true, should not otherwise
+ * @param fontName the fontName to be used to draw line numbers.
+ * @return the OurLineNumberWidget linking the two components, with the display and font set.
+ */
+ public static OurLineNumberWidget build(JTextPane textPane, JScrollPane scrollPane, boolean display, String fontName, int fontSize) {
+ Objects.requireNonNull(textPane);
+ Objects.requireNonNull(textPane.getDocument());
+ Objects.requireNonNull(scrollPane);
+ Objects.requireNonNull(fontName);
+ if ( fontSize < 1 ) {
+ throw new IllegalArgumentException("Font size must be at least 1");
+ }
+
+ OurLineNumberWidget ourLineNumberWidget = new OurLineNumberWidget(textPane, display, fontName, fontSize);
+ scrollPane.setRowHeaderView(ourLineNumberWidget);
+ return ourLineNumberWidget;
+ }
+
+ private static final boolean antiAlias = Util.onMac() || Util.onWindows();
+
+ private final JTextPane textPane;
+ private boolean display;
+ private String fontName;
+ private int fontSize;
+ private int width = 0;
+ private Font font;
+ /** assume we start showing 1 digit. */
+ private int currentMaxDigits = 1;
+ private int descentAdjust;
+
+ OurLineNumberWidget(JTextPane textPane, boolean display, String fontName, int fontSize) {
+ this.textPane = textPane;
+ this.display = display;
+ this.fontName = fontName;
+ this.fontSize = fontSize;
+
+ // falls back to 'Dialog' on not being able to find.
+ this.font = new Font(this.fontName, Font.PLAIN, this.fontSize);
+ this.descentAdjust = makeDescentAdjust();
+
+ textPane.getDocument().addDocumentListener(this);
+ textPane.addComponentListener(this);
+ textPane.addCaretListener(this);
+
+ update();
+ }
+
+ /** use current font to decide a width for the line-number view itself,
+ * based on how many digits are submitted.
+ * @param numberOfDigits
+ * @return
+ */
+ private int calculateWidthForDigits(int numberOfDigits) {
+ if ( display ) {
+ String numberOfDigitsLong = String.join("", Collections.nCopies(numberOfDigits, "0"));
+ return (int)Math.ceil(
+ font.getStringBounds(numberOfDigitsLong, new FontRenderContext(null, false, false)).getWidth() * 1.2);
+ } else {
+ return 0;
+ }
+ }
+
+ /** capture the descent of the current font, used to adjust (negative y) where the
+ * line number is drawn. Only needs to change when the font changes.
+ * @return
+ */
+ private int makeDescentAdjust() {
+ return getFontMetrics(font).getDescent();
+ }
+
+ @Override
+ protected void paintComponent(final Graphics g) {
+
+ if ( ! display ) { return; }
+
+ if ( g instanceof Graphics2D && antiAlias ) {
+ ((Graphics2D)g).setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
+ }
+
+ super.paintComponent(g);
+ // antiAlias at some point
+
+ Rectangle bounds = g.getClipBounds();
+ final int startDocumentLocation = textPane.viewToModel(new Point(0, bounds.y));
+ final int endDocumentLocation = textPane.viewToModel(new Point(0, bounds.y + bounds.height));
+
+ int docLoc = startDocumentLocation;
+ int maxDigits = 0;
+
+ while ( docLoc <= endDocumentLocation ) {
+ try {
+ Element rootElement = textPane.getDocument().getDefaultRootElement();
+ final int lineIndex = rootElement.getElementIndex(docLoc);
+ final Element line = rootElement.getElement(lineIndex);
+ if (line.getStartOffset() == docLoc) {
+ int x = niceX();
+ int y = niceY(docLoc);
+
+ String formattedLineNumber = formatLineNumberFromIndex(lineIndex);
+ if ( formattedLineNumber.length() > maxDigits ) {
+ maxDigits = formattedLineNumber.length();
+ }
+
+ g.setColor(Color.BLACK);
+ if (ifCaretOnSameLine(docLoc, rootElement)) {
+ Rectangle currentLineViewRec = textPane.modelToView(docLoc);
+ g.fillRect(0, currentLineViewRec.y, width, currentLineViewRec.height-1 );
+ g.setColor(Color.YELLOW);
+ }
+ g.setFont(font);
+ g.drawString(formattedLineNumber, x, y);
+ }
+ docLoc = Utilities.getRowEnd(textPane, docLoc) + 1;
+ } catch (BadLocationException e) {
+ // what is the right thing to do here?
+ }
+ }
+ if ( maxDigits != currentMaxDigits ) {
+ currentMaxDigits = maxDigits;
+ update();
+ }
+ }
+
+ private boolean ifCaretOnSameLine(int docLoc, Element rootElement) {
+ return rootElement.getElementIndex(docLoc) == rootElement.getElementIndex(textPane.getCaretPosition());
+ }
+
+ /** a judgement about where in the x direction is good
+ * to start drawing the line number.
+ * @return
+ */
+ private int niceX() {
+ return getInsets().left + 3;
+ }
+
+ /** a judgement about where in the y direction is good
+ * to start drawing the line number for the given document location.
+ * @param docLoc
+ * @return
+ * @throws BadLocationException
+ */
+ private int niceY(int docLoc) throws BadLocationException {
+ Rectangle viewRec = textPane.modelToView(docLoc);
+ return viewRec.y + viewRec.height - descentAdjust;
+ }
+
+ private String formatLineNumberFromIndex(int lineIndex) {
+ return String.format("%d", (lineIndex + 1));
+ }
+
+ /** Make a new width value, set new current preferred size and size,
+ * and try to get this component repainted.
+ * Currently all listener events incur this, which might be more
+ * than strictly needed.
+ */
+ private void update() {
+ width = calculateWidthForDigits(currentMaxDigits);
+ Dimension size = new Dimension(width, textPane.getHeight());
+ setPreferredSize(size);
+ setSize(size);
+ SwingUtilities.invokeLater(this::repaint);
+ }
+
+ // component listener events
+ @Override
+ public void componentResized(ComponentEvent e) {
+ update();
+ }
+
+ @Override
+ public void componentMoved(ComponentEvent e) {
+ update();
+ }
+
+ @Override
+ public void componentShown(ComponentEvent e) {
+ update();
+ }
+
+ @Override
+ public void componentHidden(ComponentEvent e) {
+ update();
+ }
+
+ // caret listener events
+ @Override
+ public void caretUpdate(CaretEvent e) {
+ update();
+ }
+
+ // document listener events
+ @Override
+ public void insertUpdate(DocumentEvent e) {
+ update();
+ }
+
+ @Override
+ public void removeUpdate(DocumentEvent e) {
+ update();
+ }
+
+ @Override
+ public void changedUpdate(DocumentEvent e) {
+ update();
+ }
+
+ /**
+ * Set whether this widget should display or not display line numbers,
+ * incur an update() call if there is a change.
+ * @param flag
+ */
+ public void setDisplay(boolean flag) {
+ boolean oldDisplay = display;
+ this.display = flag;
+ if ( this.display != oldDisplay ) {
+ update();
+ }
+ }
+
+ /**
+ * Set the fontName and fontSize for this widget. If the
+ * submitted name and size amount to a change of the font itself,
+ * incur an update() call.
+ * @param fontName
+ * @param fontSize
+ */
+ public void updateFontNameAndSize(String fontName, int fontSize) {
+ if ( fontSize < 1 ) {
+ if ( fontName == null || fontName.isEmpty() ) {
+ fontName = Font.MONOSPACED;
+ }
+ fontSize = 14;
+ }
+ String oldFontName = this.fontName;
+ int oldFontSize = this.fontSize;
+
+ this.fontName = fontName;
+ this.fontSize = fontSize;
+
+ if ( !this.fontName.equals(oldFontName) || this.fontSize != oldFontSize ) {
+ font = new Font(this.fontName, Font.PLAIN, this.fontSize);
+ descentAdjust = makeDescentAdjust();
+ update();
+ }
+ }
+
+
+}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurPDFWriter.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurPDFWriter.java
index deccdd9e6..de3961c66 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurPDFWriter.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurPDFWriter.java
@@ -226,7 +226,7 @@ public OurPDFWriter drawShape(Shape shape, boolean fillOrNot) {
* given matrix; for example, [1 0 0 1 dx dy] means "translation to dx dy" $R $G
* $B RG --> sets the stroke color (where 0 <= $R <= 1, etc) $R $G $B rg -->
* sets the fill color (where 0 <= $R <= 1, etc) Q --> restores the current
- * graphics state Page Object (3 because PAGE is #3) (4 beacuse PAGES is #4) (2
+ * graphics state Page Object (3 because PAGE is #3) (4 because PAGES is #4) (2
* because CONTENTS is #2)
* ========================================================= ================
* ============ 3 0 obj << /Type /Page /Parent 4 0 R /Contents 2 0 R >>
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxDocument.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxDocument.java
index eeb66807e..24fedaf94 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxDocument.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxDocument.java
@@ -577,7 +577,7 @@ else if (tabSize > 100)
}
/**
- * Overriden to return the full text of the document.
+ * Overridden to return the full text of the document.
*
* @return the entire text
*/
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxUndoableDocument.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxUndoableDocument.java
index 11ca13341..11227e6fe 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxUndoableDocument.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxUndoableDocument.java
@@ -60,7 +60,7 @@ final class OurSyntaxUndoableDocument extends OurSyntaxDocument {
private int now;
/**
- * The number of undoable opeartions that are currently "undone".
+ * The number of undoable operations that are currently "undone".
*/
private int undone;
@@ -219,7 +219,7 @@ public void replace(int offset, int length, String string, AttributeSet attrs) t
}
/**
- * Overriden to return the full text of the document.
+ * Overridden to return the full text of the document.
*
* @return the entire text
*/
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxWidget.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxWidget.java
index 002607726..2723bf9eb 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxWidget.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxWidget.java
@@ -120,11 +120,13 @@ public final class OurSyntaxWidget {
private volatile CompModule module;
+ private OurLineNumberWidget ourLineNumberWidget;
+
/**
* Constructs a syntax-highlighting widget.
*/
public OurSyntaxWidget(OurTabbedSyntaxWidget parent) {
- this(parent, true, "", "Monospaced", 14, 4, null, null);
+ this(parent, true, "", "Monospaced", 14, 4, false, null, null);
}
/**
@@ -133,7 +135,7 @@ public OurSyntaxWidget(OurTabbedSyntaxWidget parent) {
* @param parent
*/
@SuppressWarnings("serial" )
- public OurSyntaxWidget(OurTabbedSyntaxWidget parent, boolean enableSyntax, String text, String fontName, int fontSize, int tabSize, JComponent obj1, JComponent obj2) {
+ public OurSyntaxWidget(OurTabbedSyntaxWidget parent, boolean enableSyntax, String text, String fontName, int fontSize, int tabSize, boolean lineNumbers, JComponent obj1, JComponent obj2) {
pane.addKeyListener(new KeyListener() {
@Override
@@ -327,6 +329,9 @@ public void focusGained(FocusEvent e) {
component.setFocusable(false);
component.setMinimumSize(new Dimension(50, 50));
component.setViewportView(pane);
+
+ ourLineNumberWidget = OurLineNumberWidget.build(pane, component, lineNumbers, fontName, fontSize);
+
modified = false;
}
@@ -432,14 +437,14 @@ private void doComment() {
if (s != null && s.length() > 0) {
StringBuilder sb = new StringBuilder(s);
int i = 0;
- while (i < sb.length() - 1) {
+ while (i < sb.length()) {
if (sb.charAt(i) == '/' && sb.charAt(i + 1) == '/') {
sb.delete(i, i + 2);
} else {
sb.insert(i, "//");
i += 2;
}
- while (i < sb.length() - 1) {
+ while (i < sb.length()) {
if (sb.charAt(i) == '\n') {
i++;
break;
@@ -565,8 +570,10 @@ public boolean isFile() {
* Changes the font name, font size, and tab size for the document.
*/
void setFont(String fontName, int fontSize, int tabSize) {
- if (doc != null)
+ if (doc != null) {
doc.do_setFont(fontName, fontSize, tabSize);
+ ourLineNumberWidget.updateFontNameAndSize(fontName, fontSize);
+ }
}
/** Enables or disables syntax highlighting. */
@@ -575,6 +582,10 @@ void enableSyntax(boolean flag) {
doc.do_enableSyntax(flag);
}
+ void enableLineNumbers(boolean flag) {
+ ourLineNumberWidget.setDisplay(flag);
+ }
+
/**
* Return the number of lines represented by the current text (where partial
* line counts as a line).
@@ -865,4 +876,6 @@ public String getTooltip(MouseEvent event) {
}
return null;
}
+
+
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurTabbedSyntaxWidget.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurTabbedSyntaxWidget.java
index 5becd5587..b2cc396fd 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurTabbedSyntaxWidget.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurTabbedSyntaxWidget.java
@@ -85,6 +85,11 @@ public final class OurTabbedSyntaxWidget {
*/
private boolean syntaxHighlighting;
+ /**
+ * Whether line numbers are currently enable to displayr or not.
+ */
+ private boolean lineNumbers;
+
/** The list of clickable tabs. */
private final JPanel tabBar;
@@ -157,7 +162,7 @@ public Object do_action(Object sender, Event e, Object arg) {
private final JFrame parent;
/** Constructs a tabbed editor pane. */
- public OurTabbedSyntaxWidget(String fontName, int fontSize, int tabSize, JFrame parent) {
+ public OurTabbedSyntaxWidget(String fontName, int fontSize, int tabSize, boolean lineNumbers, JFrame parent) {
this.parent = parent;
component.setBorder(null);
component.setLayout(new BorderLayout());
@@ -174,6 +179,7 @@ public OurTabbedSyntaxWidget(String fontName, int fontSize, int tabSize, JFrame
tabBarScroller.setFocusable(false);
tabBarScroller.setBorder(null);
setFont(fontName, fontSize, tabSize);
+ this.lineNumbers = lineNumbers;
newtab(null);
tabBarScroller.addComponentListener(new ComponentListener() {
@@ -377,9 +383,18 @@ public void enableSyntax(boolean flag) {
t.enableSyntax(flag);
}
+ public void enableLineNumbers(boolean flag) {
+ lineNumbers = flag;
+ for ( OurSyntaxWidget t : tabs) {
+ t.enableLineNumbers(flag);
+ }
+ }
+
/** Returns the JTextArea of the current text buffer. */
public OurSyntaxWidget get() {
- return (me >= 0 && me < tabs.size()) ? tabs.get(me) : new OurSyntaxWidget(this);
+ return (me >= 0 && me < tabs.size()) ? tabs.get(me) :
+ new OurSyntaxWidget(this,
+ syntaxHighlighting, "", fontName, fontSize, tabSize, lineNumbers, null, null);
}
/**
@@ -438,7 +453,7 @@ public void mousePressed(MouseEvent e) {
JPanel pan = Util.onMac() ? OurUtil.makeVL(null, 2, OurUtil.makeHB(h1, lb, h2)) : OurUtil.makeVL(null, 2, OurUtil.makeHB(h1, lb, h2, GRAY), GRAY);
pan.setAlignmentX(0.0f);
pan.setAlignmentY(1.0f);
- OurSyntaxWidget text = new OurSyntaxWidget(this, syntaxHighlighting, "", fontName, fontSize, tabSize, lb, pan);
+ OurSyntaxWidget text = new OurSyntaxWidget(this, syntaxHighlighting, "", fontName, fontSize, tabSize, lineNumbers, lb, pan);
tabBar.add(pan, tabs.size());
tabs.add(text);
text.listeners.add(listener); // add listener AFTER we've updated
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Pos.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Pos.java
index a82798858..07e6b84fa 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Pos.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Pos.java
@@ -102,9 +102,9 @@ public Pos(String filename, int x, int y, int x2, int y2) {
* @param that - the other position object
*/
public Pos merge(Pos that) {
- if (that == null || that == UNKNOWN || that == this)
+ if (that == null || that.equals(UNKNOWN) || that == this)
return this;
- if (this == UNKNOWN)
+ if (this.equals(UNKNOWN))
return that;
int x = this.x, y = this.y, x2 = that.x2, y2 = that.y2;
if (that.y < y || (that.y == y && that.x < x)) {
@@ -178,6 +178,11 @@ public String toString() {
return "line " + y + ", column " + x + ", filename=" + filename;
}
+ public String toRangeString() {
+ String filePart = filename.length() == 0 ? "" : ", filename=" + filename;
+ return "line " + y + ", column " + x + " to line " + y2 + ", column " + x2 + filePart;
+ }
+
int start() {
return y * 500 + x;
}
@@ -194,6 +199,10 @@ public boolean contains(Pos pos) {
int anchor = pos.start();
int ourStart = start();
int ourEnd = end();
+
+ if(!filename.equals(pos.filename) && !"".equals(pos.filename))
+ return false;
+
if (ourStart > anchor)
return false;
@@ -308,4 +317,8 @@ public String substring(String text) {
public boolean sameFile(Pos pos) {
return this.filename.equals(pos.filename);
}
+
+ public Pos withFilename(String filename){
+ return new Pos(filename, x, y, x2, y2);
+ }
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Runner.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Runner.java
index 34aa02822..ed9f14c41 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Runner.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Runner.java
@@ -45,14 +45,14 @@ public abstract class Runner extends AbstractAction implements Runnable, WindowL
public Runner() {}
/**
- * This method should be overriden to provide the default action that this
+ * This method should be overridden to provide the default action that this
* Runner would perform.
*/
@Override
public abstract void run();
/**
- * This method should be overriden to provide the default action that this
+ * This method should be overridden to provide the default action that this
* Runner would perform given an argument.
*/
public abstract void run(Object arg);
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Util.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Util.java
index 191bd54be..47d0ce2bd 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Util.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Util.java
@@ -403,17 +403,17 @@ else if (b.equals("in"))
} else if (b.startsWith("this/")) {
return 1;
}
- int acount = 0, bcount = 0;
+ int account = 0, bcount = 0;
for (int i = 0; i < a.length(); i++) {
if (a.charAt(i) == '/')
- acount++;
+ account++;
}
for (int i = 0; i < b.length(); i++) {
if (b.charAt(i) == '/')
bcount++;
}
- if (acount != bcount)
- return (acount < bcount) ? -1 : 1;
+ if (account != bcount)
+ return (account < bcount) ? -1 : 1;
int result = a.compareToIgnoreCase(b);
return result != 0 ? result : a.compareTo(b);
}
@@ -821,7 +821,7 @@ public static int min(int bitwidth) {
/**
* Returns a mask of the form 000..0011..11 where the number of 1s is equal to
- * the number of significant bits of the highest integer withing the given
+ * the number of significant bits of the highest integer within the given
* bitwidth
*/
public static int shiftmask(int bitwidth) {
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Assert.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Assert.java
new file mode 100644
index 000000000..a7431265e
--- /dev/null
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Assert.java
@@ -0,0 +1,64 @@
+package edu.mit.csail.sdg.ast;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.List;
+
+import edu.mit.csail.sdg.alloy4.Err;
+import edu.mit.csail.sdg.alloy4.ErrorWarning;
+import edu.mit.csail.sdg.alloy4.Pos;
+
+public final class Assert extends Expr implements Clause {
+ public final Expr expr;
+ public final Pos labelPos;
+ public final String label;
+
+ public Assert(Pos pos, Pos labelPos, String label, Expr expr) {
+ super(pos, Type.FORMULA);
+ this.expr = expr;
+ this.labelPos = labelPos;
+ this.label = label;
+ }
+
+ @Override
+ public String explain() {
+ return "assert " + label;
+ }
+
+ @Override
+ public void toString(StringBuilder out, int indent) {
+ if (indent < 0) {
+ out.append(label);
+ } else {
+ for (int i = 0; i < indent; i++) {
+ out.append(' ');
+ }
+ out.append( "assert ").append(label).append('\n');
+ }
+ }
+
+ @Override
+ public T accept(VisitReturn visitor) throws Err {
+ return visitor.visit(this);
+ }
+
+ @Override
+ public Expr resolve(Type t, Collection warnings) {
+ return this;
+ }
+
+ @Override
+ public int getDepth() {
+ return 1;
+ }
+
+ @Override
+ public String getHTML() {
+ return "assert " + label;
+ }
+
+ @Override
+ public List< ? extends Browsable> getSubnodes() {
+ return Arrays.asList(expr);
+ }
+}
\ No newline at end of file
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Clause.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Clause.java
index 10d951644..8a05d182d 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Clause.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Clause.java
@@ -4,7 +4,7 @@
/**
* Unfortunately not all objects are Expr. However, from the UI we want to be
- * able to locae the clauses in the text file and what they refer to.
+ * able to locate the clauses in the text file and what they refer to.
*
* @author aqute
*
@@ -22,4 +22,25 @@ public interface Clause {
* @return a string formatted like a set
*/
String explain();
+
+ public final class Custom implements Clause{
+ final Pos pos;
+ final String explanation;
+
+ public Custom(Pos pos, String explanation) {
+ this.pos = pos;
+ this.explanation = explanation;
+ }
+
+ @Override
+ public Pos pos() {
+ return pos;
+ }
+
+ @Override
+ public String explain() {
+ return explanation;
+ }
+
+ }
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java
index 3e39158fc..033057377 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Command.java
@@ -125,6 +125,11 @@ public final class Command extends Browsable {
public final Expr nameExpr;
+ /**
+ * The 'check' or 'run' keyword
+ */
+ public final ExprVar commandKeyword;
+
/**
* Returns a human-readable string that summarizes this Run or Check command.
*/
@@ -170,6 +175,27 @@ else if (bitwidth >= 0 || maxseq >= 0 || scope.size() > 0 || minprefix >= 0 || m
return sb.toString();
}
+ /**
+ * Constructs a new Command object.
+ *
+ * @param check - true if this is a "check"; false if this is a "run"
+ * @param overall - the overall scope (0 or higher) (-1 if no overall scope was
+ * specified)
+ * @param bitwidth - the integer bitwidth (0 or higher) (-1 if it was not
+ * specified)
+ * @param maxseq - the maximum sequence length (0 or higher) (-1 if it was not
+ * specified)
+ * @param mintime - the minimal trace length (0 or higher) (-1 if it was not
+ * specified)
+ * @param maxtime - the maximal trace length (0 or higher) (-1 if it was not
+ * specified)
+ * @param formula - the formula that must be satisfied by this command
+ */
+ //extended with time scopes
+ public Command(boolean check, int overall, int bitwidth, int maxseq, int mintime, int maxtime, ExprVar commandKeyword, Expr formula) throws ErrorSyntax {
+ this(null, null, "", check, overall, bitwidth, maxseq, mintime, maxtime, -1, null, null, commandKeyword, formula, null);
+ }
+
/**
* Constructs a new Command object.
*
@@ -182,8 +208,8 @@ else if (bitwidth >= 0 || maxseq >= 0 || scope.size() > 0 || minprefix >= 0 || m
* specified)
* @param formula - the formula that must be satisfied by this command
*/
- public Command(boolean check, int overall, int bitwidth, int maxseq, Expr formula) throws ErrorSyntax {
- this(null, null, "", check, overall, bitwidth, maxseq, -1, -1, -1, null, null, formula, null);
+ public Command(boolean check, int overall, int bitwidth, int maxseq, ExprVar commandKeyword, Expr formula) throws ErrorSyntax {
+ this(null, null, "", check, overall, bitwidth, maxseq, -1, -1, -1, null, null, commandKeyword, formula, null);
}
/**
@@ -210,10 +236,11 @@ public Command(boolean check, int overall, int bitwidth, int maxseq, Expr formul
* exact though we may or may not know what the scope is yet
* @param formula - the formula that must be satisfied by this command
*/
- public Command(Pos pos, Expr e, String label, boolean check, int overall, int bitwidth, int maxseq, int minprefix, int maxprefix, int expects, Iterable scope, Iterable additionalExactSig, Expr formula, Command parent) {
+ public Command(Pos pos, Expr e, String label, boolean check, int overall, int bitwidth, int maxseq, int minprefix, int maxprefix, int expects, Iterable scope, Iterable additionalExactSig, ExprVar commandKeyword, Expr formula, Command parent) {
if (pos == null)
pos = Pos.UNKNOWN;
this.nameExpr = e;
+ this.commandKeyword = commandKeyword;
this.formula = formula;
this.pos = pos;
this.label = (label == null ? "" : label);
@@ -234,24 +261,27 @@ public Command(Pos pos, Expr e, String label, boolean check, int overall, int bi
* Constructs a new Command object where it is the same as the current object,
* except with a different formula.
*/
+ //extended with time scopes
public Command change(Expr newFormula) {
- return new Command(pos, nameExpr, label, check, overall, bitwidth, maxseq, minprefix, maxprefix, expects, scope, additionalExactScopes, newFormula, parent);
+ return new Command(pos, nameExpr, label, check, overall, bitwidth, maxseq, minprefix, maxprefix, expects, scope, additionalExactScopes, commandKeyword, newFormula, parent);
}
/**
* Constructs a new Command object where it is the same as the current object,
* except with a different scope.
*/
+ //extended with time scopes
public Command change(ConstList scope) {
- return new Command(pos, nameExpr, label, check, overall, bitwidth, maxseq, minprefix, maxprefix, expects, scope, additionalExactScopes, formula, parent);
+ return new Command(pos, nameExpr, label, check, overall, bitwidth, maxseq, minprefix, maxprefix, expects, scope, additionalExactScopes, commandKeyword, formula, parent);
}
/**
* Constructs a new Command object where it is the same as the current object,
* except with a different list of "additional exact sigs".
*/
+ //extended with time scopes
public Command change(Sig... additionalExactScopes) {
- return new Command(pos, nameExpr, label, check, overall, bitwidth, maxseq, minprefix, maxprefix, expects, scope, Util.asList(additionalExactScopes), formula, parent);
+ return new Command(pos, nameExpr, label, check, overall, bitwidth, maxseq, minprefix, maxprefix, expects, scope, Util.asList(additionalExactScopes), commandKeyword, formula, parent);
}
/**
@@ -269,10 +299,10 @@ public Command change(Sig sig, boolean isExact, int newScope) throws ErrorSyntax
public Command change(Sig sig, boolean isExact, int startingScope, int endingScope, int increment) throws ErrorSyntax {
for (int i = 0; i < scope.size(); i++)
if (scope.get(i).sig == sig) {
- CommandScope sc = new CommandScope(scope.get(i).pos, sig, isExact, startingScope, endingScope, increment);
+ CommandScope sc = new CommandScope(scope.get(i).pos, scope.get(i).sigPos, sig, isExact, startingScope, endingScope, increment);
return change(new TempList(scope).set(i, sc).makeConst());
}
- CommandScope sc = new CommandScope(Pos.UNKNOWN, sig, isExact, startingScope, endingScope, increment);
+ CommandScope sc = new CommandScope(Pos.UNKNOWN, Pos.UNKNOWN, sig, isExact, startingScope, endingScope, increment);
return change(Util.append(scope, sc));
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/CommandScope.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/CommandScope.java
index 357be5bfb..408f88b82 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/CommandScope.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/CommandScope.java
@@ -37,6 +37,10 @@ public class CommandScope {
*/
public final Pos pos;
+ /**
+ * The position of the sig reference
+ */
+ public final Pos sigPos;
/**
* The sig whose scope is being given by this CommandScope object.
*/
@@ -69,7 +73,7 @@ public class CommandScope {
* @throws ErrorSyntax if scope is less than zero
*/
public CommandScope(Sig sig, boolean isExact, int scope) throws ErrorSyntax {
- this(null, sig, isExact, scope, scope, 1);
+ this(null, null, sig, isExact, scope, scope, 1);
}
/**
@@ -87,7 +91,7 @@ public CommandScope(Sig sig, boolean isExact, int scope) throws ErrorSyntax {
* @throws ErrorSyntax if endingScope is less than startingScope
* @throws ErrorSyntax if increment is less than one
*/
- public CommandScope(Pos pos, Sig sig, boolean isExact, int startingScope, int endingScope, int increment) throws ErrorSyntax {
+ public CommandScope(Pos pos, Pos sigPos, Sig sig, boolean isExact, int startingScope, int endingScope, int increment) throws ErrorSyntax {
if (pos == null)
pos = Pos.UNKNOWN;
if (sig == null)
@@ -104,12 +108,18 @@ public CommandScope(Pos pos, Sig sig, boolean isExact, int startingScope, int en
throw new ErrorSyntax(pos, "Sig " + sig + "'s increment value cannot be " + increment + ".\nThe increment must be 1 or greater.");
this.pos = pos;
this.sig = sig;
+ this.sigPos = sigPos;
this.isExact = isExact;
this.startingScope = startingScope;
this.endingScope = endingScope;
this.increment = increment;
}
+ Expr sigRef = null;
+ public Expr sigRef(){
+ if(sigRef == null) sigRef = ExprUnary.Op.NOOP.make(sigPos, sig, null, 0);
+ return sigRef;
+ }
/** {@inheritDoc} */
@Override
public String toString() {
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Decl.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Decl.java
index 37c5b1d32..544a0148c 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Decl.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Decl.java
@@ -29,7 +29,7 @@
* variable).
*/
-public final class Decl {
+public class Decl {
/**
* If nonnull, then this decl is private (and this.isPrivate is the location of
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java
index 336c82466..2feb1531e 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java
@@ -125,7 +125,7 @@ public final Type type() {
* @param errors - the list of errors associated with this Expr node (can be
* null if there are none)
*/
- Expr(Pos pos, Pos closingBracket, boolean ambiguous, Type type, int mult, long weight, JoinableList errors) {
+ public Expr(Pos pos, Pos closingBracket, boolean ambiguous, Type type, int mult, long weight, JoinableList errors) {
this.pos = (pos == null ? Pos.UNKNOWN : pos);
this.closingBracket = (closingBracket == null ? Pos.UNKNOWN : closingBracket);
this.ambiguous = ambiguous;
@@ -140,7 +140,7 @@ public final Type type() {
}
/** This must only be called by Sig's constructor. */
- Expr(Pos pos, Type type) {
+ public Expr(Pos pos, Type type) {
this.closingBracket = Pos.UNKNOWN;
this.ambiguous = false;
this.errors = emptyListOfErrors;
@@ -240,7 +240,7 @@ public final Expr typecheck_as_set() {
/**
* Resolves this expression if ambiguous. (And if t.size()>0, it represents the
- * set of tuples whose presence/absence is relevent to the parent expression)
+ * set of tuples whose presence/absence is relevant to the parent expression)
* (Note: it's possible for t to be EMPTY, or even ambiguous!)
*
* On success: the return value will be well-typed and unambiguous
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprCall.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprCall.java
index 14c421bde..fc33446ca 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprCall.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprCall.java
@@ -31,6 +31,7 @@
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.ast.Sig.Field;
+import edu.mit.csail.sdg.parser.Macro;
/**
* Immutable; represents a call.
@@ -266,6 +267,21 @@ public Type visit(Sig x) {
return x.type;
}
+ @Override
+ public Type visit(Func x) throws Err {
+ return x.type;
+ }
+
+ @Override
+ public Type visit(Assert x) throws Err {
+ return x.type;
+ }
+
+ @Override
+ public Type visit(Macro x) throws Err {
+ return x.type();
+ }
+
@Override
public Type visit(Field x) {
return x.type;
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprList.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprList.java
index 52ddfaa80..8bb6c5b93 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprList.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprList.java
@@ -32,7 +32,7 @@
/**
* Immutable; represents disjoint[] or pred/totalOrder[] or (... and ... and ..)
- * and other similar list of arugments.
+ * and other similar list of arguments.
*
* Invariant: type!=EMPTY => (all x:args | x.mult==0)
*/
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java
index 6518c9d30..c8a4d3e0e 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Func.java
@@ -18,13 +18,16 @@
import static edu.mit.csail.sdg.alloy4.TableView.clean;
import java.util.ArrayList;
+import java.util.Collection;
import java.util.List;
import java.util.NoSuchElementException;
+import java.util.stream.Collectors;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorSyntax;
import edu.mit.csail.sdg.alloy4.ErrorType;
+import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Util;
@@ -40,7 +43,7 @@
* predicate/function call
*/
-public final class Func extends Browsable implements Clause {
+public final class Func extends Expr implements Clause {
/**
* The location in the original file where this predicate/function is declared;
@@ -59,6 +62,11 @@ public final class Func extends Browsable implements Clause {
*/
public final String label;
+ /**
+ * The position of the label
+ */
+ public final Pos labelPos;
+
/**
* True if this is a predicate; false if this is a function.
*/
@@ -133,8 +141,8 @@ public List params() {
* @throws ErrorSyntax if this function's return type declaration contains a
* predicate/function call
*/
- public Func(Pos pos, String label, List decls, Expr returnDecl, Expr body) throws Err {
- this(pos, null, label, decls, returnDecl, body);
+ public Func(Pos pos, Pos labelPos, String label, List decls, Expr returnDecl, Expr body) throws Err {
+ this(pos, null, labelPos, label, decls, returnDecl, body);
}
/**
@@ -167,12 +175,14 @@ public Func(Pos pos, String label, List decls, Expr returnDecl, Expr body)
* @throws ErrorSyntax if this function's return type declaration contains a
* predicate/function call
*/
- public Func(Pos pos, Pos isPrivate, String label, List decls, Expr returnDecl, Expr body) throws Err {
+ public Func(Pos pos, Pos isPrivate, Pos labelPos, String label, List decls, Expr returnDecl, Expr body) throws Err {
+ super(pos, Type.FORMULA);
if (pos == null)
pos = Pos.UNKNOWN;
this.pos = pos;
this.isPrivate = isPrivate;
this.label = (label == null ? "" : label);
+ this.labelPos = labelPos;
this.isPred = (returnDecl == null);
if (returnDecl == null)
returnDecl = ExprConstant.FALSE;
@@ -252,12 +262,6 @@ public final String toString() {
return (isPred ? "pred " : "fun ") + label;
}
- /** {@inheritDoc} */
- @Override
- public final Pos pos() {
- return pos;
- }
-
/** {@inheritDoc} */
@Override
public final Pos span() {
@@ -270,6 +274,12 @@ public String getHTML() {
return (isPred ? "pred " : "fun ") + label;
}
+ ExprVar labelExpr = null;
+ public Expr labelExpr(){
+ if(labelExpr == null)
+ labelExpr = ExprVar.make(labelPos, label);
+ return labelExpr;
+ }
/** {@inheritDoc} */
@Override
public List< ? extends Browsable> getSubnodes() {
@@ -284,8 +294,7 @@ public String getHTML() {
return ans;
}
- @Override
- public String explain() {
+ public String explainOld() {
if (clean(label).contains("run$")) {
return null;
}
@@ -324,4 +333,54 @@ public String explain() {
return sb.toString();
}
+ @Override
+ public String explain() {
+ StringBuilder sb = new StringBuilder();
+ if (isPred)
+ sb.append("pred ");
+ else
+ sb.append("fun ");
+
+ sb.append(clean(label));
+
+ if (decls.size() > 0 ) {
+ sb.append(" [\n");
+ sb.append(decls.stream()
+ .flatMap(decl -> decl.names.stream().map(e -> " " + e + " : " + decl.expr.type))
+ .collect(Collectors.joining(",\n")));
+ sb.append("\n]");
+ }
+ if (!isPred) {
+ sb.append(" ⟶ ").append(returnDecl.type.toString());
+ }
+ return sb.toString();
+ }
+
+ @Override
+ public void toString(StringBuilder out, int indent) {
+ if (indent < 0) {
+ out.append("(").append(label).append(" <: ").append(label).append(")");
+ } else {
+ for (int i = 0; i < indent; i++) {
+ out.append(' ');
+ }
+ out.append( isPred? "pred " : "field ").append(label).append('\n');
+ }
+ }
+
+ @Override
+ public T accept(VisitReturn visitor) throws Err {
+ return visitor.visit(this);
+ }
+
+ @Override
+ public Expr resolve(Type t, Collection warnings) {
+ return this;
+ }
+
+ @Override
+ public int getDepth() {
+ return 1;
+ }
+
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Module.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Module.java
index 07d768156..85f5b785e 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Module.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Module.java
@@ -79,7 +79,7 @@ public interface Module extends Clause {
/**
* Return an unmodifiable list of all assertions in this module.
*/
- public ConstList> getAllAssertions();
+ public ConstList getAllAssertions();
/**
* Return an unmodifiable list of all facts in this module.
@@ -110,7 +110,7 @@ public interface Module extends Clause {
public JFrame showAsTree(Listener listener);
/**
- * Parse one expression by starting fromt this module as the root module.
+ * Parse one expression by starting from this module as the root module.
*/
public Expr parseOneExpressionFromString(String input) throws Err, FileNotFoundException, IOException;
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java
index 211040e65..e422f8752 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Sig.java
@@ -20,6 +20,8 @@
import java.util.Arrays;
import java.util.Collection;
import java.util.List;
+import java.util.stream.Collectors;
+import java.util.stream.StreamSupport;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.ConstList.TempList;
@@ -33,6 +35,7 @@
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.alloy4.Version;
import edu.mit.csail.sdg.ast.Attr.AttrType;
+import org.alloytools.util.table.Table;
/**
* Mutable; represents a signature.
@@ -45,26 +48,26 @@
public abstract class Sig extends Expr implements Clause {
/** The built-in "univ" signature. */
- public static final PrimSig UNIV = new PrimSig("univ", null, true, false);
+ public static final PrimSig UNIV = new PrimSig("univ", null, null, false, false);
/** The built-in "Int" signature. */
- public static final PrimSig SIGINT = new PrimSig("Int", UNIV, false, false);
+ public static final PrimSig SIGINT = new PrimSig("Int", Pos.UNKNOWN, UNIV, false, false);
/** The built-in "seq/Int" signature. */
- public static final PrimSig SEQIDX = new PrimSig("seq/Int", SIGINT, false, true);
+ public static final PrimSig SEQIDX = new PrimSig("seq/Int", Pos.UNKNOWN, SIGINT, false, true);
/** The built-in "String" signature. */
- public static final PrimSig STRING = new PrimSig("String", UNIV, false, true);
+ public static final PrimSig STRING = new PrimSig("String", Pos.UNKNOWN, UNIV, false, true);
/** The built-in "none" signature. */
- public static final PrimSig NONE = new PrimSig("none", null, false, false);
+ public static final PrimSig NONE = new PrimSig("none", null, null, false, false);
/** The built-in "none" signature. */
public static final PrimSig GHOST = mkGhostSig();
private static final PrimSig mkGhostSig() {
try {
- return new PrimSig("Univ", null, new Attr[0]);
+ return new PrimSig(null, "Univ", null, null, new Attr[0]);
} catch (Err e) {
return null; // never happens
}
@@ -226,6 +229,11 @@ public final T accept(VisitReturn visitor) throws Err {
*/
public final Pos isVariable;
+ /**
+ * The position of the sig label
+ */
+ public final Pos labelPos;
+
/**
* The label for this sig; this name does not need to be unique.
*/
@@ -268,11 +276,12 @@ private Sig(String label, boolean var) {
this.isMeta = null;
this.isEnum = null;
this.isVariable = var ? Pos.UNKNOWN : null;
+ this.labelPos = null;
this.attributes = ConstList.make();
}
/** Constructs a new PrimSig or SubsetSig. */
- private Sig(Type type, String label, Attr... attributes) throws Err {
+ private Sig(Type type, Pos labelPos, String label, Attr... attributes) throws Err {
super(AttrType.WHERE.find(attributes), type);
this.attributes = Util.asList(attributes);
Expr oneof = ExprUnary.Op.ONEOF.make(null, this);
@@ -328,6 +337,7 @@ private Sig(Type type, String label, Attr... attributes) throws Err {
this.isVariable = isVariable;
this.label = label;
this.builtin = false;
+ this.labelPos = labelPos;
if (isLone != null && isOne != null)
throw new ErrorSyntax(isLone.merge(isOne), "You cannot declare a sig to be both lone and one.");
if (isLone != null && isSome != null)
@@ -359,6 +369,13 @@ public boolean isSame(Expr obj) {
/** Returns true iff "this is equal or subtype of that" */
public abstract boolean isSameOrDescendentOf(Sig that);
+ public boolean isEnumMember() {
+ if (this instanceof PrimSig) {
+ PrimSig _this = (PrimSig) this;
+ return _this.parent.isEnum != null;
+ } else
+ return false;
+ }
/** {@inheritDoc} */
@Override
public int getDepth() {
@@ -469,10 +486,27 @@ public Iterable descendents() throws Err {
*/
public final PrimSig parent;
+ /**
+ * The position of the reference to the parent Sig.
+ * Can be null only if parent is null
+ */
+ public final Pos parentRefPos;
+
+
+ private Expr parentRef;
+ public Expr parentRef(){
+ if(parentRef == null ){
+ parentRef = ExprUnary.Op.NOOP.make(parentRefPos , parent );
+ }
+ return parentRef;
+ }
+
/** Constructs a builtin PrimSig. */
- private PrimSig(String label, PrimSig parent, boolean var, boolean add) {
+ private PrimSig(String label, Pos parentRefPos, PrimSig parent, boolean var, boolean add) {
super(label, var);
this.parent = parent;
+ assert parent == null ? parentRefPos == null : parentRefPos != null;
+ this.parentRefPos = parentRefPos ;
if (add)
this.parent.children.add(this);
}
@@ -488,8 +522,10 @@ private PrimSig(String label, PrimSig parent, boolean var, boolean add) {
* @throws ErrorType if you attempt to extend the builtin sigs NONE, SIGINT,
* SEQIDX, or STRING
*/
- public PrimSig(String label, PrimSig parent, Attr... attributes) throws Err {
- super(((parent != null && parent.isEnum != null) ? parent.type : null), label, Util.append(attributes, Attr.SUBSIG));
+ public PrimSig(Pos labelPos, String label, Pos parentRefPos, PrimSig parent, Attr... attributes) throws Err {
+ super(((parent != null && parent.isEnum != null) ? parent.type : null), labelPos, label, Util.append(attributes, Attr.SUBSIG));
+ assert parent == null ? parentRefPos == null : parentRefPos != null;
+
if (parent == SIGINT)
throw new ErrorSyntax(pos, "sig " + label + " cannot extend the builtin \"Int\" signature");
if (parent == SEQIDX)
@@ -503,6 +539,8 @@ public PrimSig(String label, PrimSig parent, Attr... attributes) throws Err {
else if (parent != UNIV)
parent.children.add(this);
this.parent = parent;
+ this.parentRefPos = parentRefPos;
+
if (isEnum != null && parent != UNIV)
throw new ErrorType(pos, "sig " + label + " is not a toplevel sig, so it cannot be an enum.");
for (; parent != null; parent = parent.parent)
@@ -523,7 +561,7 @@ else if (parent != UNIV)
* @throws ErrorSyntax if the signature has two or more multiplicities
*/
public PrimSig(String label, Attr... attributes) throws Err {
- this(label, null, attributes);
+ this(null, label, null, null, attributes);
}
/** {@inheritDoc} */
@@ -611,6 +649,23 @@ private static Type getType(String label, Iterable parents) throws Err {
return (ans != null) ? ans : (UNIV.type);
}
+ /**
+ * The positions of references to parent Sigs (in parents field).
+ * Could be null
+ */
+ public final ConstList parentRefPoss;
+
+ private ConstList parentRefs;
+ public ConstList parentRefs(){
+ if(parentRefs == null){
+ TempList res = new TempList<>();
+ for(int i = 0; i < parents.size(); i++){
+ res.add(ExprUnary.Op.NOOP.make(parentRefPoss != null ? parentRefPoss.get(i) : Pos.UNKNOWN, parents.get(i) ));
+ }
+ parentRefs = res.makeConst();
+ }
+ return parentRefs;
+ }
/**
* Constructs a subset sig.
*
@@ -622,8 +677,8 @@ private static Type getType(String label, Iterable parents) throws Err {
* @throws ErrorSyntax if the signature has two or more multiplicities
* @throws ErrorType if parents only contains NONE
*/
- public SubsetSig(String label, Collection parents, Attr... attributes) throws Err {
- super(getType(label, parents), label, Util.append(attributes, Attr.SUBSET));
+ public SubsetSig(Pos labelPos, String label, Collection parentRefPoss, Collection parents, Attr... attributes) throws Err {
+ super(getType(label, parents), labelPos, label, Util.append(attributes, Attr.SUBSET));
if (isEnum != null)
throw new ErrorType(pos, "Subset signature cannot be an enum.");
boolean exact = false;
@@ -656,6 +711,7 @@ public SubsetSig(String label, Collection parents, Attr... attributes) thro
if (temp.size() == 0)
throw new ErrorType(pos, "Sig " + label + " must have at least one non-empty parent.");
this.parents = temp.makeConst();
+ this.parentRefPoss = parentRefPoss != null ? new TempList(parentRefPoss).makeConst() : null;
}
/** {@inheritDoc} */
@@ -696,13 +752,15 @@ public static final class Field extends ExprHasName implements Clause {
/** The declaration that this field came from. */
private Decl decl;
+ public final Pos labelPos;
+
/** Return the declaration that this field came from. */
public Decl decl() {
return decl;
}
/** Constructs a new Field object. */
- private Field(Pos pos, Pos isPrivate, Pos isMeta, Pos disjoint, Pos disjoint2, Pos isVar, Sig sig, String label, Expr bound) throws Err {
+ private Field(Pos pos, Pos isPrivate, Pos isMeta, Pos disjoint, Pos disjoint2, Pos isVar, Sig sig, Pos labelPos, String label, Expr bound) throws Err {
super(pos, label, sig.type.product(bound.type));
this.defined = bound.mult() == ExprUnary.Op.EXACTLYOF;
if (sig.builtin)
@@ -717,6 +775,7 @@ private Field(Pos pos, Pos isPrivate, Pos isMeta, Pos disjoint, Pos disjoint2, P
this.isMeta = (isMeta != null ? isMeta : sig.isMeta);
this.isVariable = isVar;
this.sig = sig;
+ this.labelPos = labelPos;
}
/**
@@ -837,7 +896,7 @@ public final Field addField(String label, Expr bound) throws Err {
// multiplicity
// symbol, we assume
// it's oneOf
- final Field f = new Field(null, null, null, null, null, null, this, label, bound);
+ final Field f = new Field(null, null, null, null, null, null, this, null, label, bound);
final Decl d = new Decl(null, null, null, null, Arrays.asList(f), bound);
f.decl = d;
fields.add(d);
@@ -867,7 +926,7 @@ public final Field addField(String label, Expr bound) throws Err {
* @throws ErrorType if the bound is not fully typechecked or is not a
* set/relation
*/
- public final Field[] addTrickyField(Pos pos, Pos isPrivate, Pos isDisjoint, Pos isDisjoint2, Pos isMeta, Pos isVar, String[] labels, Expr bound) throws Err {
+ public final Field[] addTrickyField(Pos pos, Pos isPrivate, Pos isDisjoint, Pos isDisjoint2, Pos isMeta, Pos isVar, List extends ExprHasName> labels, Expr bound) throws Err {
bound = bound.typecheck_as_set();
if (bound.ambiguous)
bound = bound.resolve_as_set(null);
@@ -876,9 +935,9 @@ public final Field[] addTrickyField(Pos pos, Pos isPrivate, Pos isDisjoint, Pos
// multiplicity
// symbol, we assume
// it's oneOf
- final Field[] f = new Field[labels.length];
+ final Field[] f = new Field[labels.size()];
for (int i = 0; i < f.length; i++)
- f[i] = new Field(pos, isPrivate, isMeta, isDisjoint, isDisjoint2, isVar, this, labels[i], bound);
+ f[i] = new Field(pos, isPrivate, isMeta, isDisjoint, isDisjoint2, isVar, this, labels.get(i).pos, labels.get(i).label, bound);
final Decl d = new Decl(isPrivate, isDisjoint, isDisjoint2, isVar, Arrays.asList(f), bound);
for (int i = 0; i < f.length; i++) {
f[i].decl = d;
@@ -917,7 +976,7 @@ public final Field addDefinedField(Pos pos, Pos isPrivate, Pos isMeta, String la
bound = bound.resolve_as_set(null);
if (bound.mult() != ExprUnary.Op.EXACTLYOF)
bound = ExprUnary.Op.EXACTLYOF.make(null, bound);
- final Field f = new Field(pos, isPrivate, isMeta, null, null, null, this, label, bound);
+ final Field f = new Field(pos, isPrivate, isMeta, null, null, null, this, null, label, bound);
final Decl d = new Decl(null, null, null, null, Arrays.asList(f), bound);
f.decl = d;
fields.add(d);
@@ -925,8 +984,10 @@ public final Field addDefinedField(Pos pos, Pos isPrivate, Pos isMeta, String la
return f;
}
- @Override
- public String explain() {
+ // TODO remove at some point
+ public String explainOld() {
+ Table t = new Table(2, 1 + realFields.size(), 1);
+
StringBuilder sb = new StringBuilder();
if (builtin)
sb.append("builtin ");
@@ -956,6 +1017,44 @@ public String explain() {
}
sb.append(" }");
+ //return sb.toString();
+
+ return t.transpose(0).toString();
+ }
+
+ @Override
+ public String explain() {
+ StringBuilder sb = new StringBuilder();
+ if (builtin)
+ sb.append("builtin ");
+ if (isEnum != null)
+ sb.append("enum ");
+ if (isAbstract != null)
+ sb.append("abstract ");
+ if (isLone != null)
+ sb.append("lone ");
+ if (isOne != null)
+ sb.append("one ");
+ if (isMeta != null)
+ sb.append("meta ");
+ if (isSome != null)
+ sb.append("some ");
+ if (isSubsig != null)
+ sb.append("sig ");
+ if (isSubset != null)
+ sb.append("subset ");
+
+ sb.append(clean(label));
+ if(! realFields.isEmpty()){
+ sb.append(" {\n");
+
+ sb.append(StreamSupport.stream(realFields.spliterator(), false)
+ .map(f -> " " + clean(f.label) + " : " +
+ clean(type.join(f.type).toString()))
+ .collect(Collectors.joining(",\n")));
+
+ sb.append("\n}");
+ }
return sb.toString();
}
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java
index 5b91dfb86..f692968b8 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQuery.java
@@ -17,6 +17,7 @@
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.ast.Sig.Field;
+import edu.mit.csail.sdg.parser.Macro;
/**
* This abstract class implements a Query visitor that walks over an Expr and
@@ -149,6 +150,21 @@ public T visit(Sig x) throws Err {
return null;
}
+ @Override
+ public T visit(Func x) throws Err {
+ return null;
+ }
+
+ @Override
+ public T visit(Assert x) throws Err {
+ return null;
+ }
+
+ @Override
+ public T visit(Macro x) throws Err {
+ return null;
+ }
+
/**
* Visits a Field node (this default implementation simply returns null)
*/
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java
index e6a03242c..f51104442 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitQueryOnce.java
@@ -4,6 +4,7 @@
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.ast.Sig.Field;
+import edu.mit.csail.sdg.parser.Macro;
/**
* Acts like VisitQuery but never traverses a node more than once.
@@ -144,4 +145,27 @@ protected boolean visited(Expr x) {
return visited.put(x, x) != null;
}
+ @Override
+ public T visit(Func x) throws Err {
+ if (visited(x))
+ return null;
+ else
+ return super.visit(x);
+ }
+
+ @Override
+ public T visit(Assert x) throws Err {
+ if (visited(x))
+ return null;
+ else
+ return super.visit(x);
+ }
+
+ @Override
+ public T visit(Macro x) throws Err {
+ if (visited(x))
+ return null;
+ else
+ return super.visit(x);
+ }
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitReturn.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitReturn.java
index 626e5ea87..c78f58890 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitReturn.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/VisitReturn.java
@@ -17,6 +17,7 @@
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.ast.Sig.Field;
+import edu.mit.csail.sdg.parser.Macro;
/**
* This abstract class defines what a Return Visitor's interface needs to be.
@@ -81,4 +82,13 @@ public T visit(ExprBadJoin x) throws Err {
/** Visits a Field node. */
public abstract T visit(Field x) throws Err;
+
+ /** Visits a Func node. */
+ public abstract T visit(Func x) throws Err;
+
+ /** Visists an Assert node. */
+ public abstract T visit(Assert x) throws Err;
+
+ /** Visits a Macro node. */
+ public abstract T visit(Macro macro) throws Err;
}
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompFilter.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompFilter.java
index 44e1491df..cfbab9411 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompFilter.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompFilter.java
@@ -27,7 +27,6 @@
import static edu.mit.csail.sdg.parser.CompSym.DISJ;
import static edu.mit.csail.sdg.parser.CompSym.EOF;
import static edu.mit.csail.sdg.parser.CompSym.EQUALS;
-import static edu.mit.csail.sdg.parser.CompSym.EXH;
import static edu.mit.csail.sdg.parser.CompSym.FUN;
import static edu.mit.csail.sdg.parser.CompSym.GT;
import static edu.mit.csail.sdg.parser.CompSym.GTE;
@@ -70,7 +69,6 @@
import static edu.mit.csail.sdg.parser.CompSym.ONE_ARROW_LONE;
import static edu.mit.csail.sdg.parser.CompSym.ONE_ARROW_ONE;
import static edu.mit.csail.sdg.parser.CompSym.ONE_ARROW_SOME;
-import static edu.mit.csail.sdg.parser.CompSym.PART;
import static edu.mit.csail.sdg.parser.CompSym.PRED;
import static edu.mit.csail.sdg.parser.CompSym.PRIVATE;
import static edu.mit.csail.sdg.parser.CompSym.RBRACE;
@@ -191,7 +189,7 @@ else if (a.sym == SOME)
temp.add(b = myread());
if (b.sym == PRIVATE)
temp.add(b = myread());
- if (b.sym == DISJ || b.sym == PART || b.sym == EXH)
+ if (b.sym == DISJ)
temp.add(b = myread());
while (b.sym == ID) {
temp.add(b = myread());
diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java
index 7fff7c4e0..adfea63e3 100644
--- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java
+++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java
@@ -40,6 +40,7 @@
import java.util.List;
import java.util.Map;
import java.util.Set;
+import java.util.stream.Collectors;
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.ConstList;
@@ -56,6 +57,7 @@
import edu.mit.csail.sdg.alloy4.SafeList;
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.alloy4.Version;
+import edu.mit.csail.sdg.ast.Assert;
import edu.mit.csail.sdg.ast.Attr;
import edu.mit.csail.sdg.ast.Browsable;
import edu.mit.csail.sdg.ast.Clause;
@@ -76,6 +78,7 @@
import edu.mit.csail.sdg.ast.ExprList;
import edu.mit.csail.sdg.ast.ExprQt;
import edu.mit.csail.sdg.ast.ExprUnary;
+import edu.mit.csail.sdg.ast.ExprUnary.Op;
import edu.mit.csail.sdg.ast.ExprVar;
import edu.mit.csail.sdg.ast.Func;
import edu.mit.csail.sdg.ast.Module;
@@ -114,7 +117,7 @@
* variable argument is passed
*/
-public final class CompModule extends Browsable implements Module {
+public class CompModule extends Browsable implements Module {
// These fields are shared by all Modules that point to each other
@@ -191,7 +194,7 @@ public String path() {
* The position of the "MODULE" line at the top of the file; Pos.UNKNOWN if the
* line has not been parsed from the file yet.
*/
- private Pos modulePos = Pos.UNKNOWN;
+ public Pos modulePos = Pos.UNKNOWN;
/**
* The text of the "MODULE" line at the top of the file; "unknown" if the line
@@ -202,7 +205,7 @@ public String path() {
/**
* Whether we have seen a name containing a dollar sign or not.
*/
- boolean seenDollar = false;
+ public boolean seenDollar = false;
/**
* Each param is mapped to its corresponding Sig (or null if we have not
@@ -222,7 +225,7 @@ public String path() {
private final Map opens = new LinkedHashMap();
/** Each sig name is mapped to its corresponding SigAST. */
- private final Map sigs = new LinkedHashMap();
+ public final Map sigs = new LinkedHashMap();
/**
* The list of params in this module whose scope shall be deemed "exact"
@@ -232,7 +235,7 @@ public String path() {
/**
* The current name resolution mode (0=pure) (1=Alloy 4.1.3 and older) (2=new)
*/
- int resolution = 1;
+ public int resolution = 1;
/**
* Each func name is mapped to a nonempty list of FunAST objects.
@@ -243,7 +246,7 @@ public String path() {
private final Map macros = new LinkedHashMap();
/** Each assertion name is mapped to its Expr. */
- private final Map asserts = new LinkedHashMap();
+ private final Map asserts = new LinkedHashMap();
/**
* The list of facts; each fact is either an untypechecked Exp or a typechecked
@@ -384,7 +387,7 @@ public Expr resolve(final Pos pos, final String name) {
match = rootmodule.globals.get(name);
if (match != null) {
if (match instanceof Macro)
- return ((Macro) match).changePos(pos);
+ return (match);//.changePos(pos);
match = ExprUnary.Op.NOOP.make(pos, match);
return ExprChoice.make(isIntsNotUsed, pos, asList(match), asList(name));
}
@@ -486,9 +489,14 @@ public Expr visit(ExprITE x) throws Err {
public Expr visit(ExprBadJoin x) throws Err {
Expr left = visitThis(x.left);
Expr right = visitThis(x.right);
+ Expr rightInner = ignoreNoops(right);
// If it's a macro invocation, instantiate it
- if (right instanceof Macro)
- return ((Macro) right).addArg(left).instantiate(this, warns);
+ if (rightInner instanceof Macro){
+ Expr instantiated = ((Macro) rightInner).addArg(left).instantiate(this, warns);
+ Expr res = ExprUnary.Op.NOOP.make(right.pos, instantiated);
+ res.setReferenced(right.referenced());
+ return res;
+ }
// check to see if it is the special builtin function "Int[]"
if (left.type().is_int() && right.isSame(Sig.SIGINT))
return left; // [AM] .cast2sigint();
@@ -499,6 +507,15 @@ public Expr visit(ExprBadJoin x) throws Err {
return process(x.pos, x.closingBracket, right.pos, ((ExprChoice) right).choices, ((ExprChoice) right).reasons, left);
}
+ public static Expr ignoreNoops(Expr e){
+ if (e instanceof ExprUnary){
+ ExprUnary eu = (ExprUnary) e;
+ if( eu.op == Op.NOOP){
+ return ignoreNoops(eu.sub);
+ }
+ }
+ return e;
+ }
/** {@inheritDoc} */
@Override
public Expr visit(ExprBinary x) throws Err {
@@ -506,8 +523,13 @@ public Expr visit(ExprBinary x) throws Err {
Expr right = visitThis(x.right);
if (x.op == ExprBinary.Op.JOIN) {
// If it's a macro invocation, instantiate it
- if (right instanceof Macro)
- return ((Macro) right).addArg(left).instantiate(this, warns);
+ Expr rightInner = ignoreNoops(right);
+ if (rightInner instanceof Macro){
+ Expr instantiated = ((Macro) rightInner).addArg(left).instantiate(this, warns);
+ Expr res = ExprUnary.Op.NOOP.make(right.pos, instantiated);
+ res.setReferenced(right.referenced());
+ return res;
+ }
// check to see if it is the special builtin function "Int[]"
if (left.type().is_int() && right.isSame(Sig.SIGINT))
return left; // [AM] .cast2sigint();
@@ -632,20 +654,9 @@ public Expr visit(ExprVar x) throws Err {
if (obj instanceof Macro) {
Macro macro = ((Macro) obj).copy();
Expr instantiated = macro.instantiate(this, warns);
- instantiated.setReferenced(new Clause() {
-
- @Override
- public Pos pos() {
- return instantiated.pos;
- }
-
- @Override
- public String explain() {
- return instantiated.toString();
- }
-
- });
- return instantiated;
+ Expr res = ExprUnary.Op.NOOP.make(x.pos, instantiated);
+ res.setReferenced(new Clause.Custom(macro.pos, macro.toString()));
+ return res;
} else
return obj;
}
@@ -674,6 +685,21 @@ public Expr visit(Sig x) {
return x;
}
+ @Override
+ public Expr visit(Func x) throws Err {
+ return x;
+ }
+
+ @Override
+ public Expr visit(Assert x) throws Err {
+ return x;
+ }
+
+ @Override
+ public Expr visit(Macro x) throws Err {
+ return x;
+ }
+
/** {@inheritDoc} */
@Override
public Expr visit(Field x) {
@@ -745,7 +771,7 @@ private Open(Pos pos, boolean isPrivate, String alias, ConstList args, S
/**
* Connect this OPEN statement to a module that it points to.
*/
- void connect(CompModule realModule) throws Err {
+ public void connect(CompModule realModule) throws Err {
if (this.realModule != null && this.realModule != realModule)
throw new ErrorFatal("Internal error (import mismatch)");
this.realModule = realModule;
@@ -788,7 +814,7 @@ public String explain() {
* @param filename - the filename corresponding to this module
* @param path - one of the path pointing to this module
*/
- CompModule(CompModule world, String filename, String path) throws Err {
+ public CompModule(CompModule world, String filename, String path) throws Err {
if (world == null) {
if (path.length() > 0)
throw new ErrorFatal("Root module misparsed by parser.");
@@ -890,9 +916,9 @@ public String getHTML() {
}
if (asserts.size() > 0) {
x = new ArrayList(asserts.size());
- for (Map.Entry e : asserts.entrySet()) {
- Pos sp = e.getValue().span();
- x.add(make(sp, sp, "assert " + e.getKey(), e.getValue()));
+ for (Map.Entry e : asserts.entrySet()) {
+ Pos sp = e.getValue().expr.span();
+ x.add(make(sp, sp, "assert " + e.getKey(), e.getValue().expr));
}
ans.add(make("" + x.size() + (x.size() > 1 ? " asserts" : " assert"), x));
}
@@ -925,7 +951,7 @@ private static String base(Sig sig) {
/**
* Generate an error message saying the given keyword is no longer supported.
*/
- static ErrorSyntax hint(Pos pos, String name) {
+ public static ErrorSyntax hint(Pos pos, String name) {
String msg = "The name \"" + name + "\" cannot be found.";
if ("exh".equals(name) || "exhaustive".equals(name) || "part".equals(name) || "partition".equals(name))
msg = msg + " If you are migrating from Alloy 3, please see Help->QuickGuide on how to translate models that use the \"" + name + "\" keyword.";
@@ -933,7 +959,7 @@ static ErrorSyntax hint(Pos pos, String name) {
}
/**
- * Parse one expression by starting fromt this module as the root module.
+ * Parse one expression by starting from this module as the root module.
*/
@Override
public Expr parseOneExpressionFromString(String input) throws Err, FileNotFoundException, IOException {
@@ -993,7 +1019,7 @@ private Object unique(Pos pos, String name, List