Merge pull request #72 from UBC-NSS/operators-same-fn

Support operator symbols that have the same semantics.
DistCompiler · Jun 20, 2018 · 8411fcf · 8411fcf
2 parents 939ecad + c7bc6e2
commit 8411fcf
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 15 deletions.
diff --git a/src/pgo/trans/intermediate/BuiltinModule.java b/src/pgo/trans/intermediate/BuiltinModule.java
@@ -1,30 +1,37 @@
 package pgo.trans.intermediate;
 
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
 
 import pgo.scope.ChainMap;
 
 public class BuiltinModule {
-	
+
 	Map<String, OperatorAccessor> operators;
-	
+
 	public BuiltinModule() {
 		this.operators = new HashMap<>();
 	}
-	
+
 	public BuiltinModule(BuiltinModule exts) {
 		this.operators = new ChainMap<>(exts.operators);
 	}
-	
+
 	public void addOperator(String name, OperatorAccessor op) {
 		operators.put(name, op);
 	}
-
+
+	public void addOperators(List<String> names, OperatorAccessor op) {
+		for (String name : names) {
+			addOperator(name, op);
+		}
+	}
+
 	public Map<String, OperatorAccessor> getOperators(){
 		return operators;
 	}
-	
+
 	public void addDefinitionsToScope(TLAScopeBuilder scope) {
 		for(Map.Entry<String, OperatorAccessor> op : operators.entrySet()) {
 			scope.defineGlobal(op.getKey(), op.getValue().getUID());

diff --git a/src/pgo/trans/intermediate/TLABuiltins.java b/src/pgo/trans/intermediate/TLABuiltins.java
@@ -120,7 +120,7 @@ public static void ensureUniqueSorted(BlockBuilder builder, Type elementType, Va
 							.accept(new PGoTypeGoTypeConversionVisitor())
 							.accept(new EqCodeGenVisitor(builder, lhs, rhs, false));
 				}));
-		universalBuiltIns.addOperator("#", new BuiltinOperator(
+		universalBuiltIns.addOperators(Arrays.asList("#", "/="), new BuiltinOperator(
 				2,
 				(origin, args, solver, generator) -> {
 					solver.addConstraint(new PGoTypeMonomorphicConstraint(origin, args.get(0), args.get(1)));
@@ -276,7 +276,7 @@ public static void ensureUniqueSorted(BlockBuilder builder, Type elementType, Va
 					}
 					return tmpSet;
 				}));
-		universalBuiltIns.addOperator("~", new TypelessBuiltinOperator(
+		universalBuiltIns.addOperators(Arrays.asList("~", "\\lnot", "\\neg"), new TypelessBuiltinOperator(
 				1,
 				(origin, args, solver, generator) -> {
 					PGoType fresh = new PGoTypeBool(Collections.singletonList(origin));
@@ -286,7 +286,7 @@ public static void ensureUniqueSorted(BlockBuilder builder, Type elementType, Va
 				(builder, origin, registry, arguments, typeMap) -> new Unary(
 						Unary.Operation.NOT, arguments.get(0))
 				));
-		universalBuiltIns.addOperator("\\/", new TypelessBuiltinOperator(
+		universalBuiltIns.addOperators(Arrays.asList("\\/", "\\lor"), new TypelessBuiltinOperator(
 				2,
 				(origin, args, solver, generator) -> {
 					PGoType fresh = new PGoTypeBool(Collections.singletonList(origin));
@@ -297,7 +297,7 @@ public static void ensureUniqueSorted(BlockBuilder builder, Type elementType, Va
 				(builder, origin, registry, arguments, typeMap) -> new Binop(
 						Binop.Operation.OR, arguments.get(0), arguments.get(1))
 				));
-		universalBuiltIns.addOperator("/\\", new TypelessBuiltinOperator(
+		universalBuiltIns.addOperators(Arrays.asList("/\\", "\\land"), new TypelessBuiltinOperator(
 				2,
 				(origin, args, solver, generator) -> {
 					PGoType fresh = new PGoTypeBool(Collections.singletonList(origin));
@@ -308,7 +308,7 @@ public static void ensureUniqueSorted(BlockBuilder builder, Type elementType, Va
 				(builder, origin, registry, arguments, typeMap) -> new Binop(
 						Binop.Operation.AND, arguments.get(0), arguments.get(1))
 				));
-		universalBuiltIns.addOperator("\\union", new TypelessBuiltinOperator(
+		universalBuiltIns.addOperators(Arrays.asList("\\union", "\\cup"), new TypelessBuiltinOperator(
 				2,
 				(origin, args, solver, generator) -> {
 					PGoType fresh = new PGoTypeSet(generator.get(), Collections.singletonList(origin));
@@ -446,15 +446,13 @@ public static void ensureUniqueSorted(BlockBuilder builder, Type elementType, Va
 				(builder, origin, registry, arguments, typeMap) -> new Binop(
 						Binop.Operation.GT, arguments.get(0), arguments.get(1))
 				));
-		// TODO: \leq =<
-		Naturals.addOperator("<=", new TypelessBuiltinOperator(
+		Naturals.addOperators(Arrays.asList("<=", "\\leq"), new TypelessBuiltinOperator(
 				2,
 				TLABuiltins::constraintBooleanNumberOperation,
 				(builder, origin, registry, arguments, typeMap) -> new Binop(
 						Binop.Operation.LEQ, arguments.get(0), arguments.get(1))
 				));
-		// TODO: \geq
-		Naturals.addOperator(">=", new TypelessBuiltinOperator(
+		Naturals.addOperators(Arrays.asList(">=", "\\geq"), new TypelessBuiltinOperator(
 				2,
 				TLABuiltins::constraintBooleanNumberOperation,
 				(builder, origin, registry, arguments, typeMap) -> new Binop(