← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2009/liu/support/mylet.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2009/liu/support/mylet.lisp
 
1
(in-package "ACL2")
 
2
;; Tue Dec 23 14:49:11 2003 macros that expands a term with a list of
 
3
;; abbrevation
 
4
 
 
5
(mutual-recursion
 
6
 (defun expand-mylet*-2-l (binding term-l)
 
7
   (declare (xargs :verify-guards nil
 
8
                   :measure (acl2-count term-l)))
 
9
   (if (endp term-l) nil
 
10
     (cons (expand-mylet*-2 binding (car term-l))
 
11
           (expand-mylet*-2-l binding (cdr term-l)))))
 
12
 
 
13
 (defun expand-mylet*-2 (binding term)
 
14
   (declare (xargs :verify-guards nil
 
15
                   :measure (acl2-count term)))
 
16
   (let ((key (car binding))
 
17
         (value (cdr binding)))
 
18
     (cond ((atom term) 
 
19
            (if (equal term key)
 
20
                value
 
21
              term))
 
22
           ((consp term)
 
23
            (if (consp term)
 
24
                (cons (car term) 
 
25
                      (expand-mylet*-2-l binding (cdr term)))
 
26
              term))
 
27
           (t term)))))
 
28
                
 
29
; (expand-mylet*-2 '(x . (f (+ x y))) 
 
30
;                  '(G (f (x x))))
 
31
 
 
32
(defun expand-mylet*-1 (binding alist)
 
33
  (declare (xargs :verify-guards nil))
 
34
  (if (endp alist) nil
 
35
    (cons (cons (caar alist)
 
36
                (expand-mylet*-2 binding (cdar alist)))
 
37
          (expand-mylet*-1 binding (cdr alist)))))
 
38
          
 
39
 
 
40
(defun expand-mylet* (bindings topTerm)
 
41
  (declare (xargs :verify-guards nil
 
42
                  :measure (len bindings)))
 
43
  (if (endp bindings) 
 
44
      topTerm
 
45
    (expand-mylet* (expand-mylet*-1 (car bindings) (cdr bindings))
 
46
                   (expand-mylet*-2 (car bindings) topTerm))))
 
47
 
 
48
;; this is a flaky substitution implementation. 
 
49
;; Only used by myself. It is ok.
 
50
 
 
51
; (expand-mylet* '((x . (f x)) 
 
52
;                  (y . (f x (f (+ x y)))))
 
53
;                '(G (f (+ x y) (y y x))))
 
54
 
 
55
(defun extract-bindings (assignments)
 
56
  (declare (xargs :verify-guards nil))
 
57
  (if (endp assignments) nil
 
58
    (cons (cons (caar assignments) (cadar assignments))
 
59
          (extract-bindings (cdr assignments)))))
 
60
 
 
61
; (extract-bindings 
 
62
;  '((cid (current-thread s))
 
63
;    (tt  (thread-table s))
 
64
;    (thread (thread-by-id cid tt))
 
65
;    (callstack (thread-call-stack thread))
 
66
;    (topframe  (top callstack))))
 
67
 
 
68
 
 
69
(defmacro mylet* (assignments theTerm)
 
70
 (let ((expanded (expand-mylet* (extract-bindings assignments) theTerm)))
 
71
      `,expanded))
 
 
b'\\ No newline at end of file'