search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

Code Generation: Case can have two default clauses #2742

Open lenary opened 9 years ago

lenary commented 9 years ago

In the defunctionalised form of Prelude.Classes.Eq.== for Nat, there are two DDefaultCase clauses.

I think this violates the (unwritten) agreement that code generators will only get one default case in a case statement. This isn't an issue for my code generator, but I could see it becoming an issue for the C compiler, for example.

bamboo commented 9 years ago

It's the same situation with simplified expressions and the cil code generator has some rather fragile support for that.

It would be much nicer not to have to handle multiple SDefaultCase clauses as well.

melted commented 7 years ago

This probably occurs when SucCase is compiled into DefaultCase.