rewriting.rkt

#lang typed/racket/no-check


;;; Types

(define-type Expr (U Symbol Term))
(define-type Term (Pairof Symbol (Listof Expr)))

(define-type Strategy (-> Expr (Option Expr)))


;;; Conventions

; t is for the subject term
; u, v, w... are for auxilary terms 
; s and p, q, r... are for strategies


;;; Primitives (some of them, anyway)

(define-syntax-rule (rule pattern expr)
  (lambda (t)
    (match t
      [pattern expr]
      [_ #f])))

(define pass (rule x x))

(define fail (rule _ #f))

(define (pipe s p)
  (lambda (t)
    (let ([u (s t)])
      (if u         
          (p u)
          #f))))

(define (alt s . more)
  (lambda (t)
    (let ((u (s t)))
      (cond
        (u u)
        ((null? more) #f)
        (#t ((apply alt more) t))))))

(define term? list?) ; close enough

(define (all s)
  (lambda (t)
    (if (term? t)
      (let ([children (map s (cdr t))])
        (if (for/or ((u children))
              (eq? u #f))
            #f
            (cons (car t) children)))
      t)))


;;; A small subset of a "standard library"

(define (try s)
  (alt s pass))

(define (repeat s)
  (lambda (t)
    ((try (pipe s (repeat s))) t)))

(define (top-down s) ; for comparison, my examples don't use it
  (lambda (t)
    ((pipe s (all (top-down s))) t)))

(define (bottom-up s)
  (lambda (t)
    ((pipe (all (bottom-up s)) s) t)))

(define (innermost s)
  (lambda (t)
    ((bottom-up (try (pipe s (innermost s)))) t)))


;;; Example: Boolean expressions

(define evaluation
  (alt (rule `(not true) 'false)
       (rule `(not false) 'true)
       
       (rule `(and true ,x) x)
       (rule `(and ,x true) x)
       (rule `(and false ,x) 'false)
       (rule `(and ,x false) 'false)
       
       (rule `(or true ,x) 'true)
       (rule `(or ,x true) 'true)
       (rule `(or false ,x) x)
       (rule `(or ,x false) x)
       ))

(define evaluate (bottom-up (repeat evaluation)))

; (evaluate '(not true))
; (evaluate '(and true unknown))
; (evaluate '(and (not false) (or true whatever)))


;;; Example: Conjunctive Normal Form

(define double-negation
  (rule `(not (not ,a)) a))

(define de-morgan
  (alt (rule `(not (and ,a ,b))
             `(or (not ,a) (not ,b)))
       (rule `(not (or ,a ,b))
             `(and (not ,a) (not ,b)))))

(define distribute-or
  (alt (rule `(or (and ,a ,b) ,c)
             `(and (or ,a ,c) (or ,b ,c)))
       (rule `(or ,a (and ,b ,c))
             `(and (or ,a ,b) (or ,a ,c)))))

(define cnf
  (innermost (alt evaluation
                  double-negation
                  de-morgan
                  distribute-or)))

; (cnf '(not (or a b)))
; (cnf '(or (and a b) c))
; (cnf '(and a (or b (and d e))))
; (cnf '(and a (or true (and d e))))