cv translator: support num_map in datatypes

[xrchz]

Although sptrees are supported in general by the cv translator, they are not supported in datatypes:

Theory fr
Ancestors
  cv_std sptree
Libs
  cv_typeLib cv_transLib

Datatype:
  foo = C1 | C2 (foo num_map)
End

val th = from_to_thm_for “:foo”

raises HOL_ERR {message = "simp_from_eq can't do: spt", origin_function = "failwith", origin_structure = "??", source_location = Loc_Unknown}

This issue is a feature request: add support for translating sptrees in datatypes.

[mn200]

This will get done as part of the wider project to BNF-ify our datatype definition package. I'll add that issue and make this a sub-part (which should amount to making sure we can register sptrees as a BNF).

[mn200]

In fact, the existing #266 is that overarching issue.