From faadf8cc3aede210cf033d17912bab41a95a9211 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Tue, 11 Jan 2022 17:35:26 +0100 Subject: [PATCH 1/8] Rename `cauder_eval` functions to match those from `erl_eval` --- src/cauder_eval.erl | 68 ++++++++++++++++--------------- src/cauder_semantics_forwards.erl | 10 ++--- 2 files changed, 40 insertions(+), 38 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 620882e..9935b84 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -1,8 +1,8 @@ -module(cauder_eval). %% API --export([seq/3, abstract/1, concrete/1, is_value/1, is_reducible/2]). --export([match_rec_pid/6, match_rec_uid/4]). +-export([exprs/3, abstract/1, concrete/1, is_value/1, is_reducible/2]). +-export([match_receive_pid/6, match_receive_uid/4]). -export([clause_line/3]). -include("cauder_message.hrl"). @@ -47,19 +47,19 @@ %% %% @see is_reducible/2 --spec eval_list(Bindings, Expressions, Stack) -> Result when +-spec expr_list(Bindings, Expressions, Stack) -> Result when Bindings :: cauder_bindings:bindings(), Expressions :: [cauder_syntax:abstract_expr()], Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). -eval_list(Bs, [E | Es], Stk) -> +expr_list(Bs, [E | Es], Stk) -> case is_reducible(E, Bs) of true -> R = #result{expr = Es1} = expr(Bs, E, Stk), R#result{expr = Es1 ++ Es}; false -> - R = #result{expr = Es1} = eval_list(Bs, Es, Stk), + R = #result{expr = Es1} = expr_list(Bs, Es, Stk), R#result{expr = [E | Es1]} end. @@ -76,13 +76,13 @@ eval_list(Bs, [E | Es], Stk) -> %% %% @see is_reducible/2 --spec seq(Bindings, Expressions, Stack) -> Result when +-spec exprs(Bindings, Expressions, Stack) -> Result when Bindings :: cauder_bindings:bindings(), Expressions :: [cauder_syntax:abstract_expr()], Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). -seq(Bs, [E | Es], Stk) -> +exprs(Bs, [E | Es], Stk) -> case is_reducible(E, Bs) of false -> case Es of @@ -157,7 +157,7 @@ expr(Bs, E = {cons, Line, H0, T0}, Stk) -> end end; expr(Bs, E = {tuple, Line, Es0}, Stk) -> - R = #result{expr = Es} = eval_list(Bs, Es0, Stk), + R = #result{expr = Es} = expr_list(Bs, Es0, Stk), case is_value(Es) of true -> Tuple = list_to_tuple(lists:map(fun concrete/1, Es)), @@ -367,7 +367,7 @@ expr(Bs0, E = {local_call, Line, F, As}, Stk0) -> expr(Bs0, E = {remote_call, Line, M, F, As}, Stk0) -> case is_reducible(As, Bs0) of true -> eval_and_update({Bs0, As, Stk0}, {5, E}); - false -> eval_remote_call(M, F, As, Stk0, Line, Bs0) + false -> remote_call(M, F, As, Stk0, Line, Bs0) end; % TODO Handle calls to self/0, spawn/1, spawn/3 expr(Bs0, E = {apply, Line, M0, F0, As}, Stk0) -> @@ -385,7 +385,7 @@ expr(Bs0, E = {apply, Line, M0, F0, As}, Stk0) -> false -> M = concrete(M0), F = concrete(F0), - eval_remote_call(M, F, As, Stk0, Line, Bs0) + remote_call(M, F, As, Stk0, Line, Bs0) end end end; @@ -468,7 +468,7 @@ expr(Bs, E = {'orelse', Line, Lhs, Rhs}, Stk) -> end end. -eval_remote_call(M, F, As, Stk0, Line, Bs0) -> +remote_call(M, F, As, Stk0, Line, Bs0) -> A = length(As), case cauder_utils:fundef_lookup({M, F, A}) of {Exported, Cs} -> @@ -498,7 +498,7 @@ eval_remote_call(M, F, As, Stk0, Line, Bs0) -> match_if(_, []) -> nomatch; match_if(Bs, [{'clause', _, [], G, B} | Cs]) -> - case concrete(eval_guard_seq(Bs, G)) of + case concrete(guard_seq(Bs, G)) of true -> {match, B}; false -> match_if(Bs, Cs) end. @@ -520,7 +520,7 @@ match_case(Bs, Cs, V) -> match_clause(Bs, Cs, [V]). match_fun(Cs, Vs) -> match_clause(cauder_bindings:new(), Cs, Vs). --spec match_rec_pid(Clauses, Bindings, RecipientPid, Mail, Sched, Sys) -> +-spec match_receive_pid(Clauses, Bindings, RecipientPid, Mail, Sched, Sys) -> {NewBindings, Body, {Message, QueuePosition}, NewMail} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), @@ -535,7 +535,7 @@ when QueuePosition :: pos_integer(), NewMail :: cauder_mailbox:mailbox(). -match_rec_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> +match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> case cauder_mailbox:find_destination(Pid, Mail) of [] -> nomatch; @@ -544,7 +544,7 @@ match_rec_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> ?SCHEDULER_Manual -> FoldQueue = fun(Msg, Map1) -> - case match_rec(Cs, Bs, #message{uid = Uid} = Msg) of + case match_receive(Cs, Bs, #message{uid = Uid} = Msg) of {match, Bs1, Body} -> maps:put(Uid, {Bs1, Body, Msg}, Map1); nomatch -> skip end @@ -572,7 +572,7 @@ match_rec_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> MatchingBranches = lists:filtermap( fun(Queue) -> {value, Msg} = queue:peek(Queue), - case match_rec(Cs, Bs, Msg) of + case match_receive(Cs, Bs, Msg) of {match, Bs1, Body} -> {true, {Bs1, Body, Msg}}; nomatch -> false end @@ -590,16 +590,16 @@ match_rec_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> end end. --spec match_rec(Clauses, Bindings, Message) -> {match, NewBindings, Body} | nomatch when +-spec match_receive(Clauses, Bindings, Message) -> {match, NewBindings, Body} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), Bindings :: cauder_bindings:bindings(), Message :: cauder_message:message(), NewBindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(). -match_rec(Cs, Bs0, #message{val = Value}) -> match_clause(Bs0, Cs, [abstract(Value)]). +match_receive(Cs, Bs0, #message{val = Value}) -> match_clause(Bs0, Cs, [abstract(Value)]). --spec match_rec_uid(Clauses, Bindings, Uid, Mail) -> +-spec match_receive_uid(Clauses, Bindings, Uid, Mail) -> {NewBindings, Body, {Message, QueuePosition}, NewMail} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), @@ -612,7 +612,7 @@ when QueuePosition :: pos_integer(), NewMail :: cauder_mailbox:mailbox(). -match_rec_uid(Cs, Bs0, Uid, Mail0) -> +match_receive_uid(Cs, Bs0, Uid, Mail0) -> case cauder_mailbox:take(Uid, Mail0) of error -> nomatch; @@ -635,7 +635,7 @@ match_clause(_, [], _) -> match_clause(Bs0, [{'clause', _, Ps, G, B} | Cs], Vs) -> case match(Bs0, Ps, Vs) of {match, Bs} -> - case concrete(eval_guard_seq(Bs, G)) of + case concrete(guard_seq(Bs, G)) of true -> {match, Bs, B}; false -> match_clause(Bs0, Cs, Vs) end; @@ -654,7 +654,7 @@ clause_line(_, [], _) -> clause_line(Bs0, [{'clause', Line, Ps, G, _} | Cs], Vs) -> case match(Bs0, Ps, Vs) of {match, Bs} -> - case concrete(eval_guard_seq(Bs, G)) of + case concrete(guard_seq(Bs, G)) of true -> Line; false -> clause_line(Bs0, Cs, Vs) end; @@ -726,36 +726,38 @@ match_tuple([E | Es], Tuple, I, Bs0) -> {match, Bs} = match1(E, element(I, Tuple), Bs0), match_tuple(Es, Tuple, I + 1, Bs). --spec eval_guard_seq(Bindings, Guards) -> Boolean when +%%%============================================================================= + +-spec guard_seq(Bindings, Guards) -> Boolean when Bindings :: cauder_bindings:bindings(), Guards :: cauder_syntax:af_guard_seq(), Boolean :: cauder_syntax:af_boolean(). -eval_guard_seq(_, []) -> +guard_seq(_, []) -> abstract(true); -eval_guard_seq(Bs, Gs) when is_list(Gs) -> +guard_seq(Bs, Gs) when is_list(Gs) -> % In a guard sequence, guards are evaluated until one is true. The remaining guards, if any, are not evaluated. % See: https://erlang.org/doc/reference_manual/expressions.html#guard-sequences - abstract(lists:any(fun(G) -> concrete(eval_guard(Bs, G)) end, Gs)). + abstract(lists:any(fun(G) -> concrete(guard(Bs, G)) end, Gs)). --spec eval_guard(Bindings, Guard) -> Boolean when +-spec guard(Bindings, Guard) -> Boolean when Bindings :: cauder_bindings:bindings(), Guard :: cauder_syntax:af_guard(), Boolean :: cauder_syntax:af_boolean(). -eval_guard(Bs, G) when is_list(G) -> - abstract(lists:all(fun(Gt) -> concrete(eval_guard_test(Bs, Gt)) end, G)). +guard(Bs, G) when is_list(G) -> + abstract(lists:all(fun(Gt) -> concrete(guard_test(Bs, Gt)) end, G)). --spec eval_guard_test(Bindings, GuardTest) -> GuardTest | Boolean when +-spec guard_test(Bindings, GuardTest) -> GuardTest | Boolean when Bindings :: cauder_bindings:bindings(), GuardTest :: cauder_syntax:af_guard_test(), Boolean :: cauder_syntax:af_boolean(). -eval_guard_test(Bs, Gt) -> +guard_test(Bs, Gt) -> case is_reducible(Gt, Bs) of true -> #result{expr = [Gt1]} = expr(Bs, Gt, cauder_stack:new()), - eval_guard_test(Bs, Gt1); + guard_test(Bs, Gt1); false -> Gt end. @@ -831,7 +833,7 @@ is_value(E) when is_tuple(E) -> false. Result :: cauder_eval:result(). eval_and_update({Bs, Es, Stk}, {Index, Tuple}) when is_list(Es) -> - R = #result{expr = Es1} = eval_list(Bs, Es, Stk), + R = #result{expr = Es1} = expr_list(Bs, Es, Stk), R#result{expr = [setelement(Index, Tuple, Es1)]}; eval_and_update({Bs, E, Stk}, {Index, Tuple}) -> R = #result{expr = [E1]} = expr(Bs, E, Stk), diff --git a/src/cauder_semantics_forwards.erl b/src/cauder_semantics_forwards.erl index 5aaad74..a16af94 100644 --- a/src/cauder_semantics_forwards.erl +++ b/src/cauder_semantics_forwards.erl @@ -39,7 +39,7 @@ step(Pid, Sys, Sched, Mode) -> #process{stack = Stk0, env = Bs0, expr = Es0} = cauder_pool:get(Pid, Sys#system.pool), - Result = cauder_eval:seq(Bs0, Es0, Stk0), + Result = cauder_eval:exprs(Bs0, Es0, Stk0), case Result#result.label of #label_tau{} -> rule_local(Pid, Result, Sys); @@ -442,7 +442,7 @@ rule_receive( {{Bs1, Es1, {Msg, QPos}, Mail1}, Log1} = case Mode of normal -> - Match = cauder_eval:match_rec_pid(Cs, Bs, Pid, Mail, Sched, Sys), + Match = cauder_eval:match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys), {_, _, {#message{uid = Uid}, _}, _} = Match, %% If the chosen message is the same specified in the log don't invalidate the log Log = @@ -453,7 +453,7 @@ rule_receive( {Match, Log}; replay -> {#log_receive{uid = Uid}, Log} = cauder_log:pop_receive(Pid, Log0), - Match = cauder_eval:match_rec_uid(Cs, Bs, Uid, Mail), + Match = cauder_eval:match_receive_uid(Cs, Bs, Uid, Mail), {Match, Log} end, @@ -601,10 +601,10 @@ check_reducibility(Cs, Pid, #system{mail = Mail, log = Log} = Sys, Mode, 'receiv IsMatch = case Mode of normal -> - cauder_eval:match_rec_pid(Cs, Bs, Pid, Mail, ?SCHEDULER_Random, Sys) =/= nomatch; + cauder_eval:match_receive_pid(Cs, Bs, Pid, Mail, ?SCHEDULER_Random, Sys) =/= nomatch; replay -> {value, #log_receive{uid = Uid}} = cauder_log:peek(Pid, Log), - cauder_eval:match_rec_uid(Cs, Bs, Uid, Mail) =/= nomatch + cauder_eval:match_receive_uid(Cs, Bs, Uid, Mail) =/= nomatch end, case IsMatch of true -> From 6cf1b9e7bbf1dd084c15b0f6f863abdb791957cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Tue, 11 Jan 2022 22:14:50 +0100 Subject: [PATCH 2/8] Reorder `expr_list/3` function --- src/cauder_eval.erl | 50 ++++++++++++++++++++++----------------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 9935b84..df9ae1c 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -38,31 +38,6 @@ %%% API %%%============================================================================= -%%------------------------------------------------------------------------------ -%% @doc Evaluates the first reducible expression from the given list. -%% -%% Evaluates the first reducible expression from the given list of expressions, -%% given an environment and a call stack, then returns a record with the updated -%% information and a label indicating the type of step performed. -%% -%% @see is_reducible/2 - --spec expr_list(Bindings, Expressions, Stack) -> Result when - Bindings :: cauder_bindings:bindings(), - Expressions :: [cauder_syntax:abstract_expr()], - Stack :: cauder_stack:stack(), - Result :: cauder_eval:result(). - -expr_list(Bs, [E | Es], Stk) -> - case is_reducible(E, Bs) of - true -> - R = #result{expr = Es1} = expr(Bs, E, Stk), - R#result{expr = Es1 ++ Es}; - false -> - R = #result{expr = Es1} = expr_list(Bs, Es, Stk), - R#result{expr = [E | Es1]} - end. - %%------------------------------------------------------------------------------ %% @doc Evaluates the given sequence of expression. %% @@ -468,6 +443,31 @@ expr(Bs, E = {'orelse', Line, Lhs, Rhs}, Stk) -> end end. +%%------------------------------------------------------------------------------ +%% @doc Evaluates the first reducible expression from the given list. +%% +%% Evaluates the first reducible expression from the given list of expressions, +%% given an environment and a call stack, then returns a record with the updated +%% information and a label indicating the type of step performed. +%% +%% @see is_reducible/2 + +-spec expr_list(Bindings, Expressions, Stack) -> Result when + Bindings :: cauder_bindings:bindings(), + Expressions :: [cauder_syntax:abstract_expr()], + Stack :: cauder_stack:stack(), + Result :: cauder_eval:result(). + +expr_list(Bs, [E | Es], Stk) -> + case is_reducible(E, Bs) of + true -> + R = #result{expr = Es1} = expr(Bs, E, Stk), + R#result{expr = Es1 ++ Es}; + false -> + R = #result{expr = Es1} = expr_list(Bs, Es, Stk), + R#result{expr = [E | Es1]} + end. + remote_call(M, F, As, Stk0, Line, Bs0) -> A = length(As), case cauder_utils:fundef_lookup({M, F, A}) of From 0fd1ec09481a6927100105ab70eb7f38c90332f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Thu, 13 Jan 2022 00:22:58 +0100 Subject: [PATCH 3/8] Refactor to match signature of `erl_eval` functions. --- src/cauder_eval.erl | 324 +++++++++++++++--------------- src/cauder_semantics_forwards.erl | 14 +- src/cauder_syntax.erl | 2 +- 3 files changed, 170 insertions(+), 170 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index df9ae1c..bca0c99 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -51,13 +51,13 @@ %% %% @see is_reducible/2 --spec exprs(Bindings, Expressions, Stack) -> Result when - Bindings :: cauder_bindings:bindings(), +-spec exprs(Expressions, Bindings, Stack) -> Result when Expressions :: [cauder_syntax:abstract_expr()], + Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). -exprs(Bs, [E | Es], Stk) -> +exprs([E | Es], Bs, Stk) -> case is_reducible(E, Bs) of false -> case Es of @@ -76,7 +76,7 @@ exprs(Bs, [E | Es], Stk) -> #result{env = Bs, expr = Es, stack = Stk} end; true -> - #result{env = Bs1, expr = Es1, stack = Stk1} = Result = expr(Bs, E, Stk), + #result{env = Bs1, expr = Es1, stack = Stk1} = Result = expr(E, Bs, Stk), case cauder_stack:pop(Stk1) of {{value, #s_function{env = Bs2, expr = Es2} = Entry}, Stk} -> Entry1 = Entry#s_function{env = Bs1, expr = Es1 ++ Es}, @@ -102,19 +102,19 @@ exprs(Bs, [E | Es], Stk) -> %% @doc Evaluates the given `Expression' and returns a tuple with an updated %% environment, the expression that resulted from the evaluation, and a label. --spec expr(Bindings, Expression, Stack) -> Result when - Bindings :: cauder_bindings:bindings(), +-spec expr(Expression, Bindings, Stack) -> Result when Expression :: cauder_syntax:abstract_expr(), + Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). -expr(Bs, {var, Line, Name}, Stk) -> +expr({var, Line, Name}, Bs, Stk) -> {ok, Value} = cauder_bindings:find(Name, Bs), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk}; -expr(Bs, E = {cons, Line, H0, T0}, Stk) -> +expr(E = {cons, Line, H0, T0}, Bs, Stk) -> case is_reducible(H0, Bs) of true -> - R = #result{expr = [H]} = expr(Bs, H0, Stk), + R = #result{expr = [H]} = expr(H0, Bs, Stk), case is_value(H) andalso is_value(T0) of true -> R#result{expr = [{value, Line, [concrete(H) | concrete(T0)]}]}; false -> R#result{expr = [setelement(3, E, H)]} @@ -122,7 +122,7 @@ expr(Bs, E = {cons, Line, H0, T0}, Stk) -> false -> case is_reducible(T0, Bs) of true -> - R = #result{expr = [T]} = expr(Bs, T0, Stk), + R = #result{expr = [T]} = expr(T0, Bs, Stk), case is_value(H0) andalso is_value(T) of true -> R#result{expr = [{value, Line, [concrete(H0) | concrete(T)]}]}; false -> R#result{expr = [setelement(4, E, T)]} @@ -131,8 +131,8 @@ expr(Bs, E = {cons, Line, H0, T0}, Stk) -> #result{env = Bs, expr = [{value, Line, [concrete(H0) | concrete(T0)]}], stack = Stk} end end; -expr(Bs, E = {tuple, Line, Es0}, Stk) -> - R = #result{expr = Es} = expr_list(Bs, Es0, Stk), +expr(E = {tuple, Line, Es0}, Bs, Stk) -> + R = #result{expr = Es} = expr_list(Es0, Bs, Stk), case is_value(Es) of true -> Tuple = list_to_tuple(lists:map(fun concrete/1, Es)), @@ -140,8 +140,8 @@ expr(Bs, E = {tuple, Line, Es0}, Stk) -> false -> R#result{expr = [setelement(3, E, Es)]} end; -expr(Bs, {'if', Line, Cs}, Stk0) -> - case match_if(Bs, Cs) of +expr({'if', Line, Cs}, Bs, Stk0) -> + case match_if(Cs, Bs) of {match, Body} -> Var = cauder_utils:temp_variable(Line), Entry = #s_block{type = 'if', expr = Body, var = Var}, @@ -150,13 +150,13 @@ expr(Bs, {'if', Line, Cs}, Stk0) -> nomatch -> error(if_clause) end; -expr(Bs0, E = {'case', Line, A, Cs}, Stk0) -> +expr(E = {'case', Line, A, Cs}, Bs0, Stk0) -> case is_reducible(A, Bs0) of true -> - eval_and_update({Bs0, A, Stk0}, {3, E}); + eval_and_update({A, Bs0, Stk0}, {3, E}); false -> - case match_case(Bs0, Cs, A) of - {match, Bs, Body} -> + case match_case(Cs, A, Bs0) of + {match, Body, Bs} -> Var = cauder_utils:temp_variable(Line), Entry = #s_block{type = 'case', expr = Body, var = Var}, Stk = cauder_stack:push(Entry, Stk0), @@ -166,7 +166,7 @@ expr(Bs0, E = {'case', Line, A, Cs}, Stk0) -> end end; %% TODO Support receive with timeout -expr(Bs, {'receive', Line, Cs}, Stk0) -> +expr({'receive', Line, Cs}, Bs, Stk0) -> % TODO One of these variables is not necessary Var = cauder_utils:temp_variable(Line), VarBody = cauder_utils:temp_variable(Line), @@ -176,7 +176,7 @@ expr(Bs, {'receive', Line, Cs}, Stk0) -> #result{env = Bs, expr = [Var], stack = Stk, label = Label}; % TODO Support fun() as entry point argument? % TODO Handle calls to interpreted fun() from uninterpreted module -expr(Bs, {'make_fun', Line, Name, Cs}, Stk0) -> +expr({'make_fun', Line, Name, Cs}, Bs, Stk0) -> {ok, M} = cauder_stack:current_module(Stk0), Arity = length(element(3, hd(Cs))), Info = {{M, Name}, Bs, Cs}, @@ -192,61 +192,61 @@ expr(Bs, {'make_fun', Line, Name, Cs}, Stk0) -> _ -> error({argument_limit, Arity}) end, #result{env = Bs, expr = [{value, Line, Fun}], stack = Stk0}; -expr(Bs, E = {bif, Line, M, F, As}, Stk) -> +expr(E = {bif, Line, M, F, As}, Bs, Stk) -> case is_reducible(As, Bs) of true -> - eval_and_update({Bs, As, Stk}, {5, E}); + eval_and_update({As, Bs, Stk}, {5, E}); false -> Value = apply(M, F, lists:map(fun concrete/1, As)), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end; -expr(Bs, {self, Line}, Stk) -> +expr({self, Line}, Bs, Stk) -> Var = cauder_utils:temp_variable(Line), Label = #label_self{var = Var}, #result{env = Bs, expr = [Var], stack = Stk, label = Label}; -expr(Bs, {node, Line}, Stk) -> +expr({node, Line}, Bs, Stk) -> Var = cauder_utils:temp_variable(Line), Label = #label_node{var = Var}, #result{env = Bs, expr = [Var], stack = Stk, label = Label}; -expr(Bs, {nodes, Line}, Stk) -> +expr({nodes, Line}, Bs, Stk) -> Var = cauder_utils:temp_variable(Line), Label = #label_nodes{var = Var}, #result{env = Bs, expr = [Var], stack = Stk, label = Label}; -expr(Bs, E = {spawn, Line, Fun}, Stk) -> +expr(E = {spawn, Line, Fun}, Bs, Stk) -> case is_reducible(Fun, Bs) of true -> - eval_and_update({Bs, Fun, Stk}, {3, E}); + eval_and_update({Fun, Bs, Stk}, {3, E}); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_fun{var = Var, function = Fun}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end; -expr(Bs, E = {spawn, Line, N, Fun}, Stk) -> +expr(E = {spawn, Line, N, Fun}, Bs, Stk) -> case is_reducible(N, Bs) of true -> - eval_and_update({Bs, N, Stk}, {3, E}); + eval_and_update({N, Bs, Stk}, {3, E}); false -> case is_reducible(Fun, Bs) of true -> - eval_and_update({Bs, Fun, Stk}, {4, E}); + eval_and_update({Fun, Bs, Stk}, {4, E}); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_fun{var = Var, node = concrete(N), function = Fun}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end end; -expr(Bs, E = {spawn, Line, M, F, As}, Stk) -> +expr(E = {spawn, Line, M, F, As}, Bs, Stk) -> case is_reducible(M, Bs) of true -> - eval_and_update({Bs, M, Stk}, {3, E}); + eval_and_update({M, Bs, Stk}, {3, E}); false -> case is_reducible(F, Bs) of true -> - eval_and_update({Bs, F, Stk}, {4, E}); + eval_and_update({F, Bs, Stk}, {4, E}); false -> case is_reducible(As, Bs) of true -> - eval_and_update({Bs, As, Stk}, {5, E}); + eval_and_update({As, Bs, Stk}, {5, E}); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_mfa{ @@ -259,22 +259,22 @@ expr(Bs, E = {spawn, Line, M, F, As}, Stk) -> end end end; -expr(Bs, E = {spawn, Line, N, M, F, As}, Stk) -> +expr(E = {spawn, Line, N, M, F, As}, Bs, Stk) -> case is_reducible(N, Bs) of true -> - eval_and_update({Bs, N, Stk}, {3, E}); + eval_and_update({N, Bs, Stk}, {3, E}); false -> case is_reducible(M, Bs) of true -> - eval_and_update({Bs, M, Stk}, {4, E}); + eval_and_update({M, Bs, Stk}, {4, E}); false -> case is_reducible(F, Bs) of true -> - eval_and_update({Bs, F, Stk}, {5, E}); + eval_and_update({F, Bs, Stk}, {5, E}); false -> case is_reducible(As, Bs) of true -> - eval_and_update({Bs, As, Stk}, {6, E}); + eval_and_update({As, Bs, Stk}, {6, E}); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_mfa{ @@ -289,74 +289,74 @@ expr(Bs, E = {spawn, Line, N, M, F, As}, Stk) -> end end end; -expr(Bs, E = {start, Line, N}, Stk) -> +expr(E = {start, Line, N}, Bs, Stk) -> case is_reducible(N, Bs) of true -> - eval_and_update({Bs, N, Stk}, {3, E}); + eval_and_update({N, Bs, Stk}, {3, E}); false -> Var = cauder_utils:temp_variable(Line), Label = #label_start{var = Var, name = concrete(N)}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end; -expr(Bs, E = {start, Line, H, N}, Stk) -> +expr(E = {start, Line, H, N}, Bs, Stk) -> case is_reducible(H, Bs) of true -> - eval_and_update({Bs, H, Stk}, {3, E}); + eval_and_update({H, Bs, Stk}, {3, E}); false -> case is_reducible(N, Bs) of true -> - eval_and_update({Bs, N, Stk}, {4, E}); + eval_and_update({N, Bs, Stk}, {4, E}); false -> Var = cauder_utils:temp_variable(Line), Label = #label_start{var = Var, name = concrete(N), host = concrete(H)}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end end; -expr(Bs, E = {Send, _, L, R}, Stk) when Send =:= 'send' orelse Send =:= 'send_op' -> +expr(E = {Send, _, L, R}, Bs, Stk) when Send =:= 'send' orelse Send =:= 'send_op' -> case is_reducible(L, Bs) of true -> - eval_and_update({Bs, L, Stk}, {3, E}); + eval_and_update({L, Bs, Stk}, {3, E}); false -> case is_reducible(R, Bs) of true -> - eval_and_update({Bs, R, Stk}, {4, E}); + eval_and_update({R, Bs, Stk}, {4, E}); false -> Label = #label_send{dst = concrete(L), val = concrete(R)}, #result{env = Bs, expr = [R], stack = Stk, label = Label} end end; -expr(Bs0, E = {local_call, Line, F, As}, Stk0) -> +expr(E = {local_call, Line, F, As}, Bs0, Stk0) -> case is_reducible(As, Bs0) of true -> - eval_and_update({Bs0, As, Stk0}, {4, E}); + eval_and_update({As, Bs0, Stk0}, {4, E}); false -> {ok, M} = cauder_stack:current_module(Stk0), A = length(As), {_, Cs} = cauder_utils:fundef_lookup({M, F, A}), - {match, Bs, Body} = match_fun(Cs, As), + {match, Body, Bs} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Entry = #s_function{mfa = {M, F, A}, env = Bs, expr = Body, var = Var}, Stk = cauder_stack:push(Entry, Stk0), #result{env = Bs0, expr = [Var], stack = Stk} end; -expr(Bs0, E = {remote_call, Line, M, F, As}, Stk0) -> +expr(E = {remote_call, Line, M, F, As}, Bs0, Stk0) -> case is_reducible(As, Bs0) of - true -> eval_and_update({Bs0, As, Stk0}, {5, E}); + true -> eval_and_update({As, Bs0, Stk0}, {5, E}); false -> remote_call(M, F, As, Stk0, Line, Bs0) end; % TODO Handle calls to self/0, spawn/1, spawn/3 -expr(Bs0, E = {apply, Line, M0, F0, As}, Stk0) -> +expr(E = {apply, Line, M0, F0, As}, Bs0, Stk0) -> case is_reducible(M0, Bs0) of true -> - eval_and_update({Bs0, M0, Stk0}, {3, E}); + eval_and_update({M0, Bs0, Stk0}, {3, E}); false -> case is_reducible(F0, Bs0) of true -> - eval_and_update({Bs0, F0, Stk0}, {4, E}); + eval_and_update({F0, Bs0, Stk0}, {4, E}); false -> case is_reducible(As, Bs0) of true -> - eval_and_update({Bs0, As, Stk0}, {5, E}); + eval_and_update({As, Bs0, Stk0}, {5, E}); false -> M = concrete(M0), F = concrete(F0), @@ -364,18 +364,18 @@ expr(Bs0, E = {apply, Line, M0, F0, As}, Stk0) -> end end end; -expr(Bs0, E = {apply_fun, Line, Fun, As}, Stk0) -> +expr(E = {apply_fun, Line, Fun, As}, Bs0, Stk0) -> case is_reducible(Fun, Bs0) of true -> - eval_and_update({Bs0, Fun, Stk0}, {3, E}); + eval_and_update({Fun, Bs0, Stk0}, {3, E}); false -> case is_reducible(As, Bs0) of true -> - eval_and_update({Bs0, As, Stk0}, {4, E}); + eval_and_update({As, Bs0, Stk0}, {4, E}); false -> A = length(As), {env, [{{M, F}, Bs1, Cs}]} = erlang:fun_info(concrete(Fun), env), - {match, Bs2, Body} = match_fun(Cs, As), + {match, Body, Bs2} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Bs = cauder_bindings:merge(Bs1, Bs2), Entry = #s_function{mfa = {M, F, A}, env = Bs, expr = Body, var = Var}, @@ -383,33 +383,33 @@ expr(Bs0, E = {apply_fun, Line, Fun, As}, Stk0) -> #result{env = Bs0, expr = [Var], stack = Stk} end end; -expr(Bs0, E = {match, _, Lhs, Rhs}, Stk) -> +expr(E = {match, _, Lhs, Rhs}, Bs0, Stk) -> case is_reducible(Lhs, Bs0) of true -> - eval_and_update({Bs0, Lhs, Stk}, {3, E}); + eval_and_update({Lhs, Bs0, Stk}, {3, E}); false -> case is_reducible(Rhs, Bs0) of true -> - eval_and_update({Bs0, Rhs, Stk}, {4, E}); + eval_and_update({Rhs, Bs0, Stk}, {4, E}); false -> - case match(Bs0, [Lhs], [Rhs]) of + case match([Lhs], [Rhs], Bs0) of {match, Bs} -> #result{env = Bs, expr = [Rhs], stack = Stk}; nomatch -> error({badmatch, concrete(Rhs)}) end end end; -expr(Bs, E = {op, Line, Op, As}, Stk) -> +expr(E = {op, Line, Op, As}, Bs, Stk) -> case is_reducible(As, Bs) of true -> - eval_and_update({Bs, As, Stk}, {4, E}); + eval_and_update({As, Bs, Stk}, {4, E}); false -> Value = apply(erlang, Op, lists:map(fun concrete/1, As)), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end; -expr(Bs, E = {'andalso', Line, Lhs, Rhs}, Stk) -> +expr(E = {'andalso', Line, Lhs, Rhs}, Bs, Stk) -> case is_reducible(Lhs, Bs) of true -> - eval_and_update({Bs, Lhs, Stk}, {3, E}); + eval_and_update({Lhs, Bs, Stk}, {3, E}); false -> case Lhs of {value, _, false} -> @@ -417,17 +417,17 @@ expr(Bs, E = {'andalso', Line, Lhs, Rhs}, Stk) -> {value, _, true} -> case is_reducible(Rhs, Bs) of true -> - eval_and_update({Bs, Rhs, Stk}, {4, E}); + eval_and_update({Rhs, Bs, Stk}, {4, E}); false -> Value = apply(erlang, 'and', [concrete(Lhs), concrete(Rhs)]), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end end end; -expr(Bs, E = {'orelse', Line, Lhs, Rhs}, Stk) -> +expr(E = {'orelse', Line, Lhs, Rhs}, Bs, Stk) -> case is_reducible(Lhs, Bs) of true -> - eval_and_update({Bs, Lhs, Stk}, {3, E}); + eval_and_update({Lhs, Bs, Stk}, {3, E}); false -> case Lhs of {value, _, true} -> @@ -435,7 +435,7 @@ expr(Bs, E = {'orelse', Line, Lhs, Rhs}, Stk) -> {value, _, false} -> case is_reducible(Rhs, Bs) of true -> - eval_and_update({Bs, Rhs, Stk}, {4, E}); + eval_and_update({Rhs, Bs, Stk}, {4, E}); false -> Value = apply(erlang, 'or', [concrete(Lhs), concrete(Rhs)]), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} @@ -452,19 +452,19 @@ expr(Bs, E = {'orelse', Line, Lhs, Rhs}, Stk) -> %% %% @see is_reducible/2 --spec expr_list(Bindings, Expressions, Stack) -> Result when - Bindings :: cauder_bindings:bindings(), +-spec expr_list(Expressions, Bindings, Stack) -> Result when Expressions :: [cauder_syntax:abstract_expr()], + Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). -expr_list(Bs, [E | Es], Stk) -> +expr_list([E | Es], Bs, Stk) -> case is_reducible(E, Bs) of true -> - R = #result{expr = Es1} = expr(Bs, E, Stk), + R = #result{expr = Es1} = expr(E, Bs, Stk), R#result{expr = Es1 ++ Es}; false -> - R = #result{expr = Es1} = expr_list(Bs, Es, Stk), + R = #result{expr = Es1} = expr_list(Es, Bs, Stk), R#result{expr = [E | Es1]} end. @@ -478,7 +478,7 @@ remote_call(M, F, As, Stk0, Line, Bs0) -> {ok, _} -> true = Exported; error when Stk0 =:= [] -> ok end, - {match, Bs, Body} = match_fun(Cs, As), + {match, Body, Bs} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Entry = #s_function{mfa = {M, F, A}, env = Bs, expr = Body, var = Var}, Stk = cauder_stack:push(Entry, Stk0), @@ -490,52 +490,52 @@ remote_call(M, F, As, Stk0, Line, Bs0) -> %%%============================================================================= --spec match_if(Bindings, Clauses) -> {match, Body} | nomatch when - Bindings :: cauder_bindings:bindings(), +-spec match_if(Clauses, Bindings) -> {match, Body} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), + Bindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(). -match_if(_, []) -> +match_if([], _) -> nomatch; -match_if(Bs, [{'clause', _, [], G, B} | Cs]) -> - case concrete(guard_seq(Bs, G)) of +match_if([{'clause', _, [], G, B} | Cs], Bs) -> + case concrete(guard_seq(G, Bs)) of true -> {match, B}; - false -> match_if(Bs, Cs) + false -> match_if(Cs, Bs) end. --spec match_case(Bindings, Clauses, Argument) -> {match, ScopeBindings, Body} | nomatch when - Bindings :: cauder_bindings:bindings(), +-spec match_case(Clauses, Argument, Bindings) -> {match, Body, ScopeBindings} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), Argument :: cauder_syntax:af_literal(), - ScopeBindings :: cauder_bindings:bindings(), - Body :: cauder_syntax:af_body(). + Bindings :: cauder_bindings:bindings(), + Body :: cauder_syntax:af_body(), + ScopeBindings :: cauder_bindings:bindings(). -match_case(Bs, Cs, V) -> match_clause(Bs, Cs, [V]). +match_case(Cs, V, Bs) -> match_clause(Cs, [V], Bs). --spec match_fun(Clauses, Arguments) -> {match, ScopeBindings, Body} | nomatch when +-spec match_fun(Clauses, Arguments) -> {match, Body, ScopeBindings} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), Arguments :: [cauder_syntax:af_literal()], - ScopeBindings :: cauder_bindings:bindings(), - Body :: cauder_syntax:af_body(). + Body :: cauder_syntax:af_body(), + ScopeBindings :: cauder_bindings:bindings(). -match_fun(Cs, Vs) -> match_clause(cauder_bindings:new(), Cs, Vs). +match_fun(Cs, Vs) -> match_clause(Cs, Vs, cauder_bindings:new()). --spec match_receive_pid(Clauses, Bindings, RecipientPid, Mail, Sched, Sys) -> - {NewBindings, Body, {Message, QueuePosition}, NewMail} | nomatch +-spec match_receive_pid(Clauses, RecipientPid, Mail, Bindings, Sched, Sys) -> + {Body, {Message, QueuePosition}, NewMail, NewBindings} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), - Bindings :: cauder_bindings:bindings(), RecipientPid :: cauder_process:id(), Mail :: cauder_mailbox:mailbox(), + Bindings :: cauder_bindings:bindings(), Sched :: cauder_message:scheduler(), Sys :: cauder_system:system(), - NewBindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(), Message :: cauder_message:message(), QueuePosition :: pos_integer(), - NewMail :: cauder_mailbox:mailbox(). + NewMail :: cauder_mailbox:mailbox(), + NewBindings :: cauder_bindings:bindings(). -match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> +match_receive_pid(Cs, Pid, Mail, Bs, Sched, Sys) -> case cauder_mailbox:find_destination(Pid, Mail) of [] -> nomatch; @@ -544,8 +544,8 @@ match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> ?SCHEDULER_Manual -> FoldQueue = fun(Msg, Map1) -> - case match_receive(Cs, Bs, #message{uid = Uid} = Msg) of - {match, Bs1, Body} -> maps:put(Uid, {Bs1, Body, Msg}, Map1); + case match_receive(Cs, #message{uid = Uid} = Msg, Bs) of + {match, Body, Bs1} -> maps:put(Uid, {Bs1, Body, Msg}, Map1); nomatch -> skip end end, @@ -562,7 +562,7 @@ match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> cauder:resume_task(), {Bs1, Body, Msg} = maps:get(Uid, MatchingBranchesMap), {QPos, NewMail} = cauder_mailbox:remove(Msg, Mail), - {Bs1, Body, {Msg, QPos}, NewMail}; + {Body, {Msg, QPos}, NewMail, Bs1}; % TODO Use suspend time {_SuspendTime, cancel} -> throw(cancel) @@ -572,8 +572,8 @@ match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> MatchingBranches = lists:filtermap( fun(Queue) -> {value, Msg} = queue:peek(Queue), - case match_receive(Cs, Bs, Msg) of - {match, Bs1, Body} -> {true, {Bs1, Body, Msg}}; + case match_receive(Cs, Msg, Bs) of + {match, Body, Bs1} -> {true, {Bs1, Body, Msg}}; nomatch -> false end end, @@ -585,97 +585,97 @@ match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys) -> Length -> {Bs1, Body, Msg} = lists:nth(rand:uniform(Length), MatchingBranches), {QPos, NewMail} = cauder_mailbox:remove(Msg, Mail), - {Bs1, Body, {Msg, QPos}, NewMail} + {Body, {Msg, QPos}, NewMail, Bs1} end end end. --spec match_receive(Clauses, Bindings, Message) -> {match, NewBindings, Body} | nomatch when +-spec match_receive(Clauses, Message, Bindings) -> {match, Body, NewBindings} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), - Bindings :: cauder_bindings:bindings(), Message :: cauder_message:message(), - NewBindings :: cauder_bindings:bindings(), - Body :: cauder_syntax:af_body(). + Bindings :: cauder_bindings:bindings(), + Body :: cauder_syntax:af_body(), + NewBindings :: cauder_bindings:bindings(). -match_receive(Cs, Bs0, #message{val = Value}) -> match_clause(Bs0, Cs, [abstract(Value)]). +match_receive(Cs, #message{val = Value}, Bs0) -> match_clause(Cs, [abstract(Value)], Bs0). --spec match_receive_uid(Clauses, Bindings, Uid, Mail) -> - {NewBindings, Body, {Message, QueuePosition}, NewMail} | nomatch +-spec match_receive_uid(Clauses, Uid, Mail, Bindings) -> + {Body, {Message, QueuePosition}, NewMail, NewBindings} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), - Bindings :: cauder_bindings:bindings(), Uid :: cauder_message:uid(), Mail :: cauder_mailbox:mailbox(), - NewBindings :: cauder_bindings:bindings(), + Bindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(), Message :: cauder_message:message(), QueuePosition :: pos_integer(), - NewMail :: cauder_mailbox:mailbox(). + NewMail :: cauder_mailbox:mailbox(), + NewBindings :: cauder_bindings:bindings(). -match_receive_uid(Cs, Bs0, Uid, Mail0) -> +match_receive_uid(Cs, Uid, Mail0, Bs0) -> case cauder_mailbox:take(Uid, Mail0) of error -> nomatch; {{Msg, QPos}, Mail1} -> - case match_clause(Bs0, Cs, [abstract(Msg#message.val)]) of - {match, Bs, Body} -> {Bs, Body, {Msg, QPos}, Mail1}; + case match_clause(Cs, [abstract(Msg#message.val)], Bs0) of + {match, Body, Bs} -> {Body, {Msg, QPos}, Mail1, Bs}; nomatch -> nomatch end end. --spec match_clause(Bindings, Clauses, Arguments) -> {match, ScopeBindings, Body} | nomatch when - Bindings :: cauder_bindings:bindings(), +-spec match_clause(Clauses, Arguments, Bindings) -> {match, Body, ScopeBindings} | nomatch when Clauses :: cauder_syntax:af_clause_seq(), Arguments :: [cauder_syntax:af_literal()], - ScopeBindings :: cauder_bindings:bindings(), - Body :: cauder_syntax:af_body(). + Bindings :: cauder_bindings:bindings(), + Body :: cauder_syntax:af_body(), + ScopeBindings :: cauder_bindings:bindings(). -match_clause(_, [], _) -> +match_clause([], _, _) -> nomatch; -match_clause(Bs0, [{'clause', _, Ps, G, B} | Cs], Vs) -> - case match(Bs0, Ps, Vs) of +match_clause([{'clause', _, Ps, G, B} | Cs], Vs, Bs0) -> + case match(Ps, Vs, Bs0) of {match, Bs} -> - case concrete(guard_seq(Bs, G)) of - true -> {match, Bs, B}; - false -> match_clause(Bs0, Cs, Vs) + case concrete(guard_seq(G, Bs)) of + true -> {match, B, Bs}; + false -> match_clause(Cs, Vs, Bs0) end; nomatch -> - match_clause(Bs0, Cs, Vs) + match_clause(Cs, Vs, Bs0) end. --spec clause_line(Bindings, Clauses, Arguments) -> Line when - Bindings :: cauder_bindings:bindings(), +-spec clause_line(Clauses, Arguments, Bindings) -> Line when Clauses :: cauder_syntax:af_clause_seq(), Arguments :: [cauder_syntax:af_literal()], + Bindings :: cauder_bindings:bindings(), Line :: non_neg_integer(). -clause_line(_, [], _) -> +clause_line([], _, _) -> -1; -clause_line(Bs0, [{'clause', Line, Ps, G, _} | Cs], Vs) -> - case match(Bs0, Ps, Vs) of +clause_line([{'clause', Line, Ps, G, _} | Cs], Vs, Bs0) -> + case match(Ps, Vs, Bs0) of {match, Bs} -> - case concrete(guard_seq(Bs, G)) of + case concrete(guard_seq(G, Bs)) of true -> Line; - false -> clause_line(Bs0, Cs, Vs) + false -> clause_line(Cs, Vs, Bs0) end; nomatch -> - clause_line(Bs0, Cs, Vs) + clause_line(Cs, Vs, Bs0) end. %% Tries to match a list of values against a list of patterns using the given environment. %% The list of values should have no variables. --spec match(Bindings, Patterns, Arguments) -> {match, NewBindings} | nomatch when - Bindings :: cauder_bindings:bindings(), +-spec match(Patterns, Arguments, Bindings) -> {match, NewBindings} | nomatch when Patterns :: [cauder_syntax:af_pattern()], Arguments :: [cauder_syntax:af_literal()], + Bindings :: cauder_bindings:bindings(), NewBindings :: cauder_bindings:bindings(). -match(Bs, [], []) -> +match([], [], Bs) -> {match, Bs}; -match(Bs0, [Pat | Ps0], [{value, _, Val} | Vs0]) when length(Ps0) == length(Vs0) -> +match([Pat | Ps0], [{value, _, Val} | Vs0], Bs0) when length(Ps0) == length(Vs0) -> case catch match1(Pat, Val, Bs0) of - {match, Bs} -> match(Bs, Ps0, Vs0); + {match, Bs} -> match(Ps0, Vs0, Bs); nomatch -> nomatch end; match(_Bs, _Ps, _Vs) -> @@ -728,36 +728,36 @@ match_tuple([E | Es], Tuple, I, Bs0) -> %%%============================================================================= --spec guard_seq(Bindings, Guards) -> Boolean when - Bindings :: cauder_bindings:bindings(), +-spec guard_seq(Guards, Bindings) -> Boolean when Guards :: cauder_syntax:af_guard_seq(), + Bindings :: cauder_bindings:bindings(), Boolean :: cauder_syntax:af_boolean(). -guard_seq(_, []) -> +guard_seq([], _) -> abstract(true); -guard_seq(Bs, Gs) when is_list(Gs) -> +guard_seq(Gs, Bs) when is_list(Gs) -> % In a guard sequence, guards are evaluated until one is true. The remaining guards, if any, are not evaluated. % See: https://erlang.org/doc/reference_manual/expressions.html#guard-sequences - abstract(lists:any(fun(G) -> concrete(guard(Bs, G)) end, Gs)). + abstract(lists:any(fun(G) -> concrete(guard(G, Bs)) end, Gs)). --spec guard(Bindings, Guard) -> Boolean when - Bindings :: cauder_bindings:bindings(), +-spec guard(Guard, Bindings) -> Boolean when Guard :: cauder_syntax:af_guard(), + Bindings :: cauder_bindings:bindings(), Boolean :: cauder_syntax:af_boolean(). -guard(Bs, G) when is_list(G) -> - abstract(lists:all(fun(Gt) -> concrete(guard_test(Bs, Gt)) end, G)). +guard(G, Bs) when is_list(G) -> + abstract(lists:all(fun(Gt) -> concrete(guard_test(Gt, Bs)) end, G)). --spec guard_test(Bindings, GuardTest) -> GuardTest | Boolean when - Bindings :: cauder_bindings:bindings(), +-spec guard_test(GuardTest, Bindings) -> GuardTest | Boolean when GuardTest :: cauder_syntax:af_guard_test(), + Bindings :: cauder_bindings:bindings(), Boolean :: cauder_syntax:af_boolean(). -guard_test(Bs, Gt) -> +guard_test(Gt, Bs) -> case is_reducible(Gt, Bs) of true -> - #result{expr = [Gt1]} = expr(Bs, Gt, cauder_stack:new()), - guard_test(Bs, Gt1); + #result{expr = [Gt1]} = expr(Gt, Bs, cauder_stack:new()), + guard_test(Gt1, Bs); false -> Gt end. @@ -824,17 +824,17 @@ is_value({cons, _, H, T}) -> is_value(H) andalso is_value(T); is_value({tuple, _, Es}) -> is_value(Es); is_value(E) when is_tuple(E) -> false. --spec eval_and_update({Bindings, Expression | [Expression], Stack}, {Index, Tuple}) -> Result when - Bindings :: cauder_bindings:bindings(), +-spec eval_and_update({Expression | [Expression], Bindings, Stack}, {Index, Tuple}) -> Result when Expression :: cauder_syntax:abstract_expr(), + Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Index :: pos_integer(), Tuple :: tuple(), Result :: cauder_eval:result(). -eval_and_update({Bs, Es, Stk}, {Index, Tuple}) when is_list(Es) -> - R = #result{expr = Es1} = expr_list(Bs, Es, Stk), +eval_and_update({Es, Bs, Stk}, {Index, Tuple}) when is_list(Es) -> + R = #result{expr = Es1} = expr_list(Es, Bs, Stk), R#result{expr = [setelement(Index, Tuple, Es1)]}; -eval_and_update({Bs, E, Stk}, {Index, Tuple}) -> - R = #result{expr = [E1]} = expr(Bs, E, Stk), +eval_and_update({E, Bs, Stk}, {Index, Tuple}) -> + R = #result{expr = [E1]} = expr(E, Bs, Stk), R#result{expr = [setelement(Index, Tuple, E1)]}. diff --git a/src/cauder_semantics_forwards.erl b/src/cauder_semantics_forwards.erl index a16af94..e26720b 100644 --- a/src/cauder_semantics_forwards.erl +++ b/src/cauder_semantics_forwards.erl @@ -39,7 +39,7 @@ step(Pid, Sys, Sched, Mode) -> #process{stack = Stk0, env = Bs0, expr = Es0} = cauder_pool:get(Pid, Sys#system.pool), - Result = cauder_eval:exprs(Bs0, Es0, Stk0), + Result = cauder_eval:exprs(Es0, Bs0, Stk0), case Result#result.label of #label_tau{} -> rule_local(Pid, Result, Sys); @@ -439,11 +439,11 @@ rule_receive( Sched, #system{mail = Mail, pool = Pool, log = Log0} = Sys ) -> - {{Bs1, Es1, {Msg, QPos}, Mail1}, Log1} = + {{Es1, {Msg, QPos}, Mail1, Bs1}, Log1} = case Mode of normal -> - Match = cauder_eval:match_receive_pid(Cs, Bs, Pid, Mail, Sched, Sys), - {_, _, {#message{uid = Uid}, _}, _} = Match, + Match = cauder_eval:match_receive_pid(Cs, Pid, Mail, Bs, Sched, Sys), + {_, {#message{uid = Uid}, _}, _, _} = Match, %% If the chosen message is the same specified in the log don't invalidate the log Log = case cauder_log:pop_receive(Pid, Log0) of @@ -453,7 +453,7 @@ rule_receive( {Match, Log}; replay -> {#log_receive{uid = Uid}, Log} = cauder_log:pop_receive(Pid, Log0), - Match = cauder_eval:match_receive_uid(Cs, Bs, Uid, Mail), + Match = cauder_eval:match_receive_uid(Cs, Uid, Mail, Bs), {Match, Log} end, @@ -601,10 +601,10 @@ check_reducibility(Cs, Pid, #system{mail = Mail, log = Log} = Sys, Mode, 'receiv IsMatch = case Mode of normal -> - cauder_eval:match_receive_pid(Cs, Bs, Pid, Mail, ?SCHEDULER_Random, Sys) =/= nomatch; + cauder_eval:match_receive_pid(Cs, Pid, Mail, Bs, ?SCHEDULER_Random, Sys) =/= nomatch; replay -> {value, #log_receive{uid = Uid}} = cauder_log:peek(Pid, Log), - cauder_eval:match_receive_uid(Cs, Bs, Uid, Mail) =/= nomatch + cauder_eval:match_receive_uid(Cs, Uid, Mail, Bs) =/= nomatch end, case IsMatch of true -> diff --git a/src/cauder_syntax.erl b/src/cauder_syntax.erl index b2f8c21..8591dc9 100644 --- a/src/cauder_syntax.erl +++ b/src/cauder_syntax.erl @@ -846,5 +846,5 @@ set_line(Node, Line) -> erl_syntax:set_pos(Node, erl_anno:new(Line)). remote_call(M, F, As) -> A = length(As), {_, Cs} = cauder_utils:fundef_lookup({M, F, A}), - Line = cauder_eval:clause_line(cauder_bindings:new(), Cs, As), + Line = cauder_eval:clause_line(Cs, As, cauder_bindings:new()), {remote_call, Line, M, F, lists:map(fun(V) -> setelement(2, V, Line) end, As)}. From 2233bb31bcb498ba2485f07cb3d4ff6da6f64ed1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Thu, 13 Jan 2022 11:05:53 +0100 Subject: [PATCH 4/8] Simplify `eval_and_update` function by removing redundant argument --- src/cauder_eval.erl | 82 +++++++++++++++++++++++---------------------- 1 file changed, 42 insertions(+), 40 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index bca0c99..69a0044 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -153,7 +153,7 @@ expr({'if', Line, Cs}, Bs, Stk0) -> expr(E = {'case', Line, A, Cs}, Bs0, Stk0) -> case is_reducible(A, Bs0) of true -> - eval_and_update({A, Bs0, Stk0}, {3, E}); + eval_and_update(3, E, Bs0, Stk0); false -> case match_case(Cs, A, Bs0) of {match, Body, Bs} -> @@ -195,7 +195,7 @@ expr({'make_fun', Line, Name, Cs}, Bs, Stk0) -> expr(E = {bif, Line, M, F, As}, Bs, Stk) -> case is_reducible(As, Bs) of true -> - eval_and_update({As, Bs, Stk}, {5, E}); + eval_and_update(5, E, Bs, Stk); false -> Value = apply(M, F, lists:map(fun concrete/1, As)), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} @@ -215,7 +215,7 @@ expr({nodes, Line}, Bs, Stk) -> expr(E = {spawn, Line, Fun}, Bs, Stk) -> case is_reducible(Fun, Bs) of true -> - eval_and_update({Fun, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_fun{var = Var, function = Fun}, @@ -224,11 +224,11 @@ expr(E = {spawn, Line, Fun}, Bs, Stk) -> expr(E = {spawn, Line, N, Fun}, Bs, Stk) -> case is_reducible(N, Bs) of true -> - eval_and_update({N, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case is_reducible(Fun, Bs) of true -> - eval_and_update({Fun, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_fun{var = Var, node = concrete(N), function = Fun}, @@ -238,15 +238,15 @@ expr(E = {spawn, Line, N, Fun}, Bs, Stk) -> expr(E = {spawn, Line, M, F, As}, Bs, Stk) -> case is_reducible(M, Bs) of true -> - eval_and_update({M, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case is_reducible(F, Bs) of true -> - eval_and_update({F, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> case is_reducible(As, Bs) of true -> - eval_and_update({As, Bs, Stk}, {5, E}); + eval_and_update(5, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_mfa{ @@ -262,19 +262,19 @@ expr(E = {spawn, Line, M, F, As}, Bs, Stk) -> expr(E = {spawn, Line, N, M, F, As}, Bs, Stk) -> case is_reducible(N, Bs) of true -> - eval_and_update({N, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case is_reducible(M, Bs) of true -> - eval_and_update({M, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> case is_reducible(F, Bs) of true -> - eval_and_update({F, Bs, Stk}, {5, E}); + eval_and_update(5, E, Bs, Stk); false -> case is_reducible(As, Bs) of true -> - eval_and_update({As, Bs, Stk}, {6, E}); + eval_and_update(6, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_mfa{ @@ -292,7 +292,7 @@ expr(E = {spawn, Line, N, M, F, As}, Bs, Stk) -> expr(E = {start, Line, N}, Bs, Stk) -> case is_reducible(N, Bs) of true -> - eval_and_update({N, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), Label = #label_start{var = Var, name = concrete(N)}, @@ -301,11 +301,11 @@ expr(E = {start, Line, N}, Bs, Stk) -> expr(E = {start, Line, H, N}, Bs, Stk) -> case is_reducible(H, Bs) of true -> - eval_and_update({H, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case is_reducible(N, Bs) of true -> - eval_and_update({N, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), Label = #label_start{var = Var, name = concrete(N), host = concrete(H)}, @@ -315,11 +315,11 @@ expr(E = {start, Line, H, N}, Bs, Stk) -> expr(E = {Send, _, L, R}, Bs, Stk) when Send =:= 'send' orelse Send =:= 'send_op' -> case is_reducible(L, Bs) of true -> - eval_and_update({L, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case is_reducible(R, Bs) of true -> - eval_and_update({R, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> Label = #label_send{dst = concrete(L), val = concrete(R)}, #result{env = Bs, expr = [R], stack = Stk, label = Label} @@ -328,7 +328,7 @@ expr(E = {Send, _, L, R}, Bs, Stk) when Send =:= 'send' orelse Send =:= 'send_op expr(E = {local_call, Line, F, As}, Bs0, Stk0) -> case is_reducible(As, Bs0) of true -> - eval_and_update({As, Bs0, Stk0}, {4, E}); + eval_and_update(4, E, Bs0, Stk0); false -> {ok, M} = cauder_stack:current_module(Stk0), A = length(As), @@ -341,22 +341,22 @@ expr(E = {local_call, Line, F, As}, Bs0, Stk0) -> end; expr(E = {remote_call, Line, M, F, As}, Bs0, Stk0) -> case is_reducible(As, Bs0) of - true -> eval_and_update({As, Bs0, Stk0}, {5, E}); + true -> eval_and_update(5, E, Bs0, Stk0); false -> remote_call(M, F, As, Stk0, Line, Bs0) end; % TODO Handle calls to self/0, spawn/1, spawn/3 expr(E = {apply, Line, M0, F0, As}, Bs0, Stk0) -> case is_reducible(M0, Bs0) of true -> - eval_and_update({M0, Bs0, Stk0}, {3, E}); + eval_and_update(3, E, Bs0, Stk0); false -> case is_reducible(F0, Bs0) of true -> - eval_and_update({F0, Bs0, Stk0}, {4, E}); + eval_and_update(4, E, Bs0, Stk0); false -> case is_reducible(As, Bs0) of true -> - eval_and_update({As, Bs0, Stk0}, {5, E}); + eval_and_update(5, E, Bs0, Stk0); false -> M = concrete(M0), F = concrete(F0), @@ -367,11 +367,11 @@ expr(E = {apply, Line, M0, F0, As}, Bs0, Stk0) -> expr(E = {apply_fun, Line, Fun, As}, Bs0, Stk0) -> case is_reducible(Fun, Bs0) of true -> - eval_and_update({Fun, Bs0, Stk0}, {3, E}); + eval_and_update(3, E, Bs0, Stk0); false -> case is_reducible(As, Bs0) of true -> - eval_and_update({As, Bs0, Stk0}, {4, E}); + eval_and_update(4, E, Bs0, Stk0); false -> A = length(As), {env, [{{M, F}, Bs1, Cs}]} = erlang:fun_info(concrete(Fun), env), @@ -386,11 +386,11 @@ expr(E = {apply_fun, Line, Fun, As}, Bs0, Stk0) -> expr(E = {match, _, Lhs, Rhs}, Bs0, Stk) -> case is_reducible(Lhs, Bs0) of true -> - eval_and_update({Lhs, Bs0, Stk}, {3, E}); + eval_and_update(3, E, Bs0, Stk); false -> case is_reducible(Rhs, Bs0) of true -> - eval_and_update({Rhs, Bs0, Stk}, {4, E}); + eval_and_update(4, E, Bs0, Stk); false -> case match([Lhs], [Rhs], Bs0) of {match, Bs} -> #result{env = Bs, expr = [Rhs], stack = Stk}; @@ -401,7 +401,7 @@ expr(E = {match, _, Lhs, Rhs}, Bs0, Stk) -> expr(E = {op, Line, Op, As}, Bs, Stk) -> case is_reducible(As, Bs) of true -> - eval_and_update({As, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> Value = apply(erlang, Op, lists:map(fun concrete/1, As)), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} @@ -409,7 +409,7 @@ expr(E = {op, Line, Op, As}, Bs, Stk) -> expr(E = {'andalso', Line, Lhs, Rhs}, Bs, Stk) -> case is_reducible(Lhs, Bs) of true -> - eval_and_update({Lhs, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case Lhs of {value, _, false} -> @@ -417,7 +417,7 @@ expr(E = {'andalso', Line, Lhs, Rhs}, Bs, Stk) -> {value, _, true} -> case is_reducible(Rhs, Bs) of true -> - eval_and_update({Rhs, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> Value = apply(erlang, 'and', [concrete(Lhs), concrete(Rhs)]), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} @@ -427,7 +427,7 @@ expr(E = {'andalso', Line, Lhs, Rhs}, Bs, Stk) -> expr(E = {'orelse', Line, Lhs, Rhs}, Bs, Stk) -> case is_reducible(Lhs, Bs) of true -> - eval_and_update({Lhs, Bs, Stk}, {3, E}); + eval_and_update(3, E, Bs, Stk); false -> case Lhs of {value, _, true} -> @@ -435,7 +435,7 @@ expr(E = {'orelse', Line, Lhs, Rhs}, Bs, Stk) -> {value, _, false} -> case is_reducible(Rhs, Bs) of true -> - eval_and_update({Rhs, Bs, Stk}, {4, E}); + eval_and_update(4, E, Bs, Stk); false -> Value = apply(erlang, 'or', [concrete(Lhs), concrete(Rhs)]), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} @@ -824,17 +824,19 @@ is_value({cons, _, H, T}) -> is_value(H) andalso is_value(T); is_value({tuple, _, Es}) -> is_value(Es); is_value(E) when is_tuple(E) -> false. --spec eval_and_update({Expression | [Expression], Bindings, Stack}, {Index, Tuple}) -> Result when +-spec eval_and_update(Index, Expression, Bindings, Stack) -> Result when + Index :: pos_integer(), Expression :: cauder_syntax:abstract_expr(), Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), - Index :: pos_integer(), - Tuple :: tuple(), Result :: cauder_eval:result(). -eval_and_update({Es, Bs, Stk}, {Index, Tuple}) when is_list(Es) -> - R = #result{expr = Es1} = expr_list(Es, Bs, Stk), - R#result{expr = [setelement(Index, Tuple, Es1)]}; -eval_and_update({E, Bs, Stk}, {Index, Tuple}) -> - R = #result{expr = [E1]} = expr(E, Bs, Stk), - R#result{expr = [setelement(Index, Tuple, E1)]}. +eval_and_update(N, Expr, Bs, Stk) -> + case element(N, Expr) of + Es when is_list(Es) -> + R = #result{expr = Es1} = expr_list(Es, Bs, Stk), + R#result{expr = [setelement(N, Expr, Es1)]}; + E -> + R = #result{expr = [E1]} = expr(E, Bs, Stk), + R#result{expr = [setelement(N, Expr, E1)]} + end. From 93e5ce38ecdbf1618fc81b950cfe06e3824c3771 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Sat, 15 Jan 2022 11:42:16 +0100 Subject: [PATCH 5/8] Refactor and rename some functions to match those from `erl_eval` --- src/cauder_eval.erl | 293 ++++++++++++++++++++++++-------------------- 1 file changed, 160 insertions(+), 133 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 69a0044..6744407 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -1,7 +1,8 @@ -module(cauder_eval). %% API --export([exprs/3, abstract/1, concrete/1, is_value/1, is_reducible/2]). +-export([exprs/3]). +-export([abstract/1, concrete/1, is_value/1, is_reducible/2]). -export([match_receive_pid/6, match_receive_uid/4]). -export([clause_line/3]). @@ -34,6 +35,11 @@ -type label_send() :: #label_send{}. -type label_receive() :: #label_receive{}. +-type expression() :: cauder_syntax:abstract_expr(). +-type expressions() :: [cauder_syntax:abstract_expr()]. +-type expression_list() :: [expression()]. +-type clauses() :: [cauder_syntax:af_clause()]. + %%%============================================================================= %%% API %%%============================================================================= @@ -52,7 +58,7 @@ %% @see is_reducible/2 -spec exprs(Expressions, Bindings, Stack) -> Result when - Expressions :: [cauder_syntax:abstract_expr()], + Expressions :: expressions(), Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). @@ -103,7 +109,7 @@ exprs([E | Es], Bs, Stk) -> %% environment, the expression that resulted from the evaluation, and a label. -spec expr(Expression, Bindings, Stack) -> Result when - Expression :: cauder_syntax:abstract_expr(), + Expression :: expression(), Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). @@ -141,29 +147,21 @@ expr(E = {tuple, Line, Es0}, Bs, Stk) -> R#result{expr = [setelement(3, E, Es)]} end; expr({'if', Line, Cs}, Bs, Stk0) -> - case match_if(Cs, Bs) of - {match, Body} -> - Var = cauder_utils:temp_variable(Line), - Entry = #s_block{type = 'if', expr = Body, var = Var}, - Stk = cauder_stack:push(Entry, Stk0), - #result{env = Bs, expr = [Var], stack = Stk}; - nomatch -> - error(if_clause) - end; + Body = if_clauses(Cs, Bs), + Var = cauder_utils:temp_variable(Line), + Entry = #s_block{type = 'if', expr = Body, var = Var}, + Stk = cauder_stack:push(Entry, Stk0), + #result{env = Bs, expr = [Var], stack = Stk}; expr(E = {'case', Line, A, Cs}, Bs0, Stk0) -> case is_reducible(A, Bs0) of true -> eval_and_update(3, E, Bs0, Stk0); false -> - case match_case(Cs, A, Bs0) of - {match, Body, Bs} -> - Var = cauder_utils:temp_variable(Line), - Entry = #s_block{type = 'case', expr = Body, var = Var}, - Stk = cauder_stack:push(Entry, Stk0), - #result{env = Bs, expr = [Var], stack = Stk}; - nomatch -> - error({case_clause, concrete(A)}) - end + {Body, Bs} = case_clauses(Cs, A, Bs0), + Var = cauder_utils:temp_variable(Line), + Entry = #s_block{type = 'case', expr = Body, var = Var}, + Stk = cauder_stack:push(Entry, Stk0), + #result{env = Bs, expr = [Var], stack = Stk} end; %% TODO Support receive with timeout expr({'receive', Line, Cs}, Bs, Stk0) -> @@ -333,7 +331,7 @@ expr(E = {local_call, Line, F, As}, Bs0, Stk0) -> {ok, M} = cauder_stack:current_module(Stk0), A = length(As), {_, Cs} = cauder_utils:fundef_lookup({M, F, A}), - {match, Body, Bs} = match_fun(Cs, As), + {Body, Bs} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Entry = #s_function{mfa = {M, F, A}, env = Bs, expr = Body, var = Var}, Stk = cauder_stack:push(Entry, Stk0), @@ -375,7 +373,7 @@ expr(E = {apply_fun, Line, Fun, As}, Bs0, Stk0) -> false -> A = length(As), {env, [{{M, F}, Bs1, Cs}]} = erlang:fun_info(concrete(Fun), env), - {match, Body, Bs2} = match_fun(Cs, As), + {Body, Bs2} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Bs = cauder_bindings:merge(Bs1, Bs2), Entry = #s_function{mfa = {M, F, A}, env = Bs, expr = Body, var = Var}, @@ -392,9 +390,10 @@ expr(E = {match, _, Lhs, Rhs}, Bs0, Stk) -> true -> eval_and_update(4, E, Bs0, Stk); false -> - case match([Lhs], [Rhs], Bs0) of + Val = concrete(Rhs), + case match(Lhs, Val, Bs0) of {match, Bs} -> #result{env = Bs, expr = [Rhs], stack = Stk}; - nomatch -> error({badmatch, concrete(Rhs)}) + nomatch -> error({badmatch, Val}) end end end; @@ -452,8 +451,8 @@ expr(E = {'orelse', Line, Lhs, Rhs}, Bs, Stk) -> %% %% @see is_reducible/2 --spec expr_list(Expressions, Bindings, Stack) -> Result when - Expressions :: [cauder_syntax:abstract_expr()], +-spec expr_list(ExpressionList, Bindings, Stack) -> Result when + ExpressionList :: expression_list(), Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). @@ -478,7 +477,7 @@ remote_call(M, F, As, Stk0, Line, Bs0) -> {ok, _} -> true = Exported; error when Stk0 =:= [] -> ok end, - {match, Body, Bs} = match_fun(Cs, As), + {Body, Bs} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Entry = #s_function{mfa = {M, F, A}, env = Bs, expr = Body, var = Var}, Stk = cauder_stack:push(Entry, Stk0), @@ -490,40 +489,59 @@ remote_call(M, F, As, Stk0, Line, Bs0) -> %%%============================================================================= --spec match_if(Clauses, Bindings) -> {match, Body} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), +-spec if_clauses(Clauses, Bindings) -> Body when + Clauses :: clauses(), Bindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(). -match_if([], _) -> - nomatch; -match_if([{'clause', _, [], G, B} | Cs], Bs) -> - case concrete(guard_seq(G, Bs)) of - true -> {match, B}; - false -> match_if(Cs, Bs) - end. +if_clauses([{'clause', _, [], G, B} | Cs], Bs) -> + case guard_seq(G, Bs) of + true -> + B; + false -> + if_clauses(Cs, Bs) + end; +if_clauses([], _Bs) -> + erlang:error('if_clause'). --spec match_case(Clauses, Argument, Bindings) -> {match, Body, ScopeBindings} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), - Argument :: cauder_syntax:af_literal(), +-spec case_clauses(Clauses, Value, Bindings) -> {Body, ScopeBindings} | nomatch when + Clauses :: clauses(), + Value :: term(), Bindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(), ScopeBindings :: cauder_bindings:bindings(). -match_case(Cs, V, Bs) -> match_clause(Cs, [V], Bs). +case_clauses(Cs, Val, Bs) -> + case match_clause(Cs, [Val], Bs) of + {B, Bs1} -> + {B, Bs1}; + nomatch -> + erlang:error({'case_clause', Val}) + end. + +-spec receive_clauses(Clauses, Message, Bindings) -> {Body, NewBindings} | nomatch when + Clauses :: clauses(), + Message :: cauder_message:message(), + Bindings :: cauder_bindings:bindings(), + Body :: cauder_syntax:af_body(), + NewBindings :: cauder_bindings:bindings(). + +receive_clauses(Cs, #message{val = Val}, Bs) -> + match_clause(Cs, [Val], Bs). --spec match_fun(Clauses, Arguments) -> {match, Body, ScopeBindings} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), - Arguments :: [cauder_syntax:af_literal()], +-spec match_fun(Clauses, ValueList) -> {Body, ScopeBindings} | nomatch when + Clauses :: clauses(), + ValueList :: [term()], Body :: cauder_syntax:af_body(), ScopeBindings :: cauder_bindings:bindings(). -match_fun(Cs, Vs) -> match_clause(Cs, Vs, cauder_bindings:new()). +match_fun(Cs, Vals) -> + match_clause(Cs, Vals, cauder_bindings:new()). -spec match_receive_pid(Clauses, RecipientPid, Mail, Bindings, Sched, Sys) -> {Body, {Message, QueuePosition}, NewMail, NewBindings} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), + Clauses :: clauses(), RecipientPid :: cauder_process:id(), Mail :: cauder_mailbox:mailbox(), Bindings :: cauder_bindings:bindings(), @@ -544,8 +562,8 @@ match_receive_pid(Cs, Pid, Mail, Bs, Sched, Sys) -> ?SCHEDULER_Manual -> FoldQueue = fun(Msg, Map1) -> - case match_receive(Cs, #message{uid = Uid} = Msg, Bs) of - {match, Body, Bs1} -> maps:put(Uid, {Bs1, Body, Msg}, Map1); + case receive_clauses(Cs, #message{uid = Uid} = Msg, Bs) of + {Body, Bs1} -> maps:put(Uid, {Bs1, Body, Msg}, Map1); nomatch -> skip end end, @@ -572,8 +590,8 @@ match_receive_pid(Cs, Pid, Mail, Bs, Sched, Sys) -> MatchingBranches = lists:filtermap( fun(Queue) -> {value, Msg} = queue:peek(Queue), - case match_receive(Cs, Msg, Bs) of - {match, Body, Bs1} -> {true, {Bs1, Body, Msg}}; + case receive_clauses(Cs, Msg, Bs) of + {Body, Bs1} -> {true, {Bs1, Body, Msg}}; nomatch -> false end end, @@ -590,19 +608,10 @@ match_receive_pid(Cs, Pid, Mail, Bs, Sched, Sys) -> end end. --spec match_receive(Clauses, Message, Bindings) -> {match, Body, NewBindings} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), - Message :: cauder_message:message(), - Bindings :: cauder_bindings:bindings(), - Body :: cauder_syntax:af_body(), - NewBindings :: cauder_bindings:bindings(). - -match_receive(Cs, #message{val = Value}, Bs0) -> match_clause(Cs, [abstract(Value)], Bs0). - -spec match_receive_uid(Clauses, Uid, Mail, Bindings) -> {Body, {Message, QueuePosition}, NewMail, NewBindings} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), + Clauses :: clauses(), Uid :: cauder_message:uid(), Mail :: cauder_mailbox:mailbox(), Bindings :: cauder_bindings:bindings(), @@ -617,149 +626,167 @@ match_receive_uid(Cs, Uid, Mail0, Bs0) -> error -> nomatch; {{Msg, QPos}, Mail1} -> - case match_clause(Cs, [abstract(Msg#message.val)], Bs0) of - {match, Body, Bs} -> {Body, {Msg, QPos}, Mail1, Bs}; + case match_clause(Cs, [Msg#message.val], Bs0) of + {Body, Bs} -> {Body, {Msg, QPos}, Mail1, Bs}; nomatch -> nomatch end end. --spec match_clause(Clauses, Arguments, Bindings) -> {match, Body, ScopeBindings} | nomatch when - Clauses :: cauder_syntax:af_clause_seq(), - Arguments :: [cauder_syntax:af_literal()], +-spec match_clause(Clauses, ValueList, Bindings) -> {Body, ScopeBindings} | nomatch when + Clauses :: clauses(), + ValueList :: [term()], Bindings :: cauder_bindings:bindings(), Body :: cauder_syntax:af_body(), ScopeBindings :: cauder_bindings:bindings(). -match_clause([], _, _) -> - nomatch; -match_clause([{'clause', _, Ps, G, B} | Cs], Vs, Bs0) -> - case match(Ps, Vs, Bs0) of - {match, Bs} -> - case concrete(guard_seq(G, Bs)) of - true -> {match, B, Bs}; - false -> match_clause(Cs, Vs, Bs0) +match_clause([{'clause', _, H, G, B} | Cs], Vals, Bs) -> + case match_list(H, Vals, Bs) of + {match, Bs1} -> + case guard_seq(G, Bs1) of + true -> {B, Bs1}; + false -> match_clause(Cs, Vals, Bs) end; nomatch -> - match_clause(Cs, Vs, Bs0) - end. + match_clause(Cs, Vals, Bs) + end; +match_clause([], _, _) -> + nomatch. --spec clause_line(Clauses, Arguments, Bindings) -> Line when - Clauses :: cauder_syntax:af_clause_seq(), - Arguments :: [cauder_syntax:af_literal()], +-spec clause_line(Clauses, ValueList, Bindings) -> Line when + Clauses :: clauses(), + ValueList :: [term()], Bindings :: cauder_bindings:bindings(), Line :: non_neg_integer(). clause_line([], _, _) -> -1; -clause_line([{'clause', Line, Ps, G, _} | Cs], Vs, Bs0) -> - case match(Ps, Vs, Bs0) of - {match, Bs} -> - case concrete(guard_seq(G, Bs)) of +clause_line([{'clause', Line, Ps, G, _} | Cs], Vals, Bs) -> + case match_list(Ps, Vals, Bs) of + {match, Bs1} -> + case guard_seq(G, Bs1) of true -> Line; - false -> clause_line(Cs, Vs, Bs0) + false -> clause_line(Cs, Vals, Bs) end; nomatch -> - clause_line(Cs, Vs, Bs0) + clause_line(Cs, Vals, Bs) end. %% Tries to match a list of values against a list of patterns using the given environment. %% The list of values should have no variables. --spec match(Patterns, Arguments, Bindings) -> {match, NewBindings} | nomatch when - Patterns :: [cauder_syntax:af_pattern()], - Arguments :: [cauder_syntax:af_literal()], +-spec match(Pattern, Term, Bindings) -> {match, NewBindings} | nomatch when + Pattern :: cauder_syntax:af_pattern(), + Term :: term(), Bindings :: cauder_bindings:bindings(), NewBindings :: cauder_bindings:bindings(). -match([], [], Bs) -> - {match, Bs}; -match([Pat | Ps0], [{value, _, Val} | Vs0], Bs0) when length(Ps0) == length(Vs0) -> - case catch match1(Pat, Val, Bs0) of - {match, Bs} -> match(Ps0, Vs0, Bs); - nomatch -> nomatch - end; -match(_Bs, _Ps, _Vs) -> - nomatch. +match(Pat, Term, Bs0) -> + case catch match1(Pat, Term, Bs0) of + invalid -> + % TODO Convert pattern to term + erlang:error({illegal_pattern, Pat}); + Other -> + Other + end. -% TODO Organize arguments to be consistent --spec match1(Pattern, Term, Bindings) -> {match, NewBindings} | no_return() when +-spec match1(Pattern, Term, Bindings) -> {match, NewBindings} when Pattern :: cauder_syntax:af_pattern(), Term :: term(), Bindings :: cauder_bindings:bindings(), NewBindings :: cauder_bindings:bindings(). -match1({value, _, V}, V, Bs) -> - {match, Bs}; +match1({value, _, T0}, T, Bs) -> + case T of + T0 -> {match, Bs}; + _ -> throw(nomatch) + end; match1({var, _, '_'}, _, Bs) -> {match, Bs}; -match1({var, _, Name}, Value, Bs0) -> - case cauder_bindings:find(Name, Bs0) of - {ok, Value} -> - {match, Bs0}; +match1({var, _, Name}, Term, Bs) -> + case cauder_bindings:find(Name, Bs) of + {ok, Term} -> + {match, Bs}; {ok, _} -> throw(nomatch); error -> - Bs1 = cauder_bindings:add(Name, Value, Bs0), - {match, Bs1} + {match, cauder_bindings:add(Name, Term, Bs)} end; -match1({match, _, Pat1, Pat2}, Term, Bs0) -> - {match, Bs1} = match1(Pat1, Term, Bs0), +match1({match, _, Pat1, Pat2}, Term, Bs) -> + {match, Bs1} = match1(Pat1, Term, Bs), match1(Pat2, Term, Bs1); -match1({cons, _, H, T}, [H1 | T1], Bs0) -> - {match, Bs} = match1(H, H1, Bs0), - match1(T, T1, Bs); +match1({cons, _, H, T}, [H1 | T1], Bs) -> + {match, Bs1} = match1(H, H1, Bs), + match1(T, T1, Bs1); +match1({cons, _, _, _}, _, _Bs) -> + throw(nomatch); match1({tuple, _, Es}, Tuple, Bs) when length(Es) =:= tuple_size(Tuple) -> match_tuple(Es, Tuple, 1, Bs); match1(_, _, _) -> - throw(nomatch). + throw(invalid). --spec match_tuple(Values, Tuple, Index, Bindings) -> {match, NewBindings} | no_return() when - Values :: [cauder_syntax:af_literal()], +-spec match_tuple(Elements, Tuple, Index, Bindings) -> {match, NewBindings} | no_return() when + Elements :: [cauder_syntax:af_pattern()], Tuple :: tuple(), Index :: pos_integer(), Bindings :: cauder_bindings:bindings(), NewBindings :: cauder_bindings:bindings(). -match_tuple([], _, _, Bs) -> - {match, Bs}; match_tuple([E | Es], Tuple, I, Bs0) -> {match, Bs} = match1(E, element(I, Tuple), Bs0), - match_tuple(Es, Tuple, I + 1, Bs). + match_tuple(Es, Tuple, I + 1, Bs); +match_tuple([], _, _, Bs) -> + {match, Bs}. + +-spec match_list(PatternList, TermList, Bindings) -> {match, NewBindings} | nomatch when + PatternList :: [cauder_syntax:af_pattern()], + TermList :: [term()], + Bindings :: cauder_bindings:bindings(), + NewBindings :: cauder_bindings:bindings(). + +match_list([P | Ps], [T | Ts], Bs) -> + case match(P, T, Bs) of + {match, Bs1} -> + match_list(Ps, Ts, Bs1); + nomatch -> + nomatch + end; +match_list([], [], Bs) -> + {match, Bs}; +match_list(_Ps, _Ts, _Bs) -> + nomatch. %%%============================================================================= --spec guard_seq(Guards, Bindings) -> Boolean when +-spec guard_seq(Guards, Bindings) -> boolean() when Guards :: cauder_syntax:af_guard_seq(), - Bindings :: cauder_bindings:bindings(), - Boolean :: cauder_syntax:af_boolean(). + Bindings :: cauder_bindings:bindings(). guard_seq([], _) -> - abstract(true); + true; guard_seq(Gs, Bs) when is_list(Gs) -> % In a guard sequence, guards are evaluated until one is true. The remaining guards, if any, are not evaluated. % See: https://erlang.org/doc/reference_manual/expressions.html#guard-sequences - abstract(lists:any(fun(G) -> concrete(guard(G, Bs)) end, Gs)). + lists:any(fun(G) -> guard(G, Bs) end, Gs). --spec guard(Guard, Bindings) -> Boolean when +-spec guard(Guard, Bindings) -> boolean() when Guard :: cauder_syntax:af_guard(), - Bindings :: cauder_bindings:bindings(), - Boolean :: cauder_syntax:af_boolean(). + Bindings :: cauder_bindings:bindings(). guard(G, Bs) when is_list(G) -> - abstract(lists:all(fun(Gt) -> concrete(guard_test(Gt, Bs)) end, G)). + lists:all(fun(Gt) -> guard_test(Gt, Bs) end, G). --spec guard_test(GuardTest, Bindings) -> GuardTest | Boolean when +-spec guard_test(GuardTest, Bindings) -> boolean() when GuardTest :: cauder_syntax:af_guard_test(), - Bindings :: cauder_bindings:bindings(), - Boolean :: cauder_syntax:af_boolean(). + Bindings :: cauder_bindings:bindings(). guard_test(Gt, Bs) -> + % TODO erl_lint:is_guard_test/1 case is_reducible(Gt, Bs) of true -> #result{expr = [Gt1]} = expr(Gt, Bs, cauder_stack:new()), guard_test(Gt1, Bs); false -> - Gt + concrete(Gt) end. %%%============================================================================= @@ -789,7 +816,7 @@ concrete({cons, _, {value, _, H}, {value, _, T}}) -> [H | T]. %% reduced any further or not, given an environment. -spec is_reducible(Expression | [Expression], Bindings) -> IsReducible when - Expression :: cauder_syntax:abstract_expr(), + Expression :: expression(), Bindings :: cauder_bindings:bindings(), IsReducible :: boolean(). @@ -814,7 +841,7 @@ is_reducible(E, _) when is_tuple(E) -> %% @doc Checks if the given abstract expression is a literal value. -spec is_value(Expression | [Expression]) -> IsValue when - Expression :: cauder_syntax:abstract_expr(), + Expression :: expression(), IsValue :: boolean(). is_value([]) -> true; @@ -826,7 +853,7 @@ is_value(E) when is_tuple(E) -> false. -spec eval_and_update(Index, Expression, Bindings, Stack) -> Result when Index :: pos_integer(), - Expression :: cauder_syntax:abstract_expr(), + Expression :: expression(), Bindings :: cauder_bindings:bindings(), Stack :: cauder_stack:stack(), Result :: cauder_eval:result(). From e3182eba5d3df885171047d8556e2f3ddbe8a2b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Sun, 16 Jan 2022 19:39:58 +0100 Subject: [PATCH 6/8] Move `abstract/1` and `concrete/1` from `cauder_eval` to `cauder_syntax` --- src/cauder_eval.erl | 92 +++++++++++++++---------------- src/cauder_semantics_forwards.erl | 2 +- src/cauder_syntax.erl | 27 ++++++++- 3 files changed, 69 insertions(+), 52 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 6744407..1ae5d60 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -2,7 +2,7 @@ %% API -export([exprs/3]). --export([abstract/1, concrete/1, is_value/1, is_reducible/2]). +-export([is_value/1, is_reducible/2]). -export([match_receive_pid/6, match_receive_uid/4]). -export([clause_line/3]). @@ -72,10 +72,18 @@ exprs([E | Es], Bs, Stk) -> {Entry, Stk1} = cauder_stack:pop(Stk), case Entry of {value, #s_function{env = Bs1, expr = Es1, var = Var}} -> - Es2 = cauder_syntax:replace_variable(Es1, setelement(2, Var, Line), concrete(E)), + Es2 = cauder_syntax:replace_variable( + Es1, + setelement(2, Var, Line), + cauder_syntax:concrete(E) + ), #result{env = Bs1, expr = Es2, stack = Stk1}; {value, #s_block{expr = Es1, var = Var}} -> - Es2 = cauder_syntax:replace_variable(Es1, setelement(2, Var, Line), concrete(E)), + Es2 = cauder_syntax:replace_variable( + Es1, + setelement(2, Var, Line), + cauder_syntax:concrete(E) + ), #result{env = Bs, expr = Es2, stack = Stk1} end; _ -> @@ -122,7 +130,7 @@ expr(E = {cons, Line, H0, T0}, Bs, Stk) -> true -> R = #result{expr = [H]} = expr(H0, Bs, Stk), case is_value(H) andalso is_value(T0) of - true -> R#result{expr = [{value, Line, [concrete(H) | concrete(T0)]}]}; + true -> R#result{expr = [{value, Line, [cauder_syntax:concrete(H) | cauder_syntax:concrete(T0)]}]}; false -> R#result{expr = [setelement(3, E, H)]} end; false -> @@ -130,18 +138,24 @@ expr(E = {cons, Line, H0, T0}, Bs, Stk) -> true -> R = #result{expr = [T]} = expr(T0, Bs, Stk), case is_value(H0) andalso is_value(T) of - true -> R#result{expr = [{value, Line, [concrete(H0) | concrete(T)]}]}; - false -> R#result{expr = [setelement(4, E, T)]} + true -> + R#result{expr = [{value, Line, [cauder_syntax:concrete(H0) | cauder_syntax:concrete(T)]}]}; + false -> + R#result{expr = [setelement(4, E, T)]} end; false -> - #result{env = Bs, expr = [{value, Line, [concrete(H0) | concrete(T0)]}], stack = Stk} + #result{ + env = Bs, + expr = [{value, Line, [cauder_syntax:concrete(H0) | cauder_syntax:concrete(T0)]}], + stack = Stk + } end end; expr(E = {tuple, Line, Es0}, Bs, Stk) -> R = #result{expr = Es} = expr_list(Es0, Bs, Stk), case is_value(Es) of true -> - Tuple = list_to_tuple(lists:map(fun concrete/1, Es)), + Tuple = list_to_tuple(lists:map(fun cauder_syntax:concrete/1, Es)), #result{env = Bs, expr = [{value, Line, Tuple}], stack = Stk}; false -> R#result{expr = [setelement(3, E, Es)]} @@ -195,7 +209,7 @@ expr(E = {bif, Line, M, F, As}, Bs, Stk) -> true -> eval_and_update(5, E, Bs, Stk); false -> - Value = apply(M, F, lists:map(fun concrete/1, As)), + Value = apply(M, F, lists:map(fun cauder_syntax:concrete/1, As)), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end; expr({self, Line}, Bs, Stk) -> @@ -229,7 +243,7 @@ expr(E = {spawn, Line, N, Fun}, Bs, Stk) -> eval_and_update(4, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), - Label = #label_spawn_fun{var = Var, node = concrete(N), function = Fun}, + Label = #label_spawn_fun{var = Var, node = cauder_syntax:concrete(N), function = Fun}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end end; @@ -249,9 +263,9 @@ expr(E = {spawn, Line, M, F, As}, Bs, Stk) -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_mfa{ var = Var, - module = concrete(M), - function = concrete(F), - args = concrete(As) + module = cauder_syntax:concrete(M), + function = cauder_syntax:concrete(F), + args = cauder_syntax:concrete(As) }, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end @@ -277,10 +291,10 @@ expr(E = {spawn, Line, N, M, F, As}, Bs, Stk) -> Var = cauder_utils:temp_variable(Line), Label = #label_spawn_mfa{ var = Var, - node = concrete(N), - module = concrete(M), - function = concrete(F), - args = concrete(As) + node = cauder_syntax:concrete(N), + module = cauder_syntax:concrete(M), + function = cauder_syntax:concrete(F), + args = cauder_syntax:concrete(As) }, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end @@ -293,7 +307,7 @@ expr(E = {start, Line, N}, Bs, Stk) -> eval_and_update(3, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), - Label = #label_start{var = Var, name = concrete(N)}, + Label = #label_start{var = Var, name = cauder_syntax:concrete(N)}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end; expr(E = {start, Line, H, N}, Bs, Stk) -> @@ -306,7 +320,7 @@ expr(E = {start, Line, H, N}, Bs, Stk) -> eval_and_update(4, E, Bs, Stk); false -> Var = cauder_utils:temp_variable(Line), - Label = #label_start{var = Var, name = concrete(N), host = concrete(H)}, + Label = #label_start{var = Var, name = cauder_syntax:concrete(N), host = cauder_syntax:concrete(H)}, #result{env = Bs, expr = [Var], stack = Stk, label = Label} end end; @@ -319,7 +333,7 @@ expr(E = {Send, _, L, R}, Bs, Stk) when Send =:= 'send' orelse Send =:= 'send_op true -> eval_and_update(4, E, Bs, Stk); false -> - Label = #label_send{dst = concrete(L), val = concrete(R)}, + Label = #label_send{dst = cauder_syntax:concrete(L), val = cauder_syntax:concrete(R)}, #result{env = Bs, expr = [R], stack = Stk, label = Label} end end; @@ -356,8 +370,8 @@ expr(E = {apply, Line, M0, F0, As}, Bs0, Stk0) -> true -> eval_and_update(5, E, Bs0, Stk0); false -> - M = concrete(M0), - F = concrete(F0), + M = cauder_syntax:concrete(M0), + F = cauder_syntax:concrete(F0), remote_call(M, F, As, Stk0, Line, Bs0) end end @@ -372,7 +386,7 @@ expr(E = {apply_fun, Line, Fun, As}, Bs0, Stk0) -> eval_and_update(4, E, Bs0, Stk0); false -> A = length(As), - {env, [{{M, F}, Bs1, Cs}]} = erlang:fun_info(concrete(Fun), env), + {env, [{{M, F}, Bs1, Cs}]} = erlang:fun_info(cauder_syntax:concrete(Fun), env), {Body, Bs2} = match_fun(Cs, As), Var = cauder_utils:temp_variable(Line), Bs = cauder_bindings:merge(Bs1, Bs2), @@ -390,7 +404,7 @@ expr(E = {match, _, Lhs, Rhs}, Bs0, Stk) -> true -> eval_and_update(4, E, Bs0, Stk); false -> - Val = concrete(Rhs), + Val = cauder_syntax:concrete(Rhs), case match(Lhs, Val, Bs0) of {match, Bs} -> #result{env = Bs, expr = [Rhs], stack = Stk}; nomatch -> error({badmatch, Val}) @@ -402,7 +416,7 @@ expr(E = {op, Line, Op, As}, Bs, Stk) -> true -> eval_and_update(4, E, Bs, Stk); false -> - Value = apply(erlang, Op, lists:map(fun concrete/1, As)), + Value = apply(erlang, Op, lists:map(fun cauder_syntax:concrete/1, As)), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end; expr(E = {'andalso', Line, Lhs, Rhs}, Bs, Stk) -> @@ -418,7 +432,7 @@ expr(E = {'andalso', Line, Lhs, Rhs}, Bs, Stk) -> true -> eval_and_update(4, E, Bs, Stk); false -> - Value = apply(erlang, 'and', [concrete(Lhs), concrete(Rhs)]), + Value = apply(erlang, 'and', [cauder_syntax:concrete(Lhs), cauder_syntax:concrete(Rhs)]), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end end @@ -436,7 +450,7 @@ expr(E = {'orelse', Line, Lhs, Rhs}, Bs, Stk) -> true -> eval_and_update(4, E, Bs, Stk); false -> - Value = apply(erlang, 'or', [concrete(Lhs), concrete(Rhs)]), + Value = apply(erlang, 'or', [cauder_syntax:concrete(Lhs), cauder_syntax:concrete(Rhs)]), #result{env = Bs, expr = [{value, Line, Value}], stack = Stk} end end @@ -483,7 +497,7 @@ remote_call(M, F, As, Stk0, Line, Bs0) -> Stk = cauder_stack:push(Entry, Stk0), #result{env = Bs0, expr = [Var], stack = Stk}; error -> - Value = apply(M, F, lists:map(fun concrete/1, As)), + Value = apply(M, F, lists:map(fun cauder_syntax:concrete/1, As)), #result{env = Bs0, expr = [{value, Line, Value}], stack = Stk0} end. @@ -786,31 +800,11 @@ guard_test(Gt, Bs) -> #result{expr = [Gt1]} = expr(Gt, Bs, cauder_stack:new()), guard_test(Gt1, Bs); false -> - concrete(Gt) + cauder_syntax:concrete(Gt) end. %%%============================================================================= -%%------------------------------------------------------------------------------ -%% @doc Converts the given Erlang term into its abstract form. - --spec abstract(Term) -> Literal when - Term :: term(), - Literal :: cauder_syntax:af_literal(). - -abstract(Value) -> {value, 0, Value}. - -%%------------------------------------------------------------------------------ -%% @doc Converts the given abstract literal element into the Erlang term that it -%% represents. - --spec concrete(Literal) -> Term when - Literal :: cauder_syntax:af_literal(), - Term :: term(). - -concrete({value, _, Value}) -> Value; -concrete({cons, _, {value, _, H}, {value, _, T}}) -> [H | T]. - %%------------------------------------------------------------------------------ %% @doc Checks if the given abstract expression (or list of expressions) can be %% reduced any further or not, given an environment. diff --git a/src/cauder_semantics_forwards.erl b/src/cauder_semantics_forwards.erl index e26720b..c79a32f 100644 --- a/src/cauder_semantics_forwards.erl +++ b/src/cauder_semantics_forwards.erl @@ -356,7 +356,7 @@ rule_spawn( node = LogEntry#log_spawn.node, pid = LogEntry#log_spawn.pid, mfa = {M, F, length(As)}, - expr = [cauder_syntax:remote_call(M, F, lists:map(fun cauder_eval:abstract/1, As))] + expr = [cauder_syntax:remote_call(M, F, lists:map(fun cauder_syntax:abstract/1, As))] } end, TraceAction = #trace_spawn{ diff --git a/src/cauder_syntax.erl b/src/cauder_syntax.erl index 8591dc9..e1ed947 100644 --- a/src/cauder_syntax.erl +++ b/src/cauder_syntax.erl @@ -10,6 +10,7 @@ %% API -export([clauses/1, expr_list/1]). +-export([abstract/1, concrete/1]). -export([replace_variable/3]). -export([to_abstract_expr/1]). -export([remote_call/3]). @@ -571,6 +572,28 @@ exception(Class, Reason) -> %%%============================================================================= +%%------------------------------------------------------------------------------ +%% @doc Converts the given Erlang term into its abstract form. + +-spec abstract(Term) -> Literal when + Term :: term(), + Literal :: cauder_syntax:af_literal(). + +abstract(Value) -> {value, 0, Value}. + +%%------------------------------------------------------------------------------ +%% @doc Converts the given abstract literal element into the Erlang term that it +%% represents. + +-spec concrete(Literal) -> Term when + Literal :: cauder_syntax:af_literal(), + Term :: term(). + +concrete({value, _, Value}) -> Value; +concrete({cons, _, {value, _, H}, {value, _, T}}) -> [H | T]. + +%%%============================================================================= + %%------------------------------------------------------------------------------ %% @doc Replaces all occurrences of the given `Variable' in each one of the %% `Expressions' with the given literal `Value'. @@ -601,14 +624,14 @@ replace_variable({cons, Line, H0, T0}, Var, Val) -> H = replace_variable(H0, Var, Val), T = replace_variable(T0, Var, Val), case cauder_eval:is_value(H) andalso cauder_eval:is_value(T) of - true -> {value, Line, [cauder_eval:concrete(H) | cauder_eval:concrete(T)]}; + true -> {value, Line, [cauder_syntax:concrete(H) | cauder_syntax:concrete(T)]}; false -> {cons, Line, H, T} end; replace_variable({tuple, Line, Es0}, Var, Val) -> Es = replace_variable(Es0, Var, Val), case cauder_eval:is_value(Es) of true -> - Tuple = list_to_tuple(lists:map(fun cauder_eval:concrete/1, Es)), + Tuple = list_to_tuple(lists:map(fun cauder_syntax:concrete/1, Es)), {value, Line, Tuple}; false -> {tuple, Line, Es} From 6da4e9ec22bf1ff1f6844a39d21f7d2048cfa003 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Sun, 16 Jan 2022 19:41:17 +0100 Subject: [PATCH 7/8] Remove `cauder_eval:clause_line/3` --- src/cauder_eval.erl | 20 -------------------- src/cauder_syntax.erl | 3 +-- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 1ae5d60..56b6c13 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -4,7 +4,6 @@ -export([exprs/3]). -export([is_value/1, is_reducible/2]). -export([match_receive_pid/6, match_receive_uid/4]). --export([clause_line/3]). -include("cauder_message.hrl"). -include("cauder_stack.hrl"). @@ -666,25 +665,6 @@ match_clause([{'clause', _, H, G, B} | Cs], Vals, Bs) -> match_clause([], _, _) -> nomatch. --spec clause_line(Clauses, ValueList, Bindings) -> Line when - Clauses :: clauses(), - ValueList :: [term()], - Bindings :: cauder_bindings:bindings(), - Line :: non_neg_integer(). - -clause_line([], _, _) -> - -1; -clause_line([{'clause', Line, Ps, G, _} | Cs], Vals, Bs) -> - case match_list(Ps, Vals, Bs) of - {match, Bs1} -> - case guard_seq(G, Bs1) of - true -> Line; - false -> clause_line(Cs, Vals, Bs) - end; - nomatch -> - clause_line(Cs, Vals, Bs) - end. - %% Tries to match a list of values against a list of patterns using the given environment. %% The list of values should have no variables. diff --git a/src/cauder_syntax.erl b/src/cauder_syntax.erl index e1ed947..42c6f76 100644 --- a/src/cauder_syntax.erl +++ b/src/cauder_syntax.erl @@ -868,6 +868,5 @@ set_line(Node, Line) -> erl_syntax:set_pos(Node, erl_anno:new(Line)). remote_call(M, F, As) -> A = length(As), - {_, Cs} = cauder_utils:fundef_lookup({M, F, A}), - Line = cauder_eval:clause_line(Cs, As, cauder_bindings:new()), + {_, [{'clause', Line, _Ps, _G, _B} | _]} = cauder_utils:fundef_lookup({M, F, A}), {remote_call, Line, M, F, lists:map(fun(V) -> setelement(2, V, Line) end, As)}. From 1c4c3790019e94f799f94d7316693c77ba5a2484 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juan=20Jos=C3=A9=20Gonz=C3=A1lez-Abril?= Date: Sun, 16 Jan 2022 19:41:41 +0100 Subject: [PATCH 8/8] Add edoc --- src/cauder_eval.erl | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/cauder_eval.erl b/src/cauder_eval.erl index 56b6c13..84b1a93 100644 --- a/src/cauder_eval.erl +++ b/src/cauder_eval.erl @@ -1,3 +1,11 @@ +%%%----------------------------------------------------------------------------- +%%% @doc The CauDEr meta interpreter. +%%% This module provides an interpreter for Erlang expressions. +%%% The expressions are in the abstract syntax as returned by `cauder_syntax'. +%%% @see erl_eval +%%% @end +%%%----------------------------------------------------------------------------- + -module(cauder_eval). %% API @@ -825,6 +833,8 @@ is_value({cons, _, H, T}) -> is_value(H) andalso is_value(T); is_value({tuple, _, Es}) -> is_value(Es); is_value(E) when is_tuple(E) -> false. +%%%============================================================================= + -spec eval_and_update(Index, Expression, Bindings, Stack) -> Result when Index :: pos_integer(), Expression :: expression(),