1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (**************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (**************************************************************************)
37 let symbol_table = Hashtbl.create 503;;
38 let symbol_table_charcount = Hashtbl.create 503;;
42 let rec countvar current_size = function
43 (Cic.Anonymous, None) -> current_size + 1 (* underscore *)
44 | (Cic.Anonymous, Some ty) -> countterm current_size ty
45 | (Cic.Name s, None) -> current_size + String.length s
46 | (Cic.Name s, Some ty) -> current_size + countterm current_size ty
48 and countterm current_size t =
49 if current_size > maxsize then current_size
51 A.AttributedTerm (_,t) -> countterm current_size t
53 List.fold_left countterm current_size l
54 | A.Binder (_,var,body) ->
55 let varsize = countvar current_size var in
56 countterm (varsize + 1) body (* binder *)
57 | A.Case (arg, _, ty, pl) ->
58 let size1 = countterm (current_size+10) arg in (* match with *)
62 | Some ty -> countterm size1 ty in
64 (fun c ((constr,vars),action) ->
66 List.fold_left countvar (c+String.length constr) vars in
67 countterm size3 action) size2 pl
68 | A.LetIn (var,s,t) ->
69 let size1 = countvar current_size var in
70 let size2 = countterm size1 s in
76 let size1 = countvar c var in
77 countterm size1 s) current_size l in
79 | A.Ident(s,None) -> current_size + (String.length s)
80 | A.Ident(s,Some l) ->
82 (fun c (v,t) -> countterm (c + (String.length v)) t)
83 (current_size + (String.length s)) l
84 | A.Implicit -> current_size + 1 (* underscore *)
89 None -> c + 1 (* underscore *)
90 | Some t -> countterm c t)
91 (current_size + 1) l (* num *)
92 | A.Num (s, _) -> current_size + String.length s
93 | A.Sort _ -> current_size + 4 (* sort name *)
94 | A.Symbol (s,_) -> current_size + String.length s
98 ((countterm 0 t) > maxsize)
104 let (n, m) = CicAst.loc_of_floc floc in
105 (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
107 (Some "helm","xref",s)
110 let map_attributes = List.map map_attribute
112 let resolve_binder = function
113 `Lambda -> Box.Text([],"\\lambda")
114 | `Pi -> Box.Text([],"\\Pi")
115 | `Exists -> Box.Text([],"\\exists")
116 | `Forall -> Box.Text([],"\\forall")
118 let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t =
120 bigast2box ~priority ~assoc ~attr t
121 else Box.Object (map_attributes attr, t)
122 and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
124 A.AttributedTerm (attr1, t) ->
125 (* attr should be empty, since AtrtributedTerm are not
126 supposed to be directly nested *)
127 bigast2box ~priority ~assoc ~attr:(attr1::~attr) t
130 (map_attributes attr,
132 Box.V([],List.map ast2box l);
134 | A.Binder (`Forall, (Cic.Anonymous, typ), body)
135 | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
136 Box.V(map_attributes attr,
137 [Box.H([],[(match typ with
138 | None -> Box.Text([], "?")
139 | Some typ -> ast2box typ);
141 Box.Text([], "\\to")]);
142 Box.indent(ast2box body)])
143 | A.Binder(kind, var, body) ->
144 Box.V(map_attributes attr,
145 [Box.H([],[resolve_binder kind;
149 Box.indent (ast2box body)])
150 | A.Case(arg, _, ty, pl) ->
151 let make_rule sep ((constr,vars),rhs) =
153 Box.V([],[Box.H([],[Box.Text([],sep);
155 make_pattern constr vars;
157 Box.Text([],"\\Rightarrow")]);
158 Box.indent (bigast2box rhs)])
160 Box.H([],[Box.Text([],sep);
162 make_pattern constr vars;
164 Box.Text([],"\\Rightarrow");
166 Box.Object([],rhs)]) in
167 let plbox = match pl with
168 [] -> Box.Text([],"[]")
172 (make_rule "[" r)::(List.map (make_rule "|") tl));
173 Box.Text([],"]")]) in
177 [ Box.H([],[Box.Text([],"[");
183 Box.V(map_attributes attr,
185 [Box.Text([],"match");
189 Box.Text([],"with")]);
192 Box.V(map_attributes attr,
194 [Box.H(map_attributes attr,
195 [Box.Text([],"match");
199 Box.Text([],"with")]);
201 | A.LetIn (var, s, t) ->
202 Box.V(map_attributes attr,
203 (make_def "let" var s "in")@[ast2box t])
204 | A.LetRec (_, vars, body) ->
206 let rec make_defs let_txt = function
209 make_def let_txt var s "in"
211 (make_def let_txt var s "")@(make_defs "and" tl) in
212 make_defs "let rec" vars in
213 Box.V(map_attributes attr,
214 definitions@[ast2box body])
215 | A.Ident (s, subst) ->
217 let rec make_substs start_txt =
221 make_subst start_txt s t "]"
223 (make_subst start_txt s t ";")@(make_substs " " tl)
226 | Some subst -> make_substs "\\subst [" subst
229 Box.V([], (* attr here or on Vbox? *)
230 [Box.Text(map_attributes attr,s);
231 Box.indent(Box.V([],subst))])
233 Box.Text([],"_") (* big? *)
238 Box.H([],[aux_option t; Box.Text([],";")]))
240 Box.V(map_attributes attr,
241 [Box.Text([],"?"^(string_of_int n));
242 Box.H([],[Box.Text([],"[");
243 Box.V([],local_context);
249 `Prop -> Box.Text([],"Prop")
250 | `Set -> Box.Text([],"Set")
251 | `Type -> Box.Text([],"Type")
252 | `CProp -> Box.Text([],"CProp"))
256 and aux_option = function
257 None -> Box.Text([],"_")
258 | Some ast -> ast2box ast
260 and make_var = function
261 (Cic.Anonymous, None) -> Box.Text([],"_:_")
262 | (Cic.Anonymous, Some t) ->
263 Box.H([],[Box.Text([],"_:");ast2box t])
264 | (Cic.Name s, None) -> Box.Text([],s)
265 | (Cic.Name s, Some t) ->
267 Box.V([],[Box.Text([],s^":");
268 Box.indent(bigast2box t)])
270 Box.H([],[Box.Text([],s^":");Box.Object([],t)])
272 and make_pattern constr =
274 [] -> Box.Text([],constr)
281 (* ignoring the type *)
282 (Cic.Anonymous, _) -> Box.Text([],"_")
283 | (Cic.Name s, _) -> Box.Text([],s) in
284 Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
285 Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
288 and make_def let_txt var def end_txt =
291 (* ignoring the type *)
292 (Cic.Anonymous, _) -> Box.Text([],"_")
293 | (Cic.Name s, _) -> Box.Text([],s)) in
295 [Box.Text([],let_txt);
302 [Box.smallskip;Box.Text([],end_txt)]
304 and make_subst start_txt varname body end_txt =
306 [Box.Text([],start_txt);
307 Box.Text([],varname);
309 Box.Text([],"\\Assign")
312 [Box.Text([],end_txt)]
314 and pretty_append l ast tail =
315 prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
318 Box.H([],Box.skip::(bigast2box ast)::tail)]
320 [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]