search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
47 stars 7 forks source link

Elaboration.Wire: tellEntry invariant and schizophrenia #59

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
From my comment in Elaboration.Wire:

There is something fishy with this |tellEntry| and the invariant of "when 
applied on a definition, this definition must be the current entry".

In reality, there are two function, one defined on Parameters and called only 
on Parameters (in @ProofState.Edition.Navigation@) (call it 
|tellParameterEntry|) and one defined on Definitions and only called by itself 
and |tellCurrentEntry| in a safe wrapper enforcing this invariant (call it 
|tellDefinitionEntry|)

If we do the split, on one hand, the invariant will always be enforced. On the 
other hand, we get two functions with a partial pattern-matching. At least, 
with two explicitly named functions, one can hardly ignore that one is for 
Parameters and the other for Definitions.

It's up to debate.

Original issue reported on code.google.com by pedag...@gmail.com on 26 Aug 2010 at 5:14