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