(defpackage :pattern-matching-examples
  (:nicknames "PMATCH-EXAMPLES")
  (:use "CL" "PATTERN-MATCHING"))
(in-package "PMATCH-EXAMPLES")

;;; Ok, let's do something funky! Hölli, beware!

;; Implement some predicate logic stuff *g*

;; We need some basic predicates
(defun binaryp (x)
  "Checks whether the argument is a binary operator"
  (funcall (one-of and or) x))

(defun operatorp (x)
  "Checks whether the argument is an operator"
  (funcall (one-of and or not) x))

(defun quantorp (x)
  "Checks whether the argument is a quantor"
  (funcall (one-of forall exists) x))

;; Translate an expression into a very simple form with only unary
;; and binary operators (NOT/AND/OR).
(defh simplify-expression
  ;; 'Implies' and 'Equiv'(valence)
  (implies ?expr1 ?expr2) -> `(or (not ,(simplify-expression expr1)) ,expr2)
  (equiv ?expr1 ?expr2) -> `(or (and expr1 expr2) (not (or expr1 expr2)))

  ;; Pass on quantors
  (?(quantor #'quantorp) ?var ?expr) -> `(,quantor ,var ,(simplify-expression expr))
  
  ;; Pass on unary and binary operators
  (not ?expr) -> `(not ,(simplify-expression expr))
  (?(op #'binaryp) ?expr1 ?expr2) -> `(,op ,(simplify-expression expr1)
					   ,(simplify-expression expr2))

  ;; Reduce not-binary operators to binary
  (?(op #'binaryp) ?expr1 . ?rest) -> `(,op ,expr1 (,op ,@rest))
  
  ;; Ignore non-matching
  ?expr -> expr)

;;; We now assume that every expression consists only of NOT/AND/OR with 
;;; atmost two arguments.

;; Perform one praenex transformation step
(defh praenex-transform
  ;; Transform negated quantors
  (not (forall ?var ?expr)) -> `(exists ,var ,(praenex `(not ,expr)))
  (not (exists ?var ?expr)) -> `(forall ,var ,(praenex `(not ,expr)))

  ;; "Lift" a quantor one level
  (?(op #'binaryp) (?(quantor #'quantorp) ?var ?expr1) 
                   ?expr2) 
     -> `(,quantor ,var ,(praenex `(,op ,expr1 
					,expr2)))
  (?(op #'binaryp) ?expr1
                   (?(quantor #'quantorp) ?var ?expr2))
     -> `(,quantor ,var ,(praenex `(,op ,expr1
					,expr2)))
  
  ;; Ignore anything else
  ?expr -> expr)
     
;; Transform an expression into praenex normal form
(defh praenex
  ;; Transform a negated expression
  (not ?expr) -> (praenex-transform `(not ,(praenex expr)))

  ;; Ignore a quantor where it does not hurt
  (?(quantor #'quantorp) ?var ?expr) -> `(,quantor ,var ,(praenex expr))

  ;; Transform 
  (?(op #'binaryp) ?expr1 ?expr2) -> (praenex-transform `(,op ,(praenex expr1)
							      ,(praenex expr2)))
  ?expr -> expr)

;; Perform one skolem transformation step
(defh skolem-transform
  (forall ?var ?expr) ?subst ?vars -> `(forall ,var ,(skolem-transform expr subst (cons var vars)))
  (exists ?var ?expr) ?subst ?vars -> (skolem-transform expr (acons var `(,(gentemp "SKOLEM") ,@(reverse vars)) subst)
					      vars)

  ;; Transform AND/OR/NOT/predicates/functors
  (?op . ?exprs) ?subst ?vars -> `(,op ,@(loop 
					   for expr in exprs
					   collect (skolem-transform expr subst vars)))
 
  ?expr ?subst ?vars -> (aif (subst (assoc expr subst))
			     (cdr subst)
			     expr))

;; Skolemize an expression in praenex normal form
(defh skolem
  ?expr -> (skolem-transform expr nil nil))

;; We would transform an arbitrary expression like this:
#+ ignore
(skolem (praenex (simplify-expression '(implies (and (p 0) (forall x (implies (p x) (p (f x)))))
						(p (f (f 0)))))))