search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
709 stars 123 forks source link

Allow equality between predicates #12

Closed pkriens closed 7 years ago

pkriens commented 7 years ago

It is now difficult to verify if two predicates are the same.

  pred a {...}
  pred b {...}

  pred equal { a = b } // fails

This then requires something like:

  pred equal { a => b else !b }

Which is kind of complexifying. I understand that it is caused by not exposing the primitive boolean to the language but I am not sure I understand why? Booleans are a common type. Although they are often abused (in Java booleans should often be an enum) they have their use. Especially here

aleksandarmilicevic commented 7 years ago

You can use a <=> b.

pkriens commented 7 years ago

thanks!

pkriens commented 7 years ago

Ah, that is nice. Sorry I missed that.

aleksandarmilicevic commented 7 years ago

The reason why = cannot be used to assert equivalence of 2 predicates is because = is a relational operator, and as such it only accepts relations as its operands. I guess it would be possible to overload the = operator to act as set equality when operands are relations and as boolean equivalence when operands are boolean; the way it is now, in my opinion, makes the language cleaner.