summaryrefslogtreecommitdiff
path: root/plugins/extraction/ocaml.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/ocaml.ml')
-rw-r--r--plugins/extraction/ocaml.ml110
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) ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 23:55:06 +0000