Fix inference bug erg found a while ago
Slava Pestov
parent
014d2ea31c
commit
1ccab34cfa
|
|
@ -61,7 +61,7 @@ HELP: effect-error
|
|||
{ $description "Throws an " { $link effect-error } "." }
|
||||
{ $error-description "Thrown when a word's inferred stack effect does not match its declared stack effect." } ;
|
||||
|
||||
HELP: recursive-declare-error
|
||||
HELP: no-recursive-declaration
|
||||
{ $error-description "Thrown when inference encounters a recursive call to a word lacking a stack effect declaration. Recursive words must declare a stack effect in order to compile. Due to implementation detail, generic words are recursive, and thus the same restriction applies." } ;
|
||||
|
||||
HELP: recursive-quotation-error
|
||||
|
|
|
|||
|
|
@ -90,8 +90,9 @@ M: object value-literal \ literal-expected inference-warning ;
|
|||
meta-d [ add-inputs ] change d-in [ + ] change ;
|
||||
|
||||
: current-effect ( -- effect )
|
||||
d-in get meta-d get length <effect>
|
||||
terminated? get over set-effect-terminated? ;
|
||||
d-in get
|
||||
meta-d get length <effect>
|
||||
terminated? get >>terminated? ;
|
||||
|
||||
: init-inference ( -- )
|
||||
terminated? off
|
||||
|
|
@ -115,13 +116,13 @@ M: wrapper apply-object
|
|||
terminated? on #terminate node, ;
|
||||
|
||||
: infer-quot ( quot rstate -- )
|
||||
recursive-state get >r
|
||||
recursive-state set
|
||||
[ apply-object terminated? get not ] all? drop
|
||||
r> recursive-state set ;
|
||||
recursive-state get [
|
||||
recursive-state set
|
||||
[ apply-object terminated? get not ] all? drop
|
||||
] dip recursive-state set ;
|
||||
|
||||
: infer-quot-recursive ( quot word label -- )
|
||||
recursive-state get -rot 2array prefix infer-quot ;
|
||||
2array recursive-state get swap prefix infer-quot ;
|
||||
|
||||
: time-bomb ( error -- )
|
||||
[ throw ] curry recursive-state get infer-quot ;
|
||||
|
|
@ -136,9 +137,9 @@ TUPLE: recursive-quotation-error quot ;
|
|||
value-literal recursive-quotation-error inference-error
|
||||
] [
|
||||
dup value-literal callable? [
|
||||
dup value-literal
|
||||
over value-recursion
|
||||
rot f 2array prefix infer-quot
|
||||
[ value-literal ]
|
||||
[ [ value-recursion ] keep f 2array prefix ]
|
||||
bi infer-quot
|
||||
] [
|
||||
drop bad-call
|
||||
] if
|
||||
|
|
@ -191,26 +192,26 @@ TUPLE: too-many-r> ;
|
|||
meta-d get push-all ;
|
||||
|
||||
: if-inline ( word true false -- )
|
||||
>r >r dup inline? r> r> if ; inline
|
||||
[ dup inline? ] 2dip if ; inline
|
||||
|
||||
: consume/produce ( effect node -- )
|
||||
over effect-in over consume-values
|
||||
over effect-out over produce-values
|
||||
node,
|
||||
effect-terminated? [ terminate ] when ;
|
||||
[ [ in>> ] dip consume-values ]
|
||||
[ [ out>> ] dip produce-values ]
|
||||
[ node, terminated?>> [ terminate ] when ]
|
||||
2tri ;
|
||||
|
||||
GENERIC: constructor ( value -- word/f )
|
||||
|
||||
GENERIC: infer-uncurry ( value -- )
|
||||
|
||||
M: curried infer-uncurry
|
||||
drop pop-d dup curried-obj push-d curried-quot push-d ;
|
||||
drop pop-d [ obj>> push-d ] [ quot>> push-d ] bi ;
|
||||
|
||||
M: curried constructor
|
||||
drop \ curry ;
|
||||
|
||||
M: composed infer-uncurry
|
||||
drop pop-d dup composed-quot1 push-d composed-quot2 push-d ;
|
||||
drop pop-d [ quot1>> push-d ] [ quot2>> push-d ] bi ;
|
||||
|
||||
M: composed constructor
|
||||
drop \ compose ;
|
||||
|
|
@ -255,13 +256,13 @@ M: object constructor drop f ;
|
|||
DEFER: unify-values
|
||||
|
||||
: unify-curries ( seq -- value )
|
||||
dup [ curried-obj ] map unify-values
|
||||
swap [ curried-quot ] map unify-values
|
||||
[ [ obj>> ] map unify-values ]
|
||||
[ [ quot>> ] map unify-values ] bi
|
||||
<curried> ;
|
||||
|
||||
: unify-composed ( seq -- value )
|
||||
dup [ composed-quot1 ] map unify-values
|
||||
swap [ composed-quot2 ] map unify-values
|
||||
[ [ quot1>> ] map unify-values ]
|
||||
[ [ quot2>> ] map unify-values ] bi
|
||||
<composed> ;
|
||||
|
||||
TUPLE: cannot-unify-specials ;
|
||||
|
|
@ -292,7 +293,7 @@ TUPLE: unbalanced-branches-error quots in out ;
|
|||
|
||||
: unify-inputs ( max-d-in d-in meta-d -- meta-d )
|
||||
dup [
|
||||
[ >r - r> length + ] keep add-inputs nip
|
||||
[ [ - ] dip length + ] keep add-inputs nip
|
||||
] [
|
||||
2nip
|
||||
] if ;
|
||||
|
|
@ -318,21 +319,24 @@ TUPLE: unbalanced-branches-error quots in out ;
|
|||
[ swap at ] curry map ;
|
||||
|
||||
: datastack-effect ( seq -- )
|
||||
dup quotation branch-variable
|
||||
over d-in branch-variable
|
||||
rot meta-d active-variable
|
||||
unify-effect meta-d set d-in set ;
|
||||
[ quotation branch-variable ]
|
||||
[ d-in branch-variable ]
|
||||
[ meta-d active-variable ] tri
|
||||
unify-effect
|
||||
[ d-in set ] [ meta-d set ] bi* ;
|
||||
|
||||
: retainstack-effect ( seq -- )
|
||||
dup quotation branch-variable
|
||||
over length 0 <repetition>
|
||||
rot meta-r active-variable
|
||||
unify-effect meta-r set drop ;
|
||||
[ quotation branch-variable ]
|
||||
[ length 0 <repetition> ]
|
||||
[ meta-r active-variable ] tri
|
||||
unify-effect
|
||||
[ drop ] [ meta-r set ] bi* ;
|
||||
|
||||
: unify-effects ( seq -- )
|
||||
dup datastack-effect
|
||||
dup retainstack-effect
|
||||
[ terminated? swap at ] all? terminated? set ;
|
||||
[ datastack-effect ]
|
||||
[ retainstack-effect ]
|
||||
[ [ terminated? swap at ] all? terminated? set ]
|
||||
tri ;
|
||||
|
||||
: unify-dataflow ( effects -- nodes )
|
||||
dataflow-graph branch-variable ;
|
||||
|
|
@ -347,14 +351,17 @@ TUPLE: unbalanced-branches-error quots in out ;
|
|||
: infer-branch ( last value -- namespace )
|
||||
[
|
||||
copy-inference
|
||||
dup value-literal quotation set
|
||||
infer-quot-value
|
||||
|
||||
[ value-literal quotation set ]
|
||||
[ infer-quot-value ]
|
||||
bi
|
||||
|
||||
terminated? get [ drop ] [ call node, ] if
|
||||
] H{ } make-assoc ; inline
|
||||
|
||||
: (infer-branches) ( last branches -- list )
|
||||
[ infer-branch ] with map
|
||||
dup unify-effects unify-dataflow ; inline
|
||||
[ unify-effects ] [ unify-dataflow ] bi ; inline
|
||||
|
||||
: infer-branches ( last branches node -- )
|
||||
#! last is a quotation which provides a #return or a #values
|
||||
|
|
@ -390,9 +397,10 @@ TUPLE: effect-error word effect ;
|
|||
|
||||
: finish-word ( word -- )
|
||||
current-effect
|
||||
2dup check-effect
|
||||
over recorded get push
|
||||
"inferred-effect" set-word-prop ;
|
||||
[ check-effect ]
|
||||
[ drop recorded get push ]
|
||||
[ "inferred-effect" set-word-prop ]
|
||||
2tri ;
|
||||
|
||||
: infer-word ( word -- effect )
|
||||
[
|
||||
|
|
@ -408,8 +416,7 @@ TUPLE: effect-error word effect ;
|
|||
|
||||
: custom-infer ( word -- )
|
||||
#! Customized inference behavior
|
||||
dup +inlined+ depends-on
|
||||
"infer" word-prop call ;
|
||||
[ +inlined+ depends-on ] [ "infer" word-prop call ] bi ;
|
||||
|
||||
: cached-infer ( word -- )
|
||||
dup "inferred-effect" word-prop make-call-node ;
|
||||
|
|
@ -422,13 +429,13 @@ TUPLE: effect-error word effect ;
|
|||
[ dup infer-word make-call-node ]
|
||||
} cond ;
|
||||
|
||||
TUPLE: recursive-declare-error word ;
|
||||
TUPLE: no-recursive-declaration word ;
|
||||
|
||||
: declared-infer ( word -- )
|
||||
dup stack-effect [
|
||||
make-call-node
|
||||
] [
|
||||
\ recursive-declare-error inference-error
|
||||
\ no-recursive-declaration inference-error
|
||||
] if* ;
|
||||
|
||||
GENERIC: collect-label-info* ( label node -- )
|
||||
|
|
@ -463,40 +470,56 @@ M: #return collect-label-info*
|
|||
: inline-block ( word -- #label data )
|
||||
[
|
||||
copy-inference nest-node
|
||||
dup word-def swap <inlined-block>
|
||||
[ word-def ] [ <inlined-block> ] bi
|
||||
[ infer-quot-recursive ] 2keep
|
||||
#label unnest-node
|
||||
dup collect-label-info
|
||||
] H{ } make-assoc ;
|
||||
|
||||
: join-values ( #label -- )
|
||||
calls>> [ node-in-d ] map meta-d get suffix
|
||||
calls>> [ in-d>> ] map meta-d get suffix
|
||||
unify-lengths unify-stacks
|
||||
meta-d [ length tail* ] change ;
|
||||
|
||||
: splice-node ( node -- )
|
||||
dup node-successor [
|
||||
dup node, penultimate-node f over set-node-successor
|
||||
dup current-node set
|
||||
] when drop ;
|
||||
dup successor>> [
|
||||
[ node, ] [ penultimate-node ] bi
|
||||
f >>successor
|
||||
current-node set
|
||||
] [ drop ] if ;
|
||||
|
||||
: apply-infer ( hash -- )
|
||||
{ meta-d meta-r d-in terminated? }
|
||||
[ swap [ at ] curry map ] keep
|
||||
[ set ] 2each ;
|
||||
: apply-infer ( data -- )
|
||||
{ meta-d meta-r d-in terminated? } swap extract-keys
|
||||
namespace swap update ;
|
||||
|
||||
: current-stack-height ( -- n )
|
||||
meta-d get length d-in get - ;
|
||||
|
||||
: word-stack-height ( word -- n )
|
||||
stack-effect [ in>> length ] [ out>> length ] bi - ;
|
||||
|
||||
: bad-recursive-declaration ( word inferred -- )
|
||||
dup 0 < [ 0 ] [ 0 swap ] if <effect> effect-error ;
|
||||
|
||||
: check-stack-height ( word height -- )
|
||||
over word-stack-height over =
|
||||
[ 2drop ] [ bad-recursive-declaration ] if ;
|
||||
|
||||
: inline-recursive-word ( word #label -- )
|
||||
current-stack-height [
|
||||
flatten-meta-d [ join-values inline-block apply-infer ] dip >>in-d
|
||||
[ node, ]
|
||||
[ calls>> [ [ flatten-curries ] modify-values ] each ]
|
||||
[ word>> ]
|
||||
tri
|
||||
] dip
|
||||
current-stack-height -
|
||||
check-stack-height ;
|
||||
|
||||
: inline-word ( word -- )
|
||||
dup inline-block over recursive-label? [
|
||||
flatten-meta-d >r
|
||||
drop join-values inline-block apply-infer
|
||||
r> over set-node-in-d
|
||||
dup node,
|
||||
calls>> [
|
||||
[ flatten-curries ] modify-values
|
||||
] each
|
||||
] [
|
||||
apply-infer node-child node-successor splice-node drop
|
||||
] if ;
|
||||
dup inline-block over recursive-label?
|
||||
[ drop inline-recursive-word ]
|
||||
[ apply-infer node-child successor>> splice-node drop ] if ;
|
||||
|
||||
M: word apply-object
|
||||
[
|
||||
|
|
|
|||
|
|
@ -15,10 +15,8 @@ M: inference-error error-help drop f ;
|
|||
|
||||
M: unbalanced-branches-error error.
|
||||
"Unbalanced branches:" print
|
||||
dup unbalanced-branches-error-quots
|
||||
over unbalanced-branches-error-in
|
||||
rot unbalanced-branches-error-out [ length ] map
|
||||
3array flip [ [ bl ] [ pprint ] interleave nl ] each ;
|
||||
[ quots>> ] [ in>> ] [ out>> [ length ] map ] tri 3array flip
|
||||
[ [ bl ] [ pprint ] interleave nl ] each ;
|
||||
|
||||
M: literal-expected summary
|
||||
drop "Literal value expected" ;
|
||||
|
|
@ -32,24 +30,24 @@ M: too-many-r> summary
|
|||
"Quotation pops retain stack elements which it did not push" ;
|
||||
|
||||
M: no-effect error.
|
||||
"Unable to infer stack effect of " write no-effect-word . ;
|
||||
"Unable to infer stack effect of " write word>> . ;
|
||||
|
||||
M: recursive-declare-error error.
|
||||
M: no-recursive-declaration error.
|
||||
"The recursive word " write
|
||||
recursive-declare-error-word pprint
|
||||
word>> pprint
|
||||
" must declare a stack effect" print ;
|
||||
|
||||
M: effect-error error.
|
||||
"Stack effects of the word " write
|
||||
dup effect-error-word pprint
|
||||
dup word>> pprint
|
||||
" do not match." print
|
||||
"Declared: " write
|
||||
dup effect-error-word stack-effect effect>string .
|
||||
"Inferred: " write effect-error-effect effect>string . ;
|
||||
dup word>> stack-effect effect>string .
|
||||
"Inferred: " write effect>> effect>string . ;
|
||||
|
||||
M: recursive-quotation-error error.
|
||||
"The quotation " write
|
||||
recursive-quotation-error-quot pprint
|
||||
quot>> pprint
|
||||
" calls itself." print
|
||||
"Stack effect inference is undecidable when quotation-level recursion is permitted." print ;
|
||||
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ ARTICLE: "inference-errors" "Inference errors"
|
|||
{ $subsection too-many-r> }
|
||||
{ $subsection unbalanced-branches-error }
|
||||
{ $subsection effect-error }
|
||||
{ $subsection recursive-declare-error } ;
|
||||
{ $subsection no-recursive-declaration } ;
|
||||
|
||||
ARTICLE: "inference" "Stack effect inference"
|
||||
"The stack effect inference tool is used to check correctness of code before it is run. It is also used by the compiler to build a dataflow graph on which optimizations can be performed. Only words for which a stack effect can be inferred will compile."
|
||||
|
|
|
|||
Loading…
Reference in New Issue