K-user mailing list

[Andrej Tokarčík <andrejtokarcik AT gmail.com>]

Hi Brandon,

On Mon, Aug 10, 2015 at 8:16 PM, Moore, Brandon Michael
<bmmoore AT illinois.edu>
 wrote:
> The incomplete features probably prevented you from compiling any of the 
> standard library or larger programs, unfortunately.

Indeed, the most obvious blocker is the lack of module system support,
which should however be not that hard to add. Missing `with' is a
major shortcoming from the perspective of practical Agda programming,
too.

> Did you notice any problems from relying on K's unification module rather 
> than replicating Agda's meta inference exactly?

Yes. Since the current implementation introduces some simplifications
-- unification.k was chosen to speed up the implementation process
after all -- I encountered programs whose metavariables could not be
solved by my semantics although they were solved by the official
typechecker. If I recall correctly, tests/beyond/Vec.agda in the Git
repo should be an example of this. (I can't test it at the moment, the
semantics is very resource-intensive).

Still, it should be checked in particular cases whether such behaviour
is not actually caused by a bug in the extensions around K's
unification module themselves instead of the fact that K's module is
taken advantage of.

> Would you like us to include this semantics in the official K repository at 
> https://github.com/kframework ?

It is no problem by me, you can certainly use it, although I am not
sure whether the (uncommented) code would be demonstrative of your
standards. ;-)

I just pushed the MIT license...

> [...]

Kind regards,
Andrej