(* TODO unicode symbol "to" *)
let mpres_implicit = Mpresentation.Mtext ([], "?")
-let map_tex use_unicode texcmd =
- let default_map_tex = Printf.sprintf "\\%s " in
- if use_unicode then
- try
- Utf8Macro.expand texcmd
- with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd
- else
- default_map_tex texcmd
-
-let resolve_binder use_unicode = function
- | `Lambda -> map_tex use_unicode "lambda"
- | `Pi -> map_tex use_unicode "Pi"
- | `Forall -> map_tex use_unicode "forall"
- | `Exists -> map_tex use_unicode "exists"
+let to_unicode s =
+ try
+ if s.[0] = '\\' then
+ Utf8Macro.expand (String.sub s 1 (String.length s - 1))
+ else s
+ with Utf8Macro.Macro_not_found _ -> s
let rec make_attributes l1 = function
| [] -> []
| Mpresentation.Mobject _ -> false
| _ -> true
-let box_of mathonly kind attrs children =
- if mathonly then Mpresentation.Mrow (attrs, children)
- else
- match kind with
- | CicNotationPt.H when List.for_all genuine_math children ->
- Mpresentation.Mrow (attrs, children)
+let box_of mathonly spec attrs children =
+ match children with
+ | [t] -> t
+ | _ ->
+ let kind, spacing, indent = spec in
+ let rec dress = function
+ | [] -> []
+ | [hd] -> [hd]
+ | hd :: tl -> hd :: Mpresentation.Mtext ([], " ") :: dress tl
+ in
+ if mathonly then Mpresentation.Mrow (attrs, dress children)
+ else
+ let attrs' =
+ if spacing then [None, "spacing", "0.5em"] else []
+ @ if indent then [None, "indent", "0em 0.5em"] else []
+ @ attrs
+ in
+ match kind with
+ | CicNotationPt.H when List.for_all genuine_math children ->
+ Mpresentation.Mrow (attrs', children)
| CicNotationPt.H ->
- mpres_of_box (Box.H (attrs, List.map box_of_mpres children))
+ mpres_of_box (Box.H (attrs', List.map box_of_mpres children))
| CicNotationPt.V ->
- mpres_of_box (Box.V (attrs, List.map box_of_mpres children))
+ mpres_of_box (Box.V (attrs', List.map box_of_mpres children))
| CicNotationPt.HV ->
- mpres_of_box (Box.HV (attrs, List.map box_of_mpres children))
+ mpres_of_box (Box.HV (attrs', List.map box_of_mpres children))
| CicNotationPt.HOV ->
- mpres_of_box (Box.HOV (attrs, List.map box_of_mpres children))
+ mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children))
let open_paren = Mpresentation.Mo ([], "(")
let closed_paren = Mpresentation.Mo ([], ")")
type child_pos = [ `Left | `Right | `Inner ]
+let pp_assoc =
+ function
+ | Gramext.LeftA -> "LeftA"
+ | Gramext.RightA -> "RightA"
+ | Gramext.NonA -> "NonA"
+
+let pp_pos =
+ function
+ | `Left -> "`Left"
+ | `Right -> "`Right"
+ | `Inner -> "`Inner"
+
+let is_atomic t =
+ let module P = Mpresentation in
+ let rec aux_mpres = function
+ | P.Mi _
+ | P.Mo _
+ | P.Mn _
+ | P.Ms _
+ | P.Mtext _
+ | P.Mspace _ -> true
+ | P.Mobject (_, box) -> aux_box box
+ | P.Maction (_, [mpres])
+ | P.Mrow (_, [mpres]) -> aux_mpres mpres
+ | _ -> false
+ and aux_box = function
+ | Box.Space _
+ | Box.Ink _
+ | Box.Text _ -> true
+ | Box.Object (_, mpres) -> aux_mpres mpres
+ | Box.H (_, [box])
+ | Box.V (_, [box])
+ | Box.HV (_, [box])
+ | Box.HOV (_, [box])
+ | Box.Action (_, [box]) -> aux_box box
+ | _ -> false
+ in
+ aux_mpres t
+
let add_parens child_prec child_assoc child_pos curr_prec t =
- if child_prec < curr_prec
+ prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec
+ (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec));
+ if is_atomic t then t
+ else if child_prec < curr_prec
|| (child_prec = curr_prec &&
child_assoc = Gramext.LeftA &&
child_pos <> `Left)
| A.AttributedTerm (`IdRef xref, t) ->
return (invoke mathonly (Some xref) prec assoc t)
- | A.Ident (literal, None) -> return (P.Mi (make_href xref, literal))
- | A.Num (literal, _) -> return (P.Mn (make_href xref, literal))
- | A.Symbol (literal, _) -> return (P.Mo (make_href xref, literal))
- | A.Uri (literal, None) -> return (P.Mi (make_href xref, literal))
+ | A.Ident (literal, _) -> return (P.Mi (make_href xref, to_unicode literal))
+ | A.Num (literal, _) -> return (P.Mn (make_href xref, to_unicode literal))
+ | A.Symbol (literal, _) -> return (P.Mo (make_href xref,to_unicode literal))
+ | A.Uri (literal, _) -> return (P.Mi (make_href xref, to_unicode literal))
(* default pretty printing shant' be implemented here *)
(* | A.Appl terms ->
| A.Magic _
| A.Variable _ -> assert false (* should have been instantiated *)
- | _ -> assert false
+ | t ->
+ prerr_endline (CicNotationPp.pp_term t);
+ assert false
and aux_literal xref prec assoc l =
let return t = t, (prec, assoc) in
let attrs = make_href xref in
match l with
| `Symbol s
- | `Keyword s -> return (P.Mo (attrs, s))
- | `Number s -> return (P.Mn (attrs, s))
+ | `Keyword s -> return (P.Mo (attrs, to_unicode s))
+ | `Number s -> return (P.Mn (attrs, to_unicode s))
and aux_layout mathonly xref prec assoc l =
let return t = t, (prec, assoc) in
let attrs = make_xref xref in
[] -> []
| [t] ->
let t', (child_prec, child_assoc) = aux mathonly xref prec assoc t in
+ prerr_endline ("T " ^ CicNotationPp.pp_term t);
[add_parens child_prec child_assoc `Right prec t']
| t :: tl ->
let t', (child_prec, child_assoc) = aux mathonly xref prec assoc t in
+ prerr_endline ( "T " ^ CicNotationPp.pp_term t);
let child_pos = if first then `Left else `Inner in
- add_parens child_prec child_assoc child_pos prec t' :: aux_list false tl
+ let hd = add_parens child_prec child_assoc child_pos prec t' in
+ hd :: aux_list false tl
in
match terms with
[t] -> [invoke mathonly xref prec assoc t]
in
fst (aux false None 0 Gramext.NonA t)
+let render_to_boxml id_to_uri t =
+ let rec print_box (t: CicNotationPres.boxml_markup) =
+ Box.box2xml print_mpres t
+ and print_mpres (t: CicNotationPres.mathml_markup) =
+ Mpresentation.print_mpres print_box t
+ in
+ let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
+ Ast2pres.add_xml_declaration xml_stream
+
projects / helm.git / blobdiff