[Agda-dev] Clauses and trailing implicit arguments

[Philipp Hausmann]

I'm now using the minimal arity of all clauses, and introduce additional 
lambdas whenever necessary. With the genuinely differing arities around, 
that's probably the best way of doing it anyhow.

Btw, thanks for the example, helped me catch one of my bugs already :)

Cheers,
Philipp



On 01/21/2015 08:51 AM, Andreas Abel wrote:
> In short, yes, this is the intended behavior.
>
> Of course, it seems weird that one clause has one more pattern 
> variable, and the other a lambda instead.  One could try to canonize 
> compiled clauses, e.g. that all the lambdas are turned into pattern 
> variables, or all the trailing pattern variables that are not matched 
> on are turned into lambdas.
>
> But be aware that there are cases the clauses genuinely have different 
> arities, e.g.
>
> Sum : Nat → Set
> Sum 0       = Nat
> Sum (suc n) = Nat → Sum n
>
> sum : (acc : Nat) (n : Nat) → Sum n
> sum acc 0         = acc
> sum acc (suc n) 0 = sum acc n
> sum acc (suc n) m = sum (m + acc) n
>
> Cheers,
> Andreas
>
> On 20.01.2015 01:39, Philipp Hausmann wrote:
>> Hi,
>>
>> I have a question about the internal Clauses/CompiledClauses
>> representation of Agda. I just learned that for certain corner-cases,
>> different clauses of the same function may take a different number of
>> arguments. This seems to break the Epic (and my own new) backend;
>> MAlonzo  isn't affected.
>>
>> It happens when an implicit argument is in trailing position, for 
>> example:
>>
>> data Nat : Set where
>>    Z : Nat
>>    S : Nat -> Nat
>>
>> f : (k : Nat) {l : Nat} -> Nat
>> f Z {l = q} = q
>> f (S a) = a
>>
>> This will yield the following clause patterns:
>> [[]r(ConP Test.Nat.Z(inductive)[] Nothing []),[]r{VarP "l"}] => length 2
>> [[]r(ConP Test.Nat.S(inductive)[] Nothing [[]r(a = VarP "a")])] => 
>> length 1
>>
>> And the following CompiledClauses:
>> case 0 of
>>    Test.Nat.Z -> done[[]r{"l"}] Var 0 []
>>    Test.Nat.S ->
>>      done[[]r("a")] Shared #44{Lam (ArgInfo {argInfoHiding = Hidden,
>> argInfoRelevance = Relevant, argInfoColors = []}) (Abs ".l" Var 1 [])}
>>
>> For the "f Z {l = q}", the clause has 2 arguments. For the "f (S a)"
>> case, the clause has only one argument. Instead, a new lambda is
>> introduced inside the clause itself.
>>
>> It seems to happen very rarely, the only two places I've seen it so far
>> in the stdlib are:
>> Data.Nat.DivMod._divMod_.dm
>> Data.Vec.Properties.sum-++-commuteFun
>>
>>
>> I think I can work around this in my own code, but I was wondering if
>> this is indeed the intended behavior?
>>
>> Cheers,
>> Philipp
>> _______________________________________________
>> Agda-dev mailing list
>> Agda-dev at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda-dev
>