There was a post about Automated Reasoning in F#, Scala, Haskell, C++, and Julia that uses a simple algorithm from John Harrison's book Handbook of Practical Logic and Automated Reasoning to simplify this equation:

e = (1 + (0 * x)) * 3) + 12

Factor has support for ML-style pattern matching and I thought it would be fun to contribute a simple solution using the match vocabulary.

We want to define a few types of expressions:

TUPLE: Var s ; TUPLE: Const n ; TUPLE: Add x y ; TUPLE: Mul x y ;

Note: we could have made this simpler by assuming integers are constants and strings are variables rather than define the`Const`

and`Var`

tuples, but I wanted to keep this close to the code in the original blog post.

To be able to pattern match, we need to define some match variables:

```
MATCH-VARS: ?x ?y ;
```

We want a way to do a single simplification of an expression:

: simplify1 ( expr -- expr' ) { { T{ Add f T{ Const f 0 } ?x } [ ?x ] } { T{ Add f ?x T{ Const f 0 } } [ ?x ] } { T{ Mul f ?x T{ Const f 1 } } [ ?x ] } { T{ Mul f T{ Const f 1 } ?x } [ ?x ] } { T{ Mul f ?x T{ Const f 0 } } [ T{ Const f 0 } ] } { T{ Mul f T{ Const f 0 } ?x } [ T{ Const f 0 } ] } { T{ Add f T{ Const f ?x } T{ Const f ?y } } [ ?x ?y + Const boa ] } { T{ Mul f T{ Const f ?x } T{ Const f ?y } } [ ?x ?y * Const boa ] } [ ] } match-cond ;

We have a way to recursively simplify some expressions:

: simplify ( expr -- expr' ) { { T{ Add f ?x ?y } [ ?x ?y [ simplify ] bi@ Add boa ] } { T{ Mul f ?x ?y } [ ?x ?y [ simplify ] bi@ Mul boa ] } [ ] } match-cond simplify1 ;

Finally, we have a word that tries to simplify a value to a constant:

: simplify-value ( expr -- str ) simplify { { T{ Const f ?x } [ ?x ] } [ drop "Could not be simplified to a Constant." ] } match-cond ;

To check that it works, we can write a unit test that simplifies the original expression above:

{ 15 } [ T{ Add f T{ Mul f T{ Add f T{ Const f 1 } T{ Mul f T{ Const f 0 } T{ Var f "x" } } } T{ Const f 3 } } T{ Const f 12 } } simplify-value ] unit-test

That's cool, but wouldn't it be better if we could work on quotations directly? Let's make a word that converts a quotation to an expression:

: >expr ( quot -- expr ) [ { { [ dup string? ] [ '[ _ Var boa ] ] } { [ dup integer? ] [ '[ _ Const boa ] ] } { [ dup \ + = ] [ drop [ Add boa ] ] } { [ dup \ * = ] [ drop [ Mul boa ] ] } } cond ] map concat call( -- expr ) ;

Now that we have that, our test case is a lot simpler:

{ 15 } [ [ "x" 0 * 1 + 3 * 12 + ] >expr simplify-value ] unit-test

The code for this is on my GitHub.

Note: this takes advantage of a small feature that I added to the match-cond word to provide a way to easily handle a fall-through pattern like the cond word.

## No comments:

Post a Comment