[<<][staapl][>>][..]
Wed May 6 11:05:43 CEST 2009

verifying a transformation rule given concrete machine semantics

Maybe it's best to find a way to verify rules first.  Or better
individual clauses.

([addlw a] [qw b] +) -> ([addlw (a b +)])

This particular one is simpler when we're able to unpack addlw:

([qw a] [cw +] [qw b] [cw +]) -> ([qw (a b +)] [cw +])

or in concatenative code compiled to the generic vm with partial eval
removed:

( a + b + ) -> ( a b + + )



[Reply][About]
[<<][staapl][>>][..]