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 (**************************************************************************)
36 module P = Mpresentation;;
38 let symbol_table = Hashtbl.create 503;;
39 let symbol_table_charcount = Hashtbl.create 503;;
43 let rec countvar current_size = function
44 (Cic.Anonymous, None) -> current_size + 1 (* underscore *)
45 | (Cic.Anonymous, Some ty) -> countterm current_size ty
46 | (Cic.Name s, None) -> current_size + String.length s
47 | (Cic.Name s, Some ty) -> current_size + countterm current_size ty
49 and countterm current_size t =
50 if current_size > maxsize then current_size
52 A.AttributedTerm (_,t) -> countterm current_size t
54 List.fold_left countterm current_size l
55 | A.Binder (_,var,body) ->
56 let varsize = countvar current_size var in
57 countterm (varsize + 1) body (* binder *)
58 | A.Case (arg, _, ty, pl) ->
59 let size1 = countterm (current_size+10) arg in (* match with *)
63 | Some ty -> countterm size1 ty in
65 (fun c ((constr,vars),action) ->
67 List.fold_left countvar (c+String.length constr) vars in
68 countterm size3 action) size2 pl
69 | A.LetIn (var,s,t) ->
70 let size1 = countvar current_size var in
71 let size2 = countterm size1 s in
77 let size1 = countvar c var in
78 countterm size1 s) current_size l in
80 | A.Ident(s,None) -> current_size + (String.length s)
81 | A.Ident(s,Some l) ->
83 (fun c (v,t) -> countterm (c + (String.length v)) t)
84 (current_size + (String.length s)) l
85 | A.Implicit -> current_size + 1 (* underscore *)
90 None -> c + 1 (* underscore *)
91 | Some t -> countterm c t)
92 (current_size + 1) l (* num *)
93 | A.Num (s, _) -> current_size + String.length s
94 | A.Sort _ -> current_size + 4 (* sort name *)
95 | A.Symbol (s,_) -> current_size + String.length s
97 | A.UserInput -> current_size
101 ((countterm 0 t) > maxsize)
104 let rec make_attributes l1 =
107 | None::tl -> make_attributes (List.tl l1) tl
109 let p,n = List.hd l1 in
110 (p,n,s)::(make_attributes (List.tl l1) tl)
113 let map_tex unicode texcmd =
114 let default_map_tex = Printf.sprintf "\\%s " in
117 Utf8Macro.expand texcmd
118 with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd
120 default_map_tex texcmd
122 let resolve_binder unicode = function
123 | `Lambda -> map_tex unicode "lambda"
124 | `Pi -> map_tex unicode "Pi"
125 | `Forall -> map_tex unicode "forall"
126 | `Exists -> map_tex unicode "exists"
129 let rec make_args f ~tail = function
131 | [arg] -> [f ~tail arg]
132 | arg :: tl -> (f ~tail:[] arg) :: (make_args f ~tail tl)
134 let append_tail ~tail box =
137 | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
139 let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
142 let lookup_uri = function
146 Some (Hashtbl.find ids_to_uris id)
147 with Not_found -> None)
149 let make_std_attributes xref =
150 let uri = lookup_uri xref in
151 make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
153 let rec ast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
155 bigast2box ~priority ~assoc ?xref ~tail t
157 let attrs = make_std_attributes xref in
158 append_tail ~tail (Box.Object (attrs, t))
160 bigast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
162 | A.AttributedTerm (`Loc _, t) -> bigast2box ?xref ~tail t
163 | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
164 | A.Appl [] -> assert false
165 | A.Appl ((hd::tl) as l) ->
166 let rec find_symbol idref = function
167 | A.AttributedTerm (`Loc _, t) -> find_symbol None t
168 | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
169 | A.Symbol (name, _) ->
171 | None -> assert false
172 | Some idref -> `Symbol (name, idref))
175 let aattr = make_attributes [Some "helm","xref"] [xref] in
176 (match find_symbol None hd with
177 | `Symbol (name, sxref) ->
178 let sattr = make_std_attributes (Some sxref) in
180 (let f = Hashtbl.find symbol_table_charcount name in
181 f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
184 (make_attributes [Some "helm","xref"] [xref],
187 make_args (fun ~tail t -> ast2box ~tail t)
188 ~tail:(")" :: tail) l);
192 (make_attributes [Some "helm","xref"] [xref],
196 (fun ~tail t -> ast2box ~tail t)
197 ~tail:(")" :: tail) l)]
199 | A.Binder (`Forall, (Cic.Anonymous, typ), body)
200 | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
201 Box.V(make_attributes [Some "helm","xref"] [xref],
203 | None -> Box.Text([], "?")
204 | Some typ -> ast2box ~tail:[] typ);
207 Box.Text([], map_tex unicode "to");
208 ast2box ~tail body])])
209 | A.Binder(kind, var, body) ->
210 Box.V(make_attributes [Some "helm","xref"] [xref],
212 [Box.Text ([None,"color","blue"], resolve_binder unicode kind);
213 make_var ~tail:("." :: tail) var]);
214 Box.indent (ast2box ~tail body)])
215 | A.Case(arg, _, ty, pl) ->
216 let make_rule ~tail sep ((constr,vars),rhs) =
218 Box.V([],[Box.H([],[Box.Text([],sep);
220 make_pattern constr vars;
222 Box.Text([],map_tex unicode "Rightarrow")]);
223 Box.indent (bigast2box ~tail rhs)])
225 Box.H([],[Box.Text([],sep);
227 make_pattern constr vars;
229 Box.Text([],map_tex unicode "Rightarrow");
231 Box.Object([],rhs)]) in
232 let plbox = match pl with
233 [] -> Box.Text([],"[]")
236 (make_rule ~tail:[] "[" r) ::
238 (fun ~tail pat -> make_rule ~tail:[] "|" pat)
245 [ Box.H([],[Box.Text([],"[");
251 Box.V(make_attributes [Some "helm","xref"] [xref],
253 [Box.Text([],"match");
254 Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg]));
258 Box.V(make_attributes [Some "helm","xref"] [xref],
260 [Box.H(make_attributes [Some "helm","xref"] [xref],
261 [Box.Text([],"match");
265 Box.Text([],"with")]);
267 | A.LetIn (var, s, t) ->
268 Box.V(make_attributes [Some "helm","xref"] [xref],
269 (make_def "let" var s "in")@[ast2box ~tail t])
270 | A.LetRec (_, vars, body) ->
272 let rec make_defs let_txt = function
275 make_def let_txt var s "in"
277 (make_def let_txt var s "")@(make_defs "and" tl) in
278 make_defs "let rec" vars in
279 Box.V(make_attributes [Some "helm","xref"] [xref],
280 definitions@[ast2box ~tail body])
281 | A.Ident (s, subst) ->
283 let rec make_substs start_txt =
287 make_subst start_txt s t ""
289 (make_subst start_txt s t ";")@(make_substs "" tl)
294 [Box.Text(make_std_attributes xref,s);
296 [Box.Text([],"[...]");
297 Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
298 Box.V([], make_substs "" subst);
299 Box.Text([], "]")])])])
300 | None -> Box.Text(make_std_attributes xref, s)
304 Box.H([], (* attr here or on Vbox? *)
305 [Box.Text(make_std_attributes xref,s);
306 Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
307 (* Box.indent(Box.V([],subst))]) *)
310 Box.Text([],"_") (* big? *)
315 Box.H([],[aux_option ~tail t; Box.Text([],";")]))
317 Box.V(make_attributes [Some "helm","xref"] [xref],
318 [Box.Text([],"?"^(string_of_int n));
319 Box.H([],[Box.Text([],"[");
320 Box.V([],local_context);
326 `Prop -> Box.Text([],"Prop")
327 | `Set -> Box.Text([],"Set")
328 | `Type -> Box.Text([],"Type")
329 | `CProp -> Box.Text([],"CProp"))
333 | A.UserInput -> Box.Text([],"")
335 and aux_option ~tail = function
336 None -> Box.Text([],"_")
337 | Some ast -> ast2box ~tail ast
339 and make_var ~tail = function
340 (Cic.Anonymous, None) -> Box.Text([],"_:_")
341 | (Cic.Anonymous, Some t) ->
342 Box.H([],[Box.Text([],"_:");ast2box ~tail t])
343 | (Cic.Name s, None) -> Box.Text([],s)
344 | (Cic.Name s, Some t) ->
346 Box.V([],[Box.Text([],s^":");
347 Box.indent(bigast2box ~tail t)])
349 Box.H([],[Box.Text([],s^":");Box.Object([],t)])
351 and make_pattern constr =
353 [] -> Box.Text([],constr)
360 (* ignoring the type *)
361 (Cic.Anonymous, _) -> Box.Text([],"_")
362 | (Cic.Name s, _) -> Box.Text([],s) in
363 Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
364 Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
367 and make_def let_txt var def end_txt =
370 (* ignoring the type *)
371 (Cic.Anonymous, _) -> Box.Text([],"_")
372 | (Cic.Name s, _) -> Box.Text([],s)) in
373 pretty_append ~tail:[end_txt]
374 [Box.Text([],let_txt);
382 and make_subst start_txt varname body end_txt =
383 pretty_append ~tail:[end_txt]
384 ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
385 [Box.Text([],varname);
387 Box.Text([],map_tex unicode "Assign")
391 and pretty_append ~tail l ast =
394 Box.H([],[Box.skip; bigast2box ~tail ast])]
396 [Box.H([],l@[Box.smallskip; (ast2box ~tail ast)])]
399 ast2box ~priority ~assoc ~tail t
402 let m_row_with_fences = P.row_with_brackets
403 let m_row = P.row_without_brackets
404 let m_open_fence = P.Mo([None, "stretchy", "false"], "(")
405 let m_close_fence = P.Mo([None, "stretchy", "false"], ")")
407 let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
408 let lookup_uri = function
412 Some (Hashtbl.find ids_to_uris id)
413 with Not_found -> None)
415 let make_std_attributes xref =
416 let uri = lookup_uri xref in
417 make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
421 | A.AttributedTerm (`Loc _, ast) -> aux ?xref ast
422 | A.AttributedTerm (`IdRef xref, ast) -> aux ~xref ast
423 | A.Symbol (name,_) ->
424 let attr = make_std_attributes xref in
426 | A.Ident (name,subst) ->
427 let attr = make_std_attributes xref in
441 | Some subst -> make_subst subst
444 | [] -> P.Mi (attr, name)
450 [(P.Mtext([],"]"))]))
452 let attr = make_attributes [Some "helm","xref"] [xref] in
460 P.Mrow ([],P.Mi (attr,"?" ^ string_of_int no) :: P.Mo ([],"[") ::
461 l' @ [P.Mo ([],"]")])
462 | A.Num (value, _) ->
463 let attr = make_attributes [Some "helm","xref"] [xref] in
465 | A.Sort `Prop -> P.Mtext ([], "Prop")
466 | A.Sort `Set -> P.Mtext ([], "Set")
467 | A.Sort `Type -> P.Mtext ([], "Type")
468 | A.Sort `CProp -> P.Mtext ([], "CProp")
469 | A.Implicit -> P.Mtext([], "?")
470 | A.UserInput -> P.Mtext([], "")
471 | A.Appl [] -> assert false
472 | A.Appl ((hd::tl) as l) ->
473 let rec find_symbol idref = function
474 | A.AttributedTerm (`Loc _, t) -> find_symbol None t
475 | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
476 | A.Symbol (name, _) ->
478 | None -> assert false
479 | Some idref -> `Symbol (name, idref))
483 let aattr = make_attributes [Some "helm","xref"] [xref] in
484 (match find_symbol None hd with
485 | `Symbol (name, sxref) ->
486 let sattr = make_std_attributes (Some sxref) in
488 (let f = Hashtbl.find symbol_table name in
489 f tl ~priority ~assoc ~ids_to_uris aattr sattr)
492 m_open_fence :: P.Mi(sattr,name)::(make_args tl) @
495 P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
497 | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
498 | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
499 let attr = make_attributes [Some "helm","xref"] [xref] in
502 P.Mtext ([], map_tex true "to");
504 | A.Binder (kind,var,body) ->
505 let attr = make_attributes [Some "helm","xref"] [xref] in
506 let binder = resolve_binder true kind in
507 let var = make_capture_variable var in
509 P.Mtext([None,"mathcolor","blue"],binder) :: var @
510 [P.Mo([],"."); aux body])
511 | A.LetIn (var,s,body) ->
512 let attr = make_attributes [Some "helm","xref"] [xref] in
514 P.Mtext([],("let ")) ::
515 (make_capture_variable var @
520 | A.LetRec (_, defs, body) ->
521 let attr = make_attributes [Some "helm","xref"] [xref] in
526 make_capture_variable var @ [P.Mtext([],"=");(aux body)]
527 | (var,body,_)::tl ->
528 make_capture_variable var @
530 (aux body)::P.Mtext([]," and")::(make_defs tl))) in
532 P.Mtext([],("let rec "))::
534 (P.Mtext([]," in ")::
536 | A.Case (arg,_,outtype,patterns) ->
537 (* TODO print outtype *)
538 let attr = make_attributes [Some "helm","xref"] [xref] in
539 let rec make_patterns =
542 | [(constr, vars),rhs] -> make_pattern constr vars rhs
543 | ((constr,vars), rhs)::tl ->
544 (make_pattern constr vars rhs)@(P.smallskip::
545 P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
546 and make_pattern constr vars rhs =
548 P.Mtext([], constr) ::
550 (List.map (fun var -> P.smallskip :: make_capture_variable var)
554 [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs]
557 P.Mtext([],"match")::P.smallskip::
558 (aux arg)::P.smallskip::
559 P.Mtext([],"with")::P.smallskip::
560 P.Mtext([],"[")::P.smallskip::
561 (make_patterns patterns)@(P.smallskip::[P.Mtext([],("]"))]))
563 and make_capture_variable (name, ty) =
566 | Cic.Anonymous -> [P.Mtext([], "_")]
567 | Cic.Name s -> [P.Mtext([], s)]
572 | Some ty -> [P.Mtext([],":"); aux ty]
576 and make_args ?(priority = 0) ?(assoc = false) =
579 | a::tl -> P.smallskip::(aux a)::(make_args tl)
585 let box_prefix = "b";;
587 let add_xml_declaration stream =
589 Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
591 Xml.xml_nempty ~prefix:box_prefix "box"
592 [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
593 Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ;
594 Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
595 Some "xmlns","xlink","http://www.w3.org/1999/xlink"
599 let ast2mpresXml ((ast, ids_to_uris) as arg) =
600 let astBox = ast2astBox arg in
601 let smallAst2mpresXml ast =
602 P.print_mpres (ast2mpres (ast, ids_to_uris))
604 (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)
606 let b_open_fence = Box.b_text [] "("
607 let b_close_fence = Box.b_text [] ")"
608 let b_v_with_fences attrs a b op =
617 let b_v_without_fences attrs a b op =
623 let _ = (** fill symbol_table *)
624 let binary f = function [a;b] -> f a b | _ -> assert false in
625 let unary f = function [a] -> f a | _ -> assert false in
626 let add_binary_op name threshold ?(assoc=`Left) symbol =
627 let assoc = match assoc with `Left -> true | `Right -> false in
628 Hashtbl.add symbol_table name (binary
629 (fun a b ~priority ~assoc ~ids_to_uris aattr sattr ->
632 | `Symbol name -> map_tex true name
635 if (priority > threshold) || (priority = threshold && assoc) then
636 m_row_with_fences aattr
637 (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
638 (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
642 (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
643 (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
644 (P.Mo(sattr,symbol))));
645 Hashtbl.add symbol_table_charcount name (binary
646 (fun a b ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr ->
649 | `Symbol name -> map_tex unicode name
653 if (priority > threshold) || (priority = threshold && assoc) then
654 b_v_with_fences aattr
655 (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
656 (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
658 (Box.Text(sattr,symbol))
660 b_v_without_fences aattr
661 (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
662 (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
664 (Box.Text(sattr,symbol))))
666 Hashtbl.add symbol_table "not" (unary
667 (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
669 m_open_fence; P.Mo([],map_tex true "lnot");
670 ast2mpres (a, ids_to_uris); m_close_fence]))));
671 Hashtbl.add symbol_table "inv" (unary
672 (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
674 P.Mrow([],[ m_open_fence; ast2mpres (a, ids_to_uris); m_close_fence]),
675 P.Mrow([],[ P.Mo([],"-"); P.Mn([],"1")]))));
676 Hashtbl.add symbol_table "opp" (unary
677 (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
681 ast2mpres (a, ids_to_uris);
683 add_binary_op "arrow" 5 ~assoc:`Right (`Symbol "to");
684 add_binary_op "eq" 40 (`Ascii "=");
685 add_binary_op "and" 20 (`Symbol "land");
686 add_binary_op "or" 10 (`Symbol "lor");
687 add_binary_op "iff" 5 (`Symbol "iff");
688 add_binary_op "leq" 40 (`Symbol "leq");
689 add_binary_op "lt" 40 (`Symbol "lt");
690 add_binary_op "geq" 40 (`Symbol "geq");
691 add_binary_op "gt" 40 (`Symbol "gt");
692 add_binary_op "plus" 60 (`Ascii "+");
693 add_binary_op "times" 70 (`Ascii "*");
694 add_binary_op "minus" 60 (`Ascii "-");
695 add_binary_op "div" 60 (`Ascii "/");