test_typechecker

extract_tests(Main,Machines,Tests) :-
    findall(test(Name,T),
    ( get_secs(Main,Machines,Secs),
    member(definitions(_,Defs),Secs),
    member(expression_definition(_,Fullname,[],string(_,TestAtom)),Defs),
    atom_chars(Fullname,CFullname),
    append(['T','E','S','T','_'],CName,CFullname),
    atom_chars(Name,CName),
    atom_codes(TestAtom,TestCodes1),append(TestCodes1,[0'.],TestCodes),
    read_from_codes(TestCodes,T)),
    Tests).

get_element([Section|Path],M,Elem) :-
    get_section(Section,M,Content),
    get_element2(Content,Path,Elem),!.

get_element2([H|T],Path,Elem) :- !,
    member(Sub,[H|T]),get_element2(Sub,Path,Elem).

get_element2(TExpr,Path,Elem) :-
    is_texpr(TExpr),
    get_texpr_expr(TExpr,Expr),
    ( Path = [] ->
    Elem=TExpr
    ; Expr = identifier(op(ID)) ->
    get_element3(Path,ID,TExpr,Elem)
    ; Expr = identifier(ID) ->
    get_element3(Path,ID,TExpr,Elem)
    ; Expr = operation(OpId,_,_,_),get_texpr_id(OpId,op(ID)) ->
    get_element3(Path,ID,TExpr,Elem)
    ; functor(Expr,Functor,_) ->
    get_element3(Path,Functor,TExpr,Elem)).

get_element3([Path],Path,TExpr,TExpr).

get_element3([Head|Rest],Head,TExpr,Elem) :-
    Rest=[_|_],
    syntaxtraversion(TExpr,_,_,_,Subs,_),
    get_element2(Subs,Rest,Elem).

get_element3([*|Rest],Pattern,TExpr,Elem) :-
    Rest=[_|_],get_element3(Rest,Pattern,TExpr,Elem).

get_element3([*|Rest],_Pattern,TExpr,Elem) :-
    Rest=[_|_],
    syntaxtraversion(TExpr,_,_,_,Subs,_),
    get_element2(Subs,[*|Rest],Elem).

get_secs(Name,Machines,Secs) :-
    member(abstract_machine(_,_ModelType,machine_header(_,Name,_),Secs),Machines).

get_secs(Name,Machines,Secs) :-
    member(refinement_machine(_,machine_header(_,Name,_),_Refines,Secs),Machines).

print_verdicts([],_).

print_verdicts([verdict(Testname,Subname,Verdict)|Rest],Before) :-
    (Before=Testname -> true ; write(Testname),write(':'),nl),
    format('~t~q~10|: ~q~n',[Subname,Verdict]),
    print_verdicts(Rest,Testname).

run_check(ElemPos:ExpectedType, Typed, Verdict) :-
    ( slashes_to_list(ElemPos,ElemPosL),
    get_element(ElemPosL,Typed,Element) ->
    ( get_texpr_type(Element,Type) ->
    ( Type == ExpectedType ->
    Verdict = pass
    ;
    safe_pretty_type(ExpectedType, PExp),
    safe_pretty_type(Type, PType),
    ajoin(['expected ',PExp,', but was ', PType],Msg),
    Verdict = fail(Msg))
    ;
    Verdict = fail('got ill-formed expression'))
    ;
    write_to_codes(ElemPos,ElemStr),
    atom_codes(ElemAtom,ElemStr),
    ajoin(['element ',ElemAtom,' not found'], Msg),
    Verdict = fail(Msg)).

run_checks([],_,_,[]).

run_checks([test(Name,Test)|Rest],Testname,Typed,[verdict(Testname,Name,Verdict)|VRest]) :-
    run_check(Test,Typed,Verdict),
    run_checks(Rest,Testname,Typed,VRest).

run_testcase(Filename,Testname,Type,Verdict) :-
    b_clear_global_set_type_definitions,
    catch(( absolute_file_name(Filename,AbsFilename),
    load_b_machine_as_term(AbsFilename,Machine,[]) ->
    ( run_testcase2(Type,Testname,Machine,Verdict) -> true
    ; Verdict = [verdict(Testname,*,error('run_testcase2 failed'))])
    ; Verdict = [verdict(Testname,*,error('unable to load testfile'))]),
    X,
    Verdict = [verdict(Testname,*,error(X))]).

run_testcase2(Type, Testname, complete_machine(Main, Machines, _), Verdict) :-
    ( extract_tests(Main,Machines,Test) ->
    ( \+ ground(Test) ->
    Verdict = [verdict(Testname,*,error('testcases not ground'))]
    ; check_machine(Main, Machines, Typed, Errors) ->
    ( run_testcase3(Type,Testname,Typed,Errors,Test,Verdict) -> true
    ; Verdict = [verdict(Testname,*,error('run_testcase3 failed'))])
    ;
    Verdict = [verdict(Testname,*,fail('type checker failed'))])
    ;
    Verdict = [verdict(Testname,*,error('extracting tests failed'))]).

run_testcase3(typesok, Testname, Typed, Errors, Tests, Verdict) :-
    ( Errors = [] ->
    Verdict = [verdict(Testname,typecheck,pass)|Verdict1],
    run_checks(Tests,Testname,Typed,Verdict1)
    ;
    Verdict = [verdict(Testname,*,fail('unexpected errors from type-checker', Errors))]).

run_typecheck_testcase(Filename,Type) :-
    run_testcase(Filename,Filename,Type,Verdicts),
    nl,print_verdicts(Verdicts,*),
    summarized_verdict(Verdicts,V),
    !,
    (V==pass -> print('All tests passed\n') ; print('Test failed\n'),fail).

safe_pretty_type(Type,Text) :-
    (pretty_type(Type,Text) -> true ; Text = '<failed to pretty type>').

slashes_to_list(A/B,List) :-
    !,slashes_to_list(A,AList),
    slashes_to_list(B,BList),
    append(AList,BList,List).

slashes_to_list(X,[X]).

summarized_verdict(Vs,Sum) :- summarized_verdict2(Vs,pass,Sum).

summarized_verdict2([],V,V).

summarized_verdict2([verdict(_,_,V)|Rest],Old,New) :-
    (V==pass -> summarized_verdict2(Rest,Old,New) ; New=fail).