=========================================================== REDUCERON MEMO 36 Case of known construction -- at compile-time and run-time Colin Runciman, 7 October 2009 =========================================================== Let's go straight into a fairly meaty example. The Mate chess end-game program includes the following function to test whether player c's king on board bd is in check from an opposing force f on square (x,y). kingInCheckFrom c bd (Pair f (Pair x y)) = case kingSquare c bd of { Pair xk yk -> case f of { King -> con ((<=) (abs ((-) x xk)) 1) ((<=) (abs ((-) y yk)) 1) ; Queen -> dis (kingInCheckFrom c bd (Pair Rook (Pair x y))) (kingInCheckFrom c bd (Pair Bishop (Pair x y))) ; Rook -> dis (con ((==) x xk) (emptyAtAll bd (filePath xk y yk))) (con ((==) y yk) (emptyAtAll bd (rankPath yk x xk))) ; Bishop -> dis (con ((==) ((-) x y) ((-) xk yk)) (emptyAtAll bd (diagPath (-) ((-) xk yk) x xk))) (con ((==) ((+) x y) ((+) xk yk)) (emptyAtAll bd (diagPath (+) ((+) xk yk) x xk))) ; Knight -> dis (con ((==) (abs ((-) x xk)) 2) ((==) (abs ((-) y yk)) 1)) (con ((==) (abs ((-) x xk)) 1) ((==) (abs ((-) y yk)) 2)) ; Pawn -> con ((==) (abs ((-) x xk)) 1) ((==) yk (onFor c y )) ; After compilation, with -i1 as usual, here is how this function is currently encoded at the reduceron combinator level (with kingInChekFrom abbreviated to kICF and arguments elided on left-hand sides): kICF v0 ... v2 = v2 [kICF#9] v0 v1; kICF#1 v0 ... v6 = (==) ((-) v1 v2) ((-) v3 v4) [con#1,con#2] (v5 [emptyAtAll#1] (diagPath (-) ((-) v3 v4) v1 v3)) [dis#1,dis#2] ((==) ((+) v1 v2) ((+) v3 v4) [con#1,con#2] (v5 [emptyAtAll#1] (diagPath (+) ((+) v3 v4) v1 v3))); kICF#2 v0 ... v6 = let { v7 = (-) v1 v3; v8 = (-) v2 v4 } in (<=) ((<=) 0 v7 [abs#1,abs#2] v7) 1 [con#1,con#2] ((<=) ((<=) 0 v8 [abs#1,abs#2] v8) 1); kICF#3 v0 ... v6 = let { v7 = (-) v1 v3; v8 = (-) v2 v4; v9 = (-) v1 v3; v10 = (-) v2 v4 } in (==) ((<=) 0 v7 [abs#1,abs#2] v7) 2 [con#1,con#2] ((==) ((<=) 0 v8 [abs#1,abs#2] v8) 1) [dis#1,dis#2] ((==) ((<=) 0 v9 [abs#1,abs#2] v9) 1 [con#1,con#2] ((==) ((<=) 0 v10 [abs#1,abs#2] v10) 2)); kICF#4 v0 ... v6 = let { v7 = (-) v1 v3 } in (==) ((<=) 0 v7 [abs#1,abs#2] v7) 1 [con#1,con#2] ((==) v4 (v6 [onFor#1,onFor#2] v2)); kICF#5 v0 ... v6 = Pair Rook (Pair v1 v2) [kICF#9] v6 v5 [dis#1,dis#2] (Pair Bishop (Pair v1 v2) [kICF#9] v6 v5); kICF#6 v0 ... v6 = (==) v1 v3 [con#1,con#2] (v5 [emptyAtAll#1] (filePath v3 v2 v4)) [dis#1,dis#2] ((==) v2 v4 [con#1,con#2] (v5 [emptyAtAll#1] (rankPath v4 v1 v3))); kICF#7 v0 ... v7 = v3 [kICF#1,kICF#2,kICF#3, kICF#4,kICF#5,kICF#6] v4 v5 v0 v1 v6 v7; kICF#8 v0 ... v5 = kingSquare v3 v4 [kICF#7] v5 v0 v1 v4 v3; kICF#9 v0 ... v4 = v1 [kICF#8] v3 v4 v0; I shall use references of the form #n to refer to the auxiliary combinators. At Compile-time --------------- In #5 we have, in the now-church-encoded Pair applications, two instances of a case with a known construction as subject: kICF#5 v0 ... v6 = Pair Rook (Pair v1 v2) [kICF#9] v6 v5 [dis#1,dis#2] (Pair Bishop (Pair v1 v2) [kICF#9] v6 v5); Considering first the Pair Rook application, we can apply the sole alternative kICF#5 v0 ... v6 = kICF#9 Rook (Pair v1 v2) [*] v6 v5 [dis#1,dis#2] (Pair Bishop (Pair v1 v2) [kICF#9] v6 v5); where [*] represents an unused look-up table argument. Now in-lining #9: kICF#5 v0 ... v6 = (Pair v1 v2) [kICF#8] v6 v5 Rook [dis#1,dis#2] (Pair Bishop (Pair v1 v2) [kICF#9] v6 v5); The same situation again! We apply the sole alternative kICF#5 v0 ... v6 = kICF#8 v1 v2 [*] v6 v5 Rook [dis#1,dis#2] (Pair Bishop (Pair v1 v2) [kICF#9] v6 v5); and then in-line it: kICF#5 v0 ... v6 = kingSquare v6 v5 [kICF#7] Rook v1 v2 v5 v6 [dis#1,dis#2] (Pair Bishop (Pair v1 v2) [kICF#9] v6 v5); The kingSquare function is recursive, so it is not helpful to in-line its application. But the Pair Bishop application can be handled in the same way as Pair Rook. We end up with: kICF#5 v0 ... v6 = kingSquare v6 v5 [kICF#7] Rook v1 v2 v5 v6 [dis#1,dis#2] (kingSquare v6 v5 [kICF#7] Bishop v1 v2 v5 v6) ; We cannot apply the sole-alternative principle any further, because we don't yet see the Pair in either case, and kingSquare might have an undefined result. But we have saved 5-10 clock cycles for each application of #5. These sorts of applications with paired arguments explicit at compile-time may not be that frequent, but they do occur -- eg. the KnuthBendix program has several. And they might occur more with more aggressive in-lining or other transformations. At Run-time ----------- At run-time we can hope for big improvements from PRS for the kingInCheck function, particularly if functions such as 'abs' become primitives too. Look at combinator #3 for example: kICF#3 v0 ... v6 = let { v7 = (-) v1 v3; v8 = (-) v2 v4; v9 = (-) v1 v3; v10 = (-) v2 v4 } in (==) ((<=) 0 v7 [abs#1,abs#2] v7) 2 [con#1,con#2] ((==) ((<=) 0 v8 [abs#1,abs#2] v8) 1) [dis#1,dis#2] ((==) ((<=) 0 v9 [abs#1,abs#2] v9) 1 [con#1,con#2] ((==) ((<=) 0 v10 [abs#1,abs#2] v10) 2)); Assuming that * v1 .. v4 are already evaluated (as they almost always will be under PRS) * 'abs' is included among primitives eligible for PRS * PRS cascades, with 4 (-) applications in a first wave, 4 'abs' applications in a second and 4 (==) comparisons in a third (optimistic?) here's a typical run-time instantiation of a #3 application. True [con#1,con#2] False [dis#1,dis#2] (False [con#1,con#2] True) Once again, we have two instances of cases with known constructors in encoded form, but now at run-time. Is there some way to detect them on-the-fly during instantiation? If so, then the instantiated body becomes still smaller and computationally cheaper: con#2 [*] False [dis#1,dis#2] con#1 [*] True The combinators for the (&&) and (||) alternatives used here are as follows. con#1 v0 v1 = False; con#2 v0 v1 = v1; dis#1 v0 v1 = v1; dis#2 v0 v1 = True; Is there any way that these could themselves be recognised as primitive, and their applications reduced at little cost, by analogy with the PRS scheme? If so, and all three ingredients can be combined -- (1) PRS, (2) application of known-case alternatives, and (3) primitive logical alternatives -- the gains for this example would be immense!