more on coding up coq type generation. up next: 1) map ROS-primitive haskell types such as P.Double below to the corresponding Coq types in RoshaskTypes.v 2) auto adding Coq imports for non primitive field types, e.g. in Twist.v needs to import Vector.v
more on coding up coq type generation.
up next:
1) map ROS-primitive haskell types such as P.Double below to the corresponding Coq types in RoshaskTypes.v
2) auto adding Coq imports for non primitive field types, e.g. in Twist.v needs to import Vector.v

The corresponding importing  problem in the Haskell side is  worse.
Perhaps we can put autogenerated ROS message types this in a dedicated Coq namespace and use Coq dependencies to infer the dependencies of the Haskell extract
on the corresponding autogenerated haskell messages types.

Below is the autogenerated .v file for Vector3.
It should look like:
https://github.com/aa755/ROSCoq/blob/eb7762c76b096e1e102a4e7f2ccead21ce21e761/src/shim/Haskell/ROSVector3Msg.v
Except P.Dpuble, it seems to do so already.
How to auto compile these auto generated .v files? use coq_makefile? scons?

Extraction Language Haskell.
Require ROSCOQ.shim.Haskell.RoshaskNodeMonad.
Require ROSCOQ.shim.Haskell.RoshaskTopic.
Require ROSCOQ.shim.Haskell.RoshaskMsg.
Require ROSCOQ.shim.Haskell.RoshaskTypes.
Require String.

Record Vector3 :=  { _x : P.Double
                   ; _y : P.Double
                   ; _z : P.Double
                   }

Extract Inductive Vector3 => "Ros.Geometry_msgs.Vector3.Vector3" [ "Ros.Geometry_msgs.Vector3.Vector3" ].
Extract Constant _x => "Ros.Geometry_msgs.Vector3._x" .
Extract Constant _y => "Ros.Geometry_msgs.Vector3._y" .
Extract Constant _z => "Ros.Geometry_msgs.Vector3._z" .
Extract Constant  subscribe => "(Ros.Node.subscribe)".
Extract Constant  publish => "(Ros.Node.advertise)".

aa755/roshask,aa755/roshask