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.
[Prev in Thread]
[Next in Thread]
some further improvements,
Stefan Israelsson Tampe<=