;;; 0CFA analysis, based on Nielson & Nielson 97.

;;; This is a straightforward 0CFA.  It uses NN97's distinction
;;; between expressions and terms.  It also uses NN97's lazy analysis
;;; of abstraction bodies.

;;; This should be moderately portable.  It uses Chez idioms for
;;; error, printf, and pretty-print, but should be otherwise standard,
;;; I think.

;;; Setting *trace* to #t will let you watch inclusions and insertions
;;; as they happen.  Toggle it with (toggle-trace) .

;;; Revision History:

;;; 0.9.4 Thu Dec 12 10:57:11 1996 Will Clinger pointed out that nil
;;; should be changed to '();  (null? v) in node->struct should have
;;; been (not ans).

(let ((version "0.9")
      (release 4)
      (date    "Thu Dec 12 10:55:43 1996"))
  (printf "cfa.scm version ~d.~d ~d~%" version release date))

;;; exp ::= term * label
;;; term ::= var of id | fun of var * exp | app of exp * exp

(define analyze!
  (lambda (exp)
    (split-exp exp
      (lambda (term l)
        (if (not (analyzed? l))
          (begin
            (mark-analyzed! l)
            (term-case term
              ;; a variable:       rho^(x) \subset ;  C^(l)
              (lambda (x) (insert-inclusion! x l))
              ;; a lambda:         (fn x body)^l \in C^(l)
              (lambda (var body-exp) (insert-element! l l))
              ;; an application:
              (lambda (rator-exp rand-exp)
                (analyze! rator-exp)
                (analyze! rand-exp)
                (split-exp rator-exp
                  (lambda (rator-term rator-label)
                    (split-exp rand-exp
                      (lambda (rand-term rand-label)
                        (for-each-abstraction-label
                          (lambda (abstraction-label)
                            (insert-conditional-inclusion!
                              abstraction-label rator-label
                              (lambda ()
                                (split-abstraction abstraction-label
                                  (lambda (bvar body-exp)
                                    (split-exp body-exp
                                      (lambda (body-term body-label)
                                        (analyze! body-exp)
                                        ; C^(l2) \subset rho^(x) sdf
                                        (insert-inclusion! rand-label bvar) 
                                        ; C^(l0) \subset C^(l)
                                        (insert-inclusion! body-label l) 
                                        ))))))))))))))))))))


;;; ****************************************************************

;;; abstract closure-solving algorithm, based on Palsberg and Schwartzbach.

;;; maintain a graph, with each node corresponding to a set.
;;; for each node x, maintain:
;;;  -- members of x    
;;;     interface:   (member-of? i x) (for-each-member x fn) add-member!
;;;  -- successors of x
;;;     interface:   (successor-of? x y) (for-each-successor x fn)
;;;                  add-successor! 
;;;  -- hypothetical constraints of x:
;;;     {(y,z)| "i \in x => (thunk)" has been asserted"}
;;;     maintained as a list of thunks.
;;;     This only makes sense for i \not in x
;;;     interface:
;;;             (add-hypothetical-constraint! i x thunk)
;;;             (for-each-hypothetical-constraint x i fn)  
;;;              --this arg order seems better to me, even tho it's
;;;                inconsistent. 
;;;             (discharge-hypothetical-constraints! x i) -- makes it empty


;;; the following routines take a consistent graph and add new
;;; constraints, solving as you go.

(define insert-element!
  (lambda (element set)                 ; add element to set, and see
                                        ; what follows
    (if (not (member-of? element set))
      (begin
        (add-member! element set)
        (if *trace* (printf "add-member! ~d ~d~%" element set))
        (for-each-successor set                       ;; follow inclusion
          (lambda (set2) (insert-element! element set2)))
        (for-each-hypothetical-constraint set element
          ;; run each hypothetical thunk
          (lambda (constraint-thunk) (constraint-thunk)))
        (discharge-hypothetical-constraints! set element) ; probably not needed
        ))))

(define insert-inclusion!
  (lambda (set1 set2)
    (if (not (successor-of? set1 set2))
      (begin
        (add-successor! set1 set2)
        (if *trace* (printf "add-inclusion! ~d ~d~%" set1 set2))
        (for-each-member set1
          (lambda (i) (insert-element! i set2)))))))

(define insert-conditional-inclusion!
  (lambda (element set1 thunk)
    ;; add "el \in set1 => (thunk)"
    (if (member-of? element set1)
      (thunk)
      (add-hypothetical-constraint! element set1 thunk))))

;; thunk is typically (lambda () (insert-inclusion! set1 set2))

;;; ****************************************************************

;;; Data structures for graphs and sets:

;;; Graph: global map *graph* :  (symbols | integers) -> node-struct 
;;;   represented as (alist of symbol*node-struct . vector of node-struct) 
;;; node-struct = (vector-of-members  list-of-successors
;;;                vector-of-hypotheticals) 

;;; Members are always abstractions, represented by their indices.

;;; these structures will be built as we go.

(define *graph* '())

;;; top level of the graph:

(define node->struct
  (lambda (v)
    (if (symbol? v)
      (let ((ans (assq v (car *graph*))))
        (if (not ans)
          (error 'node->struct "unknown node ~s" v)
          (cdr ans)))
      (if (and (number? v) (< v (vector-length (cdr *graph*))))
        (vector-ref (cdr *graph*) v)
        (error 'node->struct "unknown node ~s" v)
        ))))

(define pretty-print-node
  (lambda (node)
    (display node)
    (display ":  Members: ")
    (for-each-member node (lambda (i) (display i)(display " ")))
    (newline)
    (display "    Successors: ")
    (for-each-successor node (lambda (i) (display i)(display " ")))
    (newline)))

(define print-graph
  (lambda ()
    (for-each 
      (lambda (pair)
        (let ((node (car pair)))
          (pretty-print-node node)))
      (car *graph*))
    (let ((n (vector-length (cdr *graph*))))
      (do ((i 0 (+ i 1)))
          ((= i n))
          (pretty-print-node i)))))

;;; node structures:

(define struct->members car)
(define struct->successors cadr)
(define struct->hypotheticals caddr)

(define make-struct
  (lambda (size)
    (list
      (make-vector size #f)             ; bitvector of members
      '()                               ; list of successors
      (make-vector size '())            ; vector of hypotheticals
      )))

;;; members:

(define member-of? 
  (lambda (i x)
    (let ((struct (node->struct x)))
      (vector-ref (struct->members struct) i))))

(define (for-each-member x fn)
  (let ((members (struct->members (node->struct x))))
    (let ((n (vector-length members)))
      (do ((i 0 (+ i 1)))
          ((= i n))
          (if (vector-ref members i) (fn i))))))


(define add-member!
  (lambda (i x)
    (let ((members (struct->members (node->struct x))))
      (vector-set! members i #t))))

;;; successors -- just a list of (index | symbol)

(define (successor-of? x y)             ; is y a successor of x?
  (let ((struct (node->struct x)))
    (memv y (struct->successors struct))))

(define (for-each-successor x fn)
  (let ((successors (struct->successors (node->struct x))))
    (for-each fn successors)))

(define add-successor!
  (lambda (x y)                         ; make y a successor of x. 
    (let ((successors (struct->successors (node->struct x))))
      (if (not (memv y successors))
        (set-car! (cdr (node->struct x)) (cons y successors))))))

;;; hypotheticals are a little different, since they are doubly
;;; indexed.  They are kept as a vector of list of thunk.

(define add-hypothetical-constraint!
  (lambda (i x thunk)
    (let ((hypotheticals (struct->hypotheticals (node->struct x))))
      (let ((thunks (vector-ref hypotheticals i)))
        (vector-set! hypotheticals i (cons thunk thunks))))))

(define for-each-hypothetical-constraint
  (lambda (x i fn)
    (let ((hypotheticals (struct->hypotheticals (node->struct x))))
      (let ((thunks (vector-ref hypotheticals i)))
        (for-each
          (lambda (thunk) (fn thunk))
          thunks)))))

(define discharge-hypothetical-constraints!
  (lambda (x i)
    (let ((hypotheticals (struct->hypotheticals (node->struct x))))
      (let ((thunks (vector-ref hypotheticals i)))
        (vector-set! hypotheticals i '())))))

;;; ****************************************************************

;;; Data structures for terms and expressions

;;; exp = (label . term)
;;; term = ('var sym) | ('fn id exp) | ('app exp exp)

(define split-exp
  (lambda (exp fn)                      ; fn is (lambda (term l) ...)
    (fn (cdr exp) (car exp))))

(define make-exp cons)                 ; (build-exp label term)

(define term-case
  (lambda (term var-fcn fn-fcn app-fcn)
    (case (car term)
      ((var) (var-fcn (cadr term)))
      ((fn)  (fn-fcn (cadr term) (caddr term)))
      ((app) (app-fcn (cadr term) (caddr term)))
      (else (error 'term-case "unknown term ~s" term)))))

;;; split-abstraction and for-each-abstraction-label are dealt with
;;; where we build the term structures

;;; ****************************************************************

;;; Parsing input expressions and building term structures

(define *all-abstractions* '())
(define *analyzed* '())

;;; input expressions:

;;; exp = var | (lambda (var) exp) | (exp exp)

;;; we should curry these on the fly, as well as alpha-convert, but
;;; not for this version.

(define build-exp                      ; returns pair (term, max-label)
  (lambda (exp)                         ; an external expression!
    (let*
      ((label 0)                        ; first unused label
       (genlabel (lambda () 
                   (let ((ans label))
                     (set! label (+ 1 label))
                     ans)))
       (make-exp (lambda (x) (make-exp (genlabel) x)))
       (exp
         (let loop ((exp exp))
           (cond
             ((symbol? exp) (make-exp (list 'var exp)))
             ((eq? (car exp) 'lambda)
              (if (= (length (cadr exp)) 1)
                (make-exp
                  (list 'fn (car (cadr exp)) (loop (caddr exp))))
                (error "build-term: multiple arguments found: ~s"
                       exp)))
             ((= (length exp) 2)
              (make-exp
                (list 'app
                      (loop (car exp))
                      (loop (cadr exp)))))
             (else 
               (error "build-exp: can't deal with ~s" exp))))))
      (cons exp label))))

(define initialize-graph!
  (lambda (exp max-label)
    (let*
      ((size max-label)
       (vars (all-vars exp))
       (a-list (map (lambda (var)
                      (cons var (make-struct size)))
                    vars))
       (vec (make-vector size)))
      (do ((i 0 (+ i 1)))
          ((= i size))
          (vector-set! vec i (make-struct size)))
      (set! *graph* (cons a-list vec)))))

(define all-vars
  (lambda (exp)
    (let loop ((exp exp) (vars '()))    ; computes allvars(exp) U vars
      (split-exp exp
        (lambda (term label)
          (term-case term
            (lambda (var)
              (if (memq var vars) vars (cons var vars)))
            (lambda (var body)
              (loop body
                    (if (memq var vars) vars (cons var vars))))
            (lambda (rator rand)
              (loop rator
                    (loop rand vars)))))))))

;;; *all-abstractions* = vector of (expression | #f)

(define initialize-abstractions!
  (lambda (exp max-label)
    (set! *all-abstractions* (make-vector max-label #f))
    (let loop ((exp exp))
      (split-exp exp
        (lambda (term label)
          (term-case term
            (lambda (var) #t)
            (lambda (var body)
              (vector-set! *all-abstractions* label exp)
              (loop body))
            (lambda (rator rand)
              (loop rator)
              (loop rand))))))))

(define for-each-abstraction-label
  (lambda (fn)
    (let ((size (vector-length *all-abstractions*)))
      (do ((i 0 (+ 1 i)))
          ((= i size))
          (let ((exp-or-f (vector-ref *all-abstractions* i)))
            (if exp-or-f (fn i)))))))

(define split-abstraction
  (lambda (label fn)  ;; fn is (lambda (bar body-exp) ...)
    (let ((term (vector-ref *all-abstractions* label)))
      (fn (caddr term) (cadddr term)))))

;;; *analyzed* : vector of boolean

(define initialize-analyzed!
  (lambda (size)
    (set! *analyzed* (make-vector size #f))))

(define analyzed?
  (lambda (label)
    (vector-ref *analyzed* label)))

(define mark-analyzed!
  (lambda (label)
    (vector-set! *analyzed* label #t)))

(define *trace* #f)

(define toggle-trace
  (lambda () (set! *trace* (not *trace*))))

(define run
  (lambda (external-term)
    (let*
      ((exp-and-label (build-exp external-term))
       (exp           (car exp-and-label))
       (size          (cdr exp-and-label))
       (term          (split-exp exp (lambda (term label) term))))
      (initialize-graph! exp size)
      (initialize-abstractions! exp size)
      (initialize-analyzed! size)
      (pretty-print exp)
      (analyze! exp)
      (print-graph))))

; > (load "cfa.scm")
; cfa.scm version 0.8.2 Wed Dec 11 14:37:25 1996
; > (run '((lambda (x) (x x)) (lambda (y) (y y))))
; (8 app
;    (3 fn x (2 app (0 var x) (1 var x)))
;    (7 fn y (6 app (4 var y) (5 var y))))
; x:  Members: 7 
;     Successors: 1 0 
; y:  Members: 7 
;     Successors: 5 4 
; 0:  Members: 7 
;     Successors: 
; 1:  Members: 7 
;     Successors: y 
; 2:  Members: 
;     Successors: 8 
; 3:  Members: 3 
;     Successors: 
; 4:  Members: 7 
;     Successors: 
; 5:  Members: 7 
;     Successors: y 
; 6:  Members: 
;     Successors: 2 6 
; 7:  Members: 7 
;     Successors: x 
; 8:  Members: 
;     Successors: 
; > (run '((lambda (x) x) (lambda (y) (y y))))
; (6 app
;    (1 fn x (0 var x))
;    (5 fn y (4 app (2 var y) (3 var y))))
; x:  Members: 5 
;     Successors: 0 
; y:  Members: 
;     Successors: 
; 0:  Members: 5 
;     Successors: 6 
; 1:  Members: 1 
;     Successors: 
; 2:  Members: 
;     Successors: 
; 3:  Members: 
;     Successors: 
; 4:  Members: 
;     Successors: 
; 5:  Members: 5 
;     Successors: x 
; 6:  Members: 5 
;     Successors: 
; >