Anonymous

type expr = Var of int | Prod of expr * expr | LInv of expr | RInv of expr
let prod x y = Prod (x, y) (* prod is the group product *)

let rec string_of_expr expr =
    match expr with
        |LInv a -> "L(" ^ (string_of_expr a) ^ ")"
        |RInv a -> "R(" ^ (string_of_expr a) ^ ")"
        |Var a -> "g_" ^ (string_of_int a)
        |Prod (a, b) -> "(" ^ (string_of_expr a) ^
                        "*" ^ (string_of_expr b) ^ ")"

(* check to see if two expressions are identical *)
let rec equiv expr1 expr2 =
    match (expr1, expr2) with
        |(LInv a, LInv b) -> equiv a b
        |(RInv a, RInv b) -> equiv a b
        |(Var a, Var b) -> a = b
        |(Prod (a, b), Prod (c, d)) -> (equiv a c) && (equiv b d)
        |_ -> false


let rec test_all test lst ele =
    match lst with
        |[] -> false
        |x :: xs -> if (test x ele) then true else test_all test xs ele

let nub_by test lst =
    let rec nbr test listin listout =
        match listin with
            |[] -> listout
            |x :: xs ->
                if (test_all test listout x)
                    then nbr test xs listout
                    else nbr test xs (x :: listout) in
    nbr test lst []

let prod_id_l expr =
    prod (Var 0) expr

let prod_id_r expr =
    prod expr (Var 0)

let prod_red expr =
    match expr with
         Prod (a, Var 0)
        |Prod (Var 0, a) -> a
        |_ -> expr

let assoc_l expr =
    match expr with
        Prod (a, Prod (b, c)) -> Prod (Prod (a, b), c)
        |_ -> expr

let assoc_r expr =
    match expr with
        Prod (Prod (a, b), c) -> Prod (a, Prod (b, c))
        |_ -> expr

let inv_red expr =
    match expr with
        Prod (a, RInv b)
       |Prod (LInv a, b) -> if (equiv a b) then (Var 0) else expr
       |_ -> expr

let list_of_ids = [prod_id_l; prod_id_r; prod_red; assoc_l; assoc_r; inv_red]

let rec substitute expr_lst =
    let rec concat_lists lst acc =
        match lst with [] -> acc | x :: xs -> concat_lists xs (x @ acc) in
    let deal_with_this_one expr =
        (* first, try applying to this node *)
        let top_eval = List.map (fun f -> f expr) list_of_ids in
        (* now a bunch of recursion rules to propagate along products *)
        match expr with
            |Prod (expr1, expr2) ->
                let first_half  = List.map (fun expr -> prod expr expr2) (substitute [expr1]) in
                let second_half = List.map (fun expr -> prod expr1 expr) (substitute [expr2]) in
                first_half @ second_half @ top_eval
            |_ -> top_eval in
    let big_expr_lst = List.map deal_with_this_one expr_lst in
    nub_by equiv (concat_lists big_expr_lst [])

let prove_with_hint expr1 expr2 exprstart =
    let rec prv expr1 expr2 results =
        let new_results = substitute results in
        List.iter (fun n -> print_endline (string_of_expr n)) results;
        print_endline "---";
        if (test_all equiv results expr1) && (test_all equiv results expr2)
            then true
            else prv expr1 expr2 new_results in
    prv expr1 expr2 [exprstart]

let prove expr1 expr2 =
    prove_with_hint expr1 expr2 expr1