NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Printing precedence levels incorrect #67

Open alberdingk-thijm opened 3 years ago

alberdingk-thijm commented 3 years ago

The current precedence levels used when printing seem to have some minor inconsistencies which lead to the absence or redundancy of parentheses in some places. These occur in a couple different situations:

open Nv_lang
(* a function for reprinting parsed strings *)
let f s = Printing.exp_to_string (Parser.expreof Lexer.token (Lexing.from_string s);;
(* operator function arguments are missing parentheses *)
let s = "foldNodes (fun u -> fun v -> fun acc -> assert_node u v && acc) sol true";;
f s;; (* u"foldNodes fun u~0 -> fun v~0 -> fun acc~0 -> ((assert_node~0 u~0 ) v~0 ) && acc~0    sol~0 true" *)
(* extra parentheses around function bodies *)
let t = "fun u -> fun v -> match (u,v) with | (None, None) -> false | (_, _) -> true";;
f t;; (* u"fun u~0 -> fun v~0 -> (match (u~0,v~0) with \n | (None,None) -> false\n | (_,_) -> true\n)  " *)

I'd like to fix these inconsistencies but I'm not too familiar with how the precedence levels align between the printer and the parser.

alberdingk-thijm commented 3 years ago

@DKLoehr @nickgian can either of you lend any insight into this, or how I could modify prec_exp and the other functions here? I can see that we have some functions where parentheses get added if the precedence is lower than max_prec (func_to_string, closure_to_string) and then in exp_to_string we add parentheses if the precedence is higher in the inner expression relative to the outer one.

DKLoehr commented 3 years ago

Don't think I have much to contribute here -- if I were to try to fix this myself I'd probably just try a bunch of examples and see what the parser does, then edit printing to match that. I suspect we probably erred on the side of putting in more parens than necessary to be safe. If there are any cases where the printed version doesn't actually parse to the same thing (especially if parens are missing) that's worth fixing, but I never thought too hard about the inner workings of the printer.