;; ---------------------------------------------------------------------------
;; ~/events/token.events
;; ---------------------------------------------------------------------------

;; This is the representation for a (pre-)token, which is what the scanner is
;; to deliver.

(add-shell mk-token nil tokenp
           ((token-name (none-of) zero)
            (token-value (none-of) zero)))

(defn token-listp (l)
  (if (nlistp l)
      (equal l nil) 
      (and (tokenp (car l))
           (token-listp (cdr l)))))

;; This function filters out the token names from a token list.

(defn pick-token-names (l)
 (if (nlistp l)
     nil
     (if (tokenp (car l))
	 (cons (token-name (car l)) (pick-token-names (cdr l)))
	 (cons (car l) (pick-token-names (cdr l))))))

(deftheory tokens (MK-TOKEN PICK-TOKEN-NAMES TOKEN-LISTP))
(disable-theory tokens)