Generate Coq types for ROS messages

Overview

The topics and messages we used so far, e.g. in specification and proofs, need not be exactly the ones used by the Robot Operating System (ROS). This enables one to not worry about ROS specific details of encoding when reasoning about a cyber-physical system. However, to run these programs via the ROS, these high level topics and messages need to be mapped to formats that ROS understands, as explained in the next chapter.

Note that agents (nodes) for ROS can be written in a variety of languages such as C++, Python, Java, Haskell. For example, the ROSCoq program (software agent) in our example needs to send messages to the device drivers of the robot, which are not written in Coq. To enable this cross language interoperation ROS defines a language independent protocol (publish/subscribe) and a format for the messages that ROS agents (nodes) exchange, and how such messages need to be (de-)serialized. ROS messages types are specified as language-independent .msg files. Client libraries for a language are responsible converting a .msg file to language specific code, to create, (de-)serialize such messages in accordance with ROS guidelines, so that the agents (possibly written in a different) receiving them can correctly interpret such messages.

The roshask Haskell client library for ROS already provides a mechanism to generate Haskell types and utilities for ROS .msg files. Our fork of roshask also generates Coq wrappers for such Haskell types. The 3 files below illustrate the Haskell and Coq types generated for the message type geometry_msgs.Vector3.msg
Vector3.hs
Vector3.v
The Coq file also has directives for the compiler (extractor) from Coq to Nuprl, to ensure that the Coq type is extracted to the corresponding Haskell type, which come with (de-)serialization routines.

The roshask provides the roshask executable for generating message types. Our modifications don't change the way it is invoked, which is described when it is called without any arguments. Our modifications merely generate Coq types as well whenever Haskell types are generated, and compile the resultant Coq files.

Steps

Please ensure that you have installed our fork of roshask. Perhaps the easiest way to use roshask to generate message types is to write a package.xml which lists (as dependencies) the ROS packages exporting the required message types as .msg files. Here is the package.xml file for our example, which needs the above mentioned Vector3 message from the geometry_msgs ROS package. Then running roshask dep in the directory containing package.xml will generate and compile the Haskell and Coq files.

The generated Haskell files will be automatically registered with the ghc, and thus that Haskell compiler will know where to find such files. Coq files are not registered in a similar way. However, roshask dep will output lines of the form which begin with "Coq LoadPath" and contain the name of the relevant ROS package, which is Geometry_msgs in our example : Coq LoadPath : -R /home/abhishek/.cabal/share/x86_64-linux-ghc-7.6.3/roshask-0.3/Geometry_msgs/Ros Ros This line specifies the options needed to be passed to the Coq compiler so that it can find the generated Coq files.

##TODO The generated Coq files may fail to compile, because the generated Coq source file may depend on Coq types that haven't yet been defined. However, It should be easy to define them. If the Coq file for your ROS type doesn't compile, please create an issue stating that ROS .msg file, and I will be happy to define enough Coq types to make the Coq file for your .msg file compile.