diff options
Diffstat (limited to 'contrib/extraction/ocaml.ml')
| -rw-r--r-- | contrib/extraction/ocaml.ml | 38 |
1 files changed, 25 insertions, 13 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 483da236..35f9a83c 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml 8930 2006-06-09 02:14:34Z letouzey $ i*) +(*i $Id: ocaml.ml 9472 2007-01-05 15:49:32Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -392,7 +392,14 @@ let rec pp_Dfix init i ((rv,c,t) as fix) = (*s Pretty-printing of inductive types declaration. *) -let pp_one_ind prefix ip pl cv = +let pp_equiv param_list = function + | None -> mt () + | Some ip_equiv -> + str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv) + +let pp_comment s = str "(* " ++ s ++ str " *)" + +let pp_one_ind prefix ip ip_equiv pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = hov 2 (str " | " ++ pp_global r ++ @@ -402,13 +409,12 @@ let pp_one_ind prefix ip pl cv = prlist_with_sep (fun () -> spc () ++ str "* ") (pp_type true pl) l)) in - pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ + pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ + pp_equiv pl ip_equiv ++ str " =" ++ if Array.length cv = 0 then str " unit (* empty inductive *)" else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor (Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv)) -let pp_comment s = str "(* " ++ s ++ str " *)" - let pp_logical_ind packet = pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ fnl () ++ pp_comment (str "with constructors : " ++ @@ -422,10 +428,11 @@ let pp_singleton kn packet = pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) -let pp_record kn projs packet = +let pp_record kn projs ip_equiv packet = let l = List.combine projs packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in - str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++ + str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ + pp_equiv pl ip_equiv ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) ++ str " }" @@ -434,17 +441,20 @@ let pp_coind ip pl = let r = IndRef ip in let pl = rename_tvars keywords pl in pp_parameters pl ++ pp_global r ++ str " = " ++ - pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" + pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" ++ + fnl() ++ str "and " let pp_ind co kn ind = + let prefix = if co then "__" else "" in let some = ref false in let init= ref (str "type ") in let rec pp i = if i >= Array.length ind.ind_packets then mt () else let ip = (kn,i) in + let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in let p = ind.ind_packets.(i) in - if is_custom (IndRef (kn,i)) then pp (i+1) + if is_custom (IndRef ip) then pp (i+1) else begin some := true; if p.ip_logical then pp_logical_ind p ++ pp (i+1) @@ -453,8 +463,8 @@ let pp_ind co kn ind = begin init := (fnl () ++ str "and "); s ++ - (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) - ++ pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++ + (if co then pp_coind ip p.ip_vars else mt ()) + ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++ pp (i+1) end end @@ -468,7 +478,9 @@ let pp_mind kn i = match i.ind_info with | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i - | Record projs -> pp_record kn projs i.ind_packets.(0) + | Record projs -> + let ip_equiv = option_map (fun kn -> (kn,0)) i.ind_equiv in + pp_record kn projs ip_equiv i.ind_packets.(0) | Standard -> pp_ind false kn i let pp_decl mpl = @@ -574,7 +586,7 @@ let rec pp_structure_elem mpl = function | (l,SEmodule m) -> hov 1 (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - (* if you want signatures everywhere: *) + (*i if you want signatures everywhere: i*) (*i str " :" ++ fnl () ++ i*) (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*) str " = " ++ |