working on stack effect inference

cvs
Slava Pestov 2004-11-18 01:59:28 +00:00
parent 9c73f061a7
commit d9f823856a
15 changed files with 186 additions and 76 deletions

View File

@ -1,5 +1,6 @@
+ inference/interpreter:
- word links in stepper
- : bin 5 [ 5 bin bin 5 ] [ 2drop ] ifte ;
- combinator inference
- generic/2generic inference

View File

@ -53,9 +53,6 @@ public class Ine extends FactorParsingDefinition
if(w == null)
return;
reader.append(w.vocabulary);
reader.append(w.name);
reader.append(new FactorCompoundDefinition(w,state.first));
reader.append(reader.intern("define",false));
}
}

View File

@ -46,9 +46,6 @@ public class Symbol extends FactorParsingDefinition
throws Exception
{
FactorWord w = reader.nextWord(true);
reader.append(w.vocabulary);
reader.append(w.name);
reader.append(new FactorSymbolDefinition(w,w));
reader.append(reader.intern("define",false));
}
}

View File

@ -79,3 +79,9 @@ USE: stack
2drop
] ifte r>
] each drop ;
: unzip ( assoc -- keys values )
#! Split an association list into two lists of keys and
#! values.
[ ] [ ] rot [ uncons 2swons ] each
swap reverse swap reverse ;

View File

@ -49,3 +49,9 @@ IN: lists USE: kernel USE: stack
: 2cdr ( cons cons -- car car )
swap cdr swap cdr ;
: 2cons ( cdr1 cdr2 car1 car2 -- cons1 cons2 )
rot swons >r cons r> ;
: 2swons ( cdr1 cdr2 car1 car2 -- cons1 cons2 )
rot cons >r swons r> ;

View File

@ -203,6 +203,24 @@ DEFER: tree-contains?
2drop t
] ifte ;
: all=? ( list -- ? )
#! Check if all elements of a list are equal.
dup [ uncons [ over = ] all? nip ] [ drop t ] ifte ;
: maximize ( pred o1 o2 -- o1/o2 )
#! Return o1 if pred returns true, o2 otherwise.
[ rot call ] 2keep ? ;
: (top) ( list maximizer -- elt )
#! Return the highest element in the list, where maximizer
#! has stack effect ( o1 o2 -- max(o1,o2) ).
>r uncons r> each ;
: top ( list pred -- elt )
#! Return the highest element in the list, where pred is a
#! partial order with stack effect ( o1 o2 -- ? ).
swap [ pick >r maximize r> swap ] (top) nip ;
: (count) ( n list -- list )
>r pred dup 0 < [ drop r> ] [ dup r> cons (count) ] ifte ;

View File

@ -33,6 +33,8 @@ USE: stack
USE: vectors
USE: words
DEFER: number=
: (gcd) ( x y -- z ) dup 0 = [ drop ] [ tuck mod (gcd) ] ifte ;
: gcd ( x y -- z ) abs swap abs 2dup < [ swap ] when (gcd) ;
@ -44,7 +46,8 @@ USE: words
[ swap numerator swap numerator ] 2keep
swap denominator swap denominator ;
: ratio= ( a/b c/d -- ? ) 2>fraction = [ = ] [ 2drop f ] ifte ;
: ratio= ( a/b c/d -- ? )
2>fraction number= [ number= ] [ 2drop f ] ifte ;
: ratio-scale ( a/b c/d -- a*d b*c )
2>fraction >r * swap r> * swap ;
: ratio+d ( a/b c/d -- b*d ) denominator swap denominator * ;
@ -64,7 +67,8 @@ USE: words
[ swap real swap real ] 2keep
swap imaginary swap imaginary ;
: complex= ( x y -- ? ) 2>rect = [ = ] [ 2drop f ] ifte ;
: complex= ( x y -- ? )
2>rect number= [ number= ] [ 2drop f ] ifte ;
: complex+ ( x y -- x+y ) 2>rect + >r + r> rect> ;
: complex- ( x y -- x-y ) 2>rect - >r - r> rect> ;

View File

@ -10,9 +10,10 @@ USE: lists
[ 6 ] [ 6 gensym-vector vector-length ] unit-test
[ 3 ] [ [ { 1 2 } { 1 2 3 } ] max-vector-length ] unit-test
[ t ] [
{ 1 2 } { 1 2 3 }
unify-lengths swap vector-length swap vector-length =
[ { 1 2 } { 1 2 3 } ] unify-lengths [ vector-length ] map all=?
] unit-test
[ [ sq ] ] [ [ sq ] [ sq ] unify-result ] unit-test
@ -84,7 +85,31 @@ USE: lists
[ [ bad-recursion-2 ] infer ] unit-test-fails
! Simple combinators
[ [ 1 | 2 ] [ [ car ] keep cdr ] infer ] unit-test
[ [ 1 | 2 ] ] [ [ [ car ] keep cdr ] infer ] unit-test
! Mutual recursion
DEFER: foe
: fie ( element obj -- ? )
dup cons? [ foe ] [ eq? ] ifte ;
: foe ( element tree -- ? )
dup [
2dup car fie [
nip
] [
cdr dup cons? [
foe
] [
fie
] ifte
] ifte
] [
2drop f
] ifte ;
[ [ 2 | 1 ] ] [ [ fie ] infer ] unit-test
[ [ 2 | 1 ] ] [ [ foe ] infer ] unit-test
[ [ 2 | 1 ] ] [ [ 2list ] infer ] unit-test
[ [ 3 | 1 ] ] [ [ 3list ] infer ] unit-test
@ -96,3 +121,6 @@ USE: lists
! [ [ 1 | 1 ] ] [ [ last* ] infer ] unit-test
! [ [ 1 | 1 ] ] [ [ last ] infer ] unit-test
! [ [ 1 | 1 ] ] [ [ list? ] infer ] unit-test
[ [ 2 | 1 ] ] [ [ bitand ] infer ] unit-test
[ [ 2 | 1 ] ] [ [ number= ] infer ] unit-test

View File

@ -45,3 +45,6 @@ USE: test
[ [ [ "one" + ] [ "four" * ] ] ] [
"three" "quot-alist" get remove-assoc
] unit-test
[ [ "one" "three" "four" ] [ [ + ] [ - ] [ * ] ] ]
[ "quot-alist" get unzip ] unit-test

View File

@ -0,0 +1,34 @@
IN: scratchpad
USE: kernel
USE: lists
USE: logic
USE: math
USE: namespaces
USE: stack
USE: test
USE: strings
[ [ [ 3 2 1 ] [ 5 4 3 ] [ 6 ] ] ]
[ [ 1 2 3 ] [ 3 4 5 ] [ 6 ] 3list [ reverse ] map ] unit-test
[ f ] [ [ "Hello" { } 4/3 ] [ string? ] all? ] unit-test
[ t ] [ [ ] [ ] all? ] unit-test
[ t ] [ [ "hi" t 1/2 ] [ ] all? ] unit-test
[ [ 1 2 3 ] ] [ [ 1 4 2 5 3 6 ] [ 4 < ] subset ] unit-test
[ [ 43 "a" [ ] ] ] [ [ "a" 43 43 43 [ ] 43 "a" [ ] ] prune ] unit-test
[ [ 1 2 3 4 5 6 7 ] ] [ [ 6 4 5 7 2 1 3 ] num-sort ] unit-test
[ f ] [ [ { } { } "Hello" ] all=? ] unit-test
[ f ] [ [ { 2 } { } { } ] all=? ] unit-test
[ t ] [ [ ] all=? ] unit-test
[ t ] [ [ 1/2 ] all=? ] unit-test
[ t ] [ [ 1.0 10/10 1 ] all=? ] unit-test
[ 5 ] [ [ 5 ] [ < ] top ] unit-test
[ 5 ] [ [ 5 6 ] [ < ] top ] unit-test
[ 6 ] [ [ 5 6 ] [ > ] top ] unit-test
[ 99 ] [ 100 count [ > ] top ] unit-test
[ 0 ] [ 100 count [ < ] top ] unit-test

View File

@ -25,3 +25,11 @@ USE: test
[ [ 1 2 ] ] [ 1 2 2list ] unit-test
[ [ 1 2 3 ] ] [ 1 2 3 3list ] unit-test
[ [ "car1" | "cdr1" ] [ "car2" | "cdr2" ] ]
[ "car1" "car2" "cdr1" "cdr2" 2cons ]
unit-test
[ [ "car1" | "cdr1" ] [ "car2" | "cdr2" ] ]
[ "cdr1" "cdr2" "car1" "car2" 2swons ]
unit-test

View File

@ -60,9 +60,3 @@ USE: strings
[ [ ] ] [ 0 count ] unit-test
[ [ ] ] [ -10 count ] unit-test
[ [ 0 1 2 3 ] ] [ 4 count ] unit-test
[ [ 1 2 3 ] ] [ [ 1 4 2 5 3 6 ] [ 4 < ] subset ] unit-test
[ [ 43 "a" [ ] ] ] [ [ "a" 43 43 43 [ ] 43 "a" [ ] ] prune ] unit-test
[ [ 1 2 3 4 5 6 7 ] ] [ [ 6 4 5 7 2 1 3 ] num-sort ] unit-test

View File

@ -70,6 +70,7 @@ USE: unparser
"lists/lists"
"lists/assoc"
"lists/namespaces"
"lists/combinators"
"combinators"
"continuations"
"errors"
@ -104,12 +105,12 @@ USE: unparser
"httpd/url-encoding"
"httpd/html"
"httpd/httpd"
"crashes" test
"sbuf" test
"threads" test
"parsing-word" test
"inference" test
"interpreter" test
"crashes"
"sbuf"
"threads"
"parsing-word"
"inference"
"interpreter"
] [
test
] each
@ -127,12 +128,16 @@ USE: unparser
] each
] when
"benchmark/empty-loop" test
"benchmark/fac" test
"benchmark/fib" test
"benchmark/sort" test
"benchmark/continuations" test
"benchmark/ack" test
"benchmark/hashtables" test
"benchmark/strings" test
"benchmark/vectors" test ;
[
"benchmark/empty-loop"
"benchmark/fac"
"benchmark/fib"
"benchmark/sort"
"benchmark/continuations"
"benchmark/ack"
"benchmark/hashtables"
"benchmark/strings"
"benchmark/vectors"
] [
test
] each ;

View File

@ -62,7 +62,8 @@ SYMBOL: recursive-state
>r gensym-vector dup r> vector-append ;
: ensure ( count stack -- count stack )
#! Ensure stack has this many elements.
#! Ensure stack has this many elements. Return number of
#! elements added.
2dup vector-length > [
[ vector-length - dup ] keep inputs
] [
@ -170,7 +171,7 @@ DEFER: (infer)
#! quotations.
[ apply-object ] each ;
: (infer-branch) ( quot -- [ in-d | datastack ] )
: infer-branch ( quot -- [ in-d | datastack ] )
#! Infer the quotation's effect, restoring the meta
#! interpreter state afterwards.
[
@ -178,45 +179,41 @@ DEFER: (infer)
d-in get meta-d get cons
] with-scope ;
: infer-branch ( quot -- [ in-d | datastack ] )
#! Push f if inference failed.
[ (infer-branch) ] [ [ drop f ] when ] catch ;
: difference ( [ in | stack ] -- diff )
#! Stack height difference of infer-branch return value.
uncons vector-length - ;
: balanced? ( [ in | stack ] [ in | stack ] -- ? )
#! Check if two stack effects preserve stack height.
difference swap difference = ;
: balanced? ( list -- ? )
#! Check if a list of [ in | stack ] pairs has the same
#! stack height.
[ difference ] map all=? ;
: max-vector-length ( vector vector -- length )
swap vector-length swap vector-length max ;
: max-vector-length ( list -- length )
[ vector-length ] map [ > ] top ;
: unify-lengths ( stack stack -- stack stack )
#! If one vector is shorter, pad it with unknown results at
#! the bottom.
2dup max-vector-length
tuck swap ensure nip >r swap ensure nip r> ;
: unify-lengths ( list -- list )
#! Pad all vectors to the same length. If one vector is
#! shorter, pad it with unknown results at the bottom.
dup max-vector-length swap [ dupd ensure nip ] map nip ;
: unify-result ( obj obj -- obj )
#! Replace values with unknown result if they differ,
#! otherwise retain them.
2dup = [ drop ] [ 2drop gensym ] ifte ;
: unify-stacks ( stack stack -- stack )
: unify-stacks ( list -- stack )
#! Replace differing literals in stacks with unknown
#! results.
unify-lengths [ unify-result ] vector-2map ;
uncons [ [ unify-result ] vector-2map ] each ;
: unify ( [ in | stack ] [ in | stack ] -- )
: unify ( list -- )
#! Unify meta-interpreter state from two branches.
2dup balanced? [
2dup
2car max d-in set
2cdr unify-stacks meta-d set
dup balanced? [
unzip
unify-lengths unify-stacks meta-d set
[ > ] top d-in set
] [
"Unbalanced ifte branches" throw
"Unbalanced branches" throw
] ifte ;
: set-base ( [ in | stack ] -- )
@ -225,33 +222,38 @@ DEFER: (infer)
uncons vector-length cons r>
recursive-state acons@ ;
: recursive-branches ( false true fe te -- fe te )
#! At least one of the branches did not have a computable
#! stack effect. Set the base case to the other branch, and
#! try again.
2dup or [
dup [
dup set-base >r 2drop infer-branch r>
] [
drop dup set-base swap infer-branch rot drop
] ifte
] [
no-base-case
] ifte ;
: recursive-branch ( quot -- )
#! Set base case if inference didn't fail.
[ infer-branch set-base ] [ [ drop ] when ] catch ;
: infer-branches ( false true -- [ in | stack ] [ in | stack ] )
: infer-branches ( brachlist -- )
#! Recursive stack effect inference is done here. If one of
#! the branches has an undecidable stack effect, we set the
#! base case to this stack effect and try again.
over infer-branch over infer-branch 2dup and [
2nip ( all good )
] [
recursive-branches
] ifte ;
dup [ recursive-branch ] each [ infer-branch ] map unify ;
: infer-ifte ( -- )
#! Infer effects for both branches, unify.
pop-d pop-d pop-d drop ( condition ) infer-branches unify ;
pop-d pop-d 2list pop-d drop ( condition ) infer-branches ;
: vtable>list ( vtable -- list )
#! generic and 2generic use vectors of words, we need lists
#! of quotations. Filter out no-method. Dirty workaround;
#! later properly handle throw.
vector>list [
dup \ no-method = [ drop f ] [ unit ] ifte
] map [ ] subset ;
: infer-generic ( -- )
#! Infer effects for all branches, unify.
pop-d vtable>list peek-d drop ( dispatch ) infer-branches ;
: infer-2generic ( -- )
#! Infer effects for all branches, unify.
pop-d vtable>list
peek-d drop ( dispatch )
peek-d drop ( dispatch )
infer-branches ;
: infer ( quot -- [ in | out ] )
#! Stack effect of a quotation.
@ -260,6 +262,12 @@ DEFER: (infer)
\ call [ pop-d (infer) ] "infer" set-word-property
\ ifte [ infer-ifte ] "infer" set-word-property
\ generic [ infer-generic ] "infer" set-word-property
\ generic [ 2 | 0 ] "infer-effect" set-word-property
\ 2generic [ infer-2generic ] "infer" set-word-property
\ 2generic [ 3 | 0 ] "infer-effect" set-word-property
\ >r [ pop-d push-r ] "infer" set-word-property
\ r> [ pop-r push-d ] "infer" set-word-property

View File

@ -49,6 +49,7 @@ SYMBOL: meta-r
: pop-r meta-r get vector-pop ;
SYMBOL: meta-d
: push-d meta-d get vector-push ;
: peek-d meta-d get vector-peek ;
: pop-d meta-d get vector-pop ;
SYMBOL: meta-n
SYMBOL: meta-c