Dataprop: indexes vs constraint parameters

[Yannick Duchêne]

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.

[Yannick Duchêne]

Le mardi 22 décembre 2015 16:08:38 UTC+1, Yannick Duchêne a écrit :

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}()

[Yannick Duchêne]

Le mardi 22 décembre 2015 16:08:38 UTC+1, Yannick Duchêne a écrit :

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 …