;;HATS model in ACL2

;;ns is a function to construct a new state:
(defun ns (sdt trnsf ctrl pc-trnsf pc-tree haltp)
  (list sdt trnsf ctrl pc-trnsf pc-tree haltp))

;;sdt, trnsf , ctrl, pc-trnsf, pc-tree, and haltp are functions to access the components of a state:
(defun sdt (s) (car s))
(defun trnsf (s) (cadr s))
(defun ctrl (s) (caddr s))
(defun pc-trnsf (s) (cadddr s))
(defun pc-tree (s) (car (cddddr s)))
(defun haltp (s) (cadr (cddddr s)))

;;number-of-trnsf and rules-of-trnsf are functions to get the value of the number of transformation 
;;rules and the rules themselves which exist in trnsf. ctrl-type and ctrl-order are functions 
;;to get the ctrl type and the control order in ctrl:
(defun number-of-trnsf (trnsf)
  (cdr trnsf))
(defun rules-of-trnsf (trnsf)
  (car trnsf))
(defun ctrl-type (ctrl)
  (car ctrl))
(defun ctrl-order (ctrl)
  (cdr ctrl))
(defun lhs (trnsf)
      (cadr trnsf))
(defun rhs (trnsf)
  (caddr trnsf)) 	

;;current-trnsf and current-node are functions to get the current transformation rule to be applied 
;;and to get the current node to which the current transformation rule will be applied, respectively.
(defun current-trnsf (s)
  (nth (pc-trnsf s)
       (rules-of-trnsf (trnsf s))))
(defun current-node (s)
  (nth (pc-tree s)
       (sdt s))) ;;Works for our demonstration of one level-sibling tree

;;pc+1 is a function to increment the PCs
(defun pc+1 (pcounter)
  (+ 1 pcounter)))

;;halt is a function to add a message to a state when something wrong happens during execution.
(defun halt (msg s)
  (ns (sdt s)
      (trnsf s)
      (ctrl s)
      (pc-trnsf s)
      (pc-tree s)
      msg))

;;pat-match and the other utility  functions are used to achieve pattern matching between the 
;;transformation rule and the target tree (subtree). The output of this function will be a substitution 
;;list that will be used to instantiate the right hand side of the transformation rule.

(defconst *fail* nil)
(defconst *no-bindings* '((t . t)))

(defun variable-p (x)
  (and (symbolp x) (equal (char (symbol-name x) 0) #\?)))

(defun get-binding (var bindings)
  (assoc var bindings))

(defun binding-val (binding)
  (cdr binding))

(defun lookup (var bindings)
  (binding-val (get-binding var bindings)))

(defun extend-bindings (var val bindings)
  (cons (cons var val)
        (if (equal bindings *no-bindings*)
            nil
          bindings))) 

(defun match-variable (var input bindings)
  (let ((binding (get-binding var bindings)))
    (cond ((not binding) (extend-bindings var input bindings))
          ((equal input (binding-val binding)) bindings)
          (t *fail*))))


(defun pat-match (pattern input bindings)
  (cond ((eq bindings *fail*) *fail*)
        ((variable-p pattern)
         (match-variable pattern input bindings))
        ((equal pattern input) bindings)
        ((and (consp pattern) (consp input))
         (pat-match (rest pattern) (rest input)
                    (pat-match(first pattern) (first input)
                              bindings)))
        (t *fail*)))

;;one-transform is a function that accepts a transformation rule, a tree, and an initial binding 
;;list and return a new tree that results from instantiating the right hand side of the transformation 
;;rule if there is a match between the input tree and the right hand side of the transformation rule.
(defun one-transform (trnsf tree bindings)
  (let ((sub-list (pat-match (lhs trnsf) tree  bindings)))
    (cond  ((not (null sub-list))
            (sublis sub-list (rhs trnsf)))
           (t tree))))

;;once is a function that combine the new subtree after applying the transformation rule to it with 
;;the rest of the input tree.
(DEFUN NTHCAR (N L)
  (DECLARE (XARGS :GUARD
                  (AND (INTEGERP N)
                       (<= 0 N)
                       (TRUE-LISTP L))))
  (IF (ZP N) nil (cons (car L) (NTHCAR (+ N -1) (CDR L)))))

;;Assuming that the transformation will be applied to the root of the tree and to the 
;;first level of subtrees

 (defun apply-trnsf (trnsf tree pctree)
  (let ((node (nth pctree tree)))
    (cond ((or (acl2-numberp node)
               (null node)) tree)
          ((equal pctree 0) (one-transform trnsf tree *no-bindings*))
          (t (append (nthcar  pctree tree)
                     (cons (one-transform trnsf node *no-bindings*)
                           (nthcdr (+ 1 pctree) tree)))))))


;;once-trnsf is a function that defines a new state that results from the application of the 
;;rewrite rule to the input tree. The fields that will are the sdt, the pc-trnsf, and the pc-tree
(defun once-trnsf(s)
  (let ((trnsf (current-trnsf s))
        (tree (sdt s))
        (tree-pc (pc-tree s)))
    (ns (apply-trnsf trnsf tree tree-pc)
        (trnsf s)
        (ctrl s)
        (if (<= (pc-trnsf s)(- (number-of-trnsf (trnsf s)) 1))
            (pc+1 (pc-trnsf s))
          0)
        (if (<= (pc-trnsf s)(- (number-of-trnsf (trnsf s)) 1))
            (pc-tree s)
          (pc+1 (pc-tree s)))
        (haltp s))))

(defun fix-trnsf (s)
  s)
;;transform is a function that that determine the type of the control that will be used to apply the 
;;transformation rules to the input tree.
(defun transform (s)
  (cond ((equal (ctrl-type (ctrl s)) 'once) (once-trnsf s))
        ((equal (ctrl s) 'fix) (fix-trnsf s))
        (t (halt "ILLEGAL CONTROL" s))))

;;hats apply the function onestep to the state “s” n times. The function onestep apply the 
;;current transformation rule to the current tree node.

 (defun onestep (s)
  (if (haltp s)
      s
    (transform s)))

(defun hats (s n)
  (cond ((zp n) s)
        (t (hats (onestep s) (- n 1)))))
 
;;Example
#|
(defconst *tree0* '(*
                    (* 2 (+ 3 4))
                    (* 5 (+ 6 7))
                    (* 8 (+ 9 10))))

(defconst *tr0* '(((->
                   (* ?x (+ ?y ?z))
                   (+ (* ?x ?y) (* ?x ?z)))) . 1))

(defconst *ctrl0* '(once . post-order))

(defconst *state0*
  (ns *tree0*
      *tr0*
      *ctrl0*
      0
      0
      nil))

ACL2 !>(hats *state0* 8)
[SGC for 128 CONS pages..(1635 writable)..(T=8).GC finished]
((* (+ (* 2 3) (* 2 4))
    (+ (* 5 6) (* 5 7))
    (+ (* 8 9) (* 8 10)))
 (((|->| (* ?X (+ ?Y ?Z))
         (+ (* ?X ?Y) (* ?X ?Z))))
  . 1)
 (ONCE . POST-ORDER)
 0 4 NIL)

|#