l-interpreter.bak

#lang rosette

(require rosette/lib/angelic)

(provide find-from-states)

; an L-system is defined by a list of successors for corresponding alphabet
; an L-system can be interpreted with an initial state as input

(define (make-symbolic-successors alphabet successors)
  (map (lambda (symbol) (apply choose* successors)) alphabet))

(define (interpret successors state iterations)
  (define result (list))
  (for-each (lambda (iteration)
              (set! result (append-map (lambda (symbol)
                                         (list-ref successors symbol))
                                       state))))
  result)

(define (solve-two-states initial-state successors final-state)
  (solve (assert (equal? (interpret successors initial-state) final-state))))

(define (solve-states states successors)
  (define index 0)
  (for-each (lambda (state)
              (when (not (= index (- (length states) 1)))
                (assert (equal? (interpret successors (car state) (range (- (cdr (list-ref states (+ index 1))) (cdr state)))) (car (list-ref states (+ index 1))))))
              (set! index (+ index 1)))
            states)
  (solve (assert #t)))

(define (find-from-states states alphabet successors)
  (define symbolic-successors (make-symbolic-successors alphabet successors))
  (define actual-successors (evaluate symbolic-successors (solve-states states symbolic-successors)))
  actual-successors)