X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=35f128a05b524078b117a394cb51b87a8554f6d1;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=297a52bc5d7c09050af98740aba7cb0a51ae94ce;hpb=d7e217ef4d310903c23dd56a5943208edfeb9f20;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 297a52bc5..35f128a05 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -135,9 +135,12 @@ let box_of mathonly spec attrs children = let open_paren = Mpresentation.Mo ([], "(") let closed_paren = Mpresentation.Mo ([], ")") +let open_bracket = Mpresentation.Mo ([], "[") +let closed_bracket = Mpresentation.Mo ([], "]") let open_brace = Mpresentation.Mo ([], "{") let closed_brace = Mpresentation.Mo ([], "}") let hidden_substs = Mpresentation.Mtext ([], "{...}") +let hidden_lctxt = Mpresentation.Mtext ([], "[...]") let open_box_paren = Box.Text ([], "(") let closed_box_paren = Box.Text ([], ")") let semicolon = Mpresentation.Mo ([], ";") @@ -178,40 +181,36 @@ let is_atomic t = in aux_mpres t -let add_parens child_prec child_assoc child_pos curr_prec t = -(* eprintf - ("add_parens: " ^^ - "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!") - child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos) - curr_prec; *) - if is_atomic t then t - else if child_prec >= 0 - && (child_prec < curr_prec - || (child_prec = curr_prec && - child_assoc = Gramext.LeftA && - child_pos <> `Left) - || (child_prec = curr_prec && - child_assoc = Gramext.RightA && - child_pos <> `Right)) - then begin (* parens should be added *) -(* prerr_endline "adding parens!"; *) +let add_parens child_prec curr_prec t = + if is_atomic t then + ((*prerr_endline ("NOT adding parens around ATOMIC: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*)t) + else if child_prec >= 0 && child_prec < curr_prec then + begin + (*prerr_endline ("adding parens around: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*) match t with | Mpresentation.Mobject (_, box) -> mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ])) | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren]) end else - t + ((*prerr_endline ("NOT adding parens around: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*)t) -let render ids_to_uris ?(prec=(-1)) = +let lookup_uri ids_to_uris id = + try + let uri = Hashtbl.find ids_to_uris id in + Some (UriManager.string_of_uri uri) + with Not_found -> None +;; + +let render ~lookup_uri ?(prec=(-1)) = let module A = Ast in let module P = Mpresentation in (* let use_unicode = true in *) - let lookup_uri id = - (try - let uri = Hashtbl.find ids_to_uris id in - Some (UriManager.string_of_uri uri) - with Not_found -> None) - in let make_href xmlattrs xref = let xref_uris = List.fold_right @@ -254,10 +253,10 @@ let render ids_to_uris ?(prec=(-1)) = in (* when mathonly is true no boxes should be generated, only mrows *) (* "xref" is *) - let rec aux xmlattrs mathonly xref pos prec t = + let rec aux xmlattrs mathonly xref prec t = match t with | A.AttributedTerm _ -> - aux_attributes xmlattrs mathonly xref pos prec t + aux_attributes xmlattrs mathonly xref prec t | A.Num (literal, _) -> let attrs = (RenderingAttrs.number_attributes `MathML) @@ -290,62 +289,87 @@ let render ids_to_uris ?(prec=(-1)) = box_of mathonly (A.H, false, false) [] [ Mpres.Mi ([], name); Mpres.Mo ([], to_unicode "\\def"); - aux [] mathonly xref pos prec t ]) + aux [] mathonly xref prec t ]) substs)) @ [ closed_brace ]) in let substs_maction = toggle_action [ hidden_substs; substs' ] in box_of mathonly (A.H, false, false) [] [ name; substs_maction ]) + | A.Meta(n, l) -> + let local_context l = + box_of mathonly (A.H, false, false) [] + ([ Mpres.Mtext ([], "[") ] @ + (CicNotationUtil.dress (Mpres.Mtext ([], ";")) + (List.map + (function + | None -> Mpres.Mtext ([], "_") + | Some t -> aux xmlattrs mathonly xref prec t) l)) @ + [ Mpres.Mtext ([], "]")]) + in + let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in + box_of mathonly (A.H, false, false) [] + ([Mpres.Mtext ([], "?"^string_of_int n) ] + @ (if l <> [] then [lctxt_maction] else [])) | A.Literal l -> aux_literal xmlattrs xref prec l | A.UserInput -> Mpres.Mtext ([], "%") - | A.Layout l -> aux_layout mathonly xref pos prec l + | A.Layout l -> aux_layout mathonly xref prec l | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t); assert false - and aux_attributes xmlattrs mathonly xref pos prec t = + and aux_attributes xmlattrs mathonly xref prec t = let reset = ref false in - let new_level = ref None in + let inferred_level = ref None in + let expected_level = ref None in let new_xref = ref [] in let new_xmlattrs = ref [] in - let new_pos = ref pos in -(* let reinit = ref false in *) let rec aux_attribute = function | A.AttributedTerm (attr, t) -> (match attr with | `Loc _ | `Raw _ -> () - | `Level (-1, _) -> reset := true - | `Level (child_prec, child_assoc) -> - new_level := Some (child_prec, child_assoc) + | `Level (-1) -> reset := true + | `Level child_prec -> +(* assert (!expected_level = None); *) + expected_level := !inferred_level; + inferred_level := Some child_prec | `IdRef xref -> new_xref := xref :: !new_xref - | `ChildPos pos -> new_pos := pos | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs); aux_attribute t | t -> - (match !new_level with - | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t - | Some (child_prec, child_assoc) -> - let t' = - aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in + let prec = + match !expected_level with + | None -> prec + | Some prec -> prec + in + (match !inferred_level with + | None -> aux !new_xmlattrs mathonly new_xref prec t + | Some child_prec -> + let t' = aux !new_xmlattrs mathonly new_xref child_prec t in + (*prerr_endline + ("inferred: "^string_of_int child_prec^ + " exp: "^string_of_int prec ^ + " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false + (function x::_->x|_->assert false) 80 t');*) if !reset - then t' - else add_parens child_prec child_assoc !new_pos prec t') + then ((*prerr_endline "reset";*)t') + else add_parens child_prec prec t') in +(* prerr_endline (CicNotationPp.pp_term t); *) aux_attribute t and aux_literal xmlattrs xref prec l = let attrs = make_href xmlattrs xref in (match l with | `Symbol s -> Mpres.Mo (attrs, to_unicode s) - | `Keyword s -> Mpres.Mo (attrs, to_unicode s) + | `Keyword s -> Mpres.Mtext (attrs, to_unicode s) | `Number s -> Mpres.Mn (attrs, to_unicode s)) - and aux_layout mathonly xref pos prec l = + and aux_layout mathonly xref prec l = let attrs = make_xref xref in - let invoke' t = aux [] true (ref []) pos prec t in + let invoke' t = aux [] true (ref []) prec t in (* use the one below to reset precedence and associativity *) - let invoke_reinit t = aux [] mathonly xref `Inner ~-1 t in + let invoke_reinit t = aux [] mathonly xref ~-1 t in match l with | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2) | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2) @@ -357,23 +381,47 @@ let render ids_to_uris ?(prec=(-1)) = | A.Atop (t1, t2) -> Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1, invoke_reinit t2) + | A.InfRule (t1, t2, t3) -> + Mpres.Mstyle ([None,"mathsize","big"], + Mpres.Mrow (attrs, + [Mpres.Mfrac ([], + Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1), + Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2)); + Mpres.Mstyle ([None,"scriptlevel","2"], + Mpresentation.Mspace + (RenderingAttrs.small_skip_attributes `MathML)); + Mpres.Mstyle ([None,"scriptlevel","1"],invoke_reinit t3)])) | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t) | A.Root (t1, t2) -> Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2) | A.Box ((_, spacing, _) as kind, terms) -> let children = - aux_children mathonly spacing xref pos prec + aux_children mathonly spacing xref prec (CicNotationUtil.ungroup terms) in box_of mathonly kind attrs children + | A.Mstyle (l,terms) -> + Mpres.Mstyle + (List.map (fun (k,v) -> None,k,v) l, + box_of mathonly (A.H, false, false) attrs + (aux_children mathonly false xref prec + (CicNotationUtil.ungroup terms))) + | A.Mpadded (l,terms) -> + Mpres.Mpadded + (List.map (fun (k,v) -> None,k,v) l, + box_of mathonly (A.H, false, false) attrs + (aux_children mathonly false xref prec + (CicNotationUtil.ungroup terms))) + | A.Maction alternatives -> + toggle_action (List.map invoke_reinit alternatives) | A.Group terms -> let children = - aux_children mathonly false xref pos prec + aux_children mathonly false xref prec (CicNotationUtil.ungroup terms) in box_of mathonly (A.H, false, false) attrs children | A.Break -> assert false (* TODO? *) - and aux_children mathonly spacing xref pos prec terms = + and aux_children mathonly spacing xref prec terms = let find_clusters = let rec aux_list first clusters acc = function @@ -384,30 +432,11 @@ let render ids_to_uris ?(prec=(-1)) = | (A.Layout A.Break) :: tl -> aux_list first (List.rev acc :: clusters) [] tl | [hd] -> -(* let pos' = - if first then - pos - else - match pos with - `None -> `Right - | `Inner -> `Inner - | `Right -> `Right - | `Left -> `Inner - in *) aux_list false clusters - (aux [] mathonly xref pos prec hd :: acc) [] + (aux [] mathonly xref prec hd :: acc) [] | hd :: tl -> -(* let pos' = - match pos, first with - `None, true -> `Left - | `None, false -> `Inner - | `Left, true -> `Left - | `Left, false -> `Inner - | `Right, _ -> `Inner - | `Inner, _ -> `Inner - in *) aux_list false clusters - (aux [] mathonly xref pos prec hd :: acc) tl + (aux [] mathonly xref prec hd :: acc) tl in aux_list true [] [] in @@ -418,7 +447,7 @@ let render ids_to_uris ?(prec=(-1)) = in List.map boxify_pres (find_clusters terms) in - aux [] false (ref []) `Inner prec + aux [] false (ref []) prec let rec print_box (t: boxml_markup) = Box.box2xml print_mpres t