← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2002/martin-alonso-hidalgo-ruiz/support/generic-theory.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/2002/martin-alonso-hidalgo-ruiz/support/generic-theory.lisp
 
1
;;;============================================================================
 
2
;;;
 
3
;;; Generic theory tools.
 
4
;;;
 
5
;;;============================================================================
 
6
 
 
7
#| Certification code:
 
8
 
 
9
(certify-book "generic-theory")
 
10
 
 
11
|#
 
12
 
 
13
(in-package "ACL2")
 
14
 
 
15
;;;----------------------------------------------------------------------------
 
16
;;;
 
17
;;; Tools to obtain the event list:
 
18
;;;
 
19
;;;----------------------------------------------------------------------------
 
20
 
 
21
(defun get-event-lst-fn (event-name-lst wrld)
 
22
  (declare (xargs :mode :program))
 
23
  (cond ((endp event-name-lst) nil)
 
24
        (t (cons (get-event (car event-name-lst) wrld)
 
25
                 (get-event-lst-fn (cdr event-name-lst) wrld)))))
 
26
 
 
27
(defmacro get-event-lst (event-name-lst)
 
28
  `(get-event-lst-fn ,event-name-lst (w state)))
 
29
 
 
30
;;; Use this as follows
 
31
 
 
32
#|
 
33
 
 
34
; (get-event-lst <event-name-lst>) => <event-lst>
 
35
 
 
36
(defconst *theory*
 
37
  <event-lst>
 
38
  )
 
39
 
 
40
|#
 
41
 
 
42
;;;----------------------------------------------------------------------------
 
43
;;;
 
44
;;; Tools to instantiate the generic theory:
 
45
;;;
 
46
;;;----------------------------------------------------------------------------
 
47
 
 
48
;;; Substitutions:
 
49
 
 
50
(defun subst-equal (old new tree)
 
51
  (cond ((equal old tree) new)
 
52
        ((atom tree) tree)
 
53
        (t (cons (subst-equal old new (car tree))
 
54
                 (subst-equal old new (cdr tree))))))
 
55
 
 
56
(defun subst-equal-lst (lst tree)
 
57
  (cond ((endp lst) tree)
 
58
        (t (subst-equal-lst (cdr lst)
 
59
                            (subst-equal (caar lst) (cadar lst) tree)))))
 
60
 
 
61
;;; Generating new names:
 
62
 
 
63
(defun packn-string-in-pkg (string pkg-witness)
 
64
  (declare (xargs :mode :program))
 
65
  (intern-in-package-of-symbol string pkg-witness))
 
66
 
 
67
(defun add-name-subst (name subst suffix)
 
68
  (declare (xargs :mode :program))
 
69
  (cons (list name 
 
70
              (packn-string-in-pkg (string-append (string name) suffix) name))
 
71
        subst))
 
72
 
 
73
;;; Generating the instantiation:
 
74
 
 
75
(defun remove-old-hints (event)
 
76
  (cond ((endp event) nil)
 
77
        ((eq ':hints (car event))
 
78
         (cddr event))
 
79
        (t (cons (car event) (remove-old-hints (cdr event))))))
 
80
 
 
81
(defun functional-instance (event old-name subst)
 
82
  (append (remove-old-hints event)
 
83
          `(:hints
 
84
            (("Goal" :by
 
85
              (:functional-instance ,old-name ,@subst))))))
 
86
 
 
87
(defun functional-instance-lst (event-lst subst suffix)
 
88
  (declare (xargs :mode :program))
 
89
  (cond ((endp event-lst) nil)
 
90
        ((equal (car (car event-lst)) 'defun)
 
91
         (let ((new-subst
 
92
                (add-name-subst (cadr (car event-lst)) subst suffix)))
 
93
           (cons (subst-equal-lst new-subst (car event-lst))
 
94
                 (functional-instance-lst (cdr event-lst) new-subst suffix))))
 
95
        ((equal (car (car event-lst)) 'defthm)
 
96
         (let ((new-subst
 
97
                (add-name-subst (cadr (car event-lst)) subst suffix)))
 
98
           (cons (functional-instance
 
99
                   (subst-equal-lst new-subst (car event-lst))
 
100
                   (cadr (car event-lst))
 
101
                   subst)
 
102
                 (functional-instance-lst (cdr event-lst) subst suffix))))
 
103
        (t (functional-instance-lst (cdr event-lst) subst suffix))))
 
104
 
 
105
(defmacro make-generic-theory (theory)
 
106
  (let ((definstance-theory
 
107
          (packn-string-in-pkg 
 
108
           (string-append "DEFINSTANCE-" (string theory)) theory)))    
 
109
    `(defmacro ,definstance-theory (subst suffix)
 
110
       (list* 'encapsulate
 
111
              'nil
 
112
              (functional-instance-lst ,theory subst
 
113
                                       (string-upcase suffix))))
 
114
    ))
 
115
 
 
116
;;; This must be use as follows:
 
117
 
 
118
#|
 
119
 
 
120
(make-generic-theory *theory*)
 
121
 
 
122
|#
 
123
 
 
124
;;;============================================================================