In OpenAxiom one should be able to write a function that returns a 'Category': fricas (1) -> ST(x:Integer):Category == (x=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': fricas FI(x:Integer):Domain == (x=0 => Float;Integer) ... --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
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: fricas Type
Type: Category
fricas typeOf Type
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 fricas ST2(x: Integer): Category == (x=0 => SetCategory; Ring)Bill, your original example now works. Something is still inconsistent here: (1) -> ST(x:Integer):Category == (x=0 => SetCategory;Type) Function declaration ST : Integer -> Category has been added to workspace. Type: Void (2) -> A:=ST(0) Compiling function ST with type Integer -> Category ;;; *** |*1;ST;1;frame1392| REDEFINED ; (DEFUN |*1;ST;1;frame1392| ...) is being compiled. ;; The variable |*1;ST;1;frame1392;MV| is undefined. ;; The compiler will assume this variable is a global. (2) SetCategory Type: Category (3) -> B:=ST(1) (3) Type Type: Category (4) -> C:Category Category is a category, not a domain, and declarations require domains. (4) -> C:Category:=Ring Category is a category, not a domain, and declarations require domains. (4) -> C:=Ring (4) Ring Type: Category (5) -> )display type C Type of value of C: Category (5) -> X:Domain:=Ring -- Ring is not a domain (5) Ring Type: Category ------- If the type of a category-valued variable can be implicitly
made to be The code generation failure is fixed. So, I don't think is an issue any more. Status: fixed somewhere => closedThis is OpenAxiom specific issue that is fixed. |