Spad and inductive types

Gabriel Dos Reis <[email protected]>
Newsgroups gmane.comp.mathematics.axiom.user
Organization Texas A&M University, Department of Computer Science
Message-ID <[email protected]>
Hi,

  While writing a tutotial on programming with Spad, I realize that
I don't have a good way to present inductive types in Spad.  I know
what they would like in my ideal Spad, but we don't have that ideal
Spad yet.  So, I'm asking here how you would write inductive types
in today Spad.

  For concretness, here is a very classic example of inductive type
along with a function working on expression of such type, written in
both Haskell and New Boot.  How would you best write that in Spad?


------8<----- Begin Haskell code ------8<-----
data Expr = MkInt Int
          | MkAdd Expr Expr
	  | MkMul Expr Expr

eval::Expr -> Int
eval (MkInt i) = i
eval (MkAdd x y) = (eval x) + (eval y)
eval (MkMul x y) = (eval x) * (eval y)
------8<----- End Haskell code ------8<-------


Here is the same thing written in New Boot

------8<----- Begin Boot code ------8<-----
structure Expr == 
   MkInt(Integer)
   MkAdd(Expr, Expr)
   MkMul(Expr, Expr)

eval e ==
  case e of
     MkInt(i) => i
     MkAdd(x, y) => eval(x) + eval(y)
     MkMul(x, y) => eval(x) * eval(y)
     otherwise => error "should not happen"
------8<----- End Boot code ------8<-------


For the curious, the above New Boot code is translated as
shown below.

How would you write that in Spad.  Please, keep the discussion
on axiom-mail.

Thanks!

-- Gaby
 
; structure Expr == 
;    MkInt(Integer)
;    MkAdd(Expr, Expr)
;    MkMul(Expr, Expr)
 
(DEFUN |MkInt| #0=(|bfVar#1|) (CONS '|MkInt| (LIST . #0#)))
(DEFUN |MkAdd| #0=(|bfVar#2| |bfVar#3|) (CONS '|MkAdd| (LIST . #0#)))
(DEFUN |MkMul| #0=(|bfVar#4| |bfVar#5|) (CONS '|MkMul| (LIST . #0#)))
 
; eval e ==
;   case e of
;      MkInt(i) => i
;      MkAdd(x, y) => eval(x) + eval(y)
;      MkMul(x, y) => eval(x) * eval(y)
;      otherwise => error "should not happen"
 
(DEFUN |eval| (|e|)
  (PROG (|bfVar#7| |bfVar#6|)
    (RETURN
      (PROGN
        (SETQ |bfVar#6| |e|)
        (SETQ |bfVar#7| (CDR |bfVar#6|))
        (CASE (CAR |bfVar#6|)
          (|MkInt| (LET ((|i| (CAR |bfVar#7|))) |i|))
          (|MkAdd| (LET ((|x| (CAR |bfVar#7|)) (|y| (CADR |bfVar#7|)))
                     (+ (|eval| |x|) (|eval| |y|))))
          (|MkMul| (LET ((|x| (CAR |bfVar#7|)) (|y| (CADR |bfVar#7|)))
                     (* (|eval| |x|) (|eval| |y|))))
          (T (|error| '|should not happen|)))))))
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.