extra/logic/logic.factor

   1 ! Copyright (C) 2019-2020 KUSUMOTO Norio.
   2 ! See http://factorcode.org/license.txt for BSD license.
   3 USING: accessors arrays assocs classes classes.tuple combinators
   4 combinators.short-circuit compiler.units continuations
   5 formatting io kernel lexer lists math multiline namespaces
   6 parser prettyprint quotations sequences sequences.deep
   7 sequences.generalizations sets splitting strings vectors words
   8 words.symbol ;
   9
  10 IN: logic
  11
  12 SYMBOL: !!    ! cut operator         in prolog: !
  13 SYMBOL: __    ! anonymous variable   in prolog: _
  14 SYMBOL: ;;    ! disjunction, or      in prolog: ;
  15 SYMBOL: \+    ! negation             in prolog: not, \+
  16
  17 <PRIVATE
  18
  19 <<
  20 TUPLE: logic-pred name defs ;
  21
  22 : <pred> ( name -- pred )
  23     logic-pred new
  24         swap >>name
  25         V{ } clone >>defs ;
  26
  27 MIXIN: LOGIC-VAR
  28 SINGLETON: NORMAL-LOGIC-VAR
  29 SINGLETON: ANONYMOUSE-LOGIC-VAR
  30 INSTANCE: NORMAL-LOGIC-VAR LOGIC-VAR
  31 INSTANCE: ANONYMOUSE-LOGIC-VAR LOGIC-VAR
  32
  33 : logic-var? ( obj -- ? )
  34     dup symbol? [ get LOGIC-VAR? ] [ drop f ] if ; inline
  35
  36 SYMBOLS: *trace?* *trace-depth* ;
  37
  38 : define-logic-var ( name -- )
  39     create-word-in
  40     [ reset-generic ]
  41     [ define-symbol ]
  42     [ NORMAL-LOGIC-VAR swap set-global ] tri ;
  43
  44 : define-logic-pred ( name -- )
  45     create-word-in
  46     [ reset-generic ]
  47     [ define-symbol ]
  48     [ [ name>> <pred> ] keep set-global ] tri ;
  49
  50 PRIVATE>
  51
  52 : trace ( -- ) t *trace?* set-global ;
  53
  54 : notrace ( -- ) f *trace?* set-global ;
  55
  56 SYNTAX: LOGIC-VAR: scan-token define-logic-var ;
  57
  58 SYNTAX: LOGIC-VARS: ";" [ define-logic-var ] each-token ;
  59
  60 SYNTAX: LOGIC-PRED: scan-token define-logic-pred ;
  61
  62 SYNTAX: LOGIC-PREDS: ";" [ define-logic-pred ] each-token ;
  63 >>
  64
  65 SYNTAX: %!
  66   "!%" parse-multiline-string drop ;
  67
  68 <PRIVATE
  69
  70 TUPLE: logic-goal pred args ;
  71
  72 : called-args ( args -- args' )
  73     [ dup callable? [ call( -- term ) ] when ] map ; inline
  74
  75 :: <goal> ( pred args -- goal )
  76     pred get args called-args logic-goal boa ; inline
  77
  78 : def>goal ( goal-def -- goal ) unclip swap <goal> ;
  79
  80 : normalize ( goal-def/defs -- goal-defs )
  81     dup {
  82         [ !! = ]
  83         [ ?first dup symbol? [ get logic-pred? ] [ drop f ] if ]
  84     } 1|| [ 1array ] when ;
  85
  86 TUPLE: logic-env table ;
  87
  88 : <env> ( -- env ) logic-env new H{ } clone >>table ; inline
  89
  90 :: env-put ( x pair env -- ) pair x env table>> set-at ; inline
  91
  92 : env-get ( x env -- pair/f ) table>> at ; inline
  93
  94 : env-delete ( x env -- ) table>> delete-at ; inline
  95
  96 : env-clear ( env -- ) table>> clear-assoc ; inline
  97
  98 : dereference ( term env -- term' env' )
  99     [ 2dup env-get [ 2nip first2 t ] [ f ] if* ] loop ; inline
 100
 101 PRIVATE>
 102
 103 M: logic-env at*
 104     dereference {
 105         { [ over logic-goal? ] [
 106             [ [ pred>> ] [ args>> ] bi ] dip at <goal> t ] }
 107         { [ over tuple? ] [
 108             '[ tuple-slots [ _ at ] map ]
 109             [ class-of slots>tuple ] bi t ] }
 110         { [ over sequence? ] [
 111               '[ _ at ] map t ] }
 112         [ drop t ]
 113     } cond ; inline
 114
 115 <PRIVATE
 116
 117 TUPLE: callback-env env trail ;
 118
 119 C: <callback-env> callback-env inline
 120
 121 M: callback-env at* env>> at* ; inline
 122
 123 TUPLE: cut-info cut? ;
 124
 125 C: <cut> cut-info inline
 126
 127 : cut? ( cut-info -- ? ) cut?>> ; inline
 128
 129 : set-info ( ? cut-info -- ) cut?<< ; inline
 130
 131 : set-info-if-f ( ? cut-info -- )
 132     dup cut?>> [ 2drop ] [ cut?<< ] if ; inline
 133
 134 : 2each-until ( seq1 seq2 quot -- all-failed? ) 2 nfind 2drop f = ; inline
 135
 136 DEFER: unify*
 137
 138 :: (unify*) ( x! x-env! y! y-env! trail tmp-env -- success? )
 139     f :> ret-value!  f :> ret?!  f :> ret2?!
 140     [
 141         {
 142             { [ x logic-var? ] [
 143                   x x-env env-get :> xp
 144                   xp [
 145                       xp first2 x-env! x!
 146                       x x-env dereference x-env! x!
 147                       t
 148                   ] [
 149                       y y-env dereference y-env! y!
 150                       x y = x-env y-env eq? and [
 151                           x { y y-env } x-env env-put
 152                           x-env tmp-env eq? [
 153                               { x x-env } trail push
 154                           ] unless
 155                       ] unless
 156                       t ret?!  t ret-value!
 157                       f
 158                   ] if ] }
 159             { [ y logic-var? ] [
 160                   x y x! y!  x-env y-env x-env! y-env!
 161                   t ] }
 162             [ f ]
 163         } cond
 164     ] loop
 165     ret? [
 166         t ret-value!
 167         x y [ logic-goal? ] both? [
 168             x pred>> y pred>> = [
 169                 x args>> x!  y args>> y!
 170             ] [
 171                 f ret-value!  t ret2?!
 172             ] if
 173         ] when
 174         ret2? [
 175             {
 176                 { [ x y [ tuple? ] both? ] [
 177                       x y [ class-of ] same? [
 178                           x y [ tuple-slots ] bi@ [| x-item y-item |
 179                               x-item x-env y-item y-env trail tmp-env unify* not
 180                           ] 2each-until
 181                       ] [ f ] if ret-value! ] }
 182                 { [ x y [ sequence? ] both? ] [
 183                       x y [ class-of ] same? x y [ length ] same? and [
 184                           x y [| x-item y-item |
 185                               x-item x-env y-item y-env trail tmp-env unify* not
 186                           ] 2each-until
 187                       ] [ f ] if ret-value! ] }
 188                 [ x y = ret-value! ]
 189             } cond
 190         ] unless
 191     ] unless
 192     ret-value ;
 193
 194 :: unify* ( x x-env y y-env trail tmp-env -- success? )
 195     *trace?* get-global :> trace?
 196     0 :> depth!
 197     trace? [
 198         *trace-depth* counter depth!
 199         depth [ "\t" printf ] times
 200         "Unification of " printf x-env x of pprint
 201         " and " printf y pprint nl
 202     ] when
 203     x x-env y y-env trail tmp-env (unify*) :> success?
 204     trace? [
 205         depth [ "\t" printf ] times
 206         success? [ "==> Success\n" ] [ "==> Fail\n" ] if "%s\n" printf
 207         *trace-depth* get-global 1 - *trace-depth* set-global
 208     ] when
 209     success? ; inline
 210
 211 SYMBOLS:
 212     s-start:
 213     s-not-empty:
 214     s-cut: s-cut/iter:
 215     s-not-cut:
 216     s-defs-loop:
 217     s-callable: s-callable/iter:
 218     s-not-callable: s-not-callable/outer-iter: s-not-callable/inner-iter:
 219     s-unify?-exit:
 220     s-defs-loop-end:
 221     s-end: ;
 222
 223 TUPLE: resolver-gen
 224     { state initial: s-start: }
 225     body env cut
 226     first-goal rest-goals d-head d-body defs trail d-env d-cut
 227     sub-resolver1 sub-resolver2 i loop-end
 228     yield? return? ;
 229
 230 :: <resolver> ( body env cut -- resolver )
 231     resolver-gen new
 232         body >>body env >>env cut >>cut ; inline
 233
 234 GENERIC: next ( generator -- yield? )
 235
 236 M:: resolver-gen next ( resolver -- yield? )
 237     [
 238         f resolver return?<<
 239         f resolver yield?<<
 240         resolver state>> {
 241             { s-start: [
 242                   resolver body>> empty? [
 243                       t resolver yield?<<
 244                       s-end: resolver state<<
 245                   ] [
 246                       s-not-empty: resolver state<<
 247                   ] if ] }
 248             { s-not-empty: [
 249                   resolver body>> unclip
 250                   [ resolver rest-goals<< ] [ resolver first-goal<< ] bi*
 251                   resolver first-goal>> !! = [  ! cut
 252                       s-cut: resolver state<<
 253                   ] [
 254                       s-not-cut: resolver state<<
 255                   ] if ] }
 256             { s-cut: [
 257                   resolver [ rest-goals>> ] [ env>> ] [ cut>> ] tri <resolver>
 258                   resolver sub-resolver1<<
 259                   s-cut/iter: resolver state<< ] }
 260             { s-cut/iter: [
 261                   resolver sub-resolver1>> next [
 262                       t resolver yield?<<
 263                   ] [
 264                       t resolver cut>> set-info
 265                       s-end: resolver state<<
 266                   ] if ] }
 267             { s-not-cut: [
 268                   resolver first-goal>> callable? [
 269                       resolver first-goal>> call( -- goal ) resolver first-goal<<
 270                   ] when
 271                   *trace?* get-global [
 272                       resolver first-goal>>
 273                       [ pred>> name>> "in: { %s " printf ]
 274                       [ args>> [ "%u " printf ] each "}\n" printf ] bi
 275                   ] when
 276                   <env> resolver d-env<<
 277                   f <cut> resolver d-cut<<
 278                   resolver first-goal>> pred>> defs>> dup resolver defs<<
 279                   length 1 - dup 0 >= [
 280                       resolver loop-end<<
 281                       0 resolver i<<
 282                       s-defs-loop: resolver state<<
 283                   ] [
 284                       drop
 285                       s-end: resolver state<<
 286                   ] if ] }
 287             { s-defs-loop: [
 288                   resolver [ i>> ] [ defs>> ] bi nth
 289                   first2 [ resolver d-head<< ] [ resolver d-body<< ] bi*
 290                   resolver d-cut>> cut? resolver cut>> cut? or [
 291                       s-end: resolver state<<
 292                   ] [
 293                       V{ } clone resolver trail<<
 294                       resolver {
 295                           [ first-goal>> ]
 296                           [ env>> ]
 297                           [ d-head>> ]
 298                           [ d-env>> ]
 299                           [ trail>> ]
 300                           [ d-env>> ]
 301                       } cleave unify* [
 302                           resolver d-body>> callable? [
 303                               s-callable: resolver state<<
 304                           ] [
 305                               s-not-callable: resolver state<<
 306                           ] if
 307                       ] [
 308                           s-unify?-exit: resolver state<<
 309                       ] if
 310                   ] if ] }
 311             { s-callable: [
 312                   resolver [ d-env>> ] [ trail>> ] bi <callback-env>
 313                   resolver d-body>> call( cb-env -- ? ) [
 314                       resolver [ rest-goals>> ] [ env>> ] [ cut>> ] tri <resolver>
 315                       resolver sub-resolver1<<
 316                       s-callable/iter: resolver state<<
 317                   ] [
 318                       s-unify?-exit: resolver state<<
 319                   ] if ] }
 320             { s-callable/iter: [
 321                   resolver sub-resolver1>> next [
 322                       t resolver yield?<<
 323                   ] [
 324                       s-unify?-exit: resolver state<<
 325                   ] if ] }
 326             { s-not-callable: [
 327                   resolver [ d-body>> ] [ d-env>> ] [ d-cut>> ] tri <resolver>
 328                   resolver sub-resolver1<<
 329                   s-not-callable/outer-iter: resolver state<< ] }
 330             { s-not-callable/outer-iter: [
 331                   resolver sub-resolver1>> next [
 332                       resolver [ rest-goals>> ] [ env>> ] [ cut>> ] tri <resolver>
 333                       resolver sub-resolver2<<
 334                       s-not-callable/inner-iter: resolver state<<
 335                   ] [
 336                       s-unify?-exit: resolver state<<
 337                   ] if ] }
 338             { s-not-callable/inner-iter: [
 339                   resolver sub-resolver2>> next [
 340                       t resolver yield?<<
 341                   ] [
 342                       resolver cut>> cut? resolver d-cut>> set-info-if-f
 343                       s-not-callable/outer-iter: resolver state<<
 344                   ] if ] }
 345             { s-unify?-exit: [
 346                   resolver trail>> [ first2 env-delete ] each
 347                   resolver d-env>> env-clear
 348                   s-defs-loop-end: resolver state<< ] }
 349             { s-defs-loop-end: [
 350                   resolver [ i>> ] [ loop-end>> ] bi >= [
 351                       s-end: resolver state<<
 352                   ] [
 353                       resolver [ 1 + ] change-i drop
 354                       s-defs-loop: resolver state<<
 355                   ] if ] }
 356             { s-end: [
 357                   t resolver return?<< ] }
 358         } case
 359         resolver [ yield?>> ] [ return?>> ] bi or not
 360     ] loop
 361     resolver yield?>> ;
 362
 363 : split-body ( body -- bodies ) { ;; } split [ >array ] map ;
 364
 365 SYMBOL: *anonymouse-var-no*
 366
 367 : reset-anonymouse-var-no ( -- ) 0 *anonymouse-var-no* set-global ;
 368
 369 : proxy-var-for-'__' ( -- var-symbol )
 370     [
 371         *anonymouse-var-no* counter "ANON-%d_" sprintf
 372         "logic.private" create-word dup dup
 373         define-symbol
 374         ANONYMOUSE-LOGIC-VAR swap set-global
 375     ] with-compilation-unit ;
 376
 377 : replace-'__' ( before -- after )
 378     {
 379         { [ dup __ = ] [ drop proxy-var-for-'__' ] }
 380         { [ dup sequence? ] [ [ replace-'__' ] map ] }
 381         { [ dup tuple? ] [
 382               [ tuple-slots [ replace-'__' ] map ]
 383               [ class-of slots>tuple ] bi ] }
 384         [ ]
 385     } cond ;
 386
 387 : collect-logic-vars ( seq -- vars-array )
 388     [ logic-var? ] deep-filter members ;
 389
 390 SYMBOL: dummy-item
 391
 392 :: negation-goal ( goal -- negation-goal )
 393     "failo_" <pred> :> f-pred
 394     f-pred { } clone logic-goal boa :> f-goal
 395     V{ { f-goal [ drop f ] } } f-pred defs<<
 396     goal pred>> name>> "\\+%s_" sprintf <pred> :> negation-pred
 397     negation-pred goal args>> clone logic-goal boa :> negation-goal
 398     V{
 399         { negation-goal { goal !! f-goal } } ! \+P_ { P !! { failo_ } } rule
 400         { negation-goal { } }                ! \+P_ fact
 401     } negation-pred defs<<
 402     negation-goal ;
 403
 404 SYMBOLS: at-the-beginning at-the-end ;
 405
 406 :: (rule) ( head body pos -- )
 407     reset-anonymouse-var-no
 408     head replace-'__' def>goal :> head-goal
 409     body replace-'__' normalize
 410     split-body pos at-the-beginning = [ reverse ] when  ! disjunction
 411     dup empty? [
 412         head-goal swap 2array 1vector
 413         head-goal pred>> [
 414             pos at-the-end = [ swap ] when append!
 415         ] change-defs drop
 416     ] [
 417         f :> negation?!
 418         [
 419             [
 420                 {
 421                     { [ dup \+ = ] [ drop dummy-item t negation?! ] }
 422                     { [ dup array? ] [
 423                           def>goal negation? [ negation-goal ] when
 424                           f negation?! ] }
 425                     { [ dup callable? ] [
 426                           call( -- goal ) negation? [ negation-goal ] when
 427                           f negation?! ] }
 428                     { [ dup [ t = ] [ f = ] bi or ] [
 429                           :> t/f! negation? [ t/f not t/f! ] when
 430                           t/f "trueo_" "failo_" ? <pred> :> t/f-pred
 431                           t/f-pred { } clone logic-goal boa :> t/f-goal
 432                           V{ { t/f-goal [ drop t/f ] } } t/f-pred defs<<
 433                           t/f-goal
 434                           f negation?! ] }
 435                     { [ dup !! = ] [ f negation?! ] }  ! as '!!'
 436                     [ drop dummy-item f negation?! ]
 437                 } cond
 438             ] map dummy-item swap remove :> body-goals
 439             V{ { head-goal body-goals } }
 440             head-goal pred>> [
 441                 pos at-the-end = [ swap ] when append!
 442             ] change-defs drop
 443         ] each
 444     ] if ;
 445
 446 : (fact) ( head pos -- ) { } clone swap (rule) ;
 447
 448 PRIVATE>
 449
 450 : rule ( head body -- ) at-the-end (rule) ;
 451
 452 : rule* ( head body -- ) at-the-beginning (rule) ;
 453
 454 : rules ( defs -- ) [ first2 rule ] each ;
 455
 456 : fact ( head -- ) at-the-end (fact) ;
 457
 458 : fact* ( head -- ) at-the-beginning (fact) ;
 459
 460 : facts ( defs -- ) [ fact ] each ;
 461
 462 :: callback ( head quot: ( callback-env -- ? ) -- )
 463     head def>goal :> head-goal
 464     head-goal pred>> [
 465         { head-goal quot } suffix!
 466     ] change-defs drop ;
 467
 468 : callbacks ( defs -- ) [ first2 callback ] each ; inline
 469
 470 :: retract ( head-def -- )
 471     head-def replace-'__' def>goal :> head-goal
 472     head-goal pred>> defs>> :> defs
 473     defs [ first <env> head-goal <env> V{ } clone <env> (unify*) ] find [
 474         head-goal pred>> [ remove-nth! ] change-defs drop
 475     ] [ drop ] if ;
 476
 477 :: retract-all ( head-def -- )
 478     head-def replace-'__' def>goal :> head-goal
 479     head-goal pred>> defs>> :> defs
 480     defs [
 481         first <env> head-goal <env> V{ } clone <env> (unify*)
 482     ] reject! head-goal pred>> defs<< ;
 483
 484 : clear-pred ( pred -- ) get V{ } clone swap defs<< ;
 485
 486 :: unify ( cb-env x y -- success? )
 487     cb-env env>> :> env
 488     x env y env cb-env trail>> env (unify*) ;
 489
 490 :: is ( quot: ( env -- value ) dist -- goal )
 491     quot collect-logic-vars
 492     dup dist swap member? [ dist suffix ] unless :> args
 493     quot dist "[ %u %s is ]" sprintf <pred> :> is-pred
 494     is-pred args logic-goal boa :> is-goal
 495     V{
 496         {
 497             is-goal
 498             [| env | env dist env quot call( env -- value ) unify ]
 499         }
 500     } is-pred defs<<
 501     is-goal ;
 502
 503 :: =:= ( quot: ( env -- n m ) -- goal )
 504     quot collect-logic-vars :> args
 505     quot "[ %u =:= ]" sprintf <pred> :> =:=-pred
 506     =:=-pred args logic-goal boa :> =:=-goal
 507     V{
 508         {
 509             =:=-goal
 510             [| env |
 511                 env quot call( env -- n m )
 512                 2dup [ number? ] both? [ = ] [ 2drop f ] if ]
 513         }
 514     } =:=-pred defs<<
 515     =:=-goal ;
 516
 517 :: =\= ( quot: ( env -- n m ) -- goal )
 518     quot collect-logic-vars :> args
 519     quot "[ %u =\\= ]" sprintf <pred> :> =\=-pred
 520     =\=-pred args logic-goal boa :> =\=-goal
 521     V{
 522         {
 523             =\=-goal
 524             [| env |
 525                 env quot call( env -- n m )
 526                 2dup [ number? ] both? [ = not ] [ 2drop f ] if ]
 527         }
 528     } =\=-pred defs<<
 529     =\=-goal ;
 530
 531 :: invoke ( quot: ( env -- ) -- goal )
 532     quot collect-logic-vars :> args
 533     quot "[ %u invoke ]" sprintf <pred> :> invoke-pred
 534     invoke-pred args logic-goal boa :> invoke-goal
 535     V{
 536         { invoke-goal [| env | env quot call( env -- ) t ] }
 537     } invoke-pred defs<<
 538     invoke-goal ;
 539
 540 :: invoke* ( quot: ( env -- ? ) -- goal )
 541     quot collect-logic-vars :> args
 542     quot "[ %u invoke* ]" sprintf <pred> :> invoke*-pred
 543     invoke*-pred args logic-goal boa :> invoke*-goal
 544     V{
 545         { invoke*-goal [| env | env quot call( env -- ? ) ] }
 546     } invoke*-pred defs<<
 547     invoke*-goal ;
 548
 549 :: nquery ( goal-def/defs n/f -- bindings-array/success? )
 550     *trace?* get-global :> trace?
 551     0 :> n!
 552     f :> success?!
 553     V{ } clone :> bindings
 554     <env> :> env
 555     goal-def/defs replace-'__' normalize [ def>goal ] map
 556     env f <cut>
 557     <resolver> :> resolver
 558     [
 559         [
 560             resolver next dup [
 561                 resolver env>> table>> keys [ get NORMAL-LOGIC-VAR? ] filter
 562                 [ dup env at ] H{ } map>assoc
 563                 trace? get-global [ dup [ "%u: %u\n" printf ] assoc-each ] when
 564                 bindings push
 565                 t success?!
 566                 n/f [
 567                     n 1 + n!
 568                     n n/f >= [ return ] when
 569                 ] when
 570             ] when
 571         ] loop
 572     ] with-return
 573      bindings dup {
 574         [ empty? ]
 575         [ first keys empty? ]
 576     } 1|| [ drop success? ] [ >array ] if ;
 577
 578 : query ( goal-def/defs -- bindings-array/success? ) f nquery ;
 579
 580 ! nquery has been modified to use generators created by finite
 581 ! state machines to reduce stack consumption.
 582 ! Since the processing algorithm of the code is difficult
 583 ! to understand, the words no longer used are kept as private
 584 ! words for verification.
 585
 586 <PRIVATE
 587
 588 : each-until ( seq quot -- ) find 2drop ; inline
 589
 590 :: resolve-body ( body env cut quot: ( -- ) -- )
 591     body empty? [
 592         quot call( -- )
 593     ] [
 594         body unclip :> ( rest-goals! first-goal! )
 595         first-goal !! = [  ! cut
 596             rest-goals env cut quot resolve-body
 597             t cut set-info
 598         ] [
 599             first-goal callable? [
 600                 first-goal call( -- goal ) first-goal!
 601             ] when
 602             *trace?* get-global [
 603                 first-goal
 604                 [ pred>> name>> "in: { %s " printf ]
 605                 [ args>> [ "%u " printf ] each "}\n" printf ] bi
 606             ] when
 607             <env> :> d-env!
 608             f <cut> :> d-cut!
 609             first-goal pred>> defs>> [
 610                 first2 :> ( d-head d-body )
 611                 first-goal d-head [ args>> length ] same? [
 612                     d-cut cut? cut cut? or [ t ] [
 613                         V{ } clone :> trail
 614                         first-goal env d-head d-env trail d-env unify* [
 615                             d-body callable? [
 616                                 d-env trail <callback-env> d-body call( cb-env -- ? ) [
 617                                     rest-goals env cut quot resolve-body
 618                                 ] when
 619                             ] [
 620                                 d-body d-env d-cut [
 621                                     rest-goals env cut quot resolve-body
 622                                     cut cut? d-cut set-info-if-f
 623                                 ] resolve-body
 624                             ] if
 625                         ] when
 626                         trail [ first2 env-delete ] each
 627                         d-env env-clear
 628                         f
 629                     ] if
 630                ] [ f ] if
 631             ] each-until
 632         ] if
 633     ] if ;
 634
 635 :: (resolve) ( goal-def/defs quot: ( env -- ) -- )
 636     goal-def/defs replace-'__' normalize [ def>goal ] map :> goals
 637     <env> :> env
 638     goals env f <cut> [ env quot call( env -- ) ] resolve-body ;
 639
 640 : resolve ( goal-def/defs quot: ( env -- ) -- ) (resolve) ;
 641
 642 :: nquery/rec ( goal-def/defs n/f -- bindings-array/success? )
 643     *trace?* get-global :> trace?
 644     0 :> n!
 645     f :> success?!
 646     V{ } clone :> bindings
 647     [
 648         goal-def/defs normalize [| env |
 649             env table>> keys [ get NORMAL-LOGIC-VAR? ] filter
 650             [ dup env at ] H{ } map>assoc
 651             trace? get-global [ dup [ "%u: %u\n" printf ] assoc-each ] when
 652             bindings push
 653             t success?!
 654             n/f [
 655                 n 1 + n!
 656                 n n/f >= [ return ] when
 657             ] when
 658         ] (resolve)
 659     ] with-return
 660     bindings dup {
 661         [ empty? ]
 662         [ first keys empty? ]
 663     } 1|| [ drop success? ] [ >array ] if ;
 664
 665 : query/rec ( goal-def/defs -- bindings-array/success? )
 666     f nquery/rec ;
 667
 668 PRIVATE>
 669
 670 ! Built-in predicate definitions -----------------------------------------------------
 671
 672 LOGIC-PREDS:
 673     trueo failo
 674     varo nonvaro
 675     (<) (>) (>=) (=<) (==) (\==) (=) (\=)
 676     writeo writenlo nlo
 677     membero appendo lengtho listo ;
 678
 679 { trueo } [ drop t ] callback
 680
 681 { failo } [ drop f ] callback
 682
 683
 684 <PRIVATE LOGIC-VARS: X Y Z ; PRIVATE>
 685
 686 { varo X } [ X of logic-var? ] callback
 687
 688 { nonvaro X } [ X of logic-var? not ] callback
 689
 690
 691 { (<) X Y } [
 692     [ X of ] [ Y of ] bi 2dup [ number? ] both? [ < ] [ 2drop f ] if
 693 ] callback
 694
 695 { (>) X Y } [
 696     [ X of ] [ Y of ] bi 2dup [ number? ] both? [ > ] [ 2drop f ] if
 697 ] callback
 698
 699 { (>=) X Y } [
 700     [ X of ] [ Y of ] bi 2dup [ number? ] both? [ >= ] [ 2drop f ] if
 701 ] callback
 702
 703 { (=<) X Y } [
 704     [ X of ] [ Y of ] bi 2dup [ number? ] both? [ <= ] [ 2drop f ] if
 705 ] callback
 706
 707 { (==) X Y } [ [ X of ] [ Y of ] bi = ] callback
 708
 709 { (\==) X Y } [ [ X of ] [ Y of ] bi = not ] callback
 710
 711 { (=) X Y } [ dup [ X of ] [ Y of ] bi unify ] callback
 712
 713 { (\=) X Y } [
 714     clone [ clone ] change-env [ clone ] change-trail
 715     dup [ X of ] [ Y of ] bi unify not
 716 ] callback
 717
 718
 719 { writeo X } [
 720     X of dup sequence? [
 721         [ dup string? [ printf ] [ pprint ] if ] each
 722     ] [
 723         dup string? [ printf ] [ pprint ] if
 724     ] if t
 725 ] callback
 726
 727 { writenlo X } [
 728     X of dup sequence? [
 729         [ dup string? [ printf ] [ pprint ] if ] each
 730     ] [
 731         dup string? [ printf ] [ pprint ] if
 732     ] if nl t
 733 ] callback
 734
 735 { nlo } [ drop nl t ] callback
 736
 737
 738 <PRIVATE LOGIC-VARS: L L1 L2 L3 Head Tail N N1 ; PRIVATE>
 739
 740 { membero X L{ X . Tail } } fact
 741 { membero X L{ Head . Tail } } { membero X Tail } rule
 742
 743 { appendo L{ } L L } fact
 744 { appendo L{ X . L1 } L2 L{ X . L3 } } {
 745     { appendo L1 L2 L3 }
 746 } rule
 747
 748 { lengtho L{ } 0 } fact
 749 { lengtho L{ __ . Tail } N } {
 750     { lengtho Tail N1 }
 751     [ [ N1 of 1 + ] N is ]
 752 } rule
 753
 754 { listo L{ } } fact
 755 { listo L{ __ . __ } } fact