[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: Compiling a function for ppr breaks GCL
|
From: |
Matt Kaufmann |
|
Subject: |
[Gcl-devel] Re: Compiling a function for ppr breaks GCL |
|
Date: |
Tue, 7 Dec 2004 10:11:46 -0600 |
Thanks, Camm --
Your reply is consistent with the one I sent (they probably crossed in the
mail), but it's reassuring to see it since you understand the GCL side of
things much better than I do!
Regarding:
>> Hope this helps. Obviously I don't know what the limits on col are
>> which enabled ACL2 to infer that it could use a fixnum to represent
>> the argument.
The following edited transcript is lower-level than most may want, but I think
it illustrates what is going on. ACL2 simply uses type declarations from the
top-level declare form to create the appropriate proclaim form. Then it's up
to GCL to treat, for example, a (signed-byte 29) as a fixnum.
ACL2 !>(trace$ make-defun-declare-form)
NIL
ACL2 !>(defun foo (x y)
(declare (type (signed-byte 29) x))
(mv (1+ x) y))
.....
1> (MAKE-DEFUN-DECLARE-FORM
(DEFUN FOO (X Y)
(DECLARE (TYPE (SIGNED-BYTE 29) X))
(MV (1+ X) Y)))
<1 (MAKE-DEFUN-DECLARE-FORM
(PROCLAIM '(FTYPE (FUNCTION ((SIGNED-BYTE 29) T) T) FOO)))
.....
-- Matt
X-IronPort-MID: 339144758
X-SBRS: 1.9
X-BrightmailFiltered: true
X-Ironport-AV: i="3.87,129,1099288800";
d="scan'208"; a="339144758:sNHT15830076"
Cc: ACL2 Help <address@hidden>, address@hidden
From: Camm Maguire <address@hidden>
Date: 07 Dec 2004 11:03:01 -0500
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Content-Type: text/plain; charset=us-ascii
Reply-To: address@hidden
Sender: address@hidden
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-352 required=180
Greetings!
This is due to the sophisticated use acl2 makes of GCL's function
proclamation mechanism. In brief, argument and return types can be
inferred, proclaimed, stored in the function symbol's property list,
and used in GCL's compiler to write lisp function calls as direct C
calls without argument type checking at runtime, if compiling with
*safety* 0, the acl2 default. One great GCL feature, IMHO, is the
ability to toggle this 'fast function calling' mechanism at runtime
via (si::use-fast-links nil). Doing so, for example, in your case
defaults to slower function calling with argument type checking,
allowing the compilation to proceed.
In more detail, the ACL2 knows the following about ppr out of the box:
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(symbol-plist 'ppr)
(COMPILER::PROCLAIMED-FUNCTION T COMPILER::PROCLAIMED-RETURN-TYPE T
COMPILER::PROCLAIMED-ARG-TYPES (T FIXNUM T T T)
#:*CURRENT-ACL2-WORLD-KEY*
((SYMBOL-CLASS :PROGRAM) (STOBJS-OUT (STATE))
(FORMALS (X COL CHANNEL STATE EVISCP))
(STOBJS-IN (NIL NIL NIL STATE NIL))
(GUARD (SIGNED-BYTE-P '29 COL)) (ABSOLUTE-EVENT-NUMBER 897))
#:*GLOBAL-SYMBOL-KEY* ACL2_GLOBAL_ACL2::PPR *PREDEFINED* T
SYSTEM:PNAME "PPR")
After your redefinition, this becomes the following:
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(symbol-plist 'ppr)
(#:*CURRENT-ACL2-WORLD-KEY*
((COARSENINGS NIL) (CONGRUENCES NIL)
(TYPE-PRESCRIPTIONS
((0 (1754 PPR X COL CHANNEL STATE EVISCP) NIL
((STATE) :TYPE-PRESCRIPTION PPR) EQUAL
(PPR X COL CHANNEL STATE EVISCP) STATE))
((0 (NIL PPR X COL CHANNEL STATE EVISCP) NIL
((STATE) :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
((0 (NIL PPR X COL CHANNEL STATE EVISCP) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T)))
(RUNIC-MAPPING-PAIRS
((1752 :DEFINITION PPR) (1753 :EXECUTABLE-COUNTERPART PPR)
(1754 :TYPE-PRESCRIPTION PPR)))
(RECURSIVEP NIL)
(SYMBOL-CLASS :IDEAL :ACL2-PROPERTY-UNBOUND :PROGRAM)
(LEMMAS ((REWRITE-RULE (:DEFINITION PPR) 1752 NIL EQUAL
(PPR X COL CHANNEL STATE EVISCP) STATE ABBREVIATION
NIL NIL)))
(STOBJS-OUT (STATE) :ACL2-PROPERTY-UNBOUND (STATE))
(FORMALS (X COL CHANNEL STATE EVISCP) :ACL2-PROPERTY-UNBOUND
(X COL CHANNEL STATE EVISCP))
(STOBJS-IN (NIL NIL NIL STATE NIL) :ACL2-PROPERTY-UNBOUND
(NIL NIL NIL STATE NIL))
(BODY STATE)
(GUARD :ACL2-PROPERTY-UNBOUND (SIGNED-BYTE-P '29 COL))
(PRIMITIVE-RECURSIVE-DEFUNP T) (LEVEL-NO 0)
(UNNORMALIZED-BODY STATE)
(REDEFINED
(:OVERWRITE PPR (X COL CHANNEL STATE EVISCP)
(NIL NIL NIL STATE NIL) (STATE)))
(ABSOLUTE-EVENT-NUMBER 5409 :ACL2-PROPERTY-UNBOUND 897))
*UNDO-STACK*
((PROGN
(SETF (SYMBOL-FUNCTION 'PPR) '#<compiled-function PPR>)
(SETF (SYMBOL-FUNCTION 'ACL2_*1*_ACL2::PPR)
'#<compiled-function ACL2_*1*_ACL2::PPR>)))
COMPILER::PROCLAIMED-FUNCTION T COMPILER::PROCLAIMED-RETURN-TYPE T
COMPILER::PROCLAIMED-ARG-TYPES (T T T T T) #:*GLOBAL-SYMBOL-KEY*
ACL2_GLOBAL_ACL2::PPR *PREDEFINED* T SYSTEM:PNAME "PPR")
So we see that acl2 will have pre-compiled functions in place
expecting to call ppr with a fixnum second argment, but the function
has been changed to make this a generic lisp object. As stated
earlier, turning off 'fast-links' will enable all to go through, but
we can do better by:
ACL2 !>(defun ppr (x col channel state eviscp)
(declare (type (integer 0 500) col) (ignore x col channel eviscp))
state)
ACL2 Query (:REDEF): The name PPR is in use as a function. Its current
defun-mode is :logic. Do you want to redefine it? (N, Y, E, O or ?):
Y
Since PPR is non-recursive, its admission is trivial. We observe that
the type of PPR is described by the theorem
(EQUAL (PPR X COL CHANNEL STATE EVISCP) STATE).
(PPR * * * STATE *) => STATE.
The guard conjecture for PPR is trivial to prove. PPR is compliant
with Common Lisp.
Summary
Form: ( DEFUN PPR ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(symbol-plist 'ppr)
(#:*CURRENT-ACL2-WORLD-KEY*
((COARSENINGS NIL NIL) (CONGRUENCES NIL NIL)
(TYPE-PRESCRIPTIONS
((0 (1757 PPR X COL CHANNEL STATE EVISCP) NIL
((STATE) :TYPE-PRESCRIPTION PPR) EQUAL
(PPR X COL CHANNEL STATE EVISCP) STATE))
((0 (NIL PPR X COL CHANNEL STATE EVISCP) NIL
((STATE) :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
((0 (NIL PPR X COL CHANNEL STATE EVISCP) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
:ACL2-PROPERTY-UNBOUND
((0 (1754 PPR X COL CHANNEL STATE EVISCP) NIL
((STATE) :TYPE-PRESCRIPTION PPR) EQUAL
(PPR X COL CHANNEL STATE EVISCP) STATE))
((0 (NIL PPR X COL CHANNEL STATE EVISCP) NIL
((STATE) :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T))
((0 (NIL PPR X COL CHANNEL STATE EVISCP) NIL
(NIL :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) QUOTE T)))
(RUNIC-MAPPING-PAIRS
((1755 :DEFINITION PPR) (1756 :EXECUTABLE-COUNTERPART PPR)
(1757 :TYPE-PRESCRIPTION PPR))
:ACL2-PROPERTY-UNBOUND
((1752 :DEFINITION PPR) (1753 :EXECUTABLE-COUNTERPART PPR)
(1754 :TYPE-PRESCRIPTION PPR)))
(RECURSIVEP NIL :ACL2-PROPERTY-UNBOUND NIL)
(SYMBOL-CLASS :COMMON-LISP-COMPLIANT :IDEAL :ACL2-PROPERTY-UNBOUND
:IDEAL :ACL2-PROPERTY-UNBOUND :PROGRAM)
(LEMMAS ((REWRITE-RULE (:DEFINITION PPR) 1755 NIL EQUAL
(PPR X COL CHANNEL STATE EVISCP) STATE ABBREVIATION
NIL NIL))
NIL
((REWRITE-RULE (:DEFINITION PPR) 1752 NIL EQUAL
(PPR X COL CHANNEL STATE EVISCP) STATE ABBREVIATION
NIL NIL)))
(STOBJS-OUT (STATE) :ACL2-PROPERTY-UNBOUND (STATE)
:ACL2-PROPERTY-UNBOUND (STATE))
(FORMALS (X COL CHANNEL STATE EVISCP) :ACL2-PROPERTY-UNBOUND
(X COL CHANNEL STATE EVISCP) :ACL2-PROPERTY-UNBOUND
(X COL CHANNEL STATE EVISCP))
(STOBJS-IN (NIL NIL NIL STATE NIL) :ACL2-PROPERTY-UNBOUND
(NIL NIL NIL STATE NIL) :ACL2-PROPERTY-UNBOUND
(NIL NIL NIL STATE NIL))
(BODY STATE :ACL2-PROPERTY-UNBOUND STATE)
(GUARD (IF (INTEGERP COL)
(IF (NOT (< COL '0)) (NOT (< '500 COL)) 'NIL) 'NIL)
:ACL2-PROPERTY-UNBOUND (SIGNED-BYTE-P '29 COL))
(PRIMITIVE-RECURSIVE-DEFUNP T :ACL2-PROPERTY-UNBOUND T)
(LEVEL-NO 0 :ACL2-PROPERTY-UNBOUND 0)
(UNNORMALIZED-BODY STATE :ACL2-PROPERTY-UNBOUND STATE)
(REDEFINED
(:OVERWRITE PPR (X COL CHANNEL STATE EVISCP)
(NIL NIL NIL STATE NIL) (STATE))
(:OVERWRITE PPR (X COL CHANNEL STATE EVISCP)
(NIL NIL NIL STATE NIL) (STATE)))
(ABSOLUTE-EVENT-NUMBER 5410 :ACL2-PROPERTY-UNBOUND 5409
:ACL2-PROPERTY-UNBOUND 897))
*UNDO-STACK*
((PROGN
(SETF (SYMBOL-FUNCTION 'PPR)
'(LISP:LAMBDA-BLOCK PPR (X COL CHANNEL STATE EVISCP)
(DECLARE (IGNORE X COL CHANNEL EVISCP))
STATE))
(SETF (SYMBOL-FUNCTION 'ACL2_*1*_ACL2::PPR)
'(LISP:LAMBDA-BLOCK ACL2_*1*_ACL2::PPR
(X COL CHANNEL STATE EVISCP)
(LET ((ACL2_*1*_ACL2::PPR
(SYMBOL-CLASS 'PPR (W *THE-LIVE-STATE*))))
(COND
((EQ ACL2_*1*_ACL2::PPR :COMMON-LISP-COMPLIANT)
(RETURN-FROM ACL2_*1*_ACL2::PPR
(PPR X COL CHANNEL STATE EVISCP))))
(MAYBE-WARN-FOR-GUARD PPR)
(LABELS ((ACL2_*1*_ACL2::PPR
(X COL CHANNEL STATE EVISCP)
(DECLARE (IGNORE X COL CHANNEL EVISCP))
STATE))
(ACL2_*1*_ACL2::PPR X COL CHANNEL STATE EVISCP))))))
(PROGN
(SETF (SYMBOL-FUNCTION 'PPR) '#<compiled-function PPR>)
(SETF (SYMBOL-FUNCTION 'ACL2_*1*_ACL2::PPR)
'#<compiled-function ACL2_*1*_ACL2::PPR>)))
COMPILER::PROCLAIMED-FUNCTION T COMPILER::PROCLAIMED-RETURN-TYPE T
COMPILER::PROCLAIMED-ARG-TYPES (T FIXNUM T T T)
#:*GLOBAL-SYMBOL-KEY* ACL2_GLOBAL_ACL2::PPR *PREDEFINED* T
SYSTEM:PNAME "PPR")
ACL2>:q
:Q
ACL2>(lp)
ACL2 Version 2.9. Level 1. Cbd "/home/camm/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>:comp t
[SGC for 21 STRING pages..(8279 writable)..(T=1).GC finished]
Compiling /home/camm/TMP.lisp.
End of Pass 1.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /home/camm/TMP.lisp.
Loading /home/camm/TMP.o
start address -T 0x9db3f60 Finished loading /home/camm/TMP.o
Compiling /home/camm/TMP1.lisp.
End of Pass 1.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /home/camm/TMP1.lisp.
Loading /home/camm/TMP1.o
start address -T 0x911b000 Finished loading /home/camm/TMP1.o
ACL2 !>
Hope this helps. Obviously I don't know what the limits on col are
which enabled ACL2 to infer that it could use a fixnum to represent
the argument.
Take care,
"David L. Rager" <address@hidden> writes:
> Howdy All,
>
> I'm wondering if anyone can help shed some light on why running the
> following from a fresh ACL2 GCL prompt breaks GCL. It works fine in
> ACL (doesn't blow up - does yield blank output, as it should).
>
> ; begin test code
> (set-state-ok t)
> :redef
> (defun ppr (x col channel state eviscp)
> (declare (ignore x col channel eviscp))
> state)
> :comp t
>
> The error message is:
> "Error: Arg or result mismatch in call to PPR". From what I can
> tell, the function signature is correct, and ppr currently returns
> state with some side effects.
>
>
> This is related to a couple patches that demonstrate pretty printing
> and hiding. Since over the summer I actually modified the sources, I
> had access to the #-acl2-loop-only and #+acl2-loop-only prefixes. With
> the patches, I require two loads: one for ACL2 and one for CL. Then a
> ":comp t" must be issued so the functions run at a reasonable
> speed. It is the ":comp t" that breaks the code.
>
> Thanks!
> David
>
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah