umatch in (logic guile-log umatch) represent the lower level routines implemented in C code and loaded by that module. A matcher targeted to be used in code handling the unify variables is defined here as well.
umatch is a matcher that derives from (ice-9 match) with some extra features that relates to unifying variables. The usage is
(umatch [#:status s] [#:mode *] [#:status #f] [#:tag w] [#:name "anon"] [#:raw #f] (m ...) (pat ... code) ...) with pat utilizing: (p . q) _ , and set! get! #(...) = ` form ice-9/match plus ',' and the following symbols should not be used in fuctional position: or not cond ... ___ ,@ *** <> arguments $
’,’ can be used to quote a variable from the outside of the match
(set! s)
will define a setter s
that can be used in e.g. (<and> (s 1) ...)
, for <and>
refere to guile-log.
(get! g)
will define a getter g used with an argument representing the current state like e.g. (g S)
, with S
beeing define in the guile-log section.
[#:mode +] is used to set the kind of matcher that is initially valid it can be either of + ++ - * (see below for an explanation of these)
[#:tag w], that tag that related to backtracking to the next matcher. e.g.
(umatch #:tag next ('(1 2 3)) ((x y z) (if (number? x) (next) x)) ((x . l) l)) => '(2 3)
[#:name "anon"], this is used when outputting error messages
[#:raw #f], do not use this, this + #:mode + is the same as #:mode ++
[#:status #f], This is where the state variable should be it must be a variable which contains the current state at the entering of the matcher. This syntax symbol is resetted with new state at unifications and similar constructs which may enter new information onto implicit stack or explicit state info.
(m ...)
, is a sequence of elements to be matched in parallel
(pat ... code)
, if pat is a pattern to use to match a m the last form is the code to execute if all patterns matches.
The following feature is added to the ice-9 matchers
(+ p ...)
will match (p ...)
with the framework +
(+ + p)
will match p
with the framework +
The frameworks are,
(* (car cdr pair? null? equal? id))))) (+ (gp-car gp-cdr gp-pair!? gp-null!? gp-unify! gp-lookup)) (+r (gp-car gp-cdr gp-pair!? gp-null!? gp-unify!- gp-lookup)) (+r (gp-car gp-cdr gp-pair!? gp-null!? gp-unify!- gp-lookup)) (++ (gp-car gp-cdr gp-pair!? gp-null!? gp-unify-raw! gp-lookup)) (+r (gp-car gp-cdr gp-pair!? gp-null!? gp-unify!- gp-lookup)) (++r (gp-car gp-cdr gp-pair!? gp-null!? gp-unify-raw!- gp-lookup)) (- (gp-car gp-cdr gp-pair? gp-null? gp-m-unify! gp-lookup))
Toe explain more,
*
: the usual list framework
+
: (match (+) (1 v) (w 2))
matches and v=2,w=1
with a recurrence check e.g. if any self referenceing will appera in the matcher then the match fails. This is the safe way to do a unifying match.
++
: (match (+) (1 v) (w 2))
matches and v=2,w=1
with no recurrence check e.g. if any self referenceing will appera in the matcher then the match will not fails. This is the unsafe way to do a unifying match
because it may get into infinite recursion.
++
: (match (++) (1 v) (w 2))
matches and v=2,w=1
without
a recurrence check. Do this with care cause cyclisity is unsupportand and can
lead to a blowup of the stacks.
-
: (match (-) (1 (v = 2)) ((w = 1) 2))
matches unify
variable v = 2
at the start e.g. unify variable is looked up but never bounded.
Finally the r
modifications are primitive versions that are used
sometimes.
Also unquote directive is used in the matcher to signal an evaluation e.g. in
(umatch (x) ((a ,(+ z w)) a)) (+ z w)))
(+ z w)
will be first evaluated and then used in matching.
and
can be used and just as expected from ice-9 match. or
also works but any successful match will not backtrack.
in (logic guile-log umatch) a large set of unify constructs are loaded from a library defined in C, this api are,
The work is done with state objects containing appropriate stacks, rewind information and the assoq list of bindings. You will have the notion of a current ’gp’ state that is a fluid representing the current stack in use. Also there is a *current-state* fluid that holds the current assoq binding list/tree. You can create new stacks. The setup can be thread safe in the meaning that if you try to set a logic variable that is not associated to the supplied stack then a binding will be done by logically consing it to a datastructure that has the same functional behavior as an assoq list on the supplied state data and returned. This means that a large class (but certainly not all) of interop issues between multiple threads is solved. A state or stack datastructure will hold information on what thread-id it belongs and also have a unique id. The stack consists of actualy 4 stacks, one control stack (nc) one datastack (ns) and a stack of allocated cons cells (ncs) and one that holds the equivalent of fluids and guards. The control stack will contain unwind information, dynwinds and binding information. The cons stack is not used currently, it can be used to implement closure objects that is created from the stack in stead of the heap, we currently do not use this becuase other overhead is more significant currently e.g. the guile call overhead to C-funcitons. The dynstack is specaial in that its data is recreated at each wind. It represent the expensive winding that essentially originates from the guards and from the equivalent of fluids. Note that multiple reinstation of the other stacks are really cheap in that it does no consing, by allowing e.g. gp-fluid-set! we must pay with copying the stack at each wind, now by separating the small dynstack from the rest we get an important optimization.
*gp*
, fluid that holds the current gp-stack
*current-stack*
, fluid that holds the current assoq
(gp-make-stack id thread-id nc ns ncs)
Allocate a new state datastructure with identity number id
, thread identity number thread-id
and the sizes of the different stacks. Also it will be stupped so it can be used to unwind to e.g. w can reset the stack to the initial state calling gp-unwind
with it.
(gp-clear state)
, Reset the state to it’s initial setup.
A redo safe variable is a ordinary scheme variable object or fluid object that has the property that its state will be intelligently stored and retrieved under various premisses. Essentially if there is no mutattion further down the stack we can use the guard
version. Else between lguard and rguard the variable is guaranteed to have restorage property independent of mutation or not.
(gp-undo-safe-variable-guard var kind s
(gp-undo-safe-variable-lguard var kind s
(gp-undo-safe-variable-rguard var kind s
var
is a guile variable or fluid. We have a control parameter kind
which must not be a GP variable. and s containes the guile-log assoq state.
At rewind in context K
, the rules for restoring the state is as follows
kind = #t
, restore the state.
kind = #f
, do not restore.
K = #t
, restore the state.
K = #f
, do not restore.
kind, number and K, number
Then we will restore the state if K <= kind
.
Stack has a stack pointers to undo stacks a data stack and a cons stack and dynstack, by walking up and down these stacks we can recreate a state. The most lightweight way of winding is to use gp-newframe
and gp-unwind
where you can only go to a previous stack point stored by gp-newframe
and doing that the system forgets everything. This is fast and with no memory overhead. The other mode of operation using gp-store-state
,gp-restore-state
and gp-restore-wind
will go the full way and keep everything in memory until you drop and references to the returned state information and the gc can kick in at recollect the data. gp-store-state
will make a state data structure suitable to be for this mode of operation and gp-restore-state
will restore the infromation either backward or forward in time. Then the setup will be precisely as when the store operation was issued. To note here is that sometimes you would like to use the store and restore operation in a mode that follows a calculation like with the interleaving constructs for this operation it is very nifty to have global variables like if they lived on the heap to implement the logic. The downside is that with heap objects you typically cannot restore a state if you would like to do that. Guile log has a nifty framework to define variables that behaves just like these heap variables but with the difference that they are automagicaly restored when the user issues the gp-restore-state
. In order for this to work we use gp-restore-wind
internally when we store and restore information as we follow an algorithmic calculation path.
(gp-newframe s)
, returns the current frame incorporated in a state variable state of the stack in order to be able to backtrack.
(gp-unwind s)
, backtrack to state represented by s
that should have been returned by (gp-newframe s)
e.g. a state data structure.
The next two command is mirroring the two commands above. But for these we don’t impose the restriction to only go back in time, we can freely restore a state. Memory wise and performance this is heavier. But to note is that we do tree compression e.g. we try to reuse as much data as possible.
(gp-store-state s) -> state
, Gives a state that can be used to restore a state, this makes the unify stack act well together with call/cc constructions or using continuation closures e.g. it is possible to do continuations with these prolog stacks. Note that this is a very effective storage mechanism, basically the continuation is stored in a tree like structure.
(gp-restore-state state)
, Restore a state that is saved by gp-store-state
(gp-restore-wind state wind)
, the same as above, but they will not change the dynamic globals e.g. guarded variables to the old state depending an the algorithm described in teh beginning of this section.
For a guile variable or more prefereble (it is thread safe) for a fluid we can model it as a guile fluid but living on the guile-log stacks in stead. For this to work just use variable-ref, variable-set!, fluid-ref, fluid-set!
and
(gp-fluid-set var val)
This will bind var to val for the rest of the guile log stacks, e.g. similar to guile’s with-fluids.
(gp-var!)
, generate a new unify variable. E.g.
scheme(guile-user)> (define a (gp-var!)) scheme(guile-user)> (define b (gp-var!)) scheme(guile-user)> a $7 = <#0> scheme(guile-user)> b $8 = <#1> scheme(guile-user)> (gp-unify! a b) $9 = #t scheme(guile-user)> a $10 = <#1> scheme (guile-user)> b $11 = <#1> If executed under logical kanren assq feature then the variable is created on the heap, else it is created on the stack.
(gp->scm x s)
, Take a unify variable and a state and turn it into a
list representation, variables is transfered as is.
scheme(guile-user)> (u-set! a '(1 2)) scheme(guile-user)> a $17 = <#gp (1 2)> scheme(guile-user)> (gp->scm a) $18 = (1 2)
(gp-budy x)
, it is possible to pair variable if you do
(let ((x (gp-var!)) (y (gp-var!))) ...)
Then inside ... y = (gp-budy x)
.
(gp-var? x s)
, #t
if x
is a not bounded unify variable.
s
is the current state.
(gp-lookup x s)
If x
is a unify variable it tries to find the element it points at using state information in s
. If it is a unify variable that is returned, if it’s a scheme object that is returned If it’s a unify cons, that is returned.
(gp-var-number x)
, the variable number identifying a gp variable.
(gp-set! v a s) -> s
, set looked up unify variable v
to a
.
using state s
e.g. v
is looked up until the last variable pointing to a scheme variable. It may change the state and a new state is returned.
(gp-cons! x y)
, makes a unify cons variable out of x
and y
. To note here is that these conses are faster to allocate and they work well with rebounding later on and backtracks correctly.
(gp-pair? x s) -> s
, checks to see if x
is a pair or a unify pair
not a variable is will retrun false- Here the returned state is always the same
as the input. x
is assumed to have been looked up.
(gp-car x)
, takes the car of a unify pair or ordinary pair. x
is
assumed to have been looked up.
(gp-cdr x)
, takes the cdr of a unify pair or a ordinary pair x
is assumed to have been looked up.
(gp-unify! x y s) -> s or #f
, s
if x
and y
unifies with a recurrence check e.g. loop detection. #f
if they do not
unify (note that although this is false variables could have been unified so #f
is usually followed by a (gp-unwind Frame)
) e.g.
(let ((Fr (gp-newframe))) (if (gp-unify! x y) #t (begin (gp-unwind Fr) #f)))
(gp-unify-raw! x y s) -> s or #f
, the same as gp-unify!
but now loop detection e.g. we can end up in an infinite c-recursive loop and the stack will eventually be consumed and an error reported.
(gp-m-unify! x y s) -> s or #f
, the same as gp-unify!
but now variables are not bounded, if x is a variable then y must be the same variable and vice verse in order to unify.
Fluids functions does not change the stack parameters it is a buggy interface because the kind of stack sign should be in the state parameter that should be used as well as input.
(gp-make-var),(gp-make-var init)
makes guile log variable on the heap and an optional init value, init
.
(gp-var-set! v x)
set! a guile-log variable without backtracking !danger! do not use this anywhere else then a before a first gp-var-set
have
been issued on the variable.
(gp-var-set v x)
set a guile-log variable with backtracking the guile
stack is forced to be used to handle the backtracking.
(gp-var-ref v)
reference a guile-log var.
(gp-dynwind Redo Do Undo)
a similar tool as the dynwind construction but this one follows the current bank stack and not the call stack. Again
These two should only be used by experts.
(push-setup thunk)
, this will push a thunk
on the push stack, a setup is code that is run after the winding has ben done, typically this is used inside a dynwind.
(que-setup thunk)
, this will que thunk
on the setup que that is executed after the winding of the stack have been done.
N.B. the setup stack is executed before the setup que.
In kanren the interpretation of a variable is goverend in a state that behaves as an assq list. To find a value of a binding that list are searched for a binding. now this datastructure need not be a assq list, only sematically behave like it and that it need to be functional. The benifit is mainly that multiprocessor support is trivial by having such a feature. The intention is to execute the usage seamlessly in the background but uit can be beneficial to force the usage of them and therefore there is a public interface with primitives.
SCM (use-logical)
SCM (leave-logical)
To mark that the engine enters a region where it uses kanren logical structure
excecute the use-logical
function, and to leave use the other form.
These codes will add guards on the stack as well in order for it to work
seamlessly with regards to backtracking and state restorage.
(gp-stack-set! x v s) -> s
, forces the usage of the stack as
a method of doing an undoable set.
(gp-print x)
debug tool, prints out information of the internal representation of x
.
(gp-printer port x)
, the printer used to print unify variables
(gp-copy x)
Makes a copy of x
, but copy the references to variables and not the variables them self
(gp-get-stack)
, a debug tool. Yields the control stack containing undo information.