;; ---------------------------------------------------------------------------
;; ~/events/parser.events
;; ---------------------------------------------------------------------------
;;
;; This is the skeleton parser
;;

(enable-theory stacks)
(enable-theory lists)
(enable-theory grammar)
(enable-theory configurations)
(enable-theory derivations)

;; This is what happens to trees during reduction. It should keep the
;; frontier invariant.

(defn reduce-trees (lhs size trees)
 (if (or (lessp (stack-length trees) size)
         (not (is-stack trees))
         (zerop size))
     (emptystack)
     (push (mk-tree 
            lhs 
            (top-n size trees))
           (pop-n size trees))))

;; The list l matches s if l corresponds to s in stack order.

(defn matches-stack (l s)
 (if (not (is-stack s))
     F
     (if (is-empty s)
         (nlistp l)
         (if (nlistp l)
             T
             (and (equal (car l) (top s))
                  (matches-stack (cdr l) (pop s)))))))

;; This is the basic parsing step.

(defn parsing-step (conf tables grammar)
 (let ((input   (sel-input conf))
       (states  (sel-states conf))
       (symbols (sel-symbols conf))
       (trees   (sel-trees conf))
       (parse   (sel-parse conf))
       (deriv   (sel-deriv conf))
       (error   (sel-error conf))
       (prods   (sel-productions grammar)))

   (if (nlistp input)
       (mk-configuration
         input states symbols trees parse deriv T)
       (let ((act  (action-lookup (token-name (car input))
                                  (top states) 
                                  (sel-Actiontab tables))))
         (case (sel-action-tag act)
           (error
            ;; Set the error flag and terminate.
            (mk-configuration
             input states symbols trees parse deriv T))
           (shift
            (let ((s (sel-state-shift act)))
              (mk-configuration
               (cdr input)
               (push s states)
               ;; I only push the token-name, not the whole token.
               (push (token-name (car input)) symbols)
               (push (mk-tree (car input) nil) trees)
               parse
               deriv
               F)))
           (reduce
              (let ((label (sel-Label-Reduce act))
                    (lhs   (car (sel-Lhs-Reduce act)))
                    (size  (sel-Size-Reduce act)))
                (let ((rhs (sel-rhs (prod-nr label prods))))
                (if (or (lessp (stack-length trees) size)
                        (not (matches-stack (reverse rhs) symbols))
                        (zerop size))
                    ;; I cannot do a reduction if there are less than
                    ;; size things on the stack or if the rhs does not match,
                    ;; so terminate with error.
                    (mk-configuration
                     input states symbols trees parse deriv T)
                  (let ((goto (goto-lookup lhs
                                           (top (pop-n size states))
                                           (sel-Gototab tables))))
                    (mk-configuration
                     input
                     (push goto (pop-n size states))
                     (push lhs (pop-n size symbols))
                     (reduce-trees lhs size trees)
                     (append parse (list label))
                     (append (list (mk-Derivation-Step 
                                    (from-bottom (pop-n size symbols))
                                    (mk-prod label lhs (top-n size symbols))
                                    ;; I only use the token names.
                                    (pick-token-names input)))
                             deriv)
                     F))))))
           (otherwise
                (mk-configuration
                 input states symbols trees parse deriv T)))))))

;; I define an explicit acceptance predicate. This is the difference
;; to the standard method of parsing, which has an accept action which
;; is a special reduction. Special cases are not especially conductive
;; to proofs!

(defn accepting (conf axiom)
 (and (equal (car (sel-Input conf))
             (mk-token (end-of-file) nil))  ; input consumed
      (equal (last (sel-Parse conf))        ; Last reduction was the goal
             (list Axiom )))) 

(defn error (conf)
  (sel-Error conf))

;; This is the skeleton parser. I parse until either the clock runs out,
;; or a configuration is reached which is either in error or accepting.

(defn parse-it (conf tables grammar clock)
   (if (zerop clock) ; go buy some more time
       conf
     (if (or (error conf)
             (accepting conf (sel-axiom grammar)))
         conf
         (parse-it (parsing-step conf tables grammar) 
                   tables 
                   grammar 
                   (sub1 clock))))
 ((lessp (count clock))))

;; The input string needs an end-of-file on the end. 
;; I use the twice the length of the input (once for each read and once
;; for the maximum stack size) times the number of productions, which
;; is the same as the maximum reduction sequence possible without a cycle,
;; as an approximation for the length of the parsing process.

(defn parser (string tables grammar)
  (parse-it
   (mk-configuration
    (append string (list (mk-token (end-of-file) nil)))
    (push 0 (emptystack))
    (emptystack)
    (emptystack)
    nil
    nil
    F)
    tables
    grammar
    (times (times (length string) 2) 
           (length (sel-productions grammar))))) 

(disable-theory stacks)
(disable-theory lists)
(disable-theory grammar)
(disable-theory configurations)
(disable-theory derivations)