Make error messages consistently formatted with locations

[JoeyEremondi]

Fixed version of #37.

There are two main effects of this change. First, all error messages are printed using the same formatting, for consistency and ease of parsing. Secondly, location information is included in error messages whenever possible.

Now, error messages have the following format:

File filename on loc:
Error: error message text

For example:

File ../tests/test10st.ott on line 55, column 7 - 81:
Warning: Free variables in hom element [[G2]]

While there are a lot of changes, very little of the functionality of Ott is changed, since the changes only affect printing of errors. I've run the tests, and on my machine this causes no regressions.

Note that this PR also includes the changes from #40. This change is now independent of #40.

[PeterSewell]

This error message fixing sounds uncontroversially a good thing. The #40 diff is not so clear - without looking at the code, I'd guess that the original bug is a lack of a "principle ntr of ntr" call somewhere, so I'm a bit suspicious of adding a separate bounds coalescing phase. No time to properly look now, though - apologies!

…

On 5 September 2018 at 22:43, Joey Eremondi ***@***.***> wrote: Fixed version of #37 <#37>. There are two main effects of this change. First, all error messages are printed using the same formatting, for consistency and ease of parsing. Secondly, location information is included in error messages whenever possible. Now, error messages have the following format: File filename on loc: Error: error message text For example: File ../tests/test10st.ott on line 55, column 7 - 81: Warning: Free variables in hom element [[G2]] While there are a lot of changes, very little of the functionality of Ott is changed, since the changes only affect printing of errors. I've run the tests, and on my machine this causes no regressions. Note that this PR also includes the changes from #40 <#40>. ------------------------------ You can view, comment on, or merge this pull request online at: #41 Commit Summary - Make error messages consistently formatted with locations File Changes - *M* .gitignore <https://github.com/ott-lang/ott/pull/41/files#diff-0> (2) - *M* regression/config.otr <https://github.com/ott-lang/ott/pull/41/files#diff-1> (1) - *M* regression/regression.otl <https://github.com/ott-lang/ott/pull/41/files#diff-2> (1) - *M* src/auxl.ml <https://github.com/ott-lang/ott/pull/41/files#diff-3> (122) - *M* src/bounds.ml <https://github.com/ott-lang/ott/pull/41/files#diff-4> (66) - *M* src/bounds.mli <https://github.com/ott-lang/ott/pull/41/files#diff-5> (4) - *M* src/context_pp.ml <https://github.com/ott-lang/ott/pull/41/files#diff-6> (2) - *M* src/coq_induct.ml <https://github.com/ott-lang/ott/pull/41/files#diff-7> (2) - *M* src/defns.ml <https://github.com/ott-lang/ott/pull/41/files#diff-8> (31) - *M* src/defns.mli <https://github.com/ott-lang/ott/pull/41/files#diff-9> (6) - *M* src/dependency.ml <https://github.com/ott-lang/ott/pull/41/files#diff-10> (18) - *M* src/grammar_lexer.mll <https://github.com/ott-lang/ott/pull/41/files#diff-11> (21) - *M* src/grammar_parser.mly <https://github.com/ott-lang/ott/pull/41/files#diff-12> (4) - *M* src/grammar_pp.ml <https://github.com/ott-lang/ott/pull/41/files#diff-13> (88) - *M* src/grammar_typecheck.ml <https://github.com/ott-lang/ott/pull/41/files#diff-14> (161) - *M* src/lex_menhir_pp.ml <https://github.com/ott-lang/ott/pull/41/files#diff-15> (21) - *M* src/ln_transform.ml <https://github.com/ott-lang/ott/pull/41/files#diff-16> (76) - *M* src/location.ml <https://github.com/ott-lang/ott/pull/41/files#diff-17> (23) - *M* src/main.ml <https://github.com/ott-lang/ott/pull/41/files#diff-18> (60) - *M* src/new_term_parser.ml <https://github.com/ott-lang/ott/pull/41/files#diff-19> (2) - *M* src/subrules_pp.ml <https://github.com/ott-lang/ott/pull/41/files#diff-20> (2) - *M* src/substs_pp.ml <https://github.com/ott-lang/ott/pull/41/files#diff-21> (14) - *M* src/system_pp.ml <https://github.com/ott-lang/ott/pull/41/files#diff-22> (12) - *M* src/term_parser.ml <https://github.com/ott-lang/ott/pull/41/files#diff-23> (34) - *M* src/transform.ml <https://github.com/ott-lang/ott/pull/41/files#diff-24> (46) - *M* src/types.ml <https://github.com/ott-lang/ott/pull/41/files#diff-25> (20) - *A* tests/test_list_subrules.ott <https://github.com/ott-lang/ott/pull/41/files#diff-26> (44) Patch Links: - https://github.com/ott-lang/ott/pull/41.patch - https://github.com/ott-lang/ott/pull/41.diff — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#41>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5rDMi7GHeqAQKrwHE0KjhE7bwrJDks5uYEWdgaJpZM4Wbvyx> .

[JoeyEremondi]

@PeterSewell fair enough, would you like me to resubmit without the changes from #40 ?

[PeterSewell]

Yes please

…

On Thu, 6 Sep 2018, 01:17 Joey Eremondi, ***@***.***> wrote: @PeterSewell <https://github.com/PeterSewell> fair enough, would you like me to resubmit without the changes from #40 <#40> ? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#41 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5pCXDbAE1UQh2Bhh-BK5HIZ6zHluks5uYGlygaJpZM4Wbvyx> .

[JoeyEremondi]

@PeterSewell Okay, I've updated this PR to be independent of #40.