ROSCOQ.shim.Haskell.RoshaskTypes

ROS has a large variety of primitive message types. These can be composed into record like constructs. A collection of the primitive ROS message types can be found at http://wiki.ros.org/std_msgs roshask already generates those message types in Haskell and handles serialization and deserialization to/from messages. We want to reuse that effort. This means, for example, that the type for ROS Int8 in Coq should extract to whatever roshask uses for that type, which is Data.Int.Int8. Still, there remains a choice in Coq. We can either axiomatize the haskell type Data.Int.Int8 and its operations. An alternate approach will be to use a concrete, perhaps more logical representation in Coq. The extraction directives will be the same, regardless of the choice. The latter approach might be convenient for Coq proofs, e.g. one can do proofs by computation. For now, we are using the former choice.

this must extracted what roshask uses for ROS float type. One way to find out is to look at what roshask generates for geometry_msgs/Vector3.