Inference documentation
slava
parent
1fd34bb360
commit
634e69f711
|
|
@ -3,20 +3,6 @@ namespaces sequences ;
|
|||
|
||||
ARTICLE: "conventions" "Conventions"
|
||||
"Various conventions are used throughout the Factor documentation and source code."
|
||||
{ $heading "Stack effect conventions" }
|
||||
"A stack effect comment lists word inputs and outputs, separated by " { $snippet "--" } ". Stack elements 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:"
|
||||
{ $table
|
||||
{ { { $snippet "?" } } "a boolean" }
|
||||
{ { { $snippet "elt" } } "an object which is an element of a sequence" }
|
||||
{ { { $snippet "m" } ", " { $snippet "n" } } "an integer" }
|
||||
{ { { $snippet "obj" } } "an object" }
|
||||
{ { { $snippet "quot" } } "a quotation" }
|
||||
{ { { $snippet "seq" } } "a sequence" }
|
||||
{ { { $snippet "str" } } "a string" }
|
||||
{ { { $snippet "x" } ", " { $snippet "y" } ", " { $snippet "z" } } "a number" }
|
||||
{ { $snippet "*" } "when this symbol appears by itself in the list of outputs, it means the word unconditionally throws an error" }
|
||||
}
|
||||
"The compiler verifies stack effect comments to ensure the correct number of inputs and outputs is listed. See " { $link "compiler" } "."
|
||||
{ $heading "Word naming conventions" }
|
||||
"These conventions are not hard and fast, but are usually a good first step in understanding a word's behavior:"
|
||||
{ $table
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@ $terpri
|
|||
"10.5"
|
||||
"\"character strings\""
|
||||
"{ 1 2 3 }"
|
||||
"! And by the way, comments look like this"
|
||||
"( Or like this )"
|
||||
"! by the way, this is a comment"
|
||||
"#! and so is this"
|
||||
}
|
||||
{ $references
|
||||
{ "Factor's syntax can be extended, the parser can be called reflectively, and the " { $link . } " word is in fact a general facility for turning almost any object into a form which can be parsed back in again. If this interests you, consult the following sections:" }
|
||||
|
|
@ -52,7 +52,7 @@ $terpri
|
|||
"5 0 - ! Computes 5-0"
|
||||
"5 0 swap - ! Computes 0-5"
|
||||
}
|
||||
"Also, in the above example a stack comment is written between " { $snippet "(" } " and " { $snippet ")" } " with a mnemonic description of what the word does to the stack."
|
||||
"Also, in the above example a stack efect declaration is written between " { $snippet "(" } " and " { $snippet ")" } " with a mnemonic description of what the word does to the stack. See " { $link "effect-declaration" } " for details."
|
||||
{ $curious
|
||||
"This syntax will be familiar to anybody who has used FORTH before. However the behavior is slightly different. In most FORTH systems, the below code prints 2, because the definition of " { $snippet "b" } " still refers to the previous definition of " { $snippet "b" } ":"
|
||||
{ $code
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ ARTICLE: "handbook" "Factor documentation"
|
|||
{ $heading "Survival guide" }
|
||||
{ $list
|
||||
{ "The basic unit of code, corresponding to a \"function\" in other languages, is called a " { $emphasis "word" } " in Factor." }
|
||||
{ "Word take inputs from the stack, and leave output values on the stack. This is documented in a " { $emphasis "stack effect comment" } ", for example " { $snippet "( x y -- z )" } " denotes that a word takes two inputs, with " { $snippet "y" } " at the top of the stack, and returns one output. See " { $link "conventions" } " for details." }
|
||||
{ "Word take inputs from the stack, and leave output values on the stack. This is documented in a " { $emphasis "stack effect declaration" } ", for example " { $snippet "( x y -- z )" } " denotes that a word takes two inputs, with " { $snippet "y" } " at the top of the stack, and returns one output. See " { $link "effect-declaration" } " for details." }
|
||||
{ "You can load source files with " { $link run-file } ":"
|
||||
{ $code "\"examples/lcd.factor\" run-file" } }
|
||||
{ { "You can load " { $snippet "contrib/" } " modules with " { $link require } ":" }
|
||||
|
|
@ -40,6 +40,8 @@ ARTICLE: "handbook" "Factor documentation"
|
|||
{ $subsection "cli" }
|
||||
{ $subsection "tools" }
|
||||
{ $subsection "help" }
|
||||
{ $subsection "inference" }
|
||||
{ $subsection "compiler" }
|
||||
{ $heading "Index" }
|
||||
{ $subsection "article-index" }
|
||||
{ $subsection "primitive-index" }
|
||||
|
|
|
|||
|
|
@ -0,0 +1,100 @@
|
|||
USING: help inference interpreter kernel math sequences ;
|
||||
|
||||
ARTICLE: "effect-declaration" "Stack effect declaration"
|
||||
"It is good practice to declare the stack effects of words using the following syntax:"
|
||||
{ $code ": sq ( x -- y ) dup * ;" }
|
||||
"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:"
|
||||
{ $subsection POSTPONE: ( }
|
||||
"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:"
|
||||
{ $table
|
||||
{ { { $snippet "?" } } "a boolean" }
|
||||
{ { { $snippet "elt" } } "an object which is an element of a sequence" }
|
||||
{ { { $snippet "m" } ", " { $snippet "n" } } "an integer" }
|
||||
{ { { $snippet "obj" } } "an object" }
|
||||
{ { { $snippet "quot" } } "a quotation" }
|
||||
{ { { $snippet "seq" } } "a sequence" }
|
||||
{ { { $snippet "str" } } "a string" }
|
||||
{ { { $snippet "x" } ", " { $snippet "y" } ", " { $snippet "z" } } "a number" }
|
||||
{ { $snippet "*" } "when this symbol appears by itself in the list of outputs, it means the word unconditionally throws an error" }
|
||||
}
|
||||
"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."
|
||||
$terpri
|
||||
"Recursive words must declare a stack effect in order to compile. This includes all generic words, due to how delegation is implemented." ;
|
||||
|
||||
ARTICLE: "inference-simple" "Straight-line stack effects"
|
||||
"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."
|
||||
$terpri
|
||||
"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."
|
||||
{ $subsection d-in }
|
||||
{ $subsection meta-d }
|
||||
"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 } ":"
|
||||
{ $example "[ 1 2 3 ] infer ." "{ 0 3 }" }
|
||||
"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:"
|
||||
{ $example "[ 2 + ] infer ." "{ 1 1 }" }
|
||||
"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)." ;
|
||||
|
||||
ARTICLE: "inference-combinators" "Combinator stack effects"
|
||||
"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."
|
||||
{ $example "[ [ + ] append call ] infer ." "... an error ..." }
|
||||
"On the other hand, applying " { $link call } " to a literal value behaves as if the quotation was substituted at that point:"
|
||||
{ $example "[ [ 2 + ] call ] infer ." "{ 1 1 }" }
|
||||
"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:"
|
||||
{ $example "[ [ 2 + ] keep ] infer ." "{ 1 2 }" }
|
||||
"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."
|
||||
$terpri
|
||||
"Here is an example where the stack effect cannot be inferred:"
|
||||
{ $code ": foo 0 [ + ] ;" "[ foo reduce ] infer ." }
|
||||
"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 } ":"
|
||||
{ $example ": foo 0 [ + ] ; inline" "[ foo reduce ] infer ." "{ 1 1 }" } ;
|
||||
|
||||
ARTICLE: "inference-branches" "Branch stack effects"
|
||||
"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 } "."
|
||||
$terpri
|
||||
"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,"
|
||||
{ $example "[ [ + ] [ drop ] if ] infer ." "{ 3 1 }" }
|
||||
"The call to " { $link if } " takes one value from the stack, a generalized boolean. The first branch " { $snippet "[ + ]" } " has stack effect " { $snippet "{ 2 1 }" } " and the second has stack effect " { $snippet "{ 1 0 }" } ". Since both branches decrease the height of the stack by one, we say that the stack effect of the two branches is " { $snippet "{ 2 1 }" } ", and together with the boolean popped off the stack by " { $link if } ", this gives a total stack effect of " { $snippet "{ 3 1 }" } "." ;
|
||||
|
||||
ARTICLE: "inference-recursive" "Stack effects of recursive words"
|
||||
"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."
|
||||
$terpri
|
||||
"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 } ":"
|
||||
{ $code ": foo ( seq -- ) dup empty? [ drop ] [ dup pop foo ] if" "[ foo ] infer ." }
|
||||
"If you declare an incorrect stack effect, inference will fail also. Badly defined recursive words cannot confuse the inferencer." ;
|
||||
|
||||
ARTICLE: "inference-limitations" "Inference limitations"
|
||||
"Mutually recursive words are supported, but mutually recursive " { $emphasis "inline" } " words are not."
|
||||
$terpri
|
||||
"An inline recursive word cannot pass a quotation through the recursive call. For example, the following will not infer:"
|
||||
{ $code ": foo ( a b c -- d e f ) [ f foo drop ] when 2dup call ; inline" "[ 1 [ 1+ ] foo ] infer ." }
|
||||
"However a small change can be made:"
|
||||
{ $example ": foo ( a b c -- d ) [ 2dup f foo drop ] when call ; inline" "[ 1 [ 1+ ] t foo ] infer ." "{ 0 1 }" }
|
||||
"An inline recursive word must have a fixed stack effect in its base case. The following will not infer:"
|
||||
{ $code
|
||||
": foo ( quot ? -- ) [ f foo ] [ call ] if ; inline"
|
||||
"[ [ 5 ] t foo ] infer ."
|
||||
} ;
|
||||
|
||||
ARTICLE: "inference-custom" "Customizing inference behavior"
|
||||
"The default inference behavior of a word can be changed by storing a quotation in the " { $snippet "\"infer\"" } " word property."
|
||||
$terpri
|
||||
"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."
|
||||
$terpri
|
||||
"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."
|
||||
{ $subsection pop-literal }
|
||||
{ $subsection infer-quot }
|
||||
{ $subsection infer-quot-value } ;
|
||||
|
||||
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. A word Only words for which a stack effect can be inferred will compile."
|
||||
$terpri
|
||||
"The main entry point is a single word taking a quotation as input and returning a stack effect as output:"
|
||||
{ $subsection infer }
|
||||
"The stack effect inference tool can also check stack effect declarations for corectness:"
|
||||
{ $subsection "effect-declaration" }
|
||||
"The following articles describe the implementation of the stack effect inference algorithm:"
|
||||
{ $subsection "inference-simple" }
|
||||
{ $subsection "inference-combinators" }
|
||||
{ $subsection "inference-branches" }
|
||||
{ $subsection "inference-recursive" }
|
||||
{ $subsection "inference-limitations" }
|
||||
{ $subsection "inference-custom" } ;
|
||||
|
|
@ -25,8 +25,11 @@ $terpri
|
|||
"In the overwhelming majority of cases, your interaction with the generic word system centers on two parsing words:"
|
||||
{ $subsection POSTPONE: GENERIC: }
|
||||
{ $subsection POSTPONE: M: }
|
||||
"Generic words must declare their stack effect in order to compile. See " { $link "effect-declaration" } "."
|
||||
$terpri
|
||||
"Since classes are not linearly ordered, method ordering is an issue to keep in mind."
|
||||
{ $subsection "method-order" }
|
||||
"Generic word dispatch can be customized:"
|
||||
{ $subsection "method-combination" } ;
|
||||
|
||||
ARTICLE: "method-order" "Method ordering"
|
||||
|
|
|
|||
|
|
@ -78,9 +78,6 @@ $terpri
|
|||
} ;
|
||||
|
||||
ARTICLE: "syntax-comments" "Comments"
|
||||
"Stack effect comments:"
|
||||
{ $subsection POSTPONE: ( }
|
||||
"End of line comments:"
|
||||
{ $subsection POSTPONE: ! }
|
||||
{ $subsection POSTPONE: #! } ;
|
||||
|
||||
|
|
|
|||
|
|
@ -49,7 +49,8 @@ ARTICLE: "colon-definition" "Compound definitions"
|
|||
{ $subsection POSTPONE: : }
|
||||
{ $subsection define-compound }
|
||||
{ $subsection compound? }
|
||||
{ $subsection compound } ;
|
||||
{ $subsection compound }
|
||||
"Colon definitions should declare their stack effect, unless the definition is completely trivial. See " { $link "effect-declaration" } "." ;
|
||||
|
||||
ARTICLE: "symbols" "Symbols"
|
||||
{ $subsection POSTPONE: SYMBOL: }
|
||||
|
|
|
|||
|
|
@ -325,6 +325,7 @@ sequences vectors words ;
|
|||
"/doc/handbook/handbook.facts"
|
||||
"/doc/handbook/hashtables.facts"
|
||||
"/doc/handbook/help.facts"
|
||||
"/doc/handbook/inference.facts"
|
||||
"/doc/handbook/math.facts"
|
||||
"/doc/handbook/objects.facts"
|
||||
"/doc/handbook/parser.facts"
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ HELP: inference-error
|
|||
{ $list
|
||||
{ $link no-effect }
|
||||
{ $link literal-expected }
|
||||
{ $link check-return }
|
||||
{ $link check-retain }
|
||||
{ $link unbalanced-branches-error }
|
||||
{ $link effect-error }
|
||||
{ $link recursive-declare-error }
|
||||
|
|
@ -28,7 +28,7 @@ HELP: d-in
|
|||
HELP: terminated?
|
||||
{ $var-description "During inference, a flag set to " { $link t } " if the current control flow path unconditionally throws an error." } ;
|
||||
|
||||
HELP: check-return
|
||||
HELP: check-retain
|
||||
{ $error-description "Thrown if inference notices a quotation leaving behind elements on the retain stack." }
|
||||
{ $notes "Usually this error indicates a coding mistake; check that usages of " { $link >r } " and " { $link r> } " are balanced in this case. Writing code which intentionally does this is considered bad style." } ;
|
||||
|
||||
|
|
|
|||
|
|
@ -43,6 +43,6 @@ C: effect
|
|||
] "" make ;
|
||||
|
||||
: stack-effect ( word -- effect/f )
|
||||
dup "infer-effect" word-prop [ ] [
|
||||
dup "declared-effect" word-prop [ ] [ drop f ] ?if
|
||||
dup "declared-effect" word-prop [ ] [
|
||||
dup "infer-effect" word-prop [ ] [ drop f ] ?if
|
||||
] ?if ;
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ HELP: inline
|
|||
{ $description
|
||||
"Declares the most recently defined word as an inline word."
|
||||
$terpri
|
||||
"The compiler copies the definitions of inline words directly into the word being compiled. Combinators must be inlined in order to compile. For any other word, inlining is merely an optimization. Inlining does not affect the execution of the word in the interpreter."
|
||||
"Combinators must be inlined in order to compile - see " { $link "inference-combinators" } ". For any other word, inlining is merely an optimization. Inlining does not affect the execution of the word in the interpreter."
|
||||
} ;
|
||||
|
||||
HELP: foldable
|
||||
|
|
@ -172,20 +172,19 @@ HELP: (
|
|||
{ $syntax "( inputs -- outputs )" }
|
||||
{ $values { "inputs" "a list of tokens" } { "outputs" "a list of tokens" } }
|
||||
{ $description "Declares the stack effect of the most recently defined word, storing a new " { $link effect } " instance in the " { $snippet "\"declared-effect\"" } " word property." }
|
||||
{ $notes "Recursive words must have a declared stack effect to compile. See " { $link "compiler" } " for details." }
|
||||
{ $see-also POSTPONE: ! POSTPONE: #! } ;
|
||||
{ $notes "Recursive words must have a declared stack effect to compile. See " { $link "effect-declaration" } " for details." } ;
|
||||
|
||||
HELP: !
|
||||
{ $syntax "! comment..." }
|
||||
{ $values { "comment" "characters" } }
|
||||
{ $description "Discards all input until the end of the line." }
|
||||
{ $see-also POSTPONE: ( POSTPONE: #! } ;
|
||||
{ $see-also POSTPONE: #! } ;
|
||||
|
||||
HELP: #!
|
||||
{ $syntax "#! comment..." }
|
||||
{ $values { "comment" "characters" } }
|
||||
{ $description "Discards all input until the end of the line." }
|
||||
{ $see-also POSTPONE: ( POSTPONE: ! } ;
|
||||
{ $see-also POSTPONE: ! } ;
|
||||
|
||||
HELP: HEX:
|
||||
{ $syntax "HEX: integer" }
|
||||
|
|
|
|||
|
|
@ -183,7 +183,7 @@ M: unbalanced-branches-error error.
|
|||
M: literal-expected summary
|
||||
drop "Literal value expected" ;
|
||||
|
||||
M: check-return summary
|
||||
M: check-retain summary
|
||||
drop
|
||||
"Quotation leaves elements behind on retain stack" ;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue