initial implementation of row-polymorphism check

db4
Joe Groff 2010-03-04 19:30:08 -08:00
parent afaaf30679
commit 23de281186
4 changed files with 210 additions and 2 deletions

View File

@ -32,4 +32,11 @@ ERROR: inconsistent-recursive-call-error < inference-error word ;
ERROR: transform-expansion-error < inference-error error continuation word ;
ERROR: bad-declaration-error < inference-error declaration ;
ERROR: bad-declaration-error < inference-error declaration ;
ERROR: invalid-quotation-input < inference-error branches quots ;
ERROR: invalid-effect-variable < inference-error effect ;
ERROR: effect-variable-can't-have-type < inference-error effect ;

View File

@ -11,6 +11,7 @@ stack-checker.backend
stack-checker.branches
stack-checker.known-words
stack-checker.dependencies
stack-checker.row-polymorphism
stack-checker.recursive-state ;
IN: stack-checker.inlining
@ -141,6 +142,7 @@ SYMBOL: enter-out
: inline-word ( word -- )
commit-literals
[ depends-on-definition ]
[ infer-polymorphic? get [ check-polymorphic-effect ] [ drop ] if ]
[
dup inline-recursive-label [
call-recursive-inline-word
@ -150,7 +152,7 @@ SYMBOL: enter-out
[ dup infer-inline-word-def ]
if
] if*
] bi ;
] tri ;
M: word apply-object
dup inline? [ inline-word ] [ non-inline-word ] if ;

View File

@ -0,0 +1,96 @@
! (c)2010 Joe Groff bsd license
USING: effects fry io kernel math namespaces sequences
system tools.test
stack-checker.backend
stack-checker.errors
stack-checker.row-polymorphism
stack-checker.values ;
IN: stack-checker.row-polymorphism.tests
[ 3 f ] [ (( a b c -- d )) in-effect-variable ] unit-test
[ 0 f ] [ (( -- d )) in-effect-variable ] unit-test
[ 2 "a" ] [ (( ..a b c -- d )) in-effect-variable ] unit-test
[ (( a ..b c -- d )) in-effect-variable ] [ invalid-effect-variable? ] must-fail-with
[ (( ..a: integer b c -- d )) in-effect-variable ] [ effect-variable-can't-have-type? ] must-fail-with
: checked-each ( ..a seq quot: ( ..a x -- ..a ) -- ..a )
curry call ; inline
: checked-map ( ..a seq quot: ( ..a x -- ..a y ) -- ..a seq' )
curry call f ; inline
: checked-map-index ( ..a seq quot: ( ..a x index -- ..a y ) -- ..a seq' )
0 swap 2curry call f ; inline
: checked-if ( ..a x then: ( ..a -- ..b ) else: ( ..a -- ..b ) -- ..b )
drop nip call ; inline
: checked-if* ( ..a x then: ( ..a x -- ..b ) else: ( ..a -- ..b ) -- ..b )
drop call ; inline
: checked-with-variable ( ..a value key quot: ( ..a -- ..b ) -- ..b )
2nip call ; inline
: infer-polymorphic-quot ( quot -- vars )
t infer-polymorphic? [
unclip-last [
dup current-word set
init-inference
init-known-values
[ [ <literal> <value> [ set-known ] [ push-d ] bi ] each ]
[ stack-effect ] bi*
infer-polymorphic-vars
] with-scope
] with-variable ;
: test-poly-infer ( effect quot -- )
[ '[ _ ] ] [ '[ _ infer-polymorphic-quot ] ] bi* unit-test ; inline
: poly-infer-must-fail ( quot -- )
'[ _ infer-polymorphic-quot ] [ invalid-quotation-input? ] must-fail-with ; inline
H{ { "a" 0 } } [ [ write ] checked-each ] test-poly-infer
H{ { "a" 1 } } [ [ append ] checked-each ] test-poly-infer
H{ { "a" 0 } } [ [ ] checked-map ] test-poly-infer
H{ { "a" 0 } } [ [ reverse ] checked-map ] test-poly-infer
H{ { "a" 1 } } [ [ append dup ] checked-map ] test-poly-infer
H{ { "a" 1 } } [ [ swap nth suffix dup ] checked-map-index ] test-poly-infer
H{ { "a" 3 } { "b" 1 } } [ [ 2drop ] [ 2nip ] checked-if ] test-poly-infer
H{ { "a" 2 } { "b" 3 } } [ [ dup ] [ over ] checked-if ] test-poly-infer
H{ { "a" 0 } { "b" 1 } } [ [ os ] [ cpu ] checked-if ] test-poly-infer
H{ { "a" 1 } { "b" 2 } } [ [ os ] [ 1 + cpu ] checked-if ] test-poly-infer
H{ { "a" 0 } { "b" 0 } } [ [ write ] [ "(f)" write ] checked-if* ] test-poly-infer
H{ { "a" 0 } { "b" 1 } } [ [ ] [ f ] checked-if* ] test-poly-infer
H{ { "a" 1 } { "b" 1 } } [ [ nip ] [ drop f ] checked-if* ] test-poly-infer
H{ { "a" 1 } { "b" 1 } } [ [ nip ] [ ] checked-if* ] test-poly-infer
H{ { "a" 2 } { "b" 2 } } [ [ 3append f ] [ ] checked-if* ] test-poly-infer
H{ { "a" 0 } { "b" 0 } } [ [ drop ] [ ] checked-if* ] test-poly-infer
H{ { "a" 1 } { "b" 0 } } [ [ write ] checked-with-variable ] test-poly-infer
H{ { "a" 0 } { "b" 1 } } [ [ os ] checked-with-variable ] test-poly-infer
H{ { "a" 1 } { "b" 1 } } [ [ dup + ] checked-with-variable ] test-poly-infer
[ [ write write ] checked-each ] poly-infer-must-fail
[ [ ] checked-each ] poly-infer-must-fail
[ [ dup ] checked-map ] poly-infer-must-fail
[ [ drop ] checked-map ] poly-infer-must-fail
[ [ 1 + ] checked-map-index ] poly-infer-must-fail
[ [ dup ] [ ] checked-if ] poly-infer-must-fail
[ [ 2dup ] [ over ] checked-if ] poly-infer-must-fail
[ [ drop ] [ ] checked-if ] poly-infer-must-fail
[ [ ] [ ] checked-if* ] poly-infer-must-fail
[ [ dup ] [ ] checked-if* ] poly-infer-must-fail
[ [ drop ] [ drop ] checked-if* ] poly-infer-must-fail
[ [ ] [ drop ] checked-if* ] poly-infer-must-fail
[ [ ] [ 2dup ] checked-if* ] poly-infer-must-fail
[ "derp" checked-each ] poly-infer-must-fail
[ checked-each ] poly-infer-must-fail
[ "derp" [ "derp" ] checked-if ] poly-infer-must-fail
[ [ "derp" ] "derp" checked-if ] poly-infer-must-fail
[ [ "derp" ] checked-if ] poly-infer-must-fail

View File

@ -0,0 +1,103 @@
! (c)2010 Joe Groff bsd license
USING: accessors arrays assocs combinators combinators.short-circuit
continuations effects fry kernel locals math namespaces
quotations sequences splitting stack-checker
stack-checker.backend
stack-checker.errors
stack-checker.known-words
stack-checker.values ;
IN: stack-checker.row-polymorphism
<PRIVATE
SYMBOL: effect-variables
: quotation-effect? ( in -- ? )
dup pair? [ second effect? ] [ drop f ] if ;
: (effect-variable) ( effect in -- effect variable/f )
dup pair?
[ first ".." head? [ effect-variable-can't-have-type ] [ f ] if ]
[ ".." ?head [ drop f ] unless ] if ;
: validate-effect-variables ( effect ins/outs -- )
[ (effect-variable) ] any? [ invalid-effect-variable ] [ drop ] if ;
: effect-variable ( effect ins/outs -- count variable/f )
[ drop 0 f ] [
unclip
[ [ validate-effect-variables ] [ length ] bi ]
[ (effect-variable) ] bi*
[ 1 + f ] unless*
] if-empty ;
PRIVATE>
: in-effect-variable ( effect -- count variable/f )
dup in>> effect-variable ;
: out-effect-variable ( effect -- count variable/f )
dup out>> effect-variable ;
<PRIVATE
ERROR: abandon-check ;
:: check-variable ( actual-count declared-count variable -- difference )
actual-count declared-count -
variable [
variable effect-variables get at* nip
[ variable effect-variables get at - ]
[ variable effect-variables get set-at 0 ] if
] [
dup [ abandon-check ] unless-zero
] if ;
: adjust-variable ( diff var -- )
over 0 >=
[ effect-variables get at+ ]
[ 2drop ] if ; inline
:: (check-input) ( declared actual -- )
actual in>> length declared in-effect-variable [ check-variable ] keep :> ( in-diff in-var )
actual out>> length declared out-effect-variable [ check-variable ] keep :> ( out-diff out-var )
{ [ in-var not ] [ out-var not ] [ in-diff out-diff = ] } 0||
[
in-var [ in-diff swap adjust-variable ] when*
out-var [ out-diff swap adjust-variable ] when*
] [
abandon-check
] if ;
GENERIC: infer-known ( known -- effect )
M: object infer-known
current-word get bad-macro-input ;
M: literal infer-known
value>> dup callable? [ infer ] [ current-word get bad-macro-input ] if ;
M: composed infer-known
[ quot1>> known infer-known ] [ quot2>> known infer-known ] bi compose-effects ;
M: curried infer-known
(( -- x )) swap quot>> known infer-known compose-effects ;
: check-input ( in value -- )
over quotation-effect? [
[ second ] dip known infer-known (check-input)
] [ 2drop ] if ;
: normalize-variables ( variables -- variables' )
dup values [
infimum dup 0 <
[ '[ _ - ] assoc-map ] [ drop ] if
] unless-empty ;
PRIVATE>
: infer-polymorphic-vars ( effect -- variables )
H{ } clone
[ effect-variables [ in>> dup length ensure-d [ check-input ] 2each ] with-variable ]
keep normalize-variables ;
: check-polymorphic-effect ( word -- )
dup current-word [ stack-effect infer-polymorphic-vars drop ] with-variable ;
SYMBOL: infer-polymorphic?