Commits

Richard Lawrence committed 6fc655b

core.ss
* Initial work on validity checker
* Initial work on parsers
* Some formulae defined for convenience while testing

  • Participants
  • Parent commits 4fa5262

Comments (0)

Files changed (1)

   (and (compound-form? a)
        (not (neg-form? a))))
 
+;;; validity checker
+;;(define (valid? form)
+;;  ())
+(define (member? form l)
+  (cond ((empty? l) #f)
+	((equal? form (car l)) #t)
+	(else (member? form (cdr l)))))
+      
+(define (atomic-forms form)
+  (atomic-forms-helper form '()))
+
+(define (atomic-forms-helper f seen-atoms)
+  (if (atomic-form? f)
+      (if (member? f seen-atoms)
+	  seen-atoms
+	  (cons f seen-atoms))
+      (atoms-from-list (form-slots f) seen-atoms)))
+
+(define (atoms-from-list forms seen-atoms)
+  (if (empty? forms)
+      seen-atoms
+      (let* ((f (car forms))
+	     (rest (cdr forms))
+             (f-atoms (atomic-forms-helper f seen-atoms)))
+	(atoms-from-list rest f-atoms))))
+        
+
 ;;; parsers
 (define *unary-connectives* (list "~"))
 (define *binary-connectives* (list "&" "v" "->" "<->"))
 
+(define (try) (error "Not implemented"))
+(define (read-formula s)
+  (try
+   (read-atomic-formula s)
+   (read-negated-formula s)
+   (read-binary-formula s)
+   (error "Could not parse an LSL formula")))
+
+(define (read-atomic-formula s)
+  ; get a single, non-whitespace character.  if it's an uppercase
+  ; letter, convert it to a symbol and create an atomic
+  ; formula. otherwise, fail without consuming input
+(error "Not implemented"))
+
+(define (read-negated-formula s)
+  ; get a single, non-whitespace character.  if it's a tilde, read a
+  ; formula. otherwise, fail without consuming input
+(error "Not implemented"))
+
+(define (read-binary-formula s)
+  ; get a single, non-whitespace character.  if it's an open paren, read a formula, then read a connective, then read a formula, then read a close paren.
+(error "Not implemented"))
+
+;;;; for tests
+(define A (make-atomic-form 'A))
+(define B (make-atomic-form 'B))
+(define C (make-atomic-form 'C))
+(define A&B (make-and-form A B))
+(define ~C (make-neg-form C))
+(define A->B (make-if-form A B))
+(define B<->~C (make-iff-form B ~C))
+(define AvC (make-or-form A C))