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.LetIn (var,s,t) ->
  70         let size1 = countvar current_size var in
  71         let size2 = countterm size1 s in
  72         countterm size2 t
  73     | A.LetRec (_,l,t) ->
  74         let size1 =
  75           List.fold_left
  76             (fun c (var,s,_) ->
  77                let size1 = countvar c var in
  78                countterm size1 s) current_size l in
  79           countterm size1 t
  80     | A.Ident(s,None) -> current_size + (String.length s)
  81     | A.Ident(s,Some l) ->
  82         List.fold_left
  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 *)
  86     | A.Meta (_,l) ->
  87         List.fold_left
  88           (fun c t ->
  89              match t with
  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
  96 ;;
  97
  98 let is_big t =
  99   ((countterm 0 t) > maxsize)
 100 ;;
 101
 102 let rec make_attributes l1 =
 103   function
 104       [] -> []
 105     | None::tl -> make_attributes (List.tl l1) tl
 106     | (Some s)::tl ->
 107        let p,n = List.hd l1 in
 108         (p,n,s)::(make_attributes (List.tl l1) tl)
 109 ;;
 110
 111 let map_tex unicode texcmd =
 112   let default_map_tex = Printf.sprintf "\\%s " in
 113   if unicode then
 114     try
 115       Utf8Macro.expand texcmd
 116     with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd
 117   else
 118     default_map_tex texcmd
 119
 120 let resolve_binder unicode = function
 121   | `Lambda -> map_tex unicode "lambda"
 122   | `Pi -> map_tex unicode "Pi"
 123   | `Forall -> map_tex unicode "forall"
 124   | `Exists -> map_tex unicode "exists"
 125 ;;
 126
 127 let rec make_args f ~tail = function
 128     | [] -> assert false
 129     | [arg] -> [f ~tail arg]
 130     | arg :: tl -> (f ~tail:[] arg) :: (make_args f ~tail tl)
 131
 132 let append_tail ~tail box =
 133   match tail with
 134   | [] -> box
 135   | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
 136
 137 let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
 138   (t, ids_to_uris)
 139 =
 140   let lookup_uri = function
 141     | None -> None
 142     | Some id ->
 143         (try
 144           Some (Hashtbl.find ids_to_uris id)
 145         with Not_found -> None)
 146   in
 147   let make_std_attributes xref =
 148     let uri = lookup_uri xref in
 149     make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
 150   in
 151   let rec ast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
 152     if is_big t then
 153       bigast2box ~priority ~assoc ?xref ~tail t
 154     else
 155       let attrs = make_std_attributes xref in
 156       append_tail ~tail (Box.Object (attrs, t))
 157   and
 158   bigast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
 159   match t with
 160     | A.AttributedTerm (`Loc _, t) -> bigast2box ?xref ~tail t
 161     | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
 162     | A.Appl [] -> assert false
 163     | A.Appl ((hd::tl) as l) ->
 164         let rec find_symbol idref = function
 165           | A.AttributedTerm (`Loc _, t) -> find_symbol None t
 166           | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
 167           | A.Symbol (name, _) ->
 168               (match idref with
 169               | None -> assert false
 170               | Some idref -> `Symbol (name, idref))
 171           | _ -> `None
 172         in
 173         let aattr = make_attributes [Some "helm","xref"] [xref] in
 174         (match find_symbol None hd with
 175         | `Symbol (name, sxref) ->
 176             let sattr = make_std_attributes (Some sxref) in
 177             (try
 178               (let f = Hashtbl.find symbol_table_charcount name in
 179                f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
 180             with Not_found ->
 181               Box.H
 182                 (make_attributes [Some "helm","xref"] [xref],
 183                  [Box.Text([],"(");
 184                   Box.V([],
 185                     make_args (fun ~tail t -> ast2box ~tail t)
 186                       ~tail:(")" :: tail) l);
 187                   Box.Text([],")")]))
 188         | `None ->
 189             Box.H
 190               (make_attributes [Some "helm","xref"] [xref],
 191                [Box.Text([],"(");
 192                 Box.V([],
 193                   make_args
 194                     (fun ~tail t -> ast2box ~tail t)
 195                     ~tail:(")" :: tail) l)]
 196                 ))
 197     | A.Binder (`Forall, (Cic.Anonymous, typ), body)
 198     | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
 199         Box.V(make_attributes [Some "helm","xref"] [xref],
 200           [(match typ with
 201             | None -> Box.Text([], "?")
 202             | Some typ -> ast2box ~tail:[] typ);
 203             Box.H([],
 204               [Box.skip;
 205                Box.Text([], map_tex unicode "to");
 206                ast2box ~tail body])])
 207     | A.Binder(kind, var, body) ->
 208         Box.V(make_attributes [Some "helm","xref"] [xref],
 209               [Box.H([],
 210                 [Box.Text ([None,"color","blue"], resolve_binder unicode kind);
 211                  make_var ~tail:("." :: tail) var]);
 212                Box.indent (ast2box ~tail body)])
 213     | A.Case(arg, _, ty, pl) ->
 214         let make_rule ~tail sep ((constr,vars),rhs) =
 215           if (is_big rhs) then
 216             Box.V([],[Box.H([],[Box.Text([],sep);
 217                                 Box.smallskip;
 218                                 make_pattern constr vars;
 219                                 Box.smallskip;
 220                                 Box.Text([],map_tex unicode "Rightarrow")]);
 221                       Box.indent (bigast2box ~tail rhs)])
 222           else
 223             Box.H([],[Box.Text([],sep);
 224                       Box.smallskip;
 225                       make_pattern constr vars;
 226                       Box.smallskip;
 227                       Box.Text([],map_tex unicode "Rightarrow");
 228                       Box.smallskip;
 229                       Box.Object([],rhs)]) in
 230         let plbox = match pl with
 231             [] -> Box.Text([],"[]")
 232           | r::tl ->
 233               Box.V([],
 234                 (make_rule ~tail:[] "[" r) ::
 235                 (make_args
 236                   (fun ~tail pat -> make_rule ~tail:[] "|" pat)
 237                   ~tail:("]" :: tail)
 238                   tl))
 239         in
 240         let ty_box =
 241           match ty with
 242           | Some ty ->
 243               [ Box.H([],[Box.Text([],"[");
 244                          ast2box ~tail ty;
 245                          Box.Text([],"]")]) ]
 246           | None -> []
 247         in
 248         if is_big arg then
 249           Box.V(make_attributes [Some "helm","xref"] [xref],
 250                  ty_box @
 251                  [Box.Text([],"match");
 252                  Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg]));
 253                  Box.Text([],"with");
 254                  Box.indent plbox])
 255         else
 256           Box.V(make_attributes [Some "helm","xref"] [xref],
 257                 ty_box @
 258                 [Box.H(make_attributes [Some "helm","xref"] [xref],
 259                        [Box.Text([],"match");
 260                         Box.smallskip;
 261                         ast2box ~tail arg;
 262                         Box.smallskip;
 263                         Box.Text([],"with")]);
 264                  Box.indent plbox])
 265     | A.LetIn (var, s, t) ->
 266         Box.V(make_attributes [Some "helm","xref"] [xref],
 267               (make_def "let" var s "in")@[ast2box ~tail t])
 268     | A.LetRec (_, vars, body) ->
 269         let definitions =
 270           let rec make_defs let_txt = function
 271               [] -> []
 272             | [(var,s,_)] ->
 273                 make_def let_txt var s "in"
 274             | (var,s,_)::tl ->
 275                 (make_def let_txt var s "")@(make_defs "and" tl) in
 276           make_defs "let rec" vars in
 277         Box.V(make_attributes [Some "helm","xref"] [xref],
 278               definitions@[ast2box ~tail body])
 279     | A.Ident (s, subst) ->
 280         let subst =
 281           let rec make_substs start_txt =
 282             function
 283               [] -> []
 284             | [(s,t)] ->
 285                 make_subst start_txt s t "]"
 286             | (s,t)::tl ->
 287                 (make_subst start_txt s t ";")@(make_substs " " tl)
 288           in
 289           match subst with
 290           | Some subst -> make_substs ((map_tex unicode "subst") ^ "[") subst
 291           | None -> []
 292         in
 293         Box.V([], (* attr here or on Vbox? *)
 294               [Box.Text(make_std_attributes xref,s);
 295                Box.indent(Box.V([],subst))])
 296     | A.Implicit ->
 297         Box.Text([],"_") (* big? *)
 298     | A.Meta (n, l) ->
 299         let local_context =
 300           List.map
 301             (function t ->
 302                Box.H([],[aux_option ~tail t; Box.Text([],";")]))
 303             l in
 304         Box.V(make_attributes [Some "helm","xref"] [xref],
 305               [Box.Text([],"?"^(string_of_int n));
 306                Box.H([],[Box.Text([],"[");
 307                          Box.V([],local_context);
 308                          Box.Text([],"]")])])
 309     | A.Num (s, _) ->
 310          Box.Text([],s)
 311     | A.Sort kind ->
 312         (match kind with
 313              `Prop -> Box.Text([],"Prop")
 314            | `Set -> Box.Text([],"Set")
 315            | `Type -> Box.Text([],"Type")
 316            | `CProp -> Box.Text([],"CProp"))
 317     | A.Symbol (s, _) ->
 318         Box.Text([],s)
 319
 320   and aux_option ~tail = function
 321       None  -> Box.Text([],"_")
 322     | Some ast -> ast2box ~tail ast
 323
 324   and make_var ~tail = function
 325       (Cic.Anonymous, None) -> Box.Text([],"_:_")
 326     | (Cic.Anonymous, Some t) ->
 327         Box.H([],[Box.Text([],"_:");ast2box ~tail t])
 328     | (Cic.Name s, None) -> Box.Text([],s)
 329     | (Cic.Name s, Some t) ->
 330         if is_big t then
 331           Box.V([],[Box.Text([],s^":");
 332                     Box.indent(bigast2box ~tail t)])
 333         else
 334           Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 335
 336   and make_pattern constr =
 337     function
 338         [] -> Box.Text([],constr)
 339       | vars ->
 340           let bvars =
 341             List.fold_right
 342               (fun var acc ->
 343                  let bv =
 344                    match var with
 345                        (* ignoring the type *)
 346                        (Cic.Anonymous, _) -> Box.Text([],"_")
 347                      | (Cic.Name s, _) -> Box.Text([],s) in
 348                    Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
 349             Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
 350
 351
 352   and make_def let_txt var def end_txt =
 353     let name =
 354       (match var with
 355            (* ignoring the type *)
 356            (Cic.Anonymous, _) -> Box.Text([],"_")
 357          | (Cic.Name s, _) -> Box.Text([],s)) in
 358     pretty_append ~tail:[end_txt]
 359       [Box.Text([],let_txt);
 360        Box.smallskip;
 361        name;
 362        Box.smallskip;
 363        Box.Text([],"=")
 364       ]
 365       def
 366
 367   and make_subst start_txt varname body end_txt =
 368     pretty_append ~tail:[end_txt]
 369       [Box.Text([],start_txt);
 370        Box.Text([],varname);
 371        Box.smallskip;
 372        Box.Text([],map_tex unicode "Assign")
 373       ]
 374       body
 375
 376   and pretty_append ~tail l ast =
 377     if is_big ast then
 378       [Box.H([],l);
 379        Box.H([],[Box.skip; bigast2box ~tail ast])]
 380     else
 381       [Box.H([],l@[Box.smallskip; (ast2box ~tail ast)])]
 382
 383 in
 384 ast2box ~priority ~assoc ~tail t
 385 ;;
 386
 387 let m_row_with_fences = P.row_with_brackets
 388 let m_row = P.row_without_brackets
 389 let m_open_fence = P.Mo([None, "stretchy", "false"], "(")
 390 let m_close_fence = P.Mo([None, "stretchy", "false"], ")")
 391
 392 let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
 393   let lookup_uri = function
 394     | None -> None
 395     | Some id ->
 396         (try
 397           Some (Hashtbl.find ids_to_uris id)
 398         with Not_found -> None)
 399   in
 400   let make_std_attributes xref =
 401     let uri = lookup_uri xref in
 402     make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
 403   in
 404   let rec aux ?xref =
 405   function
 406     | A.AttributedTerm (`Loc _, ast) -> aux ?xref ast
 407     | A.AttributedTerm (`IdRef xref, ast) -> aux ~xref ast
 408     | A.Symbol (name,_) ->
 409         let attr = make_std_attributes xref in
 410         P.Mi (attr,name)
 411     | A.Ident (name,subst) ->
 412         let attr = make_std_attributes xref in
 413         let rec make_subst =
 414           (function
 415               [] -> []
 416             | (n,a)::tl ->
 417                 (aux a)::
 418                 P.Mtext([],"/")::
 419                 P.Mi([],n)::
 420                 P.Mtext([],"; ")::
 421                 P.smallskip::
 422                 (make_subst tl)) in
 423         let subst =
 424           match subst with
 425           | None -> []
 426           | Some subst -> make_subst subst
 427         in
 428         (match subst with
 429         | [] -> P.Mi (attr, name)
 430         | _ ->
 431             P.Mrow ([],
 432               P.Mi (attr,name)::
 433               P.Mtext([],"[")::
 434               subst @
 435               [(P.Mtext([],"]"))]))
 436     | A.Meta (no,l) ->
 437         let attr = make_attributes [Some "helm","xref"] [xref] in
 438         let l' =
 439          List.map
 440           (function
 441               None -> P.Mo([],"_")
 442             | Some t -> aux t
 443           ) l
 444         in
 445          P.Mrow ([],P.Mi (attr,"?" ^ string_of_int no) :: P.Mo ([],"[") ::
 446            l' @ [P.Mo ([],"]")])
 447     | A.Num (value, _) ->
 448         let attr = make_attributes [Some "helm","xref"] [xref] in
 449         P.Mn (attr,value)
 450     | A.Sort `Prop -> P.Mtext ([], "Prop")
 451     | A.Sort `Set -> P.Mtext ([], "Set")
 452     | A.Sort `Type -> P.Mtext ([], "Type")
 453     | A.Sort `CProp -> P.Mtext ([], "CProp")
 454     | A.Implicit -> P.Mtext([], "?")
 455     | A.Appl [] -> assert false
 456     | A.Appl ((hd::tl) as l) ->
 457         let rec find_symbol idref = function
 458           | A.AttributedTerm (`Loc _, t) -> find_symbol None t
 459           | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
 460           | A.Symbol (name, _) ->
 461               (match idref with
 462               | None -> assert false
 463               | Some idref -> `Symbol (name, idref))
 464           | term ->
 465               `None
 466         in
 467         let aattr = make_attributes [Some "helm","xref"] [xref] in
 468         (match find_symbol None hd with
 469         | `Symbol (name, sxref) ->
 470             let sattr = make_std_attributes (Some sxref) in
 471             (try
 472               (let f = Hashtbl.find symbol_table name in
 473                f tl ~priority ~assoc ~ids_to_uris aattr sattr)
 474             with Not_found ->
 475               P.Mrow(aattr,
 476               m_open_fence :: P.Mi(sattr,name)::(make_args tl) @
 477               [m_close_fence]))
 478         | `None ->
 479             P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
 480             [m_close_fence]))
 481     | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
 482     | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
 483         let attr = make_attributes [Some "helm","xref"] [xref] in
 484         P.Mrow (attr, [
 485           aux ty;
 486           P.Mtext ([], map_tex true "to");
 487           aux body])
 488     | A.Binder (kind,var,body) ->
 489         let attr = make_attributes [Some "helm","xref"] [xref] in
 490         let binder = resolve_binder true kind in
 491         let var = make_capture_variable var in
 492         P.Mrow (attr,
 493            P.Mtext([None,"mathcolor","blue"],binder) :: var @
 494            [P.Mo([],"."); aux body])
 495     | A.LetIn (var,s,body) ->
 496         let attr = make_attributes [Some "helm","xref"] [xref] in
 497         P.Mrow (attr,
 498            P.Mtext([],("let ")) ::
 499            (make_capture_variable var @
 500            P.Mtext([],("="))::
 501            (aux s)::
 502            P.Mtext([]," in ")::
 503            [aux body]))
 504     | A.LetRec (_, defs, body) ->
 505         let attr = make_attributes [Some "helm","xref"] [xref] in
 506         let rec make_defs =
 507           (function
 508                [] -> assert false
 509              | [(var,body,_)] ->
 510                  make_capture_variable var @ [P.Mtext([],"=");(aux body)]
 511              | (var,body,_)::tl ->
 512                  make_capture_variable var @
 513                  (P.Mtext([],"=")::
 514                   (aux body)::P.Mtext([]," and")::(make_defs tl))) in
 515         P.Mrow (attr,
 516           P.Mtext([],("let rec "))::
 517           (make_defs defs)@
 518            (P.Mtext([]," in ")::
 519            [aux body]))
 520     | A.Case (arg,_,outtype,patterns) ->
 521         (* TODO print outtype *)
 522         let attr = make_attributes [Some "helm","xref"] [xref] in
 523         let rec make_patterns =
 524           (function
 525                [] -> []
 526              | [(constr, vars),rhs] -> make_pattern constr vars rhs
 527              | ((constr,vars), rhs)::tl ->
 528                  (make_pattern constr vars rhs)@(P.smallskip::
 529                  P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
 530         and make_pattern constr vars rhs =
 531           let lhs =
 532             P.Mtext([], constr) ::
 533               (List.concat
 534                 (List.map (fun var -> P.smallskip :: make_capture_variable var)
 535                   vars))
 536           in
 537           lhs @
 538           [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs]
 539         in
 540         P.Mrow (attr,
 541           P.Mtext([],"match")::P.smallskip::
 542           (aux arg)::P.smallskip::
 543           P.Mtext([],"with")::P.smallskip::
 544           P.Mtext([],"[")::P.smallskip::
 545           (make_patterns patterns)@(P.smallskip::[P.Mtext([],("]"))]))
 546
 547   and make_capture_variable (name, ty) =
 548     let name =
 549       match name with
 550       | Cic.Anonymous -> [P.Mtext([], "_")]
 551       | Cic.Name s -> [P.Mtext([], s)]
 552     in
 553     let ty =
 554       match ty with
 555       | None -> []
 556       | Some ty -> [P.Mtext([],":"); aux ty]
 557     in
 558     name @ ty
 559
 560   and make_args ?(priority = 0) ?(assoc = false) =
 561     function
 562         [] -> []
 563       | a::tl -> P.smallskip::(aux a)::(make_args tl)
 564
 565   in
 566   aux ast
 567 ;;
 568
 569 let box_prefix = "b";;
 570
 571 let add_xml_declaration stream =
 572   [<
 573     Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 574     Xml.xml_cdata "\n";
 575     Xml.xml_nempty ~prefix:box_prefix "box"
 576       [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
 577         Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ;
 578         Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
 579         Some "xmlns","xlink","http://www.w3.org/1999/xlink"
 580       ] stream
 581   >]
 582
 583 let ast2mpresXml ((ast, ids_to_uris) as arg) =
 584   let astBox = ast2astBox arg in
 585   let smallAst2mpresXml ast =
 586     P.print_mpres (ast2mpres (ast, ids_to_uris))
 587   in
 588   (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)
 589
 590 let b_open_fence = Box.b_text [] "("
 591 let b_close_fence = Box.b_text [] ")"
 592 let b_v_with_fences attrs a b op =
 593   Box.b_h attrs [
 594     b_open_fence;
 595     Box.b_v [] [
 596       a;
 597       Box.b_h [] [ op; b ]
 598     ];
 599     b_close_fence
 600   ]
 601 let b_v_without_fences attrs a b op =
 602   Box.b_v attrs [
 603     a;
 604     Box.b_h [] [ op; b ]
 605   ]
 606
 607 let _ = (** fill symbol_table *)
 608   let binary f = function [a;b] -> f a b | _ -> assert false in
 609   let unary f = function [a] -> f a | _ -> assert false in
 610   let add_binary_op name threshold ?(assoc=`Left) symbol =
 611     let assoc = match assoc with `Left -> true | `Right -> false in
 612     Hashtbl.add symbol_table name (binary
 613       (fun a b ~priority ~assoc ~ids_to_uris aattr sattr ->
 614         let symbol =
 615           match symbol with
 616           | `Symbol name -> map_tex true name
 617           | `Ascii s -> s
 618         in
 619          if (priority > threshold) || (priority = threshold && assoc) then
 620            m_row_with_fences aattr
 621              (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
 622              (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
 623              (P.Mo(sattr,symbol))
 624          else
 625            m_row aattr
 626              (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
 627              (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
 628              (P.Mo(sattr,symbol))));
 629     Hashtbl.add symbol_table_charcount name (binary
 630       (fun a b ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr ->
 631         let symbol =
 632           match symbol with
 633           | `Symbol name -> map_tex unicode name
 634           | `Ascii s -> s
 635         in
 636
 637          if (priority > threshold) || (priority = threshold && assoc) then
 638            b_v_with_fences aattr
 639              (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
 640              (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
 641               (b, ids_to_uris))
 642              (Box.Text(sattr,symbol))
 643          else
 644            b_v_without_fences aattr
 645              (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
 646              (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
 647               (b, ids_to_uris))
 648              (Box.Text(sattr,symbol))))
 649   in
 650   Hashtbl.add symbol_table "not" (unary
 651     (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
 652        (P.Mrow([], [
 653          m_open_fence; P.Mo([],map_tex true "lnot");
 654          ast2mpres (a, ids_to_uris); m_close_fence]))));
 655   Hashtbl.add symbol_table "inv" (unary
 656     (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
 657       P.Msup([],
 658         P.Mrow([],[ m_open_fence; ast2mpres (a, ids_to_uris); m_close_fence]),
 659         P.Mrow([],[ P.Mo([],"-"); P.Mn([],"1")]))));
 660   Hashtbl.add symbol_table "opp" (unary
 661     (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
 662       P.Mrow([],[
 663         P.Mo([],"-");
 664         m_open_fence;
 665         ast2mpres (a, ids_to_uris);
 666         m_close_fence])));
 667   add_binary_op "arrow" 5 ~assoc:`Right (`Symbol "to");
 668   add_binary_op "eq" 40 (`Ascii "=");
 669   add_binary_op "and" 20 (`Symbol "land");
 670   add_binary_op "or" 10 (`Symbol "lor");
 671   add_binary_op "iff" 5 (`Symbol "iff");
 672   add_binary_op "leq" 40 (`Symbol "leq");
 673   add_binary_op "lt" 40 (`Symbol "lt");
 674   add_binary_op "geq" 40 (`Symbol "geq");
 675   add_binary_op "gt" 40 (`Symbol "gt");
 676   add_binary_op "plus" 60 (`Ascii "+");
 677   add_binary_op "times" 70 (`Ascii "*");
 678   add_binary_op "minus" 60 (`Ascii "-");
 679   add_binary_op "div" 60 (`Ascii "/");
 680