perm filename LETBYN.LSP[COM,LSP] blob
sn#695977 filedate 1983-01-18 generic text, type T, neo UTF8
; Let-by-need
; Martin Abadi, CS206
; Fall 1982
; Let-by-need is a macro similar to the let macro of MacLisp. It has the
; syntax
; (let-by-need ((var1 val1)
; ...
; (varn valn))
; body).
; Each var is an atom, each val is any Lisp form than can be evaluated, and
; body is a Lisp form. The difference between let and let-by-need is that while
; let first evaluates all the vals, binds them to the vars, and then evaluates
; the body, let-by-need will attempt to evaluate a val if it is actually needed
; in the computation of the body, and in any case not more than once. Thus, it
; should cause the minimum amount of evaluation to be done...
;
; At the present stage, this is not true in the most general case:
; + let-by-need handles satisfactorily expressions of the forms
; (lambda (u1...un) e),(and u1...un),(or u1...un),(cond ((p1 a1)...(pn an))),
; (if p a),(if p a b),(not e) -- where n is a non-negative integer;
; + it acts (successfully) on expressions of the forms
; ((lambda (u1...un) e)v1...vn) and (let ((u1 v1)...(un...vn)) e)
; only when desired (switch on lambdalbn and letlbn in status) -- note that
; it may not always be desired: let-by-need performs conversions and does
; not guarantee termination;
; + it does something similar on expressions like
; (let-by-need ((u1...v1)...(un...vn)) e) when the switch lbnlbn is on;
; in this case either the outer let-by-need is turned into a let (switch off)
; or the inner let-by-need is converted (switch on); in both subcases some
; vals from some let-by-need may happen to be computed more often than
; necessary -- unfortunately, we do not see any method to avoid this
; esthetically unsatisfactory feature: let-by-need does not handle itself
; very elegantly!
; + finally, let-by-need is turned into let in front of blocks it cannot
; penetrate, e.g. atoms or lists it does not know the meaning of (for
; instance (cons (if p a b)(or a b))); still, this let will not evaluate
; vars that do not appear free in the block.
;
; * Algorithm:
; - most of the work is done through the function letbyneed1
; - letbyneed1 is transforms its input into a "normal form" whenever
; possible; normal forms are
; (and u1...un),(or u1...un),(cond ((p1 a1)...(pn an))),
; (if p a),(if p a b),(not e),(lambda (u1...un) e),e
; where u1,p1,p,e are either
; blocks, i.e. atoms or lists with car different
; from and, or, cond, if, not, lambda (plus let, let-by-need, function
; expressed as (lambda ...), when the corresponding switches are on),
; or (not b) , with b a block;
; - the transformations are fairly simple using domain facts; essentially
; they take place from the interior to the exterior: to transform an
; expression, we first transform its car; simple examples are
; (or (and a b) c) --> (cond ((a b)(t c)))
; (if (and a b) c d) --> (if a (if b c d) d)
; (not (or a b)) --> (and (not a)(not b))
; (remark: if is handled as a special case of cond)
; - now we are ready to introduce let (i.e. to "letify") in such a way that
; no val will be evaluated more often than necessary -- at least in the
; nice cases of cond, and, etc.; expressions in normal form are letified,
; for instance
; (let-by-need ((var1 val1)...(varn valn)) (and u1...um))
; yields
; (and (let ((vari1 vali1)...(varin valin)) u1)
; (let-by-need ((var1 val1)...(varn valn)) (and u2...um))),
; where ((vari1 vali1)...(varin valin)) are the bindings necessary
; to the computation of u1 (i.e., those corresponding to its free vars);
; similar processes take place on or, cond, etc.
; - at this point we can return to let-by-need, in order to evaluate the
; modified body.
;
; * Data structures
; (note: this information is somewhat redundant wrt previous sections)
; - let-by-need receives two arguments:
; > an association list, the "pairlist"
; > the body, a Lisp form
; - it passes both to letbyneed1;
; - the body is transformed, obtaining a new Lisp form; the pairlist is
; obviously not necessary for this operation...
; - and then it is letified; here, we need the pairlist again;
; - the resulting form is returned to letbyneed1...
; - and then to let-by-need, for evaluation.
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; * A guide to the code:
; i) higher level forms: let-by-need, letbyneed1
; ii) letification functions and auxiliaries
; iii) transformation functions
; iv) conversion functions and auxiliaries
; v) negation functions
; vi) minor tools
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; let-by-need and letbyneed1
(defmacro let-by-need (pairlist body)
(letbyneed1 pairlist body))
(defun letbyneed1 (pairlist body)
(cond ((or (null body)(null pairlist)) body)
((atom body)(blockletify pairlist body))
((equal (car body) 'lambda)
(list 'lambda
(cadr body)
(letbyneed1 (unbind1 pairlist (cadr body))(caddr body))))
((and (not (atom (car body)))
(equal (caar body) 'lambda)
(status feature lambdalbn))
(letbyneed1 pairlist (convert1 body)))
((or (and (equal (car body) 'let)
(status feature letlbn))
(and (equal (car body) 'let-by-need)
(status feature lbnlbn)))
(letbyneed1 pairlist (disletify1 body)))
((equal (car body) 'not)
(list 'not (letbyneed1 pairlist (cadr body))))
((equal (car body) 'or)
(letify pairlist (ortransform (cdr body))))
((equal (car body) 'and)
(letify pairlist (andtransform (cdr body))))
((equal (car body) 'cond)
(letify pairlist (condtransform (cdr body))))
((equal (car body) 'if)
(letify pairlist (condtransform (cdr (if-to-cond body)))))
(t (blockletify pairlist body))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;letification
;letify letiies an arbitrar form
;pairlist is the pairlist and u isthe form
(defun letify(pairlist u)
(cond ((atom u)(blockletify pairlist u))
((equal (car u) 'or)(orletify pairlist (cdr u)))
((equal (car u) 'and)(andletify pairlist (cdr u)))
((equal (car u) 'cond)(condletify pairlist (cdr u)))
((equal (car u) 'if)(condletify pairlist (cdr (if-to-cond u))))
((equal (car u) 'lambda)
(list 'lambda
(cadr u)
(letify (unbind1 pairlist (cadr u))(caddr u))))
((and (not (atom (car u)))
(equal (caar u) 'lambda)
(status feature lambdalbn))
(letify pairlist (convert1 u)))
((or (and (equal (car u) 'let)
(status feature letlbn))
(and (equal (car u) 'let-by-need)
(status feature lbnlbn)))
(letify pairlist (disletify1 u)))
(t (blockletify pairlist u))))
;blockletify letifies a block
;p is the pairlist and u is the block
(defun blockletify(p u)
((lambda (v) (cond ((null v) u)
(t (list 'let v u))))
(necessary p u)))
;orletify letifies an expression of the form (or u1...un)
;p is the pairlist and u is (u1...un)
(defun orletify (p u)
((lambda (v)(cond ((null v)
(list 'or
(car u)
(letbyneed1 p (cons 'or (cdr u)))))
(t (list 'let
v
(list 'or
(car u)
(letbyneed1 (pairdif p v)
(cons 'or (cdr u))))))))
(necessary p (car u))))
;andletify letifies an expression of the form (and u1...un)
;p is the pairlist and u is (u1...un)
(defun andletify (p u)
((lambda (v)(cond ((null v)
(list 'and
(car u)
(letbyneed1 p (cons 'and (cdr u)))))
(t (list 'let
v
(list 'and
(car u)
(letbyneed1 (pairdif p v)
(cons 'and (cdr u))))))))
(necessary p (car u))))
;condletify letifies an expression of the form (cond ((p1 a1)...(pn an)));
;p is the pairlist and u is ((p1 a1)...(pn an))
(defun condletify (p u)
((lambda (v)(cond ((null v)
(cons 'cond
(list (list (caar u)
(letbyneed1 p (cadar u)))
(list t
(letbyneed1 p (cons 'cond (cdr u)))))))
(t (list 'let
v
(cons 'cond
(list (list (caar u)
(letbyneed1 (pairdif p v)
(cadar u)))
(list t
(letbyneed1 (pairdif p v)
(cons 'cond
(cdr u))))))))))
(necessary p (caar u))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;auxiliary functions for letification
;necessary returns the necessary bindings in a pairlist for the evaluation
;of a given form, i.e. those whose vars are free in the form
;p is the pairlist and u is the form
(defun necessary (p u)
(cond ((null p) nil)
((occurfree (caar p) u)
(cons (car p)
(necessary (cdr p) u)))
(t (necessary (cdr p) u))))
;occurfree determines whether the variable a occurs free in the form u
(defun occurfree (a u)
(or (equal a u)
(and (not (atom u))
(not (equal (car u) 'quote))
(not (equal (car u) 'comment))
(cond ((or (equal (car u) 'let)
(equal (car u) 'let-by-need))
(or (binder a (cadr u))
(and (not (member a (bounds (cadr u))))
(occurfree a (cddr u)))))
((equal (car u) 'lambda)
(and (not (member a (cadr u)))
(occurfree a (cddr u))))
(t (or (occurfree a (car u))
(occurfree a (cdr u))))))))
;binder determines whether a variable a occurs free in some val in a pairlist u
(defun binder (a u)
(cond ((null u) nil)
(t (or (occurfree a (cdar u))
(binder a (cdr u))))))
;pairdif returns a pairlist, the result of unbinding the vars of pairlist2 in
;pairlist1
(defun pairdif (pairlist1 pairlist2)
(unbind1 pairlist1 (bounds pairlist2)))
;bounds returns a list with the vars in pairlist
(defun bounds (pairlist)
(cond ((null pairlist) nil)
(t (cons (caar pairlist)(bounds (cdr pairlist))))))
;unbind1 returns a pairlist, the pairs of pairlist such that their var does not
;appear in varlist
(defun unbind1 (pairlist varlist)
(cond ((null varlist) pairlist)
(t (unbind1 (unbindone pairlist (car varlist))(cdr varlist)))))
;unbindone returns a pairlist, the pairs in pairlist with vars different from a
(defun unbindone (pairlist a)
(cond ((null pairlist) nil)
((equal (caar pairlist) a)(unbindone (cdr pairlist) a))
(t (cons (car pairlist)(unbindone (cdr pairlist) a)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;transformation
;transform puts in normal form an arbitrary form u
(defun transform (u)
(cond ((atom u) u)
((equal (car u) 'or)(ortransform(cdr u)))
((equal (car u) 'and)(andtransform (cdr u)))
((equal (car u) 'cond)(condtransform (cdr u)))
((equal (car u) 'if)(condtransform (cdr (if-to-cond u))))
((equal (car u) 'not)
((lambda (v) (cond ((equal (car v) 'not) v)
(t (transform v))))
(negate (cadr u))))
((and (not (atom (car u)))
(equal (caar u) 'lambda)
(status feature lambdalbn))
(transform (convert1 u)))
((or (and (equal (car u) 'let)
(status feature letlbn))
(and (equal (car u) 'let-by-need)
(status feature lbnlbn)))
(transform (disletify1 u)))
(t u)))
;ortransform puts in normal form an expression of the form (or u1...un)
;u is (u1...un)
(defun ortransform (u)
(cond ((null u) nil)
((null (cdr u))(transform (car u)))
(t ((lambda (u)(cond ((atom (car u))(cons 'or u))
((equal (caar u) 'or)
(cons 'or
(append (cdar u)(cdr u))))
((equal (caar u) 'and)
(cons 'cond
(list (list (cadar u)(cons 'and (cddar u)))
(list t (cons 'or (cdr u))))))
((equal (caar u) 'cond)
(cons 'cond
(list (list (caadar u)
(cons 'or
(cons (cadadar u)
(cdr u))))
(list t (cons 'or
(cons (cons 'cond
(cddar u))
(cdr u)))))))
((equal (caar u) 'if)
(ortransform (cons (if-to-cond (car u))
(cdr u))))
(t (cons 'or u))))
(cons (transform (car u))(cdr u))))))
;andtransform puts in normal form an expression of the form (and u1...un)
;u is (u1...un)
(defun andtransform (u)
(cond ((null u) t)
((null (cdr u))(transform (car u)))
(t ((lambda (u)(cond ((atom (car u))(cons 'and u))
((equal (caar u) 'or)
(cons 'cond
(list (list (cadar u)(cons 'and (cdr u)))
(list t (cons 'and
(cons (cons 'or
(cddar u))
(cdr u)))))))
((equal (caar u) 'and)
(cons 'and (append (cdar u)(cdr u))))
((equal (caar u) 'cond)
(cons 'cond
(list (list (caadar u)
(cons 'and
(cons (cadadar u)
(cdr u))))
(list t (cons 'and
(cons (cons 'cond
(cddar u))
(cdr u)))))))
((equal (caar u) 'if)
(andtransform (cons (if-to-cond (car u))
(cdr u))))
(t (cons 'and u))))
(cons (transform (car u))(cdr u))))))
;condtransform puts in normal form an expression of the form
;(cond ((p1 a1)...(pn an)))
;u is ((p1 a1)...(pn an))
(defun condtransform (u)
(cond ((null u) nil)
((null (cdr u))(andtransform (cons (caar u)(cdar u))))
(t ((lambda (u)(cond ((atom (caar u))(cons 'cond u))
((equal (caaar u) 'or)
(cons 'cond
(cons (list (cadaar u)(cadar u))
(cons (list (cons 'or (cddaar u))
(cadar u))
(cdr u)))))
((equal (caaar u) 'and)
(cons 'cond
(cons (list (cadaar u)
(cons 'cond
(cons (list (cons 'and
(cddaar
u))
(cadar u))
(cdr u))))
(cdr u))))
((equal (caaar u) 'cond)
(cons 'cond
(cons (list (caadaar u)
(cons 'cond
(cons (list (cadadaar u)
(cadar u))
(cdr u))))
(cons (list (cons 'cond
(cddaar u))
(cadar u))
(cdr u)))))
((equal (caaar u) 'if)
(condtransform (cons (cons (if-to-cond (caar u))
(cdar u))
(cdr u))))
(t (cons 'cond u))))
(cons (cons (transform (caar u))
(cdar u))
(cdr u))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;conversions for let, let-by-need, lambda
;convert1 converts an expression u of the form ((lambda (u1...un) body)v1...vn)
;by replacing the ui's by the bi's in the body, whenever correct
;note that this is not a complete conversion (there may be lambda's left)
(defun convert1(u)
(freelistsubs (cdr u)(cadar u)(caddar u)))
;disletify1 converts an expression u of the form
;(let ((var1 val1)...(varn valn)) body) or
;(let-by-need ((var1 val1)...(varn valn)) body) by replacing the vari's by
;the vali's in the body, whenever correct
;note that this is not a complete conversion (there may be let's and
;let-by-need's left); also note that converting a let-by-need may
;cause some of its vals to be evaluated more often than necessary
(defun disletify1(u)
(freelistsubs (vals (cadr u))(bounds (cadr u))(caddr u)))
;;;;;;;;;;;;;;;;;;;;;;
;auxiliaries for conversions
;freelistsubs substitutes the variables in the list old by the expressions in
;the list new in the form place, whenever correct
(defun freelistsubs(new old place)
(cond ((atom place)(atomsubs new old place))
((equal (car place) 'lambda)
(list 'lambda
(cadr place)
((lambda (v) (freelistsubs (car v)
(cadr v)
(caddr place)))
(unbind2 new old (cadr place)))))
((or (equal (car place) 'let)
(equal (car place) 'let-by-need))
(list (car place)
(subsinseconds new old (cadr place))
((lambda (v) (freelistsubs (car v)
(cadr v)
(caddr place)))
(unbind2 new old (bounds (cadr place))))))
(t (cons (freelistsubs new old (car place))
(freelistsubs new old (cdr place))))))
;atomsubs substitutes the variables in the list old by the expressions in the
;list new, in the atom a
(defun atomsubs (new old a)
(cond ((null old) a)
((equal (car old) a)(car new))
(t (atomsubs (cdr new)(cdr old) a))))
;subsinseconds substitutes the variables of the list old by the expressions
;of the list new in the vals of a pairlist pairlist
(defun subsinseconds(new old pairlist)
(cond ((null pairlist) nil)
(t (cons (cons (caar pairlist)
(freelistsubs new old (cdar pairlist)))
(subsinseconds new old (cdr pairlist))))))
;unbind2 is another unbinding function; here u=(u1...un) with ui expressions
;and v=(v1...vn) with vi variables, and we interpret vi bound to ui; we want
;to unbind the variables listed in w, and return a list of the form (u' v'),
;where u' and v' are the modified u and v, respectively
(defun unbind2(u v w)
(cond ((null v)(list nil nil))
((member (car v) w)(unbind2 (cdr u)(cdr v) w))
(t ((lambda (s) (list (cons (car u)(car s))
(cons (car v)(cadr s))))
(unbind2 (cdr u)(cdr v) w)))))
;vals returns a list with the vals from pairlist
(defun vals (pairlist)
(cond ((null pairlist) nil)
(t (cons (cadar pairlist)(vals (cdr pairlist))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;negation
;negate negates an arbitrary form u
(defun negate (u)
(cond ((atom u)(cond ((equal u t) nil)
((null u) t)
(t (cons 'not (list u)))))
((equal (car u) 'and)(cons 'or (negatemembers (cdr u))))
((equal (car u) 'or)(cons 'and (negatemembers (cdr u))))
((equal (car u) 'cond)(cons 'cond (negateseconds (cdr u))))
((equal (car u) 'if)(negate (if-to-cond u)))
((equal (car u) 'not)(cadr u))
((or (equal (car u) 'lambda)
(equal (car u) 'let)
(equal (car u) 'let-by-need))
(list (car u)(cadr u)(negate (caddr u))))
((and (not (atom (car u)))
(equal (caar u) 'lambda))
(cons (list 'lambda (cadr u)(negate (caddr u)))
(cdr u)))
(t (cons 'not (list u)))))
;negatemembers puts a not in front of each element of a list u
;(note: negatemembers[u]=mapcar[[lambda v.<'not v>],u])
(defun negatemembers (u)
(cond ((null u) nil)
(t (cons (list 'not (car u))
(negatemembers (cdr u))))))
;negateseconds puts a not in front of each var in a pairlist p
(defun negateseconds (p)
(cond ((null p) nil)
(t (cons (list (caar p)
(cons 'not (cdar p)))
(negateseconds (cdr p))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;minor tools
(defun cadadar (u)
(cadar (cdar u)))
(defun cadadaar (u)
(cadar (cdaar u)))
(defun caadaar (u)
(caadr (caar u)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;if-to-cond transforms a list u beginning with if into an equivalent list
;beginning with cond
(defun if-to-cond (u)
(cond ((null (cdr u))
'(cond))
((null (cdddr u))
(list 'cond (list (cadr u)(caddr u))))
(t
(list 'cond (list (cadr u)(caddr u))(list t (cadddr u))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
;[PHOTO: Recording initiated Sun 5-Dec-82 9:09PM]
;
;@c l
;?Does not match switch or keyword - "l"
;@lisp
;
;LISP 2122
;Alloc? n
;
;
;*
;; Martin Abadi
;; CS 206
;; Fall 1982
;
;; let-by-need
;
;(load 'test)
;;Loading DEFMACRO 166
;;Loading DEFMAX 98
;;Loading MACAID 119
;;Loading CNVD 2
;T
;
;(status features)
;(MACLISP PDP10 BIGNUM FASLOAD HUNK FUNARG ROMAN NEWIO SFA PAGING TOPS-20 |Stanfo
;rd LTS/
;| DEC20)
;(let-by-need ((a t)(b nil)(c t)) (if (aa or a b)(and a c)(if a b c)))
;;Loading LET 98
;T
;))
;(letbynnneed1 '((a 1)(b 2)(c 3)) '(or (if p a (and b d))(and (cond ((q a)(r s)))
; (not (or b c)))))
;(COND (P (LET ((A 1)) (OR A (AND (Q A) (AND (R S) (LET ((B 2)) (AND (NOT B) (LET
; ((C 3)) (NOT C))))))))) (T (AND T (COND (T (LET ((B 2)) (AND B D))) (T (AD T (
;LET ((A 1)) (AND (Q A) (AND (R S) (LET ((B 2)) (AND (NOT B) (LET ((C 3)) (NOT C)
;))))))))))))
;(letbyneed1 '((a 1)(b 2)(c 3)) '(list a b))
;(LET ((A 1) (B 2)) (LIST A B))
;(letbyneed1 '((a 1)(b 2)(c 3)) '(lambda (a)(if p b (and a c))))
;(LAMBDA (A) (COND (P (LET ((B 2)) B)) (T (AND T (AND A (LET ((C 3)) C))))))
;(letbyneed1 '((a 1)(b 2)(c 3)) '((lambda (p a)(list a b c)
;(letbyneed1 '((a 1)(b 2)(c 3)) '((lambda (p a)(list a b c)) b c))
;(LET ((B 2) (C 3)) ((LAMBDA (P A) (LIST A B C)) B C))
;(letbyneed1 '((a 1)(b 2)(c 3)) '(let ((r a)(t a))(if p a b)))
;(LET ((A 1) (B 2)) (LET ((R A) (T A)) (IF P A B)))
;(comment the same wuld happen with let-by-need)
;COMMENT
;
;(comment now we change some switches)
;COMMENT
;
;
;(sstatus feature lambdalbn)
;LAMBDALBN
;(sstatus feature letlbn)
;LETLBN
;(sstatus feature lbnlbn)
;LBNLBN
;(letbyneed1 '((a 1)(b 2)(c 3)) '((lambda (a)(if p (list a b) c))(or b c)))
;(COND (P (LET ((B 2) (C 3)) (LIST (OR B C) B))) (T (AND T (LET ((C 3)) C))))
;(letbyneed1 '((a 1)(b 2)(c 3)) '(let-by-need ((a b)(b p))(or b c)))
;(OR P (LET ((C 3)) C))
;(letbyneed1 '((a 1)(b 2)(c 3)) '(let ((a b)(b p)) (or a b c)))
;(LET ((B 2)) (OR B (OR P (LET ((C 3)) C))))
;;as usual the same would happen with let-by-need!
;
;(quit)
;@pop
;
;[PHOTO: Recording terminated Sun 5-Dec-82 9:26PM]
;@