help links subscribe changes refresh edit

	IssueTracker
#423 showSummary fails ←	↑	→ #425 confusion over Category

#424 Interpreter code generation failed

Edit detail for #424 Interpreter code generation failed revision 5 of 11

	1 2 3 4 5 6 7 8 9 10 11
Editor: gdr Time: 2008/05/28 22:29:18 GMT-7
Note: category valued functions

added:

However, in the interpreter we should probably try to
accomodate for as much as we can because we can *also*
do a small step semantics, e.g. interpret literally the codes.

Going back to your problem, an issue here is with what the type of
Type should be.  Currently, OpenAxiom says that Type has type Type, 
instead of Category:
\begin{axiom}
Type
typeOf Type
\end{axiom}

Another option might be to say that Type has type Category.  That
would make your function OK.  Note that the following works fine

\begin{axiom}
ST2(x: Integer): Category == (x=0 => SetCategory; Ring)

ST2 0
ST2 1
\end{axiom}

In OpenAxiom? one should be able to write a function that returns a 'Category':

axiomST(x:Integer):Category == (x=0 => SetCategory;Type)
   Function declaration ST : Integer -> Category has been added to
      workspace.

Type: Void

axiomST(0)
   Internal Error
   Interpreter code generation failed for expression
      (IF (= |#1| 0) |SetCategory| |Type|)

but we get the error message:

   Internal Error
   Interpreter code generation failed for expression
      (IF (= |#1| 0) |SetCategory| |Type|)

This is ok for functions that return 'Domain':

axiomFI(x:Integer):Domain == (x=0 => Float;Integer)
   Function declaration FI : Integer -> Domain has been added to
      workspace.

Type: Void

axiom
FI(0)

axiom

Compiling function FI with type Integer -> Domain 
; (DEFUN |*1;FI;1;initial| ...) is being compiled.
;; The variable |*1;FI;1;initial;MV| is undefined.
;; The compiler will assume this variable is a global.

(1)

Type: Domain

axiom
FI(1)

(2)

Type: Domain

... --Bill Page, Wed, 28 May 2008 17:07:17 -0700 reply

Axiom Version: => /usr/local/lib/open-axiom/x86_64-unknown-linux/1.2.0-2008-05-25

category valued functions --gdr, Wed, 28 May 2008 17:52:23 -0700 reply

Because the function of categories is to oversee domains, it is much much harder to have category valued functions with the current compilation scheme.

However, in the interpreter we should probably try to accomodate for as much as we can because we can also do a small step semantics, e.g. interpret literally the codes.

Going back to your problem, an issue here is with what the type of Type should be. Currently, OpenAxiom? says that Type has type Type, instead of Category:

axiom
Type

(3)

Type: Type

axiom
typeOf Type

(4)

Type: Type

Another option might be to say that Type has type Category. That would make your function OK. Note that the following works fine

axiomST2(x: Integer): Category == (x=0 => SetCategory; Ring)
   Function declaration ST2 : Integer -> Category has been added to
      workspace.

Type: Void

axiom
ST2 0

axiom

Compiling function ST2 with type Integer -> Category 
; (DEFUN |*1;ST2;1;initial| ...) is being compiled.
;; The variable |*1;ST2;1;initial;MV| is undefined.
;; The compiler will assume this variable is a global.

(5)

Type: Category

axiom
ST2 1

(6)

Type: Category