Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to set the module name when extracting Coq to Haskell

When I extract/compile Coq to Haskell using Extraction Language Haskell. in the Coq file and running coqtop -compile mymodule.v > MyModule.hs, I get a Haskell module which starts with module Main where.

Is there an option to set the resulting Haskell module name?

I currently pipe to sed like this -

coqtop -compile mymodule.v | sed s/Main/MyModule/ > MyModule.hs

but I'm looking for a cleaner solution.

like image 251
yairchu Avatar asked Sep 14 '17 15:09

yairchu


1 Answers

You can use Extraction "file" or Extraction Library (or its variants), e.g.

Definition foo := 6*7.

Extraction Language Haskell.
Extraction "MyModule" foo.

The above produces MyModule.hs file, which starts with module MyModule where.

like image 74
Anton Trunov Avatar answered Nov 03 '22 10:11

Anton Trunov