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

2011-07-17 Thread Alexander Burger
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)

2011-07-17 Thread Edwin Eyan Moragas
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