Further improve formatting of Core

[keyboardDrummer]

Changes

• Add a Python script in Tools that enables automatically updating the results of #guard_msg
• Update formatting of applications in Core. A good way to see how the formatting has changed is to look at the updated tests in this PR.

Before:

while (((~Int.Lt i) n)) (some ((~Int.Sub n) i)) (some ((~Bool.And ((~Int.Le i) n)) (((~Int.Div ((~Int.Mul i) ((~Int.Sub i) #1))) #2) == sum))) {sum := ((~Int.Add sum) i)
 i := ((~Int.Add i) #1)}

After:

  while
    (~Int.Lt i n)
    (some (~Int.Sub n i))
    (some (~Bool.And (~Int.Le i n) ((~Int.Div (~Int.Mul i (~Int.Sub i #1)) #2) == sum)))
  {
    sum := (~Int.Add sum i)
    i := (~Int.Add i #1)
  }

Applications in expressions require fewer parenthesis are are shown in a tree like fashion when they do not fit on a line:

Before

/-- info: Annotated expression:
((((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) (((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) (((~Prod : (arrow int (arrow string (Tup int string)))) #3) #a)) (((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) (((~Prod : (arrow int (arrow string (Tup int string)))) #4) #b)) (~Nil : (List (Tup int string)))))) #0) (λ (λ (λ (((~Int.Add : (arrow int (arrow int int))) (((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2) (λ (λ %1)))) ((((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) %1) #1) (λ (λ (λ (((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2) (λ (λ %1))))))))))))

After

/--
info: Annotated expression:
((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int))))
 ((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string)))))
  ((~Prod : (arrow int (arrow string (Tup int string)))) #3 #a)
  ((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string)))))
   ((~Prod : (arrow int (arrow string (Tup int string)))) #4 #b)
   (~Nil : (List (Tup int string)))))
 #0
 (λ (λ (λ ((~Int.Add : (arrow int (arrow int int)))
     ((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2 (λ (λ %1)))
     ((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int))))
      %1
      #1
      (λ (λ (λ ((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int)))
          %2
          (λ (λ %1))))))))))))

Testing

Updated tests

[atomb]

I noted one small suggestion for formatting, but it's not at all blocking.

[atomb]

It'd be nice to have this closer to source syntax. Maybe:

while ((x : int) == #0)
  decreases (x : int)
  invariant #true
...

And the decreases and invariant could simply be omitted when they don't exist.

[atomb]

Thanks for writing this! It'll be a huge help to all of us.