ADTs specified with Algebraic semantics, Guttag's hueristic,
can be directly implemented in ML... almost a syntactic
transformation.
-
The canonical methods of your specs are expressed in an ML "datatype"
definition
-
Each non-canonical method is defined as a "fun" definition using the
pattern matching facilities of ML. Create one alternative per
axiom.