From 07308812dcb5251843336badef927ea9e302f024 Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Tue, 10 Mar 2026 09:32:41 -0400 Subject: [PATCH] Fixing issues with the pretty printing of operators relating to parsing (in the case of qualified unary operators) and unnecessary qualification (both when given no arguments and when given arguments). close #854 --- src/ecPrinting.ml | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 30dd941ba..c3f29cdfa 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -487,7 +487,7 @@ let pp_string fmt x = let pp_path fmt p = Format.fprintf fmt "%s" (P.tostring p) -let pp_xpath fmt (xp: P.xpath) = +let pp_xpath fmt (xp: P.xpath) = Format.fprintf fmt "%s" (P.x_tostring xp) (* -------------------------------------------------------------------- *) @@ -776,6 +776,10 @@ let priority_of_unop = | _ -> None +(* -------------------------------------------------------------------- *) +let is_unop name = + (priority_of_unop name) <> None + (* -------------------------------------------------------------------- *) let is_binop name = (priority_of_binop name) <> None @@ -903,7 +907,7 @@ let pp_opname (fmt : Format.formatter) ((nm, op) : symbol list * symbol) = if op.[0] = '*' || op.[String.length op - 1] = '*' then Format.sprintf "( %s )" op else Format.sprintf "(%s)" op - end else if is_pstop op then + end else if is_pstop op || (is_unop op && nm <> []) then Format.sprintf "(%s)" op else op @@ -1085,10 +1089,11 @@ let pp_opapp ((pred : [`Expr | `Form]), (op : EcPath.path), (tvi : EcTypes.ty list), - (es : 'a list)) + (es : 'a list), + (tyopt : ty option)) = let (nm, opname) = - PPEnv.op_symb ppe op (Some (pred, tvi, (List.map t_ty es, None))) in + PPEnv.op_symb ppe op (Some (pred, tvi, (List.map t_ty es, tyopt))) in let pp_tuple_sub ppe prec fmt e = match is_tuple e with @@ -1842,7 +1847,8 @@ and pp_form_core_r (fmt : Format.formatter) (f : form) = - let pp_opapp ppe (outer : opprec * iassoc) (fmt : Format.formatter) (op, tys, es) = + let pp_opapp ppe (outer : opprec * iassoc) (fmt : Format.formatter) + (op, tys, es, tyopt) = let rec dt_sub f = match destr_app f with | ({ f_node = Fop (p, tvi) }, args) -> Some (p, tvi, args) @@ -1872,7 +1878,7 @@ and pp_form_core_r in pp_opapp ppe f_ty (dt_sub, pp_form_r, is_trm, is_tuple, is_proj) - lower_left outer fmt (`Form, op, tys, es) + lower_left outer fmt (`Form, op, tys, es, tyopt) in match f.f_node with @@ -1935,7 +1941,7 @@ and pp_form_core_r pp_let ~fv:f2.f_fv ppe pp_form_r outer fmt (lp, f1, f2) | Fop (op, tvi) -> - pp_opapp ppe outer fmt (op, tvi, []) + pp_opapp ppe outer fmt (op, tvi, [], Some f.f_ty) | Fapp ({f_node = Fop (op, _)}, [{f_node = Fapp ({f_node = Fop (op', tys)}, [f1; f2])}]) @@ -1943,10 +1949,10 @@ and pp_form_core_r && EcPath.p_equal op' EcCoreLib.CI_Bool.p_eq -> let negop = EcPath.pqoname (EcPath.prefix op') "<>" in - pp_opapp ppe outer fmt (negop, tys, [f1; f2]) + pp_opapp ppe outer fmt (negop, tys, [f1; f2], Some f.f_ty) | Fapp ({f_node = Fop (p, tys)}, args) -> - pp_opapp ppe outer fmt (p, tys, args) + pp_opapp ppe outer fmt (p, tys, args, Some f.f_ty) | Fapp (e, args) -> pp_app ppe ~pp_first:pp_form_r ~pp_sub:pp_form_r outer fmt (e, args) @@ -2859,9 +2865,9 @@ let pp_i_blk (_ppe : PPEnv.t) fmt _ = let pp_i_abstract (_ppe : PPEnv.t) fmt id = Format.fprintf fmt "%s" (EcIdent.name id) -let pp_abs_uses (ppe : PPEnv.t) fmt (aus: abs_uses) = - let pp_pv_ty ppe fmt (pv, ty) = - Format.fprintf fmt "(%a : %a)" (pp_pv ppe) pv (pp_type ppe) ty +let pp_abs_uses (ppe : PPEnv.t) fmt (aus: abs_uses) = + let pp_pv_ty ppe fmt (pv, ty) = + Format.fprintf fmt "(%a : %a)" (pp_pv ppe) pv (pp_type ppe) ty in let on_empty fmt () = Format.fprintf fmt "None" in Format.fprintf fmt "{ calls: %a, reads: %a, writes: %a }" @@ -3313,7 +3319,7 @@ module PPGoal = struct (None, fun fmt -> pp_form ppe fmt f) | EcBaseLogic.LD_abs_st aus -> - (None, fun fmt -> Format.fprintf fmt "statement %a" + (None, fun fmt -> Format.fprintf fmt "statement %a" (pp_abs_uses ppe) aus) in (ppe, (id, pdk))