;;; -*- Mode: Lisp; Package: Prolog; Base: 10; Options: ((World System)) -*-
;;; (C) Copyright 1983,1984,1985, Uppsala University

;;this is the LM-Prolog's trace facility

(define-predicate first-member
  :(options (compile-method open))
  ((first-member ?element ?list)
   (prove-once (member ?element ?list))))

(define-predicate trace
  :(options
     (argument-list (+predicator-or-predicators &rest +options))
     (documentation
       "traces each call to +PREDICATOR-OR-PREDICATORS if its a symbol,
 or each of the elements of +PREDICATOR-OR-PREDICATORS if its is list.
 The currently supported options to trace are:

 (:print-if . ?port-names) where the valid port names are
 :TRYING :SUCCEEDING :FAILING and :RE-TRYING the default is all four of them

 (:when . ?patterns) --- the tracing//stepping applies only if the call unifies
 with at least one of the ?patterns 

 :step  --- enter step mode when the predicate is entered
	    this mode is self documenting (type  for help)

 (:before ?predicator) --- ?predicator is called on the ?call upon entry
 (:after ?predicator) ---- ?predicator is called on the ?call after entry

 (:world ?world) --- ?world where the traced predicate is to live, 
		     defaults to prolog:traced-predicates"))
  ((trace ?name-or-names . ?trace-options)
   (cases ((first-member (:world ?world) ?trace-options))
	  ((= ?world traced-predicates)))
   (bag-of ? ?
    (either (member ?predicator ?name-or-names)
	    (= ?predicator ?name-or-names))
    (either (untrace ?predicator) (true))
    (either (prove-once
	      (definition (define-predicate ? (:options . ?old-options) . ?)
			  ?predicator))
	    (and (format t "~%Warning from trace: ~s is not a predicator"
			 ?predicator)
		 (fail)))
    (remove ?options-1 (:compile-method . ?) ?old-options)
    (remove ?options-2 (:indexing-patterns . ?) ?options-1)
    (substitute ?new-options (:world ?old-world) (:world ?world) ?options-2 =)
    (trace-body ?body ?predicator ?trace-options ?old-world)
    (add-world ?world)
    (define-predicate ?predicator (:options . ?new-options)
      ?body))))

(define-predicate trace-body
  ((trace-body ((?predicator . ?arguments) . ?body) ?predicator ?options ?world)
   (= ?call (?predicator . ?arguments))
   (either (first-member (:print-if . ?ports) ?options)
	   (= ?ports :(trying failing succeeding re-trying)))
   (cases ((first-member :trying ?ports) (= ?trying "Trying:    "))
	  ((= ?trying ())))
   (cases ((first-member :failing ?ports) (= ?failing "Failing:   "))
	  ((= ?failing ())))
   (cases ((first-member :succeeding ?ports)
	   (= ?succeeding "Succeeding:"))
	  ((= ?succeeding ())))
   (cases ((first-member :re-trying ?ports) (= ?re-trying "Re trying: "))
	  ((= ?re-trying ())))
   (cases ((and (= ?trying ()) (= ?failing ()) (= ?succeeding ()) (= ?re-trying ()))
	   (= ?print-in ())
	   (= ?print-out ()))
	  ((= ?print-out
	      ((print-trace-out ?succeeding ?re-trying ?indentation ?level ?call)))
	   (= ?print-in
	      ((print-trace-in ?trying ?failing ?indentation ?level ?call)))))
   (cases ((first-member :step ?options)
	   (= ?try ((do-step-response ?call ?world))))
	  ((= ?try ((call ?call ?world)))))
   (cases ((first-member (:before ?before-predicate) ?options)
	   (= ?before ((?before-predicate ?call))))
	  ((= ?before ())))
   (cases ((first-member (:after ?after-predicate) ?options)
	   (= ?after ((?after-predicate ?call))))
	  ((= ?after ())))
   (append ?inner-body ?print-in ?before ?try ?after ?print-out)
   (cases ((first-member (:when . ?patterns) ?options)
	   (= ?body ((cases ((can-prove (member ?call ?patterns)) . ?inner-body)
			    ((call ?call ?world))))))
	  ((= ?body ?inner-body)))))

(define-predicate print-trace-in 
  ((print-trace-in ?trying ?failing ?indentation ?level (?predicator . ?arguments))
   (trace-level ?level ?predicator)
   (indentation ?indentation)
   (print-trace ?trying ?failing ?indentation ?level (?predicator . ?arguments))))

(define-predicate print-trace-out
  ((print-trace-out ?trying ?failing
		    ?indentation ?level (?predicator . ?arguments))
   (print-trace ?trying ?failing ?indentation ?level (?predicator . ?arguments))
   (decrement-indentation)
   (decrement-trace-level ?predicator)))

(defun step-response-help (stream &rest ignore)
  (format stream "~%You are in the stepper.
Type either ~:C or C to step through everything (to CREEP),
Type either ~:C or L to continue (LEAP),
Type either ~:C or S to prove the current predication without any tracing (SKIP),
~:C or control-L redisplays the current predication,
Type F to cause the current predication to be FALSE,
Type T to cause the current predication to be TRUE,
Type A to give the ANSWER,
Type B or ~:C to break to a Prolog//Lisp listener."
	  #\cr #\line #\altmode #\clear-screen #\break))

(deffun step-response (call)
  (let ((response
	  (FQUERY '(:choices
		    (((creep "Creep.") #\cr #/c #/C)
		     ((leap "Leap.") #\line #/l #/L)
		     ((skip "Skip.") #\altmode #/s #/S)
		     ((false "False.") #/f #/F)
		     ((true "True.") #/t #/T)
		     ((accept "Accept.") #/a #/A)
		     ((break "Break.") #/b #/B #\break)
		     ((refresh "Refresh.") #\clear-screen #^L))
		    :list-choices nil
		    :fresh-line nil
		    :help-function
		    step-response-help)
		  " ")))
    (selectq response
      (refresh (send standard-output ':clear-screen)
	       (funcall (current-entrypoint 'print-trace-doit)
			(continuation (true))
			call)
	       (step-response call))
      (break (break "STEP") (step-response call))
      (accept (format t "~%Enter a term to unify with the current predication: ")
	      (prolog-cons 'answer (PARSE-TERM (read))))
      (t response))))

(define-predicate *indentation*
  :(options (type dynamic))
  ((*indentation* 1)))

(define-predicate indentation
  ((indentation ?indentation)
   (prove-once (*indentation* ?indentation))
   (sum ?next-indentation ?indentation 1)
   (assume ((*indentation* ?next-indentation)) :system)))

(define-predicate decrement-indentation
  ((decrement-indentation)
   (prove-once (*indentation* ?next-indentation))
   (sum ?indentation ?next-indentation -1)
   (assume ((*indentation* ?indentation)) :system)))

(define-predicate *trace-level*
  :(options (type dynamic))
  ((*trace-level* 0 ?)))

(define-predicate trace-level
  ((trace-level ?level ?predicator)
   (prove-once (*trace-level* ?old-level ?predicator))
   (sum ?level ?old-level 1)
   (assume ((*trace-level* ?level ?predicator)) :system)))

(define-predicate decrement-trace-level
  ((decrement-trace-level ?predicator)
   (prove-once (*trace-level* ?old-level ?predicator))
   (sum ?level ?old-level -1)
   (assume ((*trace-level* ?level ?predicator)) :system)))

(define-predicate print-trace-doit
  ((print-trace-doit ?call)
   (format t "~S" ?call)))

(define-predicate print-trace
  ((print-trace ?in-label ?out-label ?indentation ?level ?call)
   (lisp-value ?le-10 (min 10 '?indentation) :dont-invoke)
   (or (cases ((= ?in-label ()))
	      ((format t "~%~vt(~d)~a " ?le-10 ?level ?in-label)
	       (print-trace-doit ?call)))
       (cases ((= ?out-label ())
	       (false))
	      ((format t "~%~vt(~d)~a " ?le-10 ?level ?out-label)
	       (print-trace-doit ?call)
	       (false))))))

(define-predicate untrace
  :(options
     (argument-list (&optional predicator))
     (documentation
       "removes a trace from PREDICATOR if given, otherwise removes all traces."))
  ((untrace ?predicator)
   (predicator ?predicator traced-predicates)
   (remove-definition ?predicator traced-predicates))
  ((untrace) ;;all
   (remove-world traced-predicates)
   (bag-of ? ?
     (predicator ?predicator traced-predicates)
     (untrace ?predicator))))
	  
(define-predicate untrace-query
  :(options
     (documentation
       "queries the user for each traced predicate whether it should be untraced."))
  ((untrace-query)
   (bag-of ? ?
    (predicator ?predicator traced-predicates)
    (y-or-n "~%Untrace ~s? " ?predicator)
    (untrace ?predicator))))

(define-predicate who-state
  :(options (argument-list (+label))
	    (documentation "displays +LABEL on the run state part of the who line,
 upon backtracking the original state is restored."))
  ((who-state ?label)
   (lisp-value ?old-label (tv:process-whostate current-process) :dont-invoke)
   (unwind-protect
     (lisp-command (set-who-state '?label))
     (lisp-command (set-who-state '?old-label)))))

(deffun set-who-state (label)
  (setf (process-whostate current-process) (string label))
  (tv:who-line-run-state-update))

;;; The Step facility, by Mats Carlsson.


(defun get-p-and-world (p world)
  (and (unify p (definition-predicator *definition*))
       (unify world (option-value ':world (definition-options *definition*)))))

;;We get here with stepping turned on and with
;;*definition* closure bound to the thing we really want to call.
(define-predicate do-step
  ((do-step . ?args)
   (lisp-command (get-p-and-world '?p '?world) :dont-invoke)
   (= ?call (?p . ?args))
   (unwind-protect
     (lisp-command (step-off) :dont-invoke)
     (lisp-command (step-on) :dont-invoke))
   (print-trace-in "Trying:    " "Failing:   " ?x ?y ?call)
   (do-step-response ?call ?world)
   (print-trace-out "Succeeding:" "Re trying: " ?x ?y ?call)
   (unwind-protect
     (lisp-command (step-on) :dont-invoke)
     (lisp-command (step-off) :dont-invoke))))

(define-predicate do-step-response
  ((do-step-response ?call ?world)
   (lisp-value ?response (step-response '?call) :dont-invoke)
   (RULES ?RESPONSE
	  (CREEP (step ?call ?world))
	  (LEAP (call ?call ?world))
	  (SKIP (without-world traced-predicates (call ?call ?world)))
	  (TRUE)
	  ((ANSWER . ?call)))))

(define-predicate step
  (:options
    (:argument-list (+call &optional +world))
    (:documentation "executes CALL with global stepping turned on."))
  ((step ?call)
   (unwind-protect
     (lisp-command (step-on) :dont-invoke)
     (lisp-command (step-off) :dont-invoke))
   ?call
   (unwind-protect
     (lisp-command (step-off) :dont-invoke)
     (lisp-command (step-on) :dont-invoke)))
  ((step ?call ?world)
   (unwind-protect
     (lisp-command (step-on) :dont-invoke)
     (lisp-command (step-off) :dont-invoke))
   (call ?call ?world)
   (unwind-protect
     (lisp-command (step-off) :dont-invoke)
     (lisp-command (step-on) :dont-invoke))))