tdidriksen / idris-dev Goto Github PK

'undefined' has been given in many places where a proper error should be given instead.

This might not be our issue. We should check if this is also an issue on master.

Given a tree:

corecord Tree : Type -> Type where
  value : Tree a -> a
  left  : Tree a -> Tree a
  right : Tree a -> Tree a

The following two should be equivalent:

total causal grow : (Nat, Nat) -> Tree(Nat, Nat)
grow (n, d) = MkTree (n, d) (grow (n, n + d)) (grow (n + d, d))

total causal grow' : (Nat, Nat) -> Tree (Nat, Nat)
&value grow' (n, d) = (n, d)
&left  grow' (n, d) = grow' (n, n + d)
&right grow' (n, d) = grow' (n + d, d)

The one without copatterns work, however the one with copatterns give the following error:

simple.idr:69:14:No type declaration for value

Either I am missing something or this is a bug.

Many functions lack proper documentation. Be better than the remaining Idris documentation and document the code properly!

Currently, the following only generates a clause for cycle (S n) m:

cycle : Nat -> Nat -> Stream' Nat
&hd cycle n m = n
&tl cycle (S n) m = cycle n m

Resulting in:

cycle : Nat -> Nat -> Stream' Nat
cycle (S n) m = MkStream' (S n) cycle n m

Perhaps two clauses should be generated, such that 'cycle' is desugared to:

cycle : Nat -> Nat -> Stream' Nat
cycle Z m = MkStream' Z ?cycletl
cycle (S n) m = MkStream' (S n) cycle n m

This may or may not be an issue.

Copatterns cannot currently be used in with clauses. Beat Agda by adding this feature!

This might not be a problem. Look into this.

We currently make the user add a special token ('&' at the time of writing) in front of all left-hand side projections. It would be better if these were recognized automatically, without any guidance from the user.

Projections should be allowed to different as long as they are equivalent. The below example should be valid and should generate a constructor with one implicit:

corecord Stream : Type -> Type where
  head : Stream a -> a
  tail : Stream b -> Stream b

Branch: Corecords

Trying to define the following program:

corecord Gedde : Type where
  han : Gedde -> Maybe Nat
  hun : Gedde -> (n : Nat) -> fisk Nat (Just n)
  stime : Gedde -> Gedde
  uvist : (john : Gedde) -> case han john of
                              Just n => Vect n (Maybe Nat)
                              Nothing => Bool

I get the error:

When elaborating right hand side of x.Gedde.uvist:
Can't unify
        case block in MkGedde han hun stime han
with
        case block in MkGedde han
                              hun
                              (Delay (Force (Delay (Force stime))))
                              han

Specifically:
        Can't unify
                case block in MkGedde han hun stime han
        with
                case block in MkGedde han
                                      hun
                                      (Delay (Force (Delay (Force stime))))
                                      han

However, an equivalent record definition only issues warnings:

record A : Type where
  MkA : (han : Maybe Nat) -> (hun : (n : Nat) -> 
            fisk Nat (Just n)) -> (stime : A) -> 
            (uvist : case han of
                           Just n => Vect n (Maybe Nat)
                           Nothing => Bool) -> 
            A

I believe case analysis in types in corecords should be possible.

If we have two or more equivalent clauses, only one clause should be produced by the desugaring step.
Example:

&hd f Z = rhs1
&hd f (S n) = rhs2
&tl f Z = rhs3
&tl f (S n) = rhs4

Currently produces:

f Z = mk rhs1 rhs3
f (S n) = mk rhs2 rhs4
f Z = mk rhs1 rhs3
f (S n) = mk rhs2 rhs4

While it should only produce:

f Z = mk rhs1 rhs3
f (S n) = mk rhs2 rhs4

Currently the condition is ((not (null ps)) && hasLhsProjs (head ps), which is not very pretty. Do better!

A corecord definition such as:

corecord Foo : Type where
  bar : Foo

currently crashes Idris due to an non-exhaustive pattern match. This should produce an error message instead as bar is not a valid projection.

Setter generation does not work for corecords. It generates a warning like:

corecords.idr:3:10:Warning - can't generate setter for Corecords.Stream'.hd (tydecl Corecords.Stream'.set_hd : {a : _} -> ({Corecords.Stream'.hd_out0} : a) -> ({rec0} : Corecords.Stream' a) -> Corecords.Stream' a)

Branch: Corecords

The following results in an error when elaborating projection functions:

corecord BisimStream' : Stream' a -> Stream' a -> Type where
  phd : BisimStream' s s' -> (hd s) = (hd s')
  ptl : BisimStream' s s' -> BisimStream' (tl s) (tl s')

Explicitly adding the type to the type constructor solves this:

corecord BisimStream' : (a : Type) -> Stream' a -> Stream' a -> Type where
  phd : BisimStream' a s s' -> (hd s) = (hd s')
  ptl : BisimStream' a s s' -> BisimStream' a (tl s) (tl s')

This problem also exists for records and is as such not a problem with our implementation.

Branch: Corecords

In expandRhs, the lookup implementation assumes that the projection name is unique. This might not be the case.

Implement something akin to Hagino's merge-construct in Idris.

 fun iseq1() = merge head <= 1
                   & tail <= iseq1();

Currently all clauses do almost the same. Fix it.

The first step to elaborated copatterns is obtaining the power to create auxiliarty functions with the elaborator. Discuss!

Projections should be able to depend on each other.

Branch: Corecords

This might not be a problem. Look into this.

Currently the parser reports an error if you use parentheses around the target for a left-hand side projection. This should be possible as not having it is confusing, although perhaps it should be optional.

Copatterns currently only work with records. Make them work with corecords as well.

Currently, you cannot make left-hand side projections on clauses in where blocks. This should be possible.

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

Partial definitions with copatterns should result in metavariables for the constructor arguments that are missing, not for the entire right-hand side.

Example:

zeros : Stream Nat
&hd zeros = Z

should desugar to

zeros : Stream Nat
zeros = MkStream Z ?tail

Question: what should the environment for the metavariable be?

Post Error Messages.