Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support operator symbols that have the same semantics. #72

Merged
merged 1 commit into from
Jun 20, 2018
+20 −15
Merged

Support operator symbols that have the same semantics. #72

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions src/pgo/trans/intermediate/BuiltinModule.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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());
Expand Down
16 changes: 7 additions & 9 deletions src/pgo/trans/intermediate/TLABuiltins.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)));
Expand Down Expand Up @@ -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));
Expand All @@ -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));
Expand All @@ -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));
Expand All @@ -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));
Expand Down Expand Up @@ -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(
Expand Down