;; ---------------------------------------------------------------------------
;; ~/events/configuration.events
;; ---------------------------------------------------------------------------

;; These events are the constructors and destructors for configurations.

(enable-theory stacks)
(enable-theory grammar)
(enable-theory lists)
(enable-theory trees)

(add-shell mk-configuration Undefined-Configuration is-configuration
  ((sel-input   (none-of) zero) 
   (sel-states  (none-of) zero)
   (sel-symbols (none-of) zero)
   (sel-Trees   (none-of) zero)
   (sel-Parse   (none-of) zero)   
   (sel-Deriv   (none-of) zero)
   (sel-Error   (none-of) Zero)))

(defn stack-of-trees (trs)
  (if (not (is-stack trs))
      F
      (if (equal (EmptyStack) trs)
	  T
	  (and (is-stack trs)
	       (is-tree (top trs))
	       (stack-of-trees (pop trs)))))
  ((lessp (stack-length trs))))

(defn stack-of-numbers (trs)
  (if (not (is-stack trs))
      F
      (if (equal (EmptyStack) trs)
	  T
	  (and (is-stack trs)
	       (numberp (top trs))
	       (stack-of-numbers (pop trs)))))
  ((lessp (stack-length trs))))

;; A well-formed configuration has as its states a stack of numbers, its
;; symbols a stack of litatoms, its trees a stack consisting of individual
;; trees, etc. Probably the derivation is a well-formed derivation and so on.
;; The input can only be a list of terminals so the terminal list is needed.

(defn is-wf-configuration (c terms)
  (and (stack-of-trees (sel-trees c))
        (not (equal (sel-trees c) (EmptyStack)))
	(is-string-in (sel-input c) terms)
	(stack-of-numbers (sel-states c))))

#| This lemma MUST fail to prove!
(prove-lemma sanity-check ()
 (equal (is-wf-configuration c terms)
	F))
|#

;; This function creates the set of productions used in a tree.

(defn get-prods (flag Param)
      (if (equal flag 'tree)
	  (if (or (is-leaf Param) ; only non-terminal nodes are collected
		  (not (is-tree Param))
		  (equal Param (EmptyTree)))
	      nil 
	    (union (mk-Prod nil (sel-Root Param) (roots (sel-branches Param)))
		   (get-prods 'branches (sel-branches Param))))
	(if (equal flag 'sequence)
	    (if (nlistp Param)
		nil
	        (union (get-prods 'tree (car Param))
		       (get-prods 'sequence (cdr Param))))
	  nil)))

;; This function collects the productions for a stack of trees.

(defn nodes (tree-stack terms)
  (if (or (is-empty tree-stack)
	  (not (is-stack tree-stack)))
      nil
      (union
        (get-prods 'tree (top tree-stack))
        (nodes (pop tree-stack) terms)))
  ((lessp (stack-length tree-stack))))

(deftheory configurations 
 (NODES GET-PRODS IS-WF-CONFIGURATION STACK-OF-NUMBERS STACK-OF-TREES
  MK-CONFIGURATION ))

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