;; ---------------------------------------------------------------------------
;;   ~/events/toktrans-2.events
;; ---------------------------------------------------------------------------

;; This token transformation function looks through the token list for tokens 
;; that are in the domain of the replace alist, and replaces them with the 
;; range component. This is in contrast to toktrans-3, which has a default 
;; value to be used when the value is not found. Perhaps these two could be 
;; combined, with the default value being 'error!

(enable-theory tokens)
(enable-theory lists)

(defn make-replace (toks name dom replace-list)
  (if (nlistp toks)
      toks
      (if (and (equal (token-name (car toks)) name)
               (member (car (token-value (car toks))) dom))
          (cons (mk-token (value (car (token-value (car toks))) replace-list)
                          (token-value (car toks)))
                (make-replace (cdr toks) name dom replace-list))
          (cons (car toks)
                (make-replace (cdr toks) name dom replace-list)))))


;; I am using this as an optimization, selecting the domain once for the
;; whole token list instead of constructing it for every token.
;; This is the token transformation function toktrans-2.

(defn replace (toks name replace-list)
 (if (listp replace-list)
     (let ((dom (domain replace-list)))
       (make-replace toks name dom replace-list))
     toks))

;; I need a stepper that will demonstrate that everything else stays the
;; same and that the domain tokens get replaceed.

(defn replace-step (source target name replace-list)
 (if (nlistp source)
     (nlistp target)
      (if (and (equal (token-name (car source)) name)
               (member (car (token-value (car source))) (domain replace-list)))
         (and (equal (car target) 
                     (mk-token (value (car (token-value (car source))) 
                                      replace-list)
                          (token-value (car source))))
              (replace-step (cdr source) (cdr target) name replace-list))
         (and (equal (car source) (car target))
              (replace-step (cdr source) (cdr target) name replace-list)))))
              
;; When is replace correct?
;; When all tokens not in the domain of replace-list remain the same
;; and the tokens in the domain are replaced by the values from the alist.

(prove-lemma toktrans-2-main-theorem (rewrite)
 (implies (and (token-listp toks)
               (listp replace-list))
          (replace-step toks (replace toks name replace-list) 
                        name replace-list)))