steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Reduced stack waste, added LOGIC-RED: and LOGIC-VAR:, a little speed up.

master
kusumotonorio 2020-03-15 10:24:36 +09:00 committed by John Benediktsson
parent ee4e977fbb
commit d8f813a531
5 changed files with 397 additions and 182 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
extra/logic/examples/zebra-short/zebra-short-tests.factor
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.
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 } } }
}
[ { zebrao X } query ] unit-test

2
extra/logic/examples/zebra-short/zebra-short.factor
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.
USING: logic lists ;
IN: logic.examples.zebra-short

86
extra/logic/logic-docs.factor
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." }
{ $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:
{ $description "Creates a new logic predicate for every token until the ;." }
{ $syntax "LOGIC-PREDS: preds... ;" }
@ -121,7 +137,26 @@ HELP: LOGIC-PREDS:
"{ cato Tom } 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:
{ $description "Creates a new logic variable for every token until the ;." }
@ -131,14 +166,15 @@ HELP: LOGIC-VARS:
"USING: logic prettyprint ;"
"IN: scratchpad"
""
"LOGIC-PREDS: mouseo ;"
"LOGIC-PRED: mouseo"
"LOGIC-VARS: X ;"
"SYMBOL: Jerry"
"{ mouseo Jerry } fact"
"{ mouseo X } query ."
"{ H{ { X Jerry } } }"
}
} ;
}
{ $see-also \ LOGIC-VAR: } ;
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." }
@ -192,8 +228,8 @@ HELP: __
""
"SYMBOLS: Tom Jerry Nibbles ;"
"TUPLE: house living dining kitchen in-the-wall ;"
"LOGIC-PREDS: houseo ;"
"LOGIC-VARS: X ;"
"LOGIC-PRED: houseo"
"LOGIC-VAR: X"
""
"{ 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 } "." }
{ $examples
{ $code
"LOGIC-PREDS: N_>_0 ;"
"LOGIC-PRED: N_>_0"
"{ N_>_0 N } [ N of 0 > ] callback"
}
}
@ -271,9 +307,9 @@ HELP: clear-pred
"USING: logic prettyprint ;"
"IN: scratchpad"
""
"LOGIC-PREDS: mouseo ;"
"LOGIC-PRED: mouseo"
"SYMBOLS: Jerry Nibbles ;"
"LOGIC-VARS: X ;"
"LOGIC-VAR: X"
""
"{ mouseo Jerry } fact"
"{ mouseo Nibbles } fact"
@ -352,7 +388,7 @@ HELP: invoke
"USING: logic kernel lists assocs locals math prettyprint ;"
"IN: scratchpad"
""
"LOGIC-PREDS: fibo ;"
"LOGIC-PRED: fibo"
"LOGIC-VARS: F F1 F2 N N1 N2 ;"
""
"{ fibo 1 1 } fact"
@ -392,7 +428,7 @@ HELP: lengtho
"IN: scratchpad"
""
"SYMBOLS: Tom Jerry Nibbles ;"
"LOGIC-VARS: X ;"
"LOGIC-VAR: X"
""
"{ lengtho L{ Tom Jerry Nibbles } 3 } 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 } } }"
}
}
{ $see-also query-n } ;
{ $see-also nquery } ;
HELP: query-n
HELP: nquery
{ $values
{ "goal-def/defs" "a goal def or an array of goal defs" } { "n/f" "the highest number of responses" }
{ "bindings-array/success?" "anser" }
@ -505,7 +541,7 @@ HELP: retract
"USING: logic prettyprint ;"
"IN: scratchpad"
""
"LOGIC-PREDS: mouseo ;"
"LOGIC-PRED: mouseo"
"SYMBOLS: Jerry Nibbles ;"
""
"{ mouseo Jerry } fact"
@ -529,7 +565,7 @@ HELP: retract-all
"USING: logic prettyprint ;"
"IN: scratchpad"
""
"LOGIC-PREDS: mouseo ;"
"LOGIC-PRED: mouseo"
"SYMBOLS: Jerry Nibbles ;"
""
"{ mouseo Jerry } fact"
@ -662,7 +698,7 @@ LOGIC-PREDS: cato mouseo creatureo ;
LOGIC-VARS: X Y ;
SYMBOLS: Tom Jerry Nibbles ;"
} $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
{ $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 ... }" }
@ -728,7 +764,7 @@ SYMBOLS: Tom Jerry Nibbles ;"
} $nl
"To tell the truth, we were able to describe at once that cats and mice were creatures by doing the following." $nl
{ $code
"LOGIC-PREDS: creatureo ;
"LOGIC-PRED: creatureo
{ creatureo Y } {
{ cato Y } ;; { mouseo Y }
@ -743,9 +779,9 @@ $nl
"Gh { Gb6 } rule"
} $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
"{ creatureo Y } 2 query-n ."
"{ creatureo Y } 2 nquery ."
"{ H{ { Y Tom } } H{ { Y Jerry } } }"
} $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
{ $link membero } " is a built-in logic predicate for the relationship an element is in a list." $nl
{ $unchecked-example
"SYMBOL: Spike
"USE: lists
SYMBOL: Spike
{ membero Jerry L{ Tom Jerry Nibbles } } query .
{ membero Spike [ Tom Jerry Nibbles L{ } cons cons cons ] } query ."
"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
{ $code
"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"
} $nl
@ -839,7 +877,7 @@ SYMBOLS: mouse cat milk cheese fresh-milk Emmentaler ;
} $nl
"This is a problematical answer. We have to redefine " { $snippet "consumeso" } "." $nl
{ $code
"LOGIC-PREDS: consumeso ;
"LOGIC-PRED: consumeso
{ consumeso X milk } {
{ is-ao X mouse } ;;
@ -886,7 +924,7 @@ mouseo clear-pred
{ 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 } } }"
} $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
"USE: logic
LOGIC-PREDS: factorialo ;
LOGIC-PRED: factorialo
LOGIC-VARS: N N2 F F2 ;
{ factorialo 0 1 } fact
@ -999,7 +1037,7 @@ LOGIC-VARS: N N2 F F2 ;
{ $code
"USE: logic
LOGIC-PREDS: factorialo ;
LOGIC-PRED: factorialo
LOGIC-VARS: N N2 F F2 ;
{ factorialo 0 1 } fact

2
extra/logic/logic-tests.factor
View File

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

444
extra/logic/logic.factor
View File

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