From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- contrib/extraction/ocaml.ml | 627 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 627 insertions(+) create mode 100644 contrib/extraction/ocaml.ml (limited to 'contrib/extraction/ocaml.ml') diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml new file mode 100644 index 00000000..707ef94f --- /dev/null +++ b/contrib/extraction/ocaml.ml @@ -0,0 +1,627 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '\'' + 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_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 () + +(*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 = + 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 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()) + +(*s The pretty-printing functor. *) + +module Make = functor(P : Mlpp_param) -> struct + +let local_mpl = ref ([] : module_path list) + +let pp_global r = + if is_inline_custom r then str (find_custom r) + else P.pp_global !local_mpl r + +let empty_env () = [], P.globals () + +(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses + are needed or not. *) + +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,[]) -> pp_global r + | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r + | Tarr (t1,t2) -> + pp_par par + (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) + | Tdummy -> str "__" + | Tunknown -> str "__" + | Tcustom s -> str s + 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 expr_needs_par = function + | MLlam _ -> true + | MLcase (_,[|_|]) -> false + | MLcase _ -> true + | _ -> false + + +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,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] 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 r) par (List.tl args) + with _ -> apply (pp_global r)) + | MLcons (r,[]) -> + assert (args=[]); + if Refset.mem r !cons_cofix then + pp_par par (str "lazy " ++ pp_global r) + else pp_global r + | MLcons (r,args') -> + (try + let projs = find_projections (kn_of_r r) in + pp_record_pat (projs, List.map (pp_expr true env []) args') + with Not_found -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + if Refset.mem r !cons_cofix then + pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") + else pp_par par (pp_global r ++ spc () ++ tuple)) + | MLcase (t, pv) -> + let r,_,_ = pv.(0) in + let expr = if Refset.mem r !cons_cofix then + (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) + else + (pp_expr false env [] t) + in + (try + let projs = find_projections (kn_of_r r) 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 (List.nth projs (n-i)))) + | MLapp (MLrel i, a) when i <= n -> + if List.exists (ast_occurs_itvl 1 n) a + then raise Not_found + else + 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))) + par ((List.map (pp_expr true env' []) a) @ args)) + | _ -> raise Not_found + with Not_found -> + if Array.length pv = 1 then + let s1,s2 = pp_one_pat env 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' + (v 0 (str "match " ++ expr ++ str " with" ++ + fnl () ++ str " | " ++ pp_pat env 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 r ++ str " =" ++ spc () ++ a) + (List.combine projs args) ++ + str " }" + +and pp_one_pat env (r,ids,t) = + let ids,env' = push_vars (List.rev ids) env in + let expr = pp_expr (expr_needs_par t) env' [] t in + try + let projs = find_projections (kn_of_r r) in + pp_record_pat (projs, List.rev_map pr_id ids), expr + with Not_found -> + let args = + if ids = [] then (mt ()) + else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in + pp_global r ++ args, expr + +and pp_pat env pv = + prvect_with_sep (fun () -> (fnl () ++ str " | ")) + (fun x -> let s1,s2 = pp_one_pat env x in + hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv + +and pp_function env f t = + let bl,t' = collect_lams t in + let bl,env' = push_vars bl env in + let is_function pv = + let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in + not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl) + in + let is_not_cofix pv = + let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) + in + match t' with + | MLcase(MLrel 1,pv) when is_not_cofix pv -> + if is_function pv then + (f ++ pr_binding (List.rev (List.tl bl)) ++ + str " = function" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' pv)) + else + (f ++ pr_binding (List.rev bl) ++ + str " = match " ++ + pr_id (List.hd bl) ++ str " with" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' pv)) + + | _ -> (f ++ 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) -> pp_function env (pr_id fi) 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 () + +(*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 + 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 + +(*s Pretty-printing of inductive types declaration. *) + +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<>[])) + +let pp_one_ind prefix ip pl cv = + 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)) + in + pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ + if cv = [||] 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 : " ++ + prvect_with_sep spc pr_id packet.ip_consnames) + +let pp_singleton kn packet = + let l = rename_tvars keywords packet.ip_vars in + hov 2 (str "type " ++ pp_parameters l ++ + pp_global (IndRef (kn,0)) ++ 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 packet = + let l = List.combine (find_projections kn) packet.ip_types.(0) in + let projs = find_projections kn in + let pl = rename_tvars keywords packet.ip_vars in + str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++ + hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) + (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) + ++ str " }" + +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" + +let pp_ind co kn ind = + 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 p = ind.ind_packets.(i) in + if is_custom (IndRef (kn,i)) 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 ip p.ip_vars ++ fnl () ++ str "and " else mt ()) + ++ pp_one_ind (if co then "__" else "") ip p.ip_vars 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 -> + let nop _ = () + and add r = cons_cofix := Refset.add r !cons_cofix in + decl_iter_references nop add nop (Dind (kn,i)); + pp_ind true kn i + | Record -> pp_record kn i.ind_packets.(0) + | _ -> pp_ind false kn i + +let pp_decl mpl = + local_mpl := mpl; + function + | Dind (kn,i) as d -> pp_mind kn i + | Dtype (r, l, t) -> + if is_inline_custom r then failwith "empty phrase" + else + 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" ++ spc () ++ ids ++ pp_global r ++ + 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) + | 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 + | (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) + | (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 + | MTident kn -> + let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l)) + | 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' + | 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 + str "sig " ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + fnl () ++ str "end" + +let is_short = function MEident _ | MEapply _ -> true | _ -> false + +let rec pp_structure_elem mpl = function + | (_,SEdecl d) -> pp_decl mpl d + | (l,SEmodule m) -> + hov 1 + (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ + (* if you want signatures everywhere: *) + (*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) + | (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' + | 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 + | MEapply (me, me') -> + pp_module_expr mpl None me ++ str "(" ++ + pp_module_expr mpl 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 + 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_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 + + + -- cgit v1.2.3