login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for #219 The interpreter does not understand dependend types revision 1 of 1

1
Editor:
Time: 2007/11/17 22:10:40 GMT-8
Note: Update

changed:
-
The following Aldor construct does not yet work in Axiom.

This is in fact the reason why I would love to have Aldor working. I did not expect it to work, and it does not, but it works *almost*. The code is as follows:

\begin{aldor}
#include "axiom"

Test: with { f: (n: PositiveInteger) -> PrimeField(n) } 
   == add { f(n: PositiveInteger): PrimeField(n) == 
              10::Integer::PrimeField(n) }
\end{aldor}

Note that such a construction - the resulting domain depending on the function parameter - is currently illegal in Axiom. In Aldor it is fine.

I compiled it with Aldor as usual, and then loaded it into Axiom. As signature I got the slightly unusual:
\begin{axiom}
)di op f
\end{axiom}

and trying it out I obtained:
\begin{axiom}
f(5)$Test
\end{axiom}

which is roughly what I expected. However, to my great surprise, if you turn on the debugger (beforehand. You always have to start a fresh axiom because of the error I told you about in my previous message) with::

  )lisp (setq |$monitorNewWorld| t)

and thus trace::

  f(1783)$Test

the final bit reads::

  protected-symbol-warn called with (NIL)..IntegerMod 1783 wants
   positiveRemainder : (%,%) -> % from  Integer
  ---->Integer----> searching op table for:
   positiveRemainder : (%,%) -> % from  Integer
  <----#<compiled-function |INT;positiveRemainder;3$;28|> Integer
  goget stuffing slot 47 of IntegerMod 1783
  <------#<compiled-function |INT;positiveRemainder;3$;28|> Integer

  PrimeField n activating lazy slot 8: Integer
  PrimeField n activating lazy slot 9: IntegerPrimesPackage Integer

  ..PrimeField n wants
   prime? : Integer -> Boolean from  IntegerPrimesPackage Integer
  ---->IntegerPrimesPackage Integer----> searching op table for:
   prime? : Integer -> Boolean from  IntegerPrimesPackage Integer
  <----#<compiled-function |PRIMES;prime?;IB;4|>(IntegerPrimesPackage,Integer)
  goget stuffing slot 10 of PrimeField n
  <------#<compiled-function |PRIMES;prime?;IB;4|>(IntegerPrimesPackage,Integer)

which clearly tells you, that the calculation is done alright, only the
signature interferes with success.

Any ideas?

Peter said, that it's on the interpreter side. You can read the whole
thread on 
http://lists.gnu.org/archive/html/axiom-developer/2005-01/msg00154.html

Concerning his patches, Peter also pointed out that

- aldor "extend" does not work

- The algebra defined in libaxiom.al is not current, and for it to be rebuilt
  various .as files need to be available to the build process (axextend.as and
  friends)

- exported attributes from aldor domains are explicitly killed off by this
  patch (it's probably easy to fix, just no time at the moment).  

- Only tested the most trivial domains he could find.

From kratt6 Sat Oct 15 06:04:09 -0500 2005
From: kratt6
Date: Sat, 15 Oct 2005 06:04:09 -0500
Subject: property change
Message-ID: <20051015060409-0500@page.axiom-developer.org>

Severity: normal => wishlist 


From kratt6 Fri Nov 25 06:58:39 -0600 2005
From: kratt6
Date: Fri, 25 Nov 2005 06:58:39 -0600
Subject: Update
Message-ID: <20051125065839-0600@wiki.axiom-developer.org>

Note that with Peter''s patches the error message 'System Error: Unfortunate use of dependant type' is directly triggered by the code produced by aldor. In the lisp file, there line 201 reads::

    (|Halt| (the |SInt| 101))))

'|Halt|' is a function in 'foam_l.lisp'. I do not know why the call to this error was not produced with the old 'libaxiom.al'. Would be great if somebody could help here...

Martin

Submitted by : (unknown) at: 2007-11-17T22:10:40-08:00 (17 years ago)
Name :
Axiom Version :
Category : Severity : Status :
Optional subject :  
Optional comment :

The following Aldor construct does not yet work in Axiom.

This is in fact the reason why I would love to have Aldor working. I did not expect it to work, and it does not, but it works almost. The code is as follows:

fricas
(1) -> <aldor>
#include "axiom"
Test: with { f: (n: PositiveInteger) -> PrimeField(n) } == add { f(n: PositiveInteger): PrimeField(n) == 10::Integer::PrimeField(n) }</aldor>
fricas
Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4460571600609964226-25px001.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4460571600609964226-25px001.as", line 1: 
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.

Note that such a construction - the resulting domain depending on the function parameter - is currently illegal in Axiom. In Aldor it is fine.

I compiled it with Aldor as usual, and then loaded it into Axiom. As signature I got the slightly unusual:

fricas
)di op f
f is not a known function. FriCAS will try to list its functions which contain f in their names. This is the same output you would get by issuing )what operations f
There are possibly a great many operation names containing the substring f . Please confirm your request to have these listed by typing y or yes and then pressing Enter : Since you did not respond with y or yes the list of operation names containing f will not be displayed.

and trying it out I obtained: Axiom output parse error!

which is roughly what I expected. However, to my great surprise, if you turn on the debugger (beforehand. You always have to start a fresh axiom because of the error I told you about in my previous message) with:

  )lisp (setq |$monitorNewWorld| t)

and thus trace:

  f(1783)$Test

the final bit reads:

  protected-symbol-warn called with (NIL)..IntegerMod 1783 wants
   positiveRemainder : (%,%) -> % from  Integer
  ---->Integer----> searching op table for:
   positiveRemainder : (%,%) -> % from  Integer
  <----#<compiled-function |INT;positiveRemainder;3$;28|> Integer
  goget stuffing slot 47 of IntegerMod 1783
  <------#<compiled-function |INT;positiveRemainder;3$;28|> Integer

  PrimeField n activating lazy slot 8: Integer
  PrimeField n activating lazy slot 9: IntegerPrimesPackage Integer

  ..PrimeField n wants
   prime? : Integer -> Boolean from  IntegerPrimesPackage Integer
  ---->IntegerPrimesPackage Integer----> searching op table for:
   prime? : Integer -> Boolean from  IntegerPrimesPackage Integer
  <----#<compiled-function |PRIMES;prime?;IB;4|>(IntegerPrimesPackage,Integer)
  goget stuffing slot 10 of PrimeField n
  <------#<compiled-function |PRIMES;prime?;IB;4|>(IntegerPrimesPackage,Integer)

which clearly tells you, that the calculation is done alright, only the signature interferes with success.

Any ideas?

Peter said, that it's on the interpreter side. You can read the whole thread on http://lists.gnu.org/archive/html/axiom-developer/2005-01/msg00154.html

Concerning his patches, Peter also pointed out that

  • aldor "extend" does not work
  • The algebra defined in libaxiom.al is not current, and for it to be rebuilt various .as files need to be available to the build process (axextend.as and friends)
  • exported attributes from aldor domains are explicitly killed off by this patch (it's probably easy to fix, just no time at the moment).
  • Only tested the most trivial domains he could find.

property change --kratt6, Sat, 15 Oct 2005 06:04:09 -0500 reply
Severity: normal => wishlist

Note that with Peter''s patches the error message System Error: Unfortunate use of dependant type is directly triggered by the code produced by aldor. In the lisp file, there line 201 reads:
    (|Halt| (the |SInt| 101))))

|Halt| is a function in foam_l.lisp. I do not know why the call to this error was not produced with the old libaxiom.al. Would be great if somebody could help here...

Martin