search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 643 forks source link

Possible Inconsistent behaviour with PrettyPrint. #2465

Open jfdm opened 9 years ago

jfdm commented 9 years ago

I was playing around with the Idris semantic pretty printer (on Idris HEAD) to get semantically highlighted Idris code, and noticed that Idris now applies sugaring during the process. For example, the command:

:pp latex 80 (S (S (S Z)))

produces

\IdrisData{3}

and not

(\IdrisData{S} (\IdrisData{S} (\IdrisData{S} \IdrisData{Z})))

while

:pp latex 80 Z

produces

\IdrisData{Z} : \IdrisType{Nat}

I'm wondering if this is expected behaviour or 'teething' issues w.r.t. to the implementation. I would have imagined that both commands would either be sugared or left desugared.

david-christiansen commented 9 years ago

This is funny! I think it's because S (S (S Z)) is seen as an expression to pprint, whereas Z is seen as a definition without an RHS. Perhaps it needs a bit more thought there!