-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexecute_ghc.erl
46 lines (33 loc) · 1.71 KB
/
execute_ghc.erl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
-module(execute_ghc).
-export([execute/5, setup/0, report/0, update_coverage/1]).
compile_and_run_ghc(BaseName, ReportDirectory, true) ->
case exec:shell_exec( "ghc -dynamic -i BigStepSemanticsTraced.hs " ++ ReportDirectory ++ BaseName ++ ".hs" ) of
{0, _} -> {0, Output} = exec:shell_exec( "./" ++ ReportDirectory ++ BaseName ), Output;
{_, _} -> "failed"
end;
compile_and_run_ghc(BaseName, ReportDirectory, _Tracing) ->
case exec:shell_exec( "ghc -dynamic -i BigStepSemantics.hs " ++ ReportDirectory ++ BaseName ++ ".hs" ) of
{0, _} -> {0, Output} = exec:shell_exec( "./" ++ ReportDirectory ++ BaseName ), Output;
{_, _} -> "failed"
end.
convert_erl_to_coq(TestPath, BaseName, ReportDirectory, true) ->
misc:write_to_file(ReportDirectory ++ BaseName ++ ".hs", cst_to_ast:from_erl(TestPath, functionalSemanticHaskellTraced));
convert_erl_to_coq(TestPath, BaseName, ReportDirectory, _Tracing) ->
misc:write_to_file(ReportDirectory ++ BaseName ++ ".hs", cst_to_ast:from_erl(TestPath, functionalSemanticHaskell)).
% wrapper
execute(TestPath, BaseName, ReportDirectory, Tracing, PID) ->
Res = execute(TestPath, BaseName, ReportDirectory, Tracing),
% io:format("GHC is ready!: ~p~n", [Res]),
PID ! {Res, coq_res}.
execute(TestPath, BaseName, ReportDirectory, Tracing) ->
convert_erl_to_coq(TestPath, BaseName, ReportDirectory, Tracing),
Output = compile_and_run_ghc(BaseName, ReportDirectory, Tracing),
execute_coq:parse_coq_result(Output, Tracing).
%% ---------------------------------------------------------------------
%% Coq Coverage measurement
setup() ->
execute_coq:setup().
update_coverage(Result) ->
execute_coq:update_coverage(Result).
report() ->
execute_coq:report().