Paste number 55875: Pattern Matching via Eliminators

Paste number 55875: Pattern Matching via Eliminators
Pasted by: faxathisia
6 months, 1 week ago
#lispcafe | Context in IRC logs
Paste contents:
Raw Source | XML | Display As
;;;; Pattern matching as sugar via eliminators

;; tools to store/lookup types

(defparameter *data-types* nil)

(defun data-name (data) (caadr data))
(defun data-quantifiers (data) (cdadr data))
(defun data-constructors (data) (cddr data))
(defun constructor-name (constructor) (car constructor))
(defun constructor-quantifiers (constructor) (cdr constructor))

(defmacro data (&whole whole
                (name &rest quantifiers) &body constructors)
  (declare (ignore name quantifiers constructors))
  `(progn
    (new-data ',whole)
    ,(compute-eliminator-term whole)))

(defun new-data (data) (push (cons (data-name data) data) *data-types*))

(defun data-assoc (data-name) (cdr (assoc data-name *data-types*)))

(defun constructor-data (constructor)
  (loop for data in *data-types*
        when (find constructor (mapcar #'constructor-name (data-constructors (cdr data))))
          do (return (data-name (cdr data)))))


;; You can compute the type of an eliminator for a data decl. in a syntax directly way
;; The idea behind this is that a macro would do purely syntactic transforming before the
;;  resulting lambda term is type checked

(defun compute-eliminator-type (data)
  (let ((quantifiers (data-quantifiers data))
        (return-type :z))
    `(forall (,@quantifiers ,return-type)
             (-> ,@(mapcar #'(lambda (constructor)
                               (let ((quantifiers (constructor-quantifiers constructor)))
                                 (if (zerop (length quantifiers))
                                     return-type
                                     `(-> ,@quantifiers ,return-type))))
                           (data-constructors data))
                 ,(list* (data-name data) quantifiers)
                 ,return-type))))

(defun eliminator-name (data-name)
  (intern (string-upcase (format nil "~a-elim" data-name))))

(defun compute-eliminator-term (data)
  "This creates a CL defun we can use to test the pattern matching."
  (let ((cs (loop repeat (length (data-constructors data)) collect (gensym "cont")))
        (elim-name (eliminator-name (data-name data))))
    `(defun ,elim-name (,@cs object)
       (case (car object)
         ,@(mapcar #'(lambda (constructor cont)
                       (let ((parameters (loop for i from 1 below (length constructor)
                                            collect `(elt object ,i))))
                         (list (car constructor)
                               `(funcall ,cont ,@parameters))))
                   (data-constructors data) cs)))))


(data (bool)
  (true) (false))

(data (nat)
  (zero) (succ (nat)))

(data (maybe :a)
  (nothing) (just :a))

(data (either :a :b)
  (left :a) (right :b))

(data (product :a :b)
  (pair :a :b))

(data (list :a)
  ([]) (cons :a (list :a)))




(defun unbox-data (constructor-pattern)
  "The head constructor has been matched so take it down a stage"
  ;; TODO: double check this is right, I'm suspicious of the /= 1 case
  ;;       is there an example which shows this is wrong?
  `(,(if (= 1 (caar constructor-pattern))
         (cons (length (cdadar constructor-pattern))
               (cdadar constructor-pattern))
         (cons (1- (caar constructor-pattern))
               (cddar constructor-pattern)))
     ,@(cdr constructor-pattern)))


(defun group-patterns (patterns)
  (let ((constructor-patterns (remove-if-not #'consp patterns :key #'cadar))
        (variable-patterns (remove-if #'consp patterns :key #'cadar)))
    (if (/= 0 (length variable-patterns)) (error "impossible"))
    (let* ((head-terms (mapcar #'caadar constructor-patterns))
           (head-types (mapcar #'constructor-data head-terms)))
      (if (not (every #'(lambda (type) (equal (first head-types) type)) (rest head-types)))
          (error "Type mishmash")
          (let ((groups (mapcar #'constructor-name (data-constructors (data-assoc (first head-types))))))
            (values (first head-types)
                    (mapcar #'(lambda (group)
                                (mapcar #'unbox-data
                                        (remove-if-not #'(lambda (constructor)
                                                           (equal (caadar constructor) group))
                                                       constructor-patterns)))
                            groups)))))))

;; Desugaring a match expressing into calls to eliminators
(defun expand-match (objects)
  (lambda (patterns)
    (let ((arity (- (caar (first patterns)) (length objects))))
      (cond ((and (= 1 (length patterns))
                  (= 0 arity))
             `(lambda () ,@(cdr (first patterns))))
        
            ((and (= 1 (length patterns))
                  (= 1 arity)
                  (atom (cadar (first patterns))))
             (let ((variable (cadar (first patterns))))
               `(lambda (,variable) ,@(cdr (first patterns)))))
            
            (t (let* ((gen-objects (loop repeat arity collect (gensym "object")))
                      (objects (append objects gen-objects)))
                 (multiple-value-bind (type groups) (group-patterns patterns)
                   `(lambda (,@gen-objects)
                      (,(eliminator-name type)
                        ,@(mapcar (expand-match (rest objects)) groups) ;; these guys need to be using the gensyms
                        ,(first objects))))))))))

(defmacro match (object &body patterns)
  (flet ((numberate (pattern)
           `(,(list 1 (car pattern))
              ,@(cdr pattern))))
    `(funcall ,(funcall (expand-match nil) (mapcar #'numberate patterns))
              ,object)))



(defun tests ()
  (flet ((counter (number)
           (match number
             ((zero) "0")
             ((succ (zero)) "1")
             ((succ (succ (zero))) "3")
             ((succ (succ (succ (zero)))) "4")
             ((succ (succ (succ (succ x))))
              (declare (ignore x))
              "5+")))
         (composite (thing)
           (match thing
             ((just (left (true))) 1)
             ((just (left (false))) 2)
             ((just (right (zero))) (list '- 3))
             ((just (right (succ n))) (list 4 n))
             ((nothing) 0)))
         (pairs (foo)
           (match foo
             ((pair (true) _) "(true, *)")
             ((pair (false) (true)) "(false, true)")
             ((pair (false) (false)) "(false, true)"))))
    (list (match '(true)
            ((true) "true")
            ((false) "false"))
          (match '(false)
            ((true) "true")
            ((false) "false"))
          (counter '(zero))
          (counter '(succ (zero)))
          (counter '(succ (succ (zero))))
          (counter '(succ (succ (succ (zero)))))
          (counter '(succ (succ (succ (succ (succ (zero)))))))
          (composite '(just (left (true))))
          (composite '(just (left (false))))
          (composite '(just (right (zero))))
          (composite '(just (right (succ (succ (succ zero))))))
          (pairs '(pair (true) (true)))
          (pairs '(pair (true) (false)))
          (pairs '(pair (false) (true)))
          (pairs '(pair (false) (false))))))
;; ("true" "false" "0" "1" "3" "4" "5+" 1 2 (- 3) (4 (SUCC (SUCC ZERO)))
;;  "(true, *)" "(true, *)" "(false, true)" "(false, true)")


#||
(defparameter ex1 (match foo
                    ((true) "true")
                    ((false) "false")))
;;(FUNCALL
;; (LAMBDA (#:|object374|)
;;   (BOOL-ELIM (LAMBDA () "true") (LAMBDA () "false") #:|object374|))
;; FOO)
;; +ok

(defparameter ex2 (match foo
                    ((zero) "0")
                    ((succ (zero)) "1")
                    ((succ (succ (zero))) "3")
                    ((succ (succ (succ (zero)))) "4")
                    ((succ (succ (succ (succ x)))) "5+")))
;;(FUNCALL
;; (LAMBDA (#:|object379|)
;;   (NAT-ELIM (LAMBDA () "0")
;;             (LAMBDA (#:|object380|)
;;               (NAT-ELIM (LAMBDA () "1")
;;                         (LAMBDA (#:|object381|)
;;                           (NAT-ELIM (LAMBDA () "3")
;;                                     (LAMBDA (#:|object382|)
;;                                       (NAT-ELIM (LAMBDA () "4")
;;                                                 (LAMBDA (X) "5+")
;;                                                 #:|object382|))
;;                                     #:|object381|))
;;                         #:|object380|))
;;             #:|object379|))
;; FOO)
;; +ok

(defparameter ex2b (match foo
                     ((zero) "o")
                     ((succ x) (cons x "o"))))
;;(FUNCALL
;; (LAMBDA (#:|object384|)
;;   (NAT-ELIM (LAMBDA () "o") (LAMBDA (X) (CONS X "o")) #:|object384|))
;; FOO)
;; +ok

(defparameter ex3 (match foo
                    ((just (left (true))) 1)
                    ((just (left (false))) 2)
                    ((just (right (zero))) (list '- 3))
                    ((just (right (succ n))) (list 4 n))
                    ((nothing) 0)))
;;(FUNCALL
;; (LAMBDA (#:|object397|)
;;   (MAYBE-ELIM (LAMBDA () 0)
;;               (LAMBDA (#:|object398|)
;;                 (EITHER-ELIM
;;                  (LAMBDA (#:|object399|)
;;                    (BOOL-ELIM (LAMBDA () 1) (LAMBDA () 2) #:|object399|))
;;                  (LAMBDA (#:|object400|)
;;                    (NAT-ELIM (LAMBDA () (LIST '- 3)) (LAMBDA (N) (LIST 4 N))
;;                              #:|object400|))
;;                  #:|object398|))
;;               #:|object397|))
;; FOO)
;; +ok


(defparameter ex4 (match foo
                    ((pair (true) x) "a")
                    ((pair (false) (true)) "b")
                    ((pair (false) (false)) "c")))
;;(FUNCALL
;; (LAMBDA (#:|object389|)
;;   (PRODUCT-ELIM
;;    (LAMBDA (#:|object390| #:|object391|)
;;      (BOOL-ELIM (LAMBDA (X) "a")
;;                 (LAMBDA (#:|object392|) <---- should not take a parameter
;;                   (BOOL-ELIM (LAMBDA () "b") (LAMBDA () "c") #:|object392|)) <---- should use 391 not 392
;;                 #:|object390|))
;;    #:|object389|))
;; FOO)
;; -broken ++++++ fixed now

||#

This paste has no annotations.

Colorize as:
Show Line Numbers

Ads absolutely not by Google

Lisppaste pastes can be made by anyone at any time. Imagine a fearsomely comprehensive disclaimer of liability. Now fear, comprehensively.