spechub/Hets — pull request #1322 by cmaeder (2014-08-08 12:27:29+00:00)
Title: 1314 sort constraints

fixes #1314. The initial motivation of this issue was #1296, i.e. to avoid unnecessary sort generation constraints as goals.

The first patch https://github.com/spechub/Hets/commit/db3b74383c0afcd7a0aec50c263aec4f4e09df8d decomposes blocks into minimal sub blocks of proper dependency order.

The second patch displays the blocks as warnings, i.e. for StructuredDatatypes and Graph:

```
Basic/StructuredDatatypes.casl:527.5-531.18: ### Warning:
splittable groups of generated sorts
'[{NonEmptyBinTree2[Elem]}, {BinTree2[Elem]}]'
...
Basic/StructuredDatatypes.casl:668.5-680.16: ### Warning:
splittable groups of generated sorts
'[{List[NonEmptyNTree2[Elem]], NonEmptyList[NonEmptyNTree2[Elem]],
NonEmptyNTree2[Elem]},
{NTree2[Elem]}]'
...
Basic/Graphs.casl:351.13-352.20: ### Warning:
splittable groups of generated sorts '[{Five}, {FivePair}]'
```

The third patch is to ensure that the order of constructors and the order of mutually recursive generated sorts does not matter, also after renaming.

The next patch was needed to check this single branch. (So far all looks well.)

The last patch extends an example, to show that no sort generation theorems are created.
However trivial goals (equations with swapped sides) remain due to the changed order of constructors.

@mcodescu please review and sign off this request (using `:+1:` :+1:)