X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=84eaaeb2a7711dd85e7d898294de6729f9a5913c;hb=8c4659819a1c1f2e450d9a588ecca37d95ae48e9;hp=673df335f224d4db81427637f1c185bb31e2a9bb;hpb=407ff2f7c09ddd90eae6f390006ffe801b683164;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 673df335f..84eaaeb2a 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -181,23 +181,16 @@ let is_atomic t = in aux_mpres t -let add_parens child_prec child_assoc child_pos curr_prec t = +let add_parens child_prec 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!"; *) + else if child_prec >= 0 && child_prec < curr_prec then + begin (* parens should be added *) +(* prerr_endline "adding parens!"; *) match t with | Mpresentation.Mobject (_, box) -> mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ])) @@ -257,10 +250,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) @@ -293,7 +286,7 @@ 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 @@ -307,7 +300,7 @@ let render ids_to_uris ?(prec=(-1)) = (List.map (function | None -> Mpres.Mtext ([], "_") - | Some t -> aux xmlattrs mathonly xref pos prec t) l)) @ + | Some t -> aux xmlattrs mathonly xref prec t) l)) @ [ Mpres.Mtext ([], "]")]) in let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in @@ -316,18 +309,18 @@ let render ids_to_uris ?(prec=(-1)) = @ (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 @@ -335,22 +328,28 @@ let render ids_to_uris ?(prec=(-1)) = (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 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 !new_pos child_prec t in + aux !new_xmlattrs mathonly new_xref child_prec t in if !reset then t' - else add_parens child_prec child_assoc !new_pos prec t') + else add_parens child_prec prec t') in aux_attribute t and aux_literal xmlattrs xref prec l = @@ -359,11 +358,11 @@ let render ids_to_uris ?(prec=(-1)) = | `Symbol 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) @@ -380,18 +379,18 @@ let render ids_to_uris ?(prec=(-1)) = 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.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 @@ -402,30 +401,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 @@ -436,7 +416,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