DisplayLang is part of the Cochon UI

[GoogleCodeExporter]

While UI/Cochon contains the elaborator and distiller to and from the display 
language, it does not contain the definition of the display language. 
Presumably, the display language *is* part of the interface, not part of the 
theorem prover. 

So, as a first step, we need to move DisplayLang to UI/Cochon. In a second 
step, we would factorize code in UI/Lib.

Original issue reported on code.google.com by pedag...@gmail.com on 13 Jun 2010 at 10:47

[GoogleCodeExporter]

I am not sure I completely agree with this distinction, or rather I think there 
are two axes to consider. Certainly there is a question about which user 
interfaces to support: at the moment we only have the interactive theorem 
prover style Cochon, but we are also considering one using a text file (cf. 
Epigram 1 and Agda), and we could think about Proof General integration. 
However, I think the the high-level language issue is basically orthogonal, 
since we might want to use the same UI with different languages, or different 
UIs for the same language.

I suggest that we divide the parts up something like this, with dependencies 
mostly from top to bottom (except the appendix):

* Evidence language, including name supply
* Proof state, tactics and elaboration DSL (hopefully mostly HLL-independent)
* Features (should these contain language/UI specific code or not?)
* High-level languages (data structures, elaboration/distillation, parsing, 
pretty-printing)
   - Epigram
   - Haskell?
   - C++??
* User interfaces
   - Cochon
   - Text file thing
   - Proof General?
* Appendix containing miscellaneous rubbish

Thoughts?

Original comment by adamgundry on 15 Jun 2010 at 8:15

[GoogleCodeExporter]

Yeah, I think you got a point. In practice, this scheme doesn't work very well. 
I'm experimenting with another idea, will document it somewhere when I'm more 
convinced.

I roll back my change.

Original comment by pedag...@gmail.com on 28 Jul 2010 at 7:50

• Changed state: WontFix