Compiling and Running Haskell extracts of ROSCoq software agents

Fixing and compiling the Haskell Extract

Coq's mechanism for extracting Coq programs to Haskell has some minor imperfections. The icreateMoveToLoc.hs target in the Makefile illustrates these fixes. Here, we explain its contents.

Adding Imports

It is a known issue with Coq that the generated Haskell file may be missing some imports. One has to manually add the missing imports. The script for our example may be a good way to automate this addition.

Other fixes

When using constructive reals, one function (Qplus_strext0) is known to extract incorrectly to Haskell. Find its definition and in the type declaration, change Prelude.Either () () to Prelude.Either Any Any

Adding a main function

We showed how to create programs of type Node unit from ROSCoq software agents. When extracted, these programs will have type Node () in Haskell. The Node monad is defined in roshask, the Haskell bindings for the Robot Operating System. roshask provides the function Ros.Node.runNode of type Node () -> IO (). It can be used to write a main function of type IO (). This line adds a main function to the extract of our example.

Compiling

The result of the above fixes is known to compile with GHC.

Running it

Some familiarity with the basic graph concepts of the Robot Operating System (ROS) is needed to understand these steps

1. Start roscore: abhishek@abhishek-desktop:~$ roscore
2. Start the drivers of the robot. For our example which uses the iRobot create drivers, the following works:
   abhishek@abhishek-desktop:~$ roslaunch turtlebot_bringup minimal.launch
3. The above drivers provide an API that is different from our axiomatization of the robot, which was based on the old drivers. The difference is that the old driver kept following the last received velocity command indefinitely, whereas the new one does that for only 1/10 seconds. So we wrote a wrapper which provides the old interface by repeating the last message at 10Hz. To start our wrapper, cd to ROSCoq/roshask/Examples/Turtle/src and run ./icreateDriver. At the first time, you will need to produce this executable using ghc IcreateDriver.hs -main-is IcreateDriver -o icreateDriver
4. Running the ROSCoq program: ./icreateMoveToLoc
5. Testing it using the external agent: rostopic pub /targetpos geometry_msgs/Vector3 1 1 0 . This starts a ROS node which publishes (1,1,0) to the topic /targetpos which is subscribed by the above ROSCoq program. That program will receive it and send four messages to the icreateDriver on the topic /icreate_cmd_vel, so that the robot moves to (1,1) relative to its original position. One can log all the communication using rostopic echo /icreate_cmd_vel and rostopic echo /targetpos