diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-21 16:13:58 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-21 16:13:58 +0000 |
| commit | 9545a01076cc7b79d0d3278b1ba12e3249149716 (patch) | |
| tree | b66405b976619de4a3d2d45369c034629c06ac87 /plugins/extraction/haskell.ml | |
| parent | 63fe9ca9438693fcf4d601c05f77a4db50588b40 (diff) | |
Extract Inductive is now possible toward non-inductive types (e.g. nat => int)
For instance:
Extract Inductive nat => int [ "0" "succ" ]
"(fun fO fS n => if n=0 then fO () else fS (n-1))".
See Extraction.v for more details and caveat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/haskell.ml')
| -rw-r--r-- | plugins/extraction/haskell.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 84202d539..c1ed62b34 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -146,6 +146,14 @@ let rec pp_expr par env args = assert (args=[]); pp_par par (pp_global Cons r ++ spc () ++ prlist_with_sep spc (pp_expr true env []) args') + | MLcase (_,t, pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr true env [] t) | MLcase ((_,factors),t, pv) -> apply (pp_par par' (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ |