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
70 countterm (countterm (current_size + 3) bo) ty
71 | A.LetIn (var,s,t) ->
72 let size1 = countvar current_size var in
73 let size2 = countterm size1 s in
79 let size1 = countvar c var in
80 countterm size1 s) current_size l in
83 | A.Uri (s, None) -> current_size + (String.length s)
87 (fun c (v,t) -> countterm (c + (String.length v)) t)
88 (current_size + (String.length s)) l
89 | A.Implicit -> current_size + 1 (* underscore *)
94 None -> c + 1 (* underscore *)
95 | Some t -> countterm c t)
96 (current_size + 1) l (* num *)
97 | A.Num (s, _) -> current_size + String.length s
98 | A.Sort _ -> current_size + 4 (* sort name *)
99 | A.Symbol (s,_) -> current_size + String.length s
101 | A.UserInput -> current_size
105 ((countterm 0 t) > maxsize)
108 let rec make_attributes l1 =
111 | None::tl -> make_attributes (List.tl l1) tl
113 let p,n = List.hd l1 in
114 (p,n,s)::(make_attributes (List.tl l1) tl)
117 let map_tex unicode texcmd =
118 let default_map_tex = Printf.sprintf "\\%s " in
121 Utf8Macro.expand texcmd
122 with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd
124 default_map_tex texcmd
126 let resolve_binder unicode = function
127 | `Lambda -> map_tex unicode "lambda"
128 | `Pi -> map_tex unicode "Pi"
129 | `Forall -> map_tex unicode "forall"
130 | `Exists -> map_tex unicode "exists"
133 let rec make_args f ~tail = function
135 | [arg] -> [f ~tail arg]
136 | arg :: tl -> (f ~tail:[] arg) :: (make_args f ~tail tl)
138 let append_tail ~tail box =
141 | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
143 let rec find_symbol idref = function
144 | A.AttributedTerm (`Loc _, t) -> find_symbol None t
145 | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
146 | A.Symbol (name, _) -> `Symbol (name, idref)
149 let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
152 let lookup_uri = function
156 Some (Hashtbl.find ids_to_uris id)
157 with Not_found -> None)
159 let make_std_attributes xref =
160 let uri = lookup_uri xref in
161 make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
163 let rec ast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
165 bigast2box ~priority ~assoc ?xref ~tail t
167 let attrs = make_std_attributes xref in
168 append_tail ~tail (Box.Object (attrs, t))
170 bigast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
172 | A.AttributedTerm (`Loc _, t) -> bigast2box ?xref ~tail t
173 | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
174 | A.Appl [] -> assert false
175 | A.Appl ((hd::tl) as l) ->
176 let aattr = make_attributes [Some "helm","xref"] [xref] in
177 (match find_symbol None hd with
178 | `Symbol (name, sxref) ->
179 let sattr = make_std_attributes sxref in
181 (let f = Hashtbl.find symbol_table_charcount name in
182 f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
185 (make_attributes [Some "helm","xref"] [xref],
188 make_args (fun ~tail t -> ast2box ~tail t)
189 ~tail:(")" :: tail) l);
193 (make_attributes [Some "helm","xref"] [xref],
197 (fun ~tail t -> ast2box ~tail t)
198 ~tail:(")" :: tail) l)]
200 | A.Binder (`Forall, (Cic.Anonymous, typ), body)
201 | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
202 Box.V(make_attributes [Some "helm","xref"] [xref],
204 | None -> Box.Text([], "?")
205 | Some typ -> ast2box ~tail:[] typ);
208 Box.Text([], map_tex unicode "to");
209 ast2box ~tail body])])
210 | A.Binder(kind, var, body) ->
211 Box.V(make_attributes [Some "helm","xref"] [xref],
213 [Box.Text ([None,"color","blue"], resolve_binder unicode kind);
214 make_var ~tail:("." :: tail) var]);
215 Box.indent (ast2box ~tail body)])
216 | A.Case(arg, _, ty, pl) ->
217 let make_rule ~tail sep ((constr,vars),rhs) =
219 Box.V([],[Box.H([],[Box.Text([],sep);
221 make_pattern constr vars;
223 Box.Text([],map_tex unicode "Rightarrow")]);
224 Box.indent (bigast2box ~tail rhs)])
226 Box.H([],[Box.Text([],sep);
228 make_pattern constr vars;
230 Box.Text([],map_tex unicode "Rightarrow");
232 append_tail ~tail (Box.Object([],rhs))]) in
235 | [] -> append_tail ~tail (Box.Text([],"[]"))
236 | [r] -> (make_rule ~tail:("]" :: tail) "[" r)
239 (make_rule ~tail:[] "[" r) ::
241 (fun ~tail pat -> make_rule ~tail "|" pat)
248 [ Box.H([],[Box.Text([],"[");
254 Box.V(make_attributes [Some "helm","xref"] [xref],
256 [Box.Text([],"match");
257 Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg]));
261 Box.V(make_attributes [Some "helm","xref"] [xref],
263 [Box.H(make_attributes [Some "helm","xref"] [xref],
264 [Box.Text([],"match");
266 ast2box ~tail:[] arg;
268 Box.Text([],"with")]);
271 Box.V(make_attributes [Some "helm","xref"] [xref],
272 [Box.H([],[Box.Text([],"("); ast2box ~tail:[] bo]);
273 Box.H([],[Box.Text([],":"); ast2box ~tail ty;Box.Text([],")")])])
274 | A.LetIn (var, s, t) ->
275 Box.V(make_attributes [Some "helm","xref"] [xref],
276 (make_def "let" var s "in")@[ast2box ~tail t])
277 | A.LetRec (_, vars, body) ->
279 let rec make_defs let_txt = function
281 | [(var,s,_)] -> make_def let_txt var s "in"
283 (make_def let_txt var s "")@(make_defs "and" tl) in
284 make_defs "let rec" vars in
285 Box.V(make_attributes [Some "helm","xref"] [xref],
286 definitions@[ast2box ~tail body])
288 | A.Uri (s, subst) ->
290 let rec make_substs start_txt =
294 make_subst start_txt s t ""
296 (make_subst start_txt s t ";")@(make_substs "" tl)
301 [Box.Text(make_std_attributes xref,s);
303 [Box.Text([],"[...]");
304 Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
305 Box.V([], make_substs "" subst);
306 Box.Text([], "]")])])])
307 | None -> Box.Text(make_std_attributes xref, s)
311 Box.H([], (* attr here or on Vbox? *)
312 [Box.Text(make_std_attributes xref,s);
313 Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
314 (* Box.indent(Box.V([],subst))]) *)
317 Box.Text([],"_") (* big? *)
322 Box.H([],[aux_option ~tail t; Box.Text([],";")]))
324 Box.V(make_attributes [Some "helm","xref"] [xref],
325 [Box.Text([],"?"^(string_of_int n));
326 Box.H([],[Box.Text([],"[");
327 Box.V([],local_context);
333 `Prop -> Box.Text([],"Prop")
334 | `Set -> Box.Text([],"Set")
335 | `Type -> Box.Text([],"Type")
336 | `CProp -> Box.Text([],"CProp"))
340 | A.UserInput -> Box.Text([],"")
342 and aux_option ~tail = function
343 None -> Box.Text([],"_")
344 | Some ast -> ast2box ~tail ast
346 and make_var ~tail = function
347 (Cic.Anonymous, None) -> Box.Text([],"_:_")
348 | (Cic.Anonymous, Some t) ->
349 Box.H([],[Box.Text([],"_:");ast2box ~tail t])
350 | (Cic.Name s, None) -> Box.Text([],s)
351 | (Cic.Name s, Some t) ->
353 Box.V([],[Box.Text([],s^":");
354 Box.indent(bigast2box ~tail t)])
356 Box.H([],[Box.Text([],s^":");Box.Object([],t)])
358 and make_pattern constr =
360 [] -> Box.Text([],constr)
367 (* ignoring the type *)
368 (Cic.Anonymous, _) -> Box.Text([],"_")
369 | (Cic.Name s, _) -> Box.Text([],s) in
370 Box.smallskip::bv::acc) vars [Box.Text([],")")] in
371 Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
374 and make_def let_txt var def end_txt =
377 (* ignoring the type *)
378 (Cic.Anonymous, _) -> Box.Text([],"_")
379 | (Cic.Name s, _) -> Box.Text([],s)) in
380 pretty_append ~tail:[end_txt]
381 [Box.Text([],let_txt);
389 and make_subst start_txt varname body end_txt =
390 pretty_append ~tail:[end_txt]
391 ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
392 [Box.Text([],varname);
394 Box.Text([],map_tex unicode "Assign")
398 and pretty_append ~tail l ast =
401 Box.H([],[Box.skip; bigast2box ~tail ast])]
403 [Box.H([],l@[Box.smallskip; (ast2box ~tail ast)])]
406 ast2box ~priority ~assoc ~tail t
409 let m_row_with_fences = P.row_with_brackets
410 let m_row = P.row_without_brackets
411 let m_open_fence = P.Mo([None, "stretchy", "false"], "(")
412 let m_close_fence = P.Mo([None, "stretchy", "false"], ")")
414 let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
415 let lookup_uri = function
419 Some (Hashtbl.find ids_to_uris id)
420 with Not_found -> None)
422 let make_std_attributes xref =
423 let uri = lookup_uri xref in
424 make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
428 | A.AttributedTerm (`Loc _, ast) -> aux ?xref ast
429 | A.AttributedTerm (`IdRef xref, ast) -> aux ~xref ast
430 | A.Symbol (name,_) ->
431 let attr = make_std_attributes xref in
433 | A.Ident (name,subst)
434 | A.Uri (name,subst) ->
435 let attr = make_std_attributes xref in
449 | Some subst -> make_subst subst
452 | [] -> P.Mi (attr, name)
458 [(P.Mtext([],"]"))]))
460 let attr = make_attributes [Some "helm","xref"] [xref] in
468 P.Mrow ([],P.Mi (attr,"?" ^ string_of_int no) :: P.Mo ([],"[") ::
469 l' @ [P.Mo ([],"]")])
470 | A.Num (value, _) ->
471 let attr = make_attributes [Some "helm","xref"] [xref] in
473 | A.Sort `Prop -> P.Mtext ([], "Prop")
474 | A.Sort `Set -> P.Mtext ([], "Set")
475 | A.Sort `Type -> P.Mtext ([], "Type")
476 | A.Sort `CProp -> P.Mtext ([], "CProp")
477 | A.Implicit -> P.Mtext([], "?")
478 | A.UserInput -> P.Mtext([], "")
479 | A.Appl [] -> assert false
480 | A.Appl ((hd::tl) as l) ->
481 let aattr = make_attributes [Some "helm","xref"] [xref] in
482 (match find_symbol None hd with
483 | `Symbol (name, sxref) ->
484 let sattr = make_std_attributes sxref in
486 (let f = Hashtbl.find symbol_table name in
487 f tl ~priority ~assoc ~ids_to_uris aattr sattr)
490 m_open_fence :: P.Mi(sattr,name)::(make_args tl) @
493 P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
496 let attr = make_attributes [Some "helm","xref"] [xref] in
498 [m_open_fence; aux bo; P.Mo ([],":"); aux ty; m_close_fence])
499 | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
500 | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
501 let attr = make_attributes [Some "helm","xref"] [xref] in
504 P.Mtext ([], map_tex true "to");
506 | A.Binder (kind,var,body) ->
507 let attr = make_attributes [Some "helm","xref"] [xref] in
508 let binder = resolve_binder true kind in
509 let var = make_capture_variable var in
511 P.Mtext([None,"mathcolor","blue"],binder) :: var @
512 [P.Mo([],"."); aux body])
513 | A.LetIn (var,s,body) ->
514 let attr = make_attributes [Some "helm","xref"] [xref] in
516 P.Mtext([],("let ")) ::
517 (make_capture_variable var @
522 | A.LetRec (_, defs, body) ->
523 let attr = make_attributes [Some "helm","xref"] [xref] in
528 make_capture_variable var @ [P.Mtext([],"=");(aux body)]
529 | (var,body,_)::tl ->
530 make_capture_variable var @
532 (aux body)::P.Mtext([]," and")::(make_defs tl))) in
534 P.Mtext([],("let rec "))::
536 (P.Mtext([]," in ")::
538 | A.Case (arg,_,outtype,patterns) ->
539 (* TODO print outtype *)
540 let attr = make_attributes [Some "helm","xref"] [xref] in
541 let rec make_patterns =
544 | [(constr, vars),rhs] -> make_pattern constr vars rhs
545 | ((constr,vars), rhs)::tl ->
546 (make_pattern constr vars rhs)@(P.smallskip::
547 P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
548 and make_pattern constr vars rhs =
550 P.Mtext([], constr) ::
553 (fun var -> P.smallskip :: make_capture_variable var)
557 [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs]
560 P.Mtext([],"match")::P.smallskip::
561 (aux arg)::P.smallskip::
562 P.Mtext([],"with")::P.smallskip::
563 P.Mtext([],"[")::P.smallskip::
564 (make_patterns patterns)@(P.smallskip::[P.Mtext([],("]"))]))
566 and make_capture_variable (name, ty) =
569 | Cic.Anonymous -> [P.Mtext([], "_")]
570 | Cic.Name s -> [P.Mtext([], s)]
575 | Some ty -> [P.Mtext([],":"); aux ty]
579 and make_args ?(priority = 0) ?(assoc = false) =
582 | a::tl -> P.smallskip::(aux a)::(make_args tl)
588 let box_prefix = "b";;
590 let add_xml_declaration stream =
592 Xml.xml_cdata "<?xml version=\"1.0\" ?>\n" ;
594 Xml.xml_nempty ~prefix:box_prefix "box"
595 [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
596 Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ;
597 Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
598 Some "xmlns","xlink","http://www.w3.org/1999/xlink"
602 let ast2mpresXml ((ast, ids_to_uris) as arg) =
603 let astBox = ast2astBox arg in
604 let smallAst2mpresXml ast =
605 P.print_mpres (fun _ -> assert false) (ast2mpres (ast, ids_to_uris))
607 (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)
609 let b_open_fence = Box.b_text [] "("
610 let b_close_fence = Box.b_text [] ")"
611 let b_v_with_fences attrs a b op =
620 let b_v_without_fences attrs a b op =
626 let _ = (** fill symbol_table *)
627 let binary f = function [a;b] -> f a b | _ -> assert false in
628 let unary f = function [a] -> f a | _ -> assert false in
629 let add_binary_op name threshold ?(assoc=`Left) symbol =
630 let assoc = match assoc with `Left -> true | `Right -> false in
631 Hashtbl.add symbol_table name (binary
632 (fun a b ~priority ~assoc ~ids_to_uris aattr sattr ->
635 | `Symbol name -> map_tex true name
638 if (priority > threshold) || (priority = threshold && assoc) then
639 m_row_with_fences aattr
640 (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
641 (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
645 (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
646 (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
647 (P.Mo(sattr,symbol))));
648 Hashtbl.add symbol_table_charcount name (binary
649 (fun a b ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr ->
652 | `Symbol name -> map_tex unicode name
656 if (priority > threshold) || (priority = threshold && assoc) then
657 b_v_with_fences aattr
658 (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
659 (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
661 (Box.Text(sattr,symbol))
663 b_v_without_fences aattr
664 (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
665 (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
667 (Box.Text(sattr,symbol))))
669 Hashtbl.add symbol_table "not" (unary
670 (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
672 m_open_fence; P.Mo([],map_tex true "lnot");
673 ast2mpres (a, ids_to_uris); m_close_fence]))));
674 Hashtbl.add symbol_table "inv" (unary
675 (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
677 P.Mrow([],[ m_open_fence; ast2mpres (a, ids_to_uris); m_close_fence]),
678 P.Mrow([],[ P.Mo([],"-"); P.Mn([],"1")]))));
679 Hashtbl.add symbol_table "opp" (unary
680 (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
684 ast2mpres (a, ids_to_uris);
686 add_binary_op "arrow" 5 ~assoc:`Right (`Symbol "to");
687 add_binary_op "eq" 40 (`Ascii "=");
688 add_binary_op "and" 20 (`Symbol "land");
689 add_binary_op "or" 10 (`Symbol "lor");
690 add_binary_op "iff" 5 (`Symbol "iff");
691 add_binary_op "leq" 40 (`Symbol "leq");
692 add_binary_op "lt" 40 (`Symbol "lt");
693 add_binary_op "geq" 40 (`Symbol "geq");
694 add_binary_op "gt" 40 (`Symbol "gt");
695 add_binary_op "plus" 60 (`Ascii "+");
696 add_binary_op "times" 70 (`Ascii "*");
697 add_binary_op "minus" 60 (`Ascii "-");
698 add_binary_op "div" 60 (`Ascii "/");
699 add_binary_op "cast" 80 (`Ascii ":");