conditional exports

[Ralf Hemmecke]

I know we had this before...

Foo(F): Exports == Implementation where
F: Type
Exports ==> FooCat(F) with
...
Implementation ==> add
Rep ==> Record(mul: F, be: H)
...
if F has with qetaGrade: % -> ZZ then (*)
numberOfGaps(x: %): NN ==
t: F := multiplier x
n: PP := qetaGrade(t)::PP
...

Unfurtunately, it does not compile. It complains

error in function numberOfGaps

(SEQ (|:=| (|:| |t| F) (|multiplier| |x|))
(|:=| (|:| |n| (|PositiveInteger|))
(|::| (|qetaGrade| | << t >> |) (|PositiveInteger|)))
(|:=| (|:| |grades| (|List| (|PositiveInteger|)))
(COLLECT (IN |i| (SEGMENT 1 (- |n| 1)))
(|::| (|qetaGrade| (|first| (|basis| |x| |i|)))
(|PositiveInteger|))))
(|exit| 1 ((|Sel| (|QEtaAuxiliaryPackage|) |numberOfGaps|) |n|
|grades|)))
****** level 5 ******
$x:= t
$m:= $
$f:=
((((|n| #) (|t| # #) (|x| # #) (F # #) ...)))

>> Apparent user error:
Cannot coerce t
of mode F
to mode $

A workaround is to replace in (*) the % by an F.

ALthough working, it looks a bit odd to me. Why should the % in that
position ever refer to Foo(F)? Is there a situation where it would make
sense?

Ralf

[Waldek Hebisch]

Well, you _use_ the declaration in line:

n: PP := qetaGrade(t)::PP

In that line '%' is Foo(F). In line where you state condition
'%' means F. Unfortunately, ATM Spad compiler has limited
capability to make inferences and probably just stores info that
'qetaGrade' from '%' to ZZ is available. But at point of use
'%' has wrong meaning.

Yes, Spad compiler should properly track meaning of '%'. But
in this case using F is clearer both for compiler and readers
of the code.

--
Waldek Hebisch

[Ralf Hemmecke]

> Yes, Spad compiler should properly track meaning of '%'. But
> in this case using F is clearer both for compiler and readers
> of the code.

Well, I do not know the internal datastructure for storing the
information, but it seems that when the compiler sees the line

if F has with qetaGrade: % -> ZZ then (*)

it should attach the property to % that it actually means F (and only to
the % at the type of qetaGrade).

OK, maybe I am too naive here but perhaps it could be a small change to
let the compiler not misinterpret the % when it comes to

n: PP := qetaGrade(t)::PP

where t : F.

Maybe I should add it to the github issues section.

Ralf