X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPres.ml;h=b898f6d1fe238f2eb33618923d0486f901993b2e;hb=b84c60ff48a21a62a08e636f32cf0df46dfbe45a;hp=ebe5bf6ebb000f28e81885e0d9722e6cdc07d906;hpb=256ea270b884864d0eddd1de66bae2a2cbc513ff;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index ebe5bf6eb..b898f6d1f 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -36,20 +36,12 @@ let mpres_arrow = Mpresentation.Mo (binder_attributes, "->") (* 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 | [] -> [] @@ -73,20 +65,34 @@ let genuine_math = | 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 ([], ")") @@ -95,8 +101,50 @@ let closed_box_paren = Box.Text ([], ")") 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) @@ -146,10 +194,10 @@ let render ids_to_uris t = | 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 -> @@ -170,15 +218,17 @@ let render ids_to_uris t = | 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 @@ -203,11 +253,14 @@ let render ids_to_uris t = [] -> [] | [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] @@ -215,3 +268,12 @@ let render ids_to_uris 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 +