;; ---------------------------------------------------------------------------
;; ~/events/table-generator.events
;; ---------------------------------------------------------------------------

;; This script is for actually constructing the goto and action tables for
;; a grammar.

(enable-theory grammar)
(enable-theory lists)

:; I have defined a transition to be a three-element list consisting of a 
;; state, an input symbol, and an action. I use a similar definition for 
;; transition as the one used in the NFSA=DFSA proof. There, the third element
;; was the list of following states. Here I have just one action, which is 
;; in itself a shell determining what is to be done.
;; Since a name conflict with fsap-transition in the scanner arises,
;; I prefix mk-transition with an a-. 

(defn a-mk-transition (state input action)
  (cons (cons state input) action))

;; ---------------------------------------------------------------------------
;;      I T E M   S E T
;; ---------------------------------------------------------------------------
;; Now we want to start constructing an SLR parsing table. The first task is
;; the construction of the item set for each production in the production set.
:: This means that a special token DOT is inserted at every possible position 
;; on the rhs, and the resulting productions are collected into the item set 
;; for the production. The union (they ought to be disjoint) of the item sets 
;; for each production yields the item set for the production set. 

;; This function puts the dot between lrhs and rrhs and recurses with the
;; car of rrhs appended to lrhs, remembering the production number.

(defn shift-dots-through (lhs lrhs-in rrhs label)
  (let ((lrhs (if (nlistp lrhs-in)
                  nil
                  lrhs-in)))
        (if (nlistp rrhs)
            (list (mk-prod label lhs (append lrhs (list (dot)))))
            (append
             (list (mk-prod label lhs 
                            (append lrhs (append (list (dot)) rrhs))))
             (shift-dots-through
              lhs 
              (append lrhs (list (car rrhs))) 
              (cdr rrhs)
              label)))))

;; I split the rhs into 2 parts, the part to the left of the dot and the
;; part to the right of the dot, and insert the dot at that point.

(defn insert-dots (prod)
  (let ((lhs  (sel-lhs prod))
        (lrhs nil)
        (rrhs (sel-rhs prod))
        (label (sel-label prod)))
    (shift-dots-through lhs lrhs rrhs label)))

(defn construct-item-set (prods)
 (if (nlistp prods)
     nil
     (union (insert-dots (car prods))
            (construct-item-set (cdr prods)))))

;; This function constructs the LR(0) items for the grammar

(defn LR-0-items (grammar)
 (construct-item-set (sel-productions grammar)))

;; I use an explicit shell to obtain a tagged representation
;; and a recognizer for item-sets.

(add-shell item-set empty-item-set item-setp
 ((sel-items (none-of) zero))) ; should be listp and nil

(defn first-item (is)
 (if (nlistp (sel-items is))
     nil
     (car (sel-items is))))

(defn rest-items (is)
 (if (nlistp (sel-items is))
     nil
     (item-set (cdr (sel-items is)))))

;; I must construct my own union for shell types. 

(defn item-set-union (is1 is2)
 (if (or (equal is1 (empty-item-set))
         (nlistp (sel-items is1))
         (not (item-setp is2))
         (not (item-setp is1)))
     is2
     (if (member (first-item is1) (sel-items is2))
         (item-set-union (rest-items is1) is2)
         (item-set-union  (rest-items is1)
                          (item-set (append (list (first-item is1))
                                            (sel-items is2))))))
 ((lessp (length (sel-items is1)))))
                
(defn equal-item-set (is1 is2)
 (let ((guts-is1 (sel-items is1))
       (guts-is2 (sel-items is2)))
   (and (item-setp is1)
        (item-setp is2)
        (equal guts-is1 guts-is2))))

(defn item-set-size (item-set)
 (if (or (not (item-setp item-set))
         (nlistp (sel-items item-set))
         (equal item-set (empty-item-set)))
     0
     (add1 (item-set-size (rest-items item-set))))
 ((lessp (length (sel-items item-set)))))

; This is part of the epsilon closure. That is something that is
; reached in an epsilon step from anything in the set. This means that
; the lhs is equal to the sym, and the dot is in the first position.

(defn next-items (sym all-items)
 (if (nlistp all-items)
     nil
     (if (and 
          ;; Sym is the lhs non-terminal.
          (equal sym (car (sel-lhs (car all-items))))
          ;; Dot is in the first rhs position.
          (equal (car (sel-rhs (car all-items))) (dot)))
         (append (list (car all-items))
               (next-items sym (cdr all-items)))
         (next-items sym (cdr all-items)))))

(defn symbol-after-dot (item-rhs)
  (if (nlistp item-rhs)
      nil
      (if (equal (car item-rhs) (dot))
          (if (nlistp (cdr item-rhs))
              nil
              (cadr item-rhs))
          (symbol-after-dot (cdr item-rhs)))))

;; For all items in sis, fis is the full item set.

(defn epsilon-step-all (sis fis)
 (if (or (nlistp (sel-items sis)) 
         (equal sis (empty-item-set))
         (not (item-setp sis)))
     sis
     (item-set-union
      (item-set (next-items (symbol-after-dot (sel-rhs (first-item sis)))
                            fis))
      (epsilon-step-all (rest-items sis) fis)))
 ((lessp (item-set-size sis))))

;; Note: this closure was implemented before I figured out how to do
;; the termination. Since it works, I am NOT TOUCHING it now!

(defn closure-step (set1 set2 fis clock)
 (if (zerop clock)
     'timed-out
     (if (equal-item-set set1 set2)
         set1
         (item-set-union 
          set1 
          (closure-step set2
                        (epsilon-step-all set2 fis)
                        fis
                        (sub1 clock))))))

;; The closure adds reachable productions from the grammar until no
;; new ones can be added.

;; I need to find a clock for the closure. Since I cannot have more than 
;; the entire item set, I'll use its length.

(defn closure (seed-item-set fis)
 (let ((first  (epsilon-step-all seed-item-set fis)))
      (closure-step seed-item-set first fis (length fis))))

(defn jump-dot (item sym fis)
  (if (nlistp fis)
      nil
      (if (and (equal (sel-label item)
                      (sel-label (car fis)))
               (equal (position (dot) (sel-rhs (car fis)))
                      (add1 (position (dot) (sel-rhs item))))
               (equal (nth (position (dot) (sel-rhs item)) (sel-rhs (car fis)))
                      sym))
          (car fis)
          (jump-dot item sym (cdr fis)))))

(defn dot-sym-in-item-set (sym items fis)
 (if (nlistp items)
     nil
     (if (equal sym (nth (add1 (position (dot) (sel-rhs (car items))))
                         (sel-rhs (car items))))
         (let ((new (list (jump-dot (car items) sym fis))))
           (union new
                  (dot-sym-in-item-set sym (cdr items)  fis)))
         (dot-sym-in-item-set sym (cdr items) fis))))

;; The goto-function takes the closure of the set of items for which the
;; dot "jumps the symbol".

(defn goto-function (is symbol fis)
  (let ((jump (dot-sym-in-item-set symbol (sel-items is) fis)))
    (if (nlistp jump)
        (empty-item-set)
        (closure (item-set jump) fis))))

;; The collection for an item-set cdrs down the vocabulary (nts and terms),
;; checking the goto-function for the item-set and each vocabulary symbol.
;; If the goto-function is not empty, it is added to the collection.

(defn collection (is symbol-list fis)
 (if (nlistp symbol-list)
     nil
     (let ((goto (goto-function is (car symbol-list) fis)))
       (if (equal goto (empty-item-set))
           (collection is (cdr symbol-list) fis)
           (append 
            (list goto)
            (collection is (cdr symbol-list) fis))))))

;; The function items1 cdrs down the current collection (set of item sets)
;; adding the collection for each item set.

(defn items1 (set-of-item-sets v fis)
  (if (nlistp set-of-item-sets)
      set-of-item-sets
      (union 
       (collection (car set-of-item-sets) v fis)
       (items1 (cdr set-of-item-sets) v fis))))
        
;; The function items expands the collection by repeatedly calling
;; items one. When no new item-sets have been added, it terminates.

;; I need a clock for termination. The true measure is the difference 
;; between the full-item-set and the sis, but since the latter
;; is defined in an inner let-clause, it is not visible to the measure 
;; hint. I can use the length of the full-item-set for the measure 
;; and split the work between two functions.

(defn items (set-of-item-sets v fis clock)
 (if (zerop clock)
     (cons set-of-item-sets 'items-times-out)
     (let ((cprime (items1 set-of-item-sets v fis)))
       (if (subsetp cprime set-of-item-sets)
           set-of-item-sets
           (let ((sis (union set-of-item-sets cprime) )) 
             (items sis v fis (sub1 clock)))))))

;; Construct the canonical collection for a grammar by setting the collection 
;; to the closure for the start production for the first iteration. Then call 
;; items to iterate until no more item sets can be added to the collection. 
;; Fis is passed to keep from constructing this every time it is needed. 
;; An additional speed-up could be obtained by pre-calculating the set of 
;; productions that belong to each non-terminal.

(defn start-item (start fis)
 (if (nlistp fis)
     nil
     (if (and (equal start (sel-label (car fis)))
              (equal (car (sel-rhs (car fis))) (dot)))
         (item-set (list (car fis)))
         (start-item start (cdr fis)))))

(defn canonical-collection (grammar)
 (let ((start (sel-axiom       grammar))
       (voc   (vocab           grammar))
       (fis   (lr-0-items grammar)))
   (let ((c   (list (closure (start-item start fis) fis))))
     (items c voc fis (length fis)))))

;; ---------------------------------------------------------------------------
;;      Extracting the action table
;; ---------------------------------------------------------------------------

(defn is-completed-item (item) (equal (car (last (sel-rhs item))) (dot)))

(defn completed-items (item-set)
 (if (or (not (item-setp item-set))
         (equal item-set (empty-item-set))
         (nlistp (sel-items item-set)))
     nil
     (if (is-completed-item (first-item item-set))
         (cons (first-item item-set) (completed-items (rest-items item-set)))
         (completed-items (rest-items item-set))))
 ((lessp (item-set-size item-set)))))

(defn is-in-follow (after before follows)
  (if (nlistp follows)
      f
      (if (equal before (caar follows))
          (member after (cdar follows))
          (is-in-follow after before (cdr follows)))))

(defn valid-item (item-set sym)
 (if (or (not (item-setp item-set))
         (equal item-set (empty-item-set))
         (nlistp (sel-items item-set)))
     f
     (let ((item (first-item item-set)))
       (let ((rhs (sel-rhs item)))
         (let ((dot-pos (position (dot) rhs)))
           (if (equal sym (nth (add1 dot-pos) rhs))
               t
               (valid-item (rest-items item-set) sym))))))
 ((lessp (item-set-size item-set))))

(defn lookup-follow (sym follows)
 (if (nlistp follows)
     nil
     (if (equal sym (caar follows))
         (cdar follows)
         (lookup-follow sym (cdr follows)))))

;; The following function computes the action for one state and one symbol.

(defn state-action (item-set cc sym fis follows)
 (let ((shift (if (valid-item item-set sym)
                  (mk-shift-action 
                   (position (goto-function item-set sym fis) cc))
                  (empty-action)))
       (reduce (let ((comps (item-set (completed-items item-set))))
                 (if (equal (item-set-size comps) 1)
                     (if (member 
                          sym 
                          (lookup-follow 
                           (car (sel-lhs (first-item comps))) follows))
                         (mk-reduce-action
                          (sel-label (first-item comps))
                          (sel-lhs   (first-item comps))
                          ;; Ignore the dot.
                          (sub1 (length (sel-rhs (first-item comps))))) 
                         (empty-action))
                     (if (zerop (item-set-size comps))
                         (empty-action)
                         'reduce-reduce-conflict)))))
   (if (is-action reduce)
       (if (equal shift (empty-action))
           (if (equal reduce (empty-action))
               (mk-error-action)
               reduce)
           (if (equal reduce (empty-action)) 
               shift
               'shift-reduce-conflict))
       reduce)))
        
(defn one-state (state item-set cc terms fis follows)
  (if (nlistp terms)
      nil
      (append (list (a-mk-transition
                     state
                     (car terms)
                     (state-action item-set cc (car terms) fis follows)))
              (one-state state item-set cc (cdr terms) fis follows))))

(defn mk-actiontab (state cc fullcc terms fis follows)
  (if (nlistp cc)
      nil
      (append (one-state state (car cc) fullcc terms fis follows)
              (mk-actiontab (add1 state) (cdr cc) fullcc terms fis follows))))

;; The set of terminals must have the 'eof symbol added:
;; (mk-actiontab 0 cc cc (append terms (list (end-of-file))) fis follow)


;; ---------------------------------------------------------------------------
;;      Extracting the goto table
;; ---------------------------------------------------------------------------

;; For all nonterminals A if goto (Ii, A) = Ij then goto [i, A] = j.

;; For all states, note that the number which will represent the state 
;; is one more than the "real" state, i.e. the position in the list.

(defn mk-goto-1-nt (sis nt state fis)
  (if (zerop state)
      nil
      (let ((I-i  (nth (sub1 state) sis)))
        (let ((goto (goto-function I-i nt fis)))
          (if (equal goto (empty-item-set))
              (mk-goto-1-nt sis nt (sub1 state) fis)
              (union (list (list (cons (sub1 state) nt) 
                                 (list 'goto (position goto sis))))
                   (mk-goto-1-nt sis nt (sub1 state) fis)))))))

;; I cdr down the list of nonterminals.
        
(defn mk-gototab (sis nts fis)
  (if (nlistp nts)
      nil
      (union (mk-goto-1-nt sis (car nts) (length sis) fis)
             (mk-gototab sis (cdr nts) fis))))

                       
;; First I have to construct the canonical collection, then we make the 
;; tables and cons them together.

(defn construct-tables (grammar)
 (let ((cc      (canonical-collection grammar))
       (nts     (sel-nonterminals grammar))
       (terms   (append (sel-terminals grammar) (end-of-file)))
       (fis     (LR-0-items grammar))
       (follows (all-follows grammar)))
   (mk-Tables
    (mk-actiontab 0 cc cc terms fis follows)
    (mk-gototab cc nts fis)))))

#|
; In order to save time, I can use this (and not have to 
; calculate the canonical collection three times...

(defn construct-tables1 (cc nts terms fis follows)
   (mk-Tables
    (mk-actiontab 0 cc cc terms fis follows)
    (mk-gototab cc nts fis)))))
|#