support for past operator 'since'

haslab · Nov 10, 2016 · 3a31500 · 3a31500
1 parent 7a2494e
commit 3a31500
Show file tree

Hide file tree

Showing 20 changed files with 2,264 additions and 2,635 deletions.
diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxDocument.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4/OurSyntaxDocument.java
@@ -38,7 +38,7 @@
  *
  * <p><b>Thread Safety:</b> Can be called only by the AWT event thread
  *
- * @modified: nmm, Eduardo Pessoa (pt.uminho.haslab.pt): temporal keywords
+ * @modified: Nuno Macedo, Eduardo Pessoa // [HASLab] temporal keywords
  */
 
 class OurSyntaxDocument extends DefaultStyledDocument {
@@ -96,7 +96,7 @@ class OurSyntaxDocument extends DefaultStyledDocument {
 		"disjoint", "else", "enum", "exactly", "exh", "exhaustive", "expect", "extends", "fact", "for", "fun", "iden",
 		"iff", "implies", "in", "Int", "int", "let", "lone", "module", "no", "none", "not", "one", "open", "or", "part",
 		"partition", "pred", "private", "run", "seq", "set", "sig", "some", "String", "sum", "this", "univ", 
-		"eventually", "always", "after", "once", "historically", "previous", "until", "release" // pt.uminho.haslab: temporal keywords
+		"eventually", "always", "after", "once", "historically", "since", "previous", "until", "release" // [HASLab] temporal keywords
 	};
 
 	/** Returns true if array[start .. start+len-1] matches one of the reserved keyword. */
@@ -110,7 +110,7 @@ private static final boolean do_keyword(String array, int start, int len) {
 
 	/** Returns true if "c" can be in the start or middle or end of an identifier. */
 	private static final boolean do_iden(char c) {
-		return (c>='A' && c<='Z') || (c>='a' && c<='z') || c=='$' || (c>='0' && c<='9') || c=='_' /*|| c=='\''*/ || c=='\"'; // [HASLab]
+		return (c>='A' && c<='Z') || (c>='a' && c<='z') || c=='$' || (c>='0' && c<='9') || c=='_' /*|| c=='\''*/ || c=='\"'; // [HASLab] primed expressions
 	}
 
 	/** Constructor. */

diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/BinaryExprTemp.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/BinaryExprTemp.java
diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/ExprBinary.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/ExprBinary.java
@@ -190,7 +190,10 @@ public static enum Op {
       /** !in             */  NOT_IN("!in",false),
       /** &amp;&amp;      */  AND("&&",false),
       /** ||              */  OR("||",false),
-      /** &lt;=&gt;       */  IFF("<=>",false);
+      /** &lt;=&gt;       */  IFF("<=>",false),
+      /** until;          */  UNTIL("until",false), // [HASLab]
+      /** release;        */  RELEASE("release",false), // [HASLab]
+      /** since;          */  SINCE("since",false); // [HASLab]
 
       /** The constructor.
        * @param label - the label (for printing debugging messages)
@@ -230,7 +233,7 @@ public final Expr make(Pos pos, Pos closingBracket, Expr left, Expr right) {
               right = right.typecheck_as_int();
               break;
            }
-           case IFF: case IMPLIES: {
+           case IFF: case IMPLIES: case RELEASE: case UNTIL: case SINCE: { // [HASLab]
               left = left.typecheck_as_formula();
               right = right.typecheck_as_formula();
               break;
@@ -264,7 +267,7 @@ public final Expr make(Pos pos, Pos closingBracket, Expr left, Expr right) {
          JoinableList<Err> errs = left.errors.make(right.errors);
          if (errs.isEmpty()) switch(this) {
            case LT: case LTE: case GT: case GTE: case NOT_LT: case NOT_LTE: case NOT_GT: case NOT_GTE:
-           case AND: case OR: case IFF: case IMPLIES:
+           case AND: case OR: case IFF: case IMPLIES: case RELEASE: case UNTIL: case SINCE: // [HASLab]
               type = Type.FORMULA;
               break;
            case MUL: case DIV: case REM: case SHL: case SHR: case SHA:
@@ -341,7 +344,7 @@ public final Expr make(Pos pos, Pos closingBracket, Expr left, Expr right) {
            a=(b=Type.smallIntType());
            break;
         }
-        case AND: case OR: case IFF: case IMPLIES: {
+        case AND: case OR: case IFF: case IMPLIES: case RELEASE: case UNTIL: case SINCE: { // [HASLab]
            a=(b=Type.FORMULA);
            break;
         }

diff --git a/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/ExprCall.java b/electrum/src/main/java/edu/mit/csail/sdg/alloy4compiler/ast/ExprCall.java
@@ -96,6 +96,7 @@ private DeduceType() { }
         @Override public Type visit(ExprBinary x) throws Err {
             switch(x.op) {
               case IMPLIES: case GT: case GTE: case LT: case LTE: case IFF: case EQUALS: case IN: case OR: case AND:
+              case RELEASE: case UNTIL: case SINCE: // [HASLab]
               case NOT_LT: case NOT_GT: case NOT_LTE: case NOT_GTE: case NOT_IN: case NOT_EQUALS:
                   return Type.FORMULA;
               case MUL: case DIV: case REM: case SHL: case SHR: case SHA:
@@ -118,7 +119,7 @@ private DeduceType() { }
         @Override public Type visit(ExprUnary x) throws Err {
             Type t = x.sub.accept(this);
             switch(x.op) {
-              case NOOP: case LONEOF: case ONEOF: case SETOF: case SOMEOF: case EXACTLYOF: return t;
+              case NOOP: case LONEOF: case ONEOF: case SETOF: case SOMEOF: case EXACTLYOF: case PRIME: return t; // [HASLab]
               case CARDINALITY: case CAST2INT: return Type.smallIntType();
               case CAST2SIGINT: return Sig.SIGINT.type;
               case TRANSPOSE: return t.transpose();
@@ -142,14 +143,6 @@ private DeduceType() { }
             return (ans==null) ? EMPTY : ans;
         }
 
-        @Override
-        public Type visit(BinaryExprTemp x) throws Err {
-            return Type.FORMULA;
-        }
-
-        @Override public Type visit(ExprTemp x) throws Err {
-            return Type.FORMULA;
-        }
         @Override public Type visit(ExprLet x) throws Err {
             env.put(x.var, x.expr.accept(this));
             Type ans = x.sub.accept(this);