### Re: doProve (was Re: Ninety-Nine Lisp Problems: pilog)

```Hi Edwin,

now this got me interested. does Alex, or anybody else, have a
picolisp version of the doProve() and doUnify() c functions?

Hmm, after some searching, it seems I have only a fragment of some
initial version, when I experimented in Lisp before I rewrote the time
critical parts in C.

There is 'prove', but 'unify' seems missing. Anway:

(de prove (Q)
(when Q
(use (N NL Alt Tp1 Tp2 Env E)
(back)
(while (or Tp1 Tp2)
(cond
(Alt
(ifn
(setq E
(unify (car NL) (cdar Tp1) N (caar Alt) Env) )
(or (setq Alt (cdr Alt)) (back))
(when (cdr Alt)
(push Q
(cons N NL (cdr Alt) Tp1 Tp2 Env) ) )
(push 'NL N)
(inc 'N)
(setq
Tp2 (cons (cdr Tp1) Tp2)
Tp1 (cdar Alt)
Env E )
(off Alt) ) )
((not Tp1)
(setq  Tp1 (pop 'Tp2)  NL (cdr NL)) )
((=T (car Tp1))
(while (= (caaar Q) (car NL))
(pop Q) )
(pop 'Tp1) )
((num? (caar Tp1))
(setq E (eval (cdar Tp1)))
(push 'NL (get NL (caar Tp1)))
(setq  Tp2 (cons (cdr Tp1) Tp2)  Tp1 E) )
((pat? (caar Tp1))
(if
(and
(eval (cdar Tp1))
(unify (car NL) (caar Tp1) (car NL) @ Env) )
(setq  Tp1 (cdr Tp1)  Env @)
(back) ) )
((not (setq Alt (get (caar Tp1) T)))
(back) ) ) )
(let R NIL
(for (L Env (cdr L) (cdr L))
(when (=0 (caaar L))
(push 'R
(cons (cdaar L) (lookup 0 (cdaar L) Env)) ) ) )
(or R (bool Env)) ) ) ) )

(de back ()
(setq
Env (pop Q)
N (pop 'Env)
NL (pop 'Env)
Alt (pop 'Env)
Tp1 (pop 'Env)
Tp2 (pop 'Env) ) )

(de - X
(lookup
(get NL (or (cadr X) 1))
(car X)
Env ) )

(de unifyEnv (Lst)
(setq Env
(unify (cadr NL) Lst (car NL) Lst Env) ) )

Cheers,
- Alex
--
UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe

```

### Re: doProve (was Re: Ninety-Nine Lisp Problems: pilog)

```Hi Alex,

On Sun, Jul 17, 2011 at 3:55 PM, Alexander Burger a...@software-lab.de wrote:

Hmm, after some searching, it seems I have only a fragment of some
initial version, when I experimented in Lisp before I rewrote the time
critical parts in C.

There is 'prove', but 'unify' seems missing. Anway:

thanks for this! i'll find this useful for my personal research. :)

cheers

/e

(de prove (Q)
(when Q
(use (N NL Alt Tp1 Tp2 Env E)
(back)
(while (or Tp1 Tp2)
(cond
(Alt
(ifn
(setq E
(unify (car NL) (cdar Tp1) N (caar Alt) Env)
)
(or (setq Alt (cdr Alt)) (back))
(when (cdr Alt)
(push Q
(cons N NL (cdr Alt) Tp1 Tp2 Env) ) )
(push 'NL N)
(inc 'N)
(setq
Tp2 (cons (cdr Tp1) Tp2)
Tp1 (cdar Alt)
Env E )
(off Alt) ) )
((not Tp1)
(setq  Tp1 (pop 'Tp2)  NL (cdr NL)) )
((=T (car Tp1))
(while (= (caaar Q) (car NL))
(pop Q) )
(pop 'Tp1) )
((num? (caar Tp1))
(setq E (eval (cdar Tp1)))
(push 'NL (get NL (caar Tp1)))
(setq  Tp2 (cons (cdr Tp1) Tp2)  Tp1 E) )
((pat? (caar Tp1))
(if
(and
(eval (cdar Tp1))
(unify (car NL) (caar Tp1) (car NL) @ Env) )
(setq  Tp1 (cdr Tp1)  Env @)
(back) ) )
((not (setq Alt (get (caar Tp1) T)))
(back) ) ) )
(let R NIL
(for (L Env (cdr L) (cdr L))
(when (=0 (caaar L))
(push 'R
(cons (cdaar L) (lookup 0 (cdaar L) Env)) ) ) )
(or R (bool Env)) ) ) ) )

(de back ()
(setq
Env (pop Q)
N (pop 'Env)
NL (pop 'Env)
Alt (pop 'Env)
Tp1 (pop 'Env)
Tp2 (pop 'Env) ) )

(de - X
(lookup
(get NL (or (cadr X) 1))
(car X)
Env ) )

(de unifyEnv (Lst)
(setq Env
(unify (cadr NL) Lst (car NL) Lst Env) ) )

Cheers,
- Alex
--
UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe

--
UNSUBSCRIBE: mailto:picolisp@software-lab.de?subject=Unsubscribe

```