[Agda] A frontend for the semiring solver using the reflection API

[Wojciech Jedynak]

2012/4/2 Ramana Kumar <ramana.kumar at gmail.com>:
> 2012/4/2 Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk>
>>
>> Hi Wojciech,
>>
>> you are correct this was one of the motivating examples but as far as I
>> know nobody  has yet implemented such an interface. Thank you very much!
>
>
> There is in fact another implementation for comparison here:
> https://github.com/xplat/agda-tactics/blob/master/Tactics/Nat/Semiring.agda

Thanks, I saw somebody mention this project in the irc logs last night
after I send the mail.

I made a quick test with two examples:

--------------------------
shuffle-test2 : (a b c : ℕ) → a + b + 2 + c + b ≡ 1 + b * 2 + (c + a) + 1
shuffle-test2 a b c = quoteGoal g in (unquote (solve-goal g))

postulate
 f : ℕ → ℕ

ex-4 : ∀ n m → f n + f m ≡ f m + f n
ex-4 n m = quoteGoal g in (unquote (solve-goal g))
---------------------------

xplat's version seems to be much more complete than mine, and his
version solves both goals, however the
first one takes a couple of seconds on my machine.
In comparison, my code is able to solve the first one quickly, but has
no chance to satisfy the second one.

The reason for this is that my version (by design) handles code
containing constants and universally quantified variables *only* - the
refls are in fact used to
make Agda prove that this conditions are met in a given example.
Xplat's version, on the other hand, seems to be done the way it should
be (sound and complete). I haven't read the code yet, but the natural
way to do this seems to
use a state monad so that we can calculate unique indexes for other
subterms [like (f n) in the example below], while traversing the
terms.
Since we use terms indexed by the number of free variables, this will
probably require a lot of term rebuilding just for the sake of
making the code typecheck. It would be interesting to see if the
unquote construction results in any performance penalty.

Anyways, I'll redo my library to achieve completeness, possibly
without using unqoute, and report back in a couple of days.

Greetings,
Wojciech