← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/gacc/abstract-gacc.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/coi/gacc/abstract-gacc.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#| coi: Computational Object Inference                                       |#
4
 
#|                                                                           |#
5
 
#|===========================================================================|#
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
6
31
(in-package "ACL2")
7
32
; cert_param: (non-acl2r)
8
33
(include-book "../records/defrecord")
212
237
  (if (consp spec)
213
238
      (if (consp (car spec))
214
239
          (and (not (memberx (caar spec) (keys (cdr spec))))
215
 
               (implies (sconsp (cdar spec)) 
 
240
               (implies (sconsp (cdar spec))
216
241
                        (unique-spec (cdar spec)))
217
242
               (unique-spec (cdr spec)))
218
243
        (unique-spec (cdr spec)))
248
273
   (equal (c* spec (s a v r1) r2)
249
274
          (c* spec r1 r2)))
250
275
  :hints (("goal" :induct (c*-induction spec r1 r2))))
251
 
  
 
276
 
252
277
 
253
278
(defun c*-c*-induction (spec r1 r2 r3)
254
279
  (declare (type t spec r1 r2 r3))
257
282
          (let ((v1 (g (caar spec) r1))
258
283
                (v2 (g (caar spec) r2))
259
284
                (v3 (g (caar spec) r3)))
260
 
            (let ((v (if (sconsp (cdar spec)) 
261
 
                         (c*-c*-induction (cdar spec) v1 v2 v3) 
 
285
            (let ((v (if (sconsp (cdar spec))
 
286
                         (c*-c*-induction (cdar spec) v1 v2 v3)
262
287
                       (cons v1 v1))))
263
288
              (let ((v1 (car v))
264
289
                    (v2 (cdr v)))
381
406
  type-b-spec
382
407
  ))
383
408
 
384
 
;; Note that proving the following should allow us to conclude 
 
409
;; Note that proving the following should allow us to conclude
385
410
;;
386
 
;; (= (z* spec (goo r)) (z* spec r)) 
 
411
;; (= (z* spec (goo r)) (z* spec r))
387
412
;;
388
413
;; for any spec of which (type-b-spec) is a subset (subbag-p?). (yay)
389
414
 
598
623
        (:key1 (k1-set value g))
599
624
        (:key2 (k2-set value g))
600
625
        (t     value)))
601
 
  
 
626
 
602
627
(defun key-fix (key value)
603
628
  (declare (type t key value))
604
629
  (case key
955
980
 
956
981
;; (def list) and (use list) might be used extract these lists of
957
982
;; keys.  Intersect and Difference compare two lists and create a u/d
958
 
;; list based on the results.  
 
983
;; list based on the results.
959
984
;;
960
985
;; We will often want identity mappings (u==d).  In such case, we might
961
986
;; want the function (ud list), such that (use (ud list)) = list and (def
1133
1158
   (equal (c* (dia seg) st1 nil)
1134
1159
          (c* (dia seg) st2 nil))
1135
1160
   (equal (c* (dia seg) (step (c* use st2 nil)) nil)
1136
 
          (c* (dia seg) (step (c* use st2 nil)) nil)))) 
 
1161
          (c* (dia seg) (step (c* use st2 nil)) nil))))
1137
1162
 
1138
1163
;; Boom .. done.
1139
1164
 
1140
1165
 
1141
1166
 
1142
 
|#
1143
 
 
 
1167
|#
 
 
b'\\ No newline at end of file'