diff options
Diffstat (limited to 'plugins/extraction/ocaml.ml')
-rw-r--r-- | plugins/extraction/ocaml.ml | 110 |
1 files changed, 56 insertions, 54 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 70e71eeb..30ac3d3f 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,25 +9,21 @@ (*s Production of Ocaml syntax. *) open Pp +open Errors open Util open Names open Nameops -open Libnames +open Globnames 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_tvar id = str ("'" ^ Id.to_string id) let pp_abst = function | [] -> mt () @@ -36,10 +32,10 @@ let pp_abst = function str " ->" ++ spc () let pp_parameters l = - (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) + (pp_boxed_tuple pp_tvar l ++ space_if (not (List.is_empty l))) let pp_string_parameters l = - (pp_boxed_tuple str l ++ space_if (l<>[])) + (pp_boxed_tuple str l ++ space_if (not (List.is_empty l))) let pp_letin pat def body = let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in @@ -48,7 +44,7 @@ let pp_letin pat def body = (*s Ocaml renaming issues. *) let keywords = - List.fold_right (fun s -> Idset.add (id_of_string s)) + List.fold_right (fun s -> Id.Set.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"; @@ -57,22 +53,30 @@ let keywords = "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 + Id.Set.empty let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") -let preamble _ used_modules usf = +let pp_comment s = str "(* " ++ hov 0 s ++ str " *)" + +let pp_header_comment = function + | None -> mt () + | Some com -> pp_comment com ++ fnl () ++ fnl () + +let preamble _ comment used_modules usf = + pp_header_comment comment ++ prlist pp_open used_modules ++ - (if used_modules = [] then mt () else fnl ()) ++ + (if List.is_empty 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 = +let sig_preamble _ comment used_modules usf = + pp_header_comment comment ++ fnl () ++ fnl () ++ prlist pp_open used_modules ++ - (if used_modules = [] then mt () else fnl ()) ++ + (if List.is_empty 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*) @@ -93,7 +97,7 @@ 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] = ')') + l >= 2 && s.[0] == '(' && s.[l-1] == ')') let get_infix r = let s = find_custom r in @@ -110,22 +114,21 @@ let pp_one_field r i = function let pp_field r fields i = pp_one_field r i (List.nth fields i) -let pp_fields r fields = list_map_i (pp_one_field r) 0 fields +let pp_fields r fields = List.map_i (pp_one_field r) 0 fields (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) -let rec pp_type par vl t = +let 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 e when Errors.noncritical e -> - (str "'a" ++ int i)) + with Failure _ -> (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 not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" -> + when not (keep_singleton ()) && MutInd.equal 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 @@ -149,7 +152,7 @@ let is_bool_patt p s = | Pcons (r,[]) -> r | _ -> raise Not_found in - find_custom r = s + String.equal (find_custom r) s with Not_found -> false @@ -186,7 +189,7 @@ let rec pp_expr par env args = hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2)) | MLglob r -> (try - let args = list_skipn (projection_arity r) args in + 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 e when Errors.noncritical e -> apply (pp_global Term r)) @@ -203,35 +206,35 @@ let rec pp_expr par env args = | MLaxiom -> pp_par par (str "failwith \"AXIOM TO BE REALIZED\"") | MLcons (_,r,a) as c -> - assert (args=[]); + assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c | [a1;a2] when is_infix r -> let pp = pp_expr true env [] in pp_par par (pp a1 ++ str (get_infix r) ++ pp a2) | _ when is_coinductive r -> - let ne = (a<>[]) in + let ne = not (List.is_empty a) in let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple)) | [] -> pp_global Cons r | _ -> let fds = get_record_fields r in - if fds <> [] then + if not (List.is_empty fds) then pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a) else let tuple = pp_tuple (pp_expr true env []) a in - if str_global Cons r = "" (* hack Extract Inductive prod *) + if String.is_empty (str_global Cons r) (* hack Extract Inductive prod *) then tuple else pp_par par (pp_global Cons r ++ spc () ++ tuple) end | MLtuple l -> - assert (args = []); + assert (List.is_empty args); pp_boxed_tuple (pp_expr true env []) l | MLcase (_, t, pv) when is_custom_match pv -> if not (is_regular_match pv) then error "Cannot mix yet user-given match and general patterns."; let mkfun (ids,_,e) = - if ids <> [] then named_lams (List.rev ids) e + if not (List.is_empty ids) then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 in let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in @@ -250,7 +253,7 @@ let rec pp_expr par env args = (try pp_record_proj par env typ t pv args with Impossible -> (* Second, can this match be printed as a let-in ? *) - if Array.length pv = 1 then + if Int.equal (Array.length pv) 1 then let s1,s2 = pp_one_pat env pv.(0) in hv 0 (apply2 (pp_letin s1 head s2)) else @@ -265,8 +268,8 @@ let rec pp_expr par env args = and pp_record_proj par env typ t pv args = (* Can a match be printed as a mere record projection ? *) let fields = record_fields_of_type typ in - if fields = [] then raise Impossible; - if Array.length pv <> 1 then raise Impossible; + if List.is_empty fields then raise Impossible; + if not (Int.equal (Array.length pv) 1) then raise Impossible; if has_deep_pattern pv then raise Impossible; let (ids,pat,body) = pv.(0) in let n = List.length ids in @@ -277,7 +280,7 @@ and pp_record_proj par env typ t pv args = | _ -> raise Impossible in let rec lookup_rel i idx = function - | Prel j :: l -> if i = j then idx else lookup_rel i (idx+1) l + | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l | Pwild :: l -> lookup_rel i (idx+1) l | _ -> raise Impossible in @@ -301,15 +304,15 @@ and pp_record_pat (fields, args) = str " }" and pp_cons_pat r ppl = - if is_infix r && List.length ppl = 2 then + if is_infix r && Int.equal (List.length ppl) 2 then List.hd ppl ++ str (get_infix r) ++ List.hd (List.tl ppl) else let fields = get_record_fields r in - if fields <> [] then pp_record_pat (pp_fields r fields, ppl) - else if str_global Cons r = "" then + if not (List.is_empty fields) then pp_record_pat (pp_fields r fields, ppl) + else if String.is_empty (str_global Cons r) then pp_boxed_tuple identity ppl (* Hack Extract Inductive prod *) else - pp_global Cons r ++ space_if (ppl<>[]) ++ pp_boxed_tuple identity ppl + pp_global Cons r ++ space_if (not (List.is_empty ppl)) ++ pp_boxed_tuple identity ppl and pp_gen_pat ids env = function | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l) @@ -339,7 +342,7 @@ and pp_pat env pv = (fun i x -> let s1,s2 = pp_one_pat env x in hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++ - if i = Array.length pv - 1 then mt () else fnl ()) + if Int.equal i (Array.length pv - 1) then mt () else fnl ()) pv and pp_function env t = @@ -347,7 +350,7 @@ and pp_function env t = let bl,env' = push_vars (List.map id_of_mlid bl) env in match t' with | MLcase(Tglob(r,_),MLrel 1,pv) when - not (is_coinductive r) && get_record_fields r = [] && + not (is_coinductive r) && List.is_empty (get_record_fields r) && not (is_custom_match pv) -> if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then pr_binding (List.rev (List.tl bl)) ++ @@ -371,7 +374,7 @@ and pp_fix par env i (ids,bl) args = 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) ++ + (Array.map2 (fun id b -> (id,b)) ids bl) ++ fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) @@ -390,7 +393,7 @@ let pp_Dfix (rv,c,t) = (if init then failwith "empty phrase" else mt ()) else let void = is_inline_custom rv.(i) || - (not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED") + (not (is_custom rv.(i)) && match c.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then pp init (i+1) else @@ -413,20 +416,19 @@ let pp_equiv param_list name = function | 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 ()) ++ + (if Int.equal i 0 then mt () else fnl ()) ++ hov 3 (str "| " ++ cnames.(i) ++ - (if typs = [] then mt () else str " of ") ++ + (if List.is_empty 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 *)" + if Int.equal (Array.length ctyps) 0 then str " unit (* empty inductive *)" else fnl () ++ v 0 (prvecti pp_constructor ctyps) let pp_logical_ind packet = @@ -525,7 +527,7 @@ let pp_decl = function pp_string_parameters ids, str "=" ++ spc () ++ str s with Not_found -> pp_parameters l, - if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" + 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) @@ -632,7 +634,7 @@ and pp_module_type params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (mp, sign) -> push_visible mp params; - let l = map_succeed pp_specif sign in + let l = List.map pp_specif sign in pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ @@ -640,11 +642,11 @@ and pp_module_type params = function | 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 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' + 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 + let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); @@ -652,7 +654,7 @@ and pp_module_type params = function | 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 + 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 @@ -672,7 +674,7 @@ let rec pp_structure_elem = function | (l,SEmodule m) -> let typ = (* virtual printing of the type, in order to have a correct mli later*) - if Common.get_phase () = Pre then + if Common.get_phase () == Pre then str ": " ++ pp_module_type [] m.ml_mod_type else mt () in @@ -705,7 +707,7 @@ and pp_module_expr params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEstruct (mp, sel) -> push_visible mp params; - let l = map_succeed pp_structure_elem sel in + let l = List.map pp_structure_elem sel in pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ |