Create a gist now

Instantly share code, notes, and snippets.

@mavnn /Tests.fs
Last active Aug 29, 2015

Embed
Boolean Algebra
module Algebra.Boolean.Tests
open Microsoft.FSharp.Quotations
open Algebra.Boolean
open Xunit
[<Fact>]
let ``not pattern`` () =
Assert.Equal (<@@ true @@>, match <@@ not true @@> with Not' e -> e)
[<Fact>]
let ``Commute ||`` () =
Assert.Equal (<@@ false || true @@>, commute <@@ true || false @@>)
[<Fact>]
let ``Commute &&`` () =
Assert.Equal (<@@ false && true @@>, commute <@@ true && false @@>)
[<Fact>]
let ``Commute is top level only`` () =
Assert.Equal (<@@ false && (false || true) @@>, commute <@@ (false || true) && false @@>)
[<Fact>]
let ``Identity reduction &&`` () =
Assert.Equal (<@@ false @@>, identity <@@ true && false @@>)
[<Fact>]
let ``Identity reduction ||`` () =
Assert.Equal (<@@ true @@>, identity <@@ true || false @@>)
[<Fact>]
let ``Identity reduction recurses`` () =
Assert.Equal (<@@ true @@>, identity <@@ (true || false) && true @@>)
[<Fact>]
let ``Identity reduction recurses with none boolean`` () =
Assert.Equal (<@@ "bob" = "fred" @@>, identity <@@ ("bob" = "fred" || false) && true @@>)
[<Fact>]
let ``Identity reduction recurses with none boolean 2`` () =
Assert.Equal (<@@ "bob" = "fred" @@>, identity <@@ (false || "bob" = "fred") && true @@>)
[<Fact>]
let ``Idempotence reduction &&`` () =
Assert.Equal (<@@ true @@>, idempotence <@@ true && true @@>)
[<Fact>]
let ``Idempotence reduction ||`` () =
Assert.Equal (<@@ true @@>, idempotence <@@ true || true @@>)
[<Fact>]
let ``Associate a || b || c -> a || (b || c)`` () =
Assert.Equal (<@@ 1 = 1 || (2 = 2 || 3 = 3) @@>, associate <@@ 1 = 1 || 2 = 2 || 3 = 3 @@>)
[<Fact>]
let ``Associate a && b && c -> a && (b && c)`` () =
Assert.Equal (<@@ 1 = 1 && (2 = 2 && 3 = 3) @@>, associate <@@ 1 = 1 && 2 = 2 && 3 = 3 @@>)
[<Fact>]
let ``Associate a || (b || c) -> a || b || c`` () =
Assert.Equal (<@@ 1 = 1 || 2 = 2 || 3 = 3 @@>, associate <@@ 1 = 1 || (2 = 2 || 3 = 3) @@>)
[<Fact>]
let ``Associate a && (b && c) -> a && b && c`` () =
Assert.Equal (<@@ 1 = 1 && 2 = 2 && 3 = 3 @@>, associate <@@ 1 = 1 && (2 = 2 && 3 = 3) @@>)
[<Fact>]
let ``Annihilation reduction ||`` () =
Assert.Equal (<@@ true @@>, annihilate <@@ 1 = 2 || true @@>)
[<Fact>]
let ``Annihilation reduction &&`` () =
Assert.Equal (<@@ false @@>, annihilate <@@ 1 = 1 && false @@>)
[<Fact>]
let ``Absorption reduction 1`` () =
Assert.Equal (<@@ 2 = 1 @@>, absorb <@@ 2 = 1 && (2 = 1 || 3 = 4) @@>)
[<Fact>]
let ``Absorption reduction 2`` () =
Assert.Equal (<@@ 2 = 1 @@>, absorb <@@ 2 = 1 || (3 = 3 && 2 = 1) @@>)
[<Fact>]
let ``Complement ||`` () =
Assert.Equal (<@@ true @@>, complement <@@ true || not true @@>)
[<Fact>]
let ``Complement &&`` () =
Assert.Equal (<@@ false @@>, complement <@@ true && not true @@>)
[<Fact>]
let ``Complement || 2`` () =
Assert.Equal (<@@ true @@>, complement <@@ "fred".StartsWith "bob" || not ("fred".StartsWith "bob") @@>)
[<Fact>]
let ``Double negation`` () =
Assert.Equal (<@@ true @@>, doubleNegation <@@ not (not true) @@>)
[<Fact>]
let ``De Morgan &&`` () =
Assert.Equal (<@@ not ("bob" = "bob" || "fred" = "bob") @@>, deMorgan <@@ not ("bob" = "bob") && not ("fred" = "bob") @@>)
[<Fact>]
let ``De Morgan ||`` () =
Assert.Equal (<@@ not ("bob" = "bob" && "fred" = "bob") @@>, deMorgan <@@ not ("bob" = "bob") || not ("fred" = "bob") @@>)
[<Fact>]
let ``Beta reduction 1`` () =
Assert.Equal (<@@ "bob" @@>, beta <@@ (fun (x : string) -> x) "bob" @@>)
[<Fact>]
let ``Beta reduction 2`` () =
Assert.Equal (<@@ "bob" + "fred" @@>, beta <@@ (fun (x : string) -> x + "fred") "bob" @@>)
[<Fact>]
let ``Beta reduction 3`` () =
Assert.Equal (<@@ "bob" + "fred" @@>, beta <@@ (fun x -> fun y -> x + y) "bob" "fred" @@>)
[<Fact>]
let ``Beta reduction 4`` () =
Assert.Equal (<@@ "bob" + "fred" @@>, beta <@@ (fun x y -> x + y) "bob" "fred" @@>)
module Algebra.Boolean
open Microsoft.FSharp.Quotations
open Microsoft.FSharp.Quotations.ExprShape
open Microsoft.FSharp.Quotations.Patterns
open Microsoft.FSharp.Quotations.DerivedPatterns
let (|True'|_|) expr =
match expr with
| Value (o, t) when t = typeof<bool> && (o :?> bool) = true ->
Some expr
| _ ->
None
let (|False'|_|) expr =
match expr with
| Value (o, t) when t = typeof<bool> && (o :?> bool) = false ->
Some expr
| _ ->
None
let (|Or'|_|) expr =
match expr with
| IfThenElse (left, True' _, right) ->
Some (left, right)
| _ ->
None
let (|And'|_|) expr =
match expr with
| IfThenElse (left, right, False' _) ->
Some (left, right)
| _ ->
None
let (|Not'|_|) expr =
match expr with
| SpecificCall <@@ not @@> (_, _, [e]) ->
Some e
| _ ->
None
let associate quote =
match quote with
| Or' (Or' (l, r), r') ->
<@@ %%l || (%%r || %%r') @@>
| Or' (l, Or' (l', r)) ->
<@@ %%l || %%l' || %%r @@>
| And' (And' (l, r), r') ->
<@@ %%l && (%%r && %%r') @@>
| And' (l, And' (l', r)) ->
<@@ %%l && %%l' && %%r @@>
| _ ->
quote
let commute quote =
match quote with
| Or' (left, right) ->
<@@ %%right || %%left @@>
| And' (left, right) ->
<@@ %%right && %%left @@>
| _ ->
quote
let distribute quote =
match quote with
| And' (p, Or' (p', p'')) ->
<@@ (%%p && %%p') || (%%p && %%p'') @@>
| Or' (p, And' (p', p'')) ->
<@@ (%%p || %%p') && (%%p || %%p'') @@>
| _ ->
quote
let gather quote =
match quote with
| And' (Or'(p, p'), Or'(p'', p''')) when p = p'' ->
<@@ %%p || (%%p' && %%p''') @@>
| Or' (And'(p, p'), And'(p'', p''')) when p = p'' ->
<@@ %%p && (%%p' || %%p''') @@>
| _ ->
quote
let identity quote =
let rec transform q =
match q with
| And' (True' _, p)
| And' (p, True' _)
| Or' (False' _, p)
| Or' (p, False' _)
-> transform p
| ShapeVar v -> Expr.Var v
| ShapeLambda (v, e) -> Expr.Lambda(v, transform e)
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map transform)
transform quote
let annihilate quote =
let rec transform q =
match q with
| And' (False' f, _)
| And' (_, False' f)
-> f
| Or' (True' t, _)
| Or' (_, True' t)
-> t
| ShapeVar v -> Expr.Var v
| ShapeLambda (v, e) -> Expr.Lambda(v, transform e)
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map transform)
transform quote
let absorb quote =
let rec transform q =
match q with
| And' (p, Or' (p', _))
| And' (p, Or' (_, p'))
| And' (Or' (p', _), p)
| And' (Or' (_, p'), p)
| Or' (p, And' (p', _))
| Or' (p, And' (_, p'))
| Or' (And' (p', _), p)
| Or' (And' (_, p'), p) when p = p' ->
p
| ShapeVar v -> Expr.Var v
| ShapeLambda (v, e) -> Expr.Lambda(v, transform e)
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map transform)
transform quote
let idempotence quote =
let rec transform q =
match q with
| And' (p, p') when p = p' ->
transform p
| Or' (p, p') when p = p' ->
transform p
| ShapeVar v -> Expr.Var v
| ShapeLambda (v, e) -> Expr.Lambda(v, transform e)
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map transform)
transform quote
let complement quote =
let rec transform q =
match q with
| And' (p, Not' p')
| And' (Not' p, p') when p = p' ->
<@@ false @@>
| Or' (p, Not' p')
| Or' (Not' p, p') when p = p' ->
<@@ true @@>
| ShapeVar v -> Expr.Var v
| ShapeLambda (v, e) -> Expr.Lambda(v, transform e)
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map transform)
transform quote
let doubleNegation quote =
match quote with
| Not' (Not' p) ->
p
| _ ->
quote
let deMorgan quote =
match quote with
| Or' (Not' p, Not' p') ->
<@@ not (%%p && %%p') @@>
| And' (Not' p, Not' p') ->
<@@ not (%%p || %%p') @@>
| _ ->
quote
let beta quote =
let rec findApplication values q =
match q with
| Application (body, value) ->
findApplication (value::values) body
| ShapeLambda (v, e) ->
match values with
| [] ->
Expr.Lambda(v, findApplication [] e)
| h::t ->
findApplication t (replaceVar v.Name h e)
| ShapeVar v ->
Expr.Var v
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map (findApplication values))
and replaceVar name value body =
match body with
| ShapeVar v ->
if v.Name = name then value else Expr.Var v
| ShapeLambda (v, e) ->
Expr.Lambda(v, replaceVar name value e)
| ShapeCombination (o, es) ->
RebuildShapeCombination(o, es |> List.map (replaceVar name value))
findApplication [] quote
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment