Improve output

[KenSakayori]

This PR improves the output/logging feature of ReTHFL.
Currently, ReTHFL outputs lots of debug information to stdout.
For example,

$ rethfl input/ok/valid/sum.in 
[Main:App:Input]
  S : int -> bool =ν λn3:int.Sum n3 (λr4:int.n3 <= r4)
  Sum : int -> (int -> bool) -> bool =ν
    λx5:int.λk6:(int -> bool).x5 <= 0 && k6 0 || x5 > 0 && Sum (x5 - 1) (λy7:int.k6 (x5 + y7))
[Main:App:Simplified]
  S : int -> bool =ν λn3:int.Sum n3 (λr4:int.n3 <= r4)
  Sum : int -> (int -> bool) -> bool =ν
    λx5:int.λk6:(int -> bool).x5 <= 0 && k6 0 || x5 > 0 && Sum (x5 - 1) (λy7:int.k6 (x5 + y7))
[Main:App:Peephole]
  S : int -> bool =ν λn3:int.Sum n3 (λr4:int.n3 <= r4)
  Sum : int -> (int -> bool) -> bool =ν
    λx5:int.λk6:(int -> bool).x5 <= 0 && k6 0 || x5 > 0 && Sum (x5 - 1) (λy7:int.k6 (x5 + y7))
S *[X18()]
Sum (x11: int -> ((t12: int -> *[X1(t12,x11)]) -> *[X2(x11)]))


infering new formula: S = (∀n3: int.((Sum n3) (\r4: int.n3<=r4)))
[Result]
X18() => X19(n3)
X19(n3) => X24(n3)
X24(n3) => X2(n3)
(X24(n3) /\ X1(x20,n3)) => n3<=x20
tt => X18()


infering new formula: Sum = (\x5: int.(\(t19: int -> *[X3(t19,x5)]).((x5>0 || (k6 0)):X4(x5) && (x5<=0 || ((Sum x5 - 1) (\y7: int.(k6 x5 + y7)))):X5(x5))))
[Result]
X2(x22) => ((x22>0 \/ X3(0,x22)) /\ (x22<=0 \/ X25(x22)))
(X2(x22) /\ X3(x23,x22)) => X1(x23,x22)
X25(x5) => X2(x5 - 1)
(X25(x5) /\ X1(x21,x5 - 1)) => X3(x5 + x21,x5)
X18() => X19(n3)
X19(n3) => X24(n3)
X24(n3) => X2(n3)
(X24(n3) /\ X1(x20,n3)) => n3<=x20
tt => X18()
[Size] 1
CHC file: /tmp/hoice-231064765.smt2
Profiling:
  CHC Solver: 0.035704 sec
did not calculate refinement. Use --show-refinement
Verification Result:
  Valid
Profiling:
  total: 0.036571 sec

After the change, the output becomes

$ rethfl input/ok/valid/sum.in 
CHC file: /tmp/hoice-74276176.smt2
Profiling:
  CHC Solver: 0.057801 sec
did not calculate refinement. Use --show-refinement
Verification Result:
  Valid
Profiling:
  total: 0.058036 sec

With --show-refinement, it is as follows

$ rethfl input/ok/valid/sum.in 
CHC file: /tmp/hoice-238205435.smt2
Profiling:
  CHC Solver: 0.045280 sec
Refinement types:
S: *[tt]
Sum: (x11: int -> ((t12: int -> *[t12 + -1 * x11>=0]) -> *[tt]))
Verification Result:
  Valid
Profiling:
  total: 0.045477 sec

All the information the has been hidden can be shown by adding the verbose flag -v (with a better formatting).

$rethfl input/ok/valid/sum.in --show-refinement -v
[Main:Info:Input]
  S : int -> bool =ν λn3:int.Sum n3 (λr4:int.n3 <= r4)
  Sum : int -> (int -> bool) -> bool =ν
    λx5:int.λk6:(int -> bool).x5 <= 0 && k6 0 || x5 > 0 && Sum (x5 - 1) (λy7:int.k6 (x5 + y7))
[Trans:Info:Inline]
  []
[Main:Info:Simplified]
  S : int -> bool =ν λn3:int.Sum n3 (λr4:int.n3 <= r4)
  Sum : int -> (int -> bool) -> bool =ν
    λx5:int.λk6:(int -> bool).x5 <= 0 && k6 0 || x5 > 0 && Sum (x5 - 1) (λy7:int.k6 (x5 + y7))
[Main:Info:Peephole]
  S : int -> bool =ν λn3:int.Sum n3 (λr4:int.n3 <= r4)
  Sum : int -> (int -> bool) -> bool =ν
    λx5:int.λk6:(int -> bool).x5 <= 0 && k6 0 || x5 > 0 && Sum (x5 - 1) (λy7:int.k6 (x5 + y7))
[Rinfer:Info:Initial types]
  S: *[X18()]
  Sum: (x11: int -> ((t12: int -> *[X1(t12,x11)]) -> *[X2(x11)]))

[Rinfer:Info:Infering new formula]
  S = (∀n3: int.((Sum  (n3))  (\r4: int.(n3<=r4))))
[Rinfer:Info:Constraints]
  X18() => X19(n3)
  X19(n3) => X24(n3)
  X24(n3) => X2(n3)
  (X24(n3) /\ X1(x20,n3)) => n3<=x20
  tt => X18()

[Rinfer:Info:Infering new formula]
  Sum = (\x5: int.
          (\(t19: int -> *[X3(t19,x5)]).
            (((x5>0) || (k6  (0))):X4(x5)
              && ((x5<=0) || ((Sum  (x5 - 1))  (\y7: int.(k6  (x5 + y7))))):X5(x5))))
[Rinfer:Info:Constraints]
  X2(x22) => ((x22>0 \/ X3(0,x22)) /\ (x22<=0 \/ X25(x22)))
  (X2(x22) /\ X3(x23,x22)) => X1(x23,x22)
  X25(x5) => X2(x5 - 1)
  (X25(x5) /\ X1(x21,x5 - 1)) => X3(x5 + x21,x5)
  X18() => X19(n3)
  X19(n3) => X24(n3)
  X24(n3) => X2(n3)
  (X24(n3) /\ X1(x20,n3)) => n3<=x20
  tt => X18()

[Rinfer:Info:Size of constraints]
  1
CHC file: /tmp/hoice-19040976.smt2
[CHC Solver:Info:Model]
  (model
  (define-fun X2
    ( (v_0 Int) ) Bool
    true
  )
  (define-fun X25
    ( (v_0 Int) ) Bool
    (>= v_0 1)
  )
  (define-fun X24
    ( (v_0 Int) ) Bool
    true
  )
  (define-fun X19
    ( (v_0 Int) ) Bool
    true
  )
  (define-fun X18
    ( ) Bool
    true
  )
  (define-fun X3
    ( (v_0 Int) (v_1 Int) ) Bool
    (>= (+ v_0 (* (- 1) v_1)) 0)
  )
  (define-fun X1
    ( (v_0 Int) (v_1 Int) ) Bool
    (X3 v_0 v_1)
  )
)

Profiling:
  CHC Solver: 0.045952 sec
Refinement types:
S: *[tt]
Sum: (x11: int -> ((t12: int -> *[t12 + -1 * x11>=0]) -> *[tt]))
Verification Result:
  Valid
Profiling:
  total: 0.046588 sec

It is also possible to specify the module the user want to log.

As a byproduct, this PR implements various pretty printers.

[KenSakayori]

I don't know why And and Or are asymmetric, but I followed the original implementation.

[KenSakayori]

The pretty printer that prints type bindings now takes type environments rather than hes as the argument.
This is because hes might be cut off in the type annotation mode.
Because of this print_derived_refinement_type is also modified

[KenSakayori]

Merged as @moratorium08 told me it's okay to do so.