[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: [Axiom-mail] Spad and inductive types
From: |
Bill Page |
Subject: |
RE: [Axiom-mail] Spad and inductive types |
Date: |
Mon, 7 May 2007 03:32:59 -0400 |
On May 7, 2007 2:28 AM Martin Rubey writes:
>
> Gabriel Dos Reis writes:
>
> > 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?
>
> I'm very sorry, but I do not understand the code below.
> Could you describe what it is supposed to do? I guess: Expr
> is the name of the type (= domain?) you want to create, and
> it exports a single operation called "eval", which returns an
> integer. But what is MkInt, MkAdd and MkMul?
> Perhaps you want to say that an element in Expr can be of three
> forms, namely MkInt, MkAdd or MkMul?
>
...
> > ------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<-------
Yes, I think what Gaby wants might be written something like this
in SPAD:
)abbrev domain EX Expr
Expr:with
eval: % -> Integer
coerce: Integer -> %
_+: (%,%) -> %
_-: (%,%) -> %
== add
MkInt ==> Integer
MkAdd ==> Record(lAdd:%,rAdd:%)
MkMul ==> Record(lMul:%,rMul:%)
Rep ==> Union(MkInt,MkAdd,MkMul)
eval(x:%) ==
i := x pretend Rep
i case MkInt => i
i case MkAdd => eval(i.lAdd) + eval(i.rAdd)
i case MkMul => eval(i.lMul) * eval(i.rMul)
-- coerce(n) == autoCoerce(n)$Rep pretend %
-- x + y == autoCoerce([x,y]$MkAdd)$Rep pretend %
-- x * y == autoCoerce([x,y]$MkMul)$Rep pretend %
--------
This compiles eval, but I have a problem. Obviously one would
like to create members of this domain. But I can not seem to
persuade SPAD to compile my defintions of coerce, + and *. SPAD
tells me: Cannot pretend ...
I don't understand that. Perhaps you can see a way around it?
Regards,
Bill Page.
- [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/06
- Re: [Axiom-mail] Spad and inductive types, Martin Rubey, 2007/05/07
- RE: [Axiom-mail] Spad and inductive types,
Bill Page <=
- Re: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/07
- RE: [Axiom-mail] Spad and inductive types, Bill Page, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Ralf Hemmecke, 2007/05/08
- RE: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Ralf Hemmecke, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Ralf Hemmecke, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/08