diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-04-05 01:14:42 -0400 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-08 12:01:30 +0200 |
| commit | 19ca8f80e7e35e8f6c41c99bd311b3c7df2033e2 (patch) | |
| tree | b1e7c82be48f473a15b476cce133d1df88173289 | |
| parent | c595d5cc3105b0bec4faa0a5ed7e1c37de0c5e2c (diff) | |
add ExtrHaskellBasic.v to mirror ExtrOcamlBasic.v
| -rw-r--r-- | plugins/extraction/ExtrHaskellBasic.v | 15 | ||||
| -rw-r--r-- | plugins/extraction/vo.itarget | 1 |
2 files changed, 16 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v new file mode 100644 index 000000000..294d61023 --- /dev/null +++ b/plugins/extraction/ExtrHaskellBasic.v @@ -0,0 +1,15 @@ +(** Extraction to Haskell : use of basic Haskell types *) + +Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive unit => "()" [ "()" ]. +Extract Inductive list => "([])" [ "([])" "(:)" ]. +Extract Inductive prod => "(,)" [ "(,)" ]. + +Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. + +Extract Inlined Constant andb => "(Prelude.&&)". +Extract Inlined Constant orb => "(Prelude.||)". +Extract Inlined Constant negb => "Prelude.not". diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget index 1fe09f6fa..f04890480 100644 --- a/plugins/extraction/vo.itarget +++ b/plugins/extraction/vo.itarget @@ -1,3 +1,4 @@ +ExtrHaskellBasic.vo ExtrOcamlBasic.vo ExtrOcamlIntConv.vo ExtrOcamlBigIntConv.vo |