;; ---------------------------------------------------------------------------
;;   ~/events/toktrans-3.events
;; ---------------------------------------------------------------------------

;; This token transformation function looks through the token list for 
;; tokens with  token-name equal to name. The value is looked up in a table, 
;; as in toktrans-2. If there is no entry in the table, a default value 
;; is substituted. 

(enable-theory tokens)

(defn make-key-words (toks name dom key-words-list default)
  (if (nlistp toks)
      toks
      (if (equal (token-name (car toks)) name)
	  (if (member (token-value (car toks)) dom)
	      (cons (mk-token (value (token-value (car toks)) 
				     key-words-list) 
			      (token-value (car toks)))
		    (make-key-words (cdr toks) 
				    name dom key-words-list default))
	      (cons (mk-token default 
                              (token-value (car toks)))
		    (make-key-words (cdr toks) 
				    name dom key-words-list default)))
	  (cons (car toks)
		(make-key-words (cdr toks) 
				name dom key-words-list default)))))

(defn determine-key-words (toks name key-words-list default)
 (if (listp key-words-list)
     (let ((dom (domain key-words-list)))
       (make-key-words toks name dom key-words-list default))
     toks))

(defn key-words-step (source target name key-words-list default)
 (if (nlistp source)
     (nlistp target)
      (if (equal (token-name (car source)) name)
	  (if (member (token-value (car source)) (domain key-words-list))
	      (and (equal (car target) 
                          (mk-token (value (token-value (car source)) 
					   key-words-list) 
                                    (token-value (car source))))
		   (key-words-step (cdr source) (cdr target) 
				   name key-words-list default))
	      (and (equal (car target) 
                          (mk-token default 
                                    (token-value (car target))))
		   (key-words-step (cdr source) (cdr target) 
				   name key-words-list default)))
	  (and (equal (car source) (car target))
	       (key-words-step (cdr source) (cdr target) 
			       name key-words-list default)))))

(prove-lemma toktrans-3-main-theorem (rewrite)
 (implies (and (token-listp toks)
	       (listp key-words-list))
	  (key-words-step 
	       toks 
               (determine-key-words toks name key-words-list default) 
               name key-words-list default)))