diff options
Diffstat (limited to 'plugins/extraction/ocaml.ml')
| -rw-r--r-- | plugins/extraction/ocaml.ml | 759 |
1 files changed, 759 insertions, 0 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml new file mode 100644 index 00000000..30004677 --- /dev/null +++ b/plugins/extraction/ocaml.ml @@ -0,0 +1,759 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*s Production of Ocaml syntax. *) + +open Pp +open Util +open Names +open Nameops +open Libnames +open Table +open Miniml +open Mlutil +open Modutil +open Common +open Declarations + + +(*s Some utility functions. *) + +let pp_tvar id = + let s = string_of_id id in + if String.length s < 2 || s.[1]<>'\'' + then str ("'"^s) + else str ("' "^s) + +let pp_tuple_light f = function + | [] -> mt () + | [x] -> f true x + | l -> + pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l) + +let pp_tuple f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l) + +let pp_boxed_tuple f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l)) + +let pp_abst = function + | [] -> mt () + | l -> + str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ + str " ->" ++ spc () + +let pp_parameters l = + (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) + +let pp_string_parameters l = + (pp_boxed_tuple str l ++ space_if (l<>[])) + +(*s Ocaml renaming issues. *) + +let keywords = + List.fold_right (fun s -> Idset.add (id_of_string s)) + [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do"; + "done"; "downto"; "else"; "end"; "exception"; "external"; "false"; + "for"; "fun"; "function"; "functor"; "if"; "in"; "include"; + "inherit"; "initializer"; "lazy"; "let"; "match"; "method"; + "module"; "mutable"; "new"; "object"; "of"; "open"; "or"; + "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true"; + "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod"; + "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] + Idset.empty + +let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") + +let preamble _ used_modules usf = + prlist pp_open used_modules ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++ + (if usf.mldummy then + str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n" + else mt ()) ++ + (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ()) + +let sig_preamble _ used_modules usf = + prlist pp_open used_modules ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt()) + +(*s The pretty-printer for Ocaml syntax*) + +(* Beware of the side-effects of [pp_global] and [pp_modname]. + They are used to update table of content for modules. Many [let] + below should not be altered since they force evaluation order. +*) + +let str_global k r = + if is_inline_custom r then find_custom r else Common.pp_global k r + +let pp_global k r = str (str_global k r) + +let pp_modname mp = str (Common.pp_module mp) + +let is_infix r = + is_inline_custom r && + (let s = find_custom r in + let l = String.length s in + l >= 2 && s.[0] = '(' && s.[l-1] = ')') + +let get_infix r = + let s = find_custom r in + String.sub s 1 (String.length s - 2) + +exception NoRecord + +let find_projections = function Record l -> l | _ -> raise NoRecord + +(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses + are needed or not. *) + +let mk_ind path s = + make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s) + +let rec pp_type par vl t = + let rec pp_rec par = function + | Tmeta _ | Tvar' _ | Taxiom -> assert false + | Tvar i -> (try pp_tvar (List.nth vl (pred i)) + with _ -> (str "'a" ++ int i)) + | Tglob (r,[a1;a2]) when is_infix r -> + pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) + | Tglob (r,[]) -> pp_global Type r + | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" -> + pp_tuple_light pp_rec l + | Tglob (r,l) -> + pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r + | Tarr (t1,t2) -> + pp_par par + (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) + | Tdummy _ -> str "__" + | Tunknown -> str "__" + in + hov 0 (pp_rec par t) + +(*s Pretty-printing of expressions. [par] indicates whether + parentheses are needed or not. [env] is the list of names for the + de Bruijn variables. [args] is the list of collected arguments + (already pretty-printed). *) + +let is_ifthenelse = function + | [|(r1,[],_);(r2,[],_)|] -> + (try (find_custom r1 = "true") && (find_custom r2 = "false") + with Not_found -> false) + | _ -> false + +let expr_needs_par = function + | MLlam _ -> true + | MLcase (_,_,[|_|]) -> false + | MLcase (_,_,pv) -> not (is_ifthenelse pv) + | _ -> false + + +(** Special hack for constants of type Ascii.ascii : if an + [Extract Inductive ascii => char] has been declared, then + the constants are directly turned into chars *) + +let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" + +let check_extract_ascii () = + try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false + +let is_list_cons l = + List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l + +let pp_char l = + let rec cumul = function + | [] -> 0 + | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) + | _ -> assert false + in str ("'"^Char.escaped (Char.chr (cumul l))^"'") + +let rec pp_expr par env args = + let par' = args <> [] || par + and apply st = pp_apply st par args in + function + | MLrel n -> + let id = get_db_name n env in apply (pr_id id) + | MLapp (f,args') -> + let stl = List.map (pp_expr true env []) args' in + pp_expr par env (stl @ args) f + | MLlam _ as a -> + let fl,a' = collect_lams a in + let fl = List.map id_of_mlid fl in + let fl,env' = push_vars fl env in + let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in + apply (pp_par par' st) + | MLletin (id,a1,a2) -> + let i,env' = push_vars [id_of_mlid id] env in + let pp_id = pr_id (List.hd i) + and pp_a1 = pp_expr false env [] a1 + and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in + hv 0 + (apply + (pp_par par' + (hv 0 + (hov 2 + (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ + spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) + | MLglob r -> + (try + let args = list_skipn (projection_arity r) args in + let record = List.hd args in + pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) + with _ -> apply (pp_global Term r)) + | MLcons(_,ConstructRef ((kn,0),1),l) + when kn = ind_ascii && check_extract_ascii () & is_list_cons l -> + assert (args=[]); + pp_char l + | MLcons (Coinductive,r,[]) -> + assert (args=[]); + pp_par par (str "lazy " ++ pp_global Cons r) + | MLcons (Coinductive,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") + | MLcons (_,r,[]) -> + assert (args=[]); + pp_global Cons r + | MLcons (Record projs, r, args') -> + assert (args=[]); + pp_record_pat (projs, List.map (pp_expr true env []) args') + | MLcons (_,r,[arg1;arg2]) when is_infix r -> + assert (args=[]); + pp_par par + ((pp_expr true env [] arg1) ++ str (get_infix r) ++ + (pp_expr true env [] arg2)) + | MLcons (_,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + if str_global Cons r = "" (* hack Extract Inductive prod *) + then tuple + else pp_par par (pp_global Cons r ++ spc () ++ tuple) + | 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 ((i,factors), t, pv) -> + let expr = if i = Coinductive then + (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) + else + (pp_expr false env [] t) + in + (try + let projs = find_projections i in + let (_, ids, c) = pv.(0) in + let n = List.length ids in + match c with + | MLrel i when i <= n -> + apply (pp_par par' (pp_expr true env [] t ++ str "." ++ + pp_global Term (List.nth projs (n-i)))) + | MLapp (MLrel i, a) when i <= n -> + if List.exists (ast_occurs_itvl 1 n) a + then raise NoRecord + else + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env + in + (pp_apply + (pp_expr true env [] t ++ str "." ++ + pp_global Term (List.nth projs (n-i))) + par ((List.map (pp_expr true env' []) a) @ args)) + | _ -> raise NoRecord + with NoRecord -> + if Array.length pv = 1 then + let s1,s2 = pp_one_pat env i pv.(0) in + apply + (hv 0 + (pp_par par' + (hv 0 + (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) + ++ spc () ++ str "in") ++ + spc () ++ hov 0 s2))) + else + apply + (pp_par par' + (try pp_ifthenelse par' env expr pv + with Not_found -> + v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ + str " | " ++ pp_pat env (i,factors) pv)))) + | MLfix (i,ids,defs) -> + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + pp_fix par env' i (Array.of_list (List.rev ids'),defs) args + | MLexn s -> + (* An [MLexn] may be applied, but I don't really care. *) + pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)")) + | MLdummy -> + str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLmagic a -> + pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) + | MLaxiom -> + pp_par par (str "failwith \"AXIOM TO BE REALIZED\"") + + +and pp_record_pat (projs, args) = + str "{ " ++ + prlist_with_sep (fun () -> str ";" ++ spc ()) + (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a) + (List.combine projs args) ++ + str " }" + +and pp_ifthenelse par env expr pv = match pv with + | [|(tru,[],the);(fal,[],els)|] when + (find_custom tru = "true") && (find_custom fal = "false") + -> + hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ + hov 2 (str "then " ++ + hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++ + hov 2 (str "else " ++ + hov 2 (pp_expr (expr_needs_par els) env [] els))) + | _ -> raise Not_found + +and pp_one_pat env i (r,ids,t) = + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in + let expr = pp_expr (expr_needs_par t) env' [] t in + try + let projs = find_projections i in + pp_record_pat (projs, List.rev_map pr_id ids), expr + with NoRecord -> + (match List.rev ids with + | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2 + | [] -> pp_global Cons r + | ids -> + (* hack Extract Inductive prod *) + (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ()) + ++ pp_boxed_tuple pr_id ids), + expr + +and pp_pat env (info,factors) pv = + let factor_br, factor_l = try match factors with + | BranchFun (i::_ as l) -> check_function_branch pv.(i), l + | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l + | _ -> MLdummy, [] + with Impossible -> MLdummy, [] + in + let par = expr_needs_par factor_br in + let last = Array.length pv - 1 in + prvecti + (fun i x -> if List.mem i factor_l then mt () else + let s1,s2 = pp_one_pat env info x in + hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ + if i = last && factor_l = [] then mt () else + fnl () ++ str " | ") pv + ++ + if factor_l = [] then mt () else match factors with + | BranchFun _ -> + let ids, env' = push_vars [anonymous_name] env in + hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br) + | BranchCst _ -> + hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + | BranchNone -> mt () + +and pp_function env t = + let bl,t' = collect_lams t in + let bl,env' = push_vars (List.map id_of_mlid bl) env in + match t' with + | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) -> + if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then + pr_binding (List.rev (List.tl bl)) ++ + str " = function" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) + else + pr_binding (List.rev bl) ++ + str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) + | _ -> + pr_binding (List.rev bl) ++ + str " =" ++ fnl () ++ str " " ++ + hov 2 (pp_expr false env' [] t') + +(*s names of the functions ([ids]) are already pushed in [env], + and passed here just for convenience. *) + +and pp_fix par env i (ids,bl) args = + pp_par par + (v 0 (str "let rec " ++ + prvect_with_sep + (fun () -> fnl () ++ str "and ") + (fun (fi,ti) -> pr_id fi ++ pp_function env ti) + (array_map2 (fun id b -> (id,b)) ids bl) ++ + fnl () ++ + hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) + +let pp_val e typ = + hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ + str " **)") ++ fnl2 () + +(*s Pretty-printing of [Dfix] *) + +let pp_Dfix (rv,c,t) = + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + let rec pp sep letand i = + if i >= Array.length rv then mt () + else if is_inline_custom rv.(i) then pp sep letand (i+1) + else + let def = + if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) + else pp_function (empty_env ()) c.(i) + in + sep () ++ pp_val names.(i) t.(i) ++ + str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) + in pp mt "let rec " 0 + +(*s Pretty-printing of inductive types declaration. *) + +let pp_equiv param_list name = function + | NoEquiv, _ -> mt () + | Equiv kn, i -> + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i)) + | RenEquiv ren, _ -> + str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name + +let pp_comment s = str "(* " ++ s ++ str " *)" + +let pp_one_ind prefix ip_equiv pl name cnames ctyps = + let pl = rename_tvars keywords pl in + let pp_constructor i typs = + (if i=0 then mt () else fnl ()) ++ + hov 5 (str " | " ++ cnames.(i) ++ + (if typs = [] then mt () else str " of ") ++ + prlist_with_sep + (fun () -> spc () ++ str "* ") (pp_type true pl) typs) + in + pp_parameters pl ++ str prefix ++ name ++ + pp_equiv pl name ip_equiv ++ str " =" ++ + if Array.length ctyps = 0 then str " unit (* empty inductive *)" + else fnl () ++ v 0 (prvecti pp_constructor ctyps) + +let pp_logical_ind packet = + pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ + fnl () ++ + pp_comment (str "with constructors : " ++ + prvect_with_sep spc pr_id packet.ip_consnames) ++ + fnl () + +let pp_singleton kn packet = + let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let l = rename_tvars keywords packet.ip_vars in + hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ + pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_comment (str "singleton inductive, whose constructor was " ++ + pr_id packet.ip_consnames.(0))) + +let pp_record kn projs ip_equiv packet = + let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let projnames = List.map (pp_global Term) projs in + let l = List.combine projnames packet.ip_types.(0) in + let pl = rename_tvars keywords packet.ip_vars in + str "type " ++ pp_parameters pl ++ name ++ + pp_equiv pl name ip_equiv ++ str " = { "++ + hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) + (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) + ++ str " }" + +let pp_coind pl name = + let pl = rename_tvars keywords pl in + pp_parameters pl ++ name ++ str " = " ++ + pp_parameters pl ++ str "__" ++ name ++ 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 names = + Array.mapi (fun i p -> if p.ip_logical then mt () else + pp_global Type (IndRef (mind_of_kn kn,i))) + ind.ind_packets + in + let cnames = + Array.mapi + (fun i p -> if p.ip_logical then [||] else + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1))) + p.ip_types) + ind.ind_packets + in + let rec pp i = + if i >= Array.length ind.ind_packets then mt () + else + let ip = (mind_of_kn kn,i) in + let ip_equiv = ind.ind_equiv, i in + let p = ind.ind_packets.(i) in + 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) + else + let s = !init in + begin + init := (fnl () ++ str "and "); + s ++ + (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ + pp_one_ind + prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ + pp (i+1) + end + end + in + let st = pp 0 in if !some then st else failwith "empty phrase" + + +(*s Pretty-printing of a declaration. *) + +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_equiv,0) i.ind_packets.(0) + | Standard -> pp_ind false kn i + +let pp_decl = function + | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dind (kn,i) -> pp_mind kn i + | Dtype (r, l, t) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids, def = + try + let ids,s = find_type_custom r in + pp_string_parameters ids, str "=" ++ spc () ++ str s + with Not_found -> + pp_parameters l, + if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" + else str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + | Dterm (r, a, t) -> + let def = + if is_custom r then str (" = " ^ find_custom r) + else if is_projection r then + (prvect str (Array.make (projection_arity r) " _")) ++ + str " x = x." + else pp_function (empty_env ()) a + in + let name = pp_global Term r in + let postdef = if is_projection r then name else mt () in + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) + | Dfix (rv,defs,typs) -> + pp_Dfix (rv,defs,typs) + +let pp_alias_decl ren = function + | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Dtype (r, l, _) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Dterm (r, a, t) -> + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) + | Dfix (rv, _, _) -> + prvecti (fun i r -> if is_inline_custom r then mt () else + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ + fnl ()) + rv + +let pp_spec = function + | Sval (r,_) when is_inline_custom r -> failwith "empty phrase" + | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Sind (kn,i) -> pp_mind kn i + | Sval (r,t) -> + let def = pp_type false [] t in + let name = pp_global Term r in + hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def) + | Stype (r,vl,ot) -> + let name = pp_global Type r in + let l = rename_tvars keywords vl in + let ids, def = + try + let ids, s = find_type_custom r in + pp_string_parameters ids, str "= " ++ str s + with Not_found -> + let ids = pp_parameters l in + match ot with + | None -> ids, mt () + | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" + | Some t -> ids, str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + +let pp_alias_spec ren = function + | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Stype (r,l,_) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Sval _ -> assert false + +let rec pp_specif = function + | (_,Spec (Sval _ as s)) -> pp_spec s + | (l,Spec s) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_spec ren s + with Not_found -> pp_spec s) + | (l,Smodule mt) -> + let def = pp_module_type [] mt in + let def' = pp_module_type [] mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') + with Not_found -> Pp.mt ()) + | (l,Smodtype mt) -> + let def = pp_module_type [] mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> Pp.mt ()) + +and pp_module_type params = function + | MTident kn -> + pp_modname kn + | MTfunsig (mbid, mt, mt') -> + let typ = pp_module_type [] mt in + let name = pp_modname (MPbound mbid) in + let def = pp_module_type (MPbound mbid :: params) mt' in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def + | MTsig (mp, sign) -> + push_visible mp params; + let l = map_succeed pp_specif sign in + pop_visible (); + str "sig " ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + fnl () ++ str "end" + | MTwith(mt,ML_With_type(idl,vl,typ)) -> + let ids = pp_parameters (rename_tvars keywords vl) in + let mp_mt = msid_of_mt mt in + let l,idl' = list_sep_last idl in + let mp_w = + List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + in + let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in + push_visible mp_mt []; + let pp_w = str " with type " ++ ids ++ pp_global Type r in + pop_visible(); + pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_type false vl typ + | MTwith(mt,ML_With_module(idl,mp)) -> + let mp_mt = msid_of_mt mt in + let mp_w = + List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl + in + push_visible mp_mt []; + let pp_w = str " with module " ++ pp_modname mp_w in + pop_visible (); + pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_modname mp + +let is_short = function MEident _ | MEapply _ -> true | _ -> false + +let rec pp_structure_elem = function + | (l,SEdecl d) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_decl ren d + with Not_found -> pp_decl d) + | (l,SEmodule m) -> + let typ = + (* virtual printing of the type, in order to have a correct mli later*) + if Common.get_phase () = Pre then + str ": " ++ pp_module_type [] m.ml_mod_type + else mt () + in + let def = pp_module_expr [] m.ml_mod_expr in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 + (str "module " ++ name ++ typ ++ str " = " ++ + (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module "^ren^" = ") ++ name + with Not_found -> mt ()) + | (l,SEmodtype m) -> + let def = pp_module_type [] m in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> mt ()) + +and pp_module_expr params = function + | MEident mp -> pp_modname mp + | MEapply (me, me') -> + pp_module_expr [] me ++ str "(" ++ pp_module_expr [] me' ++ str ")" + | MEfunctor (mbid, mt, me) -> + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type [] mt in + let def = pp_module_expr (MPbound mbid :: params) me in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def + | MEstruct (mp, sel) -> + push_visible mp params; + let l = map_succeed pp_structure_elem sel in + pop_visible (); + str "struct " ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + fnl () ++ str "end" + +let do_struct f s = + let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt () + in + let ppl (mp,sel) = + push_visible mp []; + let p = prlist_strict pp sel in + (* for monolithic extraction, we try to simulate the unavailability + of [MPfile] in names by artificially nesting these [MPfile] *) + (if modular () then pop_visible ()); p + in + let p = prlist_strict ppl s in + (if not (modular ()) then repeat (List.length s) pop_visible ()); + p + +let pp_struct s = do_struct pp_structure_elem s + +let pp_signature s = do_struct pp_specif s + +let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt () + +let ocaml_descr = { + keywords = keywords; + file_suffix = ".ml"; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = Some ".mli"; + sig_preamble = sig_preamble; + pp_sig = pp_signature; + pp_decl = pp_decl; +} + + |