% type(+Kontext,+Term,-Typ)

type([(V,Ty)|Kontext],X,Typ) :-
    (var(X) ; number(X)), !,
    ( X == V -> Typ = Ty ; type(Kontext,X,Typ) ).
type([],N,Typ) :-
    number(N), !, Typ = n.
type(Kontext,(R * S),Typ) :-
    !, type(Kontext,S,Arg),
    type(Kontext,R,(ArgT -> Typ)),
    datenbank:subtype(Arg,ArgT).
type(Kontext,lam(X,Term),Typ) :-
    !, type([(X,Ty)|Kontext],Term,Val),
    Typ = (Ty -> Val).
type(Kontext,ex(X,Term),t) :-
    !, type(Kontext,lam(X,Term),(_Ty -> t)).
type(Kontext,all(X,Term),t) :-
    !, type(Kontext,lam(X,Term),(_Ty -> t)).
type(Kontext,qu(X,Term),t) :-
    !, type(Kontext,lam(X,Term),(_Ty -> t)).
type(Kontext,anzahl(X,Fml,N),t) :-
    !, type(Kontext,lam(X,Fml),_Ty->t),
    type(Kontext,N,n).
type(Kontext,neg(Fml),t) :-
    !, type(Kontext,Fml,t).
type(Kontext,(Fml1 & Fml2),t) :-
    !, type(Kontext,Fml1,t),
    type(Kontext,Fml2,t). 
type(Kontext,(Fml1 \/ Fml2),t) :-
    !, type(Kontext,(Fml1 & Fml2),t).
type(Kontext,(Fml1 => Fml2),t) :-
    !, type(Kontext,(Fml1 & Fml2),t).
type(Kontext,(Fml1 <=> Fml2),t) :-
    !, type(Kontext,(Fml1 & Fml2),t).
type(_Kontext,_Modul:_Term,Typ) :-
    !, Typ = t.
type(Kontext,Term,Typ) :-
    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',[TypF]),
           fail
       )
    ; format('\ndatenbank:~w hat keinen Typ',[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).

% typisiere(+Kontext,+Formel,-Getypte Formel).

typisiere(Env,lam(X,F),lam(X:Typ,T)) :-
   !,type(Env,lam(X,F),(Typ -> _)),
   typisiere([(X,Typ)|Env],F,T).
typisiere(Env,ex(X,F),ex(X:Typ,T)) :-
   !,type(Env,lam(X,F),(Typ -> t)),
   typisiere([(X,Typ)|Env],F,T).
typisiere(Env,all(X,F),all(X:Typ,T)) :-
   !,typisiere(Env,ex(X,F),ex(X:Typ,T)).
typisiere(Env,qu(X,F),qu(X:Typ,T)) :-
   !,typisiere(Env,ex(X,F),ex(X:Typ,T)).
typisiere(Env,anzahl(X,F,N),anzahl(X:Typ,T,N)) :-
   !,typisiere(Env,ex(X,F),ex(X:Typ,T)).

typisiere(Env,(F1 & F2), (T1 & T2)) :-
   !,typisiere(Env,F1,T1),
   typisiere(Env,F2,T2).
typisiere(Env,(F1 \/ F2), (T1 \/ T2)) :-
   !,typisiere(Env,(F1 & F2), (T1 & T2)).
typisiere(Env,(F1 => F2), (T1 => T2)) :-
   !,typisiere(Env,(F1 & F2), (T1 & T2)).
typisiere(Env,(F1 <=> F2), (T1 <=> T2)) :-
   !,typisiere(Env,(F1 & F2), (T1 & T2)).
typisiere(Env,neg(F), neg(T)) :-
   !,typisiere(Env,F,T).

typisiere(Env,Term,Term) :-
   type(Env,Term,_Typ).