(in-package "ACL2")

(defun PisNumVal (x loc)
;;checks if a string is a nv starting at a location and moving to the left
;;just a helper function
    (if (not(and (< loc (length x))
		 (integerp loc)
		 (stringp x) 
		 (> loc -1)))
	nil
      (if (and (equal loc 0)
	       (string-equal "0" (string(char x (- (length x) 1)))))
	       T
          (if (and 
	       (string-equal "s" (string(char x (- (- (length x) loc) 1))))
	       (> loc 0))
	      (PisNumVal x (+ -1 loc))
	    nil))))

(defun PisNV (x)
;;checks if x is a num val
    (PisNumVal x (- (length x) 1)))

(defun PisValue (x)
;;checks if x is a value
    (if (or (string-equal "T" x)
	    (string-equal "F" x)
	    (PisNV x))
	T
      nil))

(defun LocBegLastSeg (x loc opens)
;;locates the opening parens associated with a closing parens
;;just a helper
  (if (not (stringp x))
      nil
    (if (not(and (< loc (length x))
		 (integerp loc)
		 (stringp x) 
		 (> loc 0)))
	nil
    (if (equal opens 0)
	(+ 2 loc)
    (if (string-equal "(" (string(char x loc)))
	(locbeglastseg x (- loc 1) (+ (- 1) opens))
    (if (string-equal ")" (string(char x loc)))
	(locbeglastseg x (- loc 1) (+ opens 1))
    (locbeglastseg x (- loc 1) opens)))))))

(defun Pelse (x)
;;returns the 'else' part of a conditional
    (subseq 
	     x 
	     (locbeglastseg x (- (length x) 2) 1) 
	     (- (length x) 1)))

(defun Pthen (x)
;;returns the 'then' part of a conditional
    (subseq 
	     x 
	     (locbeglastseg x (- (length x) (+ (length (pelse x)) 4)) 1) 
	     (- (length x) (+ (length (pelse x)) 3)
	     )))

(defun Pguard (x)
;;returns the guard of a conditional
    (subseq  x 
	     2
	     (- (locbeglastseg x (- (length x) (+ (length (pelse x)) 4)) 1) 2)
	     ))

(defun Psubterm (x)
;;returns the subterm of a non-conditional
  (if (not (stringp x))
      nil
    (subseq x 1 (length x))))

(defun PinLang (x)
;;test if x is in the lang
  (cond ( (string-equal "t" x) T )
	( (string-equal "f" x) T )
	( (string-equal "0" x) T )
	( (and (> (length x) 1)
	       (> (length x) (length (psubterm x))))
	    (case (char x 0)
		  ( #\s (PinLang (psubterm x)) )
		  ( #\p (PinLang (psubterm x)) )
		  ( #\z (PinLang (psubterm x)) )
		  ( #\i (if (and (> (length x) (length (pguard x)))
				 (> (length x) (length (pthen x)))
				 (> (length x) (length (pelse x))))
			    (and (PinLang(Pguard x))
				 (PinLang(Pthen x))
				 (PinLang(Pelse x)))
			  nil))
		  (otherwise nil)))))

(defun Pstep (x)
;;one step evaluates x
    (declare (xargs :measure (acl2-count x)))
    (case (char x 0)
	  (#\p 
	   (cond ((or (not (> (length x) 1))
		      (>= (length (psubterm x)) (length x)))
		  nil)
		 ((string-equal "p0" x)
		  "0")
		 ((and (equal #\s (char (psubterm x) 0))
		       (> (length x) 2)
		       (PisNV (psubterm (psubterm x))))
		   (psubterm (psubterm x)))
		(T (concatenate 'string "p" (pstep (psubterm x))))))
	  (#\z 
	   (cond ((or (not (> (length x) 1))
		  (>= (length (psubterm x)) (length x)))
		  nil)
		 ((string-equal "z0" x)
		  "t")
		 ((Pisnv (psubterm x))
		  "f")
		 (T (concatenate 'string "z" (pstep (psubterm x))))))
	  (#\s 
	   (cond ((or (not (> (length x) 1))
		(>= (length (psubterm x)) (length x)))
		  nil)
		 (T (concatenate 'string "s" (pstep (psubterm x))))))
	  (#\i 
	   (cond ((>= (length (pguard x)) (length x))
		  nil)
		 ((equal #\t (char x 2))
		  (pthen x))
		 ((equal #\f (char x 2))
		  (pelse x))
		 (T (concatenate 'string "i("
			      (pstep (pguard x))
			      ")("
			      (pthen x)
			      ")("
			      (pelse x) 
			      ")"))))
		     ))

(defun Ptype (x)
;;returns the type of x
  (cond ((not (stringp x)) nil)
	((string-equal "t" x) "Bool")
	((string-equal "f" x) "Bool")
	((string-equal "0" x) "Nat")
	((and (equal #\i (char x 0))
	      (not (or (>= (length (pguard x)) (length x))
		       (>= (length (pelse x)) (length x))
		       (>= (length (pthen x)) (length x)))))
	 (cond ((and (string-equal (ptype (pguard x)) "Bool")
		     (string-equal (ptype (pelse x)) (ptype (pthen x)))
		     (not (equal (ptype (pelse x)) nil)))
		(ptype (pelse x)))))
	((and (equal #\s (char x 0))
	      (not (or (not (> (length x) 1))
		       (>= (length (psubterm x)) (length x))
		       (not (stringp x)))))
	 (cond ((string-equal (ptype (psubterm x)) "Nat")
		"Nat")))
	((and (equal #\p (char x 0))
	      (not (or (not (> (length x) 1))
		       (>= (length (psubterm x)) (length x))
		       (not (stringp x)))))
	      (cond ((string-equal (ptype (psubterm x)) "Nat")
	 "Nat")))
	((and (equal #\z (char x 0))
	      (not (or (not (> (length x) 1))
		       (>= (length (psubterm x)) (length x))
		       (not (stringp x)))))
	      (cond ((string-equal (ptype (psubterm x)) "Nat")
	 "Bool")))
     ))