← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/acl2s/defdata/sig.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/acl2s/defdata/sig.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(include-book ;; Newline to fool ACL2/cert.pl dependency scanner
 
3
 "../portcullis")
 
4
(acl2::begin-book t :ttags :all);$ACL2s-Preamble$|#
 
5
 
 
6
#|
 
7
Polymorphic signatures (sig macro)
 
8
author: harshrc
 
9
file name: sig.lisp
 
10
date created: [2014-08-06 Sun]
 
11
data last modified: [2014-08-07]
 
12
|#
 
13
 
 
14
(in-package "DEFDATA")
 
15
 
 
16
(include-book "defdata-core")
 
17
 
 
18
 
 
19
; DEFDATA POLYMORPHIC SUPPORT EVENT GENERATION FUNCTIONS.
 
20
 
 
21
 
 
22
(defconst *allowed-type-vars* '(:a :b :c :d :a1 :b1 :c1 :d1 :a2 :b2 :c2 :d2))
 
23
 
 
24
(defconst *tvar-typename-alist*
 
25
  '((:a . A)
 
26
    (:b . B)
 
27
    (:c . C)
 
28
    (:d . D)
 
29
    (:a1 . A1)
 
30
    (:b1 . B1)
 
31
    (:c1 . C1)
 
32
    (:d1 . D1)
 
33
    (:a2 . A2)
 
34
    (:b2 . B2)
 
35
    (:c2 . C2)
 
36
    (:d2 . D2)))
 
37
 
 
38
; type var expr -> psig fun instance template
 
39
; where type var expr is the dominating polymorphic argument expr in a sig form
 
40
(table psig-template-map nil) ;UNUSED now -- but seems like a more general idea to support arbitrary polymorphic type expressions. REVISIT
 
41
 
 
42
(defstub psig-templ-instantiation-ev (* * * * * * *) => *)
 
43
(defloop psig-inst-templates (tname tvar-sigma templates new-types kwd-alist wrld)
 
44
  (for ((templ in templates))
 
45
       (append (psig-templ-instantiation-ev tname tvar-sigma templ (table-alist 'derived-pred->poly-texp-map wrld) new-types kwd-alist wrld))))
 
46
 
 
47
(program)
 
48
 
 
49
(defun one-way-unify (pat term)
 
50
  (if (and (pseudo-termp pat)
 
51
           (pseudo-termp term))
 
52
      (acl2::one-way-unify pat term)
 
53
    (mv nil nil)))
 
54
 
 
55
(defun polymorphic-inst-defdata-events1 (p top-kwd-alist wrld)
 
56
  (b* (((cons name A) p)
 
57
       ;; (pdef (cdr (assoc-eq 'pdef A)))
 
58
       ;; (kwd-alist (cdr (assoc-eq 'kwd-alist A)))
 
59
       ((acl2::assocs pdef new-types kwd-alist) A)
 
60
;       (- (cw "pdef : ~x0" pdef))
 
61
       ((unless (consp pdef)) '())
 
62
       (kwd-alist (append kwd-alist top-kwd-alist))
 
63
       (comb (car pdef))
 
64
       (U (table-alist 'user-combinator-table wrld))
 
65
       (C (table-alist 'data-constructor-table wrld)) 
 
66
;TODO: at some time i should support polymorphic cons, but perhaps this is done by tau already SIMPLE BUT GOOD RESEARCH Question/Experiment.
 
67
; Or rather simply use a separate table psig-template-map to support polymorphism more generally
 
68
       (meta-kwd-alist (or (cdr (assoc-eq comb U)) (cdr (assoc-eq comb C))))
 
69
       
 
70
       (template (get1 :polymorphic-events meta-kwd-alist))
 
71
       (ptype (get1 :polymorphic-type-form meta-kwd-alist))
 
72
;       (- (cw "ptype : ~x0    tmpl: ~x1" ptype template)) 
 
73
       ((when (null ptype)) '()) ;no poly support
 
74
       
 
75
       (pdef (remove-names pdef))
 
76
;(one-way-unify '(alistof :a :b) '(alistof nat symbol-list))
 
77
;(T ((:B . SYMBOL-LIST) (:A . NAT)))
 
78
       ((mv yesp tvar-sigma) (one-way-unify (acl2::sublis-var *tvar-typename-alist* ptype) pdef))
 
79
 
 
80
       (verbose (get1 :verbose kwd-alist t))
 
81
        
 
82
        (- (cw? (and (not yesp) verbose) "~|Defdata/Note: Failed to unify ~x0 with ~x1. Skipping polymorphic instantiation events...~%" ptype pdef))
 
83
        ((unless yesp) '()))
 
84
                
 
85
    (psig-templ-instantiation-ev name tvar-sigma template (table-alist 'derived-pred->poly-texp-map wrld) new-types kwd-alist wrld)))
 
86
  
 
87
 
 
88
 
 
89
 
 
90
(defloop polymorphic-inst-defdata-events0 (ps kwd-alist wrld)
 
91
  (for ((p in ps)) (append (polymorphic-inst-defdata-events1 p kwd-alist wrld))))
 
92
 
 
93
(defun polymorphic-inst-defdata-events (ps kwd-alist wrld)
 
94
  (b* ((events (polymorphic-inst-defdata-events0 ps kwd-alist wrld)))
 
95
    (and (consp events)
 
96
         (cons
 
97
          `(commentary ,(get1 :print-commentary kwd-alist) "~| Polymorphic sig instantiation events...~%")
 
98
          events))))
 
99
 
 
100
 
 
101
(add-pre-post-hook defdata-defaults-table :post-hook-fns '(polymorphic-inst-defdata-events))
 
102
 
 
103
 
 
104
 
 
105
 
 
106
 
 
107
; The rest of the file concerns with the implementation of the SIG macro
 
108
 
 
109
 
 
110
 
 
111
; sig macro for polymorphic support.
 
112
 
 
113
; I dont think we are ever going to have more than 3 type parameters, but lets start with 12.
 
114
(logic)
 
115
(encapsulate 
 
116
 (((Ap *) => *) 
 
117
  ((Bp *) => *)
 
118
  ((Cp *) => *)
 
119
  ((Dp *) => *)
 
120
  ((A1p *) => *)
 
121
  ((B1p *) => *)
 
122
  ((C1p *) => *)
 
123
  ((D1p *) => *)
 
124
  ((A2p *) => *)
 
125
  ((B2p *) => *)
 
126
  ((C2p *) => *)
 
127
  ((D2p *) => *))
 
128
 
 
129
 
 
130
 (local (defun Ap (v)
 
131
          (declare (ignore v))
 
132
          t))
 
133
 
 
134
 (local (defun Bp (v)
 
135
          (declare (ignore v))
 
136
          t))
 
137
 
 
138
 (local (defun Cp (v)
 
139
          (declare (ignore v))
 
140
          t))
 
141
 
 
142
 (local (defun Dp (v)
 
143
          (declare (ignore v))
 
144
          t))
 
145
 
 
146
 (local (defun A1p (v)
 
147
          (declare (ignore v))
 
148
          t))
 
149
 
 
150
 (local (defun B1p (v)
 
151
          (declare (ignore v))
 
152
          t))
 
153
 
 
154
 (local (defun C1p (v)
 
155
          (declare (ignore v))
 
156
          t))
 
157
 
 
158
 (local (defun D1p (v)
 
159
          (declare (ignore v))
 
160
          t))
 
161
 
 
162
 (local (defun A2p (v)
 
163
          (declare (ignore v))
 
164
          t))
 
165
 
 
166
 (local (defun B2p (v)
 
167
          (declare (ignore v))
 
168
          t))
 
169
 
 
170
 (local (defun C2p (v)
 
171
          (declare (ignore v))
 
172
          t))
 
173
 
 
174
 (local (defun D2p (v)
 
175
          (declare (ignore v))
 
176
          t))
 
177
 
 
178
 
 
179
 (defthm Ap-is-predicate
 
180
   (booleanp (Ap x)))
 
181
 
 
182
 (defthm Bp-is-predicate
 
183
   (booleanp (Bp x)))
 
184
 
 
185
 (defthm Cp-is-predicate
 
186
   (booleanp (Cp x)))
 
187
 
 
188
 (defthm Dp-is-predicate
 
189
   (booleanp (Dp x)))
 
190
 
 
191
 (defthm A1p-is-predicate
 
192
   (booleanp (A1p x)))
 
193
 
 
194
 (defthm B1p-is-predicate
 
195
   (booleanp (B1p x)))
 
196
 
 
197
 (defthm C1p-is-predicate
 
198
   (booleanp (C1p x)))
 
199
 
 
200
 (defthm D1p-is-predicate
 
201
   (booleanp (D1p x)))
 
202
 
 
203
 (defthm A2p-is-predicate
 
204
   (booleanp (A2p x)))
 
205
 
 
206
 (defthm B2p-is-predicate
 
207
   (booleanp (B2p x)))
 
208
 
 
209
 (defthm C2p-is-predicate
 
210
   (booleanp (C2p x)))
 
211
 
 
212
 (defthm D2p-is-predicate
 
213
   (booleanp (D2p x))))
 
214
(program)
 
215
 
 
216
 
 
217
;(defconst *allowed-type-var->named-type-binding* (pairlis$ *allowed-type-vars* *tvar-typename-alist*))
 
218
 
 
219
 
 
220
;ACHTUNG: make sure people dont use names from defdata namespace. Note that A,Ap,... reside in defdata namespace.
 
221
(defconst *initial-tvar-M* (type-metadata-bases (strip-cdrs *tvar-typename-alist*) "DEFDATA"))
 
222
 
 
223
;maps typenames of type vars to metadata like in M.
 
224
;e.g. A -> Ap nth-A etc
 
225
(table tvar-metadata-table nil *initial-tvar-M* :clear)
 
226
 
 
227
(mutual-recursion
 
228
 (defun collect-type-vars-texp (texp ctx)
 
229
   (cond ((quotep texp) '())
 
230
         ((keywordp texp) (list texp))
 
231
         ((atom texp) '())
 
232
         ((not (true-listp texp)) ;right now we dont support named texp
 
233
          (er hard? ctx "~| ~x0 : Named type expressions not supported.~%" texp))
 
234
         (t (collect-type-vars-texps (cdr texp) ctx))))
 
235
 (defun collect-type-vars-texps (texps ctx)
 
236
   (if (endp texps) 
 
237
       '()
 
238
     (union-eq (collect-type-vars-texp (car texps) ctx)
 
239
               (collect-type-vars-texps (cdr texps) ctx))))
 
240
 )
 
241
 
 
242
(mutual-recursion
 
243
 (defun collect-undefined-typenames-texp (texp ctx wrld)
 
244
   (cond ((quotep texp) '())
 
245
         ((keywordp texp) '())
 
246
         ((atom texp) (if (predicate-name texp) '() (list texp)))
 
247
         ((not (true-listp texp)) ;right now we dont support named texp
 
248
          (er hard? ctx "~| ~x0 : Named type expressions not supported.~%" texp))
 
249
         (t (collect-undefined-typenames-texps (cdr texp) ctx wrld))))
 
250
 (defun collect-undefined-typenames-texps (texps ctx wrld)
 
251
   (if (endp texps) 
 
252
       '()
 
253
     (union-eq (collect-undefined-typenames-texp (car texps) ctx wrld)
 
254
               (collect-undefined-typenames-texps (cdr texps) ctx wrld))))
 
255
 )
 
256
 
 
257
 
 
258
;(include-book "coi/util/pseudo-translate" :dir :system)
 
259
 
 
260
(defconst *sig-keywords* '(:hints :rule-classes :verbose :satisfies))
 
261
 
 
262
;check -- also take care of monomorphic sig, but make sure only tnames are allowed!
 
263
(defun parse-sig (args ctx wrld)
 
264
  (declare (ignorable wrld))
 
265
  (b* (((mv sig kwd-val-list) (separate-kwd-args args '()))
 
266
       ((mv kwd-alist rest) (extract-keywords ctx *sig-keywords* kwd-val-list '()))
 
267
      
 
268
      ((unless (null rest)) (er hard? ctx "~| Extra args: ~x0~%" rest))
 
269
      (dep-hyp (get1 :satisfies kwd-alist))
 
270
      (x123vars (numbered-vars 'ACL2S::X (len *allowed-type-vars*)))
 
271
      (dep-vars (and dep-hyp (all-vars dep-hyp))) ;BEWARE all-vars works only for terms; it might return nil and t as variables. Use pseudo-translate here.
 
272
      ((unless (subsetp dep-vars x123vars))
 
273
       (er hard? ctx "~| Only variable arguments allowed in SATISFIES are ~x0; but given ~x1~%" x123vars dep-vars))
 
274
      (dep-hyps (cond ((null dep-hyp) nil)
 
275
                      ((or (eq dep-hyp 't) (equal dep-hyp ''t)) nil)
 
276
                      ((atom dep-hyp) (list dep-hyp))
 
277
                      ((eq (car dep-hyp) 'ACL2::AND) (cdr dep-hyp))
 
278
                      ((proper-symbolp (car dep-hyp)) (list dep-hyp))
 
279
                      (t dep-hyp)))
 
280
      (kwd-alist (put-assoc-eq :satisfies dep-hyps kwd-alist))
 
281
      ;(- (cw "sig = ~x0  kwd-alist = ~x1 " sig kwd-alist))
 
282
      )
 
283
 
 
284
  (case-match sig
 
285
    ((name arg-type-list 'ACL2::=> return-type)
 
286
     (b* (((unless (proper-symbolp name))
 
287
           (er hard? ctx "~| Name ~x0 should be a symbol.~%" name))
 
288
;simple syntax checks
 
289
          (& (check-syntax-texps arg-type-list '() '() ctx wrld))
 
290
          (undefined-typenames (collect-undefined-typenames-texps (cons return-type arg-type-list) ctx wrld))
 
291
          ((when (consp undefined-typenames))
 
292
           (er hard? ctx "~| Undefined types: ~x0~%" undefined-typenames))
 
293
          (arg-type-vars (collect-type-vars-texps arg-type-list ctx))
 
294
          (return-type-vars (collect-type-vars-texp return-type ctx))
 
295
          ((unless (subsetp return-type-vars arg-type-vars))
 
296
           (er hard? ctx "~| Return type variables should be from ~x0.~%" arg-type-vars))
 
297
; todo: do the mapping from current keyword type variables to :a :b ...
 
298
          ((unless (subsetp arg-type-vars *allowed-type-vars*))
 
299
           (er hard? ctx "~| Sorry for the inconvenience, but could you please try again choosing type variables from ~x0.~%" *allowed-type-vars*)))
 
300
       
 
301
       (list name arg-type-list return-type kwd-alist)))
 
302
        
 
303
    (& (er hard? ctx "~| General form: (sig name arg-type-list => return-type).~%" )))))
 
304
 
 
305
 
 
306
 
 
307
(defun to-symbol (obj pkg)
 
308
  (declare (xargs :guard (and (stringp pkg)
 
309
                              (not (equal pkg "")))))
 
310
  (if (symbolp obj)
 
311
      obj
 
312
    (b* (((mv & str) (acl2::fmt1!-to-string "~x0" (acons #\0 obj '()) 0)))
 
313
      (intern$ str pkg))))
 
314
 
 
315
(defloop to-symbols (objs pkg)
 
316
  (declare (xargs :guard (and (stringp pkg)
 
317
                              (not (equal pkg "")))))
 
318
  (for ((o in objs)) (collect (to-symbol o pkg))))
 
319
 
 
320
;; (defun map-fn (lst f rest-args ctx w)
 
321
;;   (if (endp lst)
 
322
;;       '()
 
323
;;     (cons (funcall-w f (cons (car lst) rest-args) ctx w)
 
324
;;           (map-fn (cdr lst) f rest-args ctx w))))
 
325
 
 
326
;; (defmacro map (lst f w &key rest-args)
 
327
;;   `(map-fn ,lst ,f ,rest-args ,w))
 
328
 
 
329
 
 
330
(defun assoceqlst1 (key A)
 
331
  (let ((entry (assoc-eq key A)))
 
332
    (and entry (list entry))))
 
333
      
 
334
 
 
335
(defloop assoc-eq-lst (keys A)
 
336
  (for ((key in keys)) (append (assoceqlst1 key A))))
 
337
 
 
338
(defun stitch-up-defuns (names params-lst decls bodies)
 
339
  (if (endp names)
 
340
    nil
 
341
    (cons (if (consp decls);not null (only include declare if its not empty)
 
342
            (list 'DEFUN (car names) (car params-lst) (car decls) (car bodies))
 
343
            (list 'DEFUN (car names) (car params-lst) (car bodies)))
 
344
          (stitch-up-defuns (cdr names)
 
345
                            (cdr params-lst)
 
346
                            (cdr decls)
 
347
                            (cdr bodies)))))
 
348
 
 
349
 
 
350
(defun make-derived-tvar-type-defthm (pred texp)
 
351
  (case-match texp
 
352
    (('LISTOF &) `((defthm ,(s+ pred '-IMPLIES-TLP)
 
353
                     (implies (,pred x)
 
354
                              (true-listp x))
 
355
                     :hints (("Goal" :in-theory (enable true-listp)))
 
356
                     :rule-classes ((:forward-chaining)
 
357
                                    (:compound-recognizer)
 
358
                                    ;(:rewrite :backchain-limit-lst 1)
 
359
                                    ))))
 
360
 
 
361
    (('ALISTOF &) `((defthm ,(s+ pred '-IMPLIES-ALISTP)
 
362
                      (implies (,pred x)
 
363
                               (alistp x))
 
364
                      :hints (("Goal" :in-theory (enable ,pred alistp)))
 
365
                      :rule-classes ((:forward-chaining)))))
 
366
    (& '())))
 
367
     
 
368
  
 
369
(defloop make-derived-tvar-type-defthms (preds texps)
 
370
  (for ((p in preds) (texp in texps))
 
371
       (append (make-derived-tvar-type-defthm p texp))))
 
372
 
 
373
 
 
374
;TODO.limitation -- Using just name for the clique tnames (LIMITATION)."
 
375
(defloop parse-top-texps (names texps ctx wrld)
 
376
  (for ((name in names) (texp in texps)) 
 
377
       (collect (parse-top-texp name texp (list name) ctx wrld))))
 
378
 
 
379
 
 
380
(defun make-sig-tvar-support-events (texps ctx wrld)
 
381
  "for each undefined tvar texp, define its predicate and if possible its type defthm"
 
382
  (b* ((M (append (table-alist 'tvar-metadata-table wrld) 
 
383
                  (table-alist 'type-metadata-table wrld)))
 
384
       (texps (remove-names-lst (remove-duplicates-equal texps)))
 
385
       (tnames  (to-symbols texps "DEFDATA"))
 
386
  
 
387
       (undef-tnames (set-difference-eq tnames (strip-cars (assoc-eq-lst tnames M))))
 
388
       
 
389
       (undef-nm-texp-alst (assoc-eq-lst undef-tnames (pairlis$ tnames texps)))
 
390
;       (- (cw "nm-texp-alst: ~x0 undef-tnames: ~x1  undef-nm-texp-alst: ~x2" nm-texp-alst undef-tnames undef-nm-texp-alst))
 
391
       ((mv undef-tnames undef-texps) (mv (strip-cars undef-nm-texp-alst) (strip-cdrs undef-nm-texp-alst)))
 
392
       (undef-n-types (parse-top-texps undef-tnames undef-texps ctx wrld))
 
393
    
 
394
 
 
395
       (C (table-alist 'data-constructor-table wrld))
 
396
       (B (table-alist 'builtin-combinator-table wrld))
 
397
       (new-types (type-metadata-bases undef-tnames "DEFDATA"))
 
398
       (M (append new-types M))
 
399
       (undef-pred-bodies (make-pred-Is undef-n-types (make-list (len undef-n-types) :initial-element 'x) nil M C B wrld))
 
400
       (undef-pred-names (make-predicate-symbol-lst undef-tnames "DEFDATA")))
 
401
;   in 
 
402
    (append (stitch-up-defuns undef-pred-names 
 
403
                              (make-list (len undef-pred-names) :initial-element '(x))
 
404
                              nil
 
405
                              undef-pred-bodies)
 
406
            (make-derived-tvar-type-defthms undef-pred-names undef-texps))))
 
407
       
 
408
 
 
409
(defconst *poly-combinators* '(listof alistof map))
 
410
 
 
411
;map: pred name -> actual tvar comb exp
 
412
(table derived-pred->poly-texp-map nil)
 
413
 
 
414
(defloop table-put-events (tble-name keys vals)
 
415
  (for ((key in keys) (val in vals))
 
416
       (collect `(TABLE ,tble-name ',key ',val :put))))
 
417
 
 
418
(defconst *sig-singular-dominant-poly-comb-limitation-msg* 
 
419
"~| SIG: Limitation -- There should be one polymorphic combinator argument that dominates all other arguments. ~
 
420
But ~x0 does not have this property. Therefore we are unable to functionally instantiate this polymorphic signature. ~
 
421
Please send this example to the implementors for considering removal of this restriction.~%")
 
422
 
 
423
(defun all-tvars (texp)
 
424
  (intersection-eq (strip-cdrs *tvar-typename-alist*) (all-vars texp)))
 
425
 
 
426
(defun all-tvars-lst (texps)
 
427
  (intersection-eq (strip-cdrs *tvar-typename-alist*) (all-vars1-lst texps '())))
 
428
 
 
429
(defun poly-type-size (ptype)
 
430
  (if (atom ptype) 
 
431
      0
 
432
    (case (car ptype)
 
433
      (oneof 1); TODO
 
434
      (listof (+ 2 (poly-type-size (cadr ptype))))
 
435
      (alistof (+ 3 (+ (poly-type-size (second ptype)) (poly-type-size (third ptype)))))
 
436
      (map (+ 4 (+ (poly-type-size (second ptype)) (poly-type-size (third ptype)))))
 
437
      (t 0))))
 
438
 
 
439
 
 
440
(defun choose-largest-poly-type (ptypes ans)
 
441
  (if (endp ptypes)
 
442
      ans
 
443
    (if (> (poly-type-size (car ptypes)) (poly-type-size ans))
 
444
        (choose-largest-poly-type (cdr ptypes) (car ptypes))
 
445
      (choose-largest-poly-type (cdr ptypes) ans))))
 
446
 
 
447
(defun pick-dominant-poly-type-expr1 (ptypes all-tvars answers)
 
448
  (if (endp ptypes)
 
449
      (choose-largest-poly-type answers (car answers))
 
450
    (if (subsetp all-tvars (all-tvars (car ptypes)))
 
451
        (pick-dominant-poly-type-expr1 (cdr ptypes) all-tvars (cons (car ptypes) answers))
 
452
      (pick-dominant-poly-type-expr1 (cdr ptypes) all-tvars answers))))
 
453
  
 
454
(defun pick-dominant-poly-type-expr (ptypes)
 
455
  (pick-dominant-poly-type-expr1 ptypes (all-tvars-lst  ptypes) nil))
 
456
 
 
457
(defun make-table-append-event2 (tble-name key1 key2 val wrld)
 
458
  (b* ((A (table-alist tble-name wrld))
 
459
       (existing-alst (get1 key1 A))
 
460
       (new-val (append (get1 key2 existing-alst) val))
 
461
       (new-alst (put-assoc-eq key2 new-val existing-alst)))
 
462
    `(TABLE ,tble-name ',key1 ',new-alst :put)))
 
463
 
 
464
(defun filter-texps-with-vars (texps)
 
465
  "Filter from normalized texps, the ones which have :a, :b, ... type vars"
 
466
  (if (endp texps)
 
467
      '()
 
468
    (if (consp (all-tvars (car texps)))
 
469
        (cons (car texps) (filter-texps-with-vars (cdr texps)))
 
470
      (filter-texps-with-vars (cdr texps)))))
 
471
      
 
472
 
 
473
(defun register-poly-sig-events (nm atypes rtype templ wrld)
 
474
;sig: proper-symbol * texps * texp * template * world -> events
 
475
  (b* ((dom-atype (pick-dominant-poly-type-expr atypes))
 
476
       (- (cw? nil "dom-atype: ~x0 nm: ~x1" dom-atype nm))
 
477
       ((when (null dom-atype))
 
478
        (prog2$ (cw *sig-singular-dominant-poly-comb-limitation-msg* atypes) nil)))
 
479
    (and (consp dom-atype)
 
480
         (b* ((pcomb (car dom-atype))
 
481
              ((unless (member-eq pcomb *poly-combinators*))
 
482
               (prog2$ 
 
483
                (cw "~x0 currently does not have polymorphic support. Skipping..." pcomb)
 
484
                nil))
 
485
              (vtypes (filter-texps-with-vars (remove-duplicates-equal (cons rtype atypes))))
 
486
              (vtnames (to-symbols vtypes "DEFDATA"))
 
487
              (vpreds (make-predicate-symbol-lst vtnames "DEFDATA")))
 
488
; now add a table entry to type-var table to map arg-pred names to their arg-types, this will help find the correct instantiation alist.
 
489
; then add the template to the corresponding user-combinator polymorphic-events entry!
 
490
           `(,@(table-put-events 'derived-pred->poly-texp-map vpreds vtypes) ;possibly redundant
 
491
             ,@(table-put-events 'tvar-metadata-table vtnames (strip-cdrs (type-metadata-bases vtnames "DEFDATA")))
 
492
             ,(make-table-append-event2 'user-combinator-table pcomb :polymorphic-events templ wrld))))))
 
493
       
 
494
 
 
495
 
 
496
(defun find-type-name (texp M)
 
497
  (if (endp M)
 
498
      :undefined
 
499
    (b* (((cons tname al) (car M))
 
500
         (pdef (get1 :prettyified-def al)))
 
501
 
 
502
      (if (equal texp pdef) ;a very strong check == we should have a weaker (better) equality
 
503
          tname
 
504
        (find-type-name texp (cdr M))))))
 
505
 
 
506
;get typenames for certain type expressions e.g (listof nat) has the type name nat-list
 
507
 
 
508
(defloop find-type-names1 (texps M)
 
509
  (for ((texp in texps)) (collect (if (and (proper-symbolp texp) (assoc-eq texp M)) 
 
510
                                      texp
 
511
                                    (find-type-name texp M)))))
 
512
 
 
513
 
 
514
 
 
515
(defun remove-exprs-with-fns (psigs fns)
 
516
  (if (endp psigs)
 
517
      '()
 
518
    (if (intersection-eq (acl2::all-fnnames (car psigs)) fns)
 
519
        (remove-exprs-with-fns (cdr psigs) fns)
 
520
      (cons (car psigs)
 
521
            (remove-exprs-with-fns (cdr psigs) fns)))))
 
522
 
 
523
 
 
524
(defun subst-vals (map sigma)
 
525
  "apply sigma to all values in map"
 
526
  (if (endp map)
 
527
      '()
 
528
    (b* (((cons key val) (car map))
 
529
         (val~ (acl2::sublis-var sigma val)))
 
530
      (cons (cons key val~)
 
531
            (subst-vals (cdr map) sigma)))))
 
532
 
 
533
 
 
534
; refactor these two functions TODO
 
535
(defun undefined-preds (pred->tname-map)
 
536
  "return all keys marked :undefined"
 
537
  (if (endp pred->tname-map)
 
538
      '()
 
539
    (if (equal (cdr (car pred->tname-map)) :undefined)
 
540
        (cons (caar pred->tname-map)
 
541
              (undefined-preds (cdr pred->tname-map)))
 
542
      (undefined-preds (cdr pred->tname-map)))))
 
543
      
 
544
(defun remove-undefined (map)
 
545
"remove all values marked :undefined"
 
546
  (if (endp map)
 
547
      '()
 
548
    (if (equal (cdr (car map)) :undefined)
 
549
        (remove-undefined (cdr map))
 
550
      (cons (car map)
 
551
            (remove-undefined (cdr map))))))
 
552
 
 
553
 
 
554
(defun predicate-name/lambda (type M)
 
555
  "find predicate characterization for type (either a symbol or a quoted
 
556
constant). In the latter return a lambda expression"
 
557
  (declare (xargs :guard (and (or (proper-symbolp type) (possible-constant-value-p type))
 
558
                              (symbol-alistp M))))
 
559
  (cond ((proper-symbolp type) (predicate-name type M))
 
560
        ((possible-constant-value-p type) `(lambda (x) (equal x ,type)))
 
561
        (t nil)))
 
562
         
 
563
(defloop predicate-names/lambdas (types M)
 
564
  (for ((type in types)) (collect (predicate-name/lambda type M))))
 
565
 
 
566
 
 
567
 
 
568
 
 
569
(defun dlistify (alist)
 
570
  (declare (xargs :guard (alistp alist)))
 
571
  (list-up-lists (strip-cars alist) (strip-cdrs alist)))
 
572
 
 
573
(defun polypred-instantiated-pred-alist (ppred->tname-map new-types wrld)
 
574
  (b* ((M (append (table-alist 'tvar-metadata-table wrld) new-types (table-alist 'type-metadata-table wrld)))
 
575
       (inst-preds (predicate-names (strip-cdrs ppred->tname-map) M)))
 
576
    (pairlis$ (strip-cars ppred->tname-map) inst-preds)))
 
577
 
 
578
(defun functional-instantiation-list (ppred->tname-map tvar-sigma new-types kwd-alist wrld)
 
579
  (b* ((M (append (table-alist 'tvar-metadata-table wrld) new-types (table-alist 'type-metadata-table wrld)))
 
580
       (A1 (pairlis$
 
581
            (predicate-names/lambdas (acl2::sublis-var-lst *tvar-typename-alist* (strip-cars tvar-sigma)) M)
 
582
            (predicate-names/lambdas (strip-cdrs tvar-sigma) M)))
 
583
       
 
584
       (A2 (polypred-instantiated-pred-alist ppred->tname-map new-types wrld))
 
585
       (ans (union-alist2 A2 A1)) ;A2 overrides A1
 
586
       (ctx 'functional-instantiation-alist)
 
587
       (- (cw? (and (or t (get1 :verbose kwd-alist t))
 
588
                    (not (alist-equiv ans (union-alist2 A1 A2))))
 
589
               "~|Defdata/Warning:: ~x0 - tvar-sigma ~x1 entries differ from ppred-instpred-map ~x2" ctx A1 A2))
 
590
       )
 
591
    (dlistify (remove-duplicates-equal ans))))
 
592
 
 
593
(defun polypred-typename-map (tvar-sigma derived-pred->poly-texp-map new-types wrld)
 
594
  (b* ((ppred->texp-map (subst-vals derived-pred->poly-texp-map tvar-sigma))
 
595
       (M (append new-types (table-alist 'type-metadata-table wrld))))
 
596
    (pairlis$ (strip-cars ppred->texp-map) 
 
597
              (find-type-names1 (strip-cdrs ppred->texp-map) M))))
 
598
 
 
599
(defloop filter-proper-symbols (xs)
 
600
  (for ((x in xs)) (append (and (proper-symbolp x) (list x)))))
 
601
 
 
602
 
 
603
(defun psig-templ-instantiation-ev-user (tname tvar-sigma templ derived-pred->poly-texp-map new-types kwd-alist wrld)
 
604
  "For given tvar-sigma, find functional instantiation and return instantiated templ"
 
605
  (b* ((ppred->tname-map (polypred-typename-map tvar-sigma derived-pred->poly-texp-map new-types wrld))
 
606
; remove signatures that have no match
 
607
       (templ (remove-exprs-with-fns templ (undefined-preds ppred->tname-map)))
 
608
 
 
609
       (fun-inst-dlist (functional-instantiation-list (remove-undefined ppred->tname-map) tvar-sigma new-types kwd-alist wrld))
 
610
 
 
611
       (pred (predicate-name tname (append new-types (table-alist 'type-metadata-table wrld))))
 
612
       (disabled (remove-eq pred (append (filter-proper-symbols (strip-cadrs fun-inst-dlist)) (get1 :disabled kwd-alist))))
 
613
       (enabled (and pred (list pred))) ;TODO.check later
 
614
       (splice-alist `((_ENABLED-RUNES_ . ,enabled) (_DISABLED-RUNES_ . ,disabled) (_FUN-INST-ALIST_ . ,fun-inst-dlist)))
 
615
       (ppred-inst-pred-alist (polypred-instantiated-pred-alist ppred->tname-map new-types wrld))
 
616
       (atom-alist (acons '_PRED_ pred ppred-inst-pred-alist))
 
617
       (str-alist (acons "_PRED_"  (symbol-name pred) '())))
 
618
    (template-subst templ
 
619
                    :features nil
 
620
                    :subtree-alist nil
 
621
                    :splice-alist splice-alist
 
622
                    :atom-alist atom-alist
 
623
                    :str-alist str-alist
 
624
                    :pkg-sym pred)))
 
625
 
 
626
(defttag t)      
 
627
(defattach (psig-templ-instantiation-ev psig-templ-instantiation-ev-user) :skip-checks t)
 
628
(defttag nil)
 
629
 
 
630
(defloop psig-templ-instantiation-events (ps templ derived-pred->poly-texp-map new-types kwd-alist wrld)
 
631
  (for ((p in ps)) (append (psig-templ-instantiation-ev (car p) (cdr p) templ derived-pred->poly-texp-map new-types kwd-alist wrld))))
 
632
 
 
633
;       (n-ret-type (parse-top-texp '* return-type1 ctx wrld))
 
634
;       (p-ret-type (untrans-texp '* n-ret-type ctx wrld))
 
635
 
 
636
 
 
637
(defconst *map-all-to-a* (pairlis$ *allowed-type-vars*
 
638
                                   (make-list (len *allowed-type-vars*) :initial-element ':a)))
 
639
 
 
640
(mutual-recursion
 
641
 (defun simplify-prop-comb-texp (pdef)
 
642
   (cond ((atom pdef) pdef)
 
643
         ((possible-constant-value-p pdef) pdef)
 
644
         ((member-eq (car pdef) '(or and oneof anyof))
 
645
          (b* ((rest (remove-duplicates-equal (simplify-prop-comb-texps (cdr pdef)))))
 
646
            (if (consp (cdr rest))
 
647
                (cons 'or rest)
 
648
              (car rest))))
 
649
         (t (cons (car pdef) (simplify-prop-comb-texps (cdr pdef))))))
 
650
 (defun simplify-prop-comb-texps (texps)
 
651
   (if (endp texps)
 
652
       '()
 
653
     (cons (simplify-prop-comb-texp (car texps))
 
654
           (simplify-prop-comb-texps (cdr texps)))))
 
655
 )
 
656
              
 
657
 
 
658
(defun find-match (ptype pdef)
 
659
  (b* ((pdef (remove-names pdef))
 
660
       ((mv yes sigma) (one-way-unify ptype pdef))
 
661
       ((when yes) (mv t sigma)))
 
662
;exceptional hack
 
663
    (if (eq (car ptype) 'LISTOF)
 
664
        (b* (((mv yes sigma) (one-way-unify ptype (simplify-prop-comb-texp (acl2::sublis-var *map-all-to-a* pdef))))
 
665
             ((unless yes) (mv yes sigma))
 
666
             (val (cdr (car sigma))) ;the lone :a mapped value
 
667
             (tvars (all-vars pdef))
 
668
             (sigma (pairlis$ tvars (make-list (len tvars) :initial-element val))))
 
669
          (mv t sigma))
 
670
      (mv nil nil))))
 
671
           
 
672
(defun find-matches1 (ptype M)
 
673
  (if (endp M)
 
674
      '()
 
675
    (b* (((cons tname al) (car M))
 
676
         (pdef (get1 :prettyified-def al))
 
677
         ((unless pdef) (find-matches1 ptype (cdr M))) ;skip types with NIL prettyified-def
 
678
         ((mv yes sigma) (find-match ptype pdef)))
 
679
      (if yes
 
680
          (cons (cons tname sigma) (find-matches1 ptype (cdr M)))
 
681
        (find-matches1 ptype (cdr M))))))
 
682
      
 
683
(defun find-matches (ptype wrld)
 
684
  (find-matches1 ptype (table-alist 'type-metadata-table wrld)))
 
685
 
 
686
(defun find/make-type-name (ptexp M)
 
687
  (if (and (proper-symbolp ptexp)
 
688
           (assoc ptexp M))
 
689
      ptexp
 
690
    (to-symbol ptexp "DEFDATA")))
 
691
 
 
692
(defloop find/make-type-names (ptexps M)
 
693
  (for ((ptexp in ptexps)) (collect (find/make-type-name ptexp M))))
 
694
  
 
695
(defun find/make-predicate-name (tname M)
 
696
  (or (predicate-name tname M) (make-predicate-symbol tname (symbol-package-name tname))))
 
697
 
 
698
(defloop find/make-predicate-names (tnames M)
 
699
  (for ((tname in tnames)) (collect (find/make-predicate-name tname M))))
 
700
 
 
701
(defun instantiate-poly-sig-events-for-current-types (as rtype templ kwd-alist wrld)
 
702
  "limited/linear instantiation of poly signatures for all current types of same shape"
 
703
  (declare (ignorable rtype))
 
704
  (b* ((atype (pick-dominant-poly-type-expr (append as (list rtype)))) ;[2014-11-25 Tue] Dont ignore return type here.
 
705
       ((when (null atype)) nil) ;msg has been already shown
 
706
       ((when (symbolp atype)) nil) ;TODO.generalize restrict free/single-variable matches.
 
707
       (tname-IA-alst (find-matches atype wrld)) ;get type -> (alistof tvar pred)  mapping
 
708
       (M (append (table-alist 'tvar-metadata-table wrld) 
 
709
                  (table-alist 'type-metadata-table wrld)))
 
710
       (arg-tnames (find/make-type-names (remove-names-lst as) M))
 
711
       (arg-preds (find/make-predicate-names arg-tnames M))
 
712
       (ret-tname (find/make-type-name (remove-names rtype) M))
 
713
       (ret-pred (find/make-predicate-name ret-tname M))
 
714
       (derived-pred->poly-texp-map (cons (cons ret-pred rtype) (pairlis$ arg-preds as)))
 
715
       )
 
716
    (psig-templ-instantiation-events tname-IA-alst templ derived-pred->poly-texp-map '() kwd-alist wrld)))
 
717
  
 
718
(defloop untrans-top-texps (nms nexps)
 
719
  (for ((nm in nms) (nexp in nexps)) (collect (untrans-top-texp nm nexp '()))))
 
720
 
 
721
(defun make-sig-defthm-body (name arg-types ret-type kwd-alist wrld)
 
722
  (b* ((M (append (table-alist 'tvar-metadata-table wrld) 
 
723
                  (table-alist 'type-metadata-table wrld)))
 
724
       (arg-tnames (find/make-type-names (remove-names-lst arg-types) M))
 
725
       (arg-preds (find/make-predicate-names arg-tnames M))
 
726
       (ret-tname (find/make-type-name (remove-names ret-type) M))
 
727
       (ret-pred (find/make-predicate-name ret-tname M))
 
728
                 
 
729
 
 
730
       (x1--xk (numbered-vars 'ACL2S::X (len arg-preds)))
 
731
       (dependent-hyps (get1 :satisfies kwd-alist)) ;they should only use x1, x2 etc
 
732
       (hyps (append (list-up-lists arg-preds x1--xk) dependent-hyps))
 
733
       (psig-defthm-body `(IMPLIES (AND . ,hyps)
 
734
                                   ,(list ret-pred (cons name x1--xk)))))
 
735
    psig-defthm-body))
 
736
       
 
737
 
 
738
(defun sig-events1 (name arg-types ret-type kwd-alist ctx wrld)
 
739
  (b* ((arg-type-list1 (acl2::sublis-var-lst *tvar-typename-alist* arg-types)) 
 
740
       (return-type1 (acl2::sublis-var *tvar-typename-alist* ret-type)) ;instead of *allowed-type-var->named-type-binding*
 
741
       (arity (len arg-types))
 
742
       
 
743
       (stars (make-list arity :initial-element '*))
 
744
       (n-arg-types (parse-top-texps stars arg-type-list1 ctx wrld))
 
745
       (n-ret-type (parse-top-texp '* return-type1 (list '*) ctx wrld))
 
746
       (p-arg-types (untrans-top-texps stars n-arg-types))
 
747
       (p-ret-type (untrans-top-texp '* n-ret-type '()))
 
748
 
 
749
       (psig-name (s+ name "-POLYMORPHIC-SIG"))
 
750
       (psig-defthm-body (make-sig-defthm-body name p-arg-types p-ret-type kwd-alist wrld))
 
751
       (poly-inst-template   `((DEFTHM ,(s+ name "-_PRED_-SIG")
 
752
                                ,psig-defthm-body
 
753
                                :hints (("Goal" :in-theory (e/d (_ENABLED-RUNES_) (,name _DISABLED-RUNES_))
 
754
                                         :use ((:functional-instance ,psig-name
 
755
                                                                     _fun-inst-alist_)))))))
 
756
;       (- (cw "args: ~x0 ret: ~x1 derived-pred->poly-texp-map: ~x2 templ: ~x3" p-arg-types p-ret-type derived-pred->poly-texp-map poly-inst-template))
 
757
       )
 
758
 
 
759
    `(,@(make-sig-tvar-support-events (cons p-ret-type p-arg-types) ctx wrld) 
 
760
 
 
761
      (DEFTHM ,psig-name  ;restriction: only one sig per function possible!
 
762
        ,psig-defthm-body
 
763
        :hints ,(or (get1 :hints kwd-alist)  `(("Goal" :in-theory (enable ,name))))
 
764
        :rule-classes ,(get1 :rule-classes kwd-alist '(:rewrite)))
 
765
 
 
766
; for functional instantiating of future types of same shape
 
767
      ,@(register-poly-sig-events name p-arg-types p-ret-type poly-inst-template wrld)
 
768
 
 
769
; functionally instantiate all current types of same shape
 
770
      ,@(instantiate-poly-sig-events-for-current-types p-arg-types p-ret-type 
 
771
                                                       poly-inst-template 
 
772
                                                       kwd-alist wrld)
 
773
      )))
 
774
     
 
775
(defun sig-events (parsed wrld)
 
776
  (b* (((list name arg-types ret-type kwd-alist) parsed)
 
777
       (testing-enabledp (get1 :testing-enabled kwd-alist nil))
 
778
       ;; dont even call acl2s-defaults if cgen/top is not included. This
 
779
       ;; allows defdata/sig to be used independently of cgen
 
780
       (local-testing-downgraded-form (and testing-enabledp 
 
781
                                           '((LOCAL (ACL2S::ACL2S-DEFAULTS :SET ACL2S::TESTING-ENABLED :naive))))))
 
782
    
 
783
    `(WITH-OUTPUT :on (acl2::summary acl2::error) 
 
784
                  :SUMMARY (ACL2::FORM) 
 
785
                  (ENCAPSULATE NIL
 
786
                   (logic)            
 
787
                   ,@local-testing-downgraded-form
 
788
                   ,@(sig-events1 name arg-types ret-type kwd-alist 'sig wrld)))))
 
789
 
 
790
 
 
791
 
 
792
(defmacro sig (&rest args)
 
793
  (b* ((verbose (let ((lst (member :verbose args)))
 
794
                   (and lst (cadr lst)))))
 
795
    `(with-output ,@(and (not verbose) '(:off :all)) 
 
796
                  :gag-mode t 
 
797
                  :stack :push
 
798
       (make-event
 
799
        (sig-events (parse-sig ',args 'sig (w state)) (w state))))))