+++ /dev/null
-(* 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.Cast (bo,ty) ->
- countterm (countterm (current_size + 3) bo) ty
- | 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] -> (make_rule ~tail:("]" :: tail) "[" r)
- | 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.Cast (bo,ty) ->
- Box.V(make_attributes [Some "helm","xref"] [xref],
- [Box.H([],[Box.Text([],"("); ast2box ~tail:[] bo]);
- Box.H([],[Box.Text([],":"); ast2box ~tail ty;Box.Text([],")")])])
- | 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.smallskip::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.Cast (bo,ty) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- P.Mrow (attr,
- [m_open_fence; aux bo; P.Mo ([],":"); aux ty; 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\" ?>\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 (fun _ -> assert false) (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 ":");
-
projects / helm.git / blobdiff