diff options
Diffstat (limited to 'contrib/extraction/ocaml.ml')
-rw-r--r-- | contrib/extraction/ocaml.ml | 704 |
1 files changed, 402 insertions, 302 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 35f9a83c..64c80a2a 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 9472 2007-01-05 15:49:32Z letouzey $ i*) +(*i $Id: ocaml.ml 10592 2008-02-27 14:16:07Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -19,10 +19,27 @@ open Table open Miniml open Mlutil open Modutil +open Common +open Declarations + (*s Some utility functions. *) -let pp_par par st = if par then str "(" ++ st ++ str ")" else st +let rec msid_of_mt = function + | MTident mp -> begin + match Modops.eval_struct (Global.env()) (SEBident mp) with + | SEBstruct(msid,_) -> MPself msid + | _ -> anomaly "Extraction:the With can't be applied to a funsig" + end + | MTwith(mt,_)-> msid_of_mt mt + | _ -> anomaly "Extraction:the With operator isn't applied to a name" + +let make_mp_with mp idl = + let idl_rev = List.rev idl in + let idl' = List.rev (List.tl idl_rev) in + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp idl') + let pp_tvar id = let s = string_of_id id in @@ -52,70 +69,12 @@ let pp_abst = function str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ str " ->" ++ spc () -let pp_apply st par args = match args with - | [] -> st - | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) - -let pr_binding = function - | [] -> mt () - | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l - -let space_if = function true -> str " " | false -> mt () - -let sec_space_if = function true -> spc () | false -> mt () - -let fnl2 () = fnl () ++ fnl () - 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 Generic renaming issues. *) - -let rec rename_id id avoid = - if Idset.mem id avoid then rename_id (lift_ident id) avoid else id - -let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) -let uppercase_id id = id_of_string (String.capitalize (string_of_id id)) - -(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *) -let pr_upper_id id = str (String.capitalize (string_of_id id)) - -(*s de Bruijn environments for programs *) - -type env = identifier list * Idset.t - -let rec rename_vars avoid = function - | [] -> - [], avoid - | id :: idl when id == dummy_name -> - (* we don't rename dummy binders *) - let (idl', avoid') = rename_vars avoid idl in - (id :: idl', avoid') - | id :: idl -> - let (idl, avoid) = rename_vars avoid idl in - let id = rename_id (lowercase_id id) avoid in - (id :: idl, Idset.add id avoid) - -let rename_tvars avoid l = - let rec rename avoid = function - | [] -> [],avoid - | id :: idl -> - let id = rename_id (lowercase_id id) avoid in - let idl, avoid = rename (Idset.add id avoid) idl in - (id :: idl, avoid) in - fst (rename avoid l) - -let push_vars ids (db,avoid) = - let ids',avoid' = rename_vars avoid ids in - ids', (ids' @ db, avoid') - -let get_db_name n (db,_) = - let id = List.nth db (pred n) in - if id = dummy_name then id_of_string "__" else id - (*s Ocaml renaming issues. *) let keywords = @@ -130,46 +89,39 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules (mldummy,tdummy,tunknown) _ = - let pp_mp = function - | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) - | _ -> assert false - in - prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules - ++ - (if used_modules = [] then mt () else fnl ()) - ++ - (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) - ++ - (if mldummy then - str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl () - else mt ()) - ++ - (if tdummy || tunknown || mldummy then fnl () else mt ()) - -let preamble_sig _ used_modules (_,tdummy,tunknown) = - let pp_mp = function - | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) - | _ -> assert false - in - prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules - ++ - (if used_modules = [] then mt () else fnl ()) - ++ - (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () - else mt()) +let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") -(*s The pretty-printing functor. *) +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 ()) -module Make = functor(P : Mlpp_param) -> struct +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()) -let local_mpl = ref ([] : module_path list) +(*s The pretty-printer for Ocaml syntax*) -let pp_global r = +let pp_global k r = if is_inline_custom r then str (find_custom r) - else P.pp_global !local_mpl r + else str (Common.pp_global k r) + +let pp_modname mp = str (Common.pp_module mp) -let empty_env () = [], P.globals () +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 @@ -187,12 +139,16 @@ let rec pp_type par vl t = | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i)) - | Tglob (r,[]) -> pp_global r + | Tglob (r,[a1;a2]) when is_infix r -> + pp_par par + (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++ + pp_rec true a2) + | Tglob (r,[]) -> pp_global Type r | Tglob (r,l) -> if r = IndRef (kn_sig,0) then pp_tuple_light pp_rec l else - pp_tuple_light pp_rec l ++ spc () ++ pp_global r + 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) @@ -206,10 +162,16 @@ let rec pp_type par vl t = 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 _ -> true + | MLcase (_,_,pv) -> not (is_ifthenelse pv) | _ -> false @@ -244,26 +206,31 @@ let rec pp_expr par env args = (try let args = list_skipn (projection_arity r) args in let record = List.hd args in - pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) - with _ -> apply (pp_global r)) + pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) + with _ -> apply (pp_global Term r)) | MLcons (Coinductive,r,[]) -> assert (args=[]); - pp_par par (str "lazy " ++ pp_global r) + 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 r ++ spc() ++ tuple ++str ")") + pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") | MLcons (_,r,[]) -> assert (args=[]); - pp_global r + 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) ++ spc () ++ str (get_infix r) ++ + spc () ++ (pp_expr true env [] arg2)) | MLcons (_,r,args') -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (pp_global r ++ spc () ++ tuple) - | MLcase (i, t, pv) -> + pp_par par (pp_global Cons r ++ spc () ++ tuple) + | MLcase ((i,factors), t, pv) -> let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else @@ -276,7 +243,7 @@ let rec pp_expr par env args = match c with | MLrel i when i <= n -> apply (pp_par par' (pp_expr true env [] t ++ str "." ++ - pp_global (List.nth projs (n-i)))) + 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 @@ -284,7 +251,7 @@ let rec pp_expr par env args = let ids,env' = push_vars (List.rev ids) env in (pp_apply (pp_expr true env [] t ++ str "." ++ - pp_global (List.nth projs (n-i))) + pp_global Term (List.nth projs (n-i))) par ((List.map (pp_expr true env' []) a) @ args)) | _ -> raise NoRecord with NoRecord -> @@ -297,11 +264,13 @@ let rec pp_expr par env args = (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) ++ spc () ++ str "in") ++ spc () ++ hov 0 s2))) - else - apply + else + apply (pp_par par' - (v 0 (str "match " ++ expr ++ str " with" ++ - fnl () ++ str " | " ++ pp_pat env i pv)))) + (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 @@ -319,10 +288,21 @@ let rec pp_expr par env args = and pp_record_pat (projs, args) = str "{ " ++ prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a) + (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 ids) env in let expr = pp_expr (expr_needs_par t) env' [] t in @@ -330,33 +310,45 @@ and pp_one_pat env i (r,ids,t) = let projs = find_projections i in pp_record_pat (projs, List.rev_map pr_id ids), expr with NoRecord -> - let args = - if ids = [] then (mt ()) - else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in - pp_global r ++ args, expr + (match List.rev ids with + | [i1;i2] when is_infix r -> + pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2 + | [] -> pp_global Cons r + | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), + expr -and pp_pat env i pv = - prvect_with_sep (fun () -> (fnl () ++ str " | ")) - (fun x -> let s1,s2 = pp_one_pat env i x in - hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv - -and pp_function env f t = +and pp_pat env (info,factors) pv = + prvecti + (fun i x -> if List.mem i factors then mt () else + let s1,s2 = pp_one_pat env info x in + hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ + (if factors = [] && i = Array.length pv-1 then mt () + else fnl () ++ str " | ")) pv + ++ + match factors with + | [] -> mt () + | i::_ -> + let (_,ids,t) = pv.(i) in + let t = ast_lift (-List.length ids) t in + hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t) + +and pp_function env t = let bl,t' = collect_lams t in let bl,env' = push_vars bl env in match t' with - | MLcase(i,MLrel 1,pv) when i=Standard -> + | MLcase(i,MLrel 1,pv) when fst i=Standard -> if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then - (f ++ pr_binding (List.rev (List.tl bl)) ++ - str " = function" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv)) + pr_binding (List.rev (List.tl bl)) ++ + str " = function" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) else - (f ++ pr_binding (List.rev bl) ++ - str " = match " ++ - pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv)) - | _ -> (f ++ pr_binding (List.rev bl) ++ - str " =" ++ fnl () ++ str " " ++ - hov 2 (pp_expr false env' [] t')) + 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. *) @@ -366,93 +358,111 @@ and pp_fix par env i (ids,bl) args = (v 0 (str "let rec " ++ prvect_with_sep (fun () -> fnl () ++ str "and ") - (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (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 = - str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ - str " **)" ++ fnl2 () + hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ + str " **)") ++ fnl2 () (*s Pretty-printing of [Dfix] *) -let rec pp_Dfix init i ((rv,c,t) as fix) = - if i >= Array.length rv then mt () - else - if is_inline_custom rv.(i) then pp_Dfix init (i+1) fix +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 e = pp_global rv.(i) in - (if init then mt () else fnl2 ()) ++ - pp_val e t.(i) ++ - str (if init then "let rec " else "and ") ++ - (if is_custom rv.(i) then e ++ str " = " ++ str (find_custom rv.(i)) - else pp_function (empty_env ()) e c.(i)) ++ - pp_Dfix false (i+1) fix - + 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 = function - | None -> mt () - | Some ip_equiv -> - str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv) +let pp_equiv param_list name = function + | NoEquiv, _ -> mt () + | Equiv kn, i -> + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (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 ip_equiv pl cv = +let pp_one_ind prefix ip_equiv pl name cnames ctyps = let pl = rename_tvars keywords pl in - let pp_constructor (r,l) = - hov 2 (str " | " ++ pp_global r ++ - match l with - | [] -> mt () - | _ -> (str " of " ++ - prlist_with_sep - (fun () -> spc () ++ str "* ") (pp_type true pl) l)) + 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 ++ 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)) + 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 () ++ + 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 (kn,0)) in let l = rename_tvars keywords packet.ip_vars in - hov 2 (str "type " ++ pp_parameters l ++ - pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++ + 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 l = List.combine projs packet.ip_types.(0) in + let name = pp_global Type (IndRef (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 ++ pp_global (IndRef (kn,0)) ++ - pp_equiv pl ip_equiv ++ str " = { "++ + str "type " ++ pp_parameters pl ++ name ++ + pp_equiv pl name ip_equiv ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) + (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) ++ str " }" -let pp_coind ip pl = - let r = IndRef ip in +let pp_coind pl name = 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 ++ 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 (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 ((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 = (kn,i) in - let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in + let ip_equiv = ind.ind_equiv, 0 in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) else begin @@ -463,8 +473,9 @@ let pp_ind co kn ind = begin init := (fnl () ++ str "and "); s ++ - (if co then pp_coind ip p.ip_vars else mt ()) - ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++ + (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 @@ -479,159 +490,248 @@ let pp_mind kn i = | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i | 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) + pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0) | Standard -> pp_ind false kn i -let pp_decl mpl = - local_mpl := mpl; - function +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) -> - if is_inline_custom r then failwith "empty phrase" - else - let pp_r = pp_global r in - let l = rename_tvars keywords l in - let ids, def = try + | 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 -> + 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" ++ spc () ++ ids ++ pp_r ++ - spc () ++ def) + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) | Dterm (r, a, t) -> - if is_inline_custom r then failwith "empty phrase" - else - let e = pp_global r in - pp_val e t ++ - hov 0 - (str "let " ++ - if is_custom r then - e ++ str " = " ++ str (find_custom r) - else if is_projection r then - let s = prvecti (fun _ -> str) - (Array.make (projection_arity r) " _") in - e ++ s ++ str " x = x." ++ e - else pp_function (empty_env ()) e a) + 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 true 0 (rv,defs,typs) - -let pp_spec mpl = - local_mpl := mpl; - function - | Sind (kn,i) -> pp_mind kn i - | Sval (r,t) -> - if is_inline_custom r then failwith "empty phrase" - else - hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++ - pp_type false [] t) - | Stype (r,vl,ot) -> - if is_inline_custom r then failwith "empty phrase" - else - 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" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def) - -let rec pp_specif mpl = function - | (_,Spec s) -> pp_spec mpl s + 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) -> - hov 1 - (str "module " ++ - P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt) + let def = pp_module_type (Some l) mt in + let def' = pp_module_type (Some l) 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) -> - hov 1 - (str "module type " ++ - P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " = " ++ fnl () ++ pp_module_type mpl None mt) - -and pp_module_type mpl ol = function + let def = pp_module_type None 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 ol = function | MTident kn -> - let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l)) + pp_modname kn | MTfunsig (mbid, mt, mt') -> - str "functor (" ++ - P.pp_module mpl (MPbound mbid) ++ - str ":" ++ - pp_module_type mpl None mt ++ - str ") ->" ++ fnl () ++ - pp_module_type mpl None mt' + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type None mt in + let def = pp_module_type None mt' in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (msid, sign) -> - let mpl = match ol, mpl with - | None, _ -> (MPself msid) :: mpl - | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl - | _ -> assert false - in - let l = map_succeed (pp_specif mpl) sign in + let tvm = top_visible_mp () in + Option.iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; + let mp = MPself msid in + push_visible mp; + 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" - + fnl () ++ str "end" + | MTwith(mt,ML_With_type(idl,vl,typ)) -> + let l = rename_tvars keywords vl in + let ids = pp_parameters l in + let mp_mt = msid_of_mt mt in + let mp = make_mp_with mp_mt idl in + let gr = ConstRef ( + (make_con mp empty_dirpath + (label_of_id ( + List.hd (List.rev idl))))) in + push_visible mp_mt; + let s = pp_module_type None mt ++ + str " with type " ++ + pp_global Type gr ++ + ids in + pop_visible(); + s ++ str "=" ++ spc () ++ + pp_type false vl typ + | MTwith(mt,ML_With_module(idl,mp)) -> + let mp_mt=msid_of_mt mt in + push_visible mp_mt; + let s = + pp_module_type None mt ++ + str " with module " ++ + (pp_modname + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp_mt idl)) + ++ str " = " + in + pop_visible (); + s ++ (pp_modname mp) + + let is_short = function MEident _ | MEapply _ -> true | _ -> false - -let rec pp_structure_elem mpl = function - | (_,SEdecl d) -> pp_decl mpl d + +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 def = pp_module_expr (Some l) m.ml_mod_expr in + let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 - (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - (*i if you want signatures everywhere: i*) - (*i str " :" ++ fnl () ++ i*) - (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*) - str " = " ++ - (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ - pp_module_expr mpl (Some l) m.ml_mod_expr) + (str "module " ++ name ++ 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) -> - hov 1 - (str "module type " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " = " ++ fnl () ++ pp_module_type mpl None m) - -and pp_module_expr mpl ol = function - | MEident mp' -> P.pp_module mpl mp' + let def = pp_module_type None 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 ol = function + | MEident mp' -> pp_modname mp' | MEfunctor (mbid, mt, me) -> - str "functor (" ++ - P.pp_module mpl (MPbound mbid) ++ - str ":" ++ - pp_module_type mpl None mt ++ - str ") ->" ++ fnl () ++ - pp_module_expr mpl None me + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type None mt in + let def = pp_module_expr None me in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEapply (me, me') -> - pp_module_expr mpl None me ++ str "(" ++ - pp_module_expr mpl None me' ++ str ")" + pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")" | MEstruct (msid, sel) -> - let mpl = match ol, mpl with - | None, _ -> (MPself msid) :: mpl - | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl - | _ -> assert false - in - let l = map_succeed (pp_structure_elem mpl) sel in + let tvm = top_visible_mp () in + let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in + push_visible mp; + 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 pp_struct s = - let pp mp s = pp_structure_elem [mp] s ++ fnl2 () in - prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s + let pp mp s = + push_visible mp; + let p = pp_structure_elem s ++ fnl2 () in + pop_visible (); p + in + prlist_strict + (fun (mp,sel) -> prlist_strict identity (map_succeed (pp mp) sel)) s let pp_signature s = - let pp mp s = pp_specif [mp] s ++ fnl2 () in - prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s - -let pp_decl mpl d = - try pp_decl mpl d with Failure "empty phrase" -> mt () - -end - + let pp mp s = + push_visible mp; + let p = pp_specif s ++ fnl2 () in + pop_visible (); p + in + prlist_strict + (fun (mp,sign) -> prlist_strict identity (map_succeed (pp mp) sign)) s + +let pp_decl d = + try pp_decl d with Failure "empty phrase" -> mt () + +let ocaml_descr = { + keywords = keywords; + file_suffix = ".ml"; + capital_file = false; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = Some ".mli"; + sig_preamble = sig_preamble; + pp_sig = pp_signature; + pp_decl = pp_decl; +} |