On Fri, Apr 21, 2023 at 05:04:25PM +0200, Ralf Hemmecke wrote:
> 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?
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
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/fricas-devel/20230421165939.ksqr2uojhu3vkay3%40fricas.math.uni.wroc.pl.
