variables([Known,Birthday]).

def_type(bb,rel(name,date)).
def_type(kn,set(name)).

invariant(birthdayBookInv).
dec_p_type(birthdayBookInv(kn,bb)).
birthdayBookInv(Known,Birthday) :- dom(Birthday,Known).

dec_p_type(n_birthdayBookInv(kn,bb)).
n_birthdayBookInv(Known,Birthday) :- neg(dom(Birthday,Known)).

invariant(pfunInv).
dec_p_type(pfunInv(bb)).
pfunInv(Birthday) :- pfun(Birthday).

dec_p_type(n_pfunInv(bb)).
n_pfunInv(Birthday) :- neg(pfun(Birthday)).

initial(birthdayBookInit).
dec_p_type(birthdayBookInit(kn,bb)).
birthdayBookInit(Known,Birthday) :-
  Known = {} &
  Birthday = {}.

dec_p_type(addBirthdayOk(kn,bb,name,date,kn,bb)).
addBirthdayOk(Known,Birthday,Name,Date,Known_,Birthday_) :-
  Name nin Known &
  un(Known,{Name},Known_) &
  un(Birthday,{[Name,Date]},Birthday_).

dec_p_type(nameAlreadyExists(kn,name)).
nameAlreadyExists(Known,Name) :-
  Name in Known.

operation(addBirthday).
dec_p_type(addBirthday(kn,bb,name,date,kn,bb)).
addBirthday(Known,Birthday,Name,Date,Known_,Birthday_) :-
  addBirthdayOk(Known,Birthday,Name,Date,Known_,Birthday_)
  or
  nameAlreadyExists(Known,Name) & Known_ = Known & Birthday_ = Birthday.

dec_p_type(findBirthdayOk(kn,bb,name,date)).
findBirthdayOk(Known,Birthday,Name,Date) :-
  Name in Known & 
  applyTo(Birthday,Name,Date).

dec_p_type(notAFriend(kn,name)).
notAFriend(Known,Name) :-
  Name nin Known.

operation(findBirthday).
dec_p_type(findBirthday(kn,bb,name,date,kn,bb)).
findBirthday(Known,Birthday,Name,Date,Known,Birthday) :-
  findBirthdayOk(Known,Birthday,Name,Date)
  or
  notAFriend(Known,Name).

operation(remind).
dec_p_type(remind(kn,bb,date,kn,kn,bb)).
remind(Known,Birthday,Today,Cards,Known,Birthday) :-
  rres(Birthday,{Today},M) & dec(M,bb) &
  dom(M,Cards).


