From c11f4fe10591d568afb410e5d96061448a437254 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 28 Sep 2005 13:35:50 +0000 Subject: [PATCH] better precedence handling, should remove useless parens --- helm/ocaml/cic_notation/cicNotationPp.ml | 4 +- helm/ocaml/cic_notation/cicNotationPres.ml | 31 +++++++---- helm/ocaml/cic_notation/cicNotationPt.ml | 2 +- helm/ocaml/cic_notation/cicNotationRew.ml | 62 ++++++++++++++++------ 4 files changed, 70 insertions(+), 29 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index e5ff1587f..b5a2e04f2 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -32,7 +32,7 @@ module Env = CicNotationEnv * be added to the output of pp_term. * set to false if you need, for example, cut and paste from matitac output to * matitatop *) -let debug_printing = false +let debug_printing = true let pp_binder = function | `Lambda -> "lambda" @@ -60,7 +60,7 @@ let pp_assoc = let pp_pos = function - `None -> "`None" +(* `None -> "`None" *) | `Left -> "`Left" | `Right -> "`Right" | `Inner -> "`Inner" diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index bed2cdd4d..cc3a204a4 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -140,7 +140,7 @@ let semicolon = Mpresentation.Mo ([], ";") let toggle_action children = Mpresentation.Maction ([None, "actiontype", "toggle"], children) -type child_pos = [ `None | `Left | `Right | `Inner ] +type child_pos = [ `Left | `Right | `Inner ] let pp_assoc = function @@ -176,14 +176,19 @@ let is_atomic t = let add_parens child_prec child_assoc child_pos curr_prec t = if is_atomic t then t - else if 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) + else if child_prec >= 0 + && (child_prec < curr_prec + || (child_prec = curr_prec && + child_assoc = Gramext.LeftA && + child_pos = `Right) + || (child_prec = curr_prec && + child_assoc = Gramext.RightA && + child_pos = `Left)) then (* parens should be added *) +(* (prerr_endline "adding parens"; + prerr_endline (Printf.sprintf "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d" + child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos + child_pos) curr_prec); *) match t with | Mpresentation.Mobject (_, box) -> mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ])) @@ -294,16 +299,19 @@ let render ids_to_uris = prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t); assert false and aux_attributes xmlattrs mathonly xref pos prec t = + let reset = ref false in let new_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) | `IdRef xref -> new_xref := xref :: !new_xref @@ -317,7 +325,8 @@ let render ids_to_uris = let t' = aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in - add_parens child_prec child_assoc !new_pos prec t') + if !reset then t' + else add_parens child_prec child_assoc !new_pos prec t') in aux_attribute t and aux_literal xmlattrs xref prec l = @@ -330,7 +339,7 @@ let render ids_to_uris = let attrs = make_xref xref in let invoke' t = aux [] true (ref []) pos prec t in (* use the one below to reset precedence and associativity *) - let invoke_reinit t = aux [] true (ref []) `None 0 t in + let invoke_reinit t = aux [] mathonly xref `Inner ~-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) @@ -403,7 +412,7 @@ let render ids_to_uris = in List.map boxify_pres (find_clusters terms) in - aux [] false (ref []) `None 0 + aux [] false (ref []) `Inner ~-1 let rec print_box (t: boxml_markup) = Box.box2xml print_mpres t diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index d889b0981..ac6a0edbd 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -41,7 +41,7 @@ let fail floc msg = type href = UriManager.uri -type child_pos = [ `None | `Left | `Right | `Inner ] +type child_pos = [ `Left | `Right | `Inner ] type term_attribute = [ `Loc of location (* source file location *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 4a02c8fff..aa171c55c 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -74,6 +74,16 @@ let resolve_binder = function let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t) +let left_pos = add_pos_info `Left +let right_pos = add_pos_info `Right +let inner_pos = add_pos_info `Inner + +let rec top_pos t = add_level_info ~-1 Gramext.NonA (inner_pos t) +(* function + | Ast.AttributedTerm (`Level _, t) -> + add_level_info ~-1 Gramext.NonA (inner_pos t) + | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, top_pos t) + | t -> add_level_info ~-1 Gramext.NonA (inner_pos t) *) let rec remove_level_info = function @@ -126,14 +136,23 @@ let pp_ast0 t k = let rec aux = function | Ast.Appl ts -> + let rec aux_args pos = + function + | [] -> [] + | [ last ] -> + let last = k last in + if pos = `Left then [ left_pos last ] else [ right_pos last ] + | hd :: tl -> + (add_pos_info pos (k hd)) :: aux_args `Inner tl + in add_level_info Ast.apply_prec Ast.apply_assoc - (hovbox true true (CicNotationUtil.dress break (List.map k ts))) + (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts))) | Ast.Binder (binder_kind, (id, ty), body) -> add_level_info Ast.binder_prec Ast.binder_assoc (hvbox false true [ binder_symbol (resolve_binder binder_kind); k id; builtin_symbol ":"; aux_ty ty; break; - builtin_symbol "."; k body ]) + builtin_symbol "."; right_pos (k body) ]) | Ast.Case (what, indty_opt, outty_opt, patterns) -> let outty_box = match outty_opt with @@ -150,7 +169,7 @@ let pp_ast0 t k = let match_box = hvbox false true [ keyword "match"; break; - hvbox false false ([ k what ] @ indty_box); break; + hvbox false false ([ top_pos (k what) ] @ indty_box); break; keyword "with" ] in let mk_case_pattern (head, href, vars) = @@ -163,7 +182,7 @@ let pp_ast0 t k = (hvbox false true [ hbox false true [ mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; - break; k rhs ])) + break; top_pos (k rhs) ])) patterns in let patterns'' = @@ -195,15 +214,15 @@ let pp_ast0 t k = | Ast.Cast (bo, ty) -> add_level_info Ast.simple_prec Ast.simple_assoc (hvbox false true [ - builtin_symbol "("; k bo; break; builtin_symbol ":"; k ty; - builtin_symbol ")"]) + builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":"; + top_pos (k ty); builtin_symbol ")"]) | Ast.LetIn (var, s, t) -> add_level_info Ast.let_in_prec Ast.let_in_assoc (hvbox false true [ hvbox false true [ keyword "let"; hvbox false true [ - aux_var var; builtin_symbol "\\def"; break; k s ]; + aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ]; break; keyword "in" ]; break; k t ]) @@ -220,7 +239,7 @@ let pp_ast0 t k = let (name, body) = fst_fun in hvbox false true [ keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; - body ] + top_pos body ] in let tl_rows = List.map @@ -434,7 +453,7 @@ let instantiate21 idrefs env l1 = | t -> CicNotationUtil.group (subst pos env t) and subst pos env = function | Ast.AttributedTerm (attr, t) as term -> - prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); +(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *) subst pos env t | Ast.Variable var -> let name, expected_ty = CicNotationEnv.declaration_of_var var in @@ -515,7 +534,7 @@ let instantiate21 idrefs env l1 = match pos with | `Inner -> `Right | `Left -> `Left - | `None -> assert false +(* | `None -> assert false *) | `Right -> `Right in [ subst pos' env child ] @@ -524,7 +543,7 @@ let instantiate21 idrefs env l1 = match pos with | `Inner -> `Inner | `Left -> `Inner - | `None -> assert false +(* | `None -> assert false *) | `Right -> `Right in (subst pos env hd) :: subst_children pos' env tl @@ -557,13 +576,12 @@ let rec pp_ast1 term = let idrefs = List.flatten (List.map CicNotationUtil.get_idrefs ctors) in - let prec, assoc, l1 = + let l1 = try Hashtbl.find level1_patterns21 pid with Not_found -> assert false in - add_level_info prec assoc - (instantiate21 idrefs (ast_env_of_env env) l1)) + instantiate21 idrefs (ast_env_of_env env) l1) let instantiate32 term_info idrefs env symbol args = let rec instantiate_arg = function @@ -680,10 +698,24 @@ let lookup_interpretations symbol = !(Hashtbl.find interpretations symbol))) with Not_found -> raise Interpretation_not_found +let fill_pos_info l1_pattern = l1_pattern +(* let rec aux toplevel pos = + function + | Ast.Layout l -> + (match l + + | Ast.Magic m -> + Ast.Box ( + | Ast.Variable _ as t -> add_pos_info pos t + | t -> t + in + aux true l1_pattern *) + let add_pretty_printer ~precedence ~associativity l2 l1 = let id = fresh_id () in + let l1' = add_level_info precedence associativity (fill_pos_info l1) in let l2' = CicNotationUtil.strip_attributes l2 in - Hashtbl.add level1_patterns21 id (precedence, associativity, l1); + Hashtbl.add level1_patterns21 id l1'; pattern21_matrix := (l2', id) :: !pattern21_matrix; load_patterns21 !pattern21_matrix; id -- 2.39.2