some further improvements

some further improvements

[Stefan Israelsson Tampe]

[-- Attachment #1: Type: text/plain, Size: 3458 bytes --]

Dear guile developers.

I've been hacking along with on the "prolog" stuff and has introduced
several improvements
that code appart from squashing a bug from time to time.


This is a little headlight on the improvements:
1.  dynamic-wind is possible, that flows with the backtracker
One of the implementations, like kanren, uses a closure to represent the
next state
and pass it along the deduction chain. This has a serious drawback for
dynamic-wind
which only works if function returns backward through the stack, but this
deducer never does
that. It only keeps on tail-calling. Still it's possible to define a kind of
dynamic wind.

2.  A fluids interface that works for the above case as well.

3. A possibility to effectively store a state so that a continuation can be
taken with that state
later on, playing nice with the gc so that the gc will clean up (hopefully)
corectly.

4. kanrens all-interleave have been implemented

5. now you can stop a backtracker by storing state in variables and then
just return to the repl e.g. this gives
a lightweight continuation like mechanism.

to note here is that the stack that similarly like the stack in guile
containing dynamic wind and fluid objects has the
property of beeing on top focus when working with prolog variables. This
means that it is important to share
information between different continuations, and the implementation does so
hopefully correctly. I don't know if
guile uses the same tricks. To note though are that in guile-unify the
datastructure is a combination of an array (or soon
a linked array structure that can grow) and a tree of single linked nature
of conses on the heap. This means that when no
state is stored almost no consing is beeing done, only when a continuation
have been stored conses start to apear. In all this means that in a prover
one can design it to mostly do backtracking on the stack which is quick and
from time to time store
a state for later continuation meaning that the overhead of consing is not a
dramatic overhead.

6, a lot of bugs has been squashed for this version so that a lot of test
cases works.

7, a first order logic prover is under development and advanced proofs have
been done already
the hard-wired version is about three times slower then the other version
based on passed closures

8. solved the tagging issue so that unify variables are smobs on a stack
(mostly) and a general cleanup of the c-code
have been done


To note is that the  CPS version has the advantage of not hooking into the
guile gut's, but can instead be a
separate shared library that can be hooked into guile.

TODO:
1. squash bugs in the typechecking example
2. continue to work and improve the prover.
3. create a postpone framework using the stored state infrastructure.
4. make use of growable stacks, and restructure the code to allow stacks to
be more modular.
5. restructure the vm instructions to be fewer and also simplify the
sematics
6. try implement closeres that live on the stack but can be moved out to the
heap when nessesary
(this improvement will be important ones compilation speeds things up so
that closure creation becomes
the bottleneck, it's on the brink on beeing important for the fast version
of the code)
7. try to make use of memoization in the type solver to reduce complexities.

That's all for now. I could discuss things more in detail, but that will be
on demand.

O yes, I forgot, a big hurray for PEG and peval.

:-)

/Stefan

[-- Attachment #2: Type: text/html, Size: 3719 bytes --]