Dataprop: indexes vs constraint parameters

Google Group
1

Not an issue, just to warn readers.

Given this (case #1):
dataprop A(i:int) =
| A1(1)
| AN(i) of A(i-1)

One can say:
prval pf_a1:A(1) = A1{1}()
prval pf_a2:A(2) = AN{2}(pf_a1)

However, given this (case #2):
dataprop A(i:int) =
| A1(1)
| AN(i+1) of A(i)

One would need to say:
prval pf_a1:A(1) = A1{1}()
prval pf_a2:A(2) = AN{1}(pf_a1)

For pf_a2, the type index is indeed 2, this is just that i is said to be
the index of pf_a1, which is 1.

Constraint parameters (is that the words?) and type indexes, do not always
match, it depends on the way the constraints are expressed. I believe it’s
better to make both match.

Another way to define A as in the second case, with index and constraint
parameter matching as in the first case (case #3):
dataprop A(i:int) =
| A1(1)
| {i:int}{j:int;i==j+1} AN(i) of A(j)

Now one may say as in case #1:
prval pf_a1:A(1) = A1{1}()
prval pf_a2:A(2) = AN{2}(pf_a1)

Beware of this, as this may sometime looks like a trap. I personally will
ban the style of case #2, to make constraints parameter and indexes match.

2

Another way to define A as in the second case, with index and constraint
parameter matching as in the first case (case #3):
dataprop A(i:int) =
| A1(1)
| {i:int}{j:int;i==j+1} AN(i) of A(j)

Now one may say as in case #1:
prval pf_a1:A(1) = A1{1}()
prval pf_a2:A(2) = AN{2}(pf_a1)

Or even this terser way, as {i:int} is implicit when not explicit:

dataprop A(i:int) =
| A1(1)
| {j:int;i==j+1} AN(i) of A(j)

prval pf_a1:A(1) = A1{1}()
prval pf_a2:A(2) = AN{2}(pf_a1)

3

I personally will ban the style of case #2, to make constraints parameter
and indexes match.

While this may occasionally ends into unfriendly cases.

Given this:
dataprop SEQ(i:int, e:int) =
| SEQ1(1, e) of int(e)
| SEQN(i, e) of ([_:int] SEQ(i-1, _), int(e))

One may want to have this:
prval s7 = SEQ1(7)
prval s78 = SEQN(s7,8)
prval s789 = SEQN(s78,9)

the i of s78 should be derived from the i of s7 and the i of s789 should be
derived from the i of s78. But the constraint solver does not handle it
well, it complains it can’t solve the constraint about i.

It seems better to explicitly tell it how to compute it. Indeed, given this
(compare third lines):
dataprop SEQ(i:int, e:int) =
| SEQ1(1, e) of int(e)
| SEQN(i+1, e) of ([_:int] SEQ(i, _), int(e))

Now fine, no complaints from the constraint solver:
prval s7 = SEQ1(7)
prval s78 = SEQN(s7,8)
prval s789 = SEQN(s78,9)

Unfortunately, in the while, it also breaks the cool style of having index
and constraint parameters match (while there is no need to give these).
prval s7:SEQ(1,7) = SEQ1{1,7}(7)
prval s78:SEQ(2,8) = SEQN{1,8}(s7,8)
prval s789:SEQ(3,9) = SEQN{2,9}(s78,9)

Second line: i as an index, is 2, while as a constraint parameter, it’s 1.
Third line: i as an index, is 3, while as a constraint parameter, it’s 2.

With the initial:
dataprop SEQ(i:int, e:int) =
| SEQ1(1, e) of int(e)
| SEQN(i, e) of ([_:int] SEQ(i-1, _), int(e))

There is no more divergence, and both match:
prval s7:SEQ(1,7) = SEQ1{1,7}(7)
prval s78:SEQ(2,8) = SEQN{2,8}(s7,8)
prval s789:SEQ(3,9) = SEQN{3,9}(s78,9)

While this is more verbose, as either one of the index or the constraint
parameter, needs to be explicitly given.

So when in a prior message I have said “I personally will ban the style of
case #2, to make constraints parameter and indexes match”, it was easy to
say, in practice, this may not be easy to always follow this style and be
terse together.

Some more stuffs to have in mind …