perm filename PLNR.ANO[P,BGB] blob
sn#097095 filedate 1974-04-17 generic text, type T, neo UTF8
COMMENT ⊗ VALID 00049 PAGES
RECORD PAGE DESCRIPTION
00001 00001
00006 00002 ANNOTATED MICRO-PLANNER
00008 00003 α TOP LEVEL INITIALIZATION
00009 00004 α ERROR MESSAGE ROUTINE
00011 00005 α MAIN EVALUATION LOOP
00014 00006 α THE 16 KINDS OF TREE NODES
00017 00007 α STORE PLANNER VALUES
00019 00008 α FETCH PLANNER VALUES
00021 00009 (DF THBKPT (L)
00023 00010 α Push a MUNG node on thTREE and mung core.
00025 00011 FETCH-GROUP PLANNER FUNCTIONS.
00026 00012 α FETCH ASSERTIONS AND CALL CONSEQUENT THEOREMS BY PATTERN
00029 00013 (DE THGOALF NIL (COND ((THTRY1)) ((THPOPT) NIL)) )
00032 00014 (DF THFIND (THA)
00034 00015 STORE-GROUP PLANNER FUNCTIONS.
00035 00016 (DF THASSERT (THA) (THASS1 THA T) )
00036 00017 THX ≡ pattern
00038 00018 (DE THPURE (XX)
00040 00019 α ADD a theorem-tag or an assertion to the associative memory
00043 00020 α ITEM POINTER - forms the associative addressing mechanism
00046 00021 (DE THREMOVE (THB)
00048 00022 (DEFPROP THREM1
00051 00023 α thPC set in thREM1 to boolean value (KIND≠"thASSERTION")
00052 00024 α PROCESS THEOREM RECOMMENDATIONS FOR THE ASSERT & ERASE PRIMITIVES
00054 00025 MATCH-GROUP PLANNER FUNCTIONS.
00055 00026 α THMATCHING returns the shortest list of assertions (or theorem
00059 00027 α MATCH1 breaks the patterns into item pairs,
00061 00028 THX - pattern key item
00062 00029 α bind THV, THNV, THRESTRICT variables and demand match.
00065 00030 α thMATCH4 is the THV, THNV and THRESTRICT EVALuator,
00067 00031 (DF THAPPLY (L)
00068 00032 (DF THDO (A)
00070 00033 α thBIND an varlist A
00072 00034 PROG-GROUP PLANNER FUNCTIONS.
00073 00035 α Macro for pushing nodes onto list
00075 00036 (DF THPROG (THA)
00077 00037 (DF THSUCCEED (THA)
00079 00038 (DF THFAIL (THA)
00082 00039 (DE THFAIL? (PRD ACT)
00084 00040 THX ≡ tree node.
00087 00041 (DF THMESSAGE (THA)
00089 00042 (DF THUNIQUE (THA)
00091 00043 BOOL-GROUP PLANNER FUNCTIONS.
00092 00044 (DF THAMONG (THA)
00094 00045 (DF THAND (A)
00095 00046 (DF THCOND (THA)
00097 00047 IO-GROUP PLANNER FUNCTIONS.
00098 00048 (DE THSEMI NIL
00100 00049 (DE THDUMP NIL
00102 ENDMK
⊗;
ANNOTATED MICRO-PLANNER
editing and commentary by B. g. Baumgart
S-expr from Sussman and Winograd via Orban
SECTIONS
1. MAIN
2. FETCH
3. STORE
4. MATCH
5. DO & BIND
6. PROG
7. BOOL
8. IO
SECTION 1.
MAIN PLANNER FUNCTION (including the Value and Lispish primitives).
thINIT;
thERT (error);
thVAL(thexp,thalist);
success-failure jump table
thSETQ (var-expr-pairs);
thVSETQ(var-expr-pairs);
thV1 (x);
thV(varname);
thNV(varname);
thASVAL(varname);
thSGAL(varname); get value of X from Alist;
thGAL(var,alist);
thBKPT(break-message);
thFLUSH (indicators);
thMUNGF;
thMUNGT;
thNOFAIL (flag);
thPUTPROP (name value indicator);
thREMPROP (name indicator);
thRPLACA (destination source);
thRPLACAS (destination source);
thURPLACA (destination source);
thRPLACD (destination source);
thRPLACDS (destination source);
thRUPLACD (destination source);
α TOP LEVEL INITIALIZATION;
(DF THINIT
(PROG NIL
(SETQ ↑A NIL)
(SETQ THSTEP NIL)
(SETQ THSTEPD NIL)
(SETQ THSTEPT NIL)
(SETQ THSTEPF NIL)
(SETQ THXX NIL)
(SETQ THTRACE NIL)
(SETQ THALIST (QUOTE ((NIL NIL))))
(MAPC (FUNCTION EVAL) (SETQ ERRLIST
@((TERPRI)
(PRINC (QUOTE micro-PLANNER/ #135 ))
(SETQ ERRLIST (CDDDR ERRLIST))
(SETQ LEVEL# -1)
(SETQ THINF NIL)
(SETQ THTREE NIL)
(SETQ THLEVEL NIL)
(THERT TOP LEVEL)) ))
(RETURN @EXIT)
))
α ERROR MESSAGE ROUTINE;
(DF THERT (ERTA)
(PROG (LISTEN ↑W ↑Q)
(SETQ LEVEL# (ADD1 LEVEL#))
(PRINT (QUOTE >>>))
(MAPC (FUNCTION THPRINT2) ERTA)
(PRINT @LISTENING)
(OR THLEVEL (THPRINT2 @THVAL))
LISTEN
(SETQ THINF NIL)
(TERPRI)(PRINC LEVEL#)(PRINC @!)
α MAIN LISTEN LOOP.
α when T decrem level and return to THINIT.
(COND ((EQ (SETQ LISTEN (READ)) @T)
(SETQ LEVEL# (SUB1 LEVEL#))
(RETURN T))
α when NIL decrem level.
((AND THLEVEL (NULL LISTEN))
(SETQ THINF T)
(SETQ LEVEL# (SUB1 LEVEL#))
(RETURN NIL))
α when sharp sign "#" decrem level and set ANS.
((AND (NOT (ATOM LISTEN))(EQ (CAR LISTEN) (QUOTE #)))
(SETQ LEVEL# (SUB1 LEVEL#))
(RETURN (SETQ ANS (CDR LISTEN))))
(THLEVEL (ERRSET (PRINT (EVAL LISTEN))))
α MAIN call for EVALUATION.
(T (ERRSET (PRINT (THVAL LISTEN THALIST))) ))
(GO LISTEN)
))
(DE THPRINT2 (X)
(PROG NIL (PRINC (QUOTE / )) (RETURN (PRINC X))))
α MAIN EVALUATION LOOP;
(DE THVAL (THEXP THALIST)
(PROG NIL
(SETQ THLEVEL (CONS (LIST THTREE THALIST) THLEVEL))
(RETURN
(PROG (THTREE THVALUE THBRANCH THOLIST THABRANCH THE THV THMESSAGE)
(SETQ THV @(THV THNV))
GO (SETQ THE THEXP)
(SETQ THEXP NIL)
(COND (↑A (SETQ ↑A NIL) (OR (THERT ↑A /- THVAL) (GO FAIL))))
(COND (THSTEP (EVAL THSTEP)))
α MAIN EXECUTION;
(COND ((ERRSET (SETQ THVALUE (EVAL THE))))
(T (PRINT THE) (SETQ THVALUE (THERT LISPERROR /- THVAL))))
GO1 (COND (THSTEPD (EVAL THSTEPD)))
(COND (THINF (GO FAIL)) α infinite failure.
(THEXP (GO GO)) α continue.
(THVALUE (GO SUCCEED)) α success.
(T (GO FAIL))) α failure.
SUCCEED
(COND (THSTEPT (EVAL THSTEPT)))
(COND ((NULL THBRANCH)
(SETQ THBRANCH THTREE)
(SETQ THABRANCH THALIST)))
(COND ((NULL THTREE)
(SETQ THLEVEL (CDR THLEVEL))
(RETURN THVALUE))
((SETQ THEXP (GET (CAAR THTREE) @THSUCCEED))
(SETQ THVALUE ((PROG2 0 THEXP (SETQ THEXP NIL))))
(GO GO1) )
((THERT BAD SUCCEED /- THVAL) (GO SUCCEED))
((GO FAIL)))
FAIL
(COND (THSTEPF (EVAL THSTEPF)))
(COND ((NULL THTREE)
(SETQ THLEVEL (CDR THLEVEL))
(RETURN NIL))
((AND THMESSAGE
(COND ((MEMQ (CAAR THTREE)
@(THMUNG THFAIL? THTRACES THMESSAGE
THPROG THAND THASSERT THERASE
THREMBIND THDO THUNDO)) NIL)
(T (THPOPT) (GO FAIL)) )))
((SETQ THEXP (GET (CAAR THTREE) @THFAIL))
(SETQ THVALUE ((PROG2 0 THEXP (SETQ THEXP NIL))))
(GO GO1) )
((THERT BAD FAIL /- THVAL) (GO SUCCEED))
((GO FAIL)))
)) ))
α THE 16 KINDS OF TREE NODES;
α SUCCESS-FAILURE JUMP TABLE - ACCESSED BY thVAL;
α FOUR VALUE TREE NODES;
(DEFPROP THMUNG THMUNGT THSUCCEED)
(DEFPROP THMUNG THMUNGF THFAIL)
(DEFPROP THREMBIND THREMBINDT THSUCCEED)
(DEFPROP THREMBIND THREMBINDF THFAIL)
(DEFPROP THDO THDOB THSUCCEED)
(DEFPROP THDO THDOB THFAIL)
(DEFPROP THUNDO THUNDOF THFAIL)
(DEFPROP THUNDO THUNDOT THSUCCEED)
α FOUR ASSOCIATIVE TREE NODES;
(DEFPROP THASSERT THASSERTT THSUCCEED)
(DEFPROP THASSERT THASSERTF THFAIL)
(DEFPROP THERASE THERASET THSUCCEED)
(DEFPROP THERASE THERASEF THFAIL)
(DEFPROP THGOAL THGOALT THSUCCEED)
(DEFPROP THGOAL THGOALF THFAIL)
(DEFPROP THFIND THFINDF THFAIL)
(DEFPROP THFIND THFINDT THSUCCEED)
α FOUR PROG TREE NODES;
(DEFPROP THPROG THPROGT THSUCCEED)
(DEFPROP THPROG THPROGF THFAIL)
(DEFPROP THTAG THTAGF THFAIL)
(DEFPROP THTAG THTAGT THSUCCEED)
(DEFPROP THFAIL? THFAIL?F THFAIL)
(DEFPROP THFAIL? THFAIL?T THSUCCEED)
(DEFPROP THMESSAGE THMESSAGEF THFAIL)
(DEFPROP THMESSAGE THMESSAGET THSUCCEED)
α FOUR BOOLEAN TREE NODES;
(DEFPROP THAND THANDT THSUCCEED)
(DEFPROP THAND THANDF THFAIL)
(DEFPROP THOR THORT THSUCCEED)
(DEFPROP THOR THORF THFAIL)
(DEFPROP THAMONG THAMONGF THFAIL)
(DEFPROP THCOND THCONDT THSUCCEED)
(DEFPROP THCOND THCONDF THFAIL)
α STORE PLANNER VALUES;
(DF THSETQ (THL1)
(PROG (THML THL) α THML is the mung list & THL is the arg list.
(SETQ THL THL1)
LOOP (COND ((NULL THL)
(THPUSH THTREE (LIST @THMUNG THML))
(RETURN THVALUE))
((NULL (CDR THL))
(PRINT THL1)
(THERT ODD NUMBER OF GOODIES /- THSETQ))
((ATOM (CAR THL)) α LISP expr;
(THPUSH THML
(LIST @SETQ (CAR THL) (LIST @QUOTE (EVAL (CAR THL)))))
(SET (CAR THL) (SETQ THVALUE (EVAL (CADR THL))) ))
(T (THRPLACAS (CDR (THSGAL (CAR THL))) α u-PLNR expr;
(SETQ THVALUE
(THVAL (CADR THL) THALIST)) )) )
(SETQ THL (CDDR THL))
(GO LOOP)
))
α can not be undone on failure propagation;
(DF THVSETQ (THA)
(PROG (A)
(SETQ A THA)
LOOP (COND ((NULL A) (RETURN THVALUE))
((NULL (CDR A))
(PRINT THA)
(THERT ODD NUMBER OF GOODIES /- THSETQ))
(T (SETQ THVALUE
(CAR (RPLACA (CDR (THSGAL (CAR A)))
(THVAL (CADR A) THALIST) )) )) )
(SETQ A (CDDR A))
(GO LOOP)
))
α FETCH PLANNER VALUES;
(DF THV (X) (THV1 (CAR X)) )
(DF THNV (X) (THV1 (CAR X)) )
(DE THV1 (X)
(PROG NIL
(SETQ THXX X)
(RETURN (COND
( (EQ (SETQ X (CADR(SASSQ X THALIST
(FUNCTION (LAMBDA NIL
(PROG NIL
(PRINT THXX)
(RETURN (THERT THUNBOUND /- THV1))
))) )))
@THUNASSIGNED)
(PRINT THXX)
(THERT THUNASSIGNED /- THV1))
(T X)))))
))
(DF THASVAL (X)
((LAMBDA (X)
(AND X (NOT (EQ (CADR X) @THUNASSIGNED)) ))
(THGAL (CAR X) THALIST)) )
))
α Get the value of X from thALIST or set X to thUNASSIGNED;
α SASSQ ≡ SASSOC.
(DE THSGAL (X)
(SASSQ (CADR X) THALIST
α WHEN X NOT ON thALIST, ALIST ← ALIST*(((CADR X)thUNASSIGNED));
(FUNCTION (LAMBDA NIL
(PROG (Y)
(SETQ Y (LIST (CADR X) @THUNASSIGNED))
(NCONC (GET @THALIST @VALUE) (LIST Y))
(RETURN Y)
))) ))
α Get the value of X from Y list or complain;
(DE THGAL (X Y)
(PROG NIL
(SETQ THXX X)
(RETURN
(SASSQ (CADR X) Y
α WHEN X NOT ON Y-LIST, give an error message.
(FUNCTION (LAMBDA NIL
(PROG NIL
(PRINT THXX)
(RETURN (THERT THUNBOUND THGAL))
))) ))) )
(DF THBKPT (L)
(OR (AND THTRACE (THTRACES @THBKPT L)) THVALUE)
)
α thFLUSH removes lists of properties from your LISP image;
(DE THFLUSH (A)
(MAPC (FUNCTION (LAMBDA (B)
(MAPC (FUNCTION (LAMBDA (C)
(MAPC (FUNCTION (LAMBDA (D)
(REMPROP D B))) C))) OBLIST))) A))
)
α MUNG on failure restores old values from the tree;
(DE THMUNGF ()
(PROG NIL
(EVLIS (CADAR THTREE))
(THPOPT)
(RETURN NIL)
))
α MUNG on success prunes the tree, the old values will never be needed;
(DE THMUNGT ()
(PROG NIL
(THPOPT)
(RETURN THVALUE)
))
α MODIFY THE PROG ENTRY IN THE SUCCESS-FAIL JUMP TABLE;
(DE THNOFAIL (THX)
(COND (THX (DEFPROP THPROG THPROGT THFAIL))
(T (DEFPROP THPROG THPROGF THFAIL))
))
α Push a MUNG node on thTREE and mung core.
(DE THPUTPROP (ATO VAL IND) α atom, value, indicator.
(PROG NIL
(THPUSH THTREE
(LIST @THMUNG(LIST(LIST @PUTPROP1
(LIST @QUOTE ATO)
(LIST @QUOTE (GET ATO IND))(LIST @QUOTE IND) )) ))
(RETURN (PUTPROP1 ATO VAL IND))
))
(DE THREMPROP (ATO IND)
(PROG NIL
(THPUSH THTREE
(LIST @THMUNG(LIST(LIST @PUTPROP1
(LIST @QUOTE ATO)(LIST @QUOTE (GET ATO IND))
(LIST @QUOTE IND)))))
(RETURN (REMPROP ATO IND))
))
α push on Mung List, and push MUNG node on thTREE.
(DE THRPLACA (X Y)
(PROG (THML)
(THRPLACAS X Y)
(THPUSH THTREE (LIST @THMUNG THML))
(RETURN X)
))
(DE THRPLACD (X Y)
(PROG (THML)
(THRPLACDS X Y)
(THPUSH THTREE (LIST @THMUNG THML))
(RETURN X)
))
α Push mung operations onto THML, which is bound elsewhere.
(DE THRPLACAS (X Y)
(PROG NIL
(THPUSH THML (LIST @THURPLACA X (CAR X)))
(RETURN (RPLACA X Y))
))
(DE THRPLACDS (X Y)
(PROG NIL
(THPUSH THML (LIST @THURPLACD X (CDR X)))
(RETURN (RPLACD X Y))
))
α The gods forgive those things we ought not to have done.
(DF THURPLACA (L) (RPLACA (CAR L) (CADR L)))
(DF THURPLACD (L) (RPLACD (CAR L) (CADR L)))
FETCH-GROUP PLANNER FUNCTIONS.
thGOAL(arg);
thGOALF;
thGOALT;
thTRY1;
thTRY(x);
thFIND(arg);
thFINDF;
thFINDT;
α FETCH ASSERTIONS AND CALL CONSEQUENT THEOREMS BY PATTERN;
THA1 ≡ recommendations
THA2 ≡ pattern-key
THX ≡ pattern-hits
THY ≡ pattern-hits from data base
THY1 ≡ have done data base search.
THZ ≡ pattern-hits from theorem base.
THZ1 ≡ have done theorem base search.
(DF THGOAL (THA)
(PROG (THX THY THY1 THZ THZ1 THA1 THA2 THV)
(SETQ THV @(THV))
(SETQ THA2 (THVARSUBST (CAR THA)))
(SETQ THA1 (CDR THA))
α data base search when no recommendations or ((rec1≠THNODB)∧(rec1≠THDBF));
(COND
((OR (NULL THA1)
(AND (NOT (AND (EQ (CAAR THA1) @THNODB)
(PROG2 (SETQ THA1 (CDR THA1)) T) ))
(NOT (EQ (CAAR THA1) @THDBF))) )
(SETQ THY1 T)
(SETQ THX (LIST (LIST @THDBF @THTRUE
(SETQ THY (THMATCHDB THA2)) )) ) ))
α theorem base search;
(SETQ THX (NCONC THX (MAPCAR (FUNCTION THTRY) THA1)))
(AND THTRACE (THTRACES @THGOAL THA2))
(THPUSH THTREE (LIST @THGOAL THA2 THX))
(RETURN NIL)
))
(DE THTRY (X) α X ≡ recommendation; THA2 ≡ pattern-key;
(COND
1. ((EQ (CAR X) @THTBF)
(LIST @THTBF
(CADR X)
(COND (THZ1 THZ)
((SETQ THZ1 T)
(SETQ THZ (THMATCHTB THA2 @THCONSE)) )) ))
2. ((EQ (CAR X) @THDBF)
(LIST @THDBF (CADR X)
(COND (THY1 THY)
((SETQ THY1 T)
(SETQ THY (THMATCHDB THA2)) )) ))
3. ((EQ (CAR X) @THUSE) (LIST @THTBF @THTRUE (CDR X)))
4. (T (PRINT X) (THERT UNCLEAR RECOMMENDATION /- THTRY))
))
(DE THGOALF NIL (COND ((THTRY1)) ((THPOPT) NIL)) )
(DE THGOALT
(PROG2 0
(COND ((EQ THVALUE @THNOVAL)
(THVARSUBST (CADAR THTREE)))
(THVALUE))
(THPOPT)
))
α THTRY1 called only by thGOALF;
THX ≡ (THDBF filter) or (THTBF filter)
THY ≡ pattern-hits
THZ ≡ thgoal-node ≡ [THGOAL pattern-key pattern-hits]
THW ≡ assertion-bucket or theorem-body
(DE THTRY1 NIL
(PROG (THX THY THZ THW THEOREM)
(SETQ THZ (CAR THTREE)) α get thgoal-node;
(SETQ THY (CDDR THZ)) α get pattern hits;
THGOAL3
(COND ((NULL (CAR THY)) (RETURN NIL))) α return FAILURE;
(SETQ THX (CAAR THY))
(GO (CAR THX))
α Data Base Pattern Filtering.
THDBF (SETQ THOLIST THALIST)
(COND ((NULL (CADDR THX))
(RPLACA THY (CDAR THY))
(GO THGOAL3))
((PROG2 0
(AND ((CADR THX) (SETQ THW (CAADDR THX)))
(THMATCH1 (CADR THZ) (CAR THW)) )
(RPLACA (CDDR THX) (CDADDR THX)) )
(RETURN THW))
(T (GO THDBF)))
α Theorem base pattern filtering.
THTBF
(COND ((NULL (CADDR THX))
(RPLACA THY (CDAR THY))
(GO THGOAL3))
((NOT
(AND (SETQ THW
(GET (SETQ THEOREM (CAADDR THX)) @THEOREM))
(EQ (CAR THW) @THCONSE)))
(PRINT THEOREM)
(THERT BAD THEOREM /- THTRY1))
((PROG2 0
(AND ((CADR THX) (CAADDR THX))
(THAPPLY1 THEOREM THW (CADR THZ)))
(RPLACA (CDDR THX) (CDADDR THX)))
(RETURN T))
(T (GO THTBF)))
))
(DF THFIND (THA)
(PROG NIL
(THBIND (CADDR THA))
(THPUSH THTREE
(LIST @THFIND
(COND ((EQ (CAR THA) @ALL) @(1 NIL NIL))
((ATOM (CAR THA)) (LIST (CAR THA) (CAR THA) T))
((CAR THA)))
(CONS 0 NIL)
(CADR THA)))
(THPUSH THTREE (LIST @THPROG (CDDR THA) NIL (CDDR THA)))
(RETURN (THPROGA))
))
(DEFPROP THFINDF NIL
(PROG NIL
(SETQ THBRANCH NIL)
(RETURN
(COND ((LESSP (CAADR (SETQ THXX (CDAR THTREE)))
(CAAR THXX)) (THPOPT) NIL)
(T (THPOPT) (CDADR THXX))))
))
(DE THFINDT NIL
(PROG (THX THY THZ THCDAR)
(AND (MEMBER (SETQ THX
(COND
((THVAR (SETQ THZ (CADDR (SETQ THCDAR (CDAR THTREE))))) (THVARS2 THZ))
((THVARSUBST THZ))))
(CADR THCDAR))
(GO GO))
(RPLACD (CADR THCDAR) (CONS THX (CDADR THCDAR)))
(AND (EQ (SETQ THY (ADD1 (CAADR THCDAR))) (CADAR THCDAR))
(RETURN (PROG2 (SETQ THBRANCH NIL)
(AND (CADDAR THCDAR) (CDADR THCDAR))
(THPOPT))))
(RPLACA (CADR THCDAR) THY)
GO (SETQ THTREE THBRANCH)
(SETQ THALIST THABRANCH)
(SETQ THBRANCH NIL)
(RETURN NIL)
))
STORE-GROUP PLANNER FUNCTIONS.
thASSERT(arg);
thASSERTF;
thASSERTT;
thERASE(arg);
thERASEF;
thERASET
thASS1(arg,flg);
thPURE
thVARS2
thVARSUBST
thVAR
thADD
thIP
thREM1
thBA
thBAP
thREMOVE
thTAE
thTRUE
(DF THASSERT (THA) (THASS1 THA T) )
(DE THASSERTF NIL
(PROG NIL
(THREMOVE (COND ((ATOM (CADAR THTREE))
(CADAR THTREE))
(T (CAADAR THTREE)) ))
(THPOPT)
(RETURN NIL)
))
(DE THASSERTT NIL (PROG2 0 (CADAR THTREE) (THPOPT)) )
(DF THERASE (THA) (THASS1 THA NIL) )
(DE THERASEF NIL
(PROG NIL
(THADD (COND ((ATOM (CADAR THTREE))
(CADAR THTREE))
(T (CAADAR THTREE)))
(COND ((ATOM (CADAR THTREE)) NIL)
(T (CDADAR THTREE))))
(THPOPT)
(RETURN NIL)))
))
(DE THERASET NIL (PROG2 0 (CADAR THTREE) (THPOPT)) )
THX ≡ pattern
THA ≡ recommendations
THY ≡ property-list
(DE THASS1 (THA P)
(PROG (THX THY1 THY TYPE PSEUDO)
α detect thPSEUDO recommendation.
(AND (CDR THA)
(EQ (CAADR THA) @THPSEUDO)
(SETQ PSEUDO T) )
α assertion purity test, (one depth of variables);
(OR (ATOM (SETQ THX (CAR THA)))
(THPURE (SETQ THX (THVARSUBST THX)))
PSEUDO
(PROG2 (PRINT THX)
(THERT IMPURE ASSERTION OR ERASURE /- THASS1)) )
α trace diagonostic.
(AND THTRACE
(NOT PSEUDO)
(THTRACES (COND (P @THASSERT) (@THERASE)) THX))
α ignore, add or remove the assertion.
(SETQ THA (COND (PSEUDO (CDDR THA)) ((CDR THA))))
(OR (SETQ THX
(COND (PSEUDO (LIST THX))
(P
(THADD THX (SETQ THY (COND
((AND THA (EQ (CAAR THA) @THPROP))
(PROG2 0 (EVAL (CADAR THA)) (SETQ THA (CDR THA))))))))
(T (THREMOVE THX))))
(RETURN NIL))
α push an assert or erase node into thTREE and chain a thDO node.
(COND (P (SETQ TYPE @THANTE)) ((SETQ TYPE @THERASING)))
(OR PSEUDO
(THPUSH THTREE (LIST (COND (P @THASSERT) (@THERASE)) THX THY)))
(SETQ THEXP (CONS @THDO (MAPCAN (FUNCTION THTAE) THA)))
(RETURN THX)
))
(DE THPURE (XX)
(ERRSET (MAPC (FUNCTION (LAMBDA (Y)
(AND (THVAR Y) (ERR NIL)))) XX))
)
(DE THVARS2 (X)
(PROG (A)
(AND (EQ (CAR X) @THEV)
(SETQ X (THVAL (CADR X) THALIST)))
(OR (MEMQ (CAR X) THV) (RETURN X))
(SETQ A (THGAL X THALIST))
(RETURN (COND ((EQ (CADR A) @THUNASSIGNED) X)
(T (CADR A)) ))
))
(DE THVARSUBST (THX)
(PROG NIL
(COND ((EQ (CAR THX) @THEV)
(SETQ THX (THVAL (CADR THX) THALIST)))
((MEMQ (CAR THX) THV) (SETQ THX (EVAL THX))))
(RETURN (COND ((ATOM THX) THX)
(T (MAPCAR (FUNCTION THVARS2) THX))))
))
(DE THVAR (X) (MEMQ (CAR X) @(THV THNV)) )
α ADD a theorem-tag or an assertion to the associative memory;
THWH ≡ kind-of-theorem
THT1 ≡ theorem-body TTL ≡ assertion-bucket
(DE THADD (THTT THPL) α THTT ≡ theorem-name or assertion.
α THPL ≡ property-list.
(PROG (THNF THWH THCK THLAS THTTL THT1 THFST THFSTP THFOO)
(SETQ THCK (COND
1. ((ATOM THTT)
α theorem tag.
(OR (SETQ THT1 (GET THTT @THEOREM))
(PROG2 (PRINT THTT)
(THERT CANT THASSERT/, NO THEOREM /- THADD)))
(SETQ THWH (CAR THT1)) α kind of theorem.
(SETQ THTTL THTT)
α while property list not null do putproping onto theorem.
(AND THPL
(PROG NIL
LP (THPUTPROP THTT (CADR THPL) (CAR THPL))
(COND ((SETQ THPL (CDDR THPL)) (GO LP)))
))
(CADDR THT1)) α theorem's pattern-key.
α break out on auxillary.
2. ((EQ (CAR THTT) @THAUX)
(RETURN ((GET (CADR THTT) @THADD) (CADDR THTT) THPL)))
α assertion.
3. (T (SETQ THWH @THASSERTION)
(SETQ THTTL (CONS THTT THPL)) THTT)))
(SETQ THNF 0)
(SETQ THLAS (LENGTH THCK))
(SETQ THFST T)
THP1 (COND
1. ((NULL THCK)
(SETQ THCK THFOO)
(SETQ THNF 0)
(SETQ THFOO (SETQ THFST NIL))
(SETQ THFSTP T)
(GO THP1))
2. ((NULL (SETQ THT1 (THIP (CAR THCK))))
(RETURN NIL))
3. ((EQ THT1 @THOK))
4. ((SETQ THFOO (NCONC THFOO (LIST
(COND ((EQ THT1 @THVRB) (CAR THCK))))))
(SETQ THCK (CDR THCK))
(GO THP1)))
α add the rest of the assertion to the associative memory.
(SETQ THFST NIL)
(MAPC (FUNCTION THIP) (CDR THCK))
(SETQ THNF 0)
(MAPC (FUNCTION THIP) THFOO)
(RETURN THTTL)
))
α ITEM POINTER - forms the associative addressing mechanism;
THWH ≡ kind of pattern thASSERTION, thCONSE, thANTE or thERASING;
THLAS ≡ length of assertion, i.e. the calling-key;
THTTL ≡ the assertion being entered into the index;
(DE THIP (THI)
(PROG (THT1 THT3 THSV THT2 THI1)
(SETQ THNF (ADD1 THNF))
α test for atomic item.
(COND
1. ((AND (ATOM THI)
(NOT (EQ THI @?))
(NOT (NUMBERP THI)))
(SETQ THI1 THI))
2. ((OR (EQ THI @?)
(MEMQ (CAR THI) @(THV THNV)))
(COND (THFST (RETURN @THVRB))
((SETQ THI1 @THVRB)) ))
3. ((RETURN @THVRB))
)
α create or modify the item buckets.
(COND
1. ((NOT (SETQ THT1 (GET THI1 THWH)))
(PUTPROP THI1(LIST NIL(LIST THNF(LIST THLAS 1 THTTL)))THWH))
2. ((EQ THT1 @THNOHASH) (RETURN @THBQF))
3. ((NOT (SETQ THT2 (ASSQ THNF (CDR THT1))))
(NCONC THT1 (LIST (LIST THNF (LIST THLAS 1 THTTL))) ))
4. ((NOT (SETQ THT3 (ASSQ THLAS (CDR THT2))))
(NCONC THT2 (LIST (LIST THLAS 1 THTTL))))
5. ((AND (OR THFST THFSTP)
(COND ((EQ THWH @THASSERTION)
(ASSOC THTT (CDDR THT3)))
(T (MEMQ THTT (CDDR THT3)))))
(RETURN NIL))
6. ((SETQ THSV (CDDR THT3))
(RPLACA (CDR THT3) (ADD1 (CADR THT3)))
(RPLACD (CDR THT3) (NCONC (LIST THTTL) THSV)))
)
(RETURN @THOK)
))
(DE THREMOVE (THB)
(PROG (THB1 THWH THNF THAL THON THBS THFST THFSTP THFOO)
(SETQ THNF 0)
(SETQ THB1
(COND ((ATOM THB)
(SETQ THBS THB)
(SETQ THWH (CAR (SETQ THB1 (GET THB @THEOREM))))
(CADDR THB1))
((EQ (CAR THB) @THAUX)
(RETURN ((GET (CADR THB) @THREMOVE) (CADDR THB))))
((SETQ THWH @THASSERTION) (SETQ THBS THB))))
(SETQ THAL (LENGTH THB1))
(SETQ THFST T)
THP1 (COND ((NULL THB1)
(SETQ THB1 THFOO)
(SETQ THNF 0)
(SETQ THFST (SETQ THFOO NIL))
(SETQ THFSTP T)
(GO THP1))
((NULL (SETQ THON (THREM1 (CAR THB1))))
(RETURN NIL))
((MEMQ THON (QUOTE (THBQF THVRB)))
(SETQ THFOO
(NCONC THFOO
(LIST
(COND ((EQ THON @THVRB) (CAR THB1))))))
(SETQ THB1 (CDR THB1))
(GO THP1)))
(SETQ THFST NIL)
(MAPC (FUNCTION THREM1) (CDR THB1))
(SETQ THNF 0)
(MAPC (FUNCTION THREM1) THFOO)
(RETURN THON)
))
(DEFPROP THREM1
(LAMBDA(THB)
(PROG (THA THSV THA1 THA2 THA3 THA4 THA5 THONE THPC)
(SETQ THNF (ADD1 THNF))
(COND ((AND (ATOM THB)
(NOT (EQ THB @?))
(NOT (NUMBERP THB)))
(SETQ THA THB))
((OR (EQ THB @?) (MEMQ (CAR THB) (QUOTE (THV THNV))))
(COND (THFST (RETURN @THVRB)) ((SETQ THA @THVRB))))
((RETURN @THVRB)))
(SETQ THA1 (GET THA THWH))
(OR THA1 (RETURN NIL))
(AND (EQ THA1 @THNOHASH) (RETURN @THBQF))
(SETQ THA2 (THBA THNF THA1))
(OR THA2 (RETURN NIL))
(SETQ THA3 (THBA THAL (CADR THA2)))
(OR THA3 (RETURN NIL))
(SETQ THA4 (CADR THA3))
(SETQ THPC (NOT (EQ THWH @THASSERTION)))
(SETQ THA5
(COND ((OR THFST THFSTP)
(THBAP THBS (CDR THA4)))
((THBA (COND (THPC THON)
(T (CAR THON)))
(CDR THA4)))))
(OR THA5 (RETURN NIL))
(SETQ THONE (CADR THA5))
(RPLACD THA5 (CDDR THA5))
(AND (NOT (EQ (CADR THA4) 1))
(OR (SETQ THSV (CDDR THA4)) T)
(RPLACA (CDR THA4) (SUB1 (CADR THA4)))
(RETURN THONE))
(SETQ THSV (CDDR THA3))
(RPLACD THA3 THSV)
(AND (CDADR THA2) (RETURN THONE))
(SETQ THSV (CDDR THA2))
(RPLACD THA2 THSV)
(AND (CDR THA1) (RETURN THONE))
(REMPROP THA THWH)
(RETURN THONE)))
EXPR)
α thPC set in thREM1 to boolean value (KIND≠"thASSERTION");
(DE THBA (TH1 TH2)
(PROG (THP)
(SETQ THP TH2)
THP1 (AND (EQ (COND (THPC (CADR THP))
(T (CAADR THP)) ) TH1)
(RETURN THP))
(OR (CDR (SETQ THP (CDR THP))) (RETURN NIL))
(GO THP1)
))
(DE THBAP (TH1 TH2)
(PROG (THP)
(SETQ THP TH2)
THP1 (AND (EQUAL (COND (THPC (CADR THP))
(T (CAADR THP))) TH1)
(RETURN THP))
(OR (CDR (SETQ THP (CDR THP))) (RETURN NIL))
(GO THP1)
))
α PROCESS THEOREM RECOMMENDATIONS FOR THE ASSERT & ERASE PRIMITIVES;
α thTAE returns a list of (thAPPLY theorem assertions)'s
derived from the recommendations.
TYPE ≡ "THANTE" or "THERASING" implicit arg from thASS1;
THY1 ≡ thMATCHTB has been called flag
THY ≡ pattern-hits from thMATCHTB;
(DE THTAE (XX)
α process the THUSE recommendations.
(COND ((EQ (CAR XX) @THUSE)
(MAPCAR (FUNCTION (LAMBDA(X)
(COND
((NOT (AND (SETQ THXX (GET X @THEOREM))
(EQ (CAR THXX) TYPE)))
(PRINT X)
(THERT BAD THEOREM /- THTAE))
((LIST @THAPPLY X (CAR THX))))))
(CDR XX)))
α process the THTBF recommendations.
((EQ (CAR XX) @THTBF)
(MAPCAN (FUNCTION (LAMBDA (Y)
(COND
(((CADR XX) Y)
(LIST (LIST @THAPPLY Y (CAR THX)))))))
(COND (THY1 THY)
((SETQ THY1 T)
(SETQ THY (THMATCHTB (CAR THX) TYPE))))))
(T (PRINT XX) (THERT UNCLEAR RECCOMMENDATION /- THTAE))))
EXPR)
(DEFPROP THTRUE
(LAMBDA (X) T)
EXPR)
MATCH-GROUP PLANNER FUNCTIONS.
thMATCHDB (pattern-key); called by thGOAL & thTRY.
thMATCHTB (pattern-key,theorem-kind); called by thTRY & thTAE.
thMATCHLIST(pattern-key,pattern-kind);
thMATCH1(thx,thy); called by thTRY & thMESSAGE.
EVLIS
thMATCH2(thx,thy);
thRESTRICT
thCHECK
thUNION
α THMATCHING returns the shortest list of assertions (or theorem
names) that match the key-pattern in one item occurence (by var or by
constant) and that are the same length as the key pattern.
(DE THMATCHDB (THV) (THMATCHLIST THV @THASSERTION) )
(DE THMATCHTB (THU THV) (THMATCHLIST THU THV) )
(DE THMATCHLIST (THTB THWH) α THTB pattern-key,THWH kind-of-pattern.
(PROG (THB1 THB2 THL THNF THAL THA1 THA2 THRN THL1 THL2 THRVC)
α ESCAPE FOR PEOPLE WHO KNOW BETTER.
(COND ((EQ (CAR THTB) @THAUX)
(RETURN((GET(CADR THTB)@THMATCHLIST)(CADDR THTB)THWH))))
α INITIALIZATION.
(SETQ THL 55571) α patterns found min cnt
(SETQ THNF 0) α item position in pattern.
(SETQ THAL (LENGTH THTB)) α length of pattern-key.
(SETQ THB1 THTB) α pattern-key remaining.
α TEST FOR END OF PATTERN-KEY, ELSE GET NEXT ITEM.
THP1 (OR THB1 (RETURN (COND (THL2 (APPEND THL1 THL2)) (THL1))))
(SETQ THNF (ADD1 THNF)) α item position in pattern.
(SETQ THB2 (CAR THB1)) α current item of pattern-key.
(SETQ THB1 (CDR THB1)) α pattern-key remaining.
α FIND CONSTANTS THAT MATCH AT THIS ITEM POSITION OF THE PATTERN-KEY.
THP3 (COND ((OR (NULL (ATOM THB2))
(NUMBERP THB2)
(EQ THB2 @?)) (GO THP1))
((NOT (SETQ THA1 (GET THB2 THWH))) (SETQ THA1 @(0 0)))
((EQ THA1 @THNOHASH) (GO THP1))
((NOT (SETQ THA1 (ASSQ THNF (CDR THA1))))
(SETQ THA1 @(0 0)))
((NOT (SETQ THA1 (ASSQ THAL (CDR THA1))))
(SETQ THA1 @(0 0))))
(SETQ THRN (CADR THA1)) α number of patterns in this bucket.
(SETQ THA1 (CDDR THA1)) α list of patterns in this bucket.
(AND (EQ THWH @THASSERTION) (GO THP2))
α THEOREMS PATTERNS ONLY - check for var at this position.
(COND ((NOT (SETQ THA2 (GET @THVRB THWH))) (SETQ THA2 @(0 0)))
((NOT (SETQ THA2 (ASSQ THNF (CDR THA2)))) α position.
(SETQ THA2 @(0 0)))
((NOT (SETQ THA2 (ASSQ THAL (CDR THA2)))) α length.
(SETQ THA2 @(0 0))))
(SETQ THRVC (CADR THA2)) α replacement var count.
(SETQ THA2 (CDDR THA2)) α the patterns in this bucket.
(AND (GREATERP (PLUS THRVC THRN) THL) (GO THP1))
α THEOREM PATTERNS ONLY - minimize pattern hits.
(SETQ THL (PLUS THRVC THRN)) α total pattern hits.
(SETQ THL1 THA1) α constant patterns.
(SETQ THL2 THA2) α var patterns.
(GO THP1)
α ASSERTIONS PATTERNS ONLY - minimize pattern hits.
THP2 (COND ((EQ THRN 0) (RETURN NIL))
((GREATERP THL THRN) (SETQ THL1 THA1) (SETQ THL THRN))
(GO THP1)
))
α MATCH1 breaks the patterns into item pairs,
α and calls MATCH2 to do the u-PLNR UNIFICATION.
α THX - PATTERN-KEY
α THY - PATTERN-TAG
(DE THMATCH1 (THX THY)
(PROG (THML) α THE MUNG LIST.
α excape to a far better world.
(COND ((EQ (CAR THX) @THAUX)
((CADR THX) (CADDR THX) THY))
α well if the TAG and the KEY are the same length,
α modulo a possible THEV call, then MAPC them thru MATCH2.
((AND (EQ (LENGTH
(COND ((EQ (CAR THX) @THEV)
(SETQ THX (THVAL (CADR THX) THOLIST)))
(THX)))
(LENGTH THY))
(ERRSET (MAPC (FUNCTION THMATCH2) THX THY)))
(AND THML (THPUSH THTREE (LIST @THMUNG THML)))
(RETURN T))
α NO MATCH - Restore the binding STATUS QUO ANTE.
(T (EVLIS THML) (RETURN NIL))
)))
(DE EVLIS (X) (MAPC (FUNCTION EVAL) X))
THX - pattern key item
THY - pattern tag item
(DE THMATCH2 (THX THY)
(PROG NIL
α do some THEV'ing when necessary.
(AND (EQ (CAR THX) @THEV)
(SETQ THX (THVAL (CADR THX) THOLIST)))
(AND (EQ (CAR THY) @THEV)
(SETQ THY (THVAL (CADR THY) THALIST)))
α perform the actual match for equals.
(RETURN
(COND
((EQ THX @?))
((EQ THY @?))
((OR (MEMQ (CAR THX) (QUOTE (THV THNV THRESTRICT)))
(MEMQ (CAR THY) (QUOTE (THV THNV THRESTRICT))))
(THMATCH3 (THMATCH4 THX THOLIST) (THMATCH4 THY THALIST)))
((EQUAL THX THY))
(T (ERR NIL)) α NO MATCH - returns to thMATCH1's errset.
)) ))
α bind THV, THNV, THRESTRICT variables and demand match.
(DE THMATCH3 (XPAIR YPAIR)
(COND
A. ((AND XPAIR
(OR (EQ (CAR THX) @THNV)
(AND (EQ (CAR THX) @THV)
(EQ (CADR XPAIR) @THUNASSIGNED)))
(THCHECK (CDDR XPAIR)
(COND (YPAIR (CADR YPAIR)) (T THY))))
(COND (YPAIR (THRPLACAS (CDR XPAIR) (CADR YPAIR))
(AND (CDDR YPAIR)
(THRPLACDS (CDR XPAIR)
(THUNION (CDDR XPAIR) (CDDR YPAIR))))
(THRPLACDS YPAIR (CDR XPAIR)))
(T (THRPLACAS (CDR XPAIR) THY))))
B. ((AND YPAIR
(OR (EQ (CAR THY) @THNV)
(AND (EQ (CAR THY) @THV)
(EQ (CADR YPAIR) @THUNASSIGNED)))
(THCHECK (CDDR YPAIR)
(COND (XPAIR (CADR XPAIR)) (T THX))))
(COND (XPAIR (THRPLACAS (CDR YPAIR) (CADR XPAIR)))
(T (THRPLACAS (CDR YPAIR) THX))))
α must now match.
C. ((AND XPAIR (EQUAL (CADR XPAIR)
(COND (YPAIR (CADR YPAIR)) (T THY)))))
D. ((AND YPAIR (EQUAL (CADR YPAIR) THX)))
α no match - return to thMATCH1's errset.
E. (T (ERR NIL))
))
(DF THRESTRICT (L)
(NCONC (THGAL (CAR L) THALIST) (APPEND (CDR L) NIL)))
)
(DE THCHECK (THPRD THX)
(OR (NULL THPRD)
(EQ THX @THUNASSIGNED)
(ERRSET (MAPC (FUNCTION (LAMBDA (THY)
(OR (THY THX) (ERR NIL)))) THPRD))
))
(DE THUNION (L1 L2)
(PROG NIL
(MAPC (FUNCTION (LAMBDA (THX)
(COND ((MEMBER THX L2))
(T (SETQ L2 (CONS THX L2))) ))) L1)
(RETURN L2)
))
α thMATCH4 is the THV, THNV and THRESTRICT EVALuator,
α under and alist.
(DE THMATCH4 (THXY THOALIST)
(COND
((THVAR THXY) (THGAL THXY THOLIST))
((EQ (CAR THXY) @THRESTRICT)
(COND
((EQ (CADR THXY) @?)
(PROG2 0
(CONS @? (CONS @THUNASSIGNED (APPEND (CDDR THXY) NIL)))
(SETQ THXY @(THNV ?)) ))
(T(MATCH5
(THGAL (CADR THXY) THOALIST)) ))
)
(T NIL) α well thXY wasn't a thV, thNV or thRESTRICT.
))
(DE MATCH5 (U)
(PROG NIL
(THRPLACDS (CDR U)(THUNION(CDDR U)(CDDR THXY)))
(SETQ THXY (CADR THXY))
(RETURN U)
))
(DE THVAR (X) (MEMQ (CAR X) @(THV THNV)) )
(DE THGAL (X Y)
(PROG NIL
(SETQ THXX X)
(RETURN
(SASSQ (CADR X) Y
α WHEN X NOT ON Y-LIST, give an error message.
(FUNCTION (LAMBDA NIL
(PROG NIL
(PRINT THXX)
(RETURN (THERT THUNBOUND THGAL))
))) ))) )
DO & BIND PLANNER FUNCTIONS.
thAPPLY(L);
thAPPLY1(theorem,body,pattern-key);
thDO(exprs);
thDO1;
thDOB;
thUNDOF;
thUNDOT;
thBIND (varlist); varlist of varnames or (varname expr)
thBI1(x);
thREMBINDF;
thREMBINDT;
(DF THAPPLY (L)
(THAPPLY1 (CAR L) (GET (CAR L) @THEOREM) (CADR L))
)
THM - theorem name
THB - theorem body
DAT - pattern key
(CADR THB) - theorem varlist
(CADDR THB) - pattern tag
(CDDR THB) - theorem steps
(DE THAPPLY1 (THM THB DAT)
(COND
α Bind the theorem's varlist.
((AND (THBIND (CADR THB))
(THMATCH1 DAT (CADDR THB)))
(AND THT (THPUSH THTREE
α push [THPROG steps NIL steps] on the tree.
(LIST @THPROG (CDDR THB) NIL (CDDR THB)))
(THPROGA) T)
α on match failure, restore binding status quo ante;
(T (SETQ THALIST THOLIST) (THPOPT) NIL)
))
(DF THDO (A)
(OR (NOT A)
(PROG2
(THPUSH THTREE (LIST @THDO A NIL NIL))
(SETQ THEXP (CAR A))
)))
(DE THDO1 NIL
(PROG NIL
(RPLACA (CDAR THTREE) (CDADAR THTREE)) α LOP STEPS;
(SETQ THEXP (CAADAR THTREE)) α GET NEXT STEP;
α Accumulate branchs into this DO's tree node;
(RETURN(COND(THBRANCH
(RPLACA (CDDAR THTREE)
(CONS THBRANCH (CADDAR THTREE)))
(SETQ THBRANCH NIL)
(RPLACA (CDDDAR THTREE)
(CONS THABRANCH (CAR (CDDDAR THTREE))) ))))
))
α thDOB is Both thDOT and thDOF;
(DE THDOB NIL
(COND
((NULL (CDADAR THTREE))
(RPLACA (CAR THTREE) @THUNDO) T) α modify node name.
((THDO1))
))
(DE THUNDOT NIL (PROG NIL (THPOPT) (RETURN T) ))
α thundo node ≡ [THUNDO stepN branchs alists];
α THXX ≡ (branchs alists);
(DE THUNDOF NIL
(PROG NIL
(COND ((NULL (CADDAR THTREE)) (THPOPT))
(T
(SETQ THXX (CDDAR THTREE))
(SETQ THALIST (CAADR THXX)) α lop off an alist;
(RPLACA (CDR THXX) (CDADR THXX))
(SETQ THTREE (CAAR THXX)) α lop off a branch;
(RPLACA THXX (CDAR THXX))
))
(RETURN NIL)
))
α thBIND an varlist A
consisting of varnam, (varnam expr), (thRESTRICT varnam filters),
or (thRESTRICT (varname expr) filters);
(DE THBIND (A)
(PROG NIL
(SETQ THOLIST THALIST) α save the old varlist.
(RETURN (OR (NULL A)
(PROG NIL
GO (COND ((NULL A)
(THPUSH THTREE (LIST @THREMBIND THOLIST))
(RETURN T)))
(THPUSH THALIST
(COND ((ATOM (CAR A))
(LIST (CAR A) @THUNASSIGNED))
((EQ (CAAR A) @THRESTRICT)
(NCONC (THBI1 (CADAR A)) (CDDAR A)))
(T (LIST (CAAR A) (EVAL (CADAR A)) )) ))
(SETQ A (CDR A))
(GO GO)
))) ))
(DE THBI1 (X)
(COND
((ATOM X) (LIST X @THUNASSIGNED))
(T (LIST (CAR X) (EVAL (CADR X))))
))
(DE THREMBINDF NIL
(PROG NIL
(SETQ THALIST (CADAR THTREE))
(THPOPT)
(RETURN NIL)
))
(DE THREMBINDT NIL
(PROG NIL
(SETQ THALIST (CADAR THTREE))
(THPOPT)
(RETURN THVALUE)
))
PROG-GROUP PLANNER FUNCTIONS.
thPUSH(thtree,node);
thPOPT;
thBRANCH;
thBRANCHUN;
thPROG(varlist,steps);
thPROGA;
thPROGF;
thPROGT;
thSUCCEED(node);
thFAIL(node);
thFAIL?(predicate,action);
thFAIL?F;
thFAIL?T;
thGO(tag);
thTAG(tag);
thTAGF;
thTAGT;
thRETURN(expr);
thFINALIZE(node);
thMESSAGE(varlist,pattern,steps);
thMESSAGEF;
thMESSAGET;
thUNIQUE(varname);
α Macro for pushing nodes onto list;
(DEFPROP THPUSH
(LAMBDA (A) (LIST @SETQ (CADR A) (LIST @CONS (CADDR A) (CADR A))))
MACRO)
(DE THPOPT NIL (SETQ THTREE (CDR THTREE)) )
(DE THBRANCH NIL
(COND
((NOT (CDADAR THTREE))) α future steps list empty.
((EQ THBRANCH THTREE) α nothun' really happened just now.
(SETQ THBRANCH NIL))
((RPLACA (CDDAR THTREE) α push a step into the past.
(CONS (LIST THBRANCH THABRANCH (CADAR THTREE))
(CADDAR THTREE)) )
(SETQ THBRANCH NIL)
))
α thprog-node ≡ [THPROG pc psl sa];
α thand-node ≡ [THAND pc psl];
(DE THBRANCHUN NIL
(PROG (X)
(RETURN
(COND
((SETQ X (CADDAR THTREE)) α get psl - past steps list;
(RPLACA (CDAR THTREE) (CADDAR X)) α restore old pc;
(RPLACA (CDDAR THTREE) (CDR X)) α lop past steps list;
(SETQ THALIST (CADAR X)) α restore old bindings;
(SETQ THTREE (CAAR X)) α restore old tree;
T)
(T (THPOPT) NIL))
)))
(DF THPROG (THA)
(PROG NIL
(THBIND (CAR THA))
(THPUSH THTREE (LIST @THPROG THA NIL THA))
(RETURN (THPROGA))
))
(DE THPROGA NIL
α this is a function applied to the CDR of a PROG tree node;
((LAMBDA(X)
(COND
α no more steps, fall off end of program;
((NULL (CDAR X)) (THPOPT) @THNOVAL)
α atomic steps are tags;
((ATOM (CADAR X))
(SETQ THEXP (LIST @THTAG (CADAR X)))
(RPLACA X (CDAR X))
THVALUE)
α lop off next step;
(T
(SETQ THEXP (CADAR X))
(RPLACA X (CDAR X))
THVALUE)))
(CDAR THTREE))
))
(DE THPROGF NIL
(PROG NIL (THBRANCHUN) (RETURN NIL) ))
(DE THPROGT NIL
(PROG NIL (THBRANCH) (RETURN (THPROGA)) ))
(DF THSUCCEED (THA)
(OR (NOT THA) α simple success on empty;
(PROG (THX)
α well THEOREM's are actually thPROGs;
(AND (EQ (CAR THA) @THEOREM)
(SETQ THA (CONS @THPROG (CDR THA))))
α Save the current tree and alist;
(SETQ THBRANCH THTREE)
(SETQ THABRANCH THALIST)
LOOP (COND
α test for tree pdl under flow;
((NULL THTREE)
(PRINT THA)
(THERT OVERPOP /- THSUCCEED))
α restore earlier bindings;
((EQ (CAAR THTREE) @THREMBIND)
(SETQ THALIST (CADAR THTREE))
(THPOPT)
(GO LOOP))
α success to this kind of tree node;
((EQ (CAAR THTREE) (CAR THA))
(THPOPT)
(RETURN
(COND ((CDR THA) (EVAL (CADR THA))) (@THNOVAL))))
α look for a tag in this tree node;
((AND (EQ (CAR THA) @THTAG)
(EQ (CAAR THTREE) @THPROG)
(SETQ THX (MEMQ (CADR THA) (CADDDAR THTREE)) ))
(RPLACA (CDAR THTREE) (CONS NIL THX))
(RETURN (THPROGT)))
α Lop off this node and continue;
(T (THPOPT) (GO LOOP)))))
))
(DF THFAIL (THA)
(AND THA
(PROG (THTREE1 THA1 THX)
(SETQ THTREE1 THTREE)
α failure to a THA1 kind of tree node;
(SETQ THA1
(COND ((EQ (CAR THA) @THEOREM) @THPROG)
((EQ (CAR THA) @THTAG) @THPROG)
((EQ (CAR THA) @THINF) (SETQ THINF T) (RETURN NIL))
((EQ (CAR THA) @THMESSAGE)
(SETQ THMESSAGE (CADR THA))
(RETURN NIL))
(T (CAR THA))))
α lop the tree until that kind of node is found;
LP1 (COND ((NULL THTREE1) α pdl underflow.
(PRINT THA)
(RETURN (THERT NOT FOUND /- THFAIL)))
((EQ (CAAR THTREE1) THA1) (GO ELP1)))
ALP1 (SETQ THTREE1 (CDR THTREE1))
(GO LP1)
α when thfailing to tag, see if the tag is in this thprog.
ELP1 (COND ((EQ (CAR THA) @THTAG)
(COND ((MEMQ (CADR THA)(CADDDAR THTREE1))(GO TAGS))
(T (GO ALP1)) )) )
α on other thfailures, splice a thfail? node into the tree.
(RPLACD THTREE1 (CONS
(LIST @THFAIL? T (AND(CDR THA)(CADR THA)) ) (CDR THTREE1)))
(SETQ THMESSAGE @THFAIL)
(RETURN NIL)
α on tag thfailures, lop the thprogs past until we reach our tag.
TAGS (SETQ THX (CADDAR THTREE1)) α get the psl of this thprog.
LP2 (COND
((NULL (CAR THX)) (GO ALP1)) α this thprog has no past.
((EQ (CAADDAR THX) (CADR THA)) α pc of this thprog at the tag.
(RPLACA (CAR THX) (CONS
(LIST @THFAIL? T (AND (CDDR THA) (CADDR THA))) (CAAR THX)))
(SETQ THMESSAGE @THFAIL)
(RETURN NIL)))
(SETQ THX (CDR THX))
(GO LP2))
))
(DE THFAIL? (PRD ACT)
(PROG NIL
(THPUSH THTREE (LIST (QUOTE THFAIL?) PRD ACT))
(RETURN THVALUE)
))
(DE THFAIL?F NIL
(COND ((EVAL (CADAR THTREE)) α test the predicate.
(PROG2 (SETQ THMESSAGE NIL)
(EVAL (CADDAR THTREE)) α do the action.
(THPOPT)))
(T (THPOPT) NIL)
))
(DE THFAIL?T NIL (PROG NIL (THPOPT) (RETURN THVALUE) ))
(DF THTAG (L)
(AND (CAR L)
(THPUSH THTREE (LIST @THTAG (CAR L)))
))
(DE THTAGF NIL (PROG NIL (THPOPT) (RETURN NIL)) )
(DE THTAGT NIL (PROG NIL (THPOPT) (RETURN THVALUE)) )
(DF THGO (X) (APPLY @THSUCCEED (CONS @THTAG X)) )
(DF THRETURN (X) (APPLY @THSUCCEED (CONS @THPROG X)) )
THX ≡ tree node.
THT ≡ argument tag.
THA ≡ (node)
(DF THFINALIZE (THA)
(PROG (THTREE1 THT THX)
(COND ((NULL THA)
(THERT BAD CALL /- THFINALIZE))
((EQ (CAR THA) @THTAG)
(SETQ THT (CADR THA)))
((EQ (CAR THA) @THEOREM)
(SETQ THA (LIST @THPROG)) ))
(SETQ THTREE (SETQ THTREE1 (CONS NIL THTREE)))
PLUP (SETQ THX (CADR THTREE1))
(COND
α test for tree underflow.
1. ((NULL (CDR THTREE1))
(PRINT THA)
(THERT OVERPOP /- THFINALIZE))
α test for tag case.
2. ((AND THT (EQ (CAR THX) @THPROG)
(MEMQ THT (CADDDR THX)))
(GO RTLEV))
α forget the past of thprogs and thands.
3. ((OR (EQ (CAR THX) @THPROG)
(EQ (CAR THX) @THAND))
(RPLACA (CDDR THX) NIL)
(SETQ THTREE1 (CDR THTREE1)))
α pass over a tree node.
4. ((EQ (CAR THX) @THREMBIND)
(SETQ THTREE1 (CDR THTREE1)))
α splice out a tree node.
5. ((RPLACD THTREE1 (CDDR THTREE1))))
α test for final node.
(COND ((EQ (CAR THX) (CAR THA))
(GO DONE)))
(GO PLUP)
α on tag thfinalize, lop the thprog's past until we reach our tag.
RTLEV (SETQ THX (CDDR THX))
LEVLP (COND ((NULL (CAR THX))
(SETQ THTREE1 (CDR THTREE1)) (GO PLUP))
((EQ (CAADDR (CAAR THX)) THT) (GO DONE)))
(RPLACA THX (CDAR THX))
(GO LEVLP)
α end of tree pruning.
DONE (SETQ THTREE (CDR THTREE))
(RETURN T)
))
(DF THMESSAGE (THA)
(PROG NIL
(THPUSH THTREE (CONS @THMESSAGE THA))
(RETURN THVALUE)
))
(DE THMESSAGET NIL (PROG NIL (THPOPT) (RETURN THVALUE) ))
α well only failures can send messages into the past.
(DE THMESSAGEF NIL
(PROG (BOD)
(SETQ BOD (CAR THTREE)) α get prog body of thmessage.
(THPOPT) α flush thmessage node.
α first bind the varlist then call for a pattern match.
(COND ((AND (THBIND (CADR BOD)) α bind varlist.
(THMATCH1 (CADDR BOD) THMESSAGE))
α on pattern match win, make noises like a thprog.
(THPUSH THTREE
(LIST @THPROG(CDDR BOD)NIL(CDDR BOD)))
(SETQ THMESSAGE NIL)
(RETURN (THPROGA)))
α on pattern match lose, restore status quo ante and fail.
(T (SETQ THALIST THOLIST) (THPOPT)))
(RETURN NIL)
))
(DF THUNIQUE (THA)
(PROG (X)
(SETQ X THALIST) α pointer to alist.
LOOP (COND ((NULL X)
(PRINT THA)
(THERT NOT FOUND /- THUNIQUE))
BEGIN BIG FUCKING COND-PAIR
| ((EQ (CAAR X) (CAR THA)) α argument varname.
| (COND ((EQ (CADAR X) @THUNIQUE)) α argument value. ←
| ((RPLACD (CAR X) (CONS @THUNIQUE |
| |
| (MAPCAR (FUNCTION (LAMBDA(Y) |
| → (COND ((ATOM Y) α fetch it or blow. |
| | (SETQ THXX Y) |
| | (CADR(SASSQ Y THALIST |
| | (FUNCTION (LAMBDA NIL (PROG NIL |
| | (PRINT THXX) |
| | (RETURN(THERT THUNBOUND /- THUNIQUE)) ))) |
| | ))) |
| | (T (THVAL Y THALIST)) |
| → ))) |
| α well er ah... mapcar cons rplacd pair cond|
| α arg var list ↓ ↓ ↓ ↓ ↓ |
| (CADAR X) ) ) ) ) ) ←
| α test for unique failure.
| (RETURN (NOT (MEMBER (CAR X) (CDR X) )) ) )
END BIG FUCKING COND-PAIR.
α lop the alist pointer until the argument varname is found.
(T (SETQ X (CDR X)) (GO LOOP) ))
))
BOOL-GROUP PLANNER FUNCTIONS.
thAMONG(varname,exprs);
thAMONGF;
thAND(exprs);
thANDF;
thANDT;
thNOT(expr);
thOR(exprs);
thOR2(flag);
thORF;
thORT;
thCOND(pairs);
thCONDF;
thCONDT;
(DF THAMONG (THA)
(COND
α when its unassigned; push a thamong onto the tree.
((EQ (CADR (SETQ THXX
(THGAL (COND ((EQ (CAAR THA) @THEV)
(THVAL (CADAR THA) THALIST))
(T (CAR THA))) THALIST)))
@THUNASSIGNED)
(THPUSH THTREE (LIST @THAMONG THXX (THVAL (CADR THA) THALIST)))
NIL)
(T
(MEMBER (CADR THXX) (THVAL (CADR THA) THALIST) ))
))
(DE THAMONGF NIL
(COND ((CADDAR THTREE)
(RPLACA (CDADAR THTREE) (CAADDR (CAR THTREE)))
(RPLACA (CDDAR THTREE) (CDADDR (CAR THTREE)))
(SETQ THBRANCH THTREE)
(SETQ THABRANCH THALIST)
(THPOPT)
T)
(T
(RPLACA (CDADAR THTREE) @THUNASSIGNED)
(THPOPT)
NIL)
))
(DF THAND (A)
(OR (NOT A)
(PROG2
(THPUSH THTREE (LIST @THAND A NIL))
(SETQ THEXP (CAR A)))
))
(DE THANDF NIL
(PROG NIL (THBRANCHUN) (RETURN NIL)) )
(DE THANDT NIL
(PROG NIL
(COND ((CDADAR THTREE)
(THBRANCH)
(SETQ THEXP (CADR (CADAR THTREE)))
(RPLACA (CDAR THTREE) (CDADAR THTREE)))
((THPOPT)))
(RETURN THVALUE)
))
(DF THNOT (THA)
(SETQ THEXP (LIST @THCOND
(LIST (CAR THA)
(QUOTE (THFAIL THAND)) )
(QUOTE ((THSUCCEED))))))
FEXPR)
(DF THOR (THA)
(AND THA
(THPUSH THTREE (LIST @THOR THA))
(SETQ THEXP (CAR THA))
))
(DF THCOND (THA)
(PROG NIL
(THPUSH THTREE (LIST @THCOND THA NIL))
(RETURN (SETQ THEXP (CAAR THA)))
))
(DE THCONDF NIL (THOR2 NIL))
(DE THCONDT NIL
(PROG NIL
(RPLACA (CAR THTREE) @THAND)
(RPLACA (CDAR THTREE) (CAADAR THTREE))
(RETURN THVALUE)
))
(DE THOR2 (P)
(COND
((AND (CADAR THTREE) (CDADAR THTREE))
(RPLACA (CDAR THTREE) (CDADAR THTREE))
(SETQ THEXP (COND
α On thOR call;
(P(PROG2 0 (CAADAR THTREE) (OR (CADAR THTREE) (THPOPT)) ))
((CAAADAR THTREE)) ))) α predicate of a pair of a thcond node;
((THPOPT) NIL)
))
(DE THORF NIL (THOR2 T))
(DE THORT NIL (PROG NIL (THPOPT) (RETURN THVALUE) ))
IO-GROUP PLANNER FUNCTIONS.
thSEMI;
thREAD;
thDATA;
thDUMP;
(DE THSEMI NIL
(PROG NIL
LP (COND ((EQ (READCH) @/;)
(RETURN NIL)))
(GO LP)
))
(DE THREAD NIL
(PROG (CHAR)
(RETURN
(COND ((EQ (SETQ CHAR (READCH)) @?) (LIST @THV (READ)))
((EQ CHAR @E) (LIST @THEV (READ)))
((EQ CHAR (QUOTE ←)) (LIST @THNV (READ)))
((EQ CHAR (QUOTE &))
(PROG NIL
CHLP
(COND ((EQ @& (READCH))
(RETURN @(COMMENT))) )
(GO CHLP)))
((EQ CHAR @T) (QUOTE (THTBF THTRUE)))
((EQ CHAR @R) @THRESTRICT)
((EQ CHAR @G) @THGOAL)
((EQ CHAR @A) @THASSERT)
((PRINT @ILLEGAL-PREFIX)
(PRINC @$)
(PRINC CHAR)
(PRINC (READ))
(ERR NIL))))
))
(DE THDATA NIL
(PROG (X)
GO (TERPRI)
(COND ((NULL (SETQ X (READ NIL)))
(RETURN T))
((PRINT (THADD (CAR X) (CDR X)))))
(GO GO)
))
(DE THDUMP NIL
(PROG (P)
α dump the theorem bodies.
(MAPC (FUNCTION (LAMBDA (BUCKET)
(MAPC (FUNCTION (LAMBDA (ATOM)
(MAPC (FUNCTION (LAMBDA (IND)
(AND (SETQ P (GET ATOM IND))
(PRINT (LIST @DEFPROP ATOM P IND)))))
(QUOTE (THCONSE THERASING THANTE)))))
BUCKET)))
OBLIST)
(PRINT (QUOTE (THDATA)))
α dump the assertions.
(MAPC (FUNCTION (LAMBDA (BUCKET)
(MAPC (FUNCTION (LAMBDA (ATOM)
(AND (SETQ ATOM (GET ATOM @THASSERTION))
(SETQ ATOM (ASSOC 1 (CDR ATOM)))
(MAPC (FUNCTION (LAMBDA(LENGTH-BUCKET)
(MAPC (FUNCTION (LAMBDA (ASRT) (PRINT ASRT)))
(CDDR LENGTH-BUCKET))))
(CDR ATOM)))))
BUCKET)))
OBLIST)
(PRINT NIL)
))