[Agda] --no-pattern-matching

[Andreas Abel]

Matteo,

here you go.

Sat Jan 18 01:16:18 CET 2014  Andreas Abel <andreas.abel at ifi.lmu.de>
   * New option --no-pattern-matching.  Disables any kind of splits in 
lhs checking.

{-# OPTIONS --no-pattern-matching #-}

data Unit : Set where
   unit : Unit

fail : Unit → Set
fail unit = Unit
-- Expected error: Pattern matching is disabled

Have fun,
Andreas

On 18.01.2014 00:37, Andreas Abel wrote:
> --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/