; =======================================================================
; FILENAME:	DivisorList.demo
; DATE:		4/15/04
; PROGRAMMER:	Albert Goldfain

; Lines beginning with a semi-colon are comments.
; Lines beginning with "^" are Lisp commands.
; All other lines are SNePS commands.
;
; To use this file: run SNePS; at the SNePS prompt (*), type:
;
;	(demo "DivisorList.demo" :av)
;	
; Make sure all necessary files are in the current working directory
; or else use full path names.
; =======================================================================
^(load "Calculator.lisp")


;TRACING OPTIONS
^(setq snip:*infertrace* nil)
^(setq snip:*plantrace* t)


;==============================================================
; PRIMITIVE ACTIONS
;==============================================================

(^ (define-primaction calc-add (object1 object2)
   	"adds object1 and object2"
   	(setf x (node-to-lisp-object (sneps:choose.ns object1)))
   	(setf y (node-to-lisp-object (sneps:choose.ns object2)))
	(format t "~&Entering ~A + ~A on my calculator.~%" x y)
   	(setf sum (sneps-calculator::plus-button x y))
	(format t "~&CALCULATOR READS: ~A~%" sum) 
   	#!((assert result ~(lisp-object-to-node sum) 
              	op calc-add 
              	arg1 ~(sneps:choose.ns object1) 
              	arg2 ~(sneps:choose.ns object2)))
	#!((assert member ~(lisp-object-to-node sum) class NaturalNumber))
   )
)

(^ (define-primaction calc-mod (object1 object2)
   	"finds the remainder of object1 divided by object2"
   	(setf modarg1 (node-to-lisp-object (sneps:choose.ns object1)))
   	(setf modarg2 (node-to-lisp-object (sneps:choose.ns object2)))
	(format t "~&Entering ~A MOD ~A on my calculator.~%" modarg1 modarg2)
   	(setf theMod (sneps-calculator::mod-button modarg1 modarg2)) 
	(format t "~&CALCULATOR READS: ~A~%" theMod)
   	#!((assert result ~(lisp-object-to-node theMod) 
              	op calc-mod 
              	arg1 ~(sneps:choose.ns object1) 
              	arg2 ~(sneps:choose.ns object2)))
	#!((assert member ~(lisp-object-to-node theMod) class NaturalNumber))
	#!((assert member ~(lisp-object-to-node theMod) class CurrentRemainder))
   )
)

(^ (define-primaction say (object1)
   "Print the argument nodes in order."
   (format t "~&~A.~%" (sneps:choose.ns object1))
   )
)

;(^ (define-primaction start-list(object1 object2)
;	"creates a new object2 list for object1"
;	(format t "~&Creating a ~A list for ~A" 
;		(sneps:choose.ns object2)
;		(sneps:choose.ns object1)
;	) 
;	#!((assert object1 ~(sneps:choose.ns object1) 
;                   rel ~(sneps:choose.ns object2) 
;                   object2 (build rest *nil) 
;          ))
;   )
;)




;(^ (define-primaction add-to-list(object1 object2)
;   	"adds object1 to the list of object2"
;   	(setf x (node-to-lisp-object (sneps:choose.ns object1)))
;   	(setf y (node-to-lisp-object (sneps:choose.ns object2)))
;	(format t "~&Finding the mod of ~A and ~A~%" x y)
;   	(setf theMod (sneps-calculator::mod-button x y)) 
;   	#!((assert result ~(lisp-object-to-node theMod) 
;              	op calc-mod 
;              	arg1 ~(sneps:choose.ns object1) 
;              	arg2 ~(sneps:choose.ns object2)))
;   )
;)



(^ (attach-primaction
    ;; built-in actions:
    snsequence snsequence
    sniterate sniterate
    snif snif
    achieve achieve
    believe believe
    disbelieve disbelieve
    withsome withsome
    withall withall
    ;;user defined actions:
    calc-add calc-add
    calc-mod calc-mod
    say say))

(define rel before after time lex member class object state object3 object4 object5 object6 object7 object8 object9 first rest dividend divisor property op arg1 arg2 result)

(assert member #nil class nil)

;==============================================================
; update-num-var
;==============================================================	
(assert forall ($theVar $oldValue $newValue)
	ant (build member *newValue class NaturalNumber)
	cq (build act (build action update-num-var object1 *theVar object2 *oldValue object3 *newValue)
		plan (build action snsequence
		    	    object1 (build action disbelieve
					   object1 (build member *oldValue
							  class *theVar))
			    object2 (build action believe
					   object1 (build member *newValue
							  class *theVar))
		     )
	   )
)

;==============================================================
; update-divisor-candidate
;==============================================================	  
(assert forall ($oldC $newC)
	&ant ((build member *oldC class DivisorCandidate)
	      (build member *newC class NewDivisorCandidate))
	cq (build act (build action update-divisor-candidate)
		plan (build action snsequence
		    	    object1 (build action disbelieve
					   object1 (build member *oldC
							  class DivisorCandidate))
			    object2 (build action believe
					   object1 (build member *newC
							  class DivisorCandidate))
			    object3 (build action disbelieve
					   object1 (build member *newC
							  class NewDivisorCandidate))
		     )
	   )
)
;==============================================================
; increment
;==============================================================	  
(assert forall $x
	ant (build member *x class NaturalNumber)
	cq (build act (build action increment object1 *x)
		plan (build action calc-add object1 1 object2 *x)
	   )
)

;==============================================================
; store-remainder
;==============================================================	
(assert forall ($x $y $z)
	&ant ((build member *x class NaturalNumber)
	      (build member *y class DivisorCandidate)
	      (build member *z class NaturalNumber))  ;TEMP
	cq (build act (build action store-remainder) 
		plan  (build action believe object1 (build member *z class CurrentRemainder))
	   )
) 		     
;==============================================================
; check-divisible
;==============================================================	
(assert forall ($x $y)
	&ant ((build member *x class NaturalNumber)
	      (build member *y class DivisorCandidate))
	cq (build act (build action check-divisible object1 *x object2 *y)
		 plan (build action snsequence
			     object1 (build action calc-mod object1 *x object2 *y)
			     object2 (build action store-remainder)
			     object3 (build action snif
					    object1 ((build condition (build member 0 class CurrentRemainder)
							    then (build action snsequence 
									object1 (build action say object1 "Found a divisor")
									object2 (build action believe
											object1 (build object1 *y
										       		       rel divisor-of
										                 object2 *x))
                                                                 )
						     )
						    (build else (build action believe
									object1 (build min 0 max 0 
										 arg (build object1 *y
											    rel divisor-of
											    object2 *x))
                                                                 )
                                                    ))
                                     )
			     object4 (build action disbelieve
					    object1 (build member (find (result- ! op) calc-mod 
                                                                        (result- ! arg1) *x 
                                                                        (result- ! arg2) *y)
							   class CurrentRemainder)
			             )
		      )
	    )
)


;==============================================================
; set-new-divisor-candidate
;==============================================================
(assert forall $x
	ant (build member *x class DivisorCandidate)
	cq (build act (build action set-new-divisor-candidate)
		 plan (build action believe
		       object1 (build member (find (result- ! op) calc-add
					      (result- ! arg1) 1
					      (result- ! arg2) *x)
				      class NewDivisorCandidate
			       )
                      )
	   )
)
			    


;==============================================================
; build-divisor-list
;==============================================================
(assert forall ($x $y)
	&ant ((build member *x class NaturalNumber)
	      (build member *y class DivisorCandidate))
	cq (build act (build action build-divisor-list object1 *x)
		 plan (build action sniterate
			     object1 ((build 
                                     condition (build min 0 max 0 arg (build object divisor-list state built))
				     then (build action snsequence
					   object1 (build action check-divisible object1 *x object2 *y)		
					   object2 (build action increment object1 *y)
					   object3 (build action set-new-divisor-candidate)
					   object4 (build action update-divisor-candidate))
					           
				     ))
		      	             
          	      )
            )
)

;==============================================================
; build-divisor-lists
;==============================================================		
(assert forall ($x $y $z)
	&ant ((build member *x class NaturalNumber)
	      (build member *y class NaturalNumber))
	cq (build act (build action build-divisor-lists object1 *x object2 *y)
		 plan (build action snsequence
				object1 (build action believe
                                               object1 (build min 0 max 0 arg (build object divisor-list state built))
                                        )
				object2 (build action believe 
					       object1 (build member 1 class DivisorCandidate)
                                        )
				object3 (build action build-divisor-list object1 *x)
				object4 (build action believe 
					       object1 (build member 1 class DivisorCandidate)
                                        )
				object5 (build action build-divisor-list object1 *y)
				object6 (build action believe object1 (build object divisor-lists state found))
		      )
	   )
)

(assert goal (build object divisor-lists state found)
	plan (build action build-divisor-lists object1 (find (member- ! class) Input1)
					       object2 (find (member- ! class) Input2))
)

(assert member 1 class NaturalNumber)
;(assert member 9999 class CurrentRemainder)
(assert min 0 max 0 arg (build object divisor-lists state found))
(perform (build action achieve object1 (build object divisor-lists state found)))
;(perform (build action update-num-var object1 CurrentRemainder object2 (find (member- ! class) CurrentRemainder) object3 1))