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 noncanonical method is defined as a "fun" definition using the
pattern matching facilities of ML. Create one alternative per
axiom.