home *** CD-ROM | disk | FTP | other *** search
/ CP/M / CPM_CDROM.iso / cpm / languags / prolog / epro23.ark / PROVE.MAC < prev    next >
Text File  |  1986-11-02  |  10KB  |  620 lines
  1.  
  2. ; ===========================================================
  3. ; PROVE.Z80
  4. ;    prove routine for E-Prolog
  5. ;    June 22, 1985
  6.  
  7.     .Z80
  8.  
  9.  
  10. FALSE    EQU    0
  11. TRUE    EQU    1
  12. EMPTY    EQU    -1
  13. UNDEF    EQU    -2
  14. FROZEN    EQU    -3
  15.  
  16. DEBUG    EQU    FALSE
  17.  
  18. HT    EQU    9
  19. LF    EQU    10
  20. CR    EQU    13
  21. CTLZ    EQU    26
  22.  
  23. CPM    EQU        0000H
  24. BDOS    EQU    CPM+0005H
  25. CDMA    EQU    CPM+0080H
  26. TPA    EQU    CPM+0100H
  27.  
  28. ;BETASTATE * prbase;
  29.     DSEG
  30. PRBASE:    DW    0
  31.     CSEG
  32. ;
  33. ;prove(glist)
  34. ;/* This routine is iterative rather than recursive
  35. ;   in order to use as little heap space as possible.     */
  36. ;  PAIR glist;    /* list of goals */    in HL
  37. ;  {
  38. ;  ALPHASTATE * ast;            in IX
  39. ;  static BETASTATE * bst;        in IY
  40. ;  static BETASTATE * bbot;
  41. ;  static int x;
  42.     DSEG
  43. BBOT:    DW    0
  44.     CSEG
  45. ;
  46. PROVE::
  47. ;  bst = prbase = makebeta(empty,listone(glist));
  48. ;#define    listone(x)    makepair((x),empty)
  49.     LD    DE,EMPTY
  50.     CALL    MKPAIR##
  51.     LD    IX,EMPTY
  52.     CALL    MKBETA##
  53.     LD    (PRBASE),IY
  54. ;  freeze(bst);
  55.     CALL    FREEZE##
  56. ;  goto bstart;
  57.     JP    BSTART
  58. ;
  59. ;/*==========*/
  60. ;   astart:    /* start an alpha state here */
  61. ;/*==========*/
  62. ASTART:
  63. ;#ifdef DEBUG
  64. IF DEBUG
  65. ;  printf("\nALPHA %04x: ",ast);
  66.     LD    HL,AS1MSG
  67.     CALL    MSG##
  68.     DSEG
  69. AS1MSG:    DB    CR,LF,'ALPHA ',0
  70.     CSEG
  71.     PUSH    IX
  72.     POP    HL
  73.     CALL    PRHEX
  74.     LD    A,' '
  75.     CALL    CHROUT##
  76. ;  eprint(ast->goal->left.list,ast->pred->subst);
  77.     CALL    XPRED##
  78.     CALL    @SUBST##
  79.     PUSH    HL
  80.     CALL    XGOAL##
  81.     CALL    @LEFT##
  82.     POP    DE
  83.     CALL    EPRINT##
  84. ;#endif
  85. ENDIF
  86. ;
  87. ;/*==========*/
  88. ;   arpt:    /* repeat this alpha state */
  89. ;/*==========*/
  90. ARPT:
  91. ;  if (numbp(ast->datb))
  92.     CALL    XDATB##
  93.     CALL    NUMBP##
  94.     JP    Z,AR1
  95. ;    {
  96. ;    /* built-in command */
  97. ;    bst = (BETASTATE *)empty;
  98.     LD    IY,EMPTY
  99. ;    if (x = (*((BOOLEAN (*)())(ast->datb)))
  100. ;               (ast->goal->left.list->right.list,ast,
  101. ;                ast->pred->subst,&bst))
  102.     CALL    XPRED##
  103.     CALL    @SUBST##
  104.     PUSH    HL        ; ast->pred->subst
  105.     CALL    XGOAL##
  106.     POP    DE
  107.     CALL    V@LEFT
  108.     CALL    V@RIGHT
  109.     PUSH    HL        ; ast->goal->left.list->right.list
  110.     PUSH    DE
  111.     CALL    XDATB##        ; ast->datb
  112.     LD    (ADDR+1),HL
  113.     POP    DE
  114.     POP    HL
  115. ADDR:    CALL    0        ; address filled in here
  116.     JR    Z,AR2
  117. ;      {
  118. ;      if (x == EMPTY)
  119.     LD    DE,EMPTY
  120.     CALL    CPHL##
  121.     JR    NZ,AR4
  122. ;        {
  123. ;        /* CUT */
  124. ;     bst = ast->back;
  125.     CALL    XBACK##
  126.     PUSH    HL
  127.     POP    IY
  128. ;     release(ast);
  129.     PUSH    IX
  130.     POP    HL
  131.     CALL    RLS##
  132. ;     ast = (bbot = (ast->pred))->pred;
  133.     CALL    XPRED##
  134.     LD    (BBOT),HL
  135.     CALL    @PRED##
  136.     PUSH    HL
  137.     POP    IX
  138. ;        if (ast == (ALPHASTATE *)empty)
  139.     LD    DE,EMPTY
  140.     CALL    CPHL##
  141.     JR    NZ,AR5X
  142. ;          return FALSE;
  143. RETF:    XOR    A
  144.     RET
  145. ; *** release from here (bst) back to there (bbot)
  146. AR5X:
  147.     CALL    BRLS##
  148.     LD    HL,(BBOT)
  149.     PUSH    IY
  150.     POP    DE
  151.     CALL    CPHL##
  152.     JR    Z,AR5
  153.     CALL    YPRED##
  154.     CALL    RLS##
  155.     CALL    @XBACK##
  156.     PUSH    HL
  157.     POP    IY
  158.     JR    AR5X
  159. ;AR5: combined with the other case, below
  160. ;
  161. AR4:
  162. ;      /* A fake beta to hold temporary data for unifies */
  163. ;      if (bst == (BETASTATE *)empty)
  164.     PUSH    IY
  165.     POP    HL
  166.     LD    DE,EMPTY
  167.     CALL    CPHL##
  168.     JR    NZ,AR9
  169. ;        bst = makebeta(ast,empty);
  170.     LD    HL,EMPTY
  171.     CALL    MKBETA##
  172. AR9:
  173. ;      freeze(bst);
  174.     CALL    FREEZE##
  175. ;      goto bstart;
  176.     JP    BSTART
  177. ;      }
  178. AR2:
  179. ;    if (bst != (BETASTATE *)empty)
  180.     PUSH    IY
  181.     POP    HL
  182.     LD    DE,EMPTY
  183.     JR    Z,AR6
  184. ;      release(bst);
  185.     CALL    BRLS##        ; ? RLS ?
  186. AR6:
  187. ;    ast->datb = empty; /* failure */
  188.     LD    HL,EMPTY
  189.     CALL    XLDATB##
  190. ;    }
  191. AR1:
  192. ;  if (ast->datb == (PAIR)empty)
  193.     CALL    XDATB##
  194.     LD    DE,EMPTY
  195.     CALL    CPHL##
  196.     JR    NZ,AR7
  197. ;    {
  198. AR5:
  199. ;    /* no (more) facts in the database - FAIL*/
  200. ;    /* roll back pointer in tree-predecessor */
  201. ;    ast->pred->assertion.list = ast->goal;
  202.     CALL    XGOAL##
  203.     PUSH    HL
  204.     CALL    XPRED##
  205.     PUSH    HL
  206.     POP    IY
  207.     POP    HL
  208.     CALL    YLASS##
  209. ;    bst = ast->back;
  210.     CALL    XBACK##
  211.     PUSH    HL
  212.     POP    IY
  213. ;    release(ast);
  214.     PUSH    IX
  215.     POP    HL
  216.     CALL    RLS##
  217. ;    goto bafail;
  218.     JP    BAFAIL
  219. ;    }
  220. AR7:
  221. ;  bst = makebeta(ast,ast->datb->left.list);
  222.     CALL    XDATB##
  223.     CALL    @LEFT##
  224.     CALL    MKBETA##
  225. ;  ast->datb = ast->datb->right.list;
  226.     CALL    XDATB##
  227.     CALL    @RIGHT##
  228.     CALL    XLDATB##
  229. ;  if (unify(ast->goal->left.list,ast->pred->subst,
  230. ;            bst->assertion.list->left.list,bst->subst))
  231.     CALL    YSUBST##
  232.     PUSH    HL
  233.     CALL    YASS##
  234.     CALL    @LEFT##
  235.     POP    DE
  236.     EXX
  237.     CALL    XPRED##
  238.     CALL    @SUBST##
  239.     PUSH    HL
  240.     CALL    XGOAL##
  241.     CALL    @LEFT
  242.     POP    DE
  243.     CALL    UNIFY##
  244.     JR    Z,AR8
  245. ;    {
  246. ;    freeze(bst);
  247.     CALL    FREEZE##
  248. ;#ifdef DEBUG
  249. IF DEBUG
  250. ;msg("  *** unified");
  251.     LD    HL,AR7MSG
  252.     CALL    MSG##
  253.     DSEG
  254. AR7MSG:    DB    '  *** unified',0
  255.     CSEG
  256. ;#endif
  257. ENDIF
  258. ;    bst->assertion.list = bst->assertion.list->right.list;
  259.     CALL    YASS##        ; *** how about variable here?
  260.     CALL    @RIGHT##
  261.     CALL    YLASS##
  262. ;    goto bstart;
  263.     JP    BSTART
  264. ;    }
  265. AR8:
  266. ;#ifdef DEBUG
  267. IF DEBUG
  268. ;msg("  *** not unified");
  269.     LD    HL,AR8MSG
  270.     CALL    MSG##
  271.     DSEG
  272. AR8MSG:    DB    '  *** not unified',0
  273.     CSEG
  274. ;#endif
  275. ENDIF
  276. ;  brelease(bst);
  277.     CALL    BRLS##
  278. ;  goto abfail;
  279.     JP    ABFAIL
  280. ;
  281. ;/*==========*/
  282. ;   absucc:    /* return to alpha after success of beta */
  283. ;/*==========*/
  284. ;  fatal("\r\nabsucc not written.");
  285. ;
  286. ;/*==========*/
  287. ;   abfail:    /* return to alpha after failure of beta */
  288. ;/*==========*/
  289. ABFAIL    EQU    ARPT
  290. ;  goto arpt;
  291. ;
  292. ;/*==========*/
  293. ;   bstart:    /* start beta state here */
  294. ;/*==========*/
  295. BSTART:
  296. ;#ifdef DEBUG
  297. IF DEBUG
  298. ;  printf("\nBETA %04x: ",bst);
  299.     LD    HL,BSMSG
  300.     CALL    MSG##
  301.     DSEG
  302. BSMSG:    DB    CR,LF,'BETA  ',0
  303.     CSEG
  304.     PUSH    IY
  305.     POP    HL
  306.     CALL    PRHEX
  307.     LD    A,' '
  308.     CALL    CHROUT##
  309. ;  eprint(bst->assertion.list,bst->subst);
  310.     CALL    YSUBST##
  311.     PUSH    HL
  312.     CALL    YASS##
  313.     POP    DE
  314.     CALL    EPRINT##
  315. ;#endif
  316. ENDIF
  317. ;
  318. ;/*==========*/
  319. ;   brpt:    /* repeat beta state */
  320. ;/*==========*/
  321. ;BRPT:
  322. ;  if (bst->assertion.list == (PAIR)empty)
  323.     CALL    YASS
  324.     LD    DE,EMPTY
  325.     CALL    CPHL##
  326.     JR    NZ,BR1
  327. ;    {
  328. ;    /* no (more) goals - Succeed */
  329. ;    bbot = bst;
  330.     LD    (BBOT),IY
  331. ;    while (bst->assertion.list == (PAIR)empty)
  332. BR3:
  333.     CALL    YASS##
  334.     LD    DE,EMPTY
  335.     CALL    CPHL##
  336.     JR    NZ,BR4
  337. ;      {
  338. ;      if (bst == prbase)
  339.     PUSH    IY
  340.     POP    HL
  341.     LD    DE,(PRBASE)
  342.     CALL    CPHL##
  343.     JR    NZ,BR5
  344. ;        {
  345. ;        if (infile == stdin && outfile == stdout)
  346.     LD    A,(INF##)
  347.     OR    A
  348.     JR    NZ,BR6
  349.     LD    A,(OUTF##)
  350.     OR    A
  351.     JR    NZ,BR6
  352. ;          msg("Yes.");
  353.     LD    HL,BR6MSG
  354.     CALL    MSG##
  355.     DSEG
  356. BR6MSG:    DB    'Yes.',0
  357.     CSEG
  358. BR6:
  359. ;        if (prvals())
  360.     CALL    PRVALS
  361.     JR    Z,BR7
  362. ;          {
  363. ;          bst = bbot;
  364.     LD    IY,(BBOT)
  365. ;          goto bafail;
  366.     JP    BAFAIL
  367. ;          }
  368. BR7:
  369. ;        else
  370. ;          return;
  371.     RET
  372. ;        }
  373. BR5:
  374. ;      bst = bst->pred->pred;
  375.     CALL    YPRED##
  376.     CALL    @PRED##
  377.     PUSH    HL
  378.     POP    IY
  379. ;      }
  380.     JR    BR3
  381. BR4:
  382. ;    ast = makealpha(bst,bst->assertion.list,bbot);
  383.     CALL    YASS##
  384.     LD    DE,(BBOT)
  385.     CALL    MKALPHA##
  386. ;    }
  387.     JR    BR2
  388. BR1:
  389. ;  else
  390. ;    /* both pointers are to bst */
  391. ;    ast = makealpha(bst,bst->assertion.list,bst);
  392.     CALL    YASS##
  393.     PUSH    IY
  394.     POP    DE
  395.     CALL    MKALPHA##
  396. BR2:
  397. ;  bst->assertion.list = bst->assertion.list->right.list;
  398.     CALL    YASS##
  399.     CALL    @RIGHT##
  400.     CALL    YLASS##
  401. ;  goto astart;
  402.     JP    ASTART
  403. ;
  404. ;/*==========*/
  405. ;   basucc:    /* return to beta after success of alpha */
  406. ;/*==========*/
  407. ;BASUCC    EQU    BRPT
  408. ;  goto brpt;
  409. ;
  410. ;/*==========*/
  411. ;   bafail:    /* return to beta after failure of alpha */
  412. ;/*==========*/
  413. BAFAIL:
  414. ;  ast = bst->pred;
  415.     CALL    YPRED##
  416.     PUSH    HL
  417.     POP    IX
  418. ;  if (ast == (ALPHASTATE *)empty)
  419.     LD    DE,EMPTY
  420.     CALL    CPHL##
  421.     JR    NZ,BA1
  422. ;    return FALSE;
  423.     XOR    A
  424.     RET
  425. BA1:
  426. ;  brelease(bst);
  427.     CALL    BRLS##
  428. ;  goto abfail;
  429.     JP    ABFAIL
  430. ;  }
  431. ;
  432. ;prvals()
  433. ;  {
  434. ;  SUBST * x;
  435. ;  int cnt;
  436.     DSEG
  437. X:    DW    0
  438. CNT:    DB    0
  439.     CSEG
  440. PRVALS:
  441. ;
  442. ;  cnt = 0;
  443.     XOR    A
  444.     LD    (CNT),A
  445. ;  for (x = prbase->subst ; substp(x) ; x++)
  446.     LD    HL,(PRBASE)
  447.     CALL    @SUBST##
  448.     LD    (X),HL
  449. PR2:
  450.     CALL    SUBSTP##
  451.     JR    Z,PR1
  452. ;    {
  453. ;    chrout('\t');
  454.     LD    A,HT
  455.     CALL    CHROUT##
  456. ;    msg(x->vname->string);
  457.     CALL    @VNAME##
  458.     CALL    @STR##
  459.     CALL    MSG##
  460. ;    msg(" = ");
  461.     LD    HL,PR1MSG
  462.     CALL    MSG##
  463.     DSEG
  464. PR1MSG:    DB    ' = ',0
  465.     CSEG
  466. ;    prval(x);
  467.     LD    HL,(X)
  468.     CALL    PRVAL
  469. ;    cnt = 1;
  470.     LD    A,1
  471.     LD    (CNT),A
  472. ;    msg("\r\n");
  473.     CALL    CRLF##
  474. ;    }
  475.     LD    HL,(X)
  476.     LD    DE,6
  477.     ADD    HL,DE
  478.     LD    (X),HL
  479.     JR    PR2
  480. PR1:
  481. ;  if (! cnt)
  482.     LD    A,(CNT)
  483.     OR    A
  484.     JR    NZ,PR3
  485. ;    {
  486. ;    msg("\r\n");
  487.     CALL    CRLF##
  488. ;    return FALSE;
  489.     XOR    A
  490.     RET
  491. ;    }
  492. PR3:
  493. ;  msg("More?");
  494.     LD    HL,PR3MSG
  495.     CALL    MSG##
  496.     DSEG
  497. PR3MSG:    DB    'More?',0
  498.     CSEG
  499. ;  while (separp(rdchar()))
  500. ;    ;
  501. PR4:
  502.     CALL    RDCHAR##
  503.     CALL    SEPARP##
  504.     JR    NZ,PR4
  505. ;  if (character == 'Y' || character == 'y')
  506. ;    return TRUE;
  507. ;  return FALSE;
  508.     LD    A,(CHR##)
  509.     CP    'Y'
  510.     JR    Z,RETT
  511.     CP    'y'
  512.     JR    Z,RETT
  513.     XOR    A
  514.     RET
  515. RETT:    LD    A,1
  516.     OR    A
  517.     RET
  518. ;  }
  519. ;
  520. ;prval(sub)
  521. ;  SUBST * sub;
  522. ;  {
  523. ;  static SUBVAL as;
  524.     DSEG
  525. AS:    DW    0
  526.     CSEG
  527. PRVAL:
  528. ;
  529. ;  as.val = value(sub);
  530.     CALL    VALUE##
  531.     LD    (AS),HL
  532. ;  if (substp(as.val))
  533.     CALL    SUBSTP##
  534.     JR    Z,PR6
  535. ;    msg(as.val->vname->string);
  536.     CALL    @VNAME##
  537.     CALL    @STR##
  538.     CALL    MSG##
  539.     RET
  540. PR6:
  541. ;  else
  542. ;    eprint(as.assgn->sexp.list,as.assgn->slist);
  543.     CALL    @SLIST##
  544.     PUSH    HL
  545.     LD    HL,(AS)
  546.     CALL    @EXPR##
  547.     POP    DE
  548.     CALL    EPRINT##
  549.     RET
  550. ;  }
  551. ;
  552. IF DEBUG
  553. ; display HL in hex
  554. PRHEX:    LD    A,H
  555.     CALL    HINYB
  556.     CALL    LONYB
  557.     LD    A,L
  558.     CALL    HINYB
  559.     CALL    LONYB
  560.     RET
  561. HINYB:    PUSH    AF
  562.     AND    0F0H
  563.     RRCA
  564.     RRCA
  565.     RRCA
  566.     RRCA
  567.     CALL    LONYBX
  568.     POP    AF
  569.     RET
  570. LONYB:    AND    00FH
  571. LONYBX:    ADD    A,90H
  572.     DAA
  573.     ADC    A,40H
  574.     DAA
  575.     JP    CHROUT##
  576. ENDIF
  577.  
  578. ; right (value if variable)
  579. ; expression in HL, substs in DE
  580. V@RIGHT:
  581.     PUSH    DE
  582.     PUSH    HL
  583.     LD    HL,@RIGHT##
  584.     LD    (V@R+1),HL
  585. V@9:    POP    HL
  586.     CALL    VARP##
  587.     JR    NZ,V@0
  588. V@R:    CALL    0        ; filled in
  589.     POP    DE
  590.     RET
  591. V@0:    POP    DE
  592.     CALL    VF##
  593.     CALL    VALUE##
  594.     PUSH    HL
  595.     CALL    SUBSTP##
  596.     JR    Z,V@1
  597.     LD    HL,V@ERR
  598.     JP    ERROR##
  599.     DSEG
  600. V@ERR:    DB    CR,LF,'Meta-variable remaining',0
  601.     CSEG
  602. V@1:    POP    HL
  603.     PUSH    HL
  604.     CALL    @SLIST##
  605.     POP    HL
  606.     PUSH    DE
  607.     CALL    @EXPR##
  608.     JR    V@R    
  609.  
  610. ; left (value if variable)
  611. ; expression in HL, substs in DE
  612. V@LEFT:
  613.     PUSH    DE
  614.     PUSH    HL
  615.     LD    HL,@LEFT##
  616.     LD    (V@R+1),HL
  617.     JR    V@9
  618.  
  619.     END
  620.