1		% (c) 2009-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(test_typechecker,[run_typecheck_testcase/2]).
6
7		:- use_module(library(codesio)).
8		:- use_module(library(file_systems)).
9
10		:- use_module(probsrc(bsyntaxtree)).
11		:- use_module(probsrc(btypechecker)).
12		:- use_module(probsrc(bmachine_structure)).
13		:- use_module(probsrc(bmachine_construction)).
14		:- use_module(probsrc(parsercall)).
15		:- use_module(probsrc(tools)).
16		:- use_module(probsrc(translate),[pretty_type/2]).
17
18		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
19		% typechecker-test framework
20
21		run_typecheck_testcase(Filename,Type) :-
22		run_testcase(Filename,Filename,Type,Verdicts),
23		nl,print_verdicts(Verdicts,*),
24		summarized_verdict(Verdicts,V),
25		!,
26		(V==pass -> print('All tests passed\n') ; print('Test failed\n'),fail).
27
28		print_verdicts([],_).
29		print_verdicts([verdict(Testname,Subname,Verdict)|Rest],Before) :-
30		(Before=Testname -> true ; write(Testname),write(':'),nl),
31		format('~t~q~10|: ~q~n',[Subname,Verdict]),
32		print_verdicts(Rest,Testname).
33
34		summarized_verdict(Vs,Sum) :- summarized_verdict2(Vs,pass,Sum).
35		summarized_verdict2([],V,V).
36		summarized_verdict2([verdict(_,_,V)|Rest],Old,New) :-
37		(V==pass -> summarized_verdict2(Rest,Old,New) ; New=fail).
38
39		:- use_module(b_global_sets,[b_clear_global_set_type_definitions/0]).
40		run_testcase(Filename,Testname,Type,Verdict) :-
41		b_clear_global_set_type_definitions,
42		catch(( absolute_file_name(Filename,AbsFilename),
43		load_b_machine_as_term(AbsFilename,Machine,[]) ->
44		( run_testcase2(Type,Testname,Machine,Verdict) -> true
45		; Verdict = [verdict(Testname,*,error('run_testcase2 failed'))])
46		; Verdict = [verdict(Testname,*,error('unable to load testfile'))]),
47		X,
48		Verdict = [verdict(Testname,*,error(X))]).
49
50		run_testcase2(Type, Testname, complete_machine(Main, Machines, _), Verdict) :-
51		( extract_tests(Main,Machines,Test) ->
52		( \+ ground(Test) ->
53		Verdict = [verdict(Testname,*,error('testcases not ground'))]
54	?	; check_machine(Main, Machines, Typed, Errors) ->
55		( run_testcase3(Type,Testname,Typed,Errors,Test,Verdict) -> true
56		; Verdict = [verdict(Testname,*,error('run_testcase3 failed'))])
57		;
58		Verdict = [verdict(Testname,*,fail('type checker failed'))])
59		;
60		Verdict = [verdict(Testname,*,error('extracting tests failed'))]).
61
62		extract_tests(Main,Machines,Tests) :-
63		findall(test(Name,T),
64		( get_secs(Main,Machines,Secs),
65		member(definitions(_,Defs),Secs),
66		member(expression_definition(_,Fullname,[],string(_,TestAtom)),Defs),
67		atom_chars(Fullname,CFullname),
68		append(['T','E','S','T','_'],CName,CFullname),
69		atom_chars(Name,CName),
70		atom_codes(TestAtom,TestCodes1),append(TestCodes1,[0'.],TestCodes),
71		read_from_codes(TestCodes,T)),
72		Tests).
73		get_secs(Name,Machines,Secs) :-
74	?	member(abstract_machine(_,_ModelType,machine_header(_,Name,_),Secs),Machines).
75		get_secs(Name,Machines,Secs) :-
76		member(refinement_machine(_,machine_header(_,Name,_),_Refines,Secs),Machines).
77
78
79		run_testcase3(typesok, Testname, Typed, Errors, Tests, Verdict) :-
80		( Errors = [] ->
81		Verdict = [verdict(Testname,typecheck,pass)|Verdict1],
82		run_checks(Tests,Testname,Typed,Verdict1)
83		;
84		Verdict = [verdict(Testname,*,fail('unexpected errors from type-checker', Errors))]).
85
86		run_checks([],_,_,[]).
87		run_checks([test(Name,Test)|Rest],Testname,Typed,[verdict(Testname,Name,Verdict)|VRest]) :-
88		run_check(Test,Typed,Verdict),
89		run_checks(Rest,Testname,Typed,VRest).
90
91		run_check(ElemPos:ExpectedType, Typed, Verdict) :-
92		( slashes_to_list(ElemPos,ElemPosL),
93		get_element(ElemPosL,Typed,Element) ->
94		( get_texpr_type(Element,Type) ->
95		( Type == ExpectedType ->
96		Verdict = pass
97		;
98		safe_pretty_type(ExpectedType, PExp),
99		safe_pretty_type(Type, PType),
100		ajoin(['expected ',PExp,', but was ', PType],Msg),
101		Verdict = fail(Msg))
102		;
103		Verdict = fail('got ill-formed expression'))
104		;
105		write_to_codes(ElemPos,ElemStr),
106		atom_codes(ElemAtom,ElemStr),
107		ajoin(['element ',ElemAtom,' not found'], Msg),
108		Verdict = fail(Msg)).
109
110		safe_pretty_type(Type,Text) :-
111		(pretty_type(Type,Text) -> true ; Text = '<failed to pretty type>').
112
113		slashes_to_list(A/B,List) :-
114		!,slashes_to_list(A,AList),
115		slashes_to_list(B,BList),
116		append(AList,BList,List).
117		slashes_to_list(X,[X]).
118
119		get_element([Section|Path],M,Elem) :-
120		get_section(Section,M,Content),
121	?	get_element2(Content,Path,Elem),!.
122		get_element2([H|T],Path,Elem) :- !,
123	?	member(Sub,[H|T]),get_element2(Sub,Path,Elem).
124		get_element2(TExpr,Path,Elem) :-
125		is_texpr(TExpr),
126		get_texpr_expr(TExpr,Expr),
127		( Path = [] ->
128		Elem=TExpr
129		; Expr = identifier(op(ID)) ->
130	?	get_element3(Path,ID,TExpr,Elem)
131		; Expr = identifier(ID) ->
132	?	get_element3(Path,ID,TExpr,Elem)
133		; Expr = operation(OpId,_,_,_),get_texpr_id(OpId,op(ID)) ->
134	?	get_element3(Path,ID,TExpr,Elem)
135		; functor(Expr,Functor,_) ->
136	?	get_element3(Path,Functor,TExpr,Elem)).
137		get_element3([Path],Path,TExpr,TExpr).
138		get_element3([Head|Rest],Head,TExpr,Elem) :-
139		Rest=[_|_],
140		syntaxtraversion(TExpr,_,_,_,Subs,_),
141	?	get_element2(Subs,Rest,Elem).
142		get_element3([*|Rest],Pattern,TExpr,Elem) :-
143	?	Rest=[_|_],get_element3(Rest,Pattern,TExpr,Elem).
144		get_element3([*|Rest],_Pattern,TExpr,Elem) :-
145		Rest=[_|_],
146		syntaxtraversion(TExpr,_,_,_,Subs,_),
147	?	get_element2(Subs,[*|Rest],Elem).