Hacker News new | ask | show | jobs
by Animats 3432 days ago
See the link listed above: https://github.com/John-Nagle/pasv/blob/master/src/CPC4/z.li...

I put all the code on Github. The oldest version of each file is exactly what ran in 1986.

The code is delicate. It's a theorem prover, and there's much manipulation of complex data structures, with little explanation of what's going on. The overall theory is documented; this is the original Oppen-Nelson simplifier and there are published papers. But the code has few comments.

1 comments

getenode is only called in a few places, and each call looks like:

  (getenode znode)
i.e. getenode is only called on znodes. The definition of makeznode is:

  (defun makeznode (node)
         (prog (l znode)
               (setq l (list (list '(1 . 1) node)))
               (xzfield node (list l node nil))
               (setq znode (tellz l node))
               (or (null znode) (eq znode node) (break makeznode))
               (return l)))
So it seems like getenode is called on a regular list whose structure looks like

  (list (list '(1 . 1) node))
Assuming "node" is an enode, the way to access it would be (cadar znode), not (cdar znode). Try changing the definition of getenode to

  (defun getenode (l) (cadar l))
and see if it runs.
I thought that way at first. But the program breaks when (getenode znode) is called on an item of type "node", not a list. This happens when (interntimes) takes the path which ends

    (or (setq znode (tellz l node)) (return t))
    (or (eq node (getenode znode)) (zmerge node (getenode znode)))))
and (tellz) has taken the path which ends (return (baserowz* i)). "baserow*" is an array which contains links to "node" items, not list cells. What "z.lisp" and "ze.lisp" are doing, by the way, is solving systems of linear inequalities by using linear programming on a sparse matrix.

Also, see

    (defun isznode (x) (and (hunkp x) (= (hunksize x) 8))) ; original

    (defun isznode (x) (equal (type-of x) 'node))   ; CL version
which indicate that znodes are hunks/structures, not lists. This is inconsistent, yet somehow it used to work.

(If you want to talk privately about this, I'm at "nagle@animats.com". Too much detail for HN.)

or abuse, ouch!

   (unless (setq znode (tellz l node))
     (return t))