[Agda] --no-pattern-matching

[Andreas Abel]

That is also an interesting option, maybe

   --shallow-pattern-matching

It is easy to just allow a single split per function definition. 
However, I guess you want to rule out hidden uses of K as well.  One way 
to get this is to disallow any pattern matching on inductive families as 
well.  You can then only match on inductive types (i.e., no indices). 
Equality would have to reside in a different module then, otherwise you 
cannot define its eliminator.

Peter Hancock might also like such an option...

Cheers,
Andreas

On 18.01.2014 00:47, Guillaume Brunerie wrote:
> Disallowing any kind of pattern matching is really extreme. As far as
> I’m concerned, I would be happy with an option limiting pattern
> matching to primitive recursion and where you can only match on one
> variable at the same time (so that any use of pattern matching would
> be equivalent to a single use of the corresponding eliminator).
>
> Guillaume
>
> 2014/1/18 Andreas Abel <andreas.abel at ifi.lmu.de>:
>> --no-pattern-matching is an extreme form of chastity, but it should not hard
>> to implement it.  If I understood correctly, you want Agda to slap your
>> fingers if you wrote a constructor pattern anywhere.
>>
>> The most principled way to implement this I can think of is to disallow any
>> kind of splitting in the checking of function left hand sides.
>>
>> Cheers,
>> Andreas
>>
>> On 17.01.2014 15:28, Matteo Acerbi wrote:
>>>
>>> every now and then I would like to forbid
>>> myself to use pattern matching at all, at least from inside a single
>>> file.
>>>
>>> I would like to have the possibility to get back to that file and make
>>> sure that I never used pattern matching in that code just by looking
>>> at the OPTIONS header.
>>>
>>> I think I would find a --no-pattern-matching option, which simply
>>> applied this restriction, but still allowed for importing modules
>>> whatever their options are, very convenient.
>>>
>>> For now I am just curious as to whether others are interested: would
>>> anyone else like such a --no-pattern-matching option?
>>
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/