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

Reply via email to