core/handbook/inference.facts

   1 USING: help inference interpreter kernel math sequences gadgets ;
   2
   3 ARTICLE: "effect-declaration" "Stack effect declaration"
   4 "It is good practice to declare the stack effects of words using the following syntax:"
   5 { $code ": sq ( x -- y ) dup * ;" }
   6 "A stack effect declaration is written in parentheses and lists word inputs and outputs, separated by " { $snippet "--" } ". Stack effect declarations are read in using a parsing word:"
   7 { $subsection POSTPONE: ( }
   8 "Stack elements in a stack effect are ordered so that the top of the stack is on the right side. Each value can be named by a data type or description. The following are some examples of value names:"
   9 { $table
  10     { { { $snippet "?" } } "a boolean" }
  11     { { { $snippet "elt" } } "an object which is an element of a sequence" }
  12     { { { $snippet "m" } ", " { $snippet "n" } } "an integer" }
  13     { { { $snippet "obj" } } "an object" }
  14     { { { $snippet "quot" } } "a quotation" }
  15     { { { $snippet "seq" } } "a sequence" }
  16     { { { $snippet "str" } } "a string" }
  17     { { { $snippet "x" } ", " { $snippet "y" } ", " { $snippet "z" } } "a number" }
  18     { { $snippet "loc" } "a screen location specified as a two-element array holding x and y co-ordinates" }
  19     { { $snippet "dim" } "a screen dimension specified as a two-element array holding width and height values" }
  20     { { $snippet "rect" } { "a " { $link rect } } }
  21     { { $snippet "*" } "when this symbol appears by itself in the list of outputs, it means the word unconditionally throws an error" }
  22 }
  23 "The stack effect inferencer verifies stack effect comments to ensure the correct number of inputs and outputs is listed. Value names are ignored; only their number matters. If a word's declared stack effect does not match its inferred stack effect, a " { $link effect-error } " is thrown."
  24 $terpri
  25 "Recursive words must declare a stack effect in order to compile. This includes all generic words, due to how delegation is implemented." ;
  26
  27 ARTICLE: "inference-simple" "Straight-line stack effects"
  28 "The simplest case to look at is that of a quotation which does not have any branches or recursion, and just pushes literals and calls words, each of which has a known stack effect."
  29 $terpri
  30 "Stack effect inference works by stepping through the quotation, while maintaining a \"shadow stack\" which tracks stack height at the current position in the quotation. Initially, the shadow stack is empty. If a word is encountered which expects more values than there are on the shadow stack, a global counter is incremented. This counter keeps track of the number of inputs the quotation expects on the stack. When inference is done, this counter, together with the final height of the shadow stack, gives the inferred stack effect."
  31 { $subsection d-in }
  32 { $subsection meta-d }
  33 "When a literal is encountered, it is simply pushed on the shadow stack. For example, the stack effect of the following quotation is inferred by pushing all three literals on the shadow stack, then taking the value of " { $link d-in } " and the length of " { $link meta-d } ":"
  34 { $example "[ 1 2 3 ] infer." "* Stack effect:\n( -- object object object )" }
  35 "In the following example, the call to " { $link + } " expects two values on the shadow stack, but only one value is present, the literal which was pushed previously. This increments the " { $link d-in } " counter by one:"
  36 { $example "[ 2 + ] infer." "* Stack effect:\n( object -- object )" }
  37 "After the call to " { $link + } ", the shadow stack contains a \"computed value placeholder\", since the inferencer has no way to know what the resulting value actually is (in fact it is arbitrary)." ;
  38
  39 ARTICLE: "inference-combinators" "Combinator stack effects"
  40 "Without further information, one cannot say what the stack effect of " { $link call } " is; it depends on the given quotation. If the inferencer encounters a " { $link call } " when the top of the stack is a computed value placeholder, a " { $link literal-expected } " error is raised."
  41 { $example "[ [ + ] append call ] infer." "... an error ..." }
  42 "On the other hand, applying " { $link call } " to a literal value behaves as if the quotation was substituted at that point:"
  43 { $example "[ [ 2 + ] call ] infer." "* Stack effect:\n( object -- object )" }
  44 "Consider a combinator such as " { $link keep } ". The combinator itself does not have a stack effect. However, since the combinator is declared " { $link POSTPONE: inline } ", a given usage of it can have a stack effect:"
  45 { $example "[ [ 2 + ] keep ] infer." "* Stack effect:\n( object -- object object )" }
  46 "In general, combinators must be declared " { $link POSTPONE: inline } " so that we can infer the stack effects of words that call them with literal quotations."
  47 $terpri
  48 "Here is an example where the stack effect cannot be inferred:"
  49 { $code ": foo 0 [ + ] ;" "[ foo reduce ] infer." }
  50 "However if " { $snippet "foo" } " was declared " { $link POSTPONE: inline } ", everything would work, since the " { $link reduce } " combinator is also " { $link POSTPONE: inline } ", and the inferencer can see the literal quotation value at the point it is passed to " { $link call } ":"
  51 { $example ": foo 0 [ + ] ; inline" "[ foo reduce ] infer." "* Stack effect:\n( object -- object )" } ;
  52
  53 ARTICLE: "inference-branches" "Branch stack effects"
  54 "Conditionals such as " { $link if } " and combinators built on " { $link if } " present a problem, in that if the two branches leave the stack at a different height, it is not clear what the stack effect should be. In this case, inference throws a " { $link unbalanced-branches-error } "."
  55 $terpri
  56 "If all branches leave the stack at the same height, then the stack effect of the conditional is just the maximum of the stack effect of each branch. For example,"
  57 { $example "[ [ + ] [ drop ] if ] infer." "* Stack effect:\n( object object object -- object )" }
  58 "The call to " { $link if } " takes one value from the stack, a generalized boolean. The first branch " { $snippet "[ + ]" } " has stack effect " { $snippet "( x x -- x )" } " and the second has stack effect " { $snippet "( x -- )" } ". Since both branches decrease the height of the stack by one, we say that the stack effect of the two branches is " { $snippet "( x x -- x )" } ", and together with the boolean popped off the stack by " { $link if } ", this gives a total stack effect of " { $snippet "( x x x -- x )" } "." ;
  59
  60 ARTICLE: "inference-recursive" "Stack effects of recursive words"
  61 "Recursive words must declare a stack effect. When a recursive call is encountered, the declared stack effect is substituted in. When inference is complete, the inferred stack effect is compared with the declared stack effect."
  62 $terpri
  63 "Attempting to infer the stack effect of a recursive word which outputs a variable number of objects on the stack will fail. For example, the following will throw an " { $link unbalanced-branches-error } ":"
  64 { $code ": foo ( seq -- ) dup empty? [ drop ] [ dup pop foo ] if" "[ foo ] infer." }
  65 "If you declare an incorrect stack effect, inference will fail also. Badly defined recursive words cannot confuse the inferencer." ;
  66
  67 ARTICLE: "inference-limitations" "Inference limitations"
  68 "Mutually recursive words are supported, but mutually recursive " { $emphasis "inline" } " words are not."
  69 $terpri
  70 "An inline recursive word cannot pass a quotation through the recursive call. For example, the following will not infer:"
  71 { $code ": foo ( a b c -- d e f ) [ f foo drop ] when 2dup call ; inline" "[ 1 [ 1+ ] foo ] infer ." }
  72 "However a small change can be made:"
  73 { $example ": foo ( a b c -- d ) [ 2dup f foo drop ] when call ; inline" "[ 1 [ 1+ ] t foo ] infer ." "{ 0 1 }" }
  74 "An inline recursive word must have a fixed stack effect in its base case. The following will not infer:"
  75 { $code
  76     ": foo ( quot ? -- ) [ f foo ] [ call ] if ; inline"
  77     "[ [ 5 ] t foo ] infer."
  78 } ;
  79
  80 ARTICLE: "inference-custom" "Customizing inference behavior"
  81 "The default inference behavior of a word can be changed by storing a quotation in the " { $snippet "\"infer\"" } " word property."
  82 $terpri
  83 "As an example, consider the " { $link cond } " word. It does not have a stack effect, even if it is inlined at a call side where the input quotations are all literal, since it applies " { $link call } " to the result of a sequence operation."
  84 $terpri
  85 "However, calls to " { $link cond } " still compile, because " { $link cond } " defines an " { $snippet "\"infer\"" } " word property which converts the " { $link cond } " form into a series of nested " { $link if } " calls at compile time."
  86 { $subsection pop-literal }
  87 { $subsection infer-quot }
  88 { $subsection infer-quot-value } ;
  89
  90 ARTICLE: "inference" "Stack effect inference"
  91 "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."
  92 $terpri
  93 "The main entry point is a single word which takes a quotation and prints its stack effect and variable usage:"
  94 { $subsection infer. }
  95 "Instead of printing the inferred information, it can be returned as objects on the stack:"
  96 { $subsection infer }
  97 "The dataflow graph used by " { $link "compiler" } " and the " { $link "ui-dataflow" } " can be obtained:"
  98 { $subsection dataflow }
  99 "The stack effect inference tool can also check stack effect declarations for corectness:"
 100 { $subsection "effect-declaration" }
 101 "The following articles describe the implementation of the stack effect inference algorithm:"
 102 { $subsection "inference-simple" }
 103 { $subsection "inference-combinators" }
 104 { $subsection "inference-branches" }
 105 { $subsection "inference-recursive" }
 106 { $subsection "inference-limitations" }
 107 { $subsection "inference-custom" } ;