X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=c82f0fb8add1cfa8366d68a4b2740b89f8e25171;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=934223e5ce276644c3875d145d83a5d339fa279e;hpb=ac0a12080b434bf0daafc08e9da240eb57f47280;p=helm.git diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index 934223e5c..c82f0fb8a 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -28,12 +28,12 @@ (* PROJECT HELM *) (* *) (* Andrea Asperti *) -(* 28/6/2003 *) +(* 28/6/2003 *) (* *) (**************************************************************************) -module P = Mpresentation;; module A = CicAst;; +module P = Mpresentation;; let symbol_table = Hashtbl.create 503;; let symbol_table_charcount = Hashtbl.create 503;; @@ -76,227 +76,614 @@ and countterm current_size t = (fun c (var,s,_) -> let size1 = countvar c var in countterm size1 s) current_size l in - countterm size1 t - | A.Ident(s,l) -> + 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) + (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 -> + List.fold_left + (fun c t -> match t with - None -> c + 1 (* underscore *) - | Some t -> countterm c t) + 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 map_attribute = +let rec make_attributes l1 = function - `Loc (n,m) -> - (Some "helm","loc",(string_of_int n)^" "^(string_of_int m)) - | `IdRef s -> - (Some "helm","xref",s) + [] -> [] + | 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_attributes = List.map map_attribute +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 resolve_binder = function - `Lambda -> Box.Text([],"\\lambda") - | `Pi -> Box.Text([],"\\Pi") - | `Exists -> Box.Text([],"\\exists") - | `Forall -> Box.Text([],"\\forall") - -let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t = - if is_big t then - bigast2box ~priority ~assoc ~attr t - else Box.Object (map_attributes attr, t) -and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = - function - A.AttributedTerm (attr1, t) -> - (* attr should be empty, since AtrtributedTerm are not - supposed to be directly nested *) - bigast2box ~priority ~assoc ~attr:(attr1::~attr) t - | A.Appl l -> - Box.H - (map_attributes attr, - [Box.Text([],"("); - Box.V([],List.map ast2box l); - Box.Text([],")")]) + +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(map_attributes attr, - [Box.H([],[resolve_binder kind; - Box.smallskip; - make_var var; - Box.Text([],".")]); - Box.indent (ast2box 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 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([],"->")]); - Box.indent (bigast2box rhs)]) - else - Box.H([],[Box.Text([],sep); - Box.smallskip; - make_pattern constr vars; - Box.smallskip; - Box.Text([],"->"); - Box.smallskip; - Box.Object([],rhs)]) in - let plbox = match pl with - [] -> Box.Text([],"[]") - | r::tl -> - Box.H([], - [Box.V([], - (make_rule "[" r)::(List.map (make_rule "|") tl)); - Box.Text([],"]")]) in - if is_big arg then - Box.V(map_attributes attr, - [Box.Text([],"match"); - Box.H([],[Box.skip; - bigast2box arg; - Box.smallskip; - Box.Text([],"with")]); - plbox]) - else - Box.V(map_attributes attr, - [Box.H(map_attributes attr, - [Box.Text([],"match"); - Box.smallskip; - ast2box arg; - Box.smallskip; - Box.Text([],"with")]); - plbox]) + 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(map_attributes attr, - (make_def "let" var s "in")@[ast2box 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(map_attributes attr, - definitions@[ast2box body]) - | A.Ident (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 - make_substs "[" subst in - Box.V([], (* attr here or on Vbox? *) - [Box.Text(map_attributes attr,s); - Box.indent(Box.V([],subst))]) + 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? *) + Box.Text([],"_") (* big? *) | A.Meta (n, l) -> - let local_context = - List.map - (function t -> - Box.H([],[aux_option t; Box.Text([],";")])) - l in - Box.V(map_attributes attr, - [Box.Text([],"?"^(string_of_int n)); - Box.H([],[Box.Text([],"["); - Box.V([],local_context); - Box.Text([],"]")])]) + 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) + 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")) + (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) - -and aux_option = function - None -> Box.Text([],"_") - | Some ast -> ast2box ast - -and make_var = function - (Cic.Anonymous, None) -> Box.Text([],"_:_") - | (Cic.Anonymous, Some t) -> - Box.H([],[Box.Text([],"_:");ast2box 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 t)]) - else - Box.H([],[Box.Text([],s^":");Box.Object([],t)]) - -and make_pattern constr = + 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 - [] -> 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 - [Box.Text([],let_txt); - Box.smallskip; - name; - Box.smallskip; - Box.Text([],"=") - ] - def - [Box.smallskip;Box.Text([],end_txt)] - -and make_subst start_txt varname body end_txt = - pretty_append - [Box.Text([],start_txt); - Box.Text([],varname); - Box.smallskip; - Box.Text([],":=") - ] - body - [Box.Text([],end_txt)] - -and pretty_append l ast tail = - if is_big ast then - [Box.H([],l); - Box.H([],Box.skip::(bigast2box ast)::tail)] - else - [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))] + | 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 "\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 ":");