% type(+Kontext,+LamTerm,-LamTermGetypt,-Typ)

type([(V,Ty)|Kontext],X,X,Typ) :-
    (var(X) ; number(X)), !,
    ( X == V -> Typ = Ty ; type(Kontext,X,X,Typ) ).
type([],X,_,_) :-
    var(X), !, fail.
type([],N,N,Typ) :-
    number(N), !, Typ = n.
type(Kontext,(R * S),(RTy * STy),Typ) :-
    !, type(Kontext,S,STy,Arg),
    type(Kontext,R,RTy,(ArgT -> Typ)),
    datenbank:subtype(Arg,ArgT).
type(Kontext,lam(X,Term),lam(X:Ty,TermTy),Typ) :-
    !, type([(X,Ty)|Kontext],Term,TermTy,ResultTy),
    Typ = (Ty -> ResultTy).
type(Kontext,neg(Fml),neg(FmlTy),t) :-
    !, type(Kontext,Fml,FmlTy,t).
type(Kontext,(Fml1 & Fml2),(Fml1Ty & Fml2Ty),t) :-
    !, type(Kontext,Fml1,Fml1Ty,t),
    type(Kontext,Fml2,Fml2Ty,t). 
type(Kontext,(Fml1 \/ Fml2),(Fml1Ty \/ Fml2Ty),t) :-
    !, type(Kontext,Fml1,Fml1Ty,t),
    type(Kontext,Fml2,Fml2Ty,t). 
type(Kontext,(Fml1 => Fml2),(Fml1Ty => Fml2Ty),t) :-
    !, type(Kontext,Fml1,Fml1Ty,t),
    type(Kontext,Fml2,Fml2Ty,t). 
type(Kontext,(Fml1 <=> Fml2),(Fml1Ty <=> Fml2Ty),t) :-
    !, type(Kontext,Fml1,Fml1Ty,t),
    type(Kontext,Fml2,Fml2Ty,t). 
type(Kontext,ex(X,Term),ex(X:Ty,TermTy),t) :-
    !, type(Kontext,lam(X,Term),lam(X:Ty,TermTy),(Ty -> t)).
type(Kontext,all(X,Term),all(X:Ty,TermTy),t) :-
    !, type(Kontext,lam(X,Term),lam(X:Ty,TermTy),(Ty -> t)).
type(Kontext,anzahl(X,Fml,N),anzahl(X:Ty,FmlTy,NTy),t) :-
    !, type(Kontext,lam(X,Fml),lam(X:Ty,FmlTy),(Ty -> t)),
    type(Kontext,N,NTy,n).
type(Kontext,qu(X,Term),qu(X:Ty,TermTy),list(Ty)) :- 
    !, type(Kontext,lam(X,Term),lam(X:Ty,TermTy),(Ty -> t)).
type(_Kontext,Modul:Term,Modul:Term,Typ) :- 
    !, Typ = t.
type(Kontext,Term,Term,Typ) :- % TermTy=Term ??
    Term =.. [F|Args],
    types(Kontext,Args,[],Typen),
    ( Typen = [], TypF = Typ
    ; Typen = [T], TypF = (T -> Typ)
    ; Typen = [T1,T2], TypF = (T1*T2 -> Typ)
    ; Typen = [T1,T2,T3], TypF = (T1*T2*T3 -> Typ)
    ),
    functor(Term,F,Arity),
    (datenbank:type(F/Arity,TypDec)
    -> (datenbank:subtype(TypDec,TypF)
       -> true
       ; format('Typfehler: datenbank:~w hat Typ ~w',[F/Arity,TypDec]),
           format('\n           Kontext erwartet Typ ~w\n',[TypF]),
           fail
       )
    ; format('\ndatenbank:~w hat keinen Typ\n',[F/Arity]),
        fail).

types(Kontext,[A|Args],Acc,TypArgs) :-
    type(Kontext,A,_,TypA),
    types(Kontext,Args,[TypA|Acc],TypArgs).
types(_Kontext,[],Typen,TypArgs) :-
    reverse(Typen,TypArgs).