Message info

Serge D. Mechveliani wrote:

>

> Dear Axiom/FriCAS developers,

>

> I have in my package DList1(T : Type):

> ...

> ==

> add

> ListPair ==> Product(List T, List T)

> lPair(xs : List T, ys : List T) : ListPair ==

> construct(xs, ys) $ ListPair

> ...

> halve(xs : List T) : ListPair == -- split a list to halfs

>

> h(ls : List T, rs : List T, ys : List T) : ListPair ==

> Fin ==> lPair(reverse ls, rs)

> empty? rs => Fin

> x := first rs

> empty? ys => Fin

> ys' := rest ys

> empty? ys' => Fin

> h (cons(x, ls), rest rs, rest ys')

> h([] :: List T, xs, xs)

>

> In the body, it is defined a local h, and then h is applied.

>

> The whole large program of several packages compiles, with regular

> messages. Then, at the run time,

> -> halve([1,2]) $DList1(Integer)

> reports something like

> "... Lisp ... the function h in DList1 is not defined."

> !

>

> 1. As h is not defined, why the compiler has not reported of this?

There are limitation in current support for local functions.

In particular recursive local functions are not supported.

Spad compiler does not detect if function is recursive, but

generates non-working code.

Why? Fixing problem requires work. AFAICS detecting problematic

cases in compiler requires more work than handling them correctly.

It would be easy to completely disable local functions, but the

working cases are too useful to do this.

> 2. How to define safely local functions, like this h ?

> I tried

> halve(xs : List T) : ListPair == h([] :: List T, xs, xs) where

>

> h(ls : List T, rs : List T, ys : List T) : ListPair ==

> Fin ==> lPair(reverse ls, rs)

> empty? rs => Fin

> x := first rs

> empty? ys => Fin

> ys' := rest ys

> empty? ys' => Fin

> h (cons(x, ls), rest rs, rest ys')

>

> -- similar as with `where' in Haskell. And it works.

IIRC it does not really give you a local function: you can

use h only in 'halve' but you do not gain access to local

variables of it.

> Then I looked into several Spad examples in src/algebra/*.spad*, and

> observed that `where' is used only in the package syntax

> == Implementation where ...

>

> Also there must be possible a syntax in which first h is defined,

> and then h is applied lower. So, I try

>

> halve(xs : List T) : ListPair ==

>

> h(ls : List T, rs : List T, ys : List T) : ListPair ==

> (

> Fin ==> lPair(reverse ls, rs)

> empty? rs => Fin

> x := first rs

> empty? ys => Fin

> ys' := rest ys'

> empty? ys' => Fin

> h (cons(x, ls), rest rs, rest ys')

> )

> h([] :: List T, xs, xs)

>

> The compiler reports

> ----------------------------------------------------

> ...

> [ a long message ]

>

> (|Fin| (|h| (|cons| |x| |ls|) (|rest| |rs|) (|rest| |ys'|))))

> |noBranch|))))

> |noBranch|))))

> |noBranch|)))))

> (|exit| 1 (|h| (|::| (|construct|) (|List| T$)) |xs| |xs|)))

> ****** level 3 ******

> $x:= (MDEF (Fin) (NIL) (NIL) (SEQ (LET G13293 ((lPair (reverse ls) rs)

> ...

>

> (exit 1 (IF #G1 (exit 4 (Fin (h (cons x ls) (rest rs) (rest ys'))))

> noBranch)))) noBranch)))) noBranch))))

>

> $m:= (Product (List T$) (List T$))

> $f:=

> ((((|ys| #) (|rs| #) (|ls| #) (|h| #) ...)))

>

> >> Apparent user error:

> compLambda: signature needed

> (+-> (ls rs ys) (MDEF (Fin) () () (SEQ (LET G13293 ((lPair

> (reverse ls) rs) (empty? rs))) (exit 1 (IF G13293 (exit 2

> (SEQ (LET #G2 (first (rs (empty? ys)))) (LET (Fin x) #G2)

> (exit 1 (IF #G2 (exit 3 (SEQ (LET #G1 (rest (ys' (empty? ys'))))

> (LET (Fin ys') #G1) (exit 1 (IF #G1 (exit 4 (Fin (h (cons x ls)

> (rest rs) (rest ys')))) noBranch)))) noBranch)))) noBranch)))))

Looks like a bug -- I will investigate.

> ----------------------------------------------------

>

> 3. I have noticed that in the functions like

> f x ==

> p x == ...

> ...

> g x == (p x) + 1

> g 2

>

> the local "==" difinitions for p and g can sometimes be

> trasposed, and sometimes the compiler reports

> "the function ... is not defined",

> "cannot compile (p x) + 1 " ...

>

> At least, at the top level after '== add' in a package,

> are the function definitions transposable?

>

> What parts in function definitions are transposable?

In general, you should declare things before using them. If

you need to use function before definition use code like:

-- declaration

f : T1 -> T2

-- Use f

-- Definition

f(x) == ...

--

Waldek Hebisch

hebisch@math.uni.wroc.pl

--

You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.

To post to this group, send email to fricas-devel@googlegroups.com.

To unsubscribe from this group, send email to fricas-devel+unsubscribe@googlegroups.com.

For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.

>

> Dear Axiom/FriCAS developers,

>

> I have in my package DList1(T : Type):

> ...

> ==

> add

> ListPair ==> Product(List T, List T)

> lPair(xs : List T, ys : List T) : ListPair ==

> construct(xs, ys) $ ListPair

> ...

> halve(xs : List T) : ListPair == -- split a list to halfs

>

> h(ls : List T, rs : List T, ys : List T) : ListPair ==

> Fin ==> lPair(reverse ls, rs)

> empty? rs => Fin

> x := first rs

> empty? ys => Fin

> ys' := rest ys

> empty? ys' => Fin

> h (cons(x, ls), rest rs, rest ys')

> h([] :: List T, xs, xs)

>

> In the body, it is defined a local h, and then h is applied.

>

> The whole large program of several packages compiles, with regular

> messages. Then, at the run time,

> -> halve([1,2]) $DList1(Integer)

> reports something like

> "... Lisp ... the function h in DList1 is not defined."

> !

>

> 1. As h is not defined, why the compiler has not reported of this?

There are limitation in current support for local functions.

In particular recursive local functions are not supported.

Spad compiler does not detect if function is recursive, but

generates non-working code.

Why? Fixing problem requires work. AFAICS detecting problematic

cases in compiler requires more work than handling them correctly.

It would be easy to completely disable local functions, but the

working cases are too useful to do this.

> 2. How to define safely local functions, like this h ?

> I tried

> halve(xs : List T) : ListPair == h([] :: List T, xs, xs) where

>

> h(ls : List T, rs : List T, ys : List T) : ListPair ==

> Fin ==> lPair(reverse ls, rs)

> empty? rs => Fin

> x := first rs

> empty? ys => Fin

> ys' := rest ys

> empty? ys' => Fin

> h (cons(x, ls), rest rs, rest ys')

>

> -- similar as with `where' in Haskell. And it works.

IIRC it does not really give you a local function: you can

use h only in 'halve' but you do not gain access to local

variables of it.

> Then I looked into several Spad examples in src/algebra/*.spad*, and

> observed that `where' is used only in the package syntax

> == Implementation where ...

>

> Also there must be possible a syntax in which first h is defined,

> and then h is applied lower. So, I try

>

> halve(xs : List T) : ListPair ==

>

> h(ls : List T, rs : List T, ys : List T) : ListPair ==

> (

> Fin ==> lPair(reverse ls, rs)

> empty? rs => Fin

> x := first rs

> empty? ys => Fin

> ys' := rest ys'

> empty? ys' => Fin

> h (cons(x, ls), rest rs, rest ys')

> )

> h([] :: List T, xs, xs)

>

> The compiler reports

> ----------------------------------------------------

> ...

> [ a long message ]

>

> (|Fin| (|h| (|cons| |x| |ls|) (|rest| |rs|) (|rest| |ys'|))))

> |noBranch|))))

> |noBranch|))))

> |noBranch|)))))

> (|exit| 1 (|h| (|::| (|construct|) (|List| T$)) |xs| |xs|)))

> ****** level 3 ******

> $x:= (MDEF (Fin) (NIL) (NIL) (SEQ (LET G13293 ((lPair (reverse ls) rs)

> ...

>

> (exit 1 (IF #G1 (exit 4 (Fin (h (cons x ls) (rest rs) (rest ys'))))

> noBranch)))) noBranch)))) noBranch))))

>

> $m:= (Product (List T$) (List T$))

> $f:=

> ((((|ys| #) (|rs| #) (|ls| #) (|h| #) ...)))

>

> >> Apparent user error:

> compLambda: signature needed

> (+-> (ls rs ys) (MDEF (Fin) () () (SEQ (LET G13293 ((lPair

> (reverse ls) rs) (empty? rs))) (exit 1 (IF G13293 (exit 2

> (SEQ (LET #G2 (first (rs (empty? ys)))) (LET (Fin x) #G2)

> (exit 1 (IF #G2 (exit 3 (SEQ (LET #G1 (rest (ys' (empty? ys'))))

> (LET (Fin ys') #G1) (exit 1 (IF #G1 (exit 4 (Fin (h (cons x ls)

> (rest rs) (rest ys')))) noBranch)))) noBranch)))) noBranch)))))

Looks like a bug -- I will investigate.

> ----------------------------------------------------

>

> 3. I have noticed that in the functions like

> f x ==

> p x == ...

> ...

> g x == (p x) + 1

> g 2

>

> the local "==" difinitions for p and g can sometimes be

> trasposed, and sometimes the compiler reports

> "the function ... is not defined",

> "cannot compile (p x) + 1 " ...

>

> At least, at the top level after '== add' in a package,

> are the function definitions transposable?

>

> What parts in function definitions are transposable?

In general, you should declare things before using them. If

you need to use function before definition use code like:

-- declaration

f : T1 -> T2

-- Use f

-- Definition

f(x) == ...

--

Waldek Hebisch

hebisch@math.uni.wroc.pl

--

You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.

To post to this group, send email to fricas-devel@googlegroups.com.

To unsubscribe from this group, send email to fricas-devel+unsubscribe@googlegroups.com.

For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.