Merge remote-tracking branch 'origin/master' into modern-harvey4

modern-harvey4
Doug Coleman 2020-03-15 13:09:22 -05:00
commit dfb3ebf509
9 changed files with 455 additions and 217 deletions

View File

@ -514,7 +514,7 @@ PRIVATE>
: 4seq ( parser1 parser2 parser3 parser4 -- parser ) : 4seq ( parser1 parser2 parser3 parser4 -- parser )
4array seq ; 4array seq ;
: seq* ( quot -- paser ) : seq* ( quot -- parser )
{ } make seq ; inline { } make seq ; inline
: choice ( seq -- parser ) : choice ( seq -- parser )
@ -529,7 +529,7 @@ PRIVATE>
: 4choice ( parser1 parser2 parser3 parser4 -- parser ) : 4choice ( parser1 parser2 parser3 parser4 -- parser )
4array choice ; 4array choice ;
: choice* ( quot -- paser ) : choice* ( quot -- parser )
{ } make choice ; inline { } make choice ; inline
: repeat0 ( parser -- parser ) : repeat0 ( parser -- parser )

View File

@ -493,13 +493,13 @@ update_script_changed() {
invoke_git diff --stat "$(invoke_git merge-base HEAD FETCH_HEAD)" FETCH_HEAD | grep 'build\.sh' >/dev/null invoke_git diff --stat "$(invoke_git merge-base HEAD FETCH_HEAD)" FETCH_HEAD | grep 'build\.sh' >/dev/null
} }
git_fetch_factorcode() { git_fetch() {
$ECHO "Fetching the git repository from github.com..." $ECHO "Fetching the git repository from github.com..."
branch=$(current_git_branch) branch=$(current_git_branch)
rm -f "$(update_script_name)" rm -f "$(update_script_name)"
invoke_git fetch "$GIT_URL" $ECHO git fetch "$GIT_URL" "$branch"
invoke_git fetch "$GIT_URL" --tags invoke_git fetch "$GIT_URL" "$branch"
if update_script_changed; then if update_script_changed; then
$ECHO "Updating and restarting the build.sh script..." $ECHO "Updating and restarting the build.sh script..."
@ -570,7 +570,9 @@ make_clean_factor() {
} }
current_git_branch() { current_git_branch() {
git rev-parse --abbrev-ref HEAD # git rev-parse --abbrev-ref HEAD # outputs HEAD for detached head
# outputs nothing for detached HEAD, which is fine for ``git fetch``
git describe --all --exact-match 2>/dev/null | sed 's=.*/=='
} }
check_url() { check_url() {
@ -680,7 +682,7 @@ install() {
update() { update() {
get_config_info get_config_info
git_fetch_factorcode git_fetch
backup_factor backup_factor
make_clean_factor make_clean_factor
} }
@ -773,7 +775,7 @@ if [[ -n "$2" ]] ; then
fi fi
if [ "$#" -gt 3 ]; then if [ "$#" -gt 3 ]; then
usage usage
$ECHO "error: too many arguments" $ECHO "error: too many arguments"
exit 1 exit 1
fi fi

View File

@ -5,13 +5,22 @@ IN: boyer-moore
HELP: <boyer-moore> HELP: <boyer-moore>
{ $values { $values
{ "pat" sequence } { "bm" boyer-moore } { "pattern" sequence } { "boyer-moore" boyer-moore }
} }
{ $description { $description
"Given a pattern performs pattern preprocessing and returns " "Given a pattern performs pattern preprocessing and returns "
"results as an (opaque) object that is reusable across " "results as an (opaque) object that is reusable across "
"searches in different sequences via " { $link search-from } "searches in different sequences via " { $link search-from } "."
" generic word." } { $examples
{ $example
"USING: boyer-moore prettyprint ;"
"\"abc\" <boyer-moore> ."
"T{ boyer-moore
{ pattern \"abc\" }
{ bad-char-table H{ { 97 0 } { 98 -1 } { 99 -2 } } }
{ good-suffix-table { 3 3 1 } }
}"
}
} ; } ;
HELP: search-from HELP: search-from
@ -21,12 +30,18 @@ HELP: search-from
{ "obj" object } { "obj" object }
{ "i/f" "the index of first match or " { $link f } } { "i/f" "the index of first match or " { $link f } }
} }
{ $description "Performs an attempt to find the first " { $contract "Performs an attempt to find the first "
"occurrence of pattern in " { $snippet "seq" } "occurrence of pattern in " { $snippet "seq" }
" starting from " { $snippet "from" } " using " " starting from " { $snippet "from" } " using "
"Boyer-Moore search algorithm. Output is the index " "Boyer-Moore search algorithm. Output is the index "
"if the attempt was succeessful and " { $link f } "if the attempt was succeessful, or " { $link f }
" otherwise." " otherwise."
} { $examples
{ $example
"USING: boyer-moore prettyprint ;"
"{ 1 2 7 10 20 2 7 10 } 3 { 2 7 10 } search-from ."
"5"
}
} ; } ;
HELP: search HELP: search
@ -37,21 +52,27 @@ HELP: search
} }
{ $description "A simpler variant of " { $link search-from } { $description "A simpler variant of " { $link search-from }
" that starts searching from the beginning of the sequence." " that starts searching from the beginning of the sequence."
} { $examples
{ $example
"USING: boyer-moore prettyprint ;"
"\"Source string\" \"ce st\" search ."
"4"
}
} ; } ;
ARTICLE: "boyer-moore" "The Boyer-Moore algorithm" ARTICLE: "boyer-moore" "The Boyer-Moore algorithm"
{ $heading "Summary" } { $heading "Summary" }
"The " { $vocab-link "boyer-moore" } " vocabulary " "The " { $vocab-link "boyer-moore" } " vocabulary "
"implements a Boyer-Moore string search algorithm with " "implements a Boyer-Moore string search algorithm with the "
"so-called 'strong good suffix shift rule'. Since algorithm is " "so-called 'strong good suffix shift rule'. Since the algorithm is "
"alphabet-independent it is applicable to searching in any " "alphabet-independent, it is applicable to searching in any "
"collection that implements " { $links "sequence-protocol" } "." "collection that implements the " { $links "sequence-protocol" } "."
{ $heading "Complexity" } { $heading "Complexity" }
"Let " { $snippet "n" } " and " { $snippet "m" } " be lengths " "Let " { $snippet "n" } " and " { $snippet "m" } " be the lengths "
"of the sequences being searched " { $emphasis "in" } " and " "of the sequences being searched " { $emphasis "in" } " and "
{ $emphasis "for" } " respectively. Then searching runs in " { $emphasis "for" } " respectively. Then searching runs in "
{ $snippet "O(n)" } " time in its worst case using additional " { $snippet "O(n)" } " time worst-case, using additional "
{ $snippet "O(m)" } " space. The preprocessing phase runs in " { $snippet "O(m)" } " space. The preprocessing phase runs in "
{ $snippet "O(m)" } " time." ; { $snippet "O(m)" } " time." ;

View File

@ -21,26 +21,26 @@ IN: boyer-moore
[ length dup ] [ <reversed> ] bi [ length dup ] [ <reversed> ] bi
[ (partial-suffixes) ] map-index 2nip ; inline [ (partial-suffixes) ] map-index 2nip ; inline
: <gs-table> ( seq -- table ) : <good-suffix-table> ( seq -- table )
z-values [ partial-suffixes ] [ normal-suffixes ] bi z-values [ partial-suffixes ] [ normal-suffixes ] bi
[ [ nip ] when* ] 2map reverse! ; inline [ [ nip ] when* ] 2map reverse! ; inline
: insert-bc-shift ( table elt len i -- table ) : insert-bad-char-shift ( table elt len i -- table )
1 + swap - swap pick 2dup key? 1 + swap - swap pick 2dup key?
[ 3drop ] [ set-at ] if ; inline [ 3drop ] [ set-at ] if ; inline
: <bc-table> ( seq -- table ) : <bad-char-table> ( seq -- table )
H{ } clone swap [ length ] keep H{ } clone swap [ length ] keep
[ insert-bc-shift ] with each-index ; inline [ insert-bad-char-shift ] with each-index ; inline
TUPLE: boyer-moore pattern bc-table gs-table ; TUPLE: boyer-moore pattern bad-char-table good-suffix-table ;
: gs-shift ( i c bm -- s ) nip gs-table>> nth-unsafe ; inline : good-suffix-shift ( i c boyer-moore -- s ) nip good-suffix-table>> nth-unsafe ; inline
: bc-shift ( i c bm -- s ) bc-table>> at dup 1 ? + ; inline : bad-char-shift ( i c boyer-moore -- s ) bad-char-table>> at dup 1 ? + ; inline
: do-shift ( pos i c bm -- newpos ) : do-shift ( pos i c boyer-moore -- newpos )
[ gs-shift ] [ bc-shift ] bi-curry 2bi max + ; inline [ good-suffix-shift ] [ bad-char-shift ] bi-curry 2bi max + ; inline
: match? ( i1 s1 i2 s2 -- ? ) [ nth-unsafe ] 2bi@ = ; inline : match? ( i1 s1 i2 s2 -- ? ) [ nth-unsafe ] 2bi@ = ; inline
@ -48,23 +48,23 @@ TUPLE: boyer-moore pattern bc-table gs-table ;
len 1 - [ [ pos + s1 ] keep s2 match? not ] len 1 - [ [ pos + s1 ] keep s2 match? not ]
find-last-integer ; inline find-last-integer ; inline
:: (search-from) ( seq from bm -- i/f ) :: (search-from) ( seq from boyer-moore -- i/f )
bm pattern>> :> pat boyer-moore pattern>> :> pat
pat length :> plen pat length :> plen
seq length plen - :> lim seq length plen - :> lim
from from
[ [
dup lim <= dup lim <=
[ [
seq pat pick plen mismatch? seq pat pick plen mismatch?
[ 2dup + seq nth-unsafe bm do-shift t ] [ f ] if* [ 2dup + seq nth-unsafe boyer-moore do-shift t ] [ f ] if*
] [ drop f f ] if ] [ drop f f ] if
] loop ; inline ] loop ; inline
PRIVATE> PRIVATE>
: <boyer-moore> ( pat -- bm ) : <boyer-moore> ( pattern -- boyer-moore )
dup <reversed> [ <bc-table> ] [ <gs-table> ] bi dup <reversed> [ <bad-char-table> ] [ <good-suffix-table> ] bi
boyer-moore boa ; boyer-moore boa ;
GENERIC: search-from ( seq from obj -- i/f ) GENERIC: search-from ( seq from obj -- i/f )

View File

@ -1,4 +1,4 @@
! Copyright (C) 2019 Your name. ! Copyright (C) 2019-2020 KUSUMOTO Norio.
! See http://factorcode.org/license.txt for BSD license. ! See http://factorcode.org/license.txt for BSD license.
USING: tools.test logic logic.examples.zebra-short ; USING: tools.test logic logic.examples.zebra-short ;
@ -6,4 +6,3 @@ USING: tools.test logic logic.examples.zebra-short ;
{ H{ { X japanese } } H{ { X japanese } } } { H{ { X japanese } } H{ { X japanese } } }
} }
[ { zebrao X } query ] unit-test [ { zebrao X } query ] unit-test

View File

@ -1,4 +1,4 @@
! Copyright (C) 2019 KUSUMOTO Norio. ! Copyright (C) 2019-2020 KUSUMOTO Norio.
! See http://factorcode.org/license.txt for BSD license. ! See http://factorcode.org/license.txt for BSD license.
USING: logic lists ; USING: logic lists ;
IN: logic.examples.zebra-short IN: logic.examples.zebra-short

View File

@ -107,6 +107,22 @@ HELP: =\=
{ $description "The quotations takes an environment and returns two values. " { $snippet "=\\=" } " returns the internal representation of the goal which returns t if values returned by the quotation are numbers and are not same.\n" { $snippet "=\\=" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." } { $description "The quotations takes an environment and returns two values. " { $snippet "=\\=" } " returns the internal representation of the goal which returns t if values returned by the quotation are numbers and are not same.\n" { $snippet "=\\=" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." }
{ $see-also (==) =:= } ; { $see-also (==) =:= } ;
HELP: LOGIC-PRED:
{ $description "Creates a new logic predicate." }
{ $syntax "LOGIC-PRED: pred" }
{ $examples
{ $code
"USE: logic"
"IN: scratchpad"
""
"LOGIC-PRED: cato"
"SYMBOL: Tom"
""
"{ cato Tom } fact"
}
}
{ $see-also \ LOGIC-PREDS: } ;
HELP: LOGIC-PREDS: HELP: LOGIC-PREDS:
{ $description "Creates a new logic predicate for every token until the ;." } { $description "Creates a new logic predicate for every token until the ;." }
{ $syntax "LOGIC-PREDS: preds... ;" } { $syntax "LOGIC-PREDS: preds... ;" }
@ -121,7 +137,26 @@ HELP: LOGIC-PREDS:
"{ cato Tom } fact" "{ cato Tom } fact"
"{ mouseo Jerry } fact" "{ mouseo Jerry } fact"
} }
} ; }
{ $see-also \ LOGIC-PRED: } ;
HELP: LOGIC-VAR:
{ $description "Creates a new logic variable." }
{ $syntax "LOGIC-VAR: var" }
{ $examples
{ $example
"USING: logic prettyprint ;"
"IN: scratchpad"
""
"LOGIC-PRED: mouseo"
"LOGIC-VAR: X"
"SYMBOL: Jerry"
"{ mouseo Jerry } fact"
"{ mouseo X } query ."
"{ H{ { X Jerry } } }"
}
}
{ $see-also \ LOGIC-VARS: } ;
HELP: LOGIC-VARS: HELP: LOGIC-VARS:
{ $description "Creates a new logic variable for every token until the ;." } { $description "Creates a new logic variable for every token until the ;." }
@ -131,14 +166,15 @@ HELP: LOGIC-VARS:
"USING: logic prettyprint ;" "USING: logic prettyprint ;"
"IN: scratchpad" "IN: scratchpad"
"" ""
"LOGIC-PREDS: mouseo ;" "LOGIC-PRED: mouseo"
"LOGIC-VARS: X ;" "LOGIC-VARS: X ;"
"SYMBOL: Jerry" "SYMBOL: Jerry"
"{ mouseo Jerry } fact" "{ mouseo Jerry } fact"
"{ mouseo X } query ." "{ mouseo X } query ."
"{ H{ { X Jerry } } }" "{ H{ { X Jerry } } }"
} }
} ; }
{ $see-also \ LOGIC-VAR: } ;
HELP: %! HELP: %!
{ $description "A multiline comment. Despite being a Prolog single-line comment, " { $link % } " is already well-known in Factor, so this variant is given instead." } { $description "A multiline comment. Despite being a Prolog single-line comment, " { $link % } " is already well-known in Factor, so this variant is given instead." }
@ -192,8 +228,8 @@ HELP: __
"" ""
"SYMBOLS: Tom Jerry Nibbles ;" "SYMBOLS: Tom Jerry Nibbles ;"
"TUPLE: house living dining kitchen in-the-wall ;" "TUPLE: house living dining kitchen in-the-wall ;"
"LOGIC-PREDS: houseo ;" "LOGIC-PRED: houseo"
"LOGIC-VARS: X ;" "LOGIC-VAR: X"
"" ""
"{ houseo T{ house" "{ houseo T{ house"
@ -240,7 +276,7 @@ HELP: callback
{ $description "Set the quotation to be called. Such quotations take an environment which holds the binding of logic variables, and returns t or " { $link f } " as a result of execution. To retrieve the values of logic variables in the environment, use " { $link of } " or " { $link at } "." } { $description "Set the quotation to be called. Such quotations take an environment which holds the binding of logic variables, and returns t or " { $link f } " as a result of execution. To retrieve the values of logic variables in the environment, use " { $link of } " or " { $link at } "." }
{ $examples { $examples
{ $code { $code
"LOGIC-PREDS: N_>_0 ;" "LOGIC-PRED: N_>_0"
"{ N_>_0 N } [ N of 0 > ] callback" "{ N_>_0 N } [ N of 0 > ] callback"
} }
} }
@ -271,9 +307,9 @@ HELP: clear-pred
"USING: logic prettyprint ;" "USING: logic prettyprint ;"
"IN: scratchpad" "IN: scratchpad"
"" ""
"LOGIC-PREDS: mouseo ;" "LOGIC-PRED: mouseo"
"SYMBOLS: Jerry Nibbles ;" "SYMBOLS: Jerry Nibbles ;"
"LOGIC-VARS: X ;" "LOGIC-VAR: X"
"" ""
"{ mouseo Jerry } fact" "{ mouseo Jerry } fact"
"{ mouseo Nibbles } fact" "{ mouseo Nibbles } fact"
@ -352,7 +388,7 @@ HELP: invoke
"USING: logic kernel lists assocs locals math prettyprint ;" "USING: logic kernel lists assocs locals math prettyprint ;"
"IN: scratchpad" "IN: scratchpad"
"" ""
"LOGIC-PREDS: fibo ;" "LOGIC-PRED: fibo"
"LOGIC-VARS: F F1 F2 N N1 N2 ;" "LOGIC-VARS: F F1 F2 N N1 N2 ;"
"" ""
"{ fibo 1 1 } fact" "{ fibo 1 1 } fact"
@ -392,7 +428,7 @@ HELP: lengtho
"IN: scratchpad" "IN: scratchpad"
"" ""
"SYMBOLS: Tom Jerry Nibbles ;" "SYMBOLS: Tom Jerry Nibbles ;"
"LOGIC-VARS: X ;" "LOGIC-VAR: X"
"" ""
"{ lengtho L{ Tom Jerry Nibbles } 3 } query ." "{ lengtho L{ Tom Jerry Nibbles } 3 } query ."
"{ lengtho L{ Tom Jerry Nibbles } X } query ." "{ lengtho L{ Tom Jerry Nibbles } X } query ."
@ -484,9 +520,9 @@ When you query with logic variable(s), you will get the answer for the logic var
"t\nf\n{ H{ { X Jerry } } H{ { X Nibbles } } }" "t\nf\n{ H{ { X Jerry } } H{ { X Nibbles } } }"
} }
} }
{ $see-also query-n } ; { $see-also nquery } ;
HELP: query-n HELP: nquery
{ $values { $values
{ "goal-def/defs" "a goal def or an array of goal defs" } { "n/f" "the highest number of responses" } { "goal-def/defs" "a goal def or an array of goal defs" } { "n/f" "the highest number of responses" }
{ "bindings-array/success?" "anser" } { "bindings-array/success?" "anser" }
@ -505,7 +541,7 @@ HELP: retract
"USING: logic prettyprint ;" "USING: logic prettyprint ;"
"IN: scratchpad" "IN: scratchpad"
"" ""
"LOGIC-PREDS: mouseo ;" "LOGIC-PRED: mouseo"
"SYMBOLS: Jerry Nibbles ;" "SYMBOLS: Jerry Nibbles ;"
"" ""
"{ mouseo Jerry } fact" "{ mouseo Jerry } fact"
@ -529,7 +565,7 @@ HELP: retract-all
"USING: logic prettyprint ;" "USING: logic prettyprint ;"
"IN: scratchpad" "IN: scratchpad"
"" ""
"LOGIC-PREDS: mouseo ;" "LOGIC-PRED: mouseo"
"SYMBOLS: Jerry Nibbles ;" "SYMBOLS: Jerry Nibbles ;"
"" ""
"{ mouseo Jerry } fact" "{ mouseo Jerry } fact"
@ -662,7 +698,7 @@ LOGIC-PREDS: cato mouseo creatureo ;
LOGIC-VARS: X Y ; LOGIC-VARS: X Y ;
SYMBOLS: Tom Jerry Nibbles ;" SYMBOLS: Tom Jerry Nibbles ;"
} $nl } $nl
"In the DSL, words that represent relationships are called " { $strong "logic predicates" } ". Use " { $link \ LOGIC-PREDS: } " to declare the predicates you want to use. " { $strong "Logic variables" } " are used to represent relationships. use " { $link \ LOGIC-VARS: } " to declare the logic variables you want to use." $nl "In the DSL, words that represent relationships are called " { $strong "logic predicates" } ". Use " { $link \ LOGIC-PRED: } " or " { $link \ LOGIC-PREDS: } " to declare the predicates you want to use. " { $strong "Logic variables" } " are used to represent relationships. use " { $link \ LOGIC-VAR: } " or " { $link \ LOGIC-VARS: } " to declare the logic variables you want to use." $nl
"In the above code, logic predicates end with the character 'o', which is a convention borrowed from miniKanren and so on, and means relation. This is not necessary, but it is useful for reducing conflicts with the words of, the parent language, Factor. We really want to write them as: " { $snippet "cat°" } ", " { $snippet "mouse°" } " and " { $snippet "creature°" } ", but we use 'o' because it's easy to type." $nl "In the above code, logic predicates end with the character 'o', which is a convention borrowed from miniKanren and so on, and means relation. This is not necessary, but it is useful for reducing conflicts with the words of, the parent language, Factor. We really want to write them as: " { $snippet "cat°" } ", " { $snippet "mouse°" } " and " { $snippet "creature°" } ", but we use 'o' because it's easy to type." $nl
{ $strong "Goals" } " are questions that " { $snippet "logic" } " tries to meet to be true. To represent a goal, write an array with a logic predicate followed by zero or more arguments. " { $snippet "logic" } " converts such definitions to internal representations." $nl { $strong "Goals" } " are questions that " { $snippet "logic" } " tries to meet to be true. To represent a goal, write an array with a logic predicate followed by zero or more arguments. " { $snippet "logic" } " converts such definitions to internal representations." $nl
{ $code "{ LOGIC-PREDICATE ARG1 ARG2 ... }" } { $code "{ LOGIC-PREDICATE ARG1 ARG2 ... }" }
@ -728,7 +764,7 @@ SYMBOLS: Tom Jerry Nibbles ;"
} $nl } $nl
"To tell the truth, we were able to describe at once that cats and mice were creatures by doing the following." $nl "To tell the truth, we were able to describe at once that cats and mice were creatures by doing the following." $nl
{ $code { $code
"LOGIC-PREDS: creatureo ; "LOGIC-PRED: creatureo
{ creatureo Y } { { creatureo Y } {
{ cato Y } ;; { mouseo Y } { cato Y } ;; { mouseo Y }
@ -743,9 +779,9 @@ $nl
"Gh { Gb6 } rule" "Gh { Gb6 } rule"
} $nl } $nl
{ $snippet "logic" } " actually converts the disjunction in that way. You may need to be careful about that when deleting definitions that you registered using " { $link rule } ", etc." $nl { $snippet "logic" } " actually converts the disjunction in that way. You may need to be careful about that when deleting definitions that you registered using " { $link rule } ", etc." $nl
"You can use " { $link query-n } " to limit the number of answers to a query. Specify a number greater than or equal to 1." $nl "You can use " { $link nquery } " to limit the number of answers to a query. Specify a number greater than or equal to 1." $nl
{ $unchecked-example { $unchecked-example
"{ creatureo Y } 2 query-n ." "{ creatureo Y } 2 nquery ."
"{ H{ { Y Tom } } H{ { Y Jerry } } }" "{ H{ { Y Tom } } H{ { Y Jerry } } }"
} $nl } $nl
"Use " { $link \+ } " to express " { $strong "negation" } ". " { $link \+ } " acts on the goal immediately following it." $nl "Use " { $link \+ } " to express " { $strong "negation" } ". " { $link \+ } " acts on the goal immediately following it." $nl
@ -776,7 +812,9 @@ $nl
"Such quotations are called only once when converting the goal definitions to internal representations." $nl "Such quotations are called only once when converting the goal definitions to internal representations." $nl
{ $link membero } " is a built-in logic predicate for the relationship an element is in a list." $nl { $link membero } " is a built-in logic predicate for the relationship an element is in a list." $nl
{ $unchecked-example { $unchecked-example
"SYMBOL: Spike "USE: lists
SYMBOL: Spike
{ membero Jerry L{ Tom Jerry Nibbles } } query . { membero Jerry L{ Tom Jerry Nibbles } } query .
{ membero Spike [ Tom Jerry Nibbles L{ } cons cons cons ] } query ." { membero Spike [ Tom Jerry Nibbles L{ } cons cons cons ] } query ."
"t\nf" "t\nf"
@ -784,7 +822,7 @@ $nl
"Recently, they moved into a small house. The house has a living room, a dining room and a kitchen. Well, humans feel that way. Each of them seems to be in their favorite room." $nl "Recently, they moved into a small house. The house has a living room, a dining room and a kitchen. Well, humans feel that way. Each of them seems to be in their favorite room." $nl
{ $code { $code
"TUPLE: house living dining kitchen in-the-wall ; "TUPLE: house living dining kitchen in-the-wall ;
LOGIC-PREDS: houseo ; LOGIC-PRED: houseo
{ houseo T{ house { living Tom } { dining f } { kitchen Nibbles } { in-the-wall Jerry } } } fact" { houseo T{ house { living Tom } { dining f } { kitchen Nibbles } { in-the-wall Jerry } } } fact"
} $nl } $nl
@ -839,7 +877,7 @@ SYMBOLS: mouse cat milk cheese fresh-milk Emmentaler ;
} $nl } $nl
"This is a problematical answer. We have to redefine " { $snippet "consumeso" } "." $nl "This is a problematical answer. We have to redefine " { $snippet "consumeso" } "." $nl
{ $code { $code
"LOGIC-PREDS: consumeso ; "LOGIC-PRED: consumeso
{ consumeso X milk } { { consumeso X milk } {
{ is-ao X mouse } ;; { is-ao X mouse } ;;
@ -886,7 +924,7 @@ mouseo clear-pred
{ mouseo Y } query . { mouseo Y } query .
{ creatureo Y } 2 query-n ." { creatureo Y } 2 nquery ."
"{ H{ { Y Nibbles } } H{ { Y Jerry } } }\n{ H{ { Y Tom } } H{ { Y Nibbles } } }" "{ H{ { Y Nibbles } } H{ { Y Jerry } } }\n{ H{ { Y Tom } } H{ { Y Nibbles } } }"
} $nl } $nl
"While " { $link clear-pred } " clears all the definition information for a given logic predicate, " { $link retract } " and " { $link retract-all } " provide selective clearing." $nl "While " { $link clear-pred } " clears all the definition information for a given logic predicate, " { $link retract } " and " { $link retract-all } " provide selective clearing." $nl
@ -940,7 +978,7 @@ mouseo clear-pred
{ $code { $code
"USE: logic "USE: logic
LOGIC-PREDS: factorialo ; LOGIC-PRED: factorialo
LOGIC-VARS: N N2 F F2 ; LOGIC-VARS: N N2 F F2 ;
{ factorialo 0 1 } fact { factorialo 0 1 } fact
@ -999,7 +1037,7 @@ LOGIC-VARS: N N2 F F2 ;
{ $code { $code
"USE: logic "USE: logic
LOGIC-PREDS: factorialo ; LOGIC-PRED: factorialo
LOGIC-VARS: N N2 F F2 ; LOGIC-VARS: N N2 F F2 ;
{ factorialo 0 1 } fact { factorialo 0 1 } fact

View File

@ -72,7 +72,7 @@ creatureo clear-pred
] unit-test ] unit-test
{ { H{ { Y Tom } } H{ { Y Jerry } } } } [ { { H{ { Y Tom } } H{ { Y Jerry } } } } [
{ creatureo Y } 2 query-n { creatureo Y } 2 nquery
] unit-test ] unit-test
SYMBOL: Spike SYMBOL: Spike

View File

@ -3,10 +3,10 @@
USING: accessors arrays assocs classes classes.tuple combinators USING: accessors arrays assocs classes classes.tuple combinators
combinators.short-circuit compiler.units continuations combinators.short-circuit compiler.units continuations
formatting fry io kernel lexer lists locals make math multiline formatting fry io kernel lexer lists locals make math multiline
namespaces parser prettyprint prettyprint.backend prettyprint.config namespaces parser prettyprint prettyprint.backend
prettyprint.custom prettyprint.sections quotations sequences prettyprint.config prettyprint.custom prettyprint.sections
sequences.deep sets splitting strings words words.symbol quotations sequences sequences.deep sequences.generalizations
vectors ; sets splitting strings vectors words words.symbol ;
IN: logic IN: logic
@ -36,27 +36,31 @@ INSTANCE: ANONYMOUSE-LOGIC-VAR LOGIC-VAR
SYMBOLS: *trace?* *trace-depth* ; SYMBOLS: *trace?* *trace-depth* ;
: define-logic-var ( name -- )
create-word-in
[ reset-generic ]
[ define-symbol ]
[ NORMAL-LOGIC-VAR swap set-global ] tri ;
: define-logic-pred ( name -- )
create-word-in
[ reset-generic ]
[ define-symbol ]
[ [ name>> <pred> ] keep set-global ] tri ;
PRIVATE> PRIVATE>
: trace ( -- ) t *trace?* set-global ; : trace ( -- ) t *trace?* set-global ;
: notrace ( -- ) f *trace?* set-global ; : notrace ( -- ) f *trace?* set-global ;
SYNTAX: LOGIC-VARS: ";" SYNTAX: LOGIC-VAR: scan-token define-logic-var ;
[
create-word-in
[ reset-generic ]
[ define-symbol ]
[ NORMAL-LOGIC-VAR swap set-global ] tri
] each-token ;
SYNTAX: LOGIC-PREDS: ";" SYNTAX: LOGIC-VARS: ";" [ define-logic-var ] each-token ;
[
create-word-in SYNTAX: LOGIC-PRED: scan-token define-logic-pred ;
[ reset-generic ]
[ define-symbol ] SYNTAX: LOGIC-PREDS: ";" [ define-logic-pred ] each-token ;
[ [ name>> <pred> ] keep set-global ] tri
] each-token ;
>> >>
SYNTAX: %! SYNTAX: %!
@ -67,12 +71,12 @@ SYNTAX: %!
TUPLE: logic-goal pred args ; TUPLE: logic-goal pred args ;
: called-args ( args -- args' ) : called-args ( args -- args' )
[ dup callable? [ call( -- term ) ] when ] map ; [ dup callable? [ call( -- term ) ] when ] map ; inline
:: <goal> ( pred args -- goal ) :: <goal> ( pred args -- goal )
pred get args called-args logic-goal boa ; inline pred get args called-args logic-goal boa ; inline
: def>goal ( goal-def -- goal ) unclip swap <goal> ; inline : def>goal ( goal-def -- goal ) unclip swap <goal> ;
: normalize ( goal-def/defs -- goal-defs ) : normalize ( goal-def/defs -- goal-defs )
dup { dup {
@ -93,7 +97,7 @@ TUPLE: logic-env table ;
: env-clear ( env -- ) table>> clear-assoc ; inline : env-clear ( env -- ) table>> clear-assoc ; inline
: dereference ( term env -- term' env' ) : dereference ( term env -- term' env' )
[ 2dup env-get [ 2nip first2 t ] [ f ] if* ] loop ; [ 2dup env-get [ 2nip first2 t ] [ f ] if* ] loop ; inline
PRIVATE> PRIVATE>
@ -107,19 +111,19 @@ M: logic-env at*
{ [ over sequence? ] [ { [ over sequence? ] [
'[ _ at ] map t ] } '[ _ at ] map t ] }
[ drop t ] [ drop t ]
} cond ; } cond ; inline
<PRIVATE <PRIVATE
TUPLE: callback-env env trail ; TUPLE: callback-env env trail ;
C: <callback-env> callback-env C: <callback-env> callback-env inline
M: callback-env at* env>> at* ; M: callback-env at* env>> at* ; inline
TUPLE: cut-info cut? ; TUPLE: cut-info cut? ;
C: <cut> cut-info C: <cut> cut-info inline
: cut? ( cut-info -- ? ) cut?>> ; inline : cut? ( cut-info -- ? ) cut?>> ; inline
@ -128,70 +132,61 @@ C: <cut> cut-info
: set-info-if-f ( ? cut-info -- ) : set-info-if-f ( ? cut-info -- )
dup cut?>> [ 2drop ] [ cut?<< ] if ; inline dup cut?>> [ 2drop ] [ cut?<< ] if ; inline
: 2each-until ( seq1 seq2 quot -- all-failed? ) 2 nfind 2drop f = ; inline
DEFER: unify* DEFER: unify*
:: (unify*) ( x! x-env! y! y-env! trail tmp-env -- success? ) :: (unify*) ( x! x-env! y! y-env! trail tmp-env -- success? )
f :> ret-value! f :> ret?! f :> ret2?! f :> ret-value! f :> ret?! f :> ret2?!
t :> loop?! [
[ loop? ] [ {
{ { [ x logic-var? ] [ { [ x logic-var? ] [
x x-env env-get :> xp! x x-env env-get :> xp
xp not [ xp [
y y-env dereference y-env! y! xp first2 x-env! x!
x y = x-env y-env eq? and [ x x-env dereference x-env! x!
x { y y-env } x-env env-put t
x-env tmp-env eq? [ ] [
{ x x-env } trail push y y-env dereference y-env! y!
] unless x y = x-env y-env eq? and [
] unless x { y y-env } x-env env-put
f loop?! t ret?! t ret-value! x-env tmp-env eq? [
] [ { x x-env } trail push
xp first2 x-env! x! ] unless
x x-env dereference x-env! x! ] unless
] if ] } t ret?! t ret-value!
{ [ y logic-var? ] [ f
x y x! y! x-env y-env x-env! y-env! ] } ] if ] }
[ f loop?! ] { [ y logic-var? ] [
x y x! y! x-env y-env x-env! y-env!
t ] }
[ f ]
} cond } cond
] while ] loop
ret? [ ret? [
t ret-value! t ret-value!
x y [ logic-goal? ] both? [ x y [ logic-goal? ] both? [
x pred>> y pred>> = [ x pred>> y pred>> = [
x args>> x! y args>> y! x args>> x! y args>> y!
] [ ] [
f ret-value! t ret2?! f ret-value! t ret2?!
] if ] if
] when ] when
ret2? [ ret2? [
{ {
{ [ x y [ tuple? ] both? ] [ { [ x y [ tuple? ] both? ] [
x y [ class-of ] same? [ x y [ class-of ] same? [
x y [ tuple-slots ] bi@ :> ( x-slots y-slots ) x y [ tuple-slots ] bi@ [| x-item y-item |
0 :> i! x-slots length 1 - :> stop-i t :> loop?! x-item x-env y-item y-env trail tmp-env unify* not
[ i stop-i <= loop? and ] [ ] 2each-until
x-slots y-slots [ i swap nth ] bi@ ] [ f ] if ret-value! ] }
:> ( x-item y-item )
x-item x-env y-item y-env trail tmp-env unify* [
f loop?!
f ret-value!
] unless
i 1 + i!
] while
] [ f ret-value! ] if ] }
{ [ x y [ sequence? ] both? ] [ { [ x y [ sequence? ] both? ] [
x y [ class-of ] same? x y [ length ] same? and [ x y [ class-of ] same? x y [ length ] same? and [
0 :> i! x length 1 - :> stop-i t :> loop?! x y [| x-item y-item |
[ i stop-i <= loop? and ] [ x-item x-env y-item y-env trail tmp-env unify* not
x y [ i swap nth ] bi@ :> ( x-item y-item ) ] 2each-until
x-item x-env y-item y-env trail tmp-env unify* [ ] [ f ] if ret-value! ] }
f loop?! [ x y = ret-value! ]
f ret-value!
] unless
i 1 + i!
] while
] [ f ret-value! ] if ] }
[ x y = ret-value! ]
} cond } cond
] unless ] unless
] unless ] unless
@ -212,54 +207,159 @@ DEFER: unify*
success? [ "==> Success\n" ] [ "==> Fail\n" ] if "%s\n" printf success? [ "==> Success\n" ] [ "==> Fail\n" ] if "%s\n" printf
*trace-depth* get-global 1 - *trace-depth* set-global *trace-depth* get-global 1 - *trace-depth* set-global
] when ] when
success? ; success? ; inline
: each-until ( seq quot -- ) find 2drop ; inline SYMBOLS:
s-start:
s-not-empty:
s-cut: s-cut/iter:
s-not-cut:
s-defs-loop:
s-callable: s-callable/iter:
s-not-callable: s-not-callable/outer-iter: s-not-callable/inner-iter:
s-unify?-exit:
s-defs-loop-end:
s-end: ;
:: resolve-body ( body env cut quot: ( -- ) -- ) TUPLE: resolver-gen
body empty? [ { state initial: s-start: }
quot call( -- ) body env cut
] [ first-goal rest-goals d-head d-body defs trail d-env d-cut
body unclip :> ( rest-goals! first-goal! ) sub-resolver1 sub-resolver2 i loop-end
first-goal !! = [ ! cut yield? return? ;
rest-goals env cut quot resolve-body
t cut set-info :: <resolver> ( body env cut -- resolver )
] [ resolver-gen new
first-goal callable? [ body >>body env >>env cut >>cut ; inline
first-goal call( -- goal ) first-goal!
] when GENERIC: next ( generator -- yield? )
*trace?* get-global [
first-goal M:: resolver-gen next ( resolver -- yield? )
[ pred>> name>> "in: { %s " printf ] [
[ args>> [ "%u " printf ] each "}\n" printf ] bi f resolver return?<<
] when f resolver yield?<<
<env> :> d-env! resolver state>> {
f <cut> :> d-cut! { s-start: [
first-goal pred>> defs>> [ resolver body>> empty? [
first2 :> ( d-head d-body ) t resolver yield?<<
first-goal d-head [ args>> length ] same? [ s-end: resolver state<<
d-cut cut? cut cut? or [ t ] [ ] [
V{ } clone :> trail s-not-empty: resolver state<<
first-goal env d-head d-env trail d-env unify* [ ] if ] }
d-body callable? [ { s-not-empty: [
d-env trail <callback-env> d-body call( cb-env -- ? ) [ resolver body>> unclip
rest-goals env cut quot resolve-body [ resolver rest-goals<< ] [ resolver first-goal<< ] bi*
] when resolver first-goal>> !! = [ ! cut
] [ s-cut: resolver state<<
d-body d-env d-cut [ ] [
rest-goals env cut quot resolve-body s-not-cut: resolver state<<
cut cut? d-cut set-info-if-f ] if ] }
] resolve-body { s-cut: [
] if resolver [ rest-goals>> ] [ env>> ] [ cut>> ] tri <resolver>
] when resolver sub-resolver1<<
trail [ first2 env-delete ] each s-cut/iter: resolver state<< ] }
d-env env-clear { s-cut/iter: [
f resolver sub-resolver1>> next [
] if t resolver yield?<<
] [ f ] if ] [
] each-until t resolver cut>> set-info
] if s-end: resolver state<<
] if ; ] if ] }
{ s-not-cut: [
resolver first-goal>> callable? [
resolver first-goal>> call( -- goal ) resolver first-goal<<
] when
*trace?* get-global [
resolver first-goal>>
[ pred>> name>> "in: { %s " printf ]
[ args>> [ "%u " printf ] each "}\n" printf ] bi
] when
<env> resolver d-env<<
f <cut> resolver d-cut<<
resolver first-goal>> pred>> defs>> dup resolver defs<<
length 1 - dup 0 >= [
resolver loop-end<<
0 resolver i<<
s-defs-loop: resolver state<<
] [
drop
s-end: resolver state<<
] if ] }
{ s-defs-loop: [
resolver [ i>> ] [ defs>> ] bi nth
first2 [ resolver d-head<< ] [ resolver d-body<< ] bi*
resolver d-cut>> cut? resolver cut>> cut? or [
s-end: resolver state<<
] [
V{ } clone resolver trail<<
resolver {
[ first-goal>> ]
[ env>> ]
[ d-head>> ]
[ d-env>> ]
[ trail>> ]
[ d-env>> ]
} cleave unify* [
resolver d-body>> callable? [
s-callable: resolver state<<
] [
s-not-callable: resolver state<<
] if
] [
s-unify?-exit: resolver state<<
] if
] if ] }
{ s-callable: [
resolver [ d-env>> ] [ trail>> ] bi <callback-env>
resolver d-body>> call( cb-env -- ? ) [
resolver [ rest-goals>> ] [ env>> ] [ cut>> ] tri <resolver>
resolver sub-resolver1<<
s-callable/iter: resolver state<<
] [
s-unify?-exit: resolver state<<
] if ] }
{ s-callable/iter: [
resolver sub-resolver1>> next [
t resolver yield?<<
] [
s-unify?-exit: resolver state<<
] if ] }
{ s-not-callable: [
resolver [ d-body>> ] [ d-env>> ] [ d-cut>> ] tri <resolver>
resolver sub-resolver1<<
s-not-callable/outer-iter: resolver state<< ] }
{ s-not-callable/outer-iter: [
resolver sub-resolver1>> next [
resolver [ rest-goals>> ] [ env>> ] [ cut>> ] tri <resolver>
resolver sub-resolver2<<
s-not-callable/inner-iter: resolver state<<
] [
s-unify?-exit: resolver state<<
] if ] }
{ s-not-callable/inner-iter: [
resolver sub-resolver2>> next [
t resolver yield?<<
] [
resolver cut>> cut? resolver d-cut>> set-info-if-f
s-not-callable/outer-iter: resolver state<<
] if ] }
{ s-unify?-exit: [
resolver trail>> [ first2 env-delete ] each
resolver d-env>> env-clear
s-defs-loop-end: resolver state<< ] }
{ s-defs-loop-end: [
resolver [ i>> ] [ loop-end>> ] bi >= [
s-end: resolver state<<
] [
resolver [ 1 + ] change-i drop
s-defs-loop: resolver state<<
] if ] }
{ s-end: [
t resolver return?<< ] }
} case
resolver [ yield?>> ] [ return?>> ] bi or [ f ] [ t ] if
] loop
resolver yield?>> ;
: split-body ( body -- bodies ) { ;; } split [ >array ] map ; : split-body ( body -- bodies ) { ;; } split [ >array ] map ;
@ -288,30 +388,18 @@ SYMBOL: *anonymouse-var-no*
: collect-logic-vars ( seq -- vars-array ) : collect-logic-vars ( seq -- vars-array )
[ logic-var? ] deep-filter members ; [ logic-var? ] deep-filter members ;
:: (resolve) ( goal-def/defs quot: ( env -- ) -- )
goal-def/defs replace-'__' normalize [ def>goal ] map :> goals
<env> :> env
goals env f <cut> [ env quot call( env -- ) ] resolve-body ;
: resolve ( goal-def/defs quot: ( env -- ) -- ) (resolve) ;
: resolve* ( goal-def/defs -- ) [ drop ] resolve ;
SYMBOL: dummy-item SYMBOL: dummy-item
:: negation-goal ( goal -- negation-goal ) :: negation-goal ( goal -- negation-goal )
"failo_" <pred> :> f-pred "failo_" <pred> :> f-pred
f-pred { } clone logic-goal boa :> f-goal f-pred { } clone logic-goal boa :> f-goal
V{ { f-goal [ drop f ] } } f-pred defs<< V{ { f-goal [ drop f ] } } f-pred defs<<
"trueo_" <pred> :> t-pred
t-pred { } clone logic-goal boa :> t-goal
V{ { t-goal [ drop t ] } } t-pred defs<<
goal pred>> name>> "\\+%s_" sprintf <pred> :> negation-pred goal pred>> name>> "\\+%s_" sprintf <pred> :> negation-pred
negation-pred goal args>> clone logic-goal boa :> negation-goal negation-pred goal args>> clone logic-goal boa :> negation-goal
V{ V{
{ negation-goal { goal !! f-goal } } { negation-goal { goal !! f-goal } } ! \+P_ { P !! { failo_ } } rule
{ negation-goal { t-goal } } { negation-goal { } } ! \+P_ fact
} negation-pred defs<< ! \+P_ { P !! { failo_ } ;; { trueo_ } } rule } negation-pred defs<<
negation-goal ; negation-goal ;
SYMBOLS: at-the-beginning at-the-end ; SYMBOLS: at-the-beginning at-the-end ;
@ -360,17 +448,17 @@ SYMBOLS: at-the-beginning at-the-end ;
PRIVATE> PRIVATE>
: rule ( head body -- ) at-the-end (rule) ; inline : rule ( head body -- ) at-the-end (rule) ;
: rule* ( head body -- ) at-the-beginning (rule) ; inline : rule* ( head body -- ) at-the-beginning (rule) ;
: rules ( defs -- ) [ first2 rule ] each ; inline : rules ( defs -- ) [ first2 rule ] each ;
: fact ( head -- ) at-the-end (fact) ; inline : fact ( head -- ) at-the-end (fact) ;
: fact* ( head -- ) at-the-beginning (fact) ; inline : fact* ( head -- ) at-the-beginning (fact) ;
: facts ( defs -- ) [ fact ] each ; inline : facts ( defs -- ) [ fact ] each ;
:: callback ( head quot: ( callback-env -- ? ) -- ) :: callback ( head quot: ( callback-env -- ? ) -- )
head def>goal :> head-goal head def>goal :> head-goal
@ -459,7 +547,100 @@ PRIVATE>
} invoke*-pred defs<< } invoke*-pred defs<<
invoke*-goal ; invoke*-goal ;
:: query-n ( goal-def/defs n/f -- bindings-array/success? ) :: nquery ( goal-def/defs n/f -- bindings-array/success? )
*trace?* get-global :> trace?
0 :> n!
f :> success?!
V{ } clone :> bindings
<env> :> env
goal-def/defs replace-'__' normalize [ def>goal ] map
env f <cut>
<resolver> :> resolver
[
[
resolver next dup [
resolver env>> table>> keys [ get NORMAL-LOGIC-VAR? ] filter
[ dup env at ] H{ } map>assoc
trace? get-global [ dup [ "%u: %u\n" printf ] assoc-each ] when
bindings push
t success?!
n/f [
n 1 + n!
n n/f >= [ return ] when
] when
] when
] loop
] with-return
bindings dup {
[ empty? ]
[ first keys empty? ]
} 1|| [ drop success? ] [ >array ] if ;
: query ( goal-def/defs -- bindings-array/success? ) f nquery ;
! nquery has been modified to use generators created by finite
! state machines to reduce stack consumption.
! Since the processing algorithm of the code is difficult
! to understand, the words no longer used are kept as private
! words for verification.
<PRIVATE
: each-until ( seq quot -- ) find 2drop ; inline
:: resolve-body ( body env cut quot: ( -- ) -- )
body empty? [
quot call( -- )
] [
body unclip :> ( rest-goals! first-goal! )
first-goal !! = [ ! cut
rest-goals env cut quot resolve-body
t cut set-info
] [
first-goal callable? [
first-goal call( -- goal ) first-goal!
] when
*trace?* get-global [
first-goal
[ pred>> name>> "in: { %s " printf ]
[ args>> [ "%u " printf ] each "}\n" printf ] bi
] when
<env> :> d-env!
f <cut> :> d-cut!
first-goal pred>> defs>> [
first2 :> ( d-head d-body )
first-goal d-head [ args>> length ] same? [
d-cut cut? cut cut? or [ t ] [
V{ } clone :> trail
first-goal env d-head d-env trail d-env unify* [
d-body callable? [
d-env trail <callback-env> d-body call( cb-env -- ? ) [
rest-goals env cut quot resolve-body
] when
] [
d-body d-env d-cut [
rest-goals env cut quot resolve-body
cut cut? d-cut set-info-if-f
] resolve-body
] if
] when
trail [ first2 env-delete ] each
d-env env-clear
f
] if
] [ f ] if
] each-until
] if
] if ;
:: (resolve) ( goal-def/defs quot: ( env -- ) -- )
goal-def/defs replace-'__' normalize [ def>goal ] map :> goals
<env> :> env
goals env f <cut> [ env quot call( env -- ) ] resolve-body ;
: resolve ( goal-def/defs quot: ( env -- ) -- ) (resolve) ;
:: nquery/rec ( goal-def/defs n/f -- bindings-array/success? )
*trace?* get-global :> trace? *trace?* get-global :> trace?
0 :> n! 0 :> n!
f :> success?! f :> success?!
@ -479,11 +660,13 @@ PRIVATE>
] with-return ] with-return
bindings dup { bindings dup {
[ empty? ] [ empty? ]
[ first keys [ get NORMAL-LOGIC-VAR? ] any? not ] [ first keys empty? ]
} 1|| [ drop success? ] [ >array ] if ; } 1|| [ drop success? ] [ >array ] if ;
: query ( goal-def/defs -- bindings-array/success? ) f query-n ; : query/rec ( goal-def/defs -- bindings-array/success? )
f nquery/rec ;
PRIVATE>
! Built-in predicate definitions ----------------------------------------------------- ! Built-in predicate definitions -----------------------------------------------------
@ -492,15 +675,14 @@ LOGIC-PREDS:
varo nonvaro varo nonvaro
(<) (>) (>=) (=<) (==) (\==) (=) (\=) (<) (>) (>=) (=<) (==) (\==) (=) (\=)
writeo writenlo nlo writeo writenlo nlo
membero appendo lengtho listo membero appendo lengtho listo ;
;
{ trueo } [ drop t ] callback { trueo } [ drop t ] callback
{ failo } [ drop f ] callback { failo } [ drop f ] callback
<PRIVATE LOGIC-VARS: A B C X Y Z ; PRIVATE> <PRIVATE LOGIC-VARS: X Y Z ; PRIVATE>
{ varo X } [ X of logic-var? ] callback { varo X } [ X of logic-var? ] callback
@ -554,25 +736,21 @@ LOGIC-PREDS:
{ nlo } [ drop nl t ] callback { nlo } [ drop nl t ] callback
{ membero X L{ X . Z } } fact <PRIVATE LOGIC-VARS: L L1 L2 L3 Head Tail N N1 ; PRIVATE>
{ membero X L{ Y . Z } } { membero X Z } rule
{ appendo L{ } A A } fact { membero X L{ X . Tail } } fact
{ appendo L{ A . X } Y L{ A . Z } } { { membero X L{ Head . Tail } } { membero X Tail } rule
{ appendo X Y Z }
{ appendo L{ } L L } fact
{ appendo L{ X . L1 } L2 L{ X . L3 } } {
{ appendo L1 L2 L3 }
} rule } rule
<PRIVATE LOGIC-VARS: Tail N N1 ; PRIVATE>
{ lengtho L{ } 0 } fact { lengtho L{ } 0 } fact
{ lengtho L{ __ . Tail } N } { { lengtho L{ __ . Tail } N } {
{ lengtho Tail N1 } { lengtho Tail N1 }
[ [ N1 of 1 + ] N is ] [ [ N1 of 1 + ] N is ]
} rule } rule
<PRIVATE LOGIC-VARS: L ; PRIVATE>
{ listo L{ } } fact { listo L{ } } fact
{ listo L{ __ . __ } } fact { listo L{ __ . __ } } fact