Implement new desugaring mechanism for copatterns

[tdidriksen]

Here are some examples of how we want to desugar copatterns in the future, in order to make where-blocks work properly (and perhaps also withs).

zeros : Stream Nat
head zeros = Z
tail zeros = zeros

-- Desugared version
zeros : Stream Nat
zeros = MkStream head_ tail_
  where
    head_ : Nat
    head_ = Z

    tail_ : Stream Nat
    tail_ = zeros

cycle : Nat -> Nat -> Stream Nat
head cycle n m = n
tail cycle Z m = cycle m m 
tail cycle (S n) m = cycle n m

-- Desugared version
cycle : Nat -> Nat -> Stream Nat
cycle n m = MkStream (head_ n m) (tail_ n m)
  where
   head_ : Nat -> Nat -> Nat
   head_ n m = n

   tail_ : Nat -> Nat -> Stream Nat
   tail_ Z m = cycle m m
   tail_ (S n) m = cycle n m

corecord Foo : Type where
  bar : Foo -> Bool
  baz : (f : Foo) -> if (bar f) then Nat else Bool

foo : Foo
bar foo = True
baz foo = S Z

-- Desugared version
foo : Foo
foo = MkFoo bar_ baz_
  where
   bar_ : Bool
   bar_ = True

   baz_ : if bar_ then Nat else Bool
   baz_ = S Z

[tdidriksen]

Actually, it would make sense to do an internal desugaring to right-hand side copatterns as an intermediate step before desugaring to constructors.