diff options
Diffstat (limited to 'contrib/extraction/haskell.ml')
| -rw-r--r-- | contrib/extraction/haskell.ml | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index c4ed364a..f924396c 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml 7653 2005-12-16 04:12:26Z letouzey $ i*) +(*i $Id: haskell.ml 8930 2006-06-09 02:14:34Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -106,7 +106,7 @@ let rec pp_type par vl t = | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) - | Tdummy -> str "()" + | Tdummy _ -> str "()" | Tunknown -> str "()" | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" in @@ -210,7 +210,7 @@ and pp_function env f t = (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ hov 2 (pp_expr false env' [] t')) - + (*s Pretty-printing of inductive types declaration. *) let pp_comment s = str "-- " ++ s ++ fnl () @@ -289,12 +289,16 @@ let pp_decl mpl = else str "=" ++ spc () ++ pp_type false l t in hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl () - | Dfix (rv, defs,_) -> - let ppv = Array.map pp_global rv in - prlist_with_sep (fun () -> fnl () ++ fnl ()) - (fun (pi,ti) -> pp_function (empty_env ()) pi ti) - (List.combine (Array.to_list ppv) (Array.to_list defs)) - ++ fnl () ++ fnl () + | Dfix (rv, defs, typs) -> + let max = Array.length rv in + let rec iter i = + if i = max then mt () + else + let e = pp_global rv.(i) in + e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () + ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl () + ++ iter (i+1) + in iter 0 | Dterm (r, a, t) -> if is_inline_custom r then mt () else |