Improve pretty printing of large formulas #540
Labels
Comments
|
Here's a harder to read example from a debugging session using the function And here's an hypothetical and more approachable rendering: |
|
Yikes!
…On Sat, Apr 9, 2022 at 5:51 AM Facundo Domínguez ***@***.***> wrote:
Here's a harder to read example from a debugging session using the
function Language.Fixpoint.Types.PrettyPrint.showFix.
((ReWrite8.mbind (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) (lqdc##$select##ReWrite8.OurMonad##1 (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) (ReWrite8.guard (mp##a1GY : (ReWrite8.MonadPlus m##a1KI)) ((x##a1H0 : int) <=
(p##a1GZ : int))) (ReWrite8.const' (ReWrite8.mreturn (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) GHC.Tuple.$40$$41$))) (ReWrite8.const' (ReWrite8.mreturn (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) (GHC.Tuple.$40$$44$$41$ (GHC.Types.$58$ (x##a1H0 : int) (lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$41$$35$$35$1 (ds_d2Mv : (Tuple [int] [int])))) (lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$41$$35$$35$2 (ds_d2Mv : (Tuple [int] [int]))))))) =
(lqdc##$select##ReWrite8.OurMonad##1 (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) (lqdc##$select##ReWrite8.OurMonad##1 (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) (ReWrite8.guard (mp##a1GY : (ReWrite8.MonadPlus m##a1KI)) ((x##a1H0 : int) <=
(p##a1GZ : int))) (ReWrite8.const' (ReWrite8.mreturn (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) GHC.Tuple.$40$$41$))) (ReWrite8.const' (ReWrite8.mreturn (ReWrite8.monad (mp##a1GY : (ReWrite8.MonadPlus m##a1KI))) (GHC.Tuple.$40$$44$$41$ (GHC.Types.$58$ (x##a1H0 : int) (lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$41$$35$$35$1 (ds_d2Mv : (Tuple [int] [int])))) (lqdc$35$$35$$36$select$35$$35$GHC.Tuple.$40$$44$$41$$35$$35$2 (ds_d2Mv : (Tuple [int] [int]))))))))
—
Reply to this email directly, view it on GitHub
<https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_540-23issuecomment-2D1093995443&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rDXEkeiimrnI7LFh_us0t5xh1e8lsmquAlN5RozngVD52GTz09_sOVIxSX1cVLXN&s=2X_0JwdZeylQNDiacYqe6hpX2EXW6-zBCeDQIbjh-dU&e=>,
or unsubscribe
<https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OFSWPFBGWDVFTV4EMTVEF4OJANCNFSM5S22OF2Q&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=rDXEkeiimrnI7LFh_us0t5xh1e8lsmquAlN5RozngVD52GTz09_sOVIxSX1cVLXN&s=ucHbiPF1wfr7_cw-MqYd_mQDowGa-GxuQ-VIwuTzm6E&e=>
.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In the .fq files generated from running LH, there are sometimes deeply indented expressions that span multiple lines and which are not particularly easy to read. Improving the formatting is important because it takes time to make sense of these expressions when debugging.
Here's an excerpt from stitch-lh
Reading the above expression improves a lot by disabling line wrapping in text editors. Still the longer lines could be broken further:
Improving readability further from there will probably require to give special formatting to nested if-then-else statements. But perhaps we can leave that for another issue.
Other declarations in the .fq files suffer of long lines too. It would be worth doing a pass over them to break them down.
The text was updated successfully, but these errors were encountered: