diff options
| author | letouzey | 2011-01-07 13:50:57 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-07 13:50:57 +0000 |
| commit | 5056083eb0b6ad626fe24d9c85370e09c8c2db91 (patch) | |
| tree | 6796140d6a5f57d01773072323a9a11a1fc79127 /plugins/extraction | |
| parent | 5db7b802bdf82f67b91fcf7371194400852595ea (diff) | |
Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/haskell.ml | 19 | ||||
| -rw-r--r-- | plugins/extraction/scheme.ml | 21 |
2 files changed, 22 insertions, 18 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 6ca4488264..9eeb25acf7 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -305,15 +305,16 @@ let pp_decl = function in hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () | Dfix (rv, defs, typs) -> - let max = Array.length rv in - let rec iter i = - if i = max then mt () - else - let e = pp_global Term rv.(i) in - e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () - ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 () - ++ iter (i+1) - in iter 0 + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + prvecti + (fun i r -> + if is_inline_custom r then mt () + else + names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () + ++ pp_function (empty_env ()) names.(i) defs.(i) ++ fnl2 ()) + rv | Dterm (r, a, t) -> if is_inline_custom r then mt () else diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 77c8e944e3..612da13499 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -161,15 +161,18 @@ let pp_decl = function | Dind _ -> mt () | Dtype _ -> mt () | Dfix (rv, defs,_) -> - let ppv = Array.map (pp_global Term) rv in - prvect_with_sep fnl - (fun (pi,ti) -> - hov 2 - (paren (str "define " ++ pi ++ spc () ++ - (pp_expr (empty_env ()) [] ti)) - ++ fnl ())) - (array_map2 (fun p b -> (p,b)) ppv defs) ++ - fnl () + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + prvecti + (fun i r -> + if is_inline_custom r then mt () + else + hov 2 + (paren (str "define " ++ names.(i) ++ spc () ++ + (pp_expr (empty_env ()) [] defs.(i))) + ++ fnl ()) ++ fnl ()) + rv | Dterm (r, a, _) -> if is_inline_custom r then mt () else |