gsdlab / clafer

Clafer is a lightweight modeling language
http://clafer.org
MIT License
45 stars 13 forks source link

Non-exhaustive patterns in "Sugar-op" and "Case" #8

Closed mantkiew closed 12 years ago

mantkiew commented 12 years ago

Using clafer 0.0.3

Case 1)

abstract A x ? y ? [ (x => ! y) && (y => ! x) ]

produces the following error:

C:\Temp>clafer3 -k -m=clafer non-exhaustive-patterns.cfr

Parse Successful! [Desugaring] [Resolving] [Analyzing String] [Optimizing] [Generating Code] All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0 Constraints: 1 Global scope: 1..* All names unique: True

[Saving File] clafer3: Intermediate\Desugarer.hs:(320,5)-(326,35): Non-exhaustive patterns in function sugarOp

Case 2)

abstract A x ? y ? [ x => ! y && y => ! x ]

produces the following error:

Parse Successful! [Desugaring] [Resolving] [Analyzing String] [Optimizing] [Generating Code] All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0 Constraints: 1 Global scope: 1..* All names unique: True

[Saving File] clafer3: Intermediate\Desugarer.hs:(316,18)-(328,80): Non-exhaustive patterns in case

Case 3)

abstract A x ? y ? [ x => ! y y => ! x ]

produces the following error:

Parse Successful! [Desugaring] [Resolving] [Analyzing String] [Optimizing] [Generating Code] All clafers: 3 | Abstract: 1 | Concrete: 2 | References: 0 Constraints: 1 Global scope: 1..* All names unique: True

[Saving File] clafer3: Intermediate\Desugarer.hs:(320,5)-(326,35): Non-exhaustive patterns in function sugarOp

Case 4)

abstract A x ? y ? [ x => ! y ] [ y => ! x ]

is correct!