← Back to branch summary

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

« back to all changes in this revision

Viewing changes to defuns.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:
defuns.lisp
1
 
; ACL2 Version 6.5 -- A Computational Logic for Applicative Common Lisp
2
 
; Copyright (C) 2014, Regents of the University of Texas
 
1
; ACL2 Version 7.0 -- A Computational Logic for Applicative Common Lisp
 
2
; Copyright (C) 2015, Regents of the University of Texas
3
3
 
4
4
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
5
5
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
798
798
          (merge-sort-length cl-set) nil nil))
799
799
        ens (match-free-override wrld) wrld state ttree)))))
800
800
 
801
 
(defun measure-clause-for-branch (name tc measure-alist rel wrld)
 
801
(defun measure-clause-for-branch (name tc measure-alist rel debug-info wrld)
802
802
 
803
803
; Name is the name of some function, say f0, in a mutually recursive
804
804
; clique.  Tc is a tests-and-call in the termination machine of f0 and hence
824
824
                    (formals f1 wrld)
825
825
                    (fargs call)
826
826
                    (cdr (assoc-eq f1 measure-alist))))
827
 
         (concl (mcons-term* rel m1-prime m0)))
828
 
    (add-literal concl
829
 
                 (dumb-negate-lit-lst tests)
830
 
                 t)))
 
827
         (concl (mcons-term* rel m1-prime m0))
 
828
         (clause (add-literal concl
 
829
                              (dumb-negate-lit-lst tests)
 
830
                              t)))
 
831
    (maybe-add-extra-info-lit debug-info call clause wrld)))
831
832
 
832
 
(defun measure-clauses-for-fn1 (name t-machine measure-alist rel wrld)
 
833
(defun measure-clauses-for-fn1 (name t-machine measure-alist rel debug-info
 
834
                                     wrld)
833
835
  (cond ((null t-machine) nil)
834
 
        (t (conjoin-clause-to-clause-set
 
836
        (t (conjoin-clause-to-clause-set-extra-info
835
837
            (measure-clause-for-branch name
836
838
                                       (car t-machine)
837
839
                                       measure-alist
838
840
                                       rel
 
841
                                       debug-info
839
842
                                       wrld)
840
843
            (measure-clauses-for-fn1 name
841
844
                                     (cdr t-machine)
842
845
                                     measure-alist
843
846
                                     rel
 
847
                                     debug-info
844
848
                                     wrld)))))
845
849
 
846
 
(defun measure-clauses-for-fn (name t-machine measure-alist mp rel wrld)
 
850
(defun measure-clauses-for-fn (name t-machine measure-alist mp rel
 
851
                                    measure-debug wrld)
847
852
 
848
853
; We form all of the clauses that are required to be theorems for the admission
849
854
; of name with the given termination machine and measures.  Mp is the "domain
868
873
 
869
874
  (cond
870
875
   ((eq mp t)
871
 
    (measure-clauses-for-fn1 name t-machine measure-alist rel wrld))
872
 
   (t (conjoin-clause-to-clause-set
873
 
       (add-literal (mcons-term* mp (cdr (assoc-eq name measure-alist)))
874
 
                    nil t)
875
 
       (measure-clauses-for-fn1 name t-machine measure-alist rel wrld)))))
 
876
    (measure-clauses-for-fn1 name t-machine measure-alist rel
 
877
                             (and measure-debug
 
878
                                  `(:measure (:relation ,name)))
 
879
                             wrld))
 
880
   (t (conjoin-clause-to-clause-set-extra-info
 
881
       (let ((mp-call (mcons-term* mp (cdr (assoc-eq name measure-alist)))))
 
882
         (maybe-add-extra-info-lit (and measure-debug
 
883
                                        `(:measure (:domain ,name)))
 
884
                                   mp-call
 
885
                                   (add-literal mp-call nil t)
 
886
                                   wrld))
 
887
       (measure-clauses-for-fn1 name t-machine measure-alist rel
 
888
                                (and measure-debug
 
889
                                     `(:measure (:relation ,name)))
 
890
                                wrld)))))
876
891
 
877
 
(defun measure-clauses-for-clique (names t-machines measure-alist mp rel wrld)
 
892
(defun measure-clauses-for-clique (names t-machines measure-alist mp rel
 
893
                                         measure-debug wrld)
878
894
 
879
895
; We assume we can obtain from wrld the 'formals for each fn in names.
880
896
 
881
897
  (cond ((null names) nil)
882
 
        (t (conjoin-clause-sets
 
898
        (t (conjoin-clause-sets+
 
899
            measure-debug
883
900
            (measure-clauses-for-fn (car names)
884
901
                                    (car t-machines)
885
 
                                    measure-alist
886
 
                                    mp rel
887
 
                                    wrld)
 
902
                                    measure-alist mp rel measure-debug wrld)
888
903
            (measure-clauses-for-clique (cdr names)
889
904
                                        (cdr t-machines)
890
 
                                        measure-alist
891
 
                                        mp rel
 
905
                                        measure-alist mp rel measure-debug
892
906
                                        wrld)))))
893
907
 
894
908
(defun tilde-*-measure-phrase1 (alist wrld)
937
951
        (t (find-?-measure (cdr measure-alist)))))
938
952
 
939
953
(defun prove-termination (names t-machines measure-alist mp rel hints otf-flg
940
 
                                bodies ctx ens wrld state ttree)
 
954
                                bodies measure-debug ctx ens wrld state ttree)
941
955
 
942
956
; Given a list of the functions introduced in a mutually recursive clique,
943
957
; their t-machines, the measure-alist for the clique, a domain predicate mp on
978
992
           (measure-clauses-for-clique names
979
993
                                       t-machines
980
994
                                       measure-alist
981
 
                                       mp rel
 
995
                                       mp rel measure-debug
982
996
                                       wrld)
983
997
           ens
984
998
           wrld ttree state))
2058
2072
    (t (value nil)))
2059
2073
   (er-let*
2060
2074
    ((wrld1 (update-w big-mutrec wrld))
2061
 
     (pair (prove-termination names nil nil mp rel nil otf-flg bodies
 
2075
     (pair (prove-termination names nil nil mp rel nil otf-flg bodies nil
2062
2076
                              ctx ens wrld1 state nil)))
2063
2077
 
2064
2078
; We know that pair is of the form (col . ttree), where col is the column
2069
2083
                 (cdr pair))))))
2070
2084
 
2071
2085
(defun prove-termination-recursive (names arglists measures t-machines
2072
 
                                          mp rel hints otf-flg bodies ctx ens
2073
 
                                          wrld state)
 
2086
                                          mp rel hints otf-flg bodies
 
2087
                                          measure-debug
 
2088
                                          ctx ens wrld state)
2074
2089
 
2075
2090
; This function separates out code from put-induction-info.
2076
2091
 
2099
2114
                             hints
2100
2115
                             otf-flg
2101
2116
                             bodies
 
2117
                             measure-debug
2102
2118
                             ctx
2103
2119
                             ens
2104
2120
                             wrld
2164
2180
            subversive-p))))
2165
2181
 
2166
2182
(defun put-induction-info (names arglists measures ruler-extenders-lst bodies
2167
 
                                 mp rel hints otf-flg big-mutrec ctx ens wrld
2168
 
                                 state)
 
2183
                                 mp rel hints otf-flg big-mutrec measure-debug
 
2184
                                 ctx ens wrld state)
2169
2185
 
2170
2186
; WARNING: This function installs a world.  That is safe at the time of this
2171
2187
; writing because this function is only called by defuns-fn0, which is only
2236
2252
                       wrld1))
2237
2253
               (triple (prove-termination-recursive
2238
2254
                        names arglists measures t-machines mp rel hints
2239
 
                        otf-flg bodies ctx ens wrld1 state)))
 
2255
                        otf-flg bodies measure-debug ctx ens wrld1 state)))
2240
2256
              (let* ((col (car triple))
2241
2257
                     (measure-alist (cadr triple))
2242
2258
                     (ttree (cddr triple)))
5660
5676
; Keep this in sync with deflabel XARGS.
5661
5677
 
5662
5678
  '(:guard :guard-hints :guard-debug
5663
 
           :hints :measure :ruler-extenders :mode :non-executable :normalize
 
5679
           :hints :measure :measure-debug
 
5680
           :ruler-extenders :mode :non-executable :normalize
5664
5681
           :otf-flg #+:non-standard-analysis :std-hints
5665
5682
           :stobjs :verify-guards :well-founded-relation
5666
5683
           :split-types))
7591
7608
 
7592
7609
                                              nil ; guard-debug default
7593
7610
                                              ctx state))
 
7611
      (measure-debug (get-unambiguous-xargs-flg :MEASURE-DEBUG
 
7612
                                                fives
 
7613
                                                nil ; guard-debug default
 
7614
                                                ctx state))
7594
7615
      (split-types-lst (get-boolean-unambiguous-xargs-flg-lst
7595
7616
                        :SPLIT-TYPES fives nil ctx state))
7596
7617
      (normalizeps (get-boolean-unambiguous-xargs-flg-lst
7791
7812
                                   wrld3
7792
7813
                                   non-executablep
7793
7814
                                   guard-debug
 
7815
                                   measure-debug
7794
7816
                                   split-types-terms
7795
7817
                                   ))))))))))))))))
7796
7818
 
7862
7884
;                  violate the translate conventions on stobjs.
7863
7885
;    guard-debug
7864
7886
;              - t or nil, used to add calls of EXTRA-INFO to guard conjectures
 
7887
;    measure-debug
 
7888
;              - t or nil, used to add calls of EXTRA-INFO to measure conjectures
7865
7889
;    split-types-terms
7866
7890
;              - list of translated terms, each corresponding to type
7867
7891
;                declarations made for a definition with XARGS keyword
7937
7961
                                 non-executablep ctx wrld state
7938
7962
                                 #+:non-standard-analysis std-p))))))))
7939
7963
 
 
7964
#+acl2-legacy-doc
7940
7965
(defmacro link-doc-to-keyword (name parent see)
7941
7966
  `(defdoc ,name
7942
7967
     ,(concatenate
7953
7978
       (string-downcase (symbol-name see))
7954
7979
       "].~/~/")))
7955
7980
 
 
7981
#+acl2-legacy-doc
7956
7982
(defmacro link-doc-to (name parent see)
7957
7983
  `(defdoc ,name
7958
7984
     ,(concatenate
8147
8173
      (wrld4 (update-w big-mutrec
8148
8174
                       (putprop-x-lst2-unless names 'split-types-term
8149
8175
                                              split-types-terms *t* wrld3)))
8150
 
 
8151
 
; Rockwell Addition:  To save time, the nu-rewriter doesn't look at
8152
 
; functions unless they contain nu-rewrite targets, as defined in
8153
 
; rewrite.lisp.  Here is where I store the property that says whether a
8154
 
; function is a target.
8155
 
 
8156
 
      (wrld5 (update-w
8157
 
              big-mutrec
8158
 
              (cond ((eq (car names) 'NTH)
8159
 
                     (putprop 'nth 'nth-update-rewriter-targetp
8160
 
                              t wrld4))
8161
 
                    ((getprop (car names) 'recursivep nil
8162
 
                              'current-acl2-world wrld4)
8163
 
 
8164
 
; Nth-update-rewriter does not go into recursive functions.  We could consider
8165
 
; redoing this computation when installing a new definition rule, as well as
8166
 
; the putprop below, but that's a heuristic decision that doesn't seem to be so
8167
 
; important.
8168
 
 
8169
 
                     wrld4)
8170
 
                    ((nth-update-rewriter-targetp (car bodies) wrld4)
8171
 
 
8172
 
; This precomputation of whether the body of the function is a
8173
 
; potential target for nth-update-rewriter is insensitive to whether
8174
 
; the functions being seen are disabled.  If the function being
8175
 
; defined calls a non-recursive function that uses NTH, then this
8176
 
; function is marked as being a target.  If later that subroutine is
8177
 
; disabled, then nth-update-rewriter will not go into it and this
8178
 
; function may no longer really be a potential target.  But if we do
8179
 
; not ``memoize'' the computation this way then it may be
8180
 
; exponentially slow, going repeatedly into large bodies called
8181
 
; more than one time in a function.
8182
 
 
8183
 
                     (putprop (car names)
8184
 
                              'nth-update-rewriter-targetp
8185
 
                              t wrld4))
8186
 
                    (t wrld4))))
8187
8176
      #+:non-standard-analysis
8188
8177
      (assumep
8189
8178
       (value (or (eq (ld-skip-proofsp state) 'include-book)
8194
8183
                      (verify-valid-std-usage names arglists bodies
8195
8184
                                              std-hints otf-flg
8196
8185
                                              (caddr tuple)
8197
 
                                              ctx ens wrld5 state)
 
8186
                                              ctx ens wrld4 state)
8198
8187
                    (value (cons col (caddr tuple)))))
8199
8188
      #+:non-standard-analysis
8200
8189
      (col (value (car col/ttree1)))
8203
8192
              #-:non-standard-analysis
8204
8193
              (value (caddr tuple))))
8205
8194
     (mv-let
8206
 
      (wrld6 ttree2)
 
8195
      (wrld5 ttree2)
8207
8196
      (putprop-body-lst names arglists bodies normalizeps
8208
8197
                        (getprop (car names) 'recursivep nil
8209
 
                                 'current-acl2-world wrld5)
8210
 
                        (make-controller-alist names wrld5)
 
8198
                                 'current-acl2-world wrld4)
 
8199
                        (make-controller-alist names wrld4)
8211
8200
                        #+:non-standard-analysis std-p
8212
 
                        ens wrld5 wrld5 nil)
 
8201
                        ens wrld4 wrld4 nil)
8213
8202
      (er-progn
8214
 
       (update-w big-mutrec wrld6)
 
8203
       (update-w big-mutrec wrld5)
8215
8204
       (mv-let
8216
 
        (wrld7 ttree2 state)
 
8205
        (wrld6 ttree2 state)
8217
8206
        (putprop-type-prescription-lst names
8218
8207
                                       subversive-p
8219
8208
                                       (fn-rune-nume (car names)
8220
 
                                                     t nil wrld6)
8221
 
                                       ens wrld6 ttree2 state)
 
8209
                                                     t nil wrld5)
 
8210
                                       ens wrld5 ttree2 state)
8222
8211
        (er-progn
8223
 
         (update-w big-mutrec wrld7)
 
8212
         (update-w big-mutrec wrld6)
8224
8213
         (er-let*
8225
 
          ((wrld8 (update-w big-mutrec
8226
 
                            (putprop-level-no-lst names wrld7)))
 
8214
          ((wrld7 (update-w big-mutrec
 
8215
                            (putprop-level-no-lst names wrld6)))
 
8216
           (wrld8 (update-w big-mutrec
 
8217
                            (putprop-primitive-recursive-defunp-lst
 
8218
                             names wrld7)))
8227
8219
           (wrld9 (update-w big-mutrec
8228
 
                            (putprop-primitive-recursive-defunp-lst
8229
 
                             names wrld8)))
8230
 
           (wrld9a (update-w big-mutrec
8231
 
                             (putprop-hereditarily-constrained-fnnames-lst
8232
 
                              names bodies wrld9)))
 
8220
                            (putprop-hereditarily-constrained-fnnames-lst
 
8221
                             names bodies wrld8)))
8233
8222
           (wrld10 (update-w big-mutrec
8234
8223
                             (put-invariant-risk
8235
8224
                              names
8236
8225
                              bodies
8237
8226
                              non-executablep
8238
8227
                              (update-doc-database-lst names docs pairs
8239
 
                                                       wrld9a))))
 
8228
                                                       wrld9))))
8240
8229
           (wrld11 (update-w big-mutrec
8241
8230
                             (putprop-x-lst1
8242
8231
                              names 'pequivs nil
8291
8280
 
8292
8281
(defun defuns-fn0 (names arglists docs pairs guards measures
8293
8282
                         ruler-extenders-lst mp rel hints guard-hints std-hints
8294
 
                         otf-flg guard-debug bodies symbol-class normalizeps
8295
 
                         split-types-terms non-executablep
 
8283
                         otf-flg guard-debug measure-debug bodies symbol-class
 
8284
                         normalizeps split-types-terms non-executablep
8296
8285
                         #+:non-standard-analysis std-p
8297
8286
                         ctx wrld state)
8298
8287
 
8317
8306
                                   hints
8318
8307
                                   otf-flg
8319
8308
                                   big-mutrec
 
8309
                                   measure-debug
8320
8310
                                   ctx ens wrld state)))
8321
8311
       (defuns-fn1
8322
8312
         tuple
8771
8761
                (wrld (nth 18 tuple))
8772
8762
                (non-executablep (nth 19 tuple))
8773
8763
                (guard-debug (nth 20 tuple))
8774
 
                (split-types-terms (nth 21 tuple)))
 
8764
                (measure-debug (nth 21 tuple))
 
8765
                (split-types-terms (nth 22 tuple)))
8775
8766
            (er-let*
8776
8767
             ((pair (defuns-fn0
8777
8768
                      names
8788
8779
                      std-hints
8789
8780
                      otf-flg
8790
8781
                      guard-debug
 
8782
                      measure-debug
8791
8783
                      bodies
8792
8784
                      symbol-class
8793
8785
                      normalizeps