The Coq mailing list

[Jannis Limperg <jannis AT limperg.de>]

Hey Gregory,

having now spent a couple weekends with MirrorCore, I must say I like
its concepts a lot (and it's far more elegant than what I had cooked
up). If you don't mind, I have a couple of questions -- some conceptual,
some practical -- that I've not yet been able to answer by staring at
the examples. They all refer to version 1.0.2.


1. Had you considered using an untyped lambda calculus as the reflected
language? It seems that dealing with reflected types introduces some
additional complexity for MirrorCore users, so I was wondering whether
that might be an option.

2. While symbol representations can be composed nicely via RSym_sum and
friends, there seem to be no similar facilities for type
representations. Is this a conceptual problem or have these just not
been written yet?

3. Relatedly: When using the reification plugin, is it possible to split
a part of the reification logic off into a library? I imagine for
example a library which reifies logical formulae over user-specified
terms (with their own reification procedure), such that MirrorCore users
don't have to copy-paste the reification logic for [and, or, impl, ...]
into every project.

4. I'm slightly confused as to how exactly [reify_expr] works.
Specifically, what do the last two arguments (in double brackets) do?

5. I noticed a bug where parsing the [+=] in [Reify Pattern] commands
fails after evaluating a [Require MirrorCore.Reify.Reify] command twice
in the same Coqtop process. Do you have any idea what might be causing this?


Wrt the ideas expressed in my last mail: They were intended for a B.Sc.
thesis and thus much, much smaller in scope; and MirrorCore essentially
supersedes them. I'm currently looking into functionality I could
develop on top of MirrorCore for more specific purposes, but if you
happened to have an appropriately sized (and at least somewhat
interesting) piece of work you wanted done, I'd be very happy to look
into that as well.


Thanks a lot (for writing MirrorCore, and in advance for any answers to
my questions),
Jannis