Greetings, and thanks for noting this! 1) To iterate, basically all functions would need to be compiled at least twice. We start with a return type of nil, and repeat until consistency.
2) What about optional argument tail recursion? I.e. an optional argument state function? Take care, Matt Kaufmann <[EMAIL PROTECTED]> writes: > Hi -- > > Regarding mutual recursion: > > I haven't followed all of the ongoing thread about compilation, so the > following remarks may be off-base. But it seems to me unfortunate to require > anything about argument or output correspondence in order to make type > inferences about mutually recursive functions. In the case of ACL2, we mark > mutually recursive function nests explicitly (search for "mutual-recursion" in > the sources). So it would be easy for ACL2 to tell GCL which functions are > mutually recursive, though I don't know if that's helpful to you or if it's a > general enough solution for other Lisp users. So maybe instead of the "state" > approach, you could just recompile when signatures change until you reach a > fixed point (or just punt with * in signatures when some number of iterations > is exceeded)? > > For example, the following ACL2 source functions are, I believe, mutually > recursive, but they have very different signatures (and some return one value > while others do not). > > (defun ev-fncall-rec-logical (fn args w big-n safe-mode gc-off latches > hard-error-returns-nilp) > ...) > (defun ev-fncall-rec (fn args w big-n safe-mode gc-off latches > hard-error-returns-nilp) > ...) > (defun ev-rec (form alist w big-n safe-mode gc-off latches > hard-error-returns-nilp) > ...) > (defun ev-rec-lst (lst alist w big-n safe-mode gc-off latches > hard-error-returns-nilp) > ...) > (defun ev-rec-acl2-unwind-protect (form alist w big-n safe-mode gc-off > latches hard-error-returns-nilp) > ...) > (defun ev-fncall (fn args state latches hard-error-returns-nilp) > ...) > (defun ev (form alist state latches hard-error-returns-nilp) > ...) > (defun ev-lst (lst alist state latches hard-error-returns-nilp) > ...) > (defun ev-fncall-w (fn args w safe-mode gc-off hard-error-returns-nilp) > ...) > (defun ev-fncall-guard-er-msg (fn guard stobjs-in args w extra-msg) > ...) > (defun ev-fncall-guard-er (fn args w latches safep) > ...) > (defun ev-fncall-msg (val wrld) > ...) > (defun untranslate1 (term iff-flg binop-tbl preprocess-fn wrld) > ...) > (defun untranslate-cons1 (term binop-tbl preprocess-fn wrld) > ...) > (defun untranslate-cons (term binop-tbl preprocess-fn wrld) > ...) > (defun untranslate-if (term iff-flg binop-tbl preprocess-fn wrld) > ...) > (defun untranslate-into-case-clauses (key term iff-flg binop-tbl > preprocess-fn > wrld) > ...) > (defun untranslate-into-cond-clauses (term iff-flg binop-tbl preprocess-fn > wrld) > ...) > (defun untranslate1-lst (lst iff-flg binop-tbl preprocess-fn wrld) > ...) > > Thanks -- > -- Matt > Cc: [EMAIL PROTECTED], [EMAIL PROTECTED], gcl-devel@gnu.org > From: Camm Maguire <[EMAIL PROTECTED]> > Date: 29 Jun 2006 11:15:49 -0400 > X-SpamAssassin-Status: No, hits=-1.9 required=5.0 > X-UTCS-Spam-Status: No, hits=-115 required=200 > > Greetings, and thanks so much for this very helpful and infomative > comparison! > > I'm still going through this list, but regarding mutual recursion, I'd > like to point out this session: > > > ============================================================================= > cd v3-0-hons-gcl-proclaim > ./saved_acl2 > GCL (GNU Common Lisp) 2.7.0 ANSI Jun 24 2006 18:43:43 > Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd) > Binary License: GPL due to GPL'ed components: (BFD UNEXEC) > Modifications of this banner must retain notice of a compatible license > Dedicated to the memory of W. Schelter > > Use (help) to get some basic information on how to use GCL. > > Temporary directory for compiler files set to /tmp/ > > ACL2 Version 3.0 built June 25, 2006 14:59:57. > Copyright (C) 2006 University of Texas at Austin > ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you > are welcome to redistribute it under certain conditions. For details, > see the GNU General Public License. > > Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). > MODIFIED for hons and such. > > See the documentation topic note-3-0 for recent changes. > Note: We have modified the prompt in some underlying Lisps to further > distinguish it from the ACL2 prompt. > > NOTE!! Proof trees are disabled in ACL2. To enable them in emacs, > look under the ACL2 source directory in interface/emacs/README.doc; > and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 > command loop. Look in the ACL2 documentation under PROOF-TREE. > > ACL2 Version 3.0. Level 1. Cbd > "/v/filer3/projects-hunt/hvg/ACL2/v3-0-hons-gcl-proclaim/". > Type :help for help. > Type (good-bye) to quit completely out of ACL2. > > ACL2 !>:q > > Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). > ACL2>(in-package 'si) > > #<"SYSTEM" package> > > SYSTEM>(maphash (lambda (x y) > (when (eq '* (cadr (call-sig y))) > (let* ((e (all-callees x nil)) > (r (all-callers x nil)) > (i (intersection e r))) > (when (and (remove x i) > (every (lambda (z) (equal (call-sig > (gethash z > *call-hash-table*)) (call-sig y))) i)) > (print (list x i)))))) *call-hash-table*) > > (ACL2::BACKQUOTE-LST (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE)) > (ACL2::BACKQUOTE (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE)) > (ACL2::GET-INDUCTION-CANDS (ACL2::GET-INDUCTION-CANDS-LST)) > (ACL2::GET-INDUCTION-CANDS-LST > (ACL2::GET-INDUCTION-CANDS ACL2::GET-INDUCTION-CANDS-LST)) > (ACL2::DEREF-VAR (ACL2::DEREF-VAR ACL2::DEREF)) > (ACL2::DEREF (ACL2::DEREF-VAR ACL2::DEREF)) > (ACL2::OCCUR-CNT-REC (ACL2::OCCUR-CNT-LST ACL2::OCCUR-CNT-REC)) > (ACL2::OCCUR-CNT-LST (ACL2::OCCUR-CNT-REC ACL2::OCCUR-CNT-LST)) > (ACL2::MEMBER-TERM (ACL2::MEMBER-COMPLEMENT-TERM ACL2::MEMBER-TERM)) > (ACL2::MEMBER-COMPLEMENT-TERM > (ACL2::MEMBER-TERM ACL2::MEMBER-COMPLEMENT-TERM)) > NIL > > SYSTEM>(call-sig (gethash 'acl2::member-term *call-hash-table*)) > > ((T T) *) > > SYSTEM>(convert-to-state 'acl2::member-term) > > ACL2::MEMBER-TERM4313 > > SYSTEM>(function-src 'ACL2::MEMBER-TERM4313) > > (LAMBDA (ACL2::LIT ACL2::CL STATE) > (DECLARE (FIXNUM STATE)) > (DECLARE (OPTIMIZE (SAFETY 0))) > (BLOCK ACL2::MEMBER-TERM4313 > (MACROLET > ((ACL2::MEMBER-COMPLEMENT-TERM (ACL2::LIT ACL2::CL) > (LIST 'ACL2::MEMBER-TERM4313 ACL2::LIT ACL2::CL 0)) > (ACL2::MEMBER-TERM (ACL2::LIT ACL2::CL) > (LIST 'ACL2::MEMBER-TERM4313 ACL2::LIT ACL2::CL 1))) > (CASE STATE > (0 > (FUNCALL (LAMBDA (ACL2::LIT ACL2::CL) > (DECLARE (OPTIMIZE (SAFETY 0))) > (BLOCK ACL2::MEMBER-COMPLEMENT-TERM > (LET* () > (IF (ATOM ACL2::LIT) > (ACL2::MEMBER-COMPLEMENT-TERM1 ACL2::LIT > ACL2::CL) > (IF (EQ 'QUOTE (CAR ACL2::LIT)) > (ACL2::MEMBER-COMPLEMENT-TERM1 > ACL2::LIT ACL2::CL) > (IF (LET > ((#:G15388 > (EQ (CAR ACL2::LIT) 'EQUAL))) > (IF #:G15388 #:G15388 > (EQ (CAR ACL2::LIT) 'ACL2::IFF))) > (ACL2::MEMBER-COMPLEMENT-TERM2 > (CAR ACL2::LIT) > (CAR (CDR ACL2::LIT)) > (CAR (CDR (CDR ACL2::LIT))) > ACL2::CL) > (IF (EQ (CAR ACL2::LIT) 'NOT) > (ACL2::MEMBER-TERM > (CAR (CDR ACL2::LIT)) ACL2::CL) > (ACL2::MEMBER-COMPLEMENT-TERM1 > ACL2::LIT ACL2::CL)))))))) > ACL2::LIT ACL2::CL)) > (OTHERWISE > (FUNCALL (LAMBDA (ACL2::LIT ACL2::CL) > (DECLARE (OPTIMIZE (SAFETY 0))) > (DECLARE (OPTIMIZE (SAFETY 0))) > (BLOCK ACL2::MEMBER-TERM > (LET* () > (BLOCK ACL2::MEMBER-TERM > (LET* () > (IF (ATOM ACL2::LIT) > (ACL2::MEMBER-EQ ACL2::LIT ACL2::CL) > (IF (EQ 'QUOTE (CAR ACL2::LIT)) > (ACL2::MEMBER-EQUAL ACL2::LIT > ACL2::CL) > (IF > (LET > ((#:G15387 > (EQ (CAR ACL2::LIT) 'EQUAL))) > (IF #:G15387 #:G15387 > (EQ (CAR ACL2::LIT) 'ACL2::IFF))) > (ACL2::MEMBER-TERM2 > (CAR ACL2::LIT) > (CAR (CDR ACL2::LIT)) > (CAR (CDR (CDR ACL2::LIT))) > ACL2::CL) > (IF (EQ (CAR ACL2::LIT) 'NOT) > (ACL2::MEMBER-COMPLEMENT-TERM > (CAR (CDR ACL2::LIT)) ACL2::CL) > (ACL2::MEMBER-EQUAL ACL2::LIT > ACL2::CL)))))))))) > ACL2::LIT ACL2::CL)))))) > NIL > ACL2::MEMBER-TERM4313 > > SYSTEM>(compile 'ACL2::MEMBER-TERM4313) > > ;; Compiling /tmp/gazonk_7059_0.lsp. > ;; End of Pass 1. > ;; End of Pass 2. > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > ;; Finished compiling /tmp/gazonk_7059_0.o. > Loading /tmp/gazonk_7059_0.o > Callee ACL2::MEMBER-TERM4313 sigchange NIL to ((T T > (INTEGER -2147483648 > 2147483647)) > T), recompiling > ACL2::MEMBER-COMPLEMENT-TERM > Callee ACL2::MEMBER-TERM4313 sigchange NIL to ((T T > (INTEGER -2147483648 > 2147483647)) > T), recompiling > ACL2::MEMBER-TERM > ;; Compiling /tmp/gazonk_7059_ymjCh7.lsp. > ;; End of Pass 1. > ;; End of Pass 2. > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > ;; Finished compiling /tmp/gazonk_7059_ymjCh7.o. > Loading /tmp/gazonk_7059_ymjCh7.o > start address -T 0xadd8f58 Finished loading /tmp/gazonk_7059_ymjCh7.o > Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T), > recompiling ACL2::SOME-ELEMENT-MEMBER-COMPLEMENT-TERM > Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T), > recompiling ACL2::ADD-LITERAL > Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T), > recompiling ACL2::ADD-LITERAL-AND-PT > ;; Compiling /tmp/gazonk_7059_sxyINA.lsp. > ;; End of Pass 1. > ;; End of Pass 2. > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > ;; Finished compiling /tmp/gazonk_7059_sxyINA.o. > Loading /tmp/gazonk_7059_sxyINA.o > start address -T 0xadda7a0 Finished loading /tmp/gazonk_7059_sxyINA.o > start address -T 0xadc24e0 Finished loading /tmp/gazonk_7059_0.o > #<compiled-function ACL2::MEMBER-TERM4313> > NIL > NIL > > SYSTEM> > > ============================================================================= > > The questions are: > > 1) what is the proper mutual recursion detection mechanism -- > i.e. if we only require that the arg types of the mutual recursion > members match, then we get the following list: > > (ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF > (ACL2::DISTRIBUTE-FIRST-IF ACL2::NORMALIZE ACL2::NORMALIZE-LST > ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF)) > (ACL2::DISTRIBUTE-FIRST-IF > (ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF ACL2::NORMALIZE > ACL2::NORMALIZE-LST)) > (ACL2::NORMALIZE > (ACL2::DISTRIBUTE-FIRST-IF ACL2::NORMALIZE ACL2::NORMALIZE-LST > ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF)) > (ACL2::BACKQUOTE-LST (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE)) > (ACL2::BACKQUOTE (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE)) > (ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC > (ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC-LIST > ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC)) > (ACL2::TS-INTERSECTION-FN > (ACL2::EVAL-TYPE-SET-LST ACL2::EVAL-TYPE-SET ACL2::TS-UNION-FN > ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN)) > (ACL2::TS-UNION-FN > (ACL2::EVAL-TYPE-SET-LST ACL2::EVAL-TYPE-SET ACL2::TS-UNION-FN > ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN)) > (ACL2::EVAL-TYPE-SET > (ACL2::TS-UNION-FN ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN > ACL2::EVAL-TYPE-SET-LST)) > (ACL2::CONTAINS-CONSTRAINED-CONSTANTP > (ACL2::CONTAINS-CONSTRAINED-CONSTANTP > ACL2::CONTAINS-CONSTRAINED-CONSTANTP-LST)) > (ACL2::FREE-OR-BOUND-VARS > (ACL2::FREE-OR-BOUND-VARS-LST ACL2::FREE-OR-BOUND-VARS)) > (COMPILER::T1EXPR (COMPILER::T1ORDINARY COMPILER::T1EXPR)) > (ACL2::FFNNAMES-SUBSETP > (ACL2::FFNNAMES-SUBSETP ACL2::FFNNAMES-SUBSETP-LISTP)) > (ACL2::GET-INDUCTION-CANDS (ACL2::GET-INDUCTION-CANDS-LST)) > (ACL2::GET-INDUCTION-CANDS-LST > (ACL2::GET-INDUCTION-CANDS ACL2::GET-INDUCTION-CANDS-LST)) > (ACL2::ALMOST-QUOTEP1 > (ACL2::ALMOST-QUOTEP1-LISTP ACL2::ALMOST-QUOTEP1)) > (ACL2::MULT-RELIEVE-FC-HYPS > (ACL2::MULT-RELIEVE-FC-HYPS ACL2::MULT-RELIEVE-ALL-FC-HYPS)) > (ACL2::FIND-FIRST-NON-LOCAL-NAME > (ACL2::FIND-FIRST-NON-LOCAL-NAME-LST > ACL2::FIND-FIRST-NON-LOCAL-NAME)) > (ACL2::ALL-CALLS (ACL2::ALL-CALLS-LST ACL2::ALL-CALLS)) > (ACL2::FFNNAMEP-MOD-MBE > (ACL2::FFNNAMEP-MOD-MBE-LST ACL2::FFNNAMEP-MOD-MBE)) > (ACL2::EV-REC > (ACL2::EV-REC-ACL2-UNWIND-PROTECT ACL2::EV-REC ACL2::EV-REC-LST > ACL2::EV-FNCALL-REC ACL2::EV-FNCALL-REC-LOGICAL)) > (ACL2::DEREF-VAR (ACL2::DEREF-VAR ACL2::DEREF)) > (ACL2::DEREF (ACL2::DEREF-VAR ACL2::DEREF)) > (ACL2::OCCUR-CNT-REC (ACL2::OCCUR-CNT-LST ACL2::OCCUR-CNT-REC)) > (ACL2::OCCUR-CNT-LST (ACL2::OCCUR-CNT-REC ACL2::OCCUR-CNT-LST)) > (ACL2::COLLECT-FFNNAMES > (ACL2::COLLECT-FFNNAMES-LST ACL2::COLLECT-FFNNAMES)) > > > ============================================================================= > SYSTEM>(mapcar (lambda (x) (call-sig (gethash x *call-hash-table*))) > '(ACL2::NOTE-CERTIFICATION-WORLD ACL2::NOTE-CERTIFICATION-WORLD-LST)) > > (((T T T T T T) *) ((T T T T T T) (VALUES T T T))) > > SYSTEM>(compile (convert-to-state 'ACL2::NOTE-CERTIFICATION-WORLD)) > > ;; Compiling /tmp/gazonk_7059_0.lsp. > ;; End of Pass 1. > ;; End of Pass 2. > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > ;; Finished compiling /tmp/gazonk_7059_0.o. > Loading /tmp/gazonk_7059_0.o > Callee ACL2::NOTE-CERTIFICATION-WORLD4331 sigchange NIL to ((T T T T T > T > (INTEGER > -2147483648 > 2147483647)) > (VALUES T T > T)), > recompiling ACL2::NOTE-CERTIFICATION-WORLD > Callee ACL2::NOTE-CERTIFICATION-WORLD4331 sigchange NIL to ((T T T T T > T > (INTEGER > -2147483648 > 2147483647)) > (VALUES T T > T)), > recompiling ACL2::NOTE-CERTIFICATION-WORLD-LST > ;; Compiling /tmp/gazonk_7059_8mFHt7.lsp. > ;; End of Pass 1. > ;; End of Pass 2. > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > ;; Finished compiling /tmp/gazonk_7059_8mFHt7.o. > Loading /tmp/gazonk_7059_8mFHt7.o > start address -T 0xadc2710 Finished loading /tmp/gazonk_7059_8mFHt7.o > start address -T 0xadbd000 Finished loading /tmp/gazonk_7059_0.o > #<compiled-function ACL2::NOTE-CERTIFICATION-WORLD4331> > NIL > NIL > > > ============================================================================= > > 2) How does one unwind the state function when any of its elements are > redefined? At one point I was thinking of passing the state > integer straight from the caller and relying on the existing > fast-link redirect mechanism to redeirect the call to the newly > redefined function from the compiled code of the caller -- this > however misses all the implicit calls from the other members of the > mutual recursion group, as they are now just wrappers to a > self-recursive state function. Now I'm thinking the cleanest > solution is to simply redefine all the group members when any one > of them are redefined. > > More explicitly: > > (defun foo (x) (unless (< x 0) (not (bar (1- x))))) > (defun bar (x) (unless (< x 0) (not (foo (1- x))))) > > convert-to-state -> > > (defun foo4351 (X STATE) > (DECLARE (FIXNUM STATE)) > (DECLARE (OPTIMIZE (SAFETY 0))) > (BLOCK FOO4351 > (MACROLET > ((BAR (X) (LIST 'FOO4351 X 0)) (FOO (X) (LIST 'FOO4351 X 1))) > (CASE STATE > (0 > (FUNCALL (LAMBDA (X) > (DECLARE (OPTIMIZE (SAFETY 0))) > (BLOCK BAR > (LET* () > (IF (NOT (< X 0)) (PROGN (NOT (FOO (- X 1)))))))) > X)) > (OTHERWISE > (FUNCALL (LAMBDA (X) > (DECLARE (OPTIMIZE (SAFETY 0))) > (DECLARE (OPTIMIZE (SAFETY 0))) > (BLOCK FOO > (LET* () > (BLOCK FOO > (LET* () > (IF (NOT (< X 0)) > (PROGN (NOT (BAR (- X 1)))))))))) > X)))))) > > (defun foo (X) (BLOCK FOO (FOO4351 X 1))) > (defun bar (X) (BLOCK BAR (FOO4351 X 0))) > > If then any of foo or bar are redefined, the other one needs to be > redefined to its origianl source. > > Eventually this should be an automatic part of do-recompile. > > I don't know if any performance sensitive code of yours is in this > form, but if so this should definitely be an improvement. Tha takr > benchmark is dramatically accelerated. > > Take care, > > Matt Kaufmann <[EMAIL PROTECTED]> writes: > > > Howdy -- > > > > Attached is a file that I used to explore discrepancies between ACL2 and > GCL in > > auto-generation of function type declarations. You probably don't need > to look > > at it unless you want to tweak it to get a more refined comparison (I > don't > > think I'll have time to do more of this for awhile but I can add > comments to > > the code and/or answer questions if you want to play with the code) or > see > > detailed results -- I'll summarize key things of interest to you just > below. > > > > First, here's the most interesting thing I found: a compiler bug that > appears > > to be due to a mistaken automatic proclaim involving > multiple-value-prog1. > > > > sundance:~> /p/bin/xg > > GCL (GNU Common Lisp) 2.7.0 ANSI Jun 24 2006 18:43:43 > > Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd) > > Binary License: GPL due to GPL'ed components: (BFD UNEXEC) > > Modifications of this banner must retain notice of a compatible license > > Dedicated to the memory of W. Schelter > > > > Use (help) to get some basic information on how to use GCL. > > > > Temporary directory for compiler files set to /tmp/ > > > > >(defun buggy () > > (multiple-value-prog1 > > (values 3 4) > > 5)) > > > > BUGGY > > > > >(buggy) > > > > 3 > > 4 > > > > >(compile 'buggy) > > > > ;; Compiling /tmp/gazonk_25691_0.lsp. > > ;; End of Pass 1. > > ;; End of Pass 2. > > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > > ;; Finished compiling /tmp/gazonk_25691_0.o. > > Loading /tmp/gazonk_25691_0.o > > start address -T 0xac70fe0 Finished loading /tmp/gazonk_25691_0.o > > #<compiled-function BUGGY> > > NIL > > NIL > > > > >(buggy) > > > > 3 > > > > >(get 'buggy 'si:proclaimed-return-type) > > > > T > > > > > > > > > The only other thing you are likely to find interesting is the > following, where > > I suspect that the return type could also correctly be deduced as T > rather than > > as the weaker *. > > > > (compile (defun weak (name) (setf (get name 'abc) nil))) > > > > ;; Compiling /tmp/gazonk_25691_0.lsp. > > ;; End of Pass 1. > > ;; End of Pass 2. > > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, > Speed=3, (Debug quality ignored) > > ;; Finished compiling /tmp/gazonk_25691_0.o. > > Loading /tmp/gazonk_25691_0.o > > start address -T 0xac795d8 Finished loading /tmp/gazonk_25691_0.o > > #<compiled-function WEAK> > > NIL > > NIL > > > > >(get 'weak 'si:proclaimed-return-type) > > > > * > > > > > > > > > Note that I deliberately coerced every declaration that implies fixnum > into > > simply 'fixnum for purposes of limiting discrepancies to interesting > cases. So > > for example, if ACL2 deduced an type of (integer 0 1000) for some > function > > argument and GCL had (signed-byte 28) for thta same argument, then this > would > > not be considered a discrepancy (both would be treated as fixnum). > > > > Most of the file is the analysis of input type discrepancies (see > "Resulting > > value of *args-mismatches*:") and output type discrepancies (see > "Resulting > > value of *output-mismatches*:"). Here are the parts of that that I > think you > > might find a little interesting, but there's nothing else major. > > > > + Many are marked with "; Mutual recursion", meaning that GCL made a > weaker > > inference than ACL2, but the function is mutually recursive with others > > (specifically, defined using (mutual-recursion (defun ...) (defun ...) > ...) > > in the ACL2 sources), so maybe this isn't news to you. > > > > + Many are marked with "GCL is missing STRING declaration (maybe not > > important?)", or substitute other types for STRING. My guess on an > > explanation is that you simply don't bother inferring types that don't > do the > > compiler any good. > > > > + There is a bug in the ACL2 3.0 sources, since fixed (thanks to Bob > Boyer), > > such that functions calling intern (or functions calling THOSE > functions, > > etc.) are returning two values instead of the intended single value. > > Mismatches due to this bug are marked with "[Intern]" and are probably > of no > > interest to you. > > > > + In a few cases GCL gets a type where ACL2 does not (marked with "GCL > nicely > > propagates where ACL2 does not:" or "Nice job by GCL"). > > > > + One GCL type inference was wrong due to the compiler bug mentioned > early in > > this email (search for "problem with multiple-value-prog1"). > > > > + One GCL type inference was weak due to the weak handling of setf shown > > earlier in this email. > > > > -- > Camm Maguire [EMAIL > PROTECTED] > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > -- Camm Maguire [EMAIL PROTECTED] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list Gcl-devel@gnu.org http://lists.gnu.org/mailman/listinfo/gcl-devel
