> | On Thu, Apr 2, 2009 at 12:06 AM, Gabriel Dos Reis wrote:
> | > If you're not proposing to export the Rep, then your proposal is a bit
> | > obscure to me. Would you mind clarifying why the above does not
> | > amount to exporting the Rep of SomeDomain?
> | >
> Bill Page wrote:
> | Because it is not part of the 'with' clause and appears to the right
> | of ==.
>
On Thu, Apr 2, 2009 at 10:38 AM, Gabriel Dos Reis wrote:
> But with your construct, in the capsule I would be able to tell what
> Rep(SomeDomain) is. That reveals the Rep of SomeDomain, and
> effectively exports it.
>
Let's take a real example from 'src/algebra/tree.spad.pamphlet':
<<domain BSTREE BinarySearchTree>>=
)abbrev domain BSTREE BinarySearchTree
++ Description: BinarySearchTree(S) is the domain of
++ a binary trees where elements are ordered across the tree.
++ A binary search tree is either empty or has
++ a value which is an S, and a
++ right and left which are both BinaryTree(S)
++ Elements are ordered across the tree.
BinarySearchTree(S: OrderedSet): Exports == Implementation where
Exports == BinaryTreeCategory(S) with
binarySearchTree: List S -> %
++ binarySearchTree(l) \undocumented
insert_!: (S,%) -> %
++ insert!(x,b) inserts element x as leaves into binary search tree b.
insertRoot_!: (S,%) -> %
++ insertRoot!(x,b) inserts element x as a root of binary search tree b.
split: (S,%) -> Record(less: %, greater: %)
++ split(x,b) splits binary tree b into two trees, one with
elements greater
++ than x, the other with elements less than x.
Implementation == BinaryTree(S) add
Rep := BinaryTree(S)
binarySearchTree(u:List S) ==
null u => empty()
tree := binaryTree(first u)
for x in rest u repeat insert_!(x,tree)
tree
insert_!(x,t) ==
empty? t => binaryTree(x)
x >= value t =>
setright_!(t,insert_!(x,right t))
t
setleft_!(t,insert_!(x,left t))
t
split(x,t) ==
empty? t => [empty(),empty()]
x > value t =>
a := split(x,right t)
[node(left t, value t, a.less), a.greater]
a := split(x,left t)
[a.less, node(a.greater, value t, right t)]
insertRoot_!(x,t) ==
a := split(x,t)
node(a.less, x, a.greater)
@
Apparently your analysis would require that 'BinaryTree(S)' is
"effectively exported" but of course it is not. In my proposal one
would write:
Implementation == Rep BinaryTree(S) add
binarySearchTree(u:List S) ==
null u => empty()
...
I can see no reason why this might imply to someone that BinaryTree(S)
is somehow "exported" when the example above does not.
--
But there is an interesting problem in the example above.
BinaryTree(S) is *both* add-inherited and specified as Rep. This is a
mistake. We should not say that a BinarySearchTree is represented as a
BinaryTree but rather that a BinarySearchTree is a particular class of
BinaryTree, i.e one where the nodes of the tree are in a specific
order. They share the same underlying representation but they are
constructed by a slightly different set of methods.
The Rep of BinaryTree(S) is 'List Tree S':
<<domain BTREE BinaryTree>>=
)abbrev domain BTREE BinaryTree
++ Description: \spadtype{BinaryTree(S)} is the domain of all
++ binary trees. A binary tree over \spad{S} is either empty or has
++ a \spadfun{value} which is an S and a \spadfun{right}
++ and \spadfun{left} which are both binary trees.
BinaryTree(S: SetCategory): Exports == Implementation where
Exports == BinaryTreeCategory(S) with
binaryTree: S -> %
++ binaryTree(v) is an non-empty binary tree
++ with value v, and left and right empty.
binaryTree: (%,S,%) -> %
++ binaryTree(l,v,r) creates a binary tree with
++ value v with left subtree l and right subtree r.
Implementation == add
Rep := List Tree S
t1 = t2 == (t1::Rep) =$Rep (t2::Rep)
...
Note: This code is currently the same in both FriCAS and OpenAxiom.
Since BinarySearchTree is a particular class of BinaryTree for
consistency in BinarySearchTree I would expect to see:
Implementation == BinaryTree(S) add
Rep == List Tree S
Note: The 2nd line above is not required in OpenAxiom.
But then we must change the implementation slightly.
binarySearchTree(u:List S) ==
tree := empty()
for x in u repeat insert_!(x,tree)
tree
insert_!(x,t) ==
empty? t => node(t,x,t)
x >= value t =>
setright_!(t,insert_!(x,right t))
t
setleft_!(t,insert_!(x,left t))
t
> | Similarly, the operations of OldDomain are not automatically
> | exported in
> |
> | Foo(...): with
> | ...
> | == OldDomain add
> | ... rep ... per ...
> |
That is my main point. The next paragraph in my email was misplaced. I
am sorry for the resulting confusion.
> | The result is exactly the same as if I had written:
> |
> | Foo(...): with
> | ...
> | == add
> | Rep==SomeDomain
> | ... rep ... per ...
>
> No, the result is not the same. In the second form, you'll have to
> write bunch of functions (for Foo) that implement functions
> implemented by OldDomain and exported by both.
>
I only meant to repeat here that the intended semantics of
> # Foo(...): with
> # ...
> # == Rep(SomeDomain) add
> # ... rep ... per ...
is exactly the same as writing:
> | Foo(...): with
> | ...
> | == add
> | Rep==SomeDomain
> | ... rep ... per ...
Regards,
Bill Page.
------------------------------------------------------------------------------
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
