3 (****************************************************************************
\r
5 * RETRIEVAL P R O V E R LOOKING FOR AXIOMS *
\r
6 * All rights reserved *
\r
8 ****************************************************************************)
\r
14 (***************************************************************************)
\r
15 (* CONSTANTS, VARIABLES AND OBJECTS USED IN PROGRAM *)
\r
16 (***************************************************************************)
\r
22 (* CHARACTER CODES <IN ASCII> *)
\r
24 CHRNEG = 78, (* NEGATION 'N' *)
\r
25 CHREQU = 69, (* EXISTENTIAL QUANTIFIER : 'E' *)
\r
26 CHRITG = 64, (* ITERATION GREAT QUANTIFIER: '@' *)
\r
27 CHRGQU = 65, (* GLOBAL QUANTIFIER : 'A' *)
\r
28 CHRITE = 85, (* EXISTENTIAL ITERATION QUANTIFIER: 'U' *)
\r
29 CHROR = 86, (* DISJUNCTION : 'V' *)
\r
30 CHRAND = 38, (* CONJUNCTION : '&' *)
\r
31 CHRCOM = 44, (* COMMA *)
\r
32 CHRLPA = 40, (* LEFT PARENTHESIS *)
\r
33 CHRRPA = 41, (* RIGHT PARENTHESIS *)
\r
34 CHRBLK = 32, (* BLANK *)
\r
35 CHREND = 63, (* FORMULA TERMINATOR : '?' *)
\r
36 CHRCRT = 10, (* CARRIAGE RETURN *)
\r
37 CHREQS = 61, (* "EQUALS" SIGN - FOR IMPLICATION *)
\r
38 CHRGTR = 62, (* "GREATER" SIGN - ALSO FOR IMPLICATION *)
\r
39 CHRLSS = 60, (* "<" -SIGN FOR EQUIVALENCE *)
\r
41 (* FORMULA NODE TYPES *)
\r
43 LOGKIND = 01, (* LOGICAL CONSTANT *)
\r
44 VARKIND = 02, (* VARIABLE *)
\r
45 EQVKIND = 03, (* EQUIVALENCE *)
\r
46 CONKIND = 04, (* CONJUNCTION *)
\r
47 DISKIND = 05, (* DISJUNCTION *)
\r
48 IMPKIND = 06, (* IMPLICATION *)
\r
49 NEGKIND = 07, (* NEGATION *)
\r
50 IGQKIND = 08, (* ITERATION GREAT QUANTIFIER *)
\r
51 ITEKIND = 09, (* ITERATION EXISTENTIAL QUANTIFIER *)
\r
52 IFFKIND = 10, (* BRANCHING *)
\r
53 BEGKIND = 11, (* BEGINNING OF A COMPOSITION *)
\r
54 WHIKIND = 12, (* CONDITIONAL ITERATION *)
\r
55 QUAKIND = 13, (* QUANTIFIER *)
\r
56 ENDKIND = 14, (* END OF COMPOSITION *)
\r
57 THNKIND = 15, (* POSITIVE CHOICE *)
\r
58 ELSKIND = 16, (* NEGATIVE CHOICE *)
\r
59 FIFKIND = 17, (* END OF BRANCHING *)
\r
60 DOFKIND = 18, (* POSITIVE CONDITIONAL ITERATION *)
\r
61 ODFKIND = 19, (* END OF CONDITIONAL ITERATION *)
\r
62 SEMKIND = 20, (* SEMICOLON *)
\r
63 VARPROG = 21, (* SUBSTITUTION FOR TERMS X:=TERM *)
\r
64 BVARPRO = 22, (* SUBSTITUTION FOR BOOLEAN VARIABLE A:=FORMULA *)
\r
65 LITKIND = 23, (* LITERAL *)
\r
66 LT1KIND = 24, (* RELATION DEFINED BY PROCEDURE *)
\r
67 FUNKIND = 25, (* FUNCTION OR CONSTANT *)
\r
68 FN1KIND = 26, (* FUNCTION DEFINED BY PROCEDURE *)
\r
69 CNTKIND = 27, (* CONSTANT - NUMBER *)
\r
70 CN1KIND = 28, (* FALSE CONSTANT *)
\r
71 VRUKIND = 29, (* SPECIAL KIND OF VARIABLE - U *)
\r
72 SUBKIND = 30, (* VARIABLE TO BE SUBSTITUTED ON *)
\r
73 CN2KIND = 31, (* CONSTANT -NOT NUMBER -OF THE FORM N *)
\r
74 ARIKIND = 32, (* ARITHMETIC OPERATORS *)
\r
75 BVAKIND = 33, (* LOGICAL VARIABLE TO BE SUBSTITUTED ON *)
\r
76 EQUKIND = 34, (* EQUALITY *)
\r
77 SIGNTRM = 35, (* TRACE OF TERM *)
\r
82 VAR KIND,IDENT:INTEGER,
\r
86 UNIT SEQUENT:CLASS;
\r
87 VAR PLEAF,LLEAF:TNODE,
\r
91 UNIT POINTER:CLASS;
\r
97 UNIT LIST_TERM:CLASS;
\r
102 UNIT LIST_AXIOMS:CLASS;
\r
108 VAR FUN_REL : TNODE,
\r
120 EQU_NUMBER:INTEGER, (* CURRENT EQUATION *)
\r
121 K_MN_K:INTEGER, (* CURRENT NUMBER OF ITERATIONS *)
\r
122 LAST_S:INTEGER, (* MAXIMAL NUMBER OF VARPROG *)
\r
123 LAST_Q:INTEGER, (* MAXIMAL NUMBER OF BVARPRO *)
\r
124 LAST_X:INTEGER, (* MAXIMAL NUMBER OF VARKIND *)
\r
125 LAST_D:INTEGER, (* MAXIMAL NUMBER OF TERM SIGN *)
\r
126 C,PEEKCH:INTEGER, (* CODES OF CURRENT CHAR FROM INPUT FILE *)
\r
127 L:INTEGER, (* NUMBER OF LAST READ CHAR FROM INPUT FILE *)
\r
128 CHARSH:INTEGER, (* CURRENT NUMBER IN LINE *)
\r
129 DIF:INTEGER, (* DISTINGUISH KINDS OF FORMULAS TO PROVE *)
\r
130 CHI:BOOLEAN, (* SHOW IF FORMULA FROM WHILE WAS PROVED *)
\r
131 LOGIC:BOOLEAN, (* TELLS WHETHER WHILE HAS ALREADY BEEN USED *)
\r
132 LL,LR:INTEGER; (* COUNTS LEFT AND RIGHT PROGRAM BRACKETS *)
\r
134 (***************************************************************************)
\r
137 (***************************************************************************)
\r
138 (* GENERATE TREE OF THE FORMULA *)
\r
139 (***************************************************************************)
\r
141 (***************************************************************************)
\r
142 (* LOOKS AT NEXT NON-BLANK ON INPUT *)
\r
144 UNIT PNC:FUNCTION:INTEGER;
\r
145 VAR D : CHARACTER;
\r
148 (* FILL PEEKCHAR IGNORING BLANKS AND CR'S *)
\r
149 WHILE PEEKCH=0 OR PEEKCH=CHRBLK OR PEEKCH=CHRCRT
\r
158 (****************************************************************************)
\r
159 (* MOVES FORWARD N STEPS AND READS CHARACTER *)
\r
161 UNIT LOOKN:PROCEDURE(N:INTEGER);
\r
170 (****************************************************************************)
\r
171 (* READS N-TH POSITION IN FILE *)
\r
172 UNIT RETN:PROCEDURE(N:INTEGER);
\r
183 (****************************************************************************)
\r
184 (* DISTINGUISH PROGRAMS WRITTEN IN LOGLAN *)
\r
186 UNIT PRKEY : FUNCTION(N:INTEGER) : INTEGER;
\r
187 VAR V,W : ARRAYOF CHARACTER,
\r
192 V(1):='I';V(2):='F';V(3):='T';V(4):='H';V(5):='E';V(6):='N';
\r
193 V(7):= 'L'; V(8):= 'S'; V(9):= 'B'; V(10):= 'G'; V(11):= 'D';
\r
194 V(12):= 'W'; V(13):= 'O';V(14):= 'i'; V(15):= 'f'; V(16):= 't';
\r
195 V(17):= 'h'; V(18):= 'e'; V(19):= 'n'; V(20):= 'l'; V(21):= 's';
\r
196 V(22):= 'b'; V(23):= 'g'; V(24):= 'd'; V(25):='w'; V(26):= 'o';
\r
199 IF NOT EOF(G) THEN
\r
210 2:IF V(1) = W(1) OR V(14) = W(1) THEN
\r
211 IF V(2) = W(2) OR V(15) = W(2) THEN RESULT:=1 FI (* 'IF' *)
\r
213 IF V(2) = W(1) OR V(15) = W(1) THEN
\r
214 IF V(1) = W(2) OR V(14) = W(2) THEN RESULT:=2 FI (* 'FI' *)
\r
216 IF V(11) = W(1) OR V(24) = W(1) THEN
\r
217 IF V(13) = W(2) OR V(26) = W(2) THEN RESULT:=3 FI (* 'DO' *)
\r
219 IF V(13) = W(1) OR V(26) = W(1) THEN
\r
220 IF V(11) = W(2) OR V(24) = W(2) THEN RESULT:=4 FI (* 'OD' *)
\r
223 3:IF V(5) = W(1) OR V(18) = W(1) THEN
\r
224 IF ((V(6) = W(2)) OR (V(19) = W(2))) AND ((V(11)=W(3))
\r
225 OR (V(24)=W(3))) THEN RESULT:=5 FI (* 'END' *)
\r
228 4:IF V(3) = W(1) OR V(16) = W(1) THEN
\r
229 IF ((V(4) = W(2)) OR (V(17)=W(2))) AND ((V(5)=W(3))
\r
230 OR (V(18)=W(3))) THEN
\r
231 IF V(6) = W(4) OR V(19) = W(4) THEN RESULT:=6 FI (* 'THEN' *)
\r
234 IF V(5) = W(1) OR V(18) = W(1) THEN
\r
235 IF ((V(7) = W(2)) OR (V(20)=W(2))) AND ((V(8)=W(3))
\r
236 OR (V(21)=W(3))) THEN IF V(5) = W(4) OR V(18) = W(4) THEN
\r
237 RESULT:=7 FI (* 'ELSE' *)
\r
241 5:IF V(9) = W(1) OR V(22) = W(1) THEN
\r
242 IF ((V(5) = W(2)) OR (V(18)=W(2))) AND ((V(10)=W(3))
\r
243 OR (V(23)=W(3))) THEN
\r
244 IF ((V(1)=W(4)) OR (V(14)=W(4))) AND ((V(6)=W(5))
\r
245 OR (V(19)=W(5))) THEN RESULT:=8 FI (* 'BEGIN' *)
\r
248 IF V(12) = W(1) OR V(25) = W(1) THEN
\r
249 IF ((V(4) = W(2)) OR (V(17)=W(2))) AND ((V(1)=W(3))
\r
250 OR (V(14)=W(3))) THEN
\r
251 IF ((V(7)=W(4)) OR (V(20)=W(4))) AND ((V(5)=W(5))
\r
252 OR (V(18)=W(5))) THEN RESULT:=9 (* 'WHILE' *)
\r
261 (*****************************************************************************)
\r
262 (* READS FORMULA FROM INPUT AND CONSTRUCT A TNODE *)
\r
264 UNIT GEN_TREE : FUNCTION : TNODE;
\r
269 T:=ARG_TREE; (* READ FIRST ARGUMENT *)
\r
270 C:=PNC; (* NEXT INPUT CHARACTER *)
\r
271 WHILE C=CHROR OR C=CHRAND OR C=CHREQS OR C=CHRLSS OR C=118
\r
272 DO (* LOOP FOR MORE *)
\r
273 S:=NEW TNODE; (* ARGUMENTS *)
\r
274 IF T=NONE THEN CALL EXCEPTIONS(1) FI; (* NULL ARGUMENT *)
\r
276 WHEN CHROR,118 : S.KIND:=DISKIND;
\r
277 WHEN CHRAND: S.KIND:=CONKIND;
\r
278 WHEN CHRLSS: IF PNC<>61 ORIF PNC<>62 THEN CALL EXCEPTIONS(1) FI;
\r
280 WHEN CHREQS: IF PNC<>CHRGTR THEN CALL EXCEPTIONS(1) FI;
\r
283 S.RIGHT:=ARG_TREE; (* NEXT ARGUMENT *)
\r
285 IF S.RIGHT=NONE THEN CALL EXCEPTIONS(1) FI;
\r
292 (****************************************************************************)
\r
293 (* READS ONE ARGUMENT OF INPUT FORMULA *)
\r
295 UNIT ARG_TREE : FUNCTION : TNODE;
\r
302 IF C=CHREND THEN RETURN FI; (* RETURN NONE *)
\r
307 WHEN CHRNEG,110 :T.KIND:=NEGKIND; (* NEGATION *)
\r
308 WHEN CHRGQU :T.KIND:=QUAKIND; (* GLOBAL QUANTIFIER *)
\r
309 C:=PNC; (* FOLLOWING VARIABLE *)
\r
310 CALL SEARCH_NUM(T.IDENT,TRUE); (* NUMBER *)
\r
311 WHEN CHREQU :S:=NEW TNODE; (* EXISTENTIAL QUANTIFIER *)
\r
312 U:=NEW TNODE; (* CONVERT TO -'A'- *)
\r
316 C:=PNC; (* VARIABLE NAME *)
\r
317 CALL SEARCH_NUM(U.IDENT,TRUE); (* VARIABLE NUMBER *)
\r
321 OTHERWISE Q:=FALSE
\r
324 T.LEFT:=ARG_TREE; (* CONTINUE DEPTH SEARCH *)
\r
325 IF T.LEFT=NONE THEN CALL EXCEPTIONS(1) FI;
\r
328 IF C=CHROR ORIF C=CHRRPA ORIF C=CHRAND ORIF C=CHREQS ORIF C=CHRGTR ORIF
\r
335 CALL EXCEPTIONS(1);
\r
338 CALL EXCEPTIONS(1);
\r
342 RESULT := GEN_TREE
\r
343 ELSE (* LITERAL ONLY *)
\r
344 RESULT := LIT_ARG (* SO READ IT *)
\r
349 (****************************************************************************)
\r
350 (* SEARCH FOR A NUMBER *)
\r
352 UNIT SEARCH_NUM:PROCEDURE(INOUT B:INTEGER;ALEF:BOOLEAN);
\r
355 IF C<48 OR C>57 THEN
\r
364 IF NOT ALEF THEN CALL RETN(L-1) FI;
\r
365 WHILE C>47 AND C<58
\r
370 IF ALEF THEN B:=B+1 FI;
\r
374 (****************************************************************************)
\r
375 (* CONSTRUCT PREDICATE *)
\r
377 UNIT PRED : PROCEDURE ( INOUT A, B : INTEGER ; ALEF : BOOLEAN );
\r
380 WHEN 61 : A := EQUKIND;
\r
381 WHEN 33 : A := LT1KIND;
\r
382 OTHERWISE A := LITKIND;
\r
383 CALL SEARCH_NUM ( B, ALEF ); (* SEARCH A NUMBER OF *)
\r
384 ESAC; (* PREDICATE *)
\r
387 (***************************************************************************)
\r
388 (* CONSTRUCT TERM *)
\r
390 UNIT MAKE_TERM : PROCEDURE ( INOUT A, B : INTEGER; C : INTEGER, ALEF : BOOLEAN );
\r
393 CALL SEARCH_NUM ( B, ALEF ); (* SEARCH A NUMBER OF *)
\r
394 END MAKE_TERM; (* TERM *)
\r
396 (***************************************************************************)
\r
397 (* GIVES A LENGTH OF PATTERN OF 'S' *)
\r
399 UNIT LEN_SUB : FUNCTION : INTEGER;
\r
403 IF C=83 OR C=115 OR C=81 OR C=113 THEN (* CHECK -S:=... OR -Q:=... *)
\r
408 IF NOT EOF(G) THEN
\r
417 IF ALFA THEN EXIT FI;
\r
418 IF C=ORD(':') THEN
\r
429 (***************************************************************************)
\r
430 (* MAKES A SUBSTITUTION *)
\r
432 UNIT SUBSTITUTION:FUNCTION:TNODE;
\r
436 IF C=83 OR C=115 THEN
\r
437 T.KIND:=VARPROG (* READ S *)
\r
439 T.KIND:=BVARPRO (* READ A *)
\r
441 CALL SEARCH_NUM(T.IDENT,TRUE); (* NUMBER OF 'S' *)
\r
444 WHEN VARPROG:T.LEFT:=LIT_ARG;
\r
445 WHEN BVARPRO:CALL RETN(L-1);T.LEFT:=GEN_TREE;CALL RETN(L-1);
\r
450 (***************************************************************************)
\r
451 (* CONSTRUCT IF-ALFA-THEN-K-ELSE-M-FI PROGRAM *)
\r
453 UNIT PROG_IF:FUNCTION:TNODE;
\r
457 T.KIND:=IFFKIND; (* 'IF' *)
\r
459 T.LEFT:=GEN_TREE; (* ALFA *)
\r
460 CALL RETN(L-1); (* BACK BEFORE 'T' *)
\r
461 IF PRKEY(4)<>6 THEN CALL EXCEPTIONS(1) FI;
\r
464 S.KIND:=THNKIND; (* 'THEN '*)
\r
466 S.LEFT:=CONSUB; (* PROGRAM 'K' *)
\r
469 IF PRKEY(4)=7 THEN (* 'ELSE' *)
\r
472 U.LEFT:=CONSUB (* PROGRAM 'M' *)
\r
476 IF PRKEY(2)<>2 THEN CALL EXCEPTIONS(1) FI;
\r
479 IF LL=LR THEN (* AFTER NESTING DO *)
\r
480 (* 'WHILE ETC ' PROGRAM ON *)
\r
481 U.RIGHT:=GEN_TREE; (* FORMULA BETA *)
\r
483 FI; (* OR TERM TAU *)
\r
487 (***************************************************************************)
\r
489 (* CONSTRUCT BEGIN-K;M;N; -OR MORE PROGRAMS- END PROGRAM *)
\r
491 UNIT PROG_BEGIN:FUNCTION:TNODE;
\r
495 T.KIND:=BEGKIND; (* 'BEGIN' *)
\r
497 IF PRKEY(3)<>5 THEN (* IF NOT 'END' *)
\r
502 V.LEFT:=CONSUB; (* FIRST PROGRAM *)
\r
504 writeln("pekch=", peekch);
\r
505 WHILE (PNC=59 OR PEEKCH = 36 ) (* LOOP FOR PROGRAMS *)
\r
508 IF PEEKCH = 36 THEN V.IDENT := 1 FI; (* UNIQUELY SUBSTITUTION *)
\r
510 V.RIGHT:=CONSUB; (* NEXT PROGRAM *)
\r
511 V.KIND:=SEMKIND; (* 'SEMICOLON' *)
\r
524 IF PRKEY(3)<>5 THEN CALL EXCEPTIONS(1) FI;
\r
526 T.IDENT:=ENDKIND; (* 'END' *)
\r
528 IF LL=LR THEN (* AFTER NESTING DO *)
\r
529 (* 'WHILE ETC ' PROGRAM ON *)
\r
530 T.RIGHT:=GEN_TREE; (* FORMULA BETA *)
\r
532 FI; (* OR TERM TAU *)
\r
536 (***************************************************************************)
\r
537 (* CONSTRUCT WHILE-ALFA-D0-K-OD PROGRAM *)
\r
539 UNIT PROG_WHILE:FUNCTION:TNODE;
\r
543 T.KIND:=WHIKIND; (* 'WHILE' *)
\r
544 T.LEFT:=GEN_TREE; (* ALFA *)
\r
545 CALL RETN(L-1); (* BACK BEFORE 'D' *)
\r
548 IF PRKEY(2)<>3 THEN CALL EXCEPTIONS(1) FI;
\r
549 V.KIND:=DOFKIND; (* 'DO' *)
\r
552 V.LEFT:=CONSUB; (* PROGRAM 'K' *)
\r
553 IF PRKEY(2)<>4 THEN CALL EXCEPTIONS(1) FI;
\r
554 V.IDENT:=ODFKIND; (* 'OD' *)
\r
556 IF LL=LR THEN (* AFTER NESTING DO *)
\r
557 (* 'WHILE ETC ' PROGRAM ON *)
\r
558 V.RIGHT:=GEN_TREE; (* FORMULA BETA *)
\r
560 FI; (* OR TERM TAU *)
\r
564 (***************************************************************************)
\r
565 (* SEARCH FOR PROGRAMS *)
\r
567 UNIT PROG:FUNCTION:TNODE;
\r
569 IF PRKEY(2)=1 THEN RESULT:=PROG_IF
\r
573 WHEN 8: RESULT:=PROG_BEGIN;
\r
574 WHEN 9: RESULT:=PROG_WHILE;
\r
575 OTHERWISE CALL RETN(L-5);
\r
580 (***************************************************************************)
\r
581 (* CONSTRUCT ITERATION EXISTENTIAL QUANTIFIER *)
\r
583 UNIT ITE_EX_Q:FUNCTION:TNODE;
\r
587 T.KIND:=ITEKIND; (* T.IDENT=0-IT MEANS *)
\r
588 C:=PNC; (* THAT RULE WAS NOT ACTIVE *)
\r
593 (***************************************************************************)
\r
594 (* CONSTRUCT ITERATION GREAT QUANTIFIER *)
\r
596 UNIT ITE_GR_Q:FUNCTION:TNODE;
\r
600 T.KIND:=IGQKIND; (* T.IDENT=0-IT MEANS *)
\r
601 C:=PNC; (* THAT RULE WAS NOT ACTIVE *)
\r
606 (*****************************************************************************)
\r
607 (* CONSTRUCT SUBSTITUTION AND READS NUMBER OF S *)
\r
609 UNIT CONSUB:FUNCTION:TNODE;
\r
614 IF C=83 ORIF C=115 ORIF C=81 ORIF C=113 THEN
\r
616 WHEN 83,115: T.KIND:=VARPROG;
\r
617 WHEN 81,113: T.KIND:=BVARPRO;
\r
619 CALL SEARCH_NUM(T.IDENT,TRUE);
\r
622 WHEN VARPROG : T.LEFT:=LIT_ARG;
\r
623 WHEN BVARPRO : CALL RETN(L-1);
\r
627 FOR I:=2 TO 4 (* IF NOT 'FI' AND NOT 'OD' *)
\r
628 DO (* AND NOT 'END' AND *)
\r
631 IF J<>0 THEN EXIT FI; (* NOT 'ELSE' THEN REPEAT *)
\r
633 IF (PNC<>59 AND PEEKCH<>36) THEN
\r
634 IF J=0 THEN T.RIGHT:=CONSUB ELSE CALL RETN(L-1); FI
\r
639 T:=LIT_ARG; (* IF NOT SUB THEN PROGRAM *)
\r
644 (***************************************************************************)
\r
645 (* READS INPUT LITERAL *)
\r
647 UNIT LIT_ARG : FUNCTION : TNODE;
\r
651 T:=NEW TNODE; (* RESERVE NODE *)
\r
652 IF LEN_SUB<>0 THEN
\r
654 C:=PNC; (* OMITED LEFT PAR *)
\r
660 WHEN 67,99 : CALL MAKE_TERM(T.KIND,T.IDENT,CN2KIND,TRUE);
\r
662 RETURN; (* CONSTANT 'C' *)
\r
663 WHEN 85 : T:=ITE_EX_Q;
\r
665 RETURN; (* ITEKIND 'U' *)
\r
666 WHEN 64 : T:=ITE_GR_Q;
\r
668 RETURN; (* IGQKIND '@' *)
\r
669 WHEN 88,120 : CALL MAKE_TERM(T.KIND,T.IDENT,VARKIND,TRUE);
\r
671 RETURN; (* VARIABLE 'X' *)
\r
672 WHEN 117 : CALL MAKE_TERM(T.KIND,T.IDENT,VRUKIND,TRUE);
\r
674 RETURN; (* VRUKIND 'u' *)
\r
675 WHEN 81,113 : CALL MAKE_TERM(T.KIND,T.IDENT,BVAKIND,TRUE);
\r
677 RETURN; (* BVAKIND 'Q'*)
\r
678 WHEN 83,115 : CALL MAKE_TERM(T.KIND,T.IDENT,SUBKIND,TRUE);
\r
680 RETURN; (* SUBKIND 'S' *)
\r
681 WHEN 61,33, (* EQUKIND '=' *)
\r
682 80,112 : CALL PRED(T.KIND,T.IDENT,TRUE);
\r
685 WHEN 71,103 : CALL MAKE_TERM ( T.KIND, T.IDENT, FUNKIND, TRUE );
\r
687 WHEN 35 : CALL MAKE_TERM ( T.KIND, T.IDENT, FN1KIND, TRUE );
\r
689 WHEN 70,102 : CALL MAKE_TERM ( T.KIND,T.IDENT,LOGKIND,TRUE );
\r
690 T.IDENT := 0; (* LOGICAL FALSE 'F' *)
\r
693 WHEN 84,116 : CALL MAKE_TERM ( T.KIND,T.IDENT,LOGKIND,TRUE );
\r
694 T.IDENT := 1; (* LOGICAL TRUE 'T' *)
\r
697 WHEN 48,49,50,51,52,53,54,55,56,57
\r
698 : CALL MAKE_TERM(T.KIND,T.IDENT,CNTKIND,FALSE);
\r
700 RETURN; (* DIGITS E.G. '2' *)
\r
701 WHEN 42,43,45,47,94 (* '*','+','-','/,'^' *)
\r
702 : CALL MAKE_TERM(T.KIND,T.IDENT,ARIKIND,TRUE);
\r
704 WHEN 37 : CALL MAKE_TERM ( T.KIND, T.IDENT, CN1KIND, TRUE );
\r
706 RETURN; (* FALSE CONSTANT *)
\r
707 WHEN 68,100 : CALL MAKE_TERM ( T.KIND, T.IDENT, SIGNTRM, TRUE );
\r
709 OTHERWISE CALL RETN(L-1);
\r
710 T:=PROG; (* PROGRAMS *)
\r
715 IF C=CHRLPA THEN (* LEFT PAR '(' *)
\r
716 C:=PNC; (* EXPECT SOME ARGUMENTS *)
\r
717 T.LEFT:=LIT_ARG; (* READ ARGUMENTS *)
\r
718 U:=T.LEFT; (* FIRST ON LEFT *)
\r
719 WHILE PNC=CHRCOM (* COMMA *)
\r
721 C:=PNC; (* LOOP FOR MORE *)
\r
722 WHILE U.RIGHT<>NONE (* OMIT PROGRAMS ON RIGHT *)
\r
726 U.RIGHT:=LIT_ARG; (* NEXT ON RIGHT *)
\r
730 IF C<>CHRRPA THEN CALL EXCEPTIONS(1) FI;(* EXPECT ')' *)
\r
739 (****************************************************************************)
\r
740 (* STOPS EXECUTION IF THERE IS AN ERROR *)
\r
742 UNIT EXCEPTIONS:PROCEDURE(N:INTEGER);
\r
745 WHEN 1:WRITELN("SYNTAX ERROR");
\r
746 WHEN 2:WRITELN("0/0");
\r
747 WHEN 3:WRITELN("DIVISION BY ZERO");
\r
748 WHEN 4:WRITELN("0^0");
\r
753 (***************************************************************************)
\r
754 (* PRINT FORMULA ON SCREEN AND TO FILE *)
\r
755 (***************************************************************************)
\r
757 (***************************************************************************)
\r
758 (* PRINT FORMULA ON SCREEN *)
\r
759 UNIT WR_FOR : PROCEDURE ( C : TNODE );
\r
761 IF C = NONE THEN RETURN FI;
\r
763 WHEN CONKIND : CALL WR_FOR_HELP ( C, '&' ); (* CONJUCTION *)
\r
764 WHEN DISKIND : CALL WR_FOR_HELP ( C, 'v' ); (* DISJUNCTION *)
\r
765 WHEN IMPKIND : CALL WR_FOR_HELP ( C, '=' ); (* IMPLICATION *)
\r
766 WHEN EQVKIND : CALL WR_FOR_HELP ( C, '<' ); (* EQUIVALENCE *)
\r
767 WHEN NEGKIND : CALL PUTCH ( 'n' );
\r
768 CALL WR_FOR ( C.LEFT ); (* NEGATION *)
\r
769 WHEN LOGKIND : IF C.IDENT = 0 THEN CALL PUTCH ( 'F' )
\r
770 ELSE CALL PUTCH ( 'T' ); (* LOGICAL CONSTANTS *)
\r
772 WHEN VARKIND : CALL PUTCH ( 'x' ); (* VARIABLE *)
\r
773 CALL PNUM ( C.IDENT ); (* AND ITS IDENTIFIER *)
\r
774 WHEN IGQKIND : CALL PUTCH ( '@' ); (* ITERATION GREAT QUANTIFIER *)
\r
775 CALL WR_FOR ( C.RIGHT );
\r
776 WHEN ITEKIND : CALL PUTCH ( 'U' ); (* EXISTENTIAL ITERATION QUANTIFIER *)
\r
777 CALL WR_FOR ( C.RIGHT );
\r
778 WHEN IFFKIND : CALL PUTCH ( 'I' ); (* IF *)
\r
779 CALL PUTCH ( 'F' );
\r
780 CALL WR_FOR ( C.LEFT ); (* ALFA *)
\r
781 CALL PUTCH ( 'T' ); (* THEN *)
\r
782 CALL PUTCH ( 'H' );
\r
783 CALL PUTCH ( 'E' );
\r
784 CALL PUTCH ( 'N' );
\r
785 CALL WR_FOR ( C.RIGHT.LEFT ); (* K *)
\r
786 IF C.RIGHT.RIGHT.KIND = ELSKIND THEN
\r
787 CALL PUTCH ( 'E' );
\r
788 CALL PUTCH ( 'L' );
\r
789 CALL PUTCH ( 'S' );
\r
790 CALL PUTCH ( 'E' ); (* ELSE *)
\r
791 CALL WR_FOR ( C.RIGHT.RIGHT.LEFT ); (* M *)
\r
793 CALL PUTCH ( 'F' ); (* FI *)
\r
794 CALL PUTCH ( 'I' );
\r
795 CALL WR_FOR ( C.RIGHT.RIGHT.RIGHT ); (* BETA *)
\r
796 WHEN BEGKIND : CALL PUTCH ( 'B' );
\r
797 CALL PUTCH ( 'E' );
\r
798 CALL PUTCH ( 'G' );
\r
799 CALL PUTCH ( 'I' );
\r
800 CALL PUTCH ( 'N' ); (* BEGIN *)
\r
801 CALL WR_FOR ( C.LEFT ); (* K *)
\r
802 CALL PUTCH ( 'E' );
\r
803 CALL PUTCH ( 'N' );
\r
804 CALL PUTCH ( 'D' ); (* END *)
\r
805 CALL WR_FOR ( C.RIGHT ); (* BETA *)
\r
806 WHEN SEMKIND : CALL WR_FOR ( C.LEFT ); (* K1 *)
\r
807 IF C.IDENT = 1 THEN
\r
808 CALL PUTCH ( '$' ) (* UNIQUELY SUBSTITUTION *)
\r
810 CALL PUTCH ( ';' ) (* SEMICOLON *)
\r
812 CALL WR_FOR ( C.RIGHT ); (* K2 *)
\r
813 WHEN WHIKIND : CALL PUTCH ( 'W' );
\r
814 CALL PUTCH ( 'H' );
\r
815 CALL PUTCH ( 'I' );
\r
816 CALL PUTCH ( 'L' );
\r
817 CALL PUTCH ( 'E' ); (* WHILE *)
\r
818 CALL WR_FOR ( C.LEFT ); (* ALFA *)
\r
819 CALL PUTCH ( 'D' );
\r
820 CALL PUTCH ( 'O' ); (* DO *)
\r
821 CALL WR_FOR ( C.RIGHT.LEFT );(* K *)
\r
822 CALL PUTCH ( 'O' );
\r
823 CALL PUTCH ( 'D' ); (* OD *)
\r
824 CALL WR_FOR ( C.RIGHT.RIGHT ); (* BETA *)
\r
825 WHEN QUAKIND : CALL PUTCH ( 'A' ); (* GREAT QUANTIFIER *)
\r
826 CALL PUTCH ( 'x' ); (* VARIABLE *)
\r
827 CALL PNUM ( C.IDENT ); (* ITS NUMBER *)
\r
828 CALL WR_FOR ( C.LEFT ); (* ALFA *)
\r
833 FN1KIND : CASE C.KIND
\r
834 WHEN EQUKIND : CALL PUTCH ( '=' );
\r
835 WHEN LITKIND : CALL PUTCH ( 'P' );
\r
836 WHEN FUNKIND : CALL PUTCH ( 'G' );
\r
837 WHEN LT1KIND : CALL PUTCH ( '!' );
\r
838 WHEN FN1KIND : CALL PUTCH ( '#' );
\r
839 ESAC; (* PREDICATE OR FUNCTION *)
\r
840 CALL PNUM ( C.IDENT );
\r
841 IF C.LEFT = NONE THEN RETURN FI;
\r
842 CALL PUTCH ( '(' );
\r
846 CALL WR_FOR ( C ); (* ARGUMENT *)
\r
847 C := C.RIGHT; (* TAKE NEXT ARGUMENT *)
\r
848 IF C <> NONE THEN CALL PUTCH ( ',' ) FI;
\r
850 CALL PUTCH ( ')' );
\r
851 WHEN CNTKIND : CALL PNUM ( C.IDENT + 1 ); (* NUMERIC CONSTANT *)
\r
852 WHEN CN1KIND : CALL PUTCH ( '%' ); (* FALSE CONSTANT *)
\r
853 CALL PNUM ( C.IDENT + 1 );
\r
854 WHEN CN2KIND : CALL PUTCH ( 'C' ); (* CONSTANT OF THE FORM 'C' *)
\r
855 CALL PNUM ( C.IDENT );
\r
856 WHEN ARIKIND : CALL PUTCH ( CHR ( C.IDENT ) ); (* ARITHMETIC OPERATION *)
\r
857 IF C.LEFT.RIGHT = NONE THEN
\r
858 CALL WR_FOR ( C.LEFT );
\r
861 CALL PUTCH ( '(' );
\r
862 CALL WR_FOR ( C.LEFT );
\r
863 CALL PUTCH ( ',' );
\r
864 CALL WR_FOR ( C.LEFT.RIGHT );
\r
865 CALL PUTCH ( ')' );
\r
866 WHEN VRUKIND : CALL PUTCH ( 'u' ); (* SPECIAL KIND OF VARIABLE *)
\r
867 CALL PNUM ( C.IDENT );
\r
868 WHEN BVAKIND : CALL PUTCH ( 'Q' ); (* LOGICAL VARIABLE *)
\r
869 CALL PNUM ( C.IDENT );
\r
870 WHEN SUBKIND : CALL PUTCH ( 'S' ); (* VARABLE TO BE SUBSTITUTED ON *)
\r
871 CALL PNUM ( C.IDENT );
\r
873 BVARPRO : IF C.KIND = VARPROG THEN
\r
874 CALL PUTCH ( 'S' ) (* SUBSTITUTION S:= *)
\r
876 CALL PUTCH ( 'Q' ); (* Q:= *)
\r
878 CALL PNUM ( C.IDENT );
\r
879 CALL PUTCH ( ':' );
\r
880 CALL PUTCH ( '=' );
\r
881 CALL WR_FOR ( C.LEFT ); (* TAU OR ALFA*)
\r
882 IF C.RIGHT = NONE THEN RETURN FI;
\r
883 CALL PUTCH ( '(' ); (* NEXT FORMULA *)
\r
884 CALL WR_FOR ( C.RIGHT );
\r
885 CALL PUTCH ( ')' );
\r
886 WHEN SIGNTRM : CALL PUTCH ( 'D' ); (* DUMKIND *)
\r
887 CALL PNUM ( C.IDENT );
\r
891 (***************************************************************************)
\r
892 (* HELP FOR WR_FOR PROCEDURE *)
\r
894 UNIT WR_FOR_HELP : PROCEDURE ( C : TNODE, CH : CHARACTER );
\r
896 CALL PUTCH ( '(' );
\r
897 CALL WR_FOR ( C.LEFT );
\r
900 WHEN '=' : CALL PUTCH ( '>' );
\r
901 WHEN '<' : CALL PUTCH ( '=' );
\r
902 CALL PUTCH ( '>' );
\r
904 CALL WR_FOR ( C.RIGHT );
\r
905 CALL PUTCH ( ')' );
\r
908 (***************************************************************************)
\r
909 (* ADDITIONAL PROCEDURES AND FUNCTIONS *)
\r
910 (***************************************************************************)
\r
912 (***************************************************************************)
\r
913 (* GIVES A VALUE OF CHARACTER *)
\r
915 UNIT VAL:FUNCTION(A:CHARACTER):INTEGER;
\r
920 (*****************************************************************************)
\r
921 (* PRINTS ALL TREES IN A SEQUENT *)
\r
923 UNIT SHOW_SEQ : PROCEDURE ( A : SEQUENT );
\r
927 CALL WR_FOR ( A.PLEAF ); (* SHOW_TREE ( A.PLEAF); *)
\r
929 CALL WR_FOR ( A.LLEAF ); (* SHOW_TREE ( A.LLEAF ); *)
\r
931 CALL SHOW_SEQ ( A.NEXT );
\r
935 (*****************************************************************************)
\r
938 UNIT SHOW_TREE : PROCEDURE ( A : TNODE );
\r
941 WRITELN(A.KIND,"=K",A.IDENT,"=I");
\r
942 CALL SHOW_TREE(A.LEFT);
\r
943 CALL SHOW_TREE(A.RIGHT);
\r
947 (****************************************************************************)
\r
948 (* MOVE UP I TNODES FROM RIGHT (P=1) OR LEFT (P=0) SIDE *)
\r
950 UNIT LIFT : PROCEDURE ( T : TNODE; I, P : INTEGER );
\r
956 WHEN 1: A := T.RIGHT;
\r
957 WHEN 0: A := T.LEFT;
\r
960 T.IDENT := A.IDENT;
\r
961 T.RIGHT := A.RIGHT;
\r
968 (****************************************************************************)
\r
969 (* MOVE UP POINTER *)
\r
971 UNIT LIFT_PNTR : PROCEDURE ( INOUT M1 : POINTER );
\r
976 CALL ERASE_SEQ ( M1.NEXT );
\r
977 IF M1.DOWN <> NONE THEN
\r
978 M1.NEXT := M1.DOWN.NEXT;
\r
979 M1.DOWN := M1.DOWN.DOWN;
\r
987 (****************************************************************************)
\r
988 (* MOVE LAST NON-EMPTY RIGHT OR LEFT TNODE OF A SEQUENT TO THE BEGINNING *)
\r
990 UNIT MOVE : PROCEDURE ( INOUT M : POINTER; P , R : INTEGER);
\r
991 VAR HEAD1,TAIL : SEQUENT,
\r
994 HEAD1 := NEW SEQUENT;
\r
995 TAIL := LAST ( M , P );
\r
996 IF P=1 THEN R := R + 1 FI;
\r
999 WHEN 0:HEAD1.LLEAF:=TAIL.LLEAF; (* LEFT TO LEFT *)
\r
1000 TAIL.LLEAF:=NONE ; (* P=0,R=0 *)
\r
1001 WHEN 3:HEAD1.PLEAF:=TAIL.PLEAF; (* RIGHT TO RIGHT *)
\r
1002 TAIL.PLEAF:=NONE; (* P=1,R=1 *)
\r
1003 WHEN 1:HEAD1.PLEAF:=TAIL.LLEAF; (* LEFT TO RIGHT *)
\r
1004 TAIL.LLEAF:=NONE; (* P=0,R=1 *)
\r
1005 WHEN 2:HEAD1.LLEAF:=TAIL.PLEAF; (* RIGHT TO LEFT *)
\r
1006 TAIL.PLEAF:=NONE; (* P=1,R=0 *)
\r
1008 HEAD1.NEXT := M.NEXT;
\r
1012 (****************************************************************************)
\r
1013 (* GIVES THE LAST NON EMPTY P-SIDE SEQUENT *)
\r
1015 UNIT LAST:FUNCTION(M:POINTER;P:INTEGER):SEQUENT;
\r
1016 VAR HEAD1:SEQUENT;
\r
1018 IF M=NONE ORIF M.NEXT=NONE THEN
\r
1024 IF HEAD1.PLEAF<>NONE THEN RESULT:=HEAD1 FI;
\r
1025 WHILE HEAD1.NEXT<>NONE
\r
1027 IF HEAD1.NEXT.PLEAF<>NONE THEN
\r
1028 RESULT:=HEAD1.NEXT
\r
1034 IF HEAD1.LLEAF<>NONE THEN RESULT:=HEAD1 FI;
\r
1035 WHILE HEAD1.NEXT<>NONE
\r
1037 IF HEAD1.NEXT.LLEAF<>NONE THEN
\r
1038 RESULT:=HEAD1.NEXT;
\r
1045 (****************************************************************************)
\r
1046 (* GO TO THE END OF A PROGRAM WITH TAU *)
\r
1048 UNIT END_OF_PRG : PROCEDURE ( INOUT C : TNODE );
\r
1050 IF C = NONE THEN RETURN FI;
\r
1051 WHILE C.RIGHT <> NONE
\r
1057 (*****************************************************************************)
\r
1058 (* GO TO THE END OF PROGRAM *)
\r
1060 UNIT END_OF_P : PROCEDURE ( INOUT C : TNODE );
\r
1063 IF C = NONE THEN RETURN FI;
\r
1064 WHILE C.RIGHT <> NONE
\r
1072 (*****************************************************************************)
\r
1073 (* GO TO THE END OF AXIOMS LIST *)
\r
1075 UNIT END_OF_AX : PROCEDURE ( INOUT AX1 : LIST_AXIOMS );
\r
1077 IF AX = NONE THEN RETURN FI;
\r
1079 WHILE AX1.NEXT <> NONE
\r
1085 (*****************************************************************************)
\r
1086 (* GO TO THE END OF POINTERS *)
\r
1088 UNIT END_OF_M : PROCEDURE ( INOUT M : POINTER , A : SEQUENT );
\r
1091 IF M = NONE THEN RETURN FI;
\r
1093 WHILE M.DOWN <> NONE
\r
1097 M1 := NEW POINTER;
\r
1099 CALL SQUEEZE ( M1 , 0 );
\r
1100 CALL SQUEEZE ( M1 , 1 );
\r
1102 CALL CUT_SEQ ( M1.NEXT );
\r
1106 (*****************************************************************************)
\r
1107 (* ERASE A TREE *)
\r
1109 UNIT ERASE : PROCEDURE ( A : TNODE );
\r
1112 CALL ERASE ( A.LEFT ); (* GO TO LAST LEFT TNODE *)
\r
1113 CALL ERASE ( A.RIGHT ); (* GO TO LAST RIGHT TNODE *)
\r
1114 KILL ( A ); (* REMOVE TNODE *)
\r
1118 (*****************************************************************************)
\r
1119 (* ERASE A SEQUENT *)
\r
1121 UNIT ERASE_SEQ : PROCEDURE ( A : SEQUENT );
\r
1124 CALL ERASE_SEQ ( A.NEXT ); (* GO TO THE LAST SEQUENT *)
\r
1125 CALL ERASE ( A.LLEAF ); (* REMOVE LEFT TREE *)
\r
1126 CALL ERASE ( A.PLEAF ); (* REMOVE RIGHT TREE *)
\r
1127 KILL ( A ); (* REMOVE SEQUENT *)
\r
1131 (*****************************************************************************)
\r
1132 (* ERASE AN EMPTY POINTER, I.E. LINKED TO THE EMPTY FORMULA ' |- ' *)
\r
1134 UNIT ERASE_PNTR : PROCEDURE ( INOUT M1 : POINTER );
\r
1136 IF M1 = NONE THEN RETURN FI; (* SEQUENT IS EMPTY *)
\r
1137 CALL LIFT_PNTR ( M1 ); (* REMOVE POINTER *)
\r
1138 CALL ERASE_PNTR ( M1 ); (* REMOVE NEXT POINTER *)
\r
1141 (*****************************************************************************)
\r
1142 (* REMOVE LIST OF AXIOMS *)
\r
1144 UNIT ERASE_AX : PROCEDURE ( AX : LIST_AXIOMS );
\r
1146 IF AX = NONE THEN RETURN FI;
\r
1147 CALL ERASE_AX ( AX.NEXT );
\r
1148 CALL ERASE ( AX.AXIOM );
\r
1151 (*****************************************************************************)
\r
1152 (* GO TO THE END OF SUBSTITUTION *)
\r
1154 UNIT END_OF_S : PROCEDURE ( INOUT A , B : TNODE );
\r
1156 IF A = NONE THEN RETURN FI;
\r
1157 WHILE A.KIND=VARPROG OR A.KIND=BVARPRO
\r
1161 IF A = NONE THEN EXIT FI ;
\r
1165 (****************************************************************************)
\r
1166 (* MAKES A COPY OF TNODE TREE *)
\r
1168 UNIT COPYTNODE : FUNCTION ( X : TNODE ) : TNODE;
\r
1171 RESULT := COPY ( X );
\r
1172 RESULT.LEFT := COPYTNODE ( X.LEFT );
\r
1173 RESULT.RIGHT := COPYTNODE ( X.RIGHT );
\r
1177 (****************************************************************************)
\r
1178 (* MAKES A COPY OF ALL SEQUENTS IN A TREE , INCLUDING TNODES *)
\r
1180 UNIT COPYSEQUENT : FUNCTION ( X : SEQUENT ) : SEQUENT;
\r
1182 IF X <> NONE THEN
\r
1183 RESULT := COPY ( X );
\r
1184 RESULT.PLEAF := COPYTNODE ( X.PLEAF );
\r
1185 RESULT.LLEAF := COPYTNODE ( X.LLEAF );
\r
1186 RESULT.NEXT := COPYSEQUENT ( X.NEXT );
\r
1190 (*****************************************************************************)
\r
1191 (* UPDATE THE GREATEST NUMBER OF VARIABLE *)
\r
1193 UNIT LAST1_X : PROCEDURE ( A : TNODE );
\r
1195 IF A=NONE THEN RETURN FI;
\r
1196 IF A.KIND=VARKIND THEN
\r
1197 IF LAST_X < A.IDENT THEN LAST_X := A.IDENT FI;
\r
1199 CALL LAST1_X ( A.LEFT );
\r
1200 CALL LAST1_X ( A.RIGHT );
\r
1203 (****************************************************************************)
\r
1204 (* LOOKING FOR THE GREATEST BVARPRO SUBSTITUTION *)
\r
1206 UNIT LAST1_Q:PROCEDURE(A:TNODE);
\r
1208 IF A=NONE THEN RETURN FI;
\r
1209 IF A.KIND=BVARPRO THEN
\r
1210 IF LAST_Q < A.IDENT THEN LAST_Q:=A.IDENT FI;
\r
1212 CALL LAST1_Q(A.RIGHT);
\r
1213 CALL LAST1_Q(A.LEFT);
\r
1216 (****************************************************************************)
\r
1217 (* UPDATE THE GREATEST NUMBER OF VARPROG *)
\r
1219 UNIT LAST1_S : PROCEDURE ( A : TNODE );
\r
1221 IF A=NONE THEN RETURN FI;
\r
1222 IF A.KIND=VARPROG THEN
\r
1223 IF LAST_S < A.IDENT THEN LAST_S := A.IDENT FI;
\r
1225 CALL LAST1_S ( A.LEFT );
\r
1226 CALL LAST1_S ( A.RIGHT );
\r
1229 (****************************************************************************)
\r
1230 (* UPDATE THE GREATEST NUMBER OF VARKIND IN THE DIFINITION TREE AND CHANGE IT
\r
1233 UNIT LAST2_S : FUNCTION ( A1 : TNODE, I : INTEGER ) : INTEGER;
\r
1237 A := M1.FUN_REL.LEFT;
\r
1240 IF K=1 THEN A := A.LEFT
\r
1241 ELSE A := A.RIGHT;
\r
1244 IF A.KIND=SUBKIND THEN RESULT := A.IDENT
\r
1245 ELSE LAST_S := LAST_S+1;
\r
1247 CALL RENAME ( A1,A.KIND,A.IDENT );
\r
1251 (****************************************************************************)
\r
1252 (* CHANGE VARKIND TO SUBKIND RESPECTIVELY *)
\r
1254 UNIT RENAME : PROCEDURE ( A1 : TNODE, I,J : INTEGER );
\r
1256 IF A1=NONE THEN RETURN FI;
\r
1257 IF A1.KIND=I AND A1.IDENT=J THEN A1.KIND := SUBKIND;
\r
1258 A1.IDENT := LAST_S
\r
1260 CALL RENAME ( A1.LEFT,I,J );
\r
1261 CALL RENAME ( A1.RIGHT,I,J );
\r
1264 (****************************************************************************)
\r
1265 (* REMOVE ALL EMPTY SEQUENTS AFTER CALLING SQUEEZE PROCEDURE *)
\r
1267 UNIT CUT_SEQ : PROCEDURE ( A : SEQUENT );
\r
1269 IF A <> NONE THEN CALL CUT_SEQ ( A.NEXT ) ELSE RETURN FI; (* GO TO THE LAST
\r
1271 IF A.PLEAF = NONE AND A.LLEAF = NONE THEN KILL ( A ) FI; (* WHEN EMPTY
\r
1275 (****************************************************************************)
\r
1276 (* FIND A CONNECTIVE NUMBER 'R' *)
\r
1278 UNIT FINDCONN : FUNCTION ( A : SEQUENT , R , P : INTEGER ) : TNODE;
\r
1281 IF A = NONE THEN RETURN FI;
\r
1283 WHEN 1: IF A.PLEAF = NONE THEN RETURN FI;
\r
1285 CALL FUNCTOR ( R , B );
\r
1287 WHEN 0: IF A.LLEAF = NONE THEN RETURN FI;
\r
1289 CALL FUNCTOR ( R , B );
\r
1294 (****************************************************************************)
\r
1295 (* SEARCH FOR A FUNCTOR *)
\r
1297 UNIT FUNCTOR : PROCEDURE ( R : INTEGER ; INOUT B : TNODE );
\r
1300 IF B.KIND = BEGKIND ANDIF B.LEFT <> NONE ANDIF B.LEFT.IDENT = 1 ANDIF
\r
1301 B.LEFT.KIND = SEMKIND THEN
\r
1304 WHILE B.KIND = VARPROG OR B.KIND = BVARPRO
\r
1308 IF B.KIND <> R THEN B := NONE FI;
\r
1311 (****************************************************************************)
\r
1312 (* LOOK FOR MORE THAN ONE EQUALITIES IN A SEQUENT OF TYPE U=TERM *)
\r
1314 UNIT SEARCH_U : FUNCTION ( A : SEQUENT ) : BOOLEAN;
\r
1319 IF A.PLEAF <> NONE THEN
\r
1320 IF A.PLEAF.KIND = EQUKIND ANDIF
\r
1321 ( A.PLEAF.LEFT.KIND = VRUKIND OR A.PLEAF.LEFT.RIGHT.KIND = VRUKIND ) THEN
\r
1333 (****************************************************************************)
\r
1334 (* CHECK WHETHER THERE IS IN A SEQUENT THE DEFINITION SYMBOL LIKE: FUNCTION,
\r
1335 LITERAL ; OR PROGRAM *)
\r
1337 UNIT CHECK_L_F_P : FUNCTION ( A : SEQUENT ) : BOOLEAN;
\r
1339 IF A <> NONE AND NOT ALFA THEN
\r
1340 ALFA := CHECK_L_F_P_TN ( A.PLEAF ) OR CHECK_L_F_P_TN ( A.LLEAF );
\r
1341 RESULT := ALFA OR CHECK_L_F_P ( A.NEXT );
\r
1345 (*****************************************************************************)
\r
1346 (* CHECK WHETHER THERE IS IN A TNODE THE DEFINITION SYMBOL LIKE: FUNCTION,
\r
1347 LITERAL ; OR PROGRAM *)
\r
1349 UNIT CHECK_L_F_P_TN : FUNCTION ( C : TNODE ) : BOOLEAN;
\r
1350 VAR BETA : BOOLEAN ;
\r
1353 BETA := ( C.KIND > 2 AND C.KIND < 23 ) OR C.KIND = LT1KIND OR
\r
1354 C.KIND = FN1KIND OR C.KIND = 4;
\r
1355 RESULT := BETA OR CHECK_L_F_P_TN ( C.LEFT ) OR CHECK_L_F_P_TN ( C.RIGHT );
\r
1359 (****************************************************************************)
\r
1360 (* WRITES A CHARACTER TO FILE *)
\r
1362 UNIT PUTCH : PROCEDURE ( A : CHARACTER );
\r
1364 IF CHARSH >= LINLNG THEN
\r
1369 CHARSH := CHARSH + 1
\r
1372 (****************************************************************************)
\r
1375 (****************************************************************************)
\r
1376 (* PRIMARY RULES AND FIRSTLY PROCEDURES AND FUNCTIONS APPLIED IN THE TREE *)
\r
1377 (****************************************************************************)
\r
1379 (****************************************************************************)
\r
1380 (* REPLACE IN SEQUENT A ALL FUNKIND WITH NUMBER N TO FN1KIND WITH NUMBER N *)
\r
1382 UNIT REP_F_SEQ : PROCEDURE ( A : SEQUENT , N : INTEGER );
\r
1384 IF A = NONE THEN RETURN FI;
\r
1385 CALL REP_FUN_N ( A.LLEAF , N );
\r
1386 CALL REP_FUN_N ( A.PLEAF , N );
\r
1387 CALL REP_F_SEQ ( A.NEXT , N );
\r
1390 (****************************************************************************)
\r
1391 (* REPLACE IN TNODE C ALL FUNKIND WITH NUMBER N TO FN1KIND WITH NUMBER N *)
\r
1393 UNIT REP_FUN_N : PROCEDURE ( C : TNODE , N : INTEGER );
\r
1395 IF C = NONE THEN RETURN FI;
\r
1396 IF C.KIND=FUNKIND AND C.IDENT = N THEN C.KIND := FN1KIND FI;
\r
1397 CALL REP_FUN_N ( C.LEFT , N );
\r
1398 CALL REP_FUN_N ( C.RIGHT , N );
\r
1401 (****************************************************************************)
\r
1402 (* REPLACE IN TNODE C ALL FUNKIND TO FN1KIND *)
\r
1404 UNIT REP_FUN : PROCEDURE ( C : TNODE );
\r
1406 IF C = NONE THEN RETURN FI;
\r
1407 IF C.KIND = FUNKIND THEN C.KIND := FN1KIND FI;
\r
1408 CALL REP_FUN ( C.LEFT );
\r
1409 CALL REP_FUN ( C.RIGHT );
\r
1412 (****************************************************************************)
\r
1413 (* REPLACE ALL LITKIND WITH NUMBER N IN SEQUENT A TO LT1KIND *)
\r
1415 UNIT REP_L_SEQ : PROCEDURE ( A :SEQUENT , N :INTEGER );
\r
1417 IF A = NONE THEN RETURN FI;
\r
1418 CALL REP_LIT_N ( A.PLEAF , N );
\r
1419 CALL REP_LIT_N ( A.LLEAF , N );
\r
1420 CALL REP_L_SEQ ( A.NEXT , N );
\r
1423 (****************************************************************************)
\r
1424 (* REPLACE ALL LITKIND IN TNODE C TO LT1KIND *)
\r
1426 UNIT REP_LIT : PROCEDURE ( C : TNODE );
\r
1428 IF C = NONE THEN RETURN FI;
\r
1429 IF C.KIND = LITKIND THEN C.KIND := LT1KIND FI;
\r
1430 CALL REP_LIT ( C.LEFT );
\r
1431 CALL REP_LIT ( C.RIGHT );
\r
1434 (****************************************************************************)
\r
1435 (* REPLACE ALL LITKIND WITH NUMBER N IN TNODE C TO LT1KIND *)
\r
1437 UNIT REP_LIT_N : PROCEDURE ( C : TNODE , N : INTEGER );
\r
1439 IF C = NONE THEN RETURN FI;
\r
1440 IF C.KIND = LITKIND AND C.IDENT = N THEN C.KIND := LT1KIND FI;
\r
1441 CALL REP_LIT_N ( C.LEFT , N );
\r
1442 CALL REP_LIT_N ( C.RIGHT , N );
\r
1445 (*****************************************************************************)
\r
1446 (* REPLACE DEFINITION SYMBOL LIKE : FUNKIND AND LITKIND INTO FN1KIND AND
\r
1447 LT1KIND RESPECTIVELY *)
\r
1449 UNIT REP_F_L : PROCEDURE ( M3 : DEF );
\r
1454 CASE M3.FUN_REL.KIND
\r
1455 WHEN EQUKIND : CALL REP_FUN_N ( M2.FUN_REL , M2.FUN_REL.LEFT.IDENT );
\r
1456 (* REPLACE FUNKIND WITH PROPER NUMBERS *)
\r
1457 (* INTO FN1KIND IN A DEFINITION TREE *)
\r
1458 CALL REP_F_SEQ ( M.NEXT , M2.FUN_REL.LEFT.IDENT );
\r
1459 (* DO THE SAME BUT IN DATA TREE *)
\r
1460 WHEN EQVKIND : CALL REP_LIT_N ( M2.FUN_REL , M2.FUN_REL.LEFT.IDENT );
\r
1461 (* REPLACE LITKIND WITH PROPER NUMBERS *)
\r
1462 (* INTO LT1KIND IN A DEFINITION TREE *)
\r
1463 CALL REP_L_SEQ ( M.NEXT , M2.FUN_REL.LEFT.IDENT );
\r
1464 (* DO THE SAME BUT IN DATA TREE *)
\r
1466 IF M2 = M3 THEN EXIT FI;
\r
1471 (*****************************************************************************)
\r
1472 (* USE THE DEFINITION OF FUNCTION *)
\r
1474 UNIT RULEDF_F : PROCEDURE ( M : POINTER, P : INTEGER, F_NUMBER : INTEGER );
\r
1475 VAR A , A1 , ALR , C , B1 : TNODE,
\r
1482 IF B=NONE ORIF B.PLEAF=NONE THEN RETURN FI;
\r
1485 WHILE A.KIND <> EQUKIND
\r
1487 IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;
\r
1491 IF FOUND_F ( B.PLEAF , B.PLEAF , A , ALR , ALFA , F_NUMBER ) THEN
\r
1493 IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;
\r
1497 IF B=NONE ORIF B.LLEAF=NONE THEN RETURN FI;
\r
1500 WHILE A.KIND <> EQUKIND
\r
1502 IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;
\r
1506 IF FOUND_F ( B.LLEAF , B.LLEAF , A , ALR , ALFA , F_NUMBER ) THEN
\r
1509 IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;
\r
1514 C := ALR.RIGHT; (* C STORES RIGHT SIDE OF *)
\r
1515 (* OPERATION CONTAINING FUNCTION *)
\r
1516 A1 := COPYTNODE ( M1.FUN_REL.LEFT.RIGHT ); (* REMEMBER K -TAU *)
\r
1517 IF ALR.LEFT = NONE THEN (* IF THERE IS NO ARGUMENT *)
\r
1521 CALL MAKE_SUB ( ALR.LEFT , A1 , B1 ); (* ALR.LEFT REFERS TO FIRST ARG *)
\r
1522 CALL LIFT ( B1 , 1 , 0 );
\r
1524 CALL END_OF_P ( A1 ); (* A1 REFERS TO THE END OF PROGRAM *)
\r
1526 IF A.LEFT = ALR THEN (* FUNCTION IS ON LEFT *)
\r
1528 A.LEFT := A1.RIGHT (* JOIN TAU *)
\r
1529 ELSE (* FUNCTION IS ON RIGHT *)
\r
1531 A.RIGHT := A1.RIGHT; (* JOIN TAU *)
\r
1533 A1.RIGHT.RIGHT := C; (* JOIN U OR SOMETHING ELSE *)
\r
1536 WHEN 1 : A1 := B.PLEAF; (* MOVE '=' BEYOND PROGRAM *)
\r
1537 B.PLEAF := B1; (* ON RIGHT *)
\r
1538 CALL END_OF_PRG ( B1 );
\r
1540 WHEN 0 : A1 := B.LLEAF; (* OR ON LEFT SIDE *)
\r
1542 CALL END_OF_PRG ( B1 );
\r
1547 (*****************************************************************************)
\r
1548 (* SEARCH FUNCTION FN1KIND IN A TREE TO BE SUBSTITUTED ON *)
\r
1550 UNIT FOUND_F : FUNCTION ( B , B1 : TNODE ; INOUT C , D : TNODE , ALFA : BOOLEAN ;
\r
1551 F_NUMBER : INTEGER ) : BOOLEAN;
\r
1554 IF B.KIND = FN1KIND AND B.IDENT = F_NUMBER THEN
\r
1563 RESULT := FOUND_F ( B.LEFT , B , C , D , ALFA , F_NUMBER )
\r
1564 OR FOUND_F ( B.RIGHT , B , C , D , ALFA , F_NUMBER )
\r
1569 (****************************************************************************)
\r
1570 (* MAKE THE SUBSTITUTION *)
\r
1572 UNIT MAKE_SUB:PROCEDURE ( D , A1 , A : TNODE );
\r
1576 IF D.RIGHT = NONE THEN (* ONLY ONE ARGUMENT *)
\r
1579 E.KIND := VARPROG;
\r
1581 E.IDENT :=LAST2_S ( A1 , 1 );
\r
1585 F := NEW TNODE; (* MORE THAN ONE ARGUMENTS *)
\r
1586 F.KIND := BEGKIND;
\r
1587 F.IDENT := ENDKIND;
\r
1589 DO (* VIEW ALL ARGUMENTS AND *)
\r
1590 (* MAKE RELEVANT SUBSTITUTION *)
\r
1591 (* CREATE SUBSTITUTION CELLS *)
\r
1593 (* AND JOIN THEM- XI:=TI *)
\r
1595 G.KIND := SEMKIND;
\r
1596 G.IDENT := 1; (* SIGN THAT SUBSTITUTION *)
\r
1597 (* SHOULD BE DONE SIMULTANEOUSLY *)
\r
1600 E.KIND := VARPROG;
\r
1601 E.LEFT := D; (* ASSOCIATE VARIABLE WITH ITS term XI:=TI *)
\r
1602 E.RIGHT := D.RIGHT;
\r
1612 E.IDENT := LAST2_S ( A1 , I ); (* ASSIGN VARPROG NEW NUMBER
\r
1613 AND UPDATE LIST OF VARPROG'S *)
\r
1618 CALL LIFT ( G , 1 , 0 );
\r
1622 (****************************************************************************)
\r
1623 (* USE A DEFINITION OF RELATION *)
\r
1625 UNIT RULEDF_L : PROCEDURE ( M : POINTER , P : INTEGER , N : INTEGER );
\r
1626 VAR A,A1,D : TNODE,
\r
1632 IF B=NONE ORIF B.PLEAF=NONE THEN RETURN FI;
\r
1634 WHILE ( A.KIND <> LT1KIND OR A.IDENT <> N ) AND A.KIND <> EQVKIND
\r
1636 IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;
\r
1641 IF B=NONE ORIF B.LLEAF=NONE THEN RETURN FI;
\r
1643 WHILE ( A.KIND <> LT1KIND OR A.IDENT <> N ) AND A.KIND <> EQVKIND
\r
1645 IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;
\r
1650 IF A.KIND = EQVKIND THEN A := A.LEFT FI;
\r
1651 D := A.LEFT; (* FIRST ARGUMENT *)
\r
1652 A1 := COPY ( M1.FUN_REL.RIGHT ); (* REMEMBER K-ALFA *)
\r
1655 CALL LIFT ( A , 1 , 1 );
\r
1659 CALL MAKE_SUB ( D , A1 , A );
\r
1661 WHEN 0 : CALL LIFT ( B.LLEAF.LEFT, 1, 0 );
\r
1662 CALL SWEEP ( B.LLEAF );
\r
1663 WHEN 1 : CALL LIFT ( B.PLEAF.LEFT, 1, 0 );
\r
1664 CALL SWEEP ( B.PLEAF );
\r
1667 WHEN 0 : A := B.LLEAF;
\r
1668 WHEN 1 : A := B.PLEAF;
\r
1670 IF A.LEFT.KIND = BEGKIND ANDIF A.LEFT.LEFT <> NONE ANDIF
\r
1671 A.LEFT.LEFT.KIND = SEMKIND ANDIF A.LEFT.LEFT.IDENT = 1 THEN
\r
1672 D := A.LEFT; (* MOVE OUT PARALLEL *)
\r
1673 A.LEFT := D.RIGHT; (* SUBSTITUTION BEYOND *)
\r
1674 D.RIGHT := A; (* EQUIVALENCE *)
\r
1676 WHEN 0 : B.LLEAF := D;
\r
1677 WHEN 1 : B.PLEAF := D;
\r
1683 (*****************************************************************************)
\r
1686 (*****************************************************************************)
\r
1688 (*****************************************************************************)
\r
1690 (****************************************************************************)
\r
1691 (* THROWING AWAY THE SEQUENCE OF SEQUENTS INCLUDING 0 ON LEFT SIDE
\r
1692 OR 1 ON RIGHT SIDE *)
\r
1694 UNIT THROW_RUBBISH : PROCEDURE ( M : POINTER );
\r
1697 IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;
\r
1701 IF A.PLEAF<>NONE THEN
\r
1702 IF A.PLEAF.IDENT=1 ANDIF A.PLEAF.KIND=LOGKIND THEN
\r
1703 CALL ERASE_SEQ ( M.NEXT ); (* IF THERE IS TRUE ON RIGHT *)
\r
1704 EXIT; (* SIDE, THEN REMOVE ALL SEQUENTS *)
\r
1706 IF DEF_LIT = 1 ANDIF A.PLEAF.KIND = LOGKIND ANDIF A.PLEAF.IDENT = 0 THEN
\r
1710 IF A.LLEAF<>NONE THEN
\r
1711 IF A.LLEAF.IDENT=0 ANDIF A.LLEAF.KIND=LOGKIND THEN
\r
1712 CALL ERASE_SEQ ( M.NEXT ); (* IF THERE IS FALSE ON LEFT *)
\r
1713 EXIT; (* SIDE, THEN REMOVE ALL SEQUENTS *)
\r
1715 IF DEF_LIT = 1 ANDIF A.LLEAF.KIND = LOGKIND ANDIF A.LLEAF.IDENT = 1 THEN
\r
1719 A := A.NEXT; (* OTHERWISE GO ON FURTHER *)
\r
1721 END THROW_RUBBISH;
\r
1723 (****************************************************************************)
\r
1724 (* CALCULATE STANDARD FUNCTIONS *,+,-,^,/ *)
\r
1726 UNIT RULEVAL : PROCEDURE ( A:TNODE; INOUT ALFA:BOOLEAN );
\r
1727 VAR BETA : BOOLEAN,
\r
1731 IF A=NONE THEN RETURN FI;
\r
1732 IF A.KIND=ARIKIND THEN (* MUST BEGIN WITH FUNCTOR *)
\r
1733 CALL CHECKCHAR ( A.LEFT , BETA ); (* CHECK WHETHER IN THE FOLLOWING
\r
1734 TREE THERE ARE ONLY STANDARD
\r
1735 FUNCTORS AND DIGITS *)
\r
1736 IF BETA THEN (* IF YES *)
\r
1738 CALL FUNCHECK ( A , BETA );
\r
1739 A.IDENT := COUNT ( A ) ; (* COUNT THIS EXPRESSION *)
\r
1743 A.KIND := CNTKIND;
\r
1745 CALL ERASE ( A.LEFT ); (* WHEN DONE REMOVE IT *)
\r
1748 ELSE (* MAKE SPECIAL ARITHMETIC *)
\r
1749 BETA := TRUE; (* OPERATIONS LIKE : X+X A.S.O. *)
\r
1750 B := COPYTNODE ( A.LEFT );
\r
1753 CALL COMPARE ( B , C , BETA ); (* COMPARE TWO TREES *)
\r
1754 IF BETA THEN (* THEY ARE EQUAL *)
\r
1758 WHEN 42 : A.IDENT := 94; (* TERM*TERM -> TERM^2 *)
\r
1759 A.LEFT.RIGHT.KIND := CNTKIND;
\r
1760 A.LEFT.RIGHT.IDENT := 2;
\r
1761 CALL ERASE ( A.LEFT.RIGHT.LEFT );
\r
1762 WHEN 43 : A.IDENT := 42; (* TERM+TERM -> 2*TERM *)
\r
1763 A.LEFT.KIND := CNTKIND;
\r
1764 A.LEFT.IDENT := 2;
\r
1765 CALL ERASE ( A.LEFT.LEFT );
\r
1770 CALL RULEVAL ( A.LEFT,ALFA );
\r
1771 CALL RULEVAL ( A.RIGHT,ALFA );
\r
1774 (****************************************************************************)
\r
1775 (* CALLS COUNT_0_1 UNTIL IT IS NOT USELESS *)
\r
1777 UNIT ZEROS_AND_ONES : PROCEDURE ( A : TNODE ; ALFA : BOOLEAN );
\r
1778 VAR BETA : BOOLEAN; (* BETA MEANS THAT COUNT_0_1 IS STILL WORKING *)
\r
1784 CALL COUNT_0_1 ( A , BETA );
\r
1785 ALFA := ALFA OR BETA;
\r
1787 END ZEROS_AND_ONES;
\r
1789 (****************************************************************************)
\r
1790 (* DOES ALL ARITHMETIC OPERATIONS *)
\r
1792 UNIT COUNT_0_1 : PROCEDURE ( B : TNODE ; INOUT ALEF : BOOLEAN );
\r
1793 VAR BETA : BOOLEAN;
\r
1795 IF B=NONE THEN RETURN FI;
\r
1796 IF B.KIND=ARIKIND THEN
\r
1798 IF B.LEFT.KIND = CNTKIND OR B.LEFT.KIND = CN1KIND THEN
\r
1800 WHEN 0: CASE B.IDENT
\r
1801 WHEN 42,94:CALL FUNCHECK ( B.LEFT.RIGHT , BETA );
\r
1802 IF B.IDENT = 94 AND B.LEFT.RIGHT.IDENT = 0
\r
1803 AND B.LEFT.RIGHT.KIND = CNTKIND THEN
\r
1804 CALL EXCEPTIONS ( 4 )
\r
1809 B.KIND := CNTKIND;
\r
1812 CALL ERASE ( B.LEFT );
\r
1816 WHEN 43:B.LEFT.RIGHT.RIGHT := B.RIGHT;
\r
1817 CALL LIFT ( B,1,0 );
\r
1818 CALL LIFT ( B,1,1 );
\r
1821 WHEN 47:IF B.LEFT.RIGHT.KIND=CNTKIND AND
\r
1822 B.LEFT.RIGHT.IDENT = 0 THEN
\r
1823 CALL EXCEPTIONS ( 2 )
\r
1825 CALL FUNCHECK ( B.LEFT.RIGHT,BETA );
\r
1827 B.KIND := CN1KIND;
\r
1829 B.KIND := CNTKIND;
\r
1832 CALL ERASE ( B.LEFT );
\r
1836 WHEN 45:CALL LIFT ( B.LEFT,1,1 );
\r
1840 WHEN 1: CASE B.IDENT
\r
1841 WHEN 42:B.LEFT.RIGHT.RIGHT := B.RIGHT;
\r
1842 CALL LIFT ( B,1,0 );
\r
1843 CALL LIFT ( B,1,1 );
\r
1846 WHEN 94:CALL FUNCHECK ( B.LEFT.RIGHT,BETA );
\r
1848 B.KIND := CN1KIND;
\r
1850 B.KIND := CNTKIND;
\r
1853 CALL ERASE ( B.LEFT );
\r
1856 WHEN 47:IF B.LEFT.RIGHT.IDENT=1 THEN
\r
1857 B.KIND := CNTKIND;
\r
1859 CALL ERASE ( B.LEFT );
\r
1866 IF B.LEFT.RIGHT.KIND = CNTKIND OR B.LEFT.RIGHT.KIND = CN1KIND THEN
\r
1867 CASE B.LEFT.RIGHT.IDENT
\r
1868 WHEN 0: CASE B.IDENT
\r
1869 WHEN 42:CALL FUNCHECK ( B.LEFT , BETA );
\r
1871 B.KIND := CN1KIND;
\r
1873 B.KIND := CNTKIND;
\r
1876 CALL ERASE ( B.LEFT );
\r
1879 WHEN 43:CALL ERASE ( B.LEFT.RIGHT );
\r
1880 B.LEFT.RIGHT := B.RIGHT;
\r
1881 CALL LIFT ( B,1,0 );
\r
1884 WHEN 94:CALL FUNCHECK ( B.LEFT,BETA );
\r
1886 B.KIND := CN1KIND;
\r
1888 B.KIND := CNTKIND;
\r
1891 CALL ERASE ( B.LEFT );
\r
1894 WHEN 47:CALL EXCEPTIONS ( 3 );
\r
1895 WHEN 45:KILL ( B.LEFT.RIGHT );
\r
1896 B.LEFT.RIGHT := B.RIGHT;
\r
1897 CALL LIFT ( B,1,0 );
\r
1901 WHEN 1: CASE B.IDENT
\r
1902 WHEN 42,47,94:B.LEFT.RIGHT.RIGHT := B.RIGHT;
\r
1903 CALL LIFT ( B,1,0 );
\r
1904 CALL LIFT ( B.RIGHT,1,1 );
\r
1912 CALL COUNT_0_1 ( B.LEFT,ALEF );
\r
1913 CALL COUNT_0_1 ( B.RIGHT,ALEF );
\r
1916 (****************************************************************************)
\r
1917 (* CHECK WHETHER THERE IS A FN1KIND OR CN1KIND IN A TREE *)
\r
1918 (* FN1KIND MEANS THE NAME OF FUNCTION DEFINED BY A PROCEDURE OF THE
\r
1921 UNIT FUNCHECK : PROCEDURE ( C : TNODE ; INOUT BETA : BOOLEAN );
\r
1923 IF C = NONE THEN RETURN FI;
\r
1924 IF C.KIND = FN1KIND OR C.KIND = CN1KIND THEN
\r
1928 CALL FUNCHECK ( C.LEFT , BETA );
\r
1929 CALL FUNCHECK ( C.RIGHT , BETA );
\r
1932 (****************************************************************************)
\r
1933 (* TERM=TERM CONVERTS TO LOGICAL 1 *)
\r
1935 UNIT RULEIDE : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
\r
1939 IF C=NONE THEN RETURN FI;
\r
1941 IF C.KIND=EQUKIND THEN
\r
1944 BVARPRO : A := C.LEFT;
\r
1945 CALL END_OF_S ( A,B );
\r
1948 CALL COMPARE ( C.LEFT,B,BETA );
\r
1950 WHEN IFFKIND : A := C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT ;
\r
1951 C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT := NONE;
\r
1952 CALL COMPARE ( C.LEFT , A , BETA );
\r
1953 C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT := A;
\r
1954 WHEN BEGKIND : A := C.LEFT.RIGHT.RIGHT;
\r
1955 C.LEFT.RIGHT.RIGHT := NONE;
\r
1956 CALL COMPARE ( C.LEFT, A ,BETA );
\r
1957 C.LEFT.RIGHT.RIGHT := A;
\r
1958 WHEN WHIKIND : A := C.LEFT.RIGHT.RIGHT.RIGHT;
\r
1959 C.LEFT.RIGHT.RIGHT.RIGHT := NONE;
\r
1960 CALL COMPARE ( C.LEFT , A , BETA );
\r
1961 C.LEFT.RIGHT.RIGHT.RIGHT := A;
\r
1962 OTHERWISE A := C.LEFT.RIGHT; (* STORE RIGHT ARGUMENT *)
\r
1963 C.LEFT.RIGHT := NONE;
\r
1964 CALL COMPARE ( C.LEFT , A , BETA );
\r
1965 C.LEFT.RIGHT := A;
\r
1968 C.KIND := LOGKIND;
\r
1970 CALL ERASE ( C.LEFT );
\r
1976 (*****************************************************************************)
\r
1977 (* COMPARE THOROUGHLY TWO TREES *)
\r
1979 UNIT COMPARE : PROCEDURE ( A,B : TNODE ; INOUT BETA : BOOLEAN );
\r
1981 IF A <> NONE AND B <> NONE THEN
\r
1982 IF A.KIND=B.KIND AND A.IDENT=B.IDENT THEN
\r
1983 CALL COMPARE ( A.LEFT,B.LEFT,BETA );
\r
1984 CALL COMPARE ( A.RIGHT,B.RIGHT,BETA )
\r
1990 IF A <> NONE OR B <> NONE THEN BETA := FALSE FI;
\r
1994 (****************************************************************************)
\r
1995 (* TERM1 <> TERM2 IN THE STANDARD INTERPRETATION CONVERTS TO 0 *)
\r
1997 UNIT RULEIDT : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
\r
1998 VAR BETA : BOOLEAN;
\r
2001 IF C = NONE THEN RETURN FI;
\r
2002 IF C.KIND = EQUKIND THEN
\r
2003 CALL CHECKCHAR ( C.LEFT,BETA );
\r
2005 IF COUNT( C.LEFT ) <> COUNT( C.LEFT.RIGHT ) THEN
\r
2006 C.KIND := LOGKIND;
\r
2008 CALL ERASE ( C.LEFT );
\r
2015 (****************************************************************************)
\r
2018 UNIT COUNT : FUNCTION ( A : TNODE ) : INTEGER;
\r
2019 VAR BASIS,I,POWER,LIMIT : INTEGER;
\r
2021 IF A.KIND <> ARIKIND THEN
\r
2025 WHEN 42 : RESULT := COUNT( A.LEFT ) * COUNT( A.LEFT.RIGHT );
\r
2026 WHEN 43 : RESULT := COUNT( A.LEFT ) + COUNT( A.LEFT.RIGHT );
\r
2027 WHEN 47 : RESULT := COUNT( A.LEFT ) DIV COUNT( A.LEFT.RIGHT );
\r
2028 WHEN 45 : RESULT := COUNT( A.LEFT ) - COUNT( A.LEFT.RIGHT );
\r
2029 WHEN 94 : IF A.LEFT.RIGHT.IDENT=0 THEN
\r
2033 BASIS := COUNT ( A.LEFT );
\r
2034 LIMIT := COUNT ( A.LEFT.RIGHT );
\r
2037 POWER := POWER * BASIS;
\r
2045 (****************************************************************************)
\r
2046 (* CHECK WHETHER TERM IS BUILT ONLY BY STANDARD FUNCTORS *)
\r
2048 UNIT CHECKCHAR : PROCEDURE ( A : TNODE ; INOUT BETA : BOOLEAN );
\r
2051 IF A.KIND=ARIKIND OR A.KIND=CNTKIND OR A.KIND=CN1KIND THEN
\r
2052 CALL CHECKCHAR ( A.LEFT , BETA );
\r
2053 CALL CHECKCHAR ( A.RIGHT , BETA )
\r
2061 (****************************************************************************)
\r
2062 (* A HELP FOR DUST_BIN PROCEDURE , MANAGE THE VERY SIMPLE BOOLEAN OPERATIONS *)
\r
2064 UNIT DUST : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
\r
2067 WHEN CONKIND: IF C.LEFT.KIND=LOGKIND THEN
\r
2069 WHEN 1: CALL ERASE ( C.LEFT );
\r
2070 CALL LIFT ( C,1,1 );
\r
2072 WHEN 0: CALL ERASE ( C.RIGHT );
\r
2073 CALL LIFT ( C,1,0 );
\r
2078 IF C.RIGHT.KIND=LOGKIND THEN
\r
2079 CASE C.RIGHT.IDENT
\r
2080 WHEN 1: CALL ERASE ( C.RIGHT );
\r
2081 CALL LIFT ( C,1,0 );
\r
2083 WHEN 0: CALL ERASE ( C.LEFT );
\r
2084 CALL LIFT ( C,1,1 );
\r
2089 WHEN DISKIND: IF C.LEFT.KIND=LOGKIND THEN
\r
2091 WHEN 1: CALL ERASE ( C.RIGHT );
\r
2092 CALL LIFT ( C,1,0 );
\r
2094 WHEN 0: CALL ERASE ( C.LEFT );
\r
2095 CALL LIFT ( C,1,1 );
\r
2100 IF C.RIGHT.KIND=LOGKIND THEN
\r
2101 CASE C.RIGHT.IDENT
\r
2102 WHEN 1: CALL ERASE ( C.LEFT );
\r
2103 CALL LIFT ( C,1,1 );
\r
2105 WHEN 0: CALL ERASE ( C.RIGHT );
\r
2106 CALL LIFT ( C,1,0 );
\r
2111 WHEN NEGKIND: IF C.LEFT.KIND=LOGKIND THEN
\r
2113 WHEN NEGKIND: CALL LIFT ( C,2,0 );
\r
2115 WHEN 1: CALL LIFT ( C,1,0 );
\r
2118 WHEN 0: CALL LIFT ( C,1,0 );
\r
2124 WHEN IMPKIND : IF C.LEFT.KIND=LOGKIND THEN
\r
2126 WHEN 1: CALL ERASE ( C.LEFT );
\r
2127 CALL LIFT ( C,1,1 );
\r
2129 WHEN 0: C.KIND := LOGKIND;
\r
2131 CALL ERASE ( C.LEFT );
\r
2132 CALL ERASE ( C.RIGHT );
\r
2137 IF C.RIGHT.KIND=LOGKIND THEN
\r
2138 CASE C.RIGHT.IDENT
\r
2139 WHEN 1: C.KIND := LOGKIND;
\r
2141 CALL ERASE ( C.LEFT );
\r
2142 CALL ERASE ( C.RIGHT );
\r
2144 WHEN 0: C.KIND:=NEGKIND;
\r
2145 CALL ERASE ( C.RIGHT );
\r
2153 (****************************************************************************)
\r
2154 (* CALLED BY SWEEP PROCEDURE *)
\r
2156 UNIT DUST_BIN : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
\r
2158 IF C = NONE THEN RETURN FI;
\r
2159 CALL RULEVAL ( C,ALFA ); (* COUNT ARITHMETIC EXPRESSIONS : '1+2 -> 3' *)
\r
2160 CALL ZEROS_AND_ONES ( C,ALFA ); (* COUNT EXPRESSIONS E.G. 0*X *)
\r
2161 CALL RULEIDT ( C,ALFA ); (* TERM1 <> TERM2 -> FALSE *)
\r
2162 CALL RULEIDE ( C,ALFA ); (* TERM1 IDENTICAL WITH TERM2 -> TRUE *)
\r
2163 CALL DUST ( C,ALFA ); (* SIMPLIFY BOOLEAN EXPRESSIONS *)
\r
2164 CALL DUST_BIN ( C.LEFT,ALFA );
\r
2165 CALL DUST_BIN ( C.RIGHT,ALFA );
\r
2168 (****************************************************************************)
\r
2169 (* MANAGE THE SWEEPING SYSTEM IN A TREE , CALL DUST_BIN PROCEDURE *)
\r
2171 UNIT SWEEP : PROCEDURE ( C : TNODE );
\r
2172 VAR ALFA : BOOLEAN;
\r
2176 DO (* SWEEP IF IT IS POSSIBLE *)
\r
2178 CALL DUST_BIN ( C , ALFA ); (* MAKE IT AND UPDATE ALFA *)
\r
2182 (****************************************************************************)
\r
2183 (* SQUEEZE A LIST OF SEQUENTS BY GETTING RID OF ALL THE HOLES *)
\r
2185 UNIT SQUEEZE : PROCEDURE ( M : POINTER , P : INTEGER );
\r
2186 VAR A,B : SEQUENT;
\r
2188 IF M=NONE ORIF M.NEXT=NONE ORIF LAST (M,P)=NONE THEN RETURN FI;
\r
2189 A := FIRSTHOLE ( M , P );
\r
2190 B := NEXTNODE ( A , P );
\r
2191 WHILE LAST(M,P).NEXT <> A
\r
2194 WHEN 1: A.PLEAF := B.PLEAF;
\r
2196 WHEN 0: A.LLEAF := B.LLEAF;
\r
2199 B := NEXTNODE ( A.NEXT , P );
\r
2200 A := FIRSTHOLE ( M , P );
\r
2204 (****************************************************************************)
\r
2205 (* SEARCH FOR THE FIRST NON-EMPTY TNODE AFTER THE FIRST HOLE *)
\r
2207 UNIT NEXTNODE : FUNCTION ( U : SEQUENT , P : INTEGER ) : SEQUENT;
\r
2208 VAR ALFA : BOOLEAN;
\r
2210 IF U=NONE THEN RETURN FI;
\r
2211 WHILE U <> NONE AND NOT ALFA
\r
2214 WHEN 1:IF U.PLEAF <> NONE THEN
\r
2220 WHEN 0:IF U.LLEAF <> NONE THEN
\r
2230 (****************************************************************************)
\r
2231 (* SEARCH FOR THE FIRST HOLE *)
\r
2233 UNIT FIRSTHOLE : FUNCTION ( M : POINTER , P : INTEGER ) : SEQUENT;
\r
2234 VAR ALFA : BOOLEAN,
\r
2237 IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;
\r
2239 WHILE A <> NONE AND NOT ALFA
\r
2242 WHEN 1: IF A.PLEAF=NONE THEN
\r
2248 WHEN 0: IF A.LLEAF=NONE THEN
\r
2258 (****************************************************************************)
\r
2260 (****************************************************************************)
\r
2261 (* ESSENTIAL RULES *)
\r
2262 (****************************************************************************)
\r
2264 (****************************************************************************)
\r
2265 (* SENDS TO PROPER RULES *)
\r
2267 UNIT RULES : PROCEDURE ( INOUT M : POINTER; P , R : INTEGER );
\r
2270 C := FINDCONN ( LAST ( M , P ) , R , P );
\r
2271 IF C=NONE THEN RETURN FI;
\r
2273 WHEN 03: CALL RULEEQU ( M,C,P );
\r
2274 WHEN 04: CALL RULECON ( M,C,P );
\r
2275 WHEN 05: CALL RULEDIS ( M,C,P );
\r
2276 WHEN 06: CALL RULEIMP ( M,C,P );
\r
2277 WHEN 07: CALL RULENEG ( M,C,P );
\r
2278 WHEN 09: IF P=1 THEN CALL RULEEXIST ( M,C,P )
\r
2279 ELSE CALL RULE_EX_GEN ( M,P,K_MN_K,C,LOGIC );
\r
2281 WHEN 08: IF P=1 THEN CALL RULE_EX_GEN ( M,P,K_MN_K,C,LOGIC )
\r
2282 ELSE CALL RULEEXIST ( M,C,P )
\r
2284 WHEN 10: CALL RULEIF ( M,C,P );
\r
2285 WHEN 11: CALL RULEBEG ( M, C, P );
\r
2286 WHEN 12: CALL RULEWHL ( M,C,P );
\r
2287 WHEN 13: CALL RULEQUAN ( M,P );
\r
2291 (****************************************************************************)
\r
2292 (* RULE FOR THE PROGRAM BEGIN-END *)
\r
2294 UNIT RULEBEG : PROCEDURE ( INOUT M : POINTER, C : TNODE, P : INTEGER );
\r
2295 VAR A,B,D,E,F : TNODE;
\r
2297 A := C.RIGHT; (* HOLD BETA *)
\r
2298 IF C.LEFT.IDENT = 1 THEN (* SIMULTANEOUSLY SUBSTITUTION *)
\r
2299 CALL BEG_SUB ( C ) ;
\r
2300 CALL MOVE ( M, P, P );
\r
2303 IF C.LEFT<>NONE THEN
\r
2304 CALL LIFT ( C, 1, 0 ); (* THROW 'BEGIN' AND 'END' *)
\r
2305 IF C.KIND=0 THEN (* ONLY ONE PROGRAM *)
\r
2306 CALL LIFT ( C, 1, 0 );
\r
2307 CALL END_OF_PRG ( C ); (* GO TO THE END OF IT *)
\r
2308 C.RIGHT := A (* REFERS TO 'BETA' *)
\r
2309 ELSE (* MORE THAN ONE PROGRAM *)
\r
2310 WHILE C.KIND=SEMKIND (* LOOP FOR NEXT PROGRAMS *)
\r
2312 B := C.RIGHT; (* HOLD NEXT PROGRAM *)
\r
2313 CALL LIFT ( C, 1, 0 ); (* THROW SEMICOLON *)
\r
2314 CALL END_OF_PRG ( C ); (* GO TO THE END OF PROGRAM *)
\r
2315 C.RIGHT := B; C:=B;
\r
2317 CALL END_OF_PRG ( C ); (* END OF LAST PROGRAM *)
\r
2318 C.RIGHT := A; (* REFERS TO 'BETA' *)
\r
2320 ELSE (* NO PROGRAM *)
\r
2321 CALL LIFT ( C, 1, 1 )
\r
2323 CALL MOVE ( M, P, P );
\r
2326 (****************************************************************************)
\r
2327 (* DO SIMULTANEOUS SUBSTITUTIONS, MADE BY RULEDF_F AND RULEDF_L
\r
2328 PROCEDURES, WHEN ONLY ATOMS LEFT *)
\r
2330 UNIT BEG_SUB : PROCEDURE ( C : TNODE );
\r
2332 IF C.RIGHT.KIND = LITKIND OR C.RIGHT.KIND = EQUKIND
\r
2333 OR C.RIGHT.KIND = LOGKIND OR C.RIGHT.KIND = BVAKIND THEN
\r
2334 (* MAKE ONLY IN ATOMS AND *)
\r
2335 (* LOGICAL CONTANTS *)
\r
2336 CALL SUB ( C, C.RIGHT );
\r
2337 CALL ERASE ( C.LEFT ); (* WHEN DONE ERASE SUBSTITUTIONS *)
\r
2338 CALL LIFT ( C, 1, 1 );
\r
2342 (*****************************************************************************)
\r
2343 (* CALLED BY BEG_SUB PROCEDURES *)
\r
2345 UNIT SUB : PROCEDURE ( A, A1 : TNODE );
\r
2346 VAR B,C,D : TNODE;
\r
2348 IF A1 = NONE THEN RETURN FI;
\r
2349 IF A1.KIND = SUBKIND THEN (* MIGHT BE CHANGED *)
\r
2350 B := A.LEFT; (* REFERS TO SEMICOLON *)
\r
2351 WHILE B <> NONE (* VIEW THE WHOLE LIST *)
\r
2353 IF B.KIND <> SEMKIND THEN
\r
2356 C := B.LEFT; (* C REFERS TO NEXT ARG *)
\r
2358 IF C.IDENT = A1.IDENT THEN (* WILL BE CHANGED *)
\r
2359 A1.LEFT := COPYTNODE ( C.LEFT ); (* S/TAU *)
\r
2360 D := A1.RIGHT; (* STORES TEMPORARILY NEXT ARG *)
\r
2361 CALL LIFT ( A1, 1, 0 ); (* REMOVE S *)
\r
2362 A1.RIGHT := D; (* LINK STORED ARG *)
\r
2363 CALL SUB ( A, A1.RIGHT ); (* REALIZE SIMULTANEOUS *)
\r
2364 (* SUBSTITUTION *)
\r
2370 CALL SUB ( A, A1.LEFT );
\r
2371 CALL SUB ( A, A1.RIGHT );
\r
2374 (****************************************************************************)
\r
2375 (* RULE FOR A PROGRAM WHILE-DO-OD *)
\r
2377 UNIT RULEWHL : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
2378 VAR B,D,E,F,G,S,T,U,V : TNODE;
\r
2380 B := C.LEFT; (* HOLD 'ALFA' *)
\r
2381 D := C.RIGHT.LEFT; (* HOLD PROGRAM 'K' *)
\r
2382 E := C.RIGHT.RIGHT; (* HOLD 'BETA' *)
\r
2383 C.KIND := BVARPRO; (* Q:=... *)
\r
2384 C.IDENT := -LAST_Q-1;
\r
2387 G.KIND := LOGKIND; (* ...1 *)
\r
2389 C.RIGHT.KIND := ITEKIND; (* ITER. GREAT QUANT. *)
\r
2390 C.RIGHT.IDENT := 0;
\r
2391 G := NEW TNODE; (* 'BEGIN' - 'END' *)
\r
2395 G.KIND := BEGKIND;
\r
2396 G.IDENT := ENDKIND;
\r
2399 U.KIND := SEMKIND; (* SEMICOLON *)
\r
2402 V.KIND := BVARPRO; (* Q:=... *)
\r
2403 V.IDENT := -LAST_Q-1;
\r
2406 T.KIND := CONKIND; (* CONJUNCTION *)
\r
2409 S.KIND := BVAKIND; (* Q *)
\r
2410 S.IDENT := -LAST_Q-1;
\r
2411 T.RIGHT := B; (* REFERS TO 'ALFA' *)
\r
2412 U.RIGHT := D; (* REFERS TO PROGRAM 'K' *)
\r
2415 T.KIND := CONKIND; (* CONJUNCTION *)
\r
2418 U.KIND := BVAKIND; (* Q *)
\r
2419 U.IDENT := -LAST_Q-1;
\r
2420 G := NEW TNODE; (* CONJUNCTION *)
\r
2422 G.KIND := CONKIND;
\r
2423 G.RIGHT := E; (* REFERS TO 'BETA' *)
\r
2426 T.KIND := NEGKIND; (* NEGATION *)
\r
2427 T.LEFT := COPYTNODE ( B ); (* OF 'ALFA' *)
\r
2428 LAST_Q := LAST_Q+1;
\r
2429 CALL MOVE ( M,P,P );
\r
2432 (****************************************************************************)
\r
2433 (* SEARCH FOR A VARIABLE NUMBER I IN FORMULA AND CHANGE IT INTO SUBKIND *)
\r
2435 UNIT SEARCH_X : PROCEDURE ( A : TNODE , I : INTEGER );
\r
2438 IF A.IDENT = I AND A.KIND = VARKIND THEN
\r
2439 A.KIND := SUBKIND;
\r
2440 A.IDENT := LAST_S;
\r
2442 CALL SEARCH_X ( A.LEFT , I );
\r
2443 CALL SEARCH_X ( A.RIGHT , I );
\r
2447 (*****************************************************************************)
\r
2448 (* BOTH RULES FOR QUANTIFIERS AX-ALFA *)
\r
2450 UNIT RULEQUAN : PROCEDURE ( M : POINTER , P : INTEGER );
\r
2451 VAR A,C,C1,D,E,F : TNODE;
\r
2453 IF P=0 THEN (* QUAN ON LEFT SIDE *)
\r
2454 IF LAST (M,0).NEXT = NONE THEN (* BOTTOM LONGER THAN TOP *)
\r
2455 LAST (M,0).NEXT := COPYSEQUENT( LAST(M,0) ); (* COPY A QUANTIFIER *)
\r
2456 CALL ERASE ( LAST(M,0).PLEAF ) (* ERASE UPPER SIDE OF SEQUENT *)
\r
2457 ELSE (* OTHERWISE *)
\r
2458 LAST(M,1).NEXT := COPYSEQUENT( LAST(M,0) ); (* COPY A QUANTIFIER *)
\r
2459 CALL ERASE ( LAST(M,0).PLEAF ); (* ERASE UPPER SIDE OF SEQUENT *)
\r
2463 WHEN 1: A := LAST (M,1).PLEAF;
\r
2464 WHEN 0: A := LAST (M,0).LLEAF;
\r
2467 WHILE C.KIND=VARPROG OR C.KIND=BVARPRO
\r
2469 C1 := C; (* C1 POINTS TO LAST S *)
\r
2470 C := C.RIGHT; (* C POINTS TO QUAN *)
\r
2472 D := NEW TNODE; (* NEW SUBSTITUTION *)
\r
2473 D.KIND := VARPROG; (* S:=... *)
\r
2474 LAST_S := LAST_S+1;
\r
2475 D.IDENT := LAST_S;
\r
2478 F.KIND := SUBKIND; (* ...:=Y *)
\r
2479 IF LAST_X <= LAST_S THEN
\r
2480 LAST_X := LAST_S + 1
\r
2482 LAST_X := LAST_X + 1
\r
2484 F.IDENT := LAST_X;
\r
2485 IF C1 = NONE THEN
\r
2490 D.RIGHT := C.LEFT; (* REFERS TO FORMULA 'ALFA' *)
\r
2491 CALL SEARCH_X ( C.LEFT , C.IDENT ); (* UPDATE NUMBERS OF BOUND *)
\r
2493 IF A.KIND = QUAKIND THEN
\r
2495 CALL LIFT ( A , 1 , 1 );
\r
2499 FI; (* ERASE QUANTIFIER TNODE *)
\r
2501 (* NEXT LINES ARE ONLY CONNECTED WITH THE LEFT SIDE QUANTIFIER *)
\r
2504 E := NEW TNODE; (* NEW SUBSTITUTION *)
\r
2505 E.KIND := VARPROG; (* Y:=... *)
\r
2506 E.IDENT := LAST_X;
\r
2507 LAST_S := LAST_X; (* UPDATE NUMBER OF LAST *)
\r
2508 (* SUBSTITUTION *)
\r
2509 F := NEW TNODE; (* ...:=TERM *)
\r
2511 F.KIND := SIGNTRM; (* JOKER TERM *)
\r
2512 LAST_D := LAST_D+1;
\r
2513 F.IDENT := LAST_D;
\r
2514 E.RIGHT := A; (* REFERS TO SUBSTITUTIONS *)
\r
2515 LAST ( M , 0 ).LLEAF := E;
\r
2516 CALL MOVE ( M , P , P ); (* MOVES THE LAST SEQUENT *)
\r
2517 (* WITHOUT QUANTIFIER *)
\r
2518 CALL SWEEP ( M.NEXT.LLEAF );
\r
2520 CALL MOVE ( M , P , P ); (* MOVES SEQUENT *)
\r
2521 (* WITH QUANTIFIER *)
\r
2524 (***************************************************************************)
\r
2525 (* HELP FOR RULEITE - MAKE COPY AND INSERT IT DOWN TO CURRENT POINTER M *)
\r
2527 UNIT K_MN_K_DOWN : PROCEDURE ( M : POINTER, E : TNODE );
\r
2528 VAR M2 : POINTER,
\r
2531 M2 := NEW POINTER;
\r
2532 M2.NEXT := COPYSEQUENT ( M.NEXT );
\r
2533 M2.DOWN := M.DOWN;
\r
2535 A1 := LAST ( M2 , 0 );
\r
2536 CALL ERASE ( A1.LLEAF );
\r
2537 A1.LLEAF := COPYTNODE ( E );
\r
2538 CALL SWEEP ( A1.LLEAF );
\r
2539 CALL SQUEEZE ( M2 , 0 );
\r
2540 CALL MOVE ( M2 , 0 , 0 )
\r
2543 (***************************************************************************)
\r
2544 (* ITERATIONAL QUANTIFIER CONNECTED WITH WHILE *)
\r
2546 UNIT RULEITE : PROCEDURE ( INOUT M : POINTER , LOGIC : BOOLEAN );
\r
2547 (* K_MN_K MEANS k IN Mn(k) *)
\r
2549 VAR A,B,C,D,E:TNODE,
\r
2555 C := COPYTNODE ( LAST ( M , 0 ).LLEAF );
\r
2556 E := C; (* E HOLDS BEGINNING OF Mn(0) *)
\r
2557 WHILE C.KIND <> ITEKIND
\r
2558 DO (* MAKE THE SAME IN FAKE TREE *)
\r
2561 OD; (* C POINTS TO ITERATION *)
\r
2562 A := COPYTNODE ( E );
\r
2563 CALL LIFT ( C , 1 , 1); (* EXPELL ITERATION QUANTIFIER *)
\r
2566 WHILE B .KIND <> ITEKIND
\r
2570 CALL LIFT ( B, 1, 1 ); (* EXPELL ITERATION QUANTIFIER *)
\r
2571 CALL ERASE ( B.LEFT );
\r
2572 CALL LIFT ( B, 1, 1 );
\r
2573 WHILE B.KIND <> CONKIND
\r
2574 DO (* GO DOWN UNTIL C CONTAINS CONJUNCTION *)
\r
2577 M2 := NEW POINTER; (* CREATES NEW BRANCH *)
\r
2578 M2.NEXT := COPYSEQUENT ( M.NEXT );
\r
2579 M2.DOWN := M.DOWN;
\r
2581 F := LAST ( M2 , 0 );
\r
2582 CALL ERASE ( F.LLEAF );
\r
2584 CALL SWEEP ( F.LLEAF );
\r
2585 CALL SQUEEZE ( M2 , 0 );
\r
2587 IF NOT LOGIC OR K_MN_K=1 THEN (* CONSTRUCT Mn(1) *)
\r
2588 M2 := NEW POINTER; (* AND INSERT IT INTO *)
\r
2589 M2.NEXT := COPYSEQUENT ( M.NEXT ); (* THE SEQUENT *)
\r
2590 F := LAST ( M2 , 0 );
\r
2591 CALL ERASE ( F.LLEAF );
\r
2592 F.LLEAF := COPYTNODE ( E );
\r
2593 M2.DOWN := M.DOWN;
\r
2595 CALL SWEEP ( F.LLEAF );
\r
2596 CALL SQUEEZE ( M2 , 0 );
\r
2598 FOR I := 0 TO K_MN_K-2
\r
2600 (* CREATE kMn(K_MN_K)ALFA *)
\r
2601 B := C; (* B POINTS TO BEGIN-END PROGRAM AFTER 'U' *)
\r
2602 WHILE B.KIND <> CONKIND
\r
2603 DO (* GOES DOWN UNTIL B CONTAINS CONJUNCTION *)
\r
2606 OD; (* B POINTS TO CONJUNCTION, A PRECEED B *)
\r
2607 D := COPYTNODE ( C ); (* D CONTAINS ONLY ONE PROGRAM K *)
\r
2608 (* AND CONJUCTION AS WELL *)
\r
2609 CALL ERASE ( A.RIGHT );
\r
2612 IF NOT LOGIC THEN (* LOGIC=TRUE MEANS THAT WHILE HAS *)
\r
2613 CALL K_MN_K_DOWN ( M, E ); (* ALREADY BEEN USED *)
\r
2617 IF LOGIC AND K_MN_K > 1 THEN (* INSERT Mn(K) INTO *)
\r
2618 CALL K_MN_K_DOWN ( M, E );
\r
2621 (* PREPARE THREE NEW FORMULAS TO PROVE FOR 'WHILE' *)
\r
2624 M3 := NEW POINTER;
\r
2625 SQNT := COPYSEQUENT ( LAST ( M.DOWN , 0 ) );
\r
2626 CALL ERASE_SEQ ( SQNT.NEXT );
\r
2627 CALL ERASE ( SQNT.PLEAF );
\r
2629 WHILE A.KIND <> CONKIND
\r
2634 WHEN 1 : CALL ERASE ( A.RIGHT );
\r
2635 CALL LIFT ( A , 1 , 0 ); (* M(l) p *)
\r
2636 WHEN 2 : CALL ERASE ( A.LEFT ); (* M(l) NOT ALFA *)
\r
2637 CALL LIFT ( A , 1 , 1 );
\r
2638 CALL ERASE ( A.RIGHT );
\r
2639 CALL LIFT ( A , 1 , 0 );
\r
2640 WHEN 3 : CALL ERASE ( A.LEFT ); (* M(l) BETA *)
\r
2641 CALL LIFT ( A , 1 , 1 );
\r
2642 CALL ERASE ( A.LEFT );
\r
2643 CALL LIFT ( A , 1 , 1 );
\r
2647 DIF := 1; (* VARIABLE DIF MEANS THAT *)
\r
2648 (* PROVE PROCEDURE WAS CALLED *)
\r
2650 CALL PROVE ( M3 , DIF ); (* PROOF FOR M(l)p, *)
\r
2651 (* M(l)NOT ALFA, *)
\r
2652 (* AND M(l)BETA *)
\r
2653 CALL ERASE_PNTR ( M3 );
\r
2654 (* IF ONE CAN PROVE CURRENT *)
\r
2655 (* SEQUENT E.G. Mn(l)p |- GENERATED *)
\r
2656 (* BY 'WHILE ' CHI IS NOT CHANGED *)
\r
2657 (* OTHERWISE CHI := FALSE IN PROVE *)
\r
2658 IF CHI THEN EXIT FI; (* FINISHED PROOF BY M(l)p *)
\r
2659 (* OR M(l)NOT ALFA *)
\r
2660 (* OR BY M(l)BETA *)
\r
2663 CALL ERASE_SEQ ( M.NEXT );
\r
2664 CALL LIFT_PNTR ( M );
\r
2665 CALL ERASE_SEQ ( M.NEXT );
\r
2666 CALL LIFT_PNTR ( M );
\r
2670 (****************************************************************************)
\r
2671 (* RULE FOR ITERATION QUANTIFIERS *)
\r
2673 UNIT RULE_EX_GEN:PROCEDURE(INOUT M:POINTER;P,K_MN_K:INTEGER,C:TNODE,LOGIC:BOOLEAN);
\r
2679 IF C.RIGHT.KIND = BEGKIND ANDIF C.RIGHT.LEFT <> NONE ANDIF
\r
2680 C.RIGHT.LEFT.LEFT <> NONE ANDIF C.RIGHT.LEFT.LEFT.IDENT < 0 THEN
\r
2681 CALL RULEITE ( M , LOGIC ); (* WHILE - ITERATION *)
\r
2685 A2 := COPYSEQUENT ( M.NEXT );
\r
2686 M2 := NEW POINTER; (* CREATE NEW BRANCH *)
\r
2689 WHEN 0: A := LAST (M2,0).LLEAF;
\r
2690 WHEN 1: A := LAST (M2,1).PLEAF;
\r
2692 IF C.IDENT = 0 THEN (* THE FIRST STEP OF ITERATION *)
\r
2693 CALL END_OF_S ( A,B );
\r
2694 CALL LIFT ( A, 1, 1 ); (* REMOVE ITERATION SIGN *)
\r
2696 CALL ERASE ( A.LEFT );
\r
2697 CALL LIFT ( A, 1, 1 ); (* REMOVE SUBSTITUTION OR *)
\r
2698 (* BEGINNING OF ANOTHER PROGRAM *)
\r
2699 IF I <> VARPROG AND I <> BVARPRO THEN
\r
2701 WHEN WHIKIND : CALL ERASE ( A.LEFT );
\r
2702 CALL LIFT ( A,1,1 );
\r
2703 WHEN IFFKIND : CALL ERASE ( A.LEFT );
\r
2704 CALL LIFT ( A,1,1 );
\r
2705 CALL ERASE ( A.LEFT );
\r
2706 CALL LIFT ( A,1,1 );
\r
2710 ELSE (* NEXT STEPS OF ITERATION *)
\r
2711 WHILE A.KIND=VARPROG OR A.KIND=BVARPRO (* OMITS SUBSTITUTION *)
\r
2716 A := A.RIGHT; (* A REFERS TO PROGRAM 'K' *)
\r
2717 IF A.KIND=VARPROG OR A.KIND=BVARPRO THEN (* CONSISTING OF SUBSTITUTION *)
\r
2718 C2 := COPYTNODE ( A );
\r
2719 CALL ERASE ( A.RIGHT );
\r
2721 ELSE (* OR ANOTHER PROGRAM *)
\r
2723 WHILE A.IDENT<>ENDKIND AND A.IDENT<>ODFKIND AND A.IDENT<>FIFKIND
\r
2726 OD; (* A OMITS PROGRAM 'K' *)
\r
2727 C2 := COPYTNODE ( D );
\r
2728 CALL ERASE ( A.RIGHT );
\r
2732 M3 := M2; (* ITERATION PUSHED TO *)
\r
2733 M2 := M; (* THE END OF A TREE *)
\r
2736 CALL MOVE ( M , P , P );
\r
2739 (****************************************************************************)
\r
2740 (* EXISTENTIAL ITERATION QUANTIFIER *)
\r
2742 UNIT RULEEXIST : PROCEDURE ( M : POINTER, C : TNODE, P : INTEGER );
\r
2743 VAR B,D,E : TNODE,
\r
2747 E := COPYTNODE ( C.RIGHT );
\r
2748 IF B.RIGHT.KIND=VARPROG OR B.RIGHT.KIND=BVARPRO THEN
\r
2749 D := B.RIGHT.RIGHT;
\r
2750 B.RIGHT.RIGHT := E
\r
2752 WHILE B.IDENT<>FIFKIND AND B.IDENT<>ODFKIND AND B.IDENT<>ENDKIND
\r
2760 WHEN 0 : IF LAST (M,0).NEXT = NONE THEN
\r
2761 LAST (M,0).NEXT := COPYSEQUENT ( LAST(M,P) )
\r
2763 LAST (M,1).NEXT := COPYSEQUENT ( LAST(M,P) )
\r
2765 E := FINDCONN ( LAST(M,0) , IGQKIND , 0 );
\r
2766 CALL ERASE ( LAST(M,0).PLEAF );
\r
2767 WHEN 1 : IF LAST (M,1).NEXT = NONE THEN
\r
2768 LAST (M,1).NEXT := COPYSEQUENT ( LAST(M,P) )
\r
2770 LAST (M,0).NEXT := COPYSEQUENT ( LAST(M,P) )
\r
2772 E := FINDCONN ( LAST(M,1) , ITEKIND , 1 );
\r
2773 CALL ERASE ( LAST(M,1).LLEAF );
\r
2775 CALL ERASE ( E.RIGHT );
\r
2777 CALL LIFT ( E , 1 , 1 );
\r
2779 WHEN 0: CALL MOVE ( M , 0 , 0 );
\r
2780 CALL SWEEP ( M.NEXT.LLEAF );
\r
2781 CALL MOVE ( M , 0 , 0 );
\r
2782 WHEN 1: CALL MOVE ( M , 1 , 1 );
\r
2783 CALL SWEEP ( M.NEXT.PLEAF );
\r
2784 CALL MOVE ( M , 1 , 1 );
\r
2788 (****************************************************************************)
\r
2789 (* RULE FOR IF-ALFA-THEN-K-ELSE-M-FI-BETA OR WITHOUT 'ELSE' PROGRAM *)
\r
2791 UNIT RULEIF : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
2792 VAR B,D,E,G,H,K : TNODE;
\r
2794 B := C.LEFT; (* HOLD 'ALFA' *)
\r
2796 D := C.RIGHT.RIGHT.RIGHT; (* HOLD BETA *)
\r
2797 C.RIGHT.RIGHT.RIGHT := NONE;
\r
2798 IF C.RIGHT.RIGHT.KIND <> ELSKIND THEN (* WITHOUT 'ELSE' *)
\r
2799 C.LEFT := B; (* REFERS TO 'ALFA' *)
\r
2800 C.KIND := CONKIND;
\r
2802 CALL LIFT ( C , 1 , 0 ); (* THROW 'THNKIND' *)
\r
2803 CALL END_OF_PRG ( C ); (* GO TO THE END OF 'K' *)
\r
2804 C.RIGHT := D (* REFERS TO 'BETA' *)
\r
2805 ELSE (* WITH 'ELSE' *)
\r
2806 C.KIND := DISKIND;
\r
2808 G.KIND := CONKIND;
\r
2810 G.LEFT := B; (* REFERS TO 'ALFA' *)
\r
2811 K := C.RIGHT.RIGHT.LEFT; (* HOLD PROGRAM 'M' *)
\r
2814 CALL LIFT ( E , 1 , 0 ); (* THROW 'THNKIND' *)
\r
2816 CALL END_OF_PRG ( G ); (* GO TO THE END OF 'K' *)
\r
2817 G.RIGHT := D; (* REFERS TO 'BETA' *)
\r
2818 H := NEW TNODE; (* 2ND ARG OF DISJUNCTION *)
\r
2820 H.KIND := CONKIND;
\r
2822 G.KIND := NEGKIND;
\r
2824 G.LEFT := COPYTNODE ( B ); (* REFERS TO 'ALFA' *)
\r
2826 CALL END_OF_PRG ( H );
\r
2827 H.RIGHT := COPYTNODE ( D ); (* REFERS TO 'BETA' *)
\r
2828 H := C.LEFT; (* CHANGE FORMULA *)
\r
2829 C.LEFT := C.RIGHT;
\r
2832 CALL MOVE ( M , P , P );
\r
2835 (****************************************************************************)
\r
2836 (* RULE FOR IMPLICATION *)
\r
2838 UNIT RULEIMP : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
2843 WHEN 1: D:= NEW SEQUENT; (* |- P => Q CONVERT TO *)
\r
2844 D.NEXT := M.NEXT; (* P |- Q *)
\r
2846 U := COPYTNODE ( LAST ( M,1 ).PLEAF );
\r
2848 CALL ERASE ( C.LEFT );
\r
2849 CALL LIFT ( C , 1 , 1 );
\r
2850 V := FINDCONN ( D, IMPKIND, 0 );
\r
2851 CALL ERASE ( V.RIGHT );
\r
2852 CALL LIFT ( V, 1, 0 );
\r
2853 CALL MOVE ( M, 1, 1 );
\r
2854 WHEN 0: C.KIND := DISKIND; (* IMPLICATION CHANGE TO *)
\r
2855 U := NEW TNODE; (* DISJUNCTION *)
\r
2856 U.KIND := NEGKIND;
\r
2859 CALL RULEDIS ( M , C , P );
\r
2863 (****************************************************************************)
\r
2864 (* RULE FOR EQUIVALENCE *)
\r
2866 UNIT RULEEQU : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
2867 VAR T,U,V,W : TNODE;
\r
2870 C.KIND := CONKIND;
\r
2871 U := COPYTNODE ( C.LEFT );
\r
2872 V := COPYTNODE ( C.RIGHT );
\r
2875 W.KIND := IMPKIND;
\r
2876 T.KIND := IMPKIND;
\r
2880 T.RIGHT := C.RIGHT;
\r
2883 CALL MOVE ( M , P , P );
\r
2886 (*****************************************************************************)
\r
2887 (* MAKE SERIAL OR PARALLEL SUBSTITUTION ON ATOMS *)
\r
2889 UNIT SUBAT : PROCEDURE ( M : POINTER , P : INTEGER );
\r
2894 IF A=NONE THEN RETURN FI;
\r
2896 WHEN 1: B := A.PLEAF;
\r
2897 WHEN 0: B := A.LLEAF;
\r
2899 IF B = NONE THEN RETURN FI;
\r
2900 IF B.KIND = BEGKIND AND B.LEFT.IDENT <> 1 THEN RETURN FI;
\r
2901 IF B.KIND = BEGKIND AND B.LEFT.IDENT = 1 AND (B.RIGHT.KIND = LITKIND
\r
2902 OR B.RIGHT.KIND = EQUKIND ) THEN CALL BEG_SUB ( B ); RETURN FI;
\r
2903 IF B.KIND = BEGKIND AND B.LEFT.IDENT = 1 AND (B.RIGHT.KIND = BVARPRO
\r
2904 OR B.RIGHT.KIND = VARPROG ) THEN CALL SER_INSERT ( B.RIGHT );RETURN
\r
2906 CALL SER_INSERT ( B );
\r
2909 (*****************************************************************************)
\r
2910 (* DO SERIAL SUBSTITUTITON *)
\r
2912 UNIT SER_INSERT : PROCEDURE ( A : TNODE );
\r
2915 CALL END_OF_S ( A, B ); (* GO TO LAST SUBSTITUTION *)
\r
2916 IF B.RIGHT.KIND = BVAKIND THEN
\r
2917 CALL SERIAL_Q ( B, B.RIGHT ) (* MAKE SERIAL SUBSTITUION *)
\r
2918 (* FOR LOGICAL VARIABLES *)
\r
2920 CALL SERIAL_SUB ( B, B.RIGHT ); (* MAKE SERIAL SUBSTITUTION *)
\r
2921 FI; (* FOR LITERALS OR EQUALITIES *)
\r
2922 CALL ERASE ( B.LEFT ); (* REMOVE TAU *)
\r
2923 CALL LIFT ( B, 1, 1 ); (* REMOVE SUBSTITUTION *)
\r
2926 (*****************************************************************************)
\r
2927 (* DO SERIAL SUBSTITUTION FOR ON LOGICAL VARIABLES - BVAKINS'S *)
\r
2929 UNIT SERIAL_Q : PROCEDURE ( C, D : TNODE );
\r
2931 IF D = NONE THEN RETURN FI;
\r
2932 IF D.IDENT = C.IDENT THEN
\r
2933 D.LEFT := COPYTNODE ( C.LEFT ); (* COPY TAU *)
\r
2934 CALL LIFT ( D , 1 , 0 ); (* REMOVE S *)
\r
2938 (*****************************************************************************)
\r
2939 (* CALLED BY SER_INSERT *)
\r
2941 UNIT SERIAL_SUB : PROCEDURE ( C,D : TNODE );
\r
2944 IF D = NONE THEN RETURN FI;
\r
2945 IF ( D.KIND = SUBKIND OR D.KIND = BVAKIND ) AND D.IDENT = C.IDENT THEN
\r
2946 E := D.RIGHT; (* STORE TEMPORARILY NEXT ARG *)
\r
2947 D.LEFT := COPYTNODE ( C.LEFT ); (* COPY TAU *)
\r
2948 CALL LIFT ( D , 1 , 0 ); (* REMOVE S *)
\r
2949 D.RIGHT := E; (* LINK NEXT ARG *)
\r
2950 CALL SERIAL_SUB ( C , D.RIGHT ); (* SEARCH FOR NEXT SUBKIND *)
\r
2953 CALL SERIAL_SUB ( C , D.LEFT );
\r
2954 CALL SERIAL_SUB ( C , D.RIGHT );
\r
2957 (****************************************************************************)
\r
2958 (* MOVES ALL ATOMS FROM THE END TO THE BEGINNING *)
\r
2960 UNIT RULEAT : PROCEDURE ( M : POINTER , P : INTEGER ; INOUT BET : BOOLEAN );
\r
2961 VAR A , B : SEQUENT;
\r
2963 IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;
\r
2966 WHEN 0 : WHILE A <> NONE
\r
2968 IF A.LLEAF <> NONE THEN
\r
2969 IF A.LLEAF.KIND <> LITKIND AND A.LLEAF.KIND <> EQUKIND
\r
2970 AND A.LLEAF.KIND <> LOGKIND AND
\r
2971 A.LLEAF.KIND <> BVAKIND THEN
\r
2977 WHEN 1 : WHILE A <> NONE
\r
2979 IF A.PLEAF <> NONE THEN
\r
2980 IF A.PLEAF.KIND <> LITKIND AND A.PLEAF.KIND <> EQUKIND
\r
2981 AND A.PLEAF.KIND <> LOGKIND AND
\r
2982 A.PLEAF.KIND <> BVAKIND THEN
\r
2989 IF B = NONE THEN RETURN FI;
\r
2990 WHILE B <> LAST ( M , P )
\r
2992 CALL MOVE ( M , P , P );
\r
2997 (****************************************************************************)
\r
2998 (* RULE FOR NEGATION *)
\r
3000 UNIT RULENEG : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
3002 CALL LIFT ( C , 1 , 0 );
\r
3003 CALL MOVE ( M , P , 1 - P );
\r
3006 (****************************************************************************)
\r
3007 (* DIVIDE A SEQUENT INTO TWO PIECES AND DEPENDING ON 'S' RE-CONSTRUCT A LIST:
\r
3008 S=1-ONE LIST; S=0-TWO LISTS *)
\r
3010 UNIT BRANCH : PROCEDURE ( M : POINTER , P , R , S : INTEGER , C : TNODE );
\r
3013 E,F,E1,F1 : TNODE;
\r
3017 E := COPYTNODE( C.LEFT );
\r
3018 F := COPYTNODE( C.RIGHT );
\r
3019 A := LAST ( M , P );
\r
3022 WHEN 0 : D.LLEAF := COPYTNODE ( A.LLEAF );
\r
3023 B.LLEAF := COPYTNODE ( A.LLEAF );
\r
3025 CALL END_OF_PRG ( E1 );
\r
3026 IF E1 <> NONE THEN
\r
3032 CALL END_OF_PRG ( E1 );
\r
3033 IF E1 <> NONE THEN
\r
3038 CALL ERASE ( A.LLEAF );
\r
3039 WHEN 1 : D.PLEAF := COPYTNODE ( A.PLEAF );
\r
3040 B.PLEAF := COPYTNODE ( A.PLEAF );
\r
3042 CALL END_OF_PRG ( E1 );
\r
3043 IF E1 <> NONE THEN
\r
3049 CALL END_OF_PRG ( E1 );
\r
3050 IF E1 <> NONE THEN
\r
3055 CALL ERASE ( A.PLEAF );
\r
3058 WHEN 0: D.NEXT := M.NEXT;
\r
3059 M2 := NEW POINTER;
\r
3060 M2.DOWN := M.DOWN;
\r
3064 B.NEXT := COPYSEQUENT ( D.NEXT );
\r
3065 WHEN 1: B.NEXT := M.NEXT;
\r
3071 (****************************************************************************)
\r
3072 (* RULE FOR CONJUNCTION *)
\r
3074 UNIT RULECON : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
3076 CALL BRANCH ( M,P,4,1-P,C );
\r
3078 WHEN 1 : CALL SWEEP ( M.DOWN.NEXT.PLEAF );
\r
3079 WHEN 0 : CALL SWEEP ( M.NEXT.NEXT.PLEAF );
\r
3083 (****************************************************************************)
\r
3084 (* RULE FOR DISJUNCTION *)
\r
3086 UNIT RULEDIS : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
\r
3088 CALL BRANCH ( M , P , 5 , P , C );
\r
3090 WHEN 0 : CALL SWEEP ( M.DOWN.NEXT.PLEAF );
\r
3091 WHEN 1 : CALL SWEEP ( M.NEXT.NEXT.PLEAF );
\r
3095 (*****************************************************************************)
\r
3098 (*****************************************************************************)
\r
3099 (* MAIN BODY OF THIS PROVER *)
\r
3100 (*****************************************************************************)
\r
3102 (*****************************************************************************)
\r
3103 (* PROVE AND RETRIEVE AXIOMS OF ALL INPUT FORMULAS *)
\r
3105 UNIT PROVE : PROCEDURE ( INOUT M : POINTER; DIF : INTEGER );
\r
3106 VAR BETA : BOOLEAN;
\r
3108 CALL SWEEP ( M.NEXT.PLEAF );
\r
3109 CALL THROW_RUBBISH ( M );
\r
3114 WHILE CHECK_L_F_P ( M.NEXT )
\r
3117 CALL SHOW_SEQ ( M.NEXT );
\r
3118 CALL PROVE_P ( M , 1 );
\r
3119 CALL MAKE_ORDER ( M );
\r
3120 CALL PROVE_P ( M , 0 );
\r
3121 CALL MAKE_ORDER ( M );
\r
3122 IF AX <> NONE THEN
\r
3123 IF SEARCH_AXIOMS ( M ) THEN
\r
3124 CALL ERASE_SEQ ( M.NEXT );
\r
3125 BETA := TRUE; (* FOUND AXIOM *)
\r
3133 CALL SHOW_SEQ ( M.NEXT );
\r
3135 IF SEARCH_AXIOMS ( M ) THEN
\r
3136 CALL ERASE_SEQ ( M.NEXT );
\r
3140 IF AX <> NONE THEN
\r
3142 CALL SHOW_TREE ( AX.AXIOM );
\r
3143 WRITELN("KONIEC");
\r
3145 IF BETA ORIF M.NEXT=NONE ORIF SEARCH_AXIOMS ( M ) THEN
\r
3146 CALL LIFT_PNTR ( M );
\r
3150 WRITE("THERE IS NO MODEL TO PROVE THIS EQUIVALENCE");
\r
3158 IF AX = NONE THEN WRITELN ( " THE FORMULA IS A THEOREM "); FI;
\r
3161 (*****************************************************************************)
\r
3162 (* DO THE RULES FOR P - SIDE UNTIL IT HAS NO USE *)
\r
3164 UNIT PROVE_P : PROCEDURE ( INOUT M : POINTER; P : INTEGER );
\r
3165 VAR R,I : INTEGER,
\r
3170 IF LAST ( M , P ) <> NONE THEN
\r
3173 IF FINDCONN ( LAST ( M , P ) , I , P ) <> NONE THEN
\r
3179 CALL RULES ( M, P, R )
\r
3182 WHEN 0 : A := LAST ( M, P ).LLEAF;
\r
3183 WHEN 1 : A := LAST ( M, P ).PLEAF;
\r
3185 IF A.KIND = BEGKIND ANDIF A.LEFT.KIND = SEMKIND ANDIF
\r
3186 A.LEFT.IDENT = 1 THEN
\r
3187 IF A.RIGHT.KIND <> VARPROG AND A.RIGHT.KIND <> BVARPRO THEN
\r
3189 WHEN 1 : CALL RULEBEG ( M, A , P );
\r
3190 WHEN 0 : CALL RULEBEG ( M, A , P );
\r
3195 IF A.RIGHT <> NONE THEN
\r
3196 IF A.KIND = VARPROG ORIF A.KIND = BVARPRO ORIF A.RIGHT.KIND = VARPROG
\r
3197 ORIF A.RIGHT.KIND = BVARPRO THEN
\r
3198 CALL SUBAT ( M, P );
\r
3200 WHEN 0 : CALL SWEEP ( LAST ( M, P ).LLEAF );
\r
3201 WHEN 1 : CALL SWEEP ( LAST ( M, P ).PLEAF );
\r
3203 CALL MOVE ( M, P, P );
\r
3207 CALL RULEAT ( M, P, BET );
\r
3208 IF NOT BET AND DEF_LIT = 1 THEN
\r
3210 CASE M1.FUN_REL.KIND
\r
3211 WHEN LITKIND : CALL RULEDF_L ( M, P, M1.FUN_REL.IDENT );
\r
3212 WHEN EQUKIND : CALL RULEDF_F ( M, P, M1.FUN_REL.LEFT.IDENT );
\r
3219 (*****************************************************************************)
\r
3220 (* DO ORDER PROCEDURES IN WHOLE SEQUENT *)
\r
3222 UNIT MAKE_ORDER : PROCEDURE ( M : POINTER );
\r
3224 IF M = NONE ORIF M.NEXT = NONE THEN RETURN FI;
\r
3225 CALL SQUEEZE ( M, 0 ); (* REMOVE HOLES *)
\r
3226 CALL SQUEEZE ( M, 1 );
\r
3227 CALL SWEEP ( M.NEXT.PLEAF ); (* MAKE SIMPLE OPERATION *)
\r
3228 CALL SWEEP ( M.NEXT.LLEAF );
\r
3229 CALL CLAS_AX ( M ); (* SEARCH CLASSICAL AXIOMS *)
\r
3230 CALL THROW_RUBBISH ( M ); (* REMOVE SEQUENT CONTAINING *)
\r
3231 (* LOGICAL CONSTANTS *)
\r
3232 IF M.NEXT <> NONE THEN CALL CUT_SEQ ( M.NEXT ) FI;
\r
3233 (* REMOVE EMPTY FORMULAS *)
\r
3236 (*****************************************************************************)
\r
3237 (* SEARCH EXTRA AXIOMS *)
\r
3239 UNIT SEARCH_AXIOMS : FUNCTION ( INOUT M : POINTER ) : BOOLEAN;
\r
3241 IF SEARCH_CN1 ( M.NEXT ) THEN
\r
3242 CALL END_OF_M ( M, M.NEXT );
\r
3245 IF LOOK_NQ ( M, 0 ) OR LOOK_NQ ( M, 1 ) OR LOOK_IDE ( M.NEXT ) THEN
\r
3247 CALL ERASE_SEQ ( M.NEXT );
\r
3249 END SEARCH_AXIOMS;
\r
3251 (****************************************************************************)
\r
3252 (* SEARCH FOR FALSE CONSTANTS IN WHOLE SEQUENT *)
\r
3254 UNIT SEARCH_CN1 : FUNCTION ( A : SEQUENT ) : BOOLEAN;
\r
3255 VAR ALFA : BOOLEAN;
\r
3259 CALL FUNCHECK ( A.PLEAF, ALFA );
\r
3260 CALL FUNCHECK ( A.LLEAF, ALFA );
\r
3269 (****************************************************************************)
\r
3270 (* SEARCH CLASSICAL AXIOMS *)
\r
3272 UNIT CLAS_AX : PROCEDURE ( M : POINTER );
\r
3273 VAR A, A1 : SEQUENT,
\r
3274 AX1 : LIST_AXIOMS,
\r
3277 IF M.NEXT=NONE THEN RETURN FI;
\r
3280 DO (* SEARCH FOR THE IDENTICAL *)
\r
3282 IF A.PLEAF <> NONE THEN (* FORMULAS IN A SEQUENT *)
\r
3284 DO (* ON BOTH SIDES *)
\r
3285 IF A1.LLEAF <> NONE THEN (* I.E. ...beta...|-...beta... *)
\r
3287 CALL COMPARE ( A.PLEAF, A1.LLEAF, ALFA);
\r
3289 CALL ERASE_SEQ ( M.NEXT ); (* WHEN FOUND - ERASE SEQUENT *)
\r
3302 IF A.PLEAF <> NONE THEN
\r
3305 IF A1.LLEAF <> NONE THEN
\r
3306 IF A.PLEAF.KIND = LITKIND OR A.PLEAF.KIND = EQUKIND THEN
\r
3307 IF A.PLEAF.KIND=A1.LLEAF.KIND AND A.PLEAF.IDENT=A1.LLEAF.IDENT
\r
3309 IF SYL_AXIOMS ( M , A1.LLEAF.LEFT , A.PLEAF.LEFT ) THEN
\r
3310 CALL ERASE_SEQ ( M.NEXT );
\r
3323 (****************************************************************************)
\r
3324 (* LOOK FOR AXIOM OF THE FORM Xi=Yi and P(X1,...,Xn) |- P(Y1,...,Yn) *)
\r
3326 UNIT SYL_AXIOMS : FUNCTION ( M : POINTER, E, F : TNODE ) : BOOLEAN;
\r
3329 BETA, ALFA : BOOLEAN;
\r
3331 WHILE E<>NONE AND F<>NONE
\r
3333 B := COPYTNODE ( E );
\r
3334 C := COPYTNODE ( F );
\r
3335 CALL ERASE ( C.RIGHT );
\r
3336 CALL ERASE ( B.RIGHT );
\r
3337 B.RIGHT := C; (* CREATE PAIR Xi->Yi *)
\r
3341 IF A.LLEAF<>NONE ANDIF A.LLEAF.KIND=EQUKIND THEN
\r
3342 D := A.LLEAF.LEFT;
\r
3344 CALL COMPARE ( D, B, ALFA ); (* SEARCH FOR RESPECTIVE PAIR *)
\r
3353 IF NOT BETA THEN RETURN FI; (* IF NOT FOUND THEN RESULT := FALSE *)
\r
3354 E := E.RIGHT; (* SEARCH FURTHER *)
\r
3355 F := F.RIGHT; (* FOR NEXT PAIR *)
\r
3360 (****************************************************************************)
\r
3361 (* LOOKING FOR NQ OR Q AXIOM *)
\r
3363 UNIT LOOK_NQ : FUNCTION ( M : POINTER, P : INTEGER ) : BOOLEAN;
\r
3365 AX2 : LIST_AXIOMS,
\r
3370 DO (* VIEW WHOLE SEQUENT *)
\r
3371 (* LOOKING FOR Q *)
\r
3373 WHEN 0 : IF A.LLEAF <> NONE THEN
\r
3374 IF A.LLEAF.KIND = BVAKIND THEN (* FOUND Q ON LEFT SIDE *)
\r
3375 IF SRCH_Q_AX ( A.LLEAF.IDENT, AX2 ) THEN
\r
3376 IF AX2.AXIOM.KIND = NEGKIND THEN
\r
3380 RESULT := FALSE (* FOUND NEGATION OF EXISTED *)
\r
3383 ELSE (* AXIOM NOT FOUND *)
\r
3384 AX2 := MAKE_AXIOM ( AX );
\r
3385 IF AX = NONE THEN AX := AX2 FI;
\r
3386 C := NEW TNODE; (* AXIOM := NOT Q *)
\r
3387 C.KIND := NEGKIND;
\r
3388 C.LEFT := COPYTNODE ( A.LLEAF );
\r
3395 WHEN 1 : IF A.PLEAF <> NONE THEN
\r
3396 IF A.PLEAF.KIND = BVAKIND THEN (* FOUND Q ON RIGHT SIDE *)
\r
3397 IF SRCH_Q_AX ( A.PLEAF.IDENT, AX2 ) THEN
\r
3398 IF AX2.AXIOM.KIND = NEGKIND THEN
\r
3399 RESULT := FALSE; (* FOUND NEGATION OF EXISTED *)
\r
3402 RESULT := TRUE; (* FOUND CORRECT AXIOM *)
\r
3404 ELSE (* AXIOM NOT FOUND *)
\r
3405 AX2 := MAKE_AXIOM ( AX );
\r
3406 IF AX = NONE THEN AX := AX2 FI;
\r
3407 AX2.AXIOM := COPYTNODE ( A.PLEAF );
\r
3418 (*****************************************************************************)
\r
3419 (* SEARCH FOR A BVAKIND IN THE SET OF AXIOMS *)
\r
3421 UNIT SRCH_Q_AX : FUNCTION ( N : INTEGER; INOUT AX2 : LIST_AXIOMS ) : BOOLEAN;
\r
3424 WHILE AX2 <> NONE
\r
3426 IF AX2.AXIOM.KIND = BVAKIND AND AX2.AXIOM.IDENT = N THEN
\r
3430 IF AX2.AXIOM.KIND = NEGKIND ANDIF AX2.AXIOM.LEFT.KIND = BVAKIND
\r
3431 AND AX2.AXIOM.LEFT.IDENT = N THEN
\r
3441 (*****************************************************************************)
\r
3442 (* CREATE A NEW AXIOM *)
\r
3444 UNIT MAKE_AXIOM : FUNCTION ( AX1 : LIST_AXIOMS ) : LIST_AXIOMS ;
\r
3446 IF AX1 = NONE THEN
\r
3447 RESULT := NEW LIST_AXIOMS;
\r
3449 CALL END_OF_AX ( AX1 );
\r
3450 AX1.NEXT := NEW LIST_AXIOMS;
\r
3451 RESULT := AX1.NEXT;
\r
3455 (*****************************************************************************)
\r
3456 (* LOOKING FOR IDENTITY AXIOM U=TAU *)
\r
3458 UNIT LOOK_IDE:FUNCTION ( A : SEQUENT ) : BOOLEAN;
\r
3459 VAR AX1 : LIST_AXIOMS,
\r
3464 IF A.PLEAF <> NONE ANDIF A.PLEAF.KIND = EQUKIND ANDIF
\r
3465 ( A.PLEAF.LEFT.KIND = VRUKIND OR A.PLEAF.LEFT.RIGHT.KIND = VRUKIND )
\r
3466 THEN (* FOUND U=TAU *)
\r
3467 CALL FUNCHECK ( A.PLEAF, ALFA );
\r
3474 CALL COMPARE ( A.PLEAF, AX1.AXIOM, ALFA );
\r
3475 IF ALFA THEN RETURN FI; (* THIS AXIOM HAS ALREADY *)
\r
3476 AX1 := AX1.NEXT; (* BEEN WRITTEN TO THE LIST *)
\r
3478 IF SEARCH_U ( A ) THEN
\r
3479 CALL END_OF_M ( M, A );
\r
3482 CALL END_OF_AX ( AX1 ); (* AXIOM NOT FOUND *)
\r
3483 IF AX = NONE THEN
\r
3484 AX1 := NEW LIST_AXIOMS;
\r
3487 AX1.NEXT := NEW LIST_AXIOMS; (* SO, THE LIST MUST BE *)
\r
3490 AX1.AXIOM := COPYTNODE ( A.PLEAF ); (* UPDATED *)
\r
3500 (*****************************************************************************)
\r
3503 (*****************************************************************************)
\r
3504 (* OUTPUT OF AXIOMS *)
\r
3505 (*****************************************************************************)
\r
3507 (*****************************************************************************)
\r
3508 (* PRINTS ALL LIST OF AXIOMS *)
\r
3510 UNIT SHOW_AX : PROCEDURE ( AX1 : LIST_AXIOMS );
\r
3512 IF AX1 <> NONE THEN
\r
3513 CALL SHOW_TREE ( AX1.AXIOM );
\r
3514 CALL SHOW_AX ( AX1.NEXT );
\r
3518 (****************************************************************************)
\r
3519 (* WRITES AXIOMS *)
\r
3521 UNIT WRITE_AXIOMS : PROCEDURE;
\r
3522 VAR AX1 : LIST_AXIOMS;
\r
3525 IF AX = NONE THEN
\r
3526 WRITE ( "IT IS TRUE WITHOUT ADDITIONAL AXIOMS" );
\r
3529 WHILE AX1 <> NONE
\r
3531 IF AX1.AXIOM.KIND = EQUKIND THEN
\r
3533 IF AX1.AXIOM.LEFT.KIND = VRUKIND THEN
\r
3534 CALL WRITE_EXPR ( AX1.AXIOM.LEFT.RIGHT )
\r
3536 CALL WRITE_EXPR ( AX1.AXIOM.LEFT );
\r
3539 CASE AX1.AXIOM.KIND
\r
3540 WHEN 7 : CALL PUTCH ( 'Q' );
\r
3541 CALL PNUM ( AX1.AXIOM.LEFT.IDENT );
\r
3542 WRITE ( " <=> FALSE" );
\r
3543 WHEN 33 : CALL PUTCH ( 'Q');
\r
3544 CALL PNUM ( AX1.AXIOM.IDENT );
\r
3545 WRITE ( " <=> TRUE" );
\r
3551 CALL ERASE_AX ( AX );
\r
3552 END WRITE_AXIOMS;
\r
3554 (****************************************************************************)
\r
3555 (* PRINT BRACKETS *)
\r
3557 UNIT PUT_BRACKET : PROCEDURE ( C : TNODE );
\r
3561 IF K=LITKIND ORIF K=FUNKIND ORIF K=42 ORIF K=43
\r
3562 ORIF K=47 ORIF K=45 ORIF K=94 THEN
\r
3563 CALL PUTCH ( '(' );
\r
3564 CALL WRITE_EXPR ( C );
\r
3565 CALL PUTCH ( ')' )
\r
3567 CALL WRITE_EXPR ( C );
\r
3571 (****************************************************************************)
\r
3574 UNIT WRITE_EXPR : PROCEDURE ( C : TNODE );
\r
3576 IF C=NONE THEN RETURN FI;
\r
3578 WHEN CN2KIND:CALL PUTCH ( 'C' );
\r
3579 CALL PNUM ( C.IDENT );
\r
3581 WHEN CNTKIND:CALL PNUM ( C.IDENT + 1 );
\r
3583 WHEN LITKIND:CALL PUTCH ( 'P' );
\r
3584 CALL PNUM ( C.IDENT );
\r
3586 IF C <> NONE THEN
\r
3587 CALL PUTCH ( '(' );
\r
3590 WHEN FUNKIND:CALL PUTCH ( 'F' );
\r
3591 CALL PNUM ( C.IDENT );
\r
3592 IF C.LEFT <> NONE THEN
\r
3593 CALL PUTCH ( '(' );
\r
3594 CALL WRITE_EXPR ( C.LEFT );
\r
3598 CALL PUTCH ( ')' )
\r
3600 CALL PUTCH ( ',' );
\r
3605 WHEN 42 :CALL PUT_BRACKET ( C.LEFT );
\r
3606 CALL PUTCH ( '*' );
\r
3607 CALL PUT_BRACKET ( C.LEFT.RIGHT );
\r
3609 WHEN 43 :CALL PUT_BRACKET ( C.LEFT );
\r
3610 CALL PUTCH ( '+' );
\r
3611 CALL PUT_BRACKET ( C.LEFT.RIGHT );
\r
3613 WHEN 45 :CALL PUT_BRACKET ( C.LEFT );
\r
3614 CALL PUTCH ( '-' );
\r
3615 CALL PUT_BRACKET ( C.LEFT.RIGHT );
\r
3617 WHEN 47 :CALL PUT_BRACKET ( C.LEFT );
\r
3618 CALL PUTCH ( '/' );
\r
3619 CALL PUT_BRACKET ( C.LEFT.RIGHT );
\r
3621 WHEN 94 :CALL PUT_BRACKET ( C.LEFT );
\r
3622 CALL PUTCH ( '^' );
\r
3623 CALL PUT_BRACKET ( C.LEFT.RIGHT );
\r
3629 (****************************************************************************)
\r
3630 (* PRINT NUMBER WITHOUT SPACES OR ZEROS CONTROLLING END OF LINE *)
\r
3632 UNIT PNUM : PROCEDURE ( N : INTEGER );
\r
3638 IF N>9 THEN I := I+1 FI;
\r
3639 IF N>99 THEN I := I+1 FI;
\r
3640 IF N>999 THEN I := I+1 FI;
\r
3641 IF N>9999 THEN I := I+1 FI;
\r
3642 IF CHARSH+1>LINLNG THEN WRITELN; CHARSH := 0 FI;
\r
3643 IF CHARSH=0 THEN WRITE(' '); FI;
\r
3645 CHARSH := CHARSH+1;
\r
3649 (****************************************************************************)
\r
3650 (* SERVES SPECIAL EXCEPTIONS - HARD EXIT FROM PROGRAM *)
\r
3654 WHEN ENDRUN: TERMINATE;
\r
3657 (****************************************************************************)
\r
3661 OPEN ( G , TEXT , UNPACK ( "RETRPROV.DAT" ) );
\r
3663 SQNT := NEW SEQUENT;
\r
3666 SQNT.PLEAF := GEN_TREE;
\r
3667 CALL LAST1_S ( SQNT.PLEAF );
\r
3668 CALL LAST1_X ( SQNT.PLEAF );
\r
3669 (* M contains f(t1,...,tn)=u or relation *)
\r
3670 WRITELN ( "PROVE WITH DEFINITION ------- 1 " );
\r
3671 WRITELN ( "PROVE WITHOUT DEFINITION ------- 2 " );
\r
3673 IF DEF_LIT = 1 THEN
\r
3674 (* M1 contains f(x1,...,xn)=Ktau or relation *)
\r
3675 OPEN ( G , TEXT , UNPACK ( "RETRPROV.DEF" ) );
\r
3680 M1.FUN_REL := GEN_TREE;
\r
3681 CALL LAST1_S ( M1.FUN_REL );
\r
3682 CALL LAST1_X ( M1.FUN_REL );
\r
3683 CALL REP_F_L ( M1 ); (* FUNKIND -> FN1KIND *)
\r
3684 (* LITKIND -> LT1KIND *)
\r
3685 CALL RULEDF_L ( M , 1 , M1.FUN_REL.LEFT.IDENT );
\r
3686 CALL RULEDF_F ( M , 1 , M1.FUN_REL.LEFT.IDENT );
\r
3690 CALL PROVE ( M , 0 );
\r
3691 CALL WRITE_AXIOMS;
\r
3694 (****************************************************************************)
\1a