core/inference/inference-docs.factor

   1 USING: help.syntax help.markup kernel sequences words io
   2 effects inference.dataflow inference.backend classes
   3 math combinators inference.transforms inference.state ;
   4 IN: inference
   5
   6 ARTICLE: "inference-simple" "Straight-line stack effects"
   7 "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."
   8 $nl
   9 "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."
  10 { $subsection d-in }
  11 { $subsection meta-d }
  12 "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 } ":"
  13 { $example "[ 1 2 3 ] infer." "( -- object object object )" }
  14 "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:"
  15 { $example "[ 2 + ] infer." "( object -- object )" }
  16 "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)." ;
  17
  18 ARTICLE: "inference-combinators" "Combinator stack effects"
  19 "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 } " without further information, a " { $link literal-expected } " error is raised."
  20 { $example "[ dup call ] infer." "... an error ..." }
  21 "On the other hand, the stack effect of applying " { $link call } " to a literal quotation or a " { $link curry } " of a literal quotation is easy to compute; it behaves as if the quotation was substituted at that point:"
  22 { $example "[ [ 2 + ] call ] infer." "( object -- object )" }
  23 "Consider a combinator such as " { $link keep } ". The combinator itself does not have a stack effect, because it applies " { $link call } " to a potentially arbitrary quotation. However, since the combinator is declared " { $link POSTPONE: inline } ", a given usage of it can have a stack effect:"
  24 { $example "[ [ 2 + ] keep ] infer." "( object -- object object )" }
  25 "Another example is the " { $link compose } " combinator. Because it is decared " { $link POSTPONE: inline } ", we can infer the stack effect of applying " { $link call } " to the result of " { $link compose } ":"
  26 { $example "[ 2 [ + ] curry [ sq ] compose ] infer." "( -- object object )" }
  27 "Incidentally, this example demonstrates that the stack effect of nested currying and composition can also be inferred."
  28 $nl
  29 "A general rule of thumb is that any word which applies " { $link call } " or " { $link curry } " to one of its inputs must be declared " { $link POSTPONE: inline } "."
  30 $nl
  31 "Here is an example where the stack effect cannot be inferred:"
  32 { $code ": foo 0 [ + ] ;" "[ foo reduce ] infer." }
  33 "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 } ":"
  34 { $example ": foo 0 [ + ] ; inline" "[ foo reduce ] infer." "( object -- object )" } ;
  35
  36 ARTICLE: "inference-branches" "Branch stack effects"
  37 "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 } "."
  38 $nl
  39 "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,"
  40 { $example "[ [ + ] [ drop ] if ] infer." "( object object object -- object )" }
  41 "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 )" } "." ;
  42
  43 ARTICLE: "inference-recursive" "Stack effects of recursive words"
  44 "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."
  45 $nl
  46 "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 } ":"
  47 { $code ": foo ( seq -- ) dup empty? [ drop ] [ dup pop foo ] if" "[ foo ] infer." }
  48 "If you declare an incorrect stack effect, inference will fail also. Badly defined recursive words cannot confuse the inferencer." ;
  49
  50 ARTICLE: "inference-limitations" "Inference limitations"
  51 "Mutually recursive words are supported, but mutually recursive " { $emphasis "inline" } " words are not."
  52 $nl
  53 "An inline recursive word cannot pass a quotation through the recursive call. For example, the following will not infer:"
  54 { $code ": foo ( a b c -- d e f ) [ f foo drop ] when 2dup call ; inline" "[ 1 [ 1+ ] foo ] infer." }
  55 "However a small change can be made:"
  56 { $example ": foo ( a b c -- d ) [ 2dup f foo drop ] when call ; inline" "[ 1 [ 1+ ] t foo ] infer." "( -- object )" }
  57 "An inline recursive word must have a fixed stack effect in its base case. The following will not infer:"
  58 { $code
  59     ": foo ( quot ? -- ) [ f foo ] [ call ] if ; inline"
  60     "[ [ 5 ] t foo ] infer."
  61 } ;
  62
  63 ARTICLE: "compiler-transforms" "Compiler transforms"
  64 "Compiler transforms can be used to allow words to compile which would otherwise not have a stack effect, and to expand combinators into more efficient code at compile time."
  65 { $subsection define-transform }
  66 "An example is the " { $link cond } " word. If the association list of quotations it is given is literal, the entire form is expanded into a series of nested calls to " { $link if } "."
  67 $nl
  68 "Further customization can be achieved by hooking into the lower-level machinery used by " { $link define-transform } ", the " { $snippet "\"infer\"" } " word property."
  69 $nl
  70 "This property can hold a quotation to be called when the stack effect of a call to this word is being inferred. This quotation can access all internal state of the stack effect inferencer, such as the known literals on the data stack."
  71 { $subsection pop-literal }
  72 { $subsection infer-quot }
  73 { $subsection infer-quot-value }
  74 "The " { $vocab-link "macros" } " vocabulary defines some nice syntax sugar which makes compiler transforms easier to work with." ;
  75
  76 ARTICLE: "dataflow-graphs" "Inspecting the dataflow graph"
  77 "The dataflow graph used by " { $link "compiler" } " can be obtained:"
  78 { $subsection dataflow }
  79 "The " { $vocab-link "optimizer.debugger" } " tool prints the dataflow graph in human readable form."
  80 $nl ;
  81
  82 ARTICLE: "inference-errors" "Inference errors"
  83 "Main wrapper for all inference errors:"
  84 { $subsection inference-error }
  85 "Specific inference errors:"
  86 { $subsection cannot-infer-effect }
  87 { $subsection literal-expected }
  88 { $subsection too-many->r }
  89 { $subsection too-many-r> }
  90 { $subsection unbalanced-branches-error }
  91 { $subsection effect-error }
  92 { $subsection missing-effect } ;
  93
  94 ARTICLE: "inference" "Stack effect inference"
  95 "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."
  96 $nl
  97 "The main entry point is a single word which takes a quotation and prints its stack effect and variable usage:"
  98 { $subsection infer. }
  99 "Instead of printing the inferred information, it can be returned as objects on the stack:"
 100 { $subsection infer }
 101 "Static stack effect inference can be combined with unit tests; see " { $link "tools.test.write" } "."
 102 $nl
 103 "The following articles describe the implementation of the stack effect inference algorithm:"
 104 { $subsection "inference-simple" }
 105 { $subsection "inference-combinators" }
 106 { $subsection "inference-branches" }
 107 { $subsection "inference-recursive" }
 108 { $subsection "inference-limitations" }
 109 { $subsection "inference-errors" }
 110 { $subsection "dataflow-graphs" }
 111 { $subsection "compiler-transforms" }
 112 { $see-also "effects" } ;
 113
 114 ABOUT: "inference"
 115
 116 HELP: inference-error
 117 { $values { "class" class } }
 118 { $description "Creates an instance of " { $snippet "class" } ", wraps it in an " { $link inference-error } " and throws the result." }
 119 { $error-description
 120     "Thrown by " { $link infer } " and " { $link dataflow } " when the stack effect of a quotation cannot be inferred."
 121     $nl
 122     "The " { $snippet "error" } " slot contains one of several possible " { $link "inference-errors" } "."
 123 } ;
 124
 125
 126 HELP: dataflow-graph
 127 { $var-description "In the dynamic extent of " { $link infer } " and " { $link dataflow } ", holds the first node of the dataflow graph being constructed." } ;
 128
 129 HELP: current-node
 130 { $var-description "In the dynamic extent of " { $link infer } " and " { $link dataflow } ", holds the most recently added node of the dataflow graph being constructed." } ;
 131
 132 HELP: infer
 133 { $values { "quot" "a quotation" } { "effect" "an instance of " { $link effect } } }
 134 { $description "Attempts to infer the quotation's stack effect. For interactive testing, the " { $link infer. } " word should be called instead since it presents the output in a nicely formatted manner." }
 135 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 136
 137 HELP: infer.
 138 { $values { "quot" "a quotation" } }
 139 { $description "Attempts to infer the quotation's stack effect, and prints this data to " { $link output-stream } "." }
 140 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 141
 142 { infer infer. } related-words
 143
 144 HELP: dataflow
 145 { $values { "quot" "a quotation" } { "dataflow" "a dataflow node" } }
 146 { $description "Attempts to construct a dataflow graph showing stack flow in the quotation." }
 147 { $notes "This is the first stage of the compiler." }
 148 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 149
 150 HELP: dataflow-with
 151 { $values { "quot" "a quotation" } { "stack" "a vector" } { "dataflow" "a dataflow node" } }
 152 { $description "Attempts to construct a dataflow graph showing stack flow in the quotation, starting with an initial data stack of values." }
 153 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 154
 155 HELP: forget-errors
 156 { $description "Removes markers indicating which words do not have stack effects."
 157 $nl
 158 "The stack effect inference code remembers which words failed to infer as an optimization, so that it does not try to infer the stack effect of words which do not have one over and over again." }
 159 { $notes "Usually this word does not need to be called directly; if a word failed to compile because of a stack effect error, fixing the word definition clears the flag automatically. However, if words failed to compile due to external factors which were subsequently rectified, such as an unavailable C library or a missing or broken compiler transform, this flag can be cleared for all words:"
 160 { $code "forget-errors" }
 161 "Subsequent invocations of the compiler will consider all words for compilation." } ;