helm/ocaml/cic_transformations/ast2pres.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (**************************************************************************)
  27 (*                                                                        *)
  28 (*                           PROJECT HELM                                 *)
  29 (*                                                                        *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
  31 (*                             28/6/2003                                  *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35 module A = CicAst;;
  36 module P = Mpresentation;;
  37
  38 let symbol_table = Hashtbl.create 503;;
  39 let symbol_table_charcount = Hashtbl.create 503;;
  40
  41 let maxsize = 25;;
  42
  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
  48
  49 and countterm current_size t =
  50   if current_size > maxsize then current_size
  51   else match t with
  52       A.AttributedTerm (_,t) -> countterm current_size t
  53     | A.Appl l ->
  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 *)
  60         let size2 =
  61           match ty with
  62               None -> size1
  63             | Some ty -> countterm size1 ty in
  64         List.fold_left
  65           (fun c ((constr,vars),action) ->
  66              let size3 =
  67                List.fold_left countvar (c+String.length constr) vars in
  68              countterm size3 action) size2 pl
  69     | A.Cast (bo,ty) ->
  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
  74         countterm size2 t
  75     | A.LetRec (_,l,t) ->
  76         let size1 =
  77           List.fold_left
  78             (fun c (var,s,_) ->
  79                let size1 = countvar c var in
  80                countterm size1 s) current_size l in
  81           countterm size1 t
  82     | A.Ident (s,None)
  83     | A.Uri (s, None) -> current_size + (String.length s)
  84     | A.Ident (s,Some l)
  85     | A.Uri (s,Some l) ->
  86         List.fold_left
  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 *)
  90     | A.Meta (_,l) ->
  91         List.fold_left
  92           (fun c t ->
  93              match t with
  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
 100
 101     | A.UserInput -> current_size
 102 ;;
 103
 104 let is_big t =
 105   ((countterm 0 t) > maxsize)
 106 ;;
 107
 108 let rec make_attributes l1 =
 109   function
 110       [] -> []
 111     | None::tl -> make_attributes (List.tl l1) tl
 112     | (Some s)::tl ->
 113        let p,n = List.hd l1 in
 114         (p,n,s)::(make_attributes (List.tl l1) tl)
 115 ;;
 116
 117 let map_tex unicode texcmd =
 118   let default_map_tex = Printf.sprintf "\\%s " in
 119   if unicode then
 120     try
 121       Utf8Macro.expand texcmd
 122     with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd
 123   else
 124     default_map_tex texcmd
 125
 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"
 131 ;;
 132
 133 let rec make_args f ~tail = function
 134     | [] -> assert false
 135     | [arg] -> [f ~tail arg]
 136     | arg :: tl -> (f ~tail:[] arg) :: (make_args f ~tail tl)
 137
 138 let append_tail ~tail box =
 139   match tail with
 140   | [] -> box
 141   | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
 142
 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)
 147   | _ -> `None
 148
 149 let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
 150   (t, ids_to_uris)
 151 =
 152   let lookup_uri = function
 153     | None -> None
 154     | Some id ->
 155         (try
 156           Some (Hashtbl.find ids_to_uris id)
 157         with Not_found -> None)
 158   in
 159   let make_std_attributes xref =
 160     let uri = lookup_uri xref in
 161     make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
 162   in
 163   let rec ast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
 164     if is_big t then
 165       bigast2box ~priority ~assoc ?xref ~tail t
 166     else
 167       let attrs = make_std_attributes xref in
 168       append_tail ~tail (Box.Object (attrs, t))
 169   and
 170   bigast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
 171   match t with
 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
 180             (try
 181               (let f = Hashtbl.find symbol_table_charcount name in
 182                f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
 183             with Not_found ->
 184               Box.H
 185                 (make_attributes [Some "helm","xref"] [xref],
 186                  [Box.Text([],"(");
 187                   Box.V([],
 188                     make_args (fun ~tail t -> ast2box ~tail t)
 189                       ~tail:(")" :: tail) l);
 190                   Box.Text([],")")]))
 191         | `None ->
 192             Box.H
 193               (make_attributes [Some "helm","xref"] [xref],
 194                [Box.Text([],"(");
 195                 Box.V([],
 196                   make_args
 197                     (fun ~tail t -> ast2box ~tail t)
 198                     ~tail:(")" :: tail) l)]
 199                 ))
 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],
 203           [(match typ with
 204             | None -> Box.Text([], "?")
 205             | Some typ -> ast2box ~tail:[] typ);
 206             Box.H([],
 207               [Box.skip;
 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],
 212               [Box.H([],
 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) =
 218           if (is_big rhs) then
 219             Box.V([],[Box.H([],[Box.Text([],sep);
 220                                 Box.smallskip;
 221                                 make_pattern constr vars;
 222                                 Box.smallskip;
 223                                 Box.Text([],map_tex unicode "Rightarrow")]);
 224                       Box.indent (bigast2box ~tail rhs)])
 225           else
 226             Box.H([],[Box.Text([],sep);
 227                       Box.smallskip;
 228                       make_pattern constr vars;
 229                       Box.smallskip;
 230                       Box.Text([],map_tex unicode "Rightarrow");
 231                       Box.smallskip;
 232                       append_tail ~tail (Box.Object([],rhs))]) in
 233         let plbox =
 234           match pl with
 235           | [] -> append_tail ~tail (Box.Text([],"[]"))
 236           | [r] -> (make_rule ~tail:("]" :: tail) "[" r)
 237           | r::tl ->
 238               Box.V([],
 239                 (make_rule ~tail:[] "[" r) ::
 240                 (make_args
 241                   (fun ~tail pat -> make_rule ~tail "|" pat)
 242                   ~tail:("]" :: tail)
 243                   tl))
 244         in
 245         let ty_box =
 246           match ty with
 247           | Some ty ->
 248               [ Box.H([],[Box.Text([],"[");
 249                          ast2box ~tail:[] ty;
 250                          Box.Text([],"]")]) ]
 251           | None -> []
 252         in
 253         if is_big arg then
 254           Box.V(make_attributes [Some "helm","xref"] [xref],
 255                  ty_box @
 256                  [Box.Text([],"match");
 257                  Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg]));
 258                  Box.Text([],"with");
 259                  Box.indent plbox])
 260         else
 261           Box.V(make_attributes [Some "helm","xref"] [xref],
 262                 ty_box @
 263                 [Box.H(make_attributes [Some "helm","xref"] [xref],
 264                        [Box.Text([],"match");
 265                         Box.smallskip;
 266                         ast2box ~tail:[] arg;
 267                         Box.smallskip;
 268                         Box.Text([],"with")]);
 269                  Box.indent plbox])
 270     | A.Cast (bo,ty) ->
 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) ->
 278         let definitions =
 279           let rec make_defs let_txt = function
 280               [] -> []
 281             | [(var,s,_)] -> make_def let_txt var s "in"
 282             | (var,s,_)::tl ->
 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])
 287     | A.Ident (s, subst)
 288     | A.Uri (s, subst) ->
 289         let subst =
 290           let rec make_substs start_txt =
 291             function
 292               [] -> []
 293             | [(s,t)] ->
 294                 make_subst start_txt s t ""
 295             | (s,t)::tl ->
 296                 (make_subst start_txt s t ";")@(make_substs "" tl)
 297           in
 298           match subst with
 299           | Some subst ->
 300               Box.H([],
 301                     [Box.Text(make_std_attributes xref,s);
 302                      Box.Action([],
 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)
 308         in
 309          subst
 310         (*
 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))]) *)
 315         *)
 316     | A.Implicit ->
 317         Box.Text([],"_") (* big? *)
 318     | A.Meta (n, l) ->
 319         let local_context =
 320           List.map
 321             (function t ->
 322                Box.H([],[aux_option ~tail t; Box.Text([],";")]))
 323             l in
 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);
 328                          Box.Text([],"]")])])
 329     | A.Num (s, _) ->
 330          Box.Text([],s)
 331     | A.Sort kind ->
 332         (match kind with
 333              `Prop -> Box.Text([],"Prop")
 334            | `Set -> Box.Text([],"Set")
 335            | `Type -> Box.Text([],"Type")
 336            | `CProp -> Box.Text([],"CProp"))
 337     | A.Symbol (s, _) ->
 338         Box.Text([],s)
 339
 340     | A.UserInput -> Box.Text([],"")
 341
 342   and aux_option ~tail = function
 343       None  -> Box.Text([],"_")
 344     | Some ast -> ast2box ~tail ast
 345
 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) ->
 352         if is_big t then
 353           Box.V([],[Box.Text([],s^":");
 354                     Box.indent(bigast2box ~tail t)])
 355         else
 356           Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 357
 358   and make_pattern constr =
 359     function
 360         [] -> Box.Text([],constr)
 361       | vars ->
 362           let bvars =
 363             List.fold_right
 364               (fun var acc ->
 365                  let bv =
 366                    match var with
 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)
 372
 373
 374   and make_def let_txt var def end_txt =
 375     let name =
 376       (match var with
 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);
 382        Box.smallskip;
 383        name;
 384        Box.smallskip;
 385        Box.Text([],"=")
 386       ]
 387       def
 388
 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);
 393         Box.smallskip;
 394         Box.Text([],map_tex unicode "Assign")
 395        ])
 396       body
 397
 398   and pretty_append ~tail l ast =
 399     if is_big ast then
 400       [Box.H([],l);
 401        Box.H([],[Box.skip; bigast2box ~tail ast])]
 402     else
 403       [Box.H([],l@[Box.smallskip; (ast2box ~tail ast)])]
 404
 405 in
 406 ast2box ~priority ~assoc ~tail t
 407 ;;
 408
 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"], ")")
 413
 414 let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
 415   let lookup_uri = function
 416     | None -> None
 417     | Some id ->
 418         (try
 419           Some (Hashtbl.find ids_to_uris id)
 420         with Not_found -> None)
 421   in
 422   let make_std_attributes xref =
 423     let uri = lookup_uri xref in
 424     make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
 425   in
 426   let rec aux ?xref =
 427   function
 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
 432         P.Mi (attr,name)
 433     | A.Ident (name,subst)
 434     | A.Uri (name,subst) ->
 435         let attr = make_std_attributes xref in
 436         let rec make_subst =
 437           (function
 438               [] -> []
 439             | (n,a)::tl ->
 440                 (aux a)::
 441                 P.Mtext([],"/")::
 442                 P.Mi([],n)::
 443                 P.Mtext([],"; ")::
 444                 P.smallskip::
 445                 (make_subst tl)) in
 446         let subst =
 447           match subst with
 448           | None -> []
 449           | Some subst -> make_subst subst
 450         in
 451         (match subst with
 452         | [] -> P.Mi (attr, name)
 453         | _ ->
 454             P.Mrow ([],
 455               P.Mi (attr,name)::
 456               P.Mtext([],"[")::
 457               subst @
 458               [(P.Mtext([],"]"))]))
 459     | A.Meta (no,l) ->
 460         let attr = make_attributes [Some "helm","xref"] [xref] in
 461         let l' =
 462          List.map
 463           (function
 464               None -> P.Mo([],"_")
 465             | Some t -> aux t
 466           ) l
 467         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
 472         P.Mn (attr,value)
 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
 485             (try
 486               (let f = Hashtbl.find symbol_table name in
 487                f tl ~priority ~assoc ~ids_to_uris aattr sattr)
 488             with Not_found ->
 489               P.Mrow(aattr,
 490               m_open_fence :: P.Mi(sattr,name)::(make_args tl) @
 491               [m_close_fence]))
 492         | `None ->
 493             P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
 494             [m_close_fence]))
 495     | A.Cast (bo,ty) ->
 496        let attr = make_attributes [Some "helm","xref"] [xref] in
 497         P.Mrow (attr,
 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
 502         P.Mrow (attr, [
 503           aux ty;
 504           P.Mtext ([], map_tex true "to");
 505           aux body])
 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
 510         P.Mrow (attr,
 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
 515         P.Mrow (attr,
 516            P.Mtext([],("let ")) ::
 517            (make_capture_variable var @
 518            P.Mtext([],("="))::
 519            (aux s)::
 520            P.Mtext([]," in ")::
 521            [aux body]))
 522     | A.LetRec (_, defs, body) ->
 523         let attr = make_attributes [Some "helm","xref"] [xref] in
 524         let rec make_defs =
 525           (function
 526                [] -> assert false
 527              | [(var,body,_)] ->
 528                  make_capture_variable var @ [P.Mtext([],"=");(aux body)]
 529              | (var,body,_)::tl ->
 530                  make_capture_variable var @
 531                  (P.Mtext([],"=")::
 532                   (aux body)::P.Mtext([]," and")::(make_defs tl))) in
 533         P.Mrow (attr,
 534           P.Mtext([],("let rec "))::
 535           (make_defs defs)@
 536            (P.Mtext([]," in ")::
 537            [aux body]))
 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 =
 542           (function
 543                [] -> []
 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 =
 549           let lhs =
 550             P.Mtext([], constr) ::
 551               (List.concat
 552                 (List.map
 553                   (fun var -> P.smallskip :: make_capture_variable var)
 554                   vars))
 555           in
 556           lhs @
 557           [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs]
 558         in
 559         P.Mrow (attr,
 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([],("]"))]))
 565
 566   and make_capture_variable (name, ty) =
 567     let name =
 568       match name with
 569       | Cic.Anonymous -> [P.Mtext([], "_")]
 570       | Cic.Name s -> [P.Mtext([], s)]
 571     in
 572     let ty =
 573       match ty with
 574       | None -> []
 575       | Some ty -> [P.Mtext([],":"); aux ty]
 576     in
 577     name @ ty
 578
 579   and make_args ?(priority = 0) ?(assoc = false) =
 580     function
 581         [] -> []
 582       | a::tl -> P.smallskip::(aux a)::(make_args tl)
 583
 584   in
 585   aux ast
 586 ;;
 587
 588 let box_prefix = "b";;
 589
 590 let add_xml_declaration stream =
 591   [<
 592     Xml.xml_cdata "<?xml version=\"1.0\" ?>\n" ;
 593     Xml.xml_cdata "\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"
 599       ] stream
 600   >]
 601
 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))
 606   in
 607   (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)
 608
 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 =
 612   Box.b_h attrs [
 613     b_open_fence;
 614     Box.b_v [] [
 615       a;
 616       Box.b_h [] [ op; b ]
 617     ];
 618     b_close_fence
 619   ]
 620 let b_v_without_fences attrs a b op =
 621   Box.b_v attrs [
 622     a;
 623     Box.b_h [] [ op; b ]
 624   ]
 625
 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 ->
 633         let symbol =
 634           match symbol with
 635           | `Symbol name -> map_tex true name
 636           | `Ascii s -> s
 637         in
 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))
 642              (P.Mo(sattr,symbol))
 643          else
 644            m_row aattr
 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 ->
 650         let symbol =
 651           match symbol with
 652           | `Symbol name -> map_tex unicode name
 653           | `Ascii s -> s
 654         in
 655
 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
 660               (b, ids_to_uris))
 661              (Box.Text(sattr,symbol))
 662          else
 663            b_v_without_fences aattr
 664              (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
 665              (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
 666               (b, ids_to_uris))
 667              (Box.Text(sattr,symbol))))
 668   in
 669   Hashtbl.add symbol_table "not" (unary
 670     (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
 671        (P.Mrow([], [
 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 ->
 676       P.Msup([],
 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 ->
 681       P.Mrow([],[
 682         P.Mo([],"-");
 683         m_open_fence;
 684         ast2mpres (a, ids_to_uris);
 685         m_close_fence])));
 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 ":");
 700