1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
9 (*i $Id: common.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
12 open OcamlExtractionTable
16 (*s Some pretty-print utility functions. *)
18 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
20 let pp_apply st par args = match args with
22 | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
24 let pr_binding = function
26 | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
28 (** By default, in module Format, you can do horizontal placing of blocks
29 even if they include newlines, as long as the number of chars in the
30 blocks are less that a line length. To avoid this awkward situation,
31 we attach a big virtual size to [fnl] newlines. *)
33 let fnl () = stras (1000000,"") ++ fnl ()
35 let space_if = function true -> str " " | false -> mt ()
38 match s.[0] with 'a' .. 'z' | 'A' .. 'Z' -> false | _ -> true
40 let rec lowercase_id id =
41 if id = "" then "x" else
42 if id.[0] = '_' then lowercase_id (String.sub id 1 (String.length id - 1)) else
43 if is_invalid_id id then lowercase_id ("x" ^ id) else
44 String.uncapitalize id
46 let rec uppercase_id id =
47 if id = "" then "T" else
48 if id.[0] = '_' then uppercase_id (String.sub id 1 (String.length id - 1)) else
49 if is_invalid_id id then uppercase_id ("x" ^ id) else
52 type kind = Term | Type | Cons
54 let upperkind = function
59 let kindcase_id k id =
60 if upperkind k then uppercase_id id else lowercase_id id
62 (*s de Bruijn environments for programs *)
64 type env = identifier list * Idset.t
66 (*s Generic renaming issues for local variable names. *)
68 let rec rename_id id avoid =
69 if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
71 let rec rename_vars avoid = function
74 | id :: idl when id == dummy_name ->
75 (* we don't rename dummy binders *)
76 let (idl', avoid') = rename_vars avoid idl in
79 let (idl, avoid) = rename_vars avoid idl in
80 let id = rename_id (lowercase_id id) avoid in
81 (id :: idl, Idset.add id avoid)
83 let rename_tvars avoid l =
84 let rec rename avoid = function
87 let id = rename_id (lowercase_id id) avoid in
88 let idl, avoid = rename (Idset.add id avoid) idl in
92 let push_vars ids (db,avoid) =
93 let ids',avoid' = rename_vars avoid ids in
94 ids', (ids' @ db, avoid')
96 let get_db_name n (db,_) =
97 let id = List.nth db (pred n) in
98 if id = dummy_name then "__" else id
100 let empty_env status = [], get_global_ids status
102 let fake_spec = NReference.Fix (0,-1,-1)
104 let safe_name_of_reference status r =
106 NReference.Ref (uri, spec) when spec = fake_spec ->
107 (* The field of a record *)
109 | _ -> NCicPp.r2s status true r
111 let maybe_capitalize b n = if b then String.capitalize n else n
113 let modname_of_filename status capitalize name =
115 let name = modname_of_filename status name in
116 status, maybe_capitalize capitalize name
118 let globs = Idset.elements (get_modnames status) in
119 let s = next_ident_away (String.uncapitalize name) globs in
120 let status = add_modname status s in
121 let status = add_modname_for_filename status name s in
122 status, maybe_capitalize capitalize s
124 let ref_renaming status (k,r) =
126 let rec ref_renaming status (k,r) =
127 try status,name_of_reference status r
129 if is_projection status r then
130 (* The reference for the projection and the field of a record are different
131 and they would be assigned different names (name clash!). So we normalize
132 the projection reference into the field reference *)
133 let NReference.Ref (uri,_) = r in
134 let fieldref = NReference.reference_of_spec uri fake_spec in
135 ref_renaming status (k,fieldref)
137 let name = safe_name_of_reference status r in
138 let globs = Idset.elements (get_global_ids status) in
139 let s = next_ident_away (kindcase_id k name) globs in
140 let status = add_global_ids status s in
141 let status = add_name_for_reference status r s in
144 ref_renaming status (k,r)
146 let baseuri = Filename.dirname (NReference.string_of_reference r) in
147 if current_baseuri status = baseuri then
150 let modname = Filename.basename (Filename.dirname (NReference.string_of_reference r)) in
151 let status,modname = modname_of_filename status true modname in
152 status, modname ^ "." ^ s
154 (* Main name printing function for a reference *)
156 let pp_global status k r = ref_renaming status (k,r)