(**************************************************************************)
module A = CicAst;;
+module P = Mpresentation;;
let symbol_table = Hashtbl.create 503;;
let symbol_table_charcount = Hashtbl.create 503;;
(fun c (var,s,_) ->
let size1 = countvar c var in
countterm size1 s) current_size l in
- countterm size1 t
- | A.Ident(s,None) -> current_size + (String.length s)
- | A.Ident(s,Some 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(map_attributes attr,
- [Box.H([],[(match typ with
- | None -> Box.Text([], "?")
- | Some typ -> ast2box typ);
- Box.smallskip;
- Box.Text([], "\\to")]);
- Box.indent(ast2box 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
+ 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 ty;
+ ast2box ~tail:[] ty;
Box.Text([],"]")]) ]
| None -> []
in
- if is_big arg then
- Box.V(map_attributes attr,
+ if is_big arg then
+ Box.V(make_attributes [Some "helm","xref"] [xref],
ty_box @
[Box.Text([],"match");
- Box.H([],[Box.skip;
- bigast2box arg;
- Box.smallskip;
- Box.Text([],"with")]);
- plbox])
- else
- Box.V(map_attributes attr,
+ 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(map_attributes attr,
- [Box.Text([],"match");
- Box.smallskip;
- ast2box arg;
- Box.smallskip;
- Box.Text([],"with")]);
- plbox])
+ [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)
+ 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 -> make_substs "[" subst
- | None -> []
+ | 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
- Box.V([], (* attr here or on Vbox? *)
- [Box.Text(map_attributes attr,s);
- Box.indent(Box.V([],subst))])
+ 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 =
- prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
- 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 "<?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 ":");
projects / helm.git / blobdiff