(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(**************************************************************************)
(*                                                                        *)
(*                           PROJECT HELM                                 *)
(*                                                                        *)
(*                Andrea Asperti <asperti@cs.unibo.it>                    *)
(*                             28/6/2003                                  *)
(*                                                                        *)
(**************************************************************************)

module A = CicAst;;
module P = Mpresentation;;

let symbol_table = Hashtbl.create 503;;
let symbol_table_charcount = Hashtbl.create 503;;

let maxsize = 25;;

let rec countvar current_size = function
    (Cic.Anonymous, None) -> current_size + 1 (* underscore *)
  | (Cic.Anonymous, Some ty) -> countterm current_size ty
  | (Cic.Name s, None) -> current_size + String.length s
  | (Cic.Name s, Some ty) -> current_size + countterm current_size ty

and countterm current_size t =
  if current_size > maxsize then current_size 
  else match t with
      A.AttributedTerm (_,t) -> countterm current_size t
    | A.Appl l -> 
        List.fold_left countterm current_size l
    | A.Binder (_,var,body) -> 
        let varsize = countvar current_size var in
        countterm (varsize + 1) body (* binder *)
    | A.Case (arg, _, ty, pl) ->
        let size1 = countterm (current_size+10) arg in (* match with *)
        let size2 =
          match ty with
              None -> size1
            | Some ty -> countterm size1 ty in
        List.fold_left 
          (fun c ((constr,vars),action) ->
             let size3 =
               List.fold_left countvar (c+String.length constr) vars in
             countterm size3 action) size2 pl 
    | A.LetIn (var,s,t) ->
        let size1 = countvar current_size var in
        let size2 = countterm size1 s in
        countterm size2 t
    | A.LetRec (_,l,t) ->
        let size1 =
          List.fold_left
            (fun c (var,s,_) -> 
               let size1 = countvar c var in
               countterm size1 s) current_size l in
          countterm size1 t
    | A.Ident (s,None)
    | A.Uri (s, None) -> current_size + (String.length s)
    | A.Ident (s,Some l)
    | A.Uri (s,Some l) ->
        List.fold_left 
          (fun c (v,t) -> countterm (c + (String.length v)) t) 
          (current_size + (String.length s)) l
    | A.Implicit -> current_size + 1 (* underscore *)
    | A.Meta (_,l) ->
        List.fold_left 
          (fun c t -> 
             match t with
                 None -> c + 1 (* underscore *)
               | Some t -> countterm c t)
          (current_size + 1) l (* num *)
    | A.Num (s, _) -> current_size + String.length s
    | A.Sort _ -> current_size + 4 (* sort name *)
    | A.Symbol (s,_) -> current_size + String.length s

    | A.UserInput -> current_size
;;

let is_big t = 
  ((countterm 0 t) > maxsize)
;;

let rec make_attributes l1 =
  function
      [] -> []
    | None::tl -> make_attributes (List.tl l1) tl
    | (Some s)::tl ->
       let p,n = List.hd l1 in
        (p,n,s)::(make_attributes (List.tl l1) tl)
;;

let map_tex unicode texcmd =
  let default_map_tex = Printf.sprintf "\\%s " in
  if unicode then
    try
      Utf8Macro.expand texcmd
    with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd
  else
    default_map_tex texcmd

let resolve_binder unicode = function
  | `Lambda -> map_tex unicode "lambda"
  | `Pi -> map_tex unicode "Pi"
  | `Forall -> map_tex unicode "forall"
  | `Exists -> map_tex unicode "exists"
;;

let rec make_args f ~tail = function
    | [] -> assert false
    | [arg] -> [f ~tail arg]
    | arg :: tl -> (f ~tail:[] arg) :: (make_args f ~tail tl)

let append_tail ~tail box =
  match tail with
  | [] -> box
  | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))

let rec find_symbol idref = function
  | A.AttributedTerm (`Loc _, t) -> find_symbol None t
  | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
  | A.Symbol (name, _) -> `Symbol (name, idref)
  | _ -> `None

let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
  (t, ids_to_uris)
=
  let lookup_uri = function
    | None -> None
    | Some id ->
        (try
          Some (Hashtbl.find ids_to_uris id)
        with Not_found -> None)
  in
  let make_std_attributes xref =
    let uri = lookup_uri xref in
    make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
  in
  let rec ast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
    if is_big t then 
      bigast2box ~priority ~assoc ?xref ~tail t
    else
      let attrs = make_std_attributes xref in
      append_tail ~tail (Box.Object (attrs, t))
  and
  bigast2box ?(priority = 0) ?(assoc = false) ?xref ~tail t =
  match t with
    | A.AttributedTerm (`Loc _, t) -> bigast2box ?xref ~tail t
    | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
    | A.Appl [] -> assert false
    | A.Appl ((hd::tl) as l) ->
        let aattr = make_attributes [Some "helm","xref"] [xref] in
        (match find_symbol None hd with
        | `Symbol (name, sxref) ->
            let sattr = make_std_attributes sxref in
            (try 
              (let f = Hashtbl.find symbol_table_charcount name in
               f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
            with Not_found ->
              Box.H 
                (make_attributes [Some "helm","xref"] [xref],
                 [Box.Text([],"(");
                  Box.V([],
                    make_args (fun ~tail t -> ast2box ~tail t)
                      ~tail:(")" :: tail) l);
                  Box.Text([],")")]))
        | `None ->
            Box.H 
              (make_attributes [Some "helm","xref"] [xref],
               [Box.Text([],"(");
                Box.V([],
                  make_args
                    (fun ~tail t -> ast2box ~tail t)
                    ~tail:(")" :: tail) l)]
                ))
    | A.Binder (`Forall, (Cic.Anonymous, typ), body)
    | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
        Box.V(make_attributes [Some "helm","xref"] [xref],
          [(match typ with
            | None -> Box.Text([], "?")
            | Some typ -> ast2box ~tail:[] typ);
            Box.H([],
              [Box.skip;
               Box.Text([], map_tex unicode "to");
               ast2box ~tail body])])
    | A.Binder(kind, var, body) ->
        Box.V(make_attributes [Some "helm","xref"] [xref],
              [Box.H([],
                [Box.Text ([None,"color","blue"], resolve_binder unicode kind);
                 make_var ~tail:("." :: tail) var]);
               Box.indent (ast2box ~tail body)])
    | A.Case(arg, _, ty, pl) ->
        let make_rule ~tail sep ((constr,vars),rhs) =
          if (is_big rhs) then
            Box.V([],[Box.H([],[Box.Text([],sep);
                                Box.smallskip; 
                                make_pattern constr vars;
                                Box.smallskip; 
                                Box.Text([],map_tex unicode "Rightarrow")]);
                      Box.indent (bigast2box ~tail rhs)])
          else
            Box.H([],[Box.Text([],sep);
                      Box.smallskip; 
                      make_pattern constr vars;
                      Box.smallskip; 
                      Box.Text([],map_tex unicode "Rightarrow");
                      Box.smallskip; 
                      append_tail ~tail (Box.Object([],rhs))]) in
        let plbox =
          match pl with
            [] -> append_tail ~tail (Box.Text([],"[]"))
          | r::tl -> 
              Box.V([],
                (make_rule ~tail:[] "[" r) ::
                (make_args
                  (fun ~tail pat -> make_rule ~tail "|" pat)
                  ~tail:("]" :: tail)
                  tl))
        in
        let ty_box =
          match ty with
          | Some ty ->
              [ Box.H([],[Box.Text([],"[");
                         ast2box ~tail:[] ty;
                         Box.Text([],"]")]) ]
          | None -> []
        in
        if is_big arg then
          Box.V(make_attributes [Some "helm","xref"] [xref],
                 ty_box @
                 [Box.Text([],"match");
                 Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg]));
                 Box.Text([],"with");
                 Box.indent plbox])
        else
          Box.V(make_attributes [Some "helm","xref"] [xref],
                ty_box @
                [Box.H(make_attributes [Some "helm","xref"] [xref],
                       [Box.Text([],"match");
                        Box.smallskip;
                        ast2box ~tail:[] arg;
                        Box.smallskip;
                        Box.Text([],"with")]);
                 Box.indent plbox])
    | A.LetIn (var, s, t) ->
        Box.V(make_attributes [Some "helm","xref"] [xref],
              (make_def "let" var s "in")@[ast2box ~tail t])
    | A.LetRec (_, vars, body) ->
        let definitions =
          let rec make_defs let_txt = function
              [] -> []
            | [(var,s,_)] -> make_def let_txt var s "in"
            | (var,s,_)::tl ->
                (make_def let_txt var s "")@(make_defs "and" tl) in
          make_defs "let rec" vars in
        Box.V(make_attributes [Some "helm","xref"] [xref],
              definitions@[ast2box ~tail body])
    | A.Ident (s, subst)
    | A.Uri (s, subst) ->
        let subst =
          let rec make_substs start_txt = 
            function
              [] -> []
            | [(s,t)] -> 
                make_subst start_txt s t ""
            | (s,t)::tl ->
                (make_subst start_txt s t ";")@(make_substs "" tl)
          in
          match subst with
          | Some subst ->
	      Box.H([],
	            [Box.Text(make_std_attributes xref,s);
		     Box.Action([],
		       [Box.Text([],"[...]");
		        Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
	                 Box.V([], make_substs "" subst);
		         Box.Text([], "]")])])])
          | None -> Box.Text(make_std_attributes xref, s)
        in
	 subst
	(*
        Box.H([], (* attr here or on Vbox? *)
              [Box.Text(make_std_attributes xref,s);
	       Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
               (* Box.indent(Box.V([],subst))]) *)
	*)
    | A.Implicit -> 
        Box.Text([],"_") (* big? *)
    | A.Meta (n, l) ->
        let local_context =
          List.map 
            (function t -> 
               Box.H([],[aux_option ~tail t; Box.Text([],";")])) 
            l in
        Box.V(make_attributes [Some "helm","xref"] [xref],
              [Box.Text([],"?"^(string_of_int n));
               Box.H([],[Box.Text([],"[");
                         Box.V([],local_context);
                         Box.Text([],"]")])])
    | A.Num (s, _) -> 
         Box.Text([],s)
    | A.Sort kind ->
        (match kind with 
             `Prop -> Box.Text([],"Prop")
           | `Set -> Box.Text([],"Set")
           | `Type -> Box.Text([],"Type")   
           | `CProp -> Box.Text([],"CProp"))    
    | A.Symbol (s, _) -> 
        Box.Text([],s)

    | A.UserInput -> Box.Text([],"")

  and aux_option ~tail = function
      None  -> Box.Text([],"_")
    | Some ast -> ast2box ~tail ast 

  and make_var ~tail = function
      (Cic.Anonymous, None) -> Box.Text([],"_:_")
    | (Cic.Anonymous, Some t) -> 
        Box.H([],[Box.Text([],"_:");ast2box ~tail t])
    | (Cic.Name s, None) -> Box.Text([],s)
    | (Cic.Name s, Some t) ->
        if is_big t then
          Box.V([],[Box.Text([],s^":");
                    Box.indent(bigast2box ~tail t)])
        else
          Box.H([],[Box.Text([],s^":");Box.Object([],t)])

  and make_pattern constr = 
    function
        [] -> Box.Text([],constr)
      | vars -> 
          let bvars =
            List.fold_right 
              (fun var acc -> 
                 let bv = 
                   match var with
                       (* ignoring the type *)
                       (Cic.Anonymous, _) -> Box.Text([],"_")
                     | (Cic.Name s, _) -> Box.Text([],s) in
                   Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
            Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
      

  and make_def let_txt var def end_txt =
    let name = 
      (match var with
           (* ignoring the type *)
           (Cic.Anonymous, _) -> Box.Text([],"_") 
         | (Cic.Name s, _) -> Box.Text([],s)) in
    pretty_append ~tail:[end_txt]
      [Box.Text([],let_txt);
       Box.smallskip;
       name;
       Box.smallskip;
       Box.Text([],"=")
      ]
      def 

  and make_subst start_txt varname body end_txt =
    pretty_append ~tail:[end_txt]
      ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
       [Box.Text([],varname);
        Box.smallskip;
        Box.Text([],map_tex unicode "Assign")
       ])
      body
            
  and pretty_append ~tail l ast =
    if is_big ast then
      [Box.H([],l);
       Box.H([],[Box.skip; bigast2box ~tail ast])]
    else
      [Box.H([],l@[Box.smallskip; (ast2box ~tail ast)])]

in
ast2box ~priority ~assoc ~tail t
;;

let m_row_with_fences = P.row_with_brackets
let m_row = P.row_without_brackets
let m_open_fence = P.Mo([None, "stretchy", "false"], "(")
let m_close_fence = P.Mo([None, "stretchy", "false"], ")")

let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
  let lookup_uri = function
    | None -> None
    | Some id ->
        (try
          Some (Hashtbl.find ids_to_uris id)
        with Not_found -> None)
  in
  let make_std_attributes xref =
    let uri = lookup_uri xref in
    make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri]
  in
  let rec aux ?xref =
  function
    | A.AttributedTerm (`Loc _, ast) -> aux ?xref ast
    | A.AttributedTerm (`IdRef xref, ast) -> aux ~xref ast
    | A.Symbol (name,_) -> 
        let attr = make_std_attributes xref in
        P.Mi (attr,name)
    | A.Ident (name,subst)
    | A.Uri (name,subst) ->
        let attr = make_std_attributes xref in
        let rec make_subst =
          (function 
              [] -> []
            | (n,a)::tl ->
                (aux a)::
                P.Mtext([],"/")::
                P.Mi([],n)::
                P.Mtext([],"; ")::
                P.smallskip::
                (make_subst tl)) in
        let subst =
          match subst with
          | None -> []
          | Some subst -> make_subst subst
        in
        (match subst with
        | [] -> P.Mi (attr, name)
        | _ ->
            P.Mrow ([],
              P.Mi (attr,name)::
              P.Mtext([],"[")::
              subst @
              [(P.Mtext([],"]"))]))
    | A.Meta (no,l) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let l' =
         List.map
          (function
              None -> P.Mo([],"_")
            | Some t -> aux t
          ) l
        in
         P.Mrow ([],P.Mi (attr,"?" ^ string_of_int no) :: P.Mo ([],"[") ::
           l' @ [P.Mo ([],"]")])
    | A.Num (value, _) -> 
        let attr = make_attributes [Some "helm","xref"] [xref] in
        P.Mn (attr,value)
    | A.Sort `Prop -> P.Mtext ([], "Prop")
    | A.Sort `Set -> P.Mtext ([], "Set")
    | A.Sort `Type -> P.Mtext ([], "Type")
    | A.Sort `CProp -> P.Mtext ([], "CProp")
    | A.Implicit -> P.Mtext([], "?")
    | A.UserInput -> P.Mtext([], "")
    | A.Appl [] -> assert false
    | A.Appl ((hd::tl) as l) ->
        let aattr = make_attributes [Some "helm","xref"] [xref] in
        (match find_symbol None hd with
        | `Symbol (name, sxref) ->
            let sattr = make_std_attributes sxref in
            (try 
              (let f = Hashtbl.find symbol_table name in
               f tl ~priority ~assoc ~ids_to_uris aattr sattr)
            with Not_found ->
              P.Mrow(aattr,
              m_open_fence :: P.Mi(sattr,name)::(make_args tl) @
              [m_close_fence]))
        | `None ->
            P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
            [m_close_fence]))
    | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
    | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        P.Mrow (attr, [
          aux ty;
          P.Mtext ([], map_tex true "to");
          aux body])
    | A.Binder (kind,var,body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let binder = resolve_binder true kind in
        let var = make_capture_variable var in
        P.Mrow (attr, 
           P.Mtext([None,"mathcolor","blue"],binder) :: var @ 
           [P.Mo([],"."); aux body])
    | A.LetIn (var,s,body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        P.Mrow (attr, 
           P.Mtext([],("let ")) ::
           (make_capture_variable var @
           P.Mtext([],("="))::
           (aux s)::
           P.Mtext([]," in ")::
           [aux body]))
    | A.LetRec (_, defs, body) ->
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let rec make_defs =
          (function 
               [] -> assert false
             | [(var,body,_)] -> 
                 make_capture_variable var @ [P.Mtext([],"=");(aux body)]
             | (var,body,_)::tl -> 
                 make_capture_variable var @
                 (P.Mtext([],"=")::
                  (aux body)::P.Mtext([]," and")::(make_defs tl))) in
        P.Mrow (attr,  
          P.Mtext([],("let rec "))::
          (make_defs defs)@
           (P.Mtext([]," in ")::
           [aux body]))
    | A.Case (arg,_,outtype,patterns) ->
        (* TODO print outtype *)
        let attr = make_attributes [Some "helm","xref"] [xref] in
        let rec make_patterns =
          (function 
               [] -> []
             | [(constr, vars),rhs] -> make_pattern constr vars rhs
             | ((constr,vars), rhs)::tl -> 
                 (make_pattern constr vars rhs)@(P.smallskip::
                 P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
        and make_pattern constr vars rhs =           
          let lhs = 
            P.Mtext([], constr) ::
              (List.concat
                (List.map
                  (fun var -> P.smallskip :: make_capture_variable var)
                  vars))
          in
          lhs @
          [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs]
        in
        P.Mrow (attr,
          P.Mtext([],"match")::P.smallskip::
          (aux arg)::P.smallskip::
          P.Mtext([],"with")::P.smallskip::
          P.Mtext([],"[")::P.smallskip::
          (make_patterns patterns)@(P.smallskip::[P.Mtext([],("]"))]))

  and make_capture_variable (name, ty) =
    let name =
      match name with
      | Cic.Anonymous -> [P.Mtext([], "_")]
      | Cic.Name s -> [P.Mtext([], s)]
    in
    let ty =
      match ty with
      | None -> []
      | Some ty -> [P.Mtext([],":"); aux ty]
    in
    name @ ty

  and make_args ?(priority = 0) ?(assoc = false) =
    function
        [] -> []
      | a::tl -> P.smallskip::(aux a)::(make_args tl)

  in
  aux ast
;;

let box_prefix = "b";;

let add_xml_declaration stream =
  [<
    Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
    Xml.xml_cdata "\n";
    Xml.xml_nempty ~prefix:box_prefix "box"
      [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
        Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ;
        Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
        Some "xmlns","xlink","http://www.w3.org/1999/xlink"
      ] stream
  >]

let ast2mpresXml ((ast, ids_to_uris) as arg) =
  let astBox = ast2astBox arg in
  let smallAst2mpresXml ast =
    P.print_mpres (ast2mpres (ast, ids_to_uris))
  in
  (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)

let b_open_fence = Box.b_text [] "("
let b_close_fence = Box.b_text [] ")"
let b_v_with_fences attrs a b op =
  Box.b_h attrs [
    b_open_fence;
    Box.b_v [] [
      a;
      Box.b_h [] [ op; b ]
    ];
    b_close_fence
  ]
let b_v_without_fences attrs a b op =
  Box.b_v attrs [
    a;
    Box.b_h [] [ op; b ]
  ]

let _ = (** fill symbol_table *)
  let binary f = function [a;b] -> f a b | _ -> assert false in
  let unary f = function [a] -> f a | _ -> assert false in
  let add_binary_op name threshold ?(assoc=`Left) symbol =
    let assoc = match assoc with `Left -> true | `Right -> false in
    Hashtbl.add symbol_table name (binary
      (fun a b ~priority ~assoc ~ids_to_uris aattr sattr ->
        let symbol =
          match symbol with
          | `Symbol name -> map_tex true name
          | `Ascii s -> s
        in
         if (priority > threshold) || (priority = threshold && assoc) then
           m_row_with_fences aattr
             (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
             (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
             (P.Mo(sattr,symbol))
         else 
           m_row aattr
             (ast2mpres ~priority:threshold ~assoc (a, ids_to_uris))
             (ast2mpres ~priority:threshold ~assoc:(not assoc) (b, ids_to_uris))
             (P.Mo(sattr,symbol))));
    Hashtbl.add symbol_table_charcount name (binary
      (fun a b ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr ->
        let symbol =
          match symbol with
          | `Symbol name -> map_tex unicode name
          | `Ascii s -> s
        in

         if (priority > threshold) || (priority = threshold && assoc) then
           b_v_with_fences aattr
             (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
             (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
              (b, ids_to_uris))
             (Box.Text(sattr,symbol))
         else 
           b_v_without_fences aattr
             (ast2astBox ~priority:threshold ~assoc ~tail:[] (a, ids_to_uris))
             (ast2astBox ~priority:threshold ~assoc:(not assoc) ~tail
              (b, ids_to_uris))
             (Box.Text(sattr,symbol))))
  in
  Hashtbl.add symbol_table "not" (unary
    (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
       (P.Mrow([], [
         m_open_fence; P.Mo([],map_tex true "lnot");
         ast2mpres (a, ids_to_uris); m_close_fence]))));
  Hashtbl.add symbol_table "inv" (unary
    (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
      P.Msup([],
        P.Mrow([],[ m_open_fence; ast2mpres (a, ids_to_uris); m_close_fence]),
        P.Mrow([],[ P.Mo([],"-"); P.Mn([],"1")]))));
  Hashtbl.add symbol_table "opp" (unary
    (fun a ~priority ~assoc ~ids_to_uris attr sattr ->
      P.Mrow([],[
        P.Mo([],"-");
        m_open_fence;
        ast2mpres (a, ids_to_uris);
        m_close_fence])));
  add_binary_op "arrow" 5 ~assoc:`Right (`Symbol "to");
  add_binary_op "eq" 40 (`Ascii "=");
  add_binary_op "and" 20 (`Symbol "land");
  add_binary_op "or" 10 (`Symbol "lor");
  add_binary_op "iff" 5 (`Symbol "iff");
  add_binary_op "leq" 40 (`Symbol "leq");
  add_binary_op "lt" 40 (`Symbol "lt");
  add_binary_op "geq" 40 (`Symbol "geq");
  add_binary_op "gt" 40 (`Symbol "gt");
  add_binary_op "plus" 60 (`Ascii "+");
  add_binary_op "times" 70 (`Ascii "*");
  add_binary_op "minus" 60 (`Ascii "-");
  add_binary_op "div" 60 (`Ascii "/");
  add_binary_op "cast" 80 (`Ascii ":");