Pretty printing problems

[edwinb]

There's a couple of small things which have changed in the new pretty printing code. They're minor (so I'll stick them in the same issue report), but we should probably fix them before the next release.

Firstly:

Idris> sequence [[1,2,3],[4,5,6]]
Can't disambiguate name: ::,::,::

This should give fully qualified names for each ::.

Secondly, given the following lemma:

  revrev : (xs : List a) -> rev (rev xs) = xs
  revrev xs = ?revrev_prf

Theorem proving mode for :p revrev_prf gives:

----------                 Goal:                  ----------
{hole0} : (a : Type) ->
 (xs : Prelude.List.List a) -> Main.rev {a = a} (Main.rev {a = a} xs) = xs

I can see that it is useful to have implicits shown in many cases, but often (as here) I think it's a bit cluttered. So I think the display here ought to respect the showimplicits setting. (Separately, maybe it'd be nice to set/unset options from within proof mode.)

[david-christiansen]

I'll take care of these as soon as I get a couple of minutes. Thanks for pointing them out!

[edwinb]

I've fixed the first of these by being careful to display the name rather than the term at the head. test040 catches this now!

[david-christiansen]

Here's another problem: bad alignment in the prover.

  f : Type -> Type
  g : Type -> Type
  h : Type -> Type
  inject : (A : Type) -> (f A) -> g A
  project : (A1 : Type) -> (g A1) -> Maybe (f A1)
  injectProject : (A2 : Type) ->
(ga : g A2) ->
(fa : f A2) ->
(project A2 ga = Just fa) -> ga = inject A2 fa
  projectInject : (A3 : Type) ->
(fa1 : f A3) ->
project A3 (inject A3 fa1) = Just fa1
  a : Type
  x : f a
--------------------------------------
injection_rhs : :+: g h a

which should be

  f : Type -> Type
  g : Type -> Type
  h : Type -> Type
  inject : (A : Type) -> (f A) -> g A
  project : (A1 : Type) -> (g A1) -> Maybe (f A1)
  injectProject : (A2 : Type) ->
                  (ga : g A2) ->
                  (fa : f A2) ->
                  (project A2 ga = Just fa) -> ga = inject A2 fa
  projectInject : (A3 : Type) ->
                  (fa1 : f A3) ->
                  project A3 (inject A3 fa1) = Just fa1
  a : Type
  x : f a
--------------------------------------
injection_rhs : :+: g h a