"Pushing a literal has stack effect " { $snippet "( -- x )" } ". The stack effect of a most words is always known statically from the declaration. Stack effects of " { $link POSTPONE:inline } " words and " { $link "macros" } ", may depend on literals pushed on the stack prior to the call, and this case is discussed in " { $link "inference-combinators" } "."
{ "The combinator must be called with a quotation that is either literal or built from literal quotations, " { $link curry } ", and " { $link compose } ". (Note that quotations that use " { $vocab-link "fry" } " or " { $vocab-link "locals" } " use " { $link curry } " and " { $link compose } " from the perspective of the stack checker.)" }
{ "If the word is declared " { $link POSTPONE:inline } ", the combinator may additionally be called on one of the word's input parameters or with quotations built from the word's input parameters, literal quotations, " { $link curry } ", and " { $link compose } ". When inline, a word is itself considered to be a combinator, and its callers must in turn satisfy these conditions." }
"If neither condition holds, the stack checker throws a " { $link unknown-macro-input } " or " { $link bad-macro-input } " error. To make the code compile, a runtime checking combinator such as " { $link POSTPONE:call( } " must be used instead. See " { $link "inference-escape" } " for details. An inline combinator can be called with an unknown quotation by " { $link curry } "ing the quotation onto a literal quotation that uses " { $link POSTPONE:call( } "."
"The following word calls a quotation twice; the word is declared " { $link POSTPONE:inline } ", since it invokes " { $link call } " on the result of " { $link compose } " on an input parameter:"
{ $code ": twice ( value quot -- result ) dup compose call ; inline" }
"The following code now passes the stack checker; it would fail were " { $snippet "twice" } " not declared " { $link POSTPONE:inline } ":"
"In the next example, " { $link POSTPONE:call( } " must be used because the quotation is the result of calling a runtime accessor, and the compiler cannot make any static assumptions about this quotation at all:"
"However this fails to pass the stack checker since there is no guarantee the quotation has the right stack effect for " { $link map } ". It can be wrapped in a new quotation with a declaration:"
"This restriction exists because without further information, one cannot say what the stack effect of " { $link call } " is; it depends on the given quotation. If the stack checker encounters a " { $link call } " without further information, a " { $link unknown-macro-input } " or " { $link bad-macro-input } " error is raised."
"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."
"The stack checker cannot guarantee that a literal quotation is still literal if it is passed on the data stack to an inlined recursive combinator such as " { $link each } " or " { $link map } ". For example, the following will not infer:"
"Conditionals such as " { $link if } " and combinators built on top have the same restrictions as " { $link POSTPONE:inline } " combinators (see " { $link "inference-combinators" } ") with the additional requirement that all branches leave the stack at the same height. If this is not the case, the stack checker throws a " { $link unbalanced-branches-error } "."
"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,"
"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 )" } ".";
"Most combinators do not call themselves recursively directly; instead, they are implemented in terms of existing combinators, for example " { $link while } ", " { $link map } ", and the " { $link "compositional-combinators" } ". In these cases, the rules outlined in " { $link "inference-combinators" } " apply."
"Combinators which are recursive require additional care. In addition to being declared " { $link POSTPONE:inline } ", they must be declared " { $link POSTPONE:recursive } ". There are three restrictions that only apply to combinators with this declaration:"
{ $heading "Input quotation declaration" }
"Input parameters which are quotations must be annotated as much in the stack effect. For example, the following will not infer:"
"The effect of the nested quotation itself is only present for documentation purposes; the mere presence of a nested effect is sufficient to mark that value as a quotation parameter."
{ $heading "Data flow restrictions" }
"The stack checker does not trace data flow in two instances."
{ $link "inference" } " can be used interactively to print stack effects of quotations without running them. It can also be used from " { $link "combinators.smart" } "."
"In a static checking regime, sometimes it is necessary to step outside the boundaries and run some code which cannot be statically checked; perhaps this code is constructed at run-time. There are two ways to get around the static stack checker."
$nl
"If the stack effect of a word or quotation is known, but the word or quotation itself is not, " { $link POSTPONE:execute( } " or " { $link POSTPONE:call( } " can be used. See " { $link "call" } " for details."
$nl
"If the stack effect is not known, the code being called cannot manipulate the datastack directly. Instead, it must reflect the datastack into an array:"
"The surrounding code has a static stack effect since " { $link with-datastack } " has one. However, the array passed in as input may be transformed arbitrarily by calling this combinator.";
ARTICLE: "inference""Stack effect checking"
"The " { $link "compiler" } " checks the " { $link "effects" } " of words before they can be run. This ensures that words take exactly the number of inputs and outputs that the programmer declares in source."
$nl
"Words that do not pass the stack checker are rejected and cannot be run, and so essentially this defines a very simple and permissive type system that nevertheless catches some invalid programs and enables compiler optimizations."
$nl
"If a word's stack effect cannot be inferred, a compile error is reported. See " { $link "compiler-errors" } "."
{ $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." }
{ $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
HELP:infer.
{ $values { "quot""a quotation" } }
{ $description "Attempts to infer the quotation's stack effect, and prints this data to " { $link output-stream } "." }
{ $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
