# Using erlang2trs: some examples

Using the available tool, one can transform some provided examples as follows.

## Example 1

### Source Erlang code

```main -> factorial({atom_s,{atom_s,{atom_s,atom_z}}}).

factorial(X) -> case X of
atom_z -> {atom_s,atom_z};
{atom_s,Y} -> mult(X,factorial(Y))
end.

mult(X,Y) -> case X of
atom_z -> atom_z;
{atom_s,Z} -> sum(Y,mult(Z,Y))
end.

sum(X,Y) -> case X of
atom_z -> Y;
{atom_s,Z} -> W=sum(Z,Y), {atom_s,W}
end.
```

### Transformed Curry program

```data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | S | Z | T2 Exp Exp

reduce_global current visited = current

send_msg _ _ [] = []
send_msg j e (State i b m : s)
| i==j      = State i b (m++[e]) : s
| otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys

init = reduce_global [State 0 (I 2) [], State 1 main []] []

main = (factorial (T2 S (T2 S (T2 S Z))))
fun1 Z (x:[])  = (T2 S Z)
fun1 (T2 S y) (x:[])  = (mult x (factorial y))
factorial x  = (fun1 x (x:[]))
fun2 Z (x:(y:[]))  = Z
fun2 (T2 S z) (x:(y:[]))  = (sum y (mult z y))
mult x y  = (fun2 x (x:(y:[])))
fun3 Z (x:(y:[]))  = y
fun3 (T2 S z) (x:(y:[]))  = (fun4 (sum z y) (y:(z:[])))
fun4 w (y:(z:[]))  = (T2 S w)
sum x y  = (fun3 x (x:(y:[])))
```

## Example 2

### Source Erlang code

```main -> Pid = spawn(foo),
Pid ! atom_hello.

atom_hello -> atom_yes;
atom_world -> atom_no
end.
```

### Transformed Curry program

```data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | Hello | Yes | No | World

reduce_global current visited
| member current visited  = current
| isFinal current         = current
| otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
| (isDef exp)  = False
| otherwise    = isFinal xs

isDef x = case x of
SPAWN _ _ _  -> True
SEND _ _ _ _ -> True
AREC _ _ _   -> True
SELF _ _     -> True
_            -> False

brec 3 fresh = case fresh of
Hello -> True
World -> True
_ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i Hello m : ss)) visited = reduce_global (s0 : (ss ++ [State i Hello m])) visited
reduce (s0 : (State i Yes m : ss)) visited = reduce_global (s0 : (ss ++ [State i Yes m])) visited
reduce (s0 : (State i No m : ss)) visited = reduce_global (s0 : (ss ++ [State i No m])) visited
reduce (s0 : (State i World m : ss)) visited = reduce_global (s0 : (ss ++ [State i World m])) visited

reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited

reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited

reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited

send_msg _ _ [] = []
send_msg j e (State i b m : s)
| i==j      = State i b (m++[e]) : s
| otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys

init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 2 e fresh  = e
spawn 1 pid []  = (SEND 2 pid Hello [])
main = (SPAWN 1 foo [])
rec 3 Hello []  = Yes
rec 3 World []  = No
foo = (AREC 3 [] [])
```

## Example 3

### Source Erlang code

```main -> Ser = spawn(server),
Cli = spawn(client(Ser)),
Cli ! atom_start.

Pid -> atom_ok
end,
server.

client(Ser) -> S = self,
X -> Ser ! S
end,
client(Ser).
```

### Transformed Curry program

```data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | Start

reduce_global current visited
| member current visited  = current
| isFinal current         = current
| otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
| (isDef exp)  = False
| otherwise    = isFinal xs

isDef x = case x of
SPAWN _ _ _  -> True
SEND _ _ _ _ -> True
AREC _ _ _   -> True
SELF _ _     -> True
_            -> False

brec 4 fresh = case fresh of
pid -> True
_ -> False

brec 6 fresh = case fresh of
x -> True
_ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i Start m : ss)) visited = reduce_global (s0 : (ss ++ [State i Start m])) visited

reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited

reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited

reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited

reduce (s0 : (State i (SELF n args) m : s)) visited = reduce_global (s0 : (s ++ [State i (self n (I i) args) m])) visited

send_msg _ _ [] = []
send_msg j e (State i b m : s)
| i==j      = State i b (m++[e]) : s
| otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys

init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 3 e fresh  = e
send 7 e (s:(ser:[]))  = (client ser)
spawn 2 cli (ser:[])  = (SEND 3 cli Start [])
spawn 1 ser []  = (SPAWN 2 (client ser) (ser:[]))
main = (SPAWN 1 server [])
rec 4 pid []  = server
rec 6 x (s:(ser:[]))  = (SEND 7 ser s (s:(ser:[])))
server = (AREC 4 [] [])
self 5 s (ser:[])  = (AREC 6 [] (s:(ser:[])))
client ser  = (SELF 5 (ser:[]))
```

## Example 4

### Source Erlang code

```main -> Pid2 = spawn(proc2),
Pid1 = spawn(proc1(Pid2)),
Pid1 ! atom_hello,
Pid2 ! atom_world.

X -> Pid ! X
end.

X -> atom_ok
end.
```

### Transformed Curry program

```data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | World | Hello | Ok

reduce_global current visited
| member current visited  = current
| isFinal current         = current
| otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
| (isDef exp)  = False
| otherwise    = isFinal xs

isDef x = case x of
SPAWN _ _ _  -> True
SEND _ _ _ _ -> True
AREC _ _ _   -> True
SELF _ _     -> True
_            -> False

brec 5 fresh = case fresh of
x -> True
_ -> False

brec 7 fresh = case fresh of
x -> True
_ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i World m : ss)) visited = reduce_global (s0 : (ss ++ [State i World m])) visited
reduce (s0 : (State i Hello m : ss)) visited = reduce_global (s0 : (ss ++ [State i Hello m])) visited
reduce (s0 : (State i Ok m : ss)) visited = reduce_global (s0 : (ss ++ [State i Ok m])) visited

reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited

reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited

reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited

send_msg _ _ [] = []
send_msg j e (State i b m : s)
| i==j      = State i b (m++[e]) : s
| otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys

init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 4 e fresh  = e
send 3 e (pid1:(pid2:[]))  = (SEND 4 pid2 World [])
send 6 e fresh  = e
spawn 2 pid1 (pid2:[])  = (SEND 3 pid1 Hello (pid1:(pid2:[])))
spawn 1 pid2 []  = (SPAWN 2 (proc1 pid2) (pid2:[]))
main = (SPAWN 1 proc2 [])
rec 5 x (pid:[])  = (SEND 6 pid x [])
rec 7 x []  = Ok
proc1 pid  = (AREC 5 [] (pid:[]))
proc2 = (AREC 7 [] [])
```

## Example 5

### Source Erlang code

```main -> Pid = spawn(proc2),
Pid ! atom_a.

proc2 -> Pid = spawn(proc3),
X -> Pid ! X
end.

X -> atom_ok
end.
```

### Transformed Curry program

```data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | A | Ok

reduce_global current visited
| member current visited  = current
| isFinal current         = current
| otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
| (isDef exp)  = False
| otherwise    = isFinal xs

isDef x = case x of
SPAWN _ _ _  -> True
SEND _ _ _ _ -> True
AREC _ _ _   -> True
SELF _ _     -> True
_            -> False

brec 4 fresh = case fresh of
x -> True
_ -> False

brec 6 fresh = case fresh of
x -> True
_ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i A m : ss)) visited = reduce_global (s0 : (ss ++ [State i A m])) visited
reduce (s0 : (State i Ok m : ss)) visited = reduce_global (s0 : (ss ++ [State i Ok m])) visited

reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited

reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited

reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited

send_msg _ _ [] = []
send_msg j e (State i b m : s)
| i==j      = State i b (m++[e]) : s
| otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys

init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 2 e fresh  = e
send 5 e fresh  = e
spawn 1 pid []  = (SEND 2 pid A [])
spawn 3 pid []  = (AREC 4 [] (pid:[]))
main = (SPAWN 1 proc2 [])
rec 4 x (pid:[])  = (SEND 5 pid x [])
rec 6 x []  = Ok
proc2 = (SPAWN 3 proc3 [])
proc3 = (AREC 6 [] [])
```

## Example 6

### Source Erlang code

```main ->
Res = spawn(res({atom_a,atom_a})),
Left = spawn(left(Res)),
Right = spawn(right(Res)).

res(State) ->
{atom_c,S} -> S ! State
end,
{atom_u,NewState} -> res(NewState)
end.

left(Res) ->
S = self,
Res ! {atom_c,S},
Res ! {atom_u,{atom_b,B}},
Res ! {atom_c,S},
left_aux(Res)
end.

left_aux(Res) ->
Res ! {atom_u,{atom_b,atom_b}}
end.

right(Res) ->
S = self,
Res ! {atom_c,S},
Res ! {atom_u,{A,atom_b}},
Res ! {atom_c,S},
right_aux(Res)
end.

right_aux(Res) ->
Res ! {atom_u,{atom_b,atom_b}}
end.
```

### Transformed Curry program

```data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | A | U | C | B | T2 Exp Exp

reduce_global current visited
| member current visited  = current
| isFinal current         = current
| otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
| (isDef exp)  = False
| otherwise    = isFinal xs

isDef x = case x of
SPAWN _ _ _  -> True
SEND _ _ _ _ -> True
AREC _ _ _   -> True
SELF _ _     -> True
_            -> False

brec 4 fresh = case fresh of
(T2 C s) -> True
_ -> False

brec 6 fresh = case fresh of
(T2 U newstate) -> True
_ -> False

brec 9 fresh = case fresh of
(T2 A b) -> True
_ -> False

brec 12 fresh = case fresh of
(T2 B A) -> True
_ -> False

brec 16 fresh = case fresh of
(T2 a A) -> True
_ -> False

brec 19 fresh = case fresh of
(T2 A B) -> True
_ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i (T2 fresh1 fresh2) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (T2 fresh1 fresh2) m])) visited
reduce (s0 : (State i A m : ss)) visited = reduce_global (s0 : (ss ++ [State i A m])) visited
reduce (s0 : (State i U m : ss)) visited = reduce_global (s0 : (ss ++ [State i U m])) visited
reduce (s0 : (State i C m : ss)) visited = reduce_global (s0 : (ss ++ [State i C m])) visited
reduce (s0 : (State i B m : ss)) visited = reduce_global (s0 : (ss ++ [State i B m])) visited

reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited

reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited

reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited

reduce (s0 : (State i (SELF n args) m : s)) visited = reduce_global (s0 : (s ++ [State i (self n (I i) args) m])) visited

send_msg _ _ [] = []
send_msg j e (State i b m : s)
| i==j      = State i b (m++[e]) : s
| otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys

init = reduce_global [State 0 (I 2) [], State 1 main []] []

spawn 3 right fresh  = right
spawn 2 left (res:[])  = (SPAWN 3 (right res) [])
spawn 1 res []  = (SPAWN 2 (left res) (res:[]))
main = (SPAWN 1 (res (T2 A A)) [])
rec 6 (T2 U newstate) []  = (res newstate)
rec 4 (T2 C s) (state:[])  = (SEND 5 s state (s:(state:[])))
rec 9 (T2 A b) (res:(s:[]))  = (SEND 10 res (T2 U (T2 B b)) (b:(res:(s:[]))))
rec 12 (T2 B A) (res:[])  = (SEND 13 res (T2 U (T2 B B)) [])
rec 16 (T2 a A) (res:(s:[]))  = (SEND 17 res (T2 U (T2 a B)) (a:(res:(s:[]))))
rec 19 (T2 A B) (res:[])  = (SEND 20 res (T2 U (T2 B B)) [])
send 5 e (s:(state:[]))  = (AREC 6 [] [])
send 11 e (res:(s:[]))  = (left_aux res)
send 10 e (b:(res:(s:[])))  = (SEND 11 res (T2 C s) (res:(s:[])))
send 8 e (res:(s:[]))  = (AREC 9 [] (res:(s:[])))
send 13 e fresh  = e
send 18 e (res:(s:[]))  = (right_aux res)
send 17 e (a:(res:(s:[])))  = (SEND 18 res (T2 C s) (res:(s:[])))
send 15 e (res:(s:[]))  = (AREC 16 [] (res:(s:[])))
send 20 e fresh  = e
res state  = (AREC 4 [] (state:[]))
self 7 s (res:[])  = (SEND 8 res (T2 C s) (res:(s:[])))
self 14 s (res:[])  = (SEND 15 res (T2 C s) (res:(s:[])))
left res  = (SELF 7 (res:[]))
left_aux res  = (AREC 12 [] (res:[]))
right res  = (SELF 14 (res:[]))
right_aux res  = (AREC 19 [] (res:[]))
```