V4.lsp

; Mini-PrologII
; boot.lsp
;

(defun mini-PrologII ()         ; to run it
  (banner)
  (format t "~A~%" (load "mlg.Start"))
  (myloop (read_prompt)))

(defun read_prompt ()
  (terpri)
  (format t "| ?- ")
  (read_code_tail))

(defun banner ()
  (dotimes (i 2) (terpri))
  (format t "Mini-PrologII~%")
  (dotimes (i 2) (terpri)))

(defun l ()
  (format t "Back to Mini-PrologII top-level~%")
  (myloop (read_prompt)))
; mini-Cprolog & mini-PrologII
; cparser.lsp
;

(defvar *lvarloc nil)                   ; list of local vars
(defvar *lvarglob nil)                  ; list of global vars
(set-macro-character #\% (get-macro-character #\;))

(defun rch ()                           ; skips Newline
  (do ((ch (read-char) (read-char)))
      ((char/= ch #\Newline) ch)))
(defun rchnsep ()                       ; skips Newline and Space
  (do ((ch (rch) (rch)))
      ((char/= ch #\space) ch)))

(defun special (ch) (char= ch '#\_))
(defun alphanum (ch)                    ; symbol normal constituant
  (or (alphanumericp ch) (special ch)))
(defun valdigit (ch) (digit-char-p ch))

(defun read_number (ch)                 ; next integer
  (do ((v (valdigit ch) (+ (* v 10) (valdigit (read-char)))))
      ((not (digit-char-p (peek-char))) v)))

(defun implode (lch) (intern (map 'string #'identity lch)))

(defun read_atom (ch)                   ; next normal symbol
  (do ((lch (list ch) (push (read-char) lch)))
      ((not (alphanum (peek-char))) (implode (reverse lch)))))

(defun read_at (ch)                     ; next special symbol
  (do ((lch (list ch) (push (read-char) lch)))
      ((char= (peek-char) #\') (read-char) (implode (reverse lch)))))

(defun read_string (ch)                 ; Prolog list of ascii codes
  (do ((lch (list (char-int ch)) (push (char-int (read-char)) lch)))
      ((char= (peek-char) #\") (read-char) (do_l (reverse lch)))))

(defun read_var (ch n)                  ; next variable
  (status (read_atom ch) n))

(defun status (nom n)                   ; n is the term's depth
  (if (= n 1)                           ; local if not yet global
      (unless (member nom *lvarglob) (pushnew nom *lvarloc))
    (progn (if (member nom *lvarloc)    ; else global
               (setq *lvarloc (delete nom *lvarloc)))
           (pushnew nom *lvarglob)))
  nom)

(defun read_simple (ch n)               ; next simple term
  (cond
   ((or (upper-case-p ch) (special ch)) (read_var ch n))
   ((digit-char-p ch) (read_number ch))
   ((char= ch #\") (read_string (read-char)))
   ((char= ch #\') (read_at (read-char)))
   (t (read_atom ch))))

(defun read_fct (ch n)                  ; next functional term
  (let ((fct (read_simple ch n)) (c (rchnsep)))
    (if (char= c #\()                   ; reads its arguments
        (let ((la (read_args (rchnsep) (1+ n))))
          (cons (list fct (length la)) la)) ; adds its descriptor
      (progn (unread-char c) fct))))    ; else atom

(defun read_args (ch n)                 ; args of a functional term
  (let ((arg (read_term ch n)))
    (if (char= (rchnsep) #\,)
        (cons arg (read_args (rchnsep) n))
      (list arg))))

(defun read_list (ch n)                 ; next list
  (if (char= ch #\])                    ; ending with the empty list
      ()
    (let ((te (read_term ch n)))        ; gets the head
      (case (rchnsep)
            (#\, (list '(\.  2) te (read_list (rchnsep) n)))
            (#\| (prog1                 ; dotted pair
                     (list '(\. 2) te (read_term (rchnsep) n))
                   (rchnsep)))
            (#\] (list '(\. 2) te nil))))))

(defun read_term (ch n)                 ; next term
  (if (char= ch #\[) (read_list (rchnsep) (1+ n)) (read_fct ch n)))

(defun read_tail (ch)                   ; read the body of a rule
  (let ((tete (read_pred ch)))          ; gets the first goal
    (if (char= (rchnsep) #\.)
        (list tete)
      (cons tete (read_tail (rchnsep))))))

(defun read_clause (ch)                 ; reads a clause
  (let ((tete (read_pred ch)))
    (if (char= (rchnsep) #\.)
        (list tete)
      (progn (read-char) (cons tete (read_tail (rchnsep)))))))

(defun c (l)                            ; codes once read
  (if (atom l)
      (if (member l *lvarloc)
          (cons 'L (position l *lvarloc))
        (if (member l *lvarglob) (cons 'G (position l *lvarglob)) l))
    (if (eq (car l) '!)                 ; the cut with its intern
        (list '! (length *lvarloc))     ; argument
      (cons (c (car l)) (c (cdr l))))))
; mini-PrologII
; parser.lsp
;

(defun read_code_cl ()          ; to read and code a clause
  (let ((*lvarloc ()) (*lvarglob ()))
    (let ((x (read_clause (rchnsep))))
      (maj_locglob (car x) (car (last x)))
      (cons             ; number of local and global
       (cons (length *lvarloc) (length *lvarglob)) ; vars
       (c x)))))

(defun read_code_tail ()        ; idem for a query
  (setq *lvarloc () *lvarglob ())
  (let ((x (read_tail (rchnsep))))
    (cons
     (cons (length *lvarloc) (length *lvarglob))
     (append (c x) (list '(|true|))))))

(defun read_pred (ch)           ; to read a literal
  (let ((nom (read_atom ch)) (c (rchnsep)))
    (if (char= c #\()
    (cons nom
          (read_args (rchnsep)
             (if (member nom '(|dif| |freeze|))
                 2      ; a var occurring in a dif
               1)))     ; or in a freeze is global
      (progn (unread-char c) (list nom)))))

(defun unsafe? (x h q)          ; occurs in the body
  (and (member x q) (not (member x h)))) ; but not in the head

(defun maj_locglob (h q)        ; to classify the variables
  (mapc #'(lambda (x)
        (when (unsafe? x h q)
          (setq *lvarloc (delete x *lvarloc))
          (push x *lvarglob)))
    *lvarloc))
; mini-PrologII
; blocks.lsp
;

; I. Registers
;
(defconstant BottomFR 1)        ; bottom of frozen goals stack
(defconstant BottomG 3000)      ; bottom of global stack
(defconstant BottomL 6000)      ; bottom of local stack
(defconstant BottomTR 10000)        ; bottom of trail
(defconstant A 12000)           ; max of trail

(defvar Mem (make-array 12050 :initial-element 0))
(defvar FR)             ; top of frozen goals stack
(defvar TR)             ; top of trail
(defvar L)              ; top of local stack
(defvar G)              ; top of global stack
(defvar CP)             ; current continuation
(defvar CL)
(defvar Cut_pt)             ; specific cut
(defvar FRCP)               ; awakened goals
(defvar BL)             ; backtracking registers
(defvar BG)
(defvar PC)             ; currents goal and its
(defvar PCE)                ; environments
(defvar PCG)
(defvar Duboulot)

(defmacro vset (v i x) `(setf (svref ,v ,i) ,x))

; II. Local Stack
;
;deterministic block [CL CP G Cut E]
;
(defmacro CL (b) `(svref Mem ,b))
(defmacro CP (b) `(svref Mem (1+ ,b)))
(defmacro G (b) `(svref Mem (+ ,b 2)))
(defmacro Cut (b) `(svref Mem (+ ,b 3)))
(defmacro E (b) `(+ ,b 4))

(defmacro push_cont ()          ; saves continuation
  `(progn (vset Mem L CL) (vset Mem (1+ L) CP)))

(defmacro push_E (n)            ; allocates local env
  `(let ((top (+ L 4 ,n)))
     (if (>= top BottomTR)
     (throw 'debord (print "Local Stack Overflow")))
     (vset Mem (+ L 3) Cut_pt)
     (dotimes (i ,n top)        ; n local free variables
          (vset Mem (decf top) (cons 'LIBRE BottomG)))))

(defmacro maj_L (nl)            ; updates top of local stack
  `(incf L (+ 4 ,nl)))


;choice-point : [a1 .. an A FR BCP BCL BG BL BP TR]
;
(defmacro TR (b) `(svref Mem (1- ,b)))
(defmacro BP (b) `(svref Mem (- ,b 2)))
(defmacro BL (b) `(svref Mem (- ,b 3)))
(defmacro BG (b) `(svref Mem (- ,b 4)))
(defmacro BCL (b) `(svref Mem (- ,b 5)))
(defmacro BCP (b) `(svref Mem (- ,b 6)))
(defmacro FR (b) `(svref Mem (- ,b 7)))
(defmacro A (b) `(svref Mem (- ,b 8)))

(defun save_args ()         ; save args of current goal
  (dotimes (i (svref Mem A) (vset Mem (incf L i) i))
       (vset Mem (+ L i) (svref Mem (+ A i 1)))))

(defun push_choix ()            ; allocates a choice point
  (save_args)               ; goal args
  (vset Mem (incf L) FR)        ; top of f.g. stack
  (vset Mem (incf L) CP)        ; continuation
  (vset Mem (incf L) CL)
  (vset Mem (incf L) G)         ; top of global stack
  (vset Mem (incf L) BL)        ; last choice point
  (vset Mem (incf L 2) TR)      ; top of trail
  (setq BL (incf L) BG G))      ; new last choice point

(defun push_bpr (reste) (vset Mem (- BL 2) reste))

(defmacro size_C (b) `(+ 8 (A ,b)))

(defun pop_choix ()
  (setq L (- BL (size_C BL))        ; pops the block
    BL (BL BL)          ; updates backtrack reg.
    BG (if (zerop BL) BottomG (BG BL))))

; III. Global Stack
;
(defmacro push_G (n)
  `(let ((top (+ G ,n)))
     (if (>= top BottomL)
     (throw 'debord (print "Global Stack Overflow")))
     (dotimes (i ,n (vset Mem (+ L 2) G)) ; n free global vars
          (vset Mem (decf top) (cons 'LIBRE BottomG)))))
(defmacro maj_G (n) `(incf G ,n))

;IV. Trail
;
(defmacro fgblock (x) `(cdr (svref Mem ,x)))

(defun pushtrail (x)
  (if (>= TR A) (throw 'debord (print "Trail Overflow")))
  (vset Mem TR x)
  (incf TR))

(defun poptrail (top)
  (do () ((= TR top))
      (let ((x (svref Mem (decf TR))))
    (if (numberp x)         ; classical var else frozen
        (vset Mem x (cons 'LIBRE BottomG))
      (vset Mem (car x) (cons 'LIBRE (cdr x)))))))

; V. Frozen Goals Stack
;
(defmacro FGvar (x) `(svref Mem ,x))
(defmacro FGtail (x) `(svref Mem (1+ ,x)))
(defmacro FGgoal (x) `(svref Mem (+ 2 ,x)))
(defmacro FGenv (x) `(svref Mem (+ 3 ,x)))
(defmacro frozen? (x) `(< (fgblock ,x) BottomG))

(defmacro push_fg (v b eb r)        ; allocates a frozen block
  `(if (>= (+ FR 3) BottomG)
       (throw 'debord (print "Frozen Goals Stack Overflow"))
     (progn (vset Mem FR ,v)
        (vset Mem (incf FR) ,r)
        (vset Mem (incf FR) ,b)
        (vset Mem (incf FR) ,eb)
        (incf FR))))
; miniCprolog & Mini-PrologII
; cutili.lsp
;

(defmacro nloc (c) `(caar ,c))          ; number of local vars
(defmacro nglob (c) `(cdar ,c))         ; number of global vars
(defmacro head (c) `(cadr ,c))          ; head of a clause
(defmacro tail (c) `(cddr ,c))          ; body of a clause
(defmacro pred (g) `(car ,g))           ; predicate symbol
(defmacro largs (g) `(cdr ,g))          ; list of arguments

(defmacro functor (des) `(car ,des))
(defmacro arity (des) `(cadr ,des))
(defmacro des (te) `(car ,te))          ; functor/arity
(defmacro var? (v) `(and (consp ,v) (numberp (cdr ,v))))
(defmacro list? (x) `(eq (functor (des ,x)) '\.))

(defmacro user? (g)                     ; user defined predicate
  `(get (pred ,g) 'def))
(defmacro builtin? (g)                  ; builtin predicate
  `(get (pred ,g) 'evaluable))
(defmacro def_of (g)                    ; gets the subset of clauses
  `(get (pred ,g)                       ; depending on the nature of
        (if (largs ,g)                  ; the first arg of goal PC
            (nature (car (ultimate (car (largs ,g)) PCE PCG)))
          'def)))

(defun nature (te)                      ; determines the associated
  (cond                                 ; subset according to
   ((var? te) 'def)                     ; clause indexing
   ((null te) 'empty)
   ((atom te) 'atom)
   ((list? te) 'list)
   (t 'fonct)))

(defun add_cl (pred c ind)              ; adds a clause to the end
  (setf (get pred ind) (append (get pred ind) (list c))))

(set-macro-character                    ; to automatically read,
 #\$                                    ; code and index
 #'(lambda (stream char)
     (let* ( (*standard-input* stream) (c (read_code_cl)))
       (add_cl (pred (head c)) c 'def)  ; always in the var subset
       (if (largs (head c))
           (let ((b (nature (car (largs (head c))))))
             (if (eq b 'def)            ; first arg is a variable
                 (mapc                  ; add c to all the subsets
                  #' (lambda (x) (add_cl (pred (head c)) c x))
                  '(atom empty list fonct))
               (add_cl (pred (head c)) c b))))) ; add to only one subset
     (values)))

(defun answer ()                        ; prints the values of vars
  (printvar)                            ; occurring in the query
  (if (zerop BL)                        ; no more choice point
      (setq Duboulot nil)
    (if (and (princ "More : ")          ; asks the user
             (string= (read-line) ";")) ; if necessary
        (backtrack)                     ; forces backtracking
      (setq Duboulot nil))))

(defun printvar ()
  (if (and (null *lvarloc)              ; ground query ?
           (null *lvarglob))
      (format t "Yes ~%")               ; success
    (let ((nl -1) (ng -1))
      (mapc                             ; first, local variables
       #' (lambda (x)
            (format t "~A = " x)
            (write1 (ult (cons 'L (incf nl)) (E BottomL))) (terpri))
       *lvarloc)
      (mapc                             ; then global variables
       #' (lambda (x)
            (format t "~A = " x)
            (write1 (ult (cons 'G (incf ng)) BottomG)) (terpri))
       *lvarglob))))
; mini-PrologII
; unify.lsp
;

(defmacro bind (x sq e xt)      ; binds x to (sq,e)
  `(progn (if (or (and (> ,x BottomL) (< ,x BL)) (< ,x BG))
          (pushtrail ,xt))      ; if post-bound trail it
      (rplaca (svref Mem ,x) ,sq)
      (rplacd (svref Mem ,x) ,e)))

(defun bindte (x sq e)          ; binds x to (sq,e)
  (if (frozen? x)
      (let ((y (fgblock x)))
    (push y FRCP)           ; awakes the delayed goals
    (bind x sq e (cons x y)))   ; to trail the old value
    (bind x sq e x)))

(defun bindfg (x b eb r)        ; binds x to the frozen goal b
  (bind x 'LIBRE FR (if (frozen? x) (cons x r) x))
  (push_fg x b eb r))           ; allocates a new frozen block

(defun unify_with (largs el eg)     ; unifies head of clause
  (catch 'impossible            ; with registers Ai
    (dotimes (i (svref Mem A))
         (unif
          (let ((te (svref Mem (+ A 1 i)))) (val (car te) (cdr te)))
          (ultimate (pop largs) el eg)))))

; mini-Cprolog & mini-PrologII
; cunify.lsp
;
(defmacro adr (v e) `(+ (cdr ,v) ,e))
(defmacro value (v e) `(svref Mem (adr ,v ,e)))

(defun ult (v e)                        ; dereferences variable v
  (let ((te (value v e)))               ; in environment e
    (cond
     ((eq (car te) 'LIBRE) (cons v e))  ; if unbound, itself
     ((var? (car te)) (ult (car te) (cdr te)))
     ( te))))                           ; its value

(defun val (x e)                        ; generalises to a term
  (if (var? x) (ult x e) (cons x e)))

(defun ultimate (x el eg)               ; idem but selects env
  (if (var? x)
      (if (eq (car x) 'L) (ult x el) (ult x eg))
    (cons x eg)))

(defmacro bindv (x ex y ey)             ; L2 Binding
  `(let ((ax (adr ,x ,ex)) (ay (adr ,y ,ey)))
     (if (< ax ay)                      ; the younger one is always
         (bindte ay ,x ,ex)             ; bound to the senior one
       (bindte ax ,y ,ey))))

(defun unif (t1 t2)                     ; unify two terms t1 and t2
  (let ((x (car t1)) (ex (cdr t1)) (y (car t2)) (ey (cdr t2)))
    (cond
     ((var? y)
      (if (var? x)                      ; two variables
          (if (= (adr x ex) (adr y ey)) t (bindv y ey x ex))
        (bindte (adr y ey) x ex)))      ; binds y
     ((var? x) (bindte (adr x ex) y ey))
     ((and (atom x) (atom y))           ; two constants
      (if (eql x y) t (throw 'impossible 'fail)))
     ((or (atom x) (atom y)) (throw 'impossible 'fail))
     ( (let ((dx (pop x)) (dy (pop y))) ; two structured terms
         (if (and (eq (functor dx) (functor dy))
                  (= (arity dx) (arity dy)))
             (do () ((null x))          ; same functor and arity
                 (unif (val (pop x) ex) (val (pop y) ey)))
           (throw 'impossible 'fail)))))))
; mini-PrologII
; resol.lsp
;

(defun forward ()
  (do () ((null Duboulot) (format t "no More~%"))
      (cond ((and (null CP)     ; empty continuation
          (null FRCP))      ; no awaken goals
         (answer))
        ((load_PC)          ; selects first goal
         (cond
          ((user? PC)       ; user defined
           (let ((d (def_of PC)))   ; associated set of clauses
         (if d (pr2 d) (backtrack))))
          ((builtin? PC)        ; builtin
           (if (eq (apply (car PC) (cdr PC)) 'fail)
           (backtrack)      ; evaluation fails
         (cont_eval)))
          ((backtrack)))))))    ; undefined predicate

(defun load_A (largs el eg)     ; loads Ai registers with
  (dotimes (i (length largs) (vset Mem A i)) ; goal's args
       (vset Mem (+ A i 1) (ultimate (pop largs) el eg))))

(defun load_PC ()
  (if FRCP
      (let ((x ()))
    (do ()              ; sorts the goals depending on
        ((null FRCP))       ; their freezing times
        (setq x (add_fg (pop FRCP) x)))
    (do ()              ; allocates blocks in the
        ((null x))          ; corresponding order
        (create_block (abs (pop x))))))
  (setq PC (pop CP) PCE (E CL) PCG (G CL) Cut_pt BL))

(defun other_fg (b r)
  (if (< (FGtail b) BottomG) (add_fg (FGtail b) r) r))

(defun add_fg (b r)         ; sorts the various awakened
  (let ((b1 (if (numberp (FGgoal b)) (FGgoal b) b))) ; goals
    (if (eq (pred (FGgoal b1)) '|dif|)  ; dif first
    (insert (- b1) (other_fg b r))
      (let* ((v (svref Mem (FGvar b1))) ; it is a freeze
         (te (val (car v) (cdr v))))
    (if (var? (car te))     ; the var is still unbound
        (let ((y (adr (car te) (cdr te))))
          (bindfg y b1 nil (fgblock y)) ; delaying is perpetuated
          (other_fg b r))
      (insert b1 (other_fg b r))))))) ; insert the goal

(defun insert (b l)         ; sorts the goals according to
  (if (or (null l) (> b (car l)))   ; their freezing times
      (cons b l)
    (cons (car l) (insert b (cdr l)))))

(defmacro dec_goal (x)
  `(if (atom ,x) (list ,x) (cons (caar ,x) (cdr ,x))))

(defun create_block (b)         ; block for an awakened goal
  (push_cont)               ; saves current continuation
  (vset Mem (+ L 2) (FGenv b))      ; its global env
  (vset Mem (+ L 3) Cut_pt)     ; the corresponding cut point
  (setq CP (list (FGgoal b)) CL L)  ; new continuation
  (maj_L 0))                ; ends the block

(defun pr2 (paq)            ; proves PC
  (load_A (largs PC) PCE PCG)       ; loads its arguments
  (if CP
      (pr paq)
    (progn              ; if last call and no interm.
      (if (<= BL CL) (setq L CL))   ; choice point then LCO
      (setq CP (CP CL) CL (CL CL))  ; next continuation
      (pr paq))))

(defun cont_eval ()
  (unless CP (if (<= BL CL) (setq L CL)) (setq CP (CP CL) CL (CL CL))))

(defun pr (paq)
  (if (cdr paq)             ; alloc. choice point
      (progn (push_choix) (pr_choice paq))
    (pr_det (car paq))))        ; else deterministic

(defun pr_det (c)
  (if (eq (unify_with           ; first tries to unify
       (largs (head c))
       (push_E (nloc c))
       (push_G (nglob c)))
          'fail)
      (backtrack)
    (progn              ; success
      (maj_G (nglob c))         ; terminates global env
      (when (tail c)            ; c is rule
        (push_cont) saves current cont.
        (setq CP (tail c) CL L) ; new one
        (maj_L (nloc c))))))    ; terminates local block

(defun pr_choice (paq)
  (let* ((resu (shallow_backtrack paq)) (c (car resu)) (r (cdr resu)))
    (cond ((null r)         ; only one candidate remains
       (pop_choix)          ; pops the rerun part
       (pr_det c))          ; proof is now deterministic
      ( (push_bpr r)
        (maj_G (nglob c))
        (when (tail c)      ; c is a rule
          (push_cont)       ; saves current cont.
          (setq CP (tail c) CL L) ; new one
          (maj_L (nloc c))))))) ; terminates local block

(defun shallow_backtrack (paq)      ; looks for a first success
  (if (and (cdr paq)            ; more than one candidate
       (eq (unify_with      ; and unification fails
        (largs (head (car paq)))
        (push_E (nloc (car paq)))
        (push_G (nglob (car paq))))
           'fail))
      (progn
    (setq FRCP nil FR (FR BL))  ; restores registers
    (poptrail (TR BL))      ; restores env
    (shallow_backtrack (cdr paq)))
    paq))

(defun backtrack ()
  (if (zerop BL)            ; no more choice points
      (setq Duboulot nil)       ; restores registers
    (progn (setq L BL G BG FR (FR L) FRCP nil Cut_pt (BL BL)
         CP (BCP L) CL (BCL L) Cut_pt (BL BL))
       (load_A2)
       (poptrail (TR BL))       ; restores env
       (pr_choice (BP L)))))    ; relaunch the proof

(defun load_A2 ()           ; restores Ai registers
  (let ((deb (- L (size_C L))))
    (dotimes (i (A L) (vset Mem A i))
         (vset Mem (+ A i 1) (svref Mem (+ deb i))))))

(defun myloop (c)
  (setq FR BottomFR G BottomG L BottomL TR BottomTR Cut_pt 0
        CP nil CL 0  BL 0 BG BottomG FRCP nil Duboulot t)
  (push_cont)               ; initial continuation
  (push_E (nloc c))         ; local env. for the query
  (push_G (nglob c))            ; global env. for the query
  (setq CP (cdr c) CL L)        ; current continuation
  (maj_L (nloc c))          ; ends local block
  (maj_G (nglob c)) (read-char)     ; ends global block
  (catch 'debord (forward))
  (myloop (read_prompt)))

; Mini-PrologII
; pred.lsp
;
(defvar Ob_Micro_Log
      '(|write| |nl| |tab| |read| |get| |get0|
    |var| |nonvar| |atomic| |atom| |number|
    ! |fail| |true|
    |divi| |mod| |plus| |minus| |mult| |le| |lt|
    |name| |consult| |abolish| |cputime| |statistics|
    |call| |freeze| |dif| |frozen_goals|))
(mapc #'(lambda (x) (setf (get x 'evaluable) t)) Ob_Micro_Log)

; !/0
(defun ! (n)
  (setq BL (Cut CL) BG (if (zerop BL) BottomG (BG BL))
    L (+ CL 4 n)))          ; updates local stack

; call/1 (+term)
(defun |call| (x)
  (if (var? x)
      (let ((te (ultimate x PCE PCG)))  ; dereferences it
    (unless CP
        (if (<= BL CL) (setq L CL)) ; applies LCO
        (setq CP (CP CL) CL (CL CL))) ; new continuation
    (push_cont)         ; saves continuation
    (vset Mem (+ L 2) (cdr te)) ; global env.
    (vset Mem (+ L 3) Cut_pt)   ; cut point
    (setq CP (list (dec_goal (car te))) CL L)
    (maj_L 0))          ; ends local block
    (push (dec_goal x) CP)))        ; adds it to CP

; freeze/2 (?var,+term)
(defun |freeze| (x p)
  (let ((xte (ultimate x PCE PCG))) ; dereferences the var
    (if (var? (car xte))        ; unbound
    (let ((y (adr (car xte) (cdr xte))) ; the location
          (pte (ultimate p PCE PCG))) ; dereferences the goal
      (bindfg y (dec_goal (car pte)) (cdr pte) (fgblock y)))
      (|call| p))))         ; else call p

; dif/2 (?term,?term)
(defun |dif| (x y)
  (let ((BL L) (BG G) (str TR) (FRCP nil)) ; saves registers
    (if (eq (uni x y) 'fail)        ; unification fails
    (poptrail str)          ; restores env and succeeds
      (if (/= TR str)           ; one var bound
      (let* ((xv (svref Mem (1- TR))) ; selects one var
         (v (if (numberp xv) xv (car xv))))
        (poptrail str)      ; restores env
        (bindfg v PC PCG (fgblock v))) ; perpetuates the delaying
    'fail))))           ; fails if equals

; statistics/0
(defun |statistics| ()
  (format t " local stack : ~A (~A used)~%"
      (- BottomTR BottomL) (- L BottomL))
  (format t " global stack : ~A (~A used)~%"
      (- BottomL BottomG) (- G BottomG))
  (format t " trail : ~A (~A used)~%"
      (- A BottomTR) (- TR BottomTR))
  (format t " frozen-goals stack : ~A (~A used)~%"
      BottomG (- FR BottomFR)))

; frozen_goals/0
(defun |frozen_goals| ()
  (do ((i (- FR 4) (- i 4)))        ; scans the frozen goals stack
      ((< i 0))
      (if (eq (car (svref Mem (FGvar i))) 'LIBRE) ; unbound
      (let ((b (if (numberp (FGgoal i)) (FGgoal i) i)))
        (writesf (pred (FGgoal b)) (largs (FGgoal b)) (FGenv b))
        (format t " frozen upon X~A~%" (FGvar i))))))
; mini-Cprolog & mini-PrologII
; cpred.lsp
;

(defmacro value1 (x) `(car (ultimate ,x PCE PCG)))
(defun uni (x y)
  (catch 'impossible
    (unif (ultimate x PCE PCG) (ultimate y PCE PCG))))
                    ;write/1 (?term)
(defun |write| (x)
  (write1 (ultimate x PCE PCG)))
(defun write1 (te)          ; depending on te
  (let ((x (car te)) (e (cdr te)))
    (cond
     ((null x) (format t "[]"))
     ((atom x) (format t "~A" x))
     ((var? x) (format t "X~A" (adr x e)))
     ((list? x) (format t "[")
      (writesl (val (cadr x) e) (val (caddr x) e))
      (format t "]"))
     ((writesf (functor (des x)) (largs x) e)))))
(defun writesl (te r)           ; for a list
  (write1 te)
  (let ((q (car r)) (e (cdr r)))
    (cond
     ((null q))
     ((var? q) (format t "|X~A" (adr q e)))
     (t (format t ",")
    (writesl (val (cadr q) e) (val (caddr q) e))))))
(defun writesf (fct largs e)        ; for a functional term
  (format t "~A(" fct)
  (write1 (val (car largs) e))
  (mapc #' (lambda (x) (format t ",") (write1 (val x e)))
       (cdr largs))
  (format t ")"))
                    ;nl/0
(defun |nl| () (terpri))
                    ;tab/1 (+int)
(defun |tab| (x)
  (dotimes (i (value1 x)) (format t " ")))
                    ;read/1 (?term)
(defun |read| (x)
  (let ((te (read_terme)))      ; gets the term
    (catch 'impossible
      (unif (ultimate x PCE PCG)
        (cons (cdr te) (push1_g (car te)))))))
(defun read_terme ()
  (let ((*lvarloc nil) (*lvarglob nil))
    (let ((te (read_term (rchnsep) 2)))
      (rchnsep) (cons (length *lvarglob) (c te)))))
(defun push1_g (n)
  (if (>= (+ G n) BottomL)      ; allocates a global env
      (throw 'debord (print "Global Stack Overflow")))
  (dotimes (i n (- G n))
       (vset Mem G (cons 'LIBRE BottomG))
       (incf G)))
                    ;get/1 (?car)
(defun |get| (x)
  (uni x (char-int (rchnsep))))
                    ;get0/1 (?car)
(defun |get0| (x)
  (uni x (char-int (read-char))))
                    ;var/1 (?term)
(defun |var| (x)
  (unless (var? (value1 x)) 'fail))
                    ;nonvar/1 (?term)
(defun |nonvar| (x)
  (if (var? (value1 x)) 'fail))
                    ;atomic/1 (?term)
(defun |atomic| (x)
  (if (listp (value1 x)) 'fail))
                    ;atom/1 (?term)
(defun |atom| (x)
  (unless (symbolp (value1 x)) 'fail))
                    ;number/1 (?term)
(defun |number| (x)
  (unless (numberp (value1 x)) 'fail))
                    ;fail/0
(defun |fail| () 'fail)
                    ;true/0
(defun |true| ())
                    ;divi/3 (+int,+int,?int)
(defun |divi| (x y z)
  (uni z (floor (value1 x) (value1 y))))
                    ;mod/3 (+int,+int,?int)
(defun |mod| (x y z)
  (uni z (rem (value1 x) (value1 y))))
                    ;plus/3 (+int,+int,?int)
(defun |plus| (x y z)
  (uni z (+ (value1 x) (value1 y))))
                    ;minus/3 (+int,+int,?int)
(defun |minus| (x y z)
  (uni z (- (value1 x) (value1 y))))
                    ;mult/3 (+int,+int,?int)
(defun |mult| (x y z)
  (uni z (* (value1 x) (value1 y))))
                    ;le/2 (+int,+int)
(defun |le| (x y)
  (if (> (value1 x) (value1 y)) 'fail))
                    ;lt/2 (+int,+int)
(defun |lt| (x y)
  (if (>= (value1 x) (value1 y)) 'fail))
                    ;name/2 (?atom,?list)
(defun |name| (x y)
  (let ((b (value1 x)))
     (if (var? b)
         (uni x (impl (undo_l (ultimate y PCE PCG))))
         (uni y (do_l (expl b))))))

(defun undo_l (te)
  (let ((x (car te)) (e (cdr te)))
    (if (atom x)
    x
      (cons (undo_l (val (cadr x) e)) (undo_l (val (caddr x) e))))))
(defun do_l (x)
  (if (atom x) x (list '(\. 2) (car x) (do_l (cdr x)))))
(defun impl (l)
  (intern (map 'string #'int-char l)))
(defun expl (at)
  (map 'list #'char-int (string at)))

                    ;consult/1 (+atom)
(defun |consult| (f)
  (format t "~A~%" (load (value1 f))))
                    ; abolish/1 (+ atom)
(defun |abolish| (p)
  (mapc  #'(lambda (x) (setf (get p x) nil))
     '(atom empty list fonct def)))
                    ; cputime/1 (? int)
(defun |cputime| (x)
  (uni x (float (/ (get-internal-run-time)
           internal-time-units-per-second))))