diff options
author | Nickolai Zeldovich <nickolai@csail.mit.edu> | 2016-02-08 16:08:10 -0500 |
---|---|---|
committer | Nickolai Zeldovich <nickolai@csail.mit.edu> | 2016-02-19 16:02:30 -0500 |
commit | 8bac7b9e0a149cd8f374ac63f33ec4ecfc5ae2d2 (patch) | |
tree | 8a1617989f89e2c20b688b2be00b9423220587de /library/declaremods.ml | |
parent | a4b457bef4290fed3f2869795f1539de53b3805a (diff) |
Fix Haskell extraction for terms over 45 characters long
The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name. In particular, with a term
name of 46 characters or more, the following Coq code:
Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
Extraction Language Haskell.
Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.
would produce:
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
Unit
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
Tt
which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).
This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).
Diffstat (limited to 'library/declaremods.ml')
0 files changed, 0 insertions, 0 deletions