Perhaps you have seen the wooden dolls made in Russia that nest within
each other. Create an abstract data type (ADT) using a signature
and structure in ML to model a wooden-doll factory. You will need
a type doll and a type box. There will be
the following operations on the ADT:
- baby
-
The client of a factory can ask for the creation of a "baby" doll,
one that is solid wood and contains no other doll.
- shell
-
The client
can return any doll d to the factory and ask for a "shell" doll,
a new, hollow doll d' that contains d.
- box
-
The client can pass a list of dolls back to the factory
and ask for a shipping carton (box) containing them all.
- weight
-
The weight of a baby doll is 10 grams. The weight of a shell doll
containing n dolls 10(n+1) plus the weight of all
the dolls contained.
The weight of a box is 1000 grams plus the weight of the dolls contained.
The client can ask for the weight of any box.
There are no other operations on dolls and boxes.
- Write the ML signature that models a doll factory.
- Write a reference implementation: that is, an ML structure
that implements this signature as straightforwardly as possible.
In your reference implementation, creation of a doll or construction
of a box should just be the application of a data constructor.
- Write a structure that implements this signature more
efficiently.
For each type in the signature, use as efficient a representation as
possible, given the set of operations required.
- Prove the equivalence of your two implementations.
Please show the simulation relation ~
as precisely as you can.
Hint: Instead of defining ~ in closed form
the way the Queue relation R in lecture was defined,
you may give an inductive definition.
Note:
A baby doll weighs 10 grams.
A doll shell(baby) weighs 30 grams: 20 for the shell, 10 for the
baby.
The doll shell(shell(baby))
weighs 60 grams: 30 for the outer shell,
20 for the inner shell, 10 for the baby.
If I create
a = baby
b = shell(a)
c = baby
d = shell(c)
e = shell(d)
Then I can create a box with the list [b,e].