Automated Reasoning in Erlang

sum_types.erl

%%
%% Inspired from http://phdp.github.io/posts/2015-04-05-automated-reasoning.html
%%

-module(sum_types) .
-export([simplify/1,print/1,main/0]) .

-type expr() :: myvar(string()) | const(integer()) | add(expr(),expr()) | mul(expr(),expr()) .

-type myvar(A) :: {var,A} .
-type const(A) :: {const,A} .
-type add(A,B) :: {add,A,B} .
-type mul(A,B) :: {mul,A,B} .

-spec simplify1(expr()) -> expr() .
-spec simplify(expr()) -> expr() .

simplify1(E) ->
    case E of
        {add,{const,0},X} -> X ;
        {add,X,{const,0}} -> X ;
        {add,{const,X},{const,Y}} -> {const,X+Y} ;
        {mul,{const,0},_} -> {const,0} ;
        {mul,_,{const,0}} -> {const,0} ;
        {mul,{const,1},X} -> X ;
        {mul,X,{const,1}} -> X ;
        {mul,{const,X},{const,Y}} -> {const,X*Y} ;
        _ -> E
    end .
        

simplify(E) ->
    case E of
        {add,X,Y} -> simplify1({add,simplify(X),simplify(Y)}) ;
        {mul,X,Y} -> simplify1({mul,simplify(X),simplify(Y)}) ;
        _ -> simplify1(E)
    end .
          
print(E) ->
    case E of
        {const,X} -> io:write(X) ;
        _ -> io:write("Could not simplify the expression to a constant.")
    end .

main() ->
    Ex = {add,
         {mul,{add,{const,1},{mul,{const,0},{var,"x"}}},{const,3}},
         {const,12}} ,
    
    S = simplify(Ex) ,

    print(S) .