1:- module(qwerty, []).    2
    3:- reexport(library(qwerty/exports)).    4
    5:- dynamic term_to_check/1.    6
    7rule_head(H :- _, Head) => Head = H.
    8rule_head(Fact,   Head) => Head = Fact.
    9
   10term_functor(Term, F) :-
   11    functor(Term, F, _).
   12
   13fst_pair(X, X-_).
   14
   15init_infers -->
   16    maplist(rule_head),
   17    maplist(term_functor),
   18    sort,
   19    maplist(fst_pair),
   20    list_to_assoc.
   21
   22unwanted_term(begin_of_file).
   23unwanted_term(:- _).
   24
   25check_and_infer(Infers, Term, Type) :-
   26    $(typecheck(Infers, Term, Type)),
   27    % Unify rule's head type with predicate's inferred type.
   28    $(rule_head(Term, Head)),
   29    $(term_functor(Head, F)),
   30    $(get_assoc(F, Infers, HeadType_)),
   31    $(rule_head(Type, HeadType)), % (:-)/2 gets skolemized so we can take its head as though it were a term.
   32    (HeadType_ = HeadType
   33    -> true
   34    ;  throw(error(ill_typed(failed_unification(HeadType_ = HeadType)), _))
   35    ).
   36
   37user:term_expansion(end_of_file, []) :-
   38    % Collect stored terms
   39    findall(Term, retract(term_to_check(Term)), Terms),
   40    init_infers(Terms, Infers),
   41    writeln('Terms:'),
   42    maplist(writeln, Terms),
   43    maplist(check_and_infer(Infers), Terms, _).
   44
   45user:term_expansion(Term, [Term]) :-
   46    \+ unwanted_term(Term),
   47    assertz(term_to_check(Term)). % Store term