All navigation paths are consistently such that brackets are not needed leveraging left-associativity of join (.), see leftAssocDeref.cfr, navAndDeref.cfr, and navAndDeref.als.reg. This should have positive impact on reasoning speed with Alloy.
Fixed incorrect typing of quantified expressions with and without local declarations:
for some P, no P, one P, P must not be TBoolean, whereas
for some x : X | P, no x : X | P, one x : X | P, X must not be TBoolean and P must be TBoolean.
Added Alloy and Choco escapes, see escapes.cfr. Code in Alloy escapes is included at the beginning of the Alloy output, whereas, Choco escapes are included at the end of Choco output.
Block and line comments, as well as Alloy and Choco escape blocks are new token types, which retain their position for easier processing.
Changed ref to dref.
Added handling and deprecation warnings for deprecated ref and &; instead dref and ** should be used, see deprecated.cfr
Fixed bugs with incorrect addition of .drefs in arithmetic, see arithmetic.cfr.
Fixed missing links bugs in HTML output.
Preserve positions which were lost in Desugarer, ResolverName, and Optimizer, making it impossible to trace back from Ast to IR in some cases.
Links were incorrectly generated for this, parent, and dref.
Avoided unnecessary double parsing in Clafer.parse.
Added continuous integration with TravisCI. Restored compatibility with GHC 7.8.3, 7.8.4, 7.10.1, and 7.10.2.
Added support for stack tool, both GHC 7.8.4 with LTS-2.22 and 7.10.2 with LTS-3.3 work.
.
), see leftAssocDeref.cfr, navAndDeref.cfr, and navAndDeref.als.reg. This should have positive impact on reasoning speed with Alloy..dref
is not needed anymore, see EDM_Intro.cfr, NestedInheritanceAndReference2.cfr, i84-references-pointing-to-the-same-object.cfr , and mergeExpAndSetExpAlloy.cfr.some
quantifier when needed, see quantifierAndDefaultSome.cfr and ifthenelse.cfr.if/then/else
expressions allowing both boolean and non-boolean consequents, see i144-if-then-else.cfr and ifthenelse.cfr.some P, no P, one P
,P
must not beTBoolean
, whereassome x : X | P, no x : X | P, one x : X | P
,X
must not beTBoolean
andP
must beTBoolean
.ref
todref
.ref
and&
; insteaddref
and**
should be used, see deprecated.cfr.dref
s in arithmetic, see arithmetic.cfr.Desugarer
,ResolverName
, andOptimizer
, making it impossible to trace back from Ast to IR in some cases.this
,parent
, anddref
.Clafer.parse
.stack
tool, both GHC 7.8.4 with LTS-2.22 and 7.10.2 with LTS-3.3 work.