typechecker

assert_type_error :-
    retract(type_error(_N)),fail.

assert_type_error :-
    assertz(type_error(yes)).

assert_user_type(Type,Def) :-
    %print_message(add_type(Type,Def)),
    translate_type_def(Def,TranslatedDef,Type),!,
    (user_defined_type(Type,OldDef)
    -> (OldDef = TranslatedDef -> true
    ; print_error('### Type Clash for: '), print_error(Type),
    print_error(OldDef), print_error(TranslatedDef)
    )
    ; (predefined_type(Type)
    -> print_error('### Trying to redefine built-in type: '), print_error(Type)
    ; assertz(user_defined_type(Type,TranslatedDef))
)
).

assert_user_type(Type,Def) :-
    print_error('### Could not translate type description for type:'),
    print_error(Type), print_error(Def).

check_cyclic(X) :- cyclic_term(X),!,
    print('### Cyclic Term : '), nl,
    safe_print_term(X),nl,
    fail.

check_cyclic(_).

check_types :- % print('% Checking user defined types: '),
    user_defined_type(Type,Descr),
    (legal_type_description(Descr) -> true %,(print(Type),print(' '))
    ; print_error('### Error in type definition:'), print_error(Type),
    print_error(Descr)),
    fail.

check_types :- % print('% Checking user defined types: '),
    user_defined_type(Type,Descr), user_defined_type(Type,Descr2),
    Descr \= Descr2,
    print_error('### Multiple Definitions for type:'), print_error(Type),
    fail.

check_types. % :- nl.

debug_non_ground_term(X) :- var(X),!, print('-> top level is variable: '), print(X),nl.

debug_non_ground_term(X) :- debug_non_ground_term(X,[]).

debug_non_ground_term(X,_) :- ground(X),!.

debug_non_ground_term(X,T) :- X =.. [Fun|Args], l_debug_ng(Args,[Fun|T],1).

ground_check(X) :- (ground(X) -> true ;
    print_error('### Not ground: '), print_error(X),nl,debug_non_ground_term(X),fail).

is_inf(X) :- cyclic_term(X).

l_debug_ng([],_,_).

l_debug_ng([H|T],Hist,NrOfArg) :-
    (var(H) -> print('--> Arg #'), print(NrOfArg), print(' of '), print(Hist),nl ; debug_non_ground_term(H,Hist)),
    A1 is NrOfArg+1,
    l_debug_ng(T,Hist,A1).

l_legal_type_description([]).

l_legal_type_description([Type1|Rest]) :-
    legal_type_description(Type1),
    l_legal_type_description(Rest).

l_safe_print([]).

l_safe_print([Term|T]) :-
    (is_inf(Term)
    -> (print('!CYCLIC!('),write_term(Term,[max_depth(3)]),print(')'))
    ; (print(Term))
    ),
    (T=[] -> true ; print(',') ),
    l_safe_print(T).

l_term_is_of_type([],[],_PrintErrMsg).

l_term_is_of_type([Term1|Rest],[Type1|TypeList],PrintErrMsg) :-
    term_is_of_type(Term1,Type1,PrintErrMsg),!,
    l_term_is_of_type(Rest,TypeList,PrintErrMsg).

l_translate_type_def([],[],_Cur).

l_translate_type_def([A|T],[AT|TT],Cur) :-
    translate_type_def(A,AT,Cur), l_translate_type_def(T,TT,Cur).

legal_type_description(X) :- var(X),!,fail.

legal_type_description(any) :- !.

legal_type_description(ground) :- !.

legal_type_description(nonground) :- !.

legal_type_description(var) :- !.

legal_type_description(nonvar) :- !.

legal_type_description(integer) :- !.

legal_type_description(float) :- !.

legal_type_description(number) :- !.

legal_type_description(atom) :- !.

legal_type_description(atomic) :- !.

legal_type_description(compound) :- !.

legal_type_description(simple) :- !.

legal_type_description(mutable) :- !.

legal_type_description(ask(_Type)) :- !.

legal_type_description(call(Call)) :- Call=Module:Pred,atomic(Module),atomic(Pred),!.

legal_type_description(list(Type)) :- !,
    legal_type_description(Type).

legal_type_description(vlist(Type)) :- !,
    legal_type_description(Type).

legal_type_description(term(Functor,TypeList)) :- !,
    (length(TypeList,Arity),functor(T,Functor,Arity),
    user_defined_type(T,_)
    -> print_message(informational,'*** Warning: term also exists as type:'), print_message(informational,T)
    ; true
    ),
    l_legal_type_description(TypeList).

legal_type_description(vterm(_Functor,TypeList)) :- !,
    l_legal_type_description(TypeList).

legal_type_description((Type1 ; Type2)) :- !,
    legal_type_description(Type1),!,legal_type_description(Type2).

legal_type_description(Type) :-
    \+(predefined_type(Type)),
    user_defined_type(Type,_Descr),!.

legal_type_description(type(Type)) :- !,print_error('### Illegal type descriptor: '),
    print('### type/1 can only be used in type definitions'),
    print_error(Type),fail.

legal_type_description(Type) :- print_error('### Illegal type descriptor: '),
    print_error(Type),fail.

predefined_type(any).

predefined_type(ground).

predefined_type(nonground).

predefined_type(var).

predefined_type(nonvar).

predefined_type(integer).

predefined_type(float).

predefined_type(number).

predefined_type(atom).

predefined_type(atomic).

predefined_type(simple).

predefined_type(compound).

predefined_type(mutable).

predefined_type(list(_X)).

predefined_type(term(_F,_TL)).

predefined_type(vlist(_X)).

predefined_type(vterm(_F,_TL)).

predefined_type(ask(_T)).

predefined_type(call(_)).

print_inf_error(Term,Type,PrintErrMsg) :- PrintErrMsg \= no, nl,
    print_error('### Cyclic Term Error: Requested Type '),print_error(Type),
    print_error('### Term: '),safe_print_term(Term),nl,
    assert_type_error.

print_type_error(T,Type,_,PP) :-
    (legal_type_description(Type) -> true
    ; print_error(pp(PP)),print_error(illegal_type(Type)),print_error(term(T))),
    fail.

print_type_error(Term,Type,PrintErrMsg,PP) :- PrintErrMsg\=no, nl,
    %print(err(Term,Type)),nl,nl,
    print_error('### Type Error Occured! Type:'),print_error(Type),
    print_error('### Term:'),safe_print_term(Term),nl,
    print_error('### ProgramPoint:'),safe_print_term(PP),nl,
    assert_type_error.

print_types :- print_message(informational,'---------'),user_defined_type(Type,Descr),
    print_message(informational,type(Type,Descr)),fail.

print_types :- print_message(informational,'---------').

reset_type_error :-
    retract(type_error(_N)),fail.

reset_type_error :-
    assertz(type_error(no)).

safe_print_term(X) :- var(X),!,print(X).

safe_print_term(X) :- is_inf(X),!,
    X =.. [Func|Args],
    print(Func),print('('),
    l_safe_print(Args),
    print(')').

safe_print_term(X) :- print(X).

term_is_of_type(Term,Descr,PrintErrMsg) :-
    is_inf(Term),!,
    print_inf_error(Term,Descr,PrintErrMsg). %read(_Cont).

term_is_of_type(_Term,any,_PrintErrMsg) :-
    !. /* anything is of type any */

term_is_of_type(Term,ground,_PrintErrMsg) :-
    ground(Term),!.

term_is_of_type(Term,nonground,_PrintErrMsg) :-
    \+(ground(Term)),!.

term_is_of_type(Term,var,_PrintErrMsg) :-
    var(Term),!.

term_is_of_type(Term,nonvar,_PrintErrMsg) :-
    nonvar(Term),!.

term_is_of_type(Term,integer,_PrintErrMsg) :-
    integer(Term),!.

term_is_of_type(Term,float,_PrintErrMsg) :-
    float(Term),!.

term_is_of_type(Term,number,_PrintErrMsg) :-
    number(Term),!.

term_is_of_type(Term,atom,_PrintErrMsg) :-
    atom(Term),!.

term_is_of_type(Term,atomic,_PrintErrMsg) :-
    atomic(Term),!.

term_is_of_type(Term,compound,_PrintErrMsg) :-
    compound(Term),!.

term_is_of_type(Term,simple,_PrintErrMsg) :-
    \+ compound(Term),!.

term_is_of_type(Term,mutable,_PrintErrMsg) :-
    mutable(Term),!.

term_is_of_type(Term,ask(Type),_PrintErrMsg) :-
    !,
    print('Type => '),print(Type),nl,
    print('Term => '),print(Term),nl,
    print('(y or n) =>'),read(UserChoice),
    UserChoice=y.

term_is_of_type(Term,call(Module:Predicate),_PrintErrMsg) :-
    functor(Call,Predicate,1),
    arg(1,Call,Term),
    call(Module:Call).

term_is_of_type(Term,list(Type),PrintErrMsg) :-
    var(Term),!,
    print_type_error(Term,list(Type),PrintErrMsg,term_is_of_type).

term_is_of_type([],list(_Type),_PrintErrMsg) :- !.

term_is_of_type([Head|Tail],list(Type),PrintErrMsg) :-
    term_is_of_type(Head,Type,PrintErrMsg),!,
    term_is_of_type(Tail,list(Type),yes).

term_is_of_type(Term,vlist(_Type),_PrintErrMsg) :-
    var(Term),!. /* also to avoid modifying Term in the next 2 clauses */

term_is_of_type([],vlist(_Type),_PrintErrMsg) :- !.

term_is_of_type([Head|Tail],vlist(Type),PrintErrMsg) :-
    term_is_of_type(Head,Type,PrintErrMsg),!,
    term_is_of_type(Tail,vlist(Type),yes).

term_is_of_type(Term,term(Functor,ArgTypeList),PrintErrMsg) :-
    var(Term),!,
    print_type_error(Term,term(Functor,ArgTypeList),PrintErrMsg,term_is_of_type_var).

term_is_of_type(Term,term(Functor,ArgTypeList),_PrintErrMsg) :-
    Term =.. [Functor|Args],!,
    l_term_is_of_type(Args,ArgTypeList,yes), !.

term_is_of_type(Term,vterm(_Functor,_ArgTypeList),_PrintErrMsg) :-
    var(Term),!. /* also to avoid modifying Term in the next clause */

term_is_of_type(Term,vterm(Functor,ArgTypeList),_PrintErrMsg) :-
    Term =.. [Functor|Args],!,
    l_term_is_of_type(Args,ArgTypeList,yes), !.

term_is_of_type(Term,Type,PrintErrMsg) :-
    \+(predefined_type(Type)),
    user_defined_type(Type,Descr), /* user defined type; we assume single definition exists */
    !,
    term_is_of_type(Term,Descr,PrintErrMsg).

term_is_of_type(Term,(Type1 ; Type2),PrintErrMsg) :-
    (term_is_of_type(Term,Type1,no) -> true
    ; term_is_of_type(Term,Type2,PrintErrMsg)),
    !.

term_is_of_type(Term,Type,PrintErrMsg) :-
    print_type_error(Term,Type,PrintErrMsg,term_is_of_type_catchall).

translate_type_def(X,any,_) :- var(X),!,print_error('### Variable Type !').

translate_type_def(call(Module:Call),call(Module:Call),_) :- !.

translate_type_def(type(X),X,_) :- !.

translate_type_def(list(X),list(TX),Cur) :- !, translate_type_def(X,TX,Cur).

translate_type_def(vlist(X),vlist(TX),Cur) :- !, translate_type_def(X,TX,Cur).

translate_type_def((X;Y),(TX;TY),Cur) :- !,
    translate_type_def(X,TX,Cur), translate_type_def(Y,TY,Cur).

translate_type_def(term(F,A),term(F,TA),Cur) :- !, l_translate_type_def(A,TA,Cur).

translate_type_def(vterm(F,A),vterm(F,TA),Cur) :- !, l_translate_type_def(A,TA,Cur).

translate_type_def(X,X,CurType) :- (predefined_type(X) ; user_defined_type(X,_) ; X=CurType),!.

translate_type_def(X,term(Fun,TArgs),Cur) :- nonvar(X), X =.. [Fun|Args], !,
    l_translate_type_def(Args,TArgs,Cur).

translate_type_def(X,X,_) :-
    print_message(informational,'*** Forward type reference'), print_message(informational,X).

type(Type +--> Def) :- assert_user_type(Type,Def),!.

type(Type = Def) :- assert_user_type(Type,Def),!.

type(TD) :- print_error('### Illegal Type Declaration: '), print_error(TD),nl.

type_check(Term,Type) :- %print_message(type_check(Term,Type)),
    reset_type_error,
    (term_is_of_type(Term,Type,yes)
    -> \+(type_error_occurred)
    ; \+(type_error_occurred), print_type_error(Term,Type,yes,type_check),fail).

type_error(no).

type_error_occurred :-
    type_error(yes).