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 (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
106 (Some "helm","xref",s)
109 let map_attributes = List.map map_attribute
111 let resolve_binder = function
112 `Lambda -> Box.Text([],"\\lambda")
113 | `Pi -> Box.Text([],"\\Pi")
114 | `Exists -> Box.Text([],"\\exists")
115 | `Forall -> Box.Text([],"\\forall")
117 let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t =
119 bigast2box ~priority ~assoc ~attr t
120 else Box.Object (map_attributes attr, t)
121 and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
123 A.AttributedTerm (attr1, t) ->
124 (* attr should be empty, since AtrtributedTerm are not
125 supposed to be directly nested *)
126 bigast2box ~priority ~assoc ~attr:(attr1::~attr) t
129 (map_attributes attr,
131 Box.V([],List.map ast2box l);
133 | A.Binder (`Forall, (Cic.Anonymous, typ), body)
134 | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
135 Box.V(map_attributes attr,
136 [Box.H([],[(match typ with
137 | None -> Box.Text([], "?")
138 | Some typ -> ast2box typ);
140 Box.Text([], "\\to")]);
141 Box.indent(ast2box body)])
142 | A.Binder(kind, var, body) ->
143 Box.V(map_attributes attr,
144 [Box.H([],[resolve_binder kind;
148 Box.indent (ast2box body)])
149 | A.Case(arg, _, ty, pl) ->
150 let make_rule sep ((constr,vars),rhs) =
152 Box.V([],[Box.H([],[Box.Text([],sep);
154 make_pattern constr vars;
156 Box.Text([],"\Rightarrow")]);
157 Box.indent (bigast2box rhs)])
159 Box.H([],[Box.Text([],sep);
161 make_pattern constr vars;
163 Box.Text([],"\Rightarrow");
165 Box.Object([],rhs)]) in
166 let plbox = match pl with
167 [] -> Box.Text([],"[]")
171 (make_rule "[" r)::(List.map (make_rule "|") tl));
172 Box.Text([],"]")]) in
176 [ Box.H([],[Box.Text([],"[");
182 Box.V(map_attributes attr,
184 [Box.Text([],"match");
188 Box.Text([],"with")]);
191 Box.V(map_attributes attr,
193 [Box.H(map_attributes attr,
194 [Box.Text([],"match");
198 Box.Text([],"with")]);
200 | A.LetIn (var, s, t) ->
201 Box.V(map_attributes attr,
202 (make_def "let" var s "in")@[ast2box t])
203 | A.LetRec (_, vars, body) ->
205 let rec make_defs let_txt = function
208 make_def let_txt var s "in"
210 (make_def let_txt var s "")@(make_defs "and" tl) in
211 make_defs "let rec" vars in
212 Box.V(map_attributes attr,
213 definitions@[ast2box body])
214 | A.Ident (s, subst) ->
216 let rec make_substs start_txt =
220 make_subst start_txt s t "]"
222 (make_subst start_txt s t ";")@(make_substs " " tl)
225 | Some subst -> make_substs "\\subst [" subst
228 Box.V([], (* attr here or on Vbox? *)
229 [Box.Text(map_attributes attr,s);
230 Box.indent(Box.V([],subst))])
232 Box.Text([],"_") (* big? *)
237 Box.H([],[aux_option t; Box.Text([],";")]))
239 Box.V(map_attributes attr,
240 [Box.Text([],"?"^(string_of_int n));
241 Box.H([],[Box.Text([],"[");
242 Box.V([],local_context);
248 `Prop -> Box.Text([],"Prop")
249 | `Set -> Box.Text([],"Set")
250 | `Type -> Box.Text([],"Type")
251 | `CProp -> Box.Text([],"CProp"))
255 and aux_option = function
256 None -> Box.Text([],"_")
257 | Some ast -> ast2box ast
259 and make_var = function
260 (Cic.Anonymous, None) -> Box.Text([],"_:_")
261 | (Cic.Anonymous, Some t) ->
262 Box.H([],[Box.Text([],"_:");ast2box t])
263 | (Cic.Name s, None) -> Box.Text([],s)
264 | (Cic.Name s, Some t) ->
266 Box.V([],[Box.Text([],s^":");
267 Box.indent(bigast2box t)])
269 Box.H([],[Box.Text([],s^":");Box.Object([],t)])
271 and make_pattern constr =
273 [] -> Box.Text([],constr)
280 (* ignoring the type *)
281 (Cic.Anonymous, _) -> Box.Text([],"_")
282 | (Cic.Name s, _) -> Box.Text([],s) in
283 Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
284 Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
287 and make_def let_txt var def end_txt =
290 (* ignoring the type *)
291 (Cic.Anonymous, _) -> Box.Text([],"_")
292 | (Cic.Name s, _) -> Box.Text([],s)) in
294 [Box.Text([],let_txt);
301 [Box.smallskip;Box.Text([],end_txt)]
303 and make_subst start_txt varname body end_txt =
305 [Box.Text([],start_txt);
306 Box.Text([],varname);
308 Box.Text([],"\Assign")
311 [Box.Text([],end_txt)]
313 and pretty_append l ast tail =
314 prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
317 Box.H([],Box.skip::(bigast2box ast)::tail)]
319 [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]