(in-package "ACL2")

(defun PinLang (x)
; returns T iff x is in language
	; check that length of x = 1, 2, or 4
	(if 
		(or (not (consp x))
			(not (or (equal (length x) 1)
			(equal (length x) 2)
			(equal (length x) 4))))
	nil
	;check that it's well-formed if so
	(cond 
		((equal '(t) x) T)
		((equal '(f) x) T)
		((equal '(0) x) T)
		; if length x = 2, then x is a succ, pred or iszero
		((and (equal (length x) 2)
			(or (equal (car x) 's)
			(equal (car x) 'p)
			(equal (car x) 'z)))
		(PinLang (cadr x)))
		; if it's length 4, then is an if
		((and (equal (car x) 'i)
			(equal (length x) 4))
		(and (PinLang (cadr x))
			(PinLang (caddr x))
			(PinLang (cadddr x))))
		(T nil))))

(defun PisNV (x)
;returns T iff x is a num val
	(cond
		((equal (length x) 1) (equal (car x) '0))
		((and (equal (length x) 2)
			(equal (car x) 's)
			(equal (length (cadr x)) 2))
		(PisNV (cadr x)))
	(T nil)))

(defun PisValue (x)
;returns T iff x is a value
	(if (PinLang x)
		(or 
			(equal '(t) x)
			(equal '(f) x)
			(PisNV x))
	nil))

(defun PStep (x)
	;returns the one-step evaluation of x
	(if (PinLang x) ; check that x is in the language
	(case (car x) ; case on the first call in x
		('t '(t)) ; t -> t
		('f '(f)) ; f -> f
		('0 '(0)) ; 0 -> 0
		; case that (car x) is p		
		('p 
			(cond
				; pred 0 -> 0
				((equal (cadr x) '(0)) '(0))
				; p (s nv) -> nv
				((and (equal 's (caadr x))
					(PisNV (cadadr x)))
				(cadadr x))
				; t -> t' then p t -> p t'
				(T (list 'p (PStep (cadr x))))))
		; case that (car x) is z
		('z
			(cond
				; z 0 -> T
				((equal (cadr x) '(0)) '(T))
				; z s 0 -> F
				((Pisnv (cadr x)) '(F))
				; t -> t' then z t -> z t'
				(T (list 'z (PStep (cadr x))))))
		; case that (car x) is s
		; t -> t' then s t -> s t'
		('s (list 's (PStep (cadr x))))
		; case that (car x) is i
		('i
			(cond
				; i (T) (a) (b) -> a
				((equal '(t) (cadr x)) (caddr x))
				; i (F) (a) (b) -> b
				((equal '(f) (cadr x)) (cadddr x))
				; t -> t' then i (t) (a) (b) -> i (t') (a) (b)
				(T (list 'i (PStep (cadr x))
					(caddr x) (cadddr x)))))
		(T nil)) ; else, cannot step
	nil)) ; not in language

(defun Ptype (x)
;returns 1 iff type of x is Bool
;returns 2 iff type of x is Nat
	(if (PinLang x)
	(cond 
		;type of t, f, 0 = 1, 1, 2		
		((equal '(t) x) 1)
		((equal '(f) x) 1)
		((equal '(0) x) 2)
		; if x is a pred or succ and
		; if the cadr is a nat, then type x = 2
		((and 
			(or 
				(equal (car x) 's)
				(equal (car x) 'p))
			(equal (Ptype (cadr x)) 2))
			2)
		; if x is a iszero and 
		; cadr is type 2, then type x is 1
		((and 
			(equal (car x) 'z)
			(equal (Ptype (cadr x)) 2))
			1)
		; if x is an if
		; if type gaurd is 1 and type of branches is equal
		; if type of branches are non-nil, type x = type of branch
		((and
			(equal (car x) 'i)
			(equal (ptype (cadr x)) 1)
			(equal (ptype (caddr x)) (ptype (cadddr x))))
		(ptype (caddr x)))
		(T nil)) ; nothing else is well-typed
	nil)) ;not in lang

(defthm progress (implies (or 
				(equal (ptype x) 1)
				(equal (ptype x) 2))
			(not (equal (pstep x) nil))))

(defthm preservation (implies (and (or 
					(equal (ptype x) 1)
					(equal (ptype x) 2))
				(not (equal (pstep x) nil)))
			(equal (ptype (pstep x)) (ptype x))))

(defthm soundness (implies (or 
				(equal (ptype x) 1)
				(equal (ptype x) 2))
			(equal (ptype x) (ptype (pstep x)))))