guile-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

some further improvements


From: Stefan Israelsson Tampe
Subject: some further improvements
Date: Wed, 21 Sep 2011 23:30:29 +0200

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



reply via email to

[Prev in Thread] Current Thread [Next in Thread]