;;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)
|#