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