[Small-cl-src] Pattern matching in function headers
Julian Stecklina
der_julian at web.de
Sat Jun 5 15:53:15 UTC 2004
Hello,
I had the idea to do pattern matching in function definitions as
Haskell allows. Any comments are welcome.
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: pmatch.lisp
URL: <https://mailman.common-lisp.net/pipermail/small-cl-src/attachments/20040605/394b6116/attachment.ksh>
-------------- next part --------------
(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 , at 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)))))))
-------------- next part --------------
Regards,
--
Julian Stecklina
Signed and encrypted mail welcome.
Key-Server: pgp.mit.edu Key-ID: 0xD65B2AB5
FA38 DCD3 00EC 97B8 6DD8 D7CC 35D8 8D0E D65B 2AB5
Any sufficiently complicated C or Fortran program
contains an ad hoc informally-specified bug-ridden
slow implementation of half of Common Lisp.
- Greenspun's Tenth Rule of Programming
More information about the Small-cl-src
mailing list