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.ml169
1 files changed, 87 insertions, 82 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc..96d87604 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(*s Production of Ocaml syntax. *)
@@ -12,7 +14,7 @@ open Pp
open CErrors
open Util
open Names
-open Nameops
+open ModPath
open Globnames
open Table
open Miniml
@@ -28,7 +30,7 @@ let pp_tvar id = str ("'" ^ Id.to_string id)
let pp_abst = function
| [] -> mt ()
| l ->
- str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
+ str "fun " ++ prlist_with_sep (fun () -> str " ") Id.print l ++
str " ->" ++ spc ()
let pp_parameters l =
@@ -66,7 +68,7 @@ let pp_header_comment = function
| None -> mt ()
| Some com -> pp_comment com ++ fnl2 ()
-let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
let pp_tdummy usf =
if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
@@ -100,11 +102,41 @@ let pp_global k r = str (str_global k r)
let pp_modname mp = str (Common.pp_module mp)
+(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
+
+let infix_symbols =
+ ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
+let operator_chars =
+ [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
+
+(* infix ops in OCaml, but disallowed by preceding grammar *)
+
+let builtin_infixes =
+ [ "::" ; "," ]
+
+let substring_all_opchars s start stop =
+ let rec check_char i =
+ if i >= stop then true
+ else
+ List.mem s.[i] operator_chars && check_char (i+1)
+ in
+ check_char start
+
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 len = String.length s in
+ len >= 3 &&
+ (* parenthesized *)
+ (s.[0] == '(' && s.[len-1] == ')' &&
+ let inparens = String.trim (String.sub s 1 (len - 2)) in
+ let inparens_len = String.length inparens in
+ (* either, begins with infix symbol, any remainder is all operator chars *)
+ (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) ||
+ (* or, starts with #, at least one more char, all are operator chars *)
+ (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) ||
+ (* or, is an OCaml built-in infix *)
+ (List.mem inparens builtin_infixes)))
let get_infix r =
let s = find_custom r in
@@ -182,7 +214,7 @@ let rec pp_expr par env args =
(* Try to survive to the occurrence of a Dummy rel.
TODO: we should get rid of this hack (cf. #592) *)
let id = if Id.equal id dummy_name then Id.of_string "__" else id in
- apply (pr_id id)
+ apply (Id.print id)
| MLapp (f,args') ->
let stl = List.map (pp_expr true env []) args' in
pp_expr par env (stl @ args) f
@@ -194,7 +226,7 @@ let rec pp_expr par env args =
apply2 st
| MLletin (id,a1,a2) ->
let i,env' = push_vars [id_of_mlid id] env in
- let pp_id = pr_id (List.hd i)
+ let pp_id = Id.print (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 (apply2 (pp_letin pp_id pp_a1 pp_a2))
@@ -246,7 +278,7 @@ let rec pp_expr par env 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.";
+ user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
let mkfun (ids,_,e) =
if not (List.is_empty ids) then named_lams (List.rev ids) e
else dummy_lams (ast_lift 1 e) 1
@@ -330,10 +362,10 @@ and pp_cons_pat r ppl =
and pp_gen_pat ids env = function
| Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
- | Pusual r -> pp_cons_pat r (List.map pr_id ids)
+ | Pusual r -> pp_cons_pat r (List.map Id.print ids)
| Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l
| Pwild -> str "_"
- | Prel n -> pr_id (get_db_name n env)
+ | Prel n -> Id.print (get_db_name n env)
and pp_ifthenelse env expr pv = match pv with
| [|([],tru,the);([],fal,els)|] when
@@ -372,7 +404,7 @@ and pp_function env t =
v 0 (pp_pat env' pv)
else
pr_binding (List.rev bl) ++
- str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+ str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++
v 0 (pp_pat env' pv)
| _ ->
pr_binding (List.rev bl) ++
@@ -387,10 +419,10 @@ and pp_fix par env i (ids,bl) args =
(v 0 (str "let rec " ++
prvect_with_sep
(fun () -> fnl () ++ str "and ")
- (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
+ (fun (fi,ti) -> Id.print 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)))
+ hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
(* Ad-hoc double-newline in v boxes, with enough negative whitespace
to avoid indenting the intermediate blank line *)
@@ -431,7 +463,7 @@ let pp_Dfix (rv,c,t) =
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))
+ str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i))
| RenEquiv ren, _ ->
str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
@@ -451,10 +483,10 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps =
else fnl () ++ v 0 (prvecti pp_constructor ctyps)
let pp_logical_ind packet =
- pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+ pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
fnl () ++
pp_comment (str "with constructors : " ++
- prvect_with_sep spc pr_id packet.ip_consnames) ++
+ prvect_with_sep spc Id.print packet.ip_consnames) ++
fnl ()
let pp_singleton kn packet =
@@ -463,7 +495,7 @@ let pp_singleton kn packet =
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)))
+ Id.print packet.ip_consnames.(0)))
let pp_record kn fields ip_equiv packet =
let ind = IndRef (kn,0) in
@@ -555,24 +587,6 @@ let pp_decl = function
| 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 -> mt ()
| Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,42 +611,32 @@ let pp_spec = function
in
hov 2 (str "type " ++ ids ++ name ++ 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
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> pp_spec s
+ | Some ren ->
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)
+ str ("include module type of struct include "^ren^" end"))
| (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 ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> Pp.mt ()
+ | Some ren ->
+ fnl () ++
+ hov 1 (str ("module "^ren^" :") ++ spc () ++
+ str "module type of struct include " ++ name ++ str " end"))
| (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 ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> Pp.mt ()
+ | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_type params = function
| MTident kn ->
@@ -646,15 +650,17 @@ and pp_module_type params = function
push_visible mp params;
let try_pp_specif l x =
let px = pp_specif x in
- if Pp.is_empty px then l else px::l
+ if Pp.ismt px then l else px::l
in
(* We cannot use fold_right here due to side effects in pp_specif *)
let l = List.fold_left try_pp_specif [] sign in
let l = List.rev l in
pop_visible ();
str "sig" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
- fnl () ++ str "end"
+ (if List.is_empty l then mt ()
+ else
+ v 1 (str " " ++ prlist_with_sep cut2 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
@@ -681,12 +687,11 @@ 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
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> pp_decl d
+ | Some ren ->
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)
+ fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
| (l,SEmodule m) ->
let typ =
(* virtual printing of the type, in order to have a correct mli later*)
@@ -699,18 +704,16 @@ let rec pp_structure_elem = function
hov 1
(str "module " ++ name ++ typ ++ str " =" ++
(if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
- (try
- let ren = Common.check_duplicate (top_visible_mp ()) l in
- fnl () ++ str ("module "^ren^" = ") ++ name
- with Not_found -> mt ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+ | None -> 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 ())
+ (match Common.get_duplicate (top_visible_mp ()) l with
+ | None -> mt ()
+ | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_expr params = function
| MEident mp -> pp_modname mp
@@ -725,15 +728,17 @@ and pp_module_expr params = function
push_visible mp params;
let try_pp_structure_elem l x =
let px = pp_structure_elem x in
- if Pp.is_empty px then l else px::l
+ if Pp.ismt px then l else px::l
in
(* We cannot use fold_right here due to side effects in pp_structure_elem *)
let l = List.fold_left try_pp_structure_elem [] sel in
let l = List.rev l in
pop_visible ();
str "struct" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
- fnl () ++ str "end"
+ (if List.is_empty l then mt ()
+ else
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+ ++ str "end"
let rec prlist_sep_nonempty sep f = function
| [] -> mt ()
@@ -741,7 +746,7 @@ let rec prlist_sep_nonempty sep f = function
| h::t ->
let e = f h in
let r = prlist_sep_nonempty sep f t in
- if Pp.is_empty e then r
+ if Pp.ismt e then r
else e ++ sep () ++ r
let do_struct f s =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 20:27:10 +0000