Commits

Richard Lawrence  committed 4fa5262

Initial hack up: represent LSL formulae

  • Participants

Comments (0)

Files changed (2)

+*~
+#lang scheme
+;;;; LSL
+;; (define (expression? e)
+;;   (or (atomic-form? e)
+;;       (compound-form? e)))
+
+;; we treat formulae in a data-directed style:
+;; every formula knows its own type and how to evaluate and print itself
+
+;; a default printer: can handle atomic sentences and connectives of any arity
+(define (default-printer type slots)
+  (if (equal? type 'atom)
+      (symbol->string (car slots))
+      (string-append
+       (symbol->string type)
+       "("
+       (string-join (map print-form slots) ",")
+       ")")))
+
+;; a factory for printers of binary expressions: returns a printer
+;; that separates two sub-expressions with a string representing
+;; connective and surrounds the whole expression with parentheses
+(define (make-binary-printer connective left right)
+  (lambda ()
+    (string-append "(" (print-form left) connective (print-form right) ")")))
+
+;; functions for creating formulae in a truth-functional language
+(define (make-form type slots evaluator [printer #f])
+  (list type slots evaluator
+	(or printer
+	    (lambda () (default-printer type slots)))))
+(define (form-type form)
+  (car form))
+(define (form-slots form)
+  (cadr form))
+(define (form-evaluator form)
+  (caddr form))
+(define (form-printer form)
+  (cadddr form))
+(define (form-arity form)
+  (length (form-slots form)))
+(define (print-form form)
+  ((form-printer form)))
+(define (lookup a bindings)
+  (cadr (assoc a bindings)))
+(define (eval-form form bindings)
+  ((form-evaluator form) bindings))
+  
+(define (make-atomic-form a)
+  (make-form 'atom (list a) (lambda (bindings) (lookup a bindings))))
+(define (atomic-form? a)
+  (equal? (car a) 'atom))
+(define (make-neg-form a)
+  (make-form '~
+             (list a)
+             (lambda (bindings) (not (eval-form a bindings)))
+             (lambda () (string-append "~" (print-form a)))))
+(define (neg-form? a)
+  (equal? (car a) '~))
+(define (make-and-form left right)
+  (make-form '&
+	     (list left right)
+	     (lambda (bindings)
+	       (and (eval-form left bindings) (eval-form right bindings)))
+             (make-binary-printer " & " left right)))
+(define (and-form? a)
+  (equal? (car a) '&))
+(define (make-or-form left right)
+  (make-form 'v
+             (list left right)
+             (lambda (bindings)
+               (or (eval-form left bindings) (eval-form right bindings)))
+             (make-binary-printer " v " left right)))
+(define (or-form? a)
+  (equal? (car a) 'v))
+(define (make-if-form antecedent consequent)
+  (make-form 'if
+             (list antecedent consequent)
+             (lambda (bindings)
+               (or (not (eval-form antecedent bindings))
+                   (eval-form consequent bindings)))
+             (make-binary-printer " -> " antecedent consequent)))
+(define (if-form? a)
+  (equal? (car a) 'if))
+(define (make-iff-form left right)
+  (make-form 'iff
+             (list left right)
+             (lambda (bindings)
+               (let ((leftp (eval-form left bindings))
+                     (rightp (eval-form right bindings)))
+               (or (and leftp rightp) (and (not leftp) (not rightp)))))
+             (make-binary-printer " <-> " left right)))
+(define (iff-form? a)
+  (equal? (car a) 'iff))
+
+(define (compound-form? a)
+  (or
+   (neg-form? a)
+   (and-form? a)
+   (or-form? a)
+   (if-form? a)
+   (iff-form? a)))
+(define (binary-form? a)
+  (and (compound-form? a)
+       (not (neg-form? a))))
+
+;;; parsers
+(define *unary-connectives* (list "~"))
+(define *binary-connectives* (list "&" "v" "->" "<->"))
+