/*
// AlgoDat II, Aufgabe 44
// Christian Semrau

Type Datum

Functions:
  mk_date: INT x INT x INT --> Datum   Konstruktor
  tag: Datum --> INT                   Selektor
  monat: Datum --> INT                 Selektor
  jahr: Datum --> INT                  Selektor
  is_before: Datum x Datum --> BOOL    Praedikat
  equal: Datum x Datum --> BOOL        Praedikat
  next: Datum --> Datum
  previous: Datum --> Datum
  plus: Datum x INT --> Datum
  // positiv = Zukunft, negativ = Vergangenheit
  between: Datum x Datum --> INT
  // Tage zwischen erstem und zweitem Datum

Axioms: forall d,e, f: Datum, t, m, j, n:INT
  tag(mk_date(t,m,j)) = t
  monat(mk_date(t,m,j)) = m
  jahr(mk_date(t,m,j)) = j

  next(mk_date(t,m,j)) =
    if t<30 then mk_date(t+1,m,j) else
    if m<12 then mk_date(1,m+1,j) else
    mk_date(1,1,j+1)
  previous(next(d)) = d
  // previous wird ueber next definiert

  plus(d, 0) = d
  plus(d, n) = plus(next(d), n-1)
  // wollen wir die Regel anwenden, muessen wir bei positivem n nach
  // rechts gehen und bei negativem n nach links, damit n sich der 0
  // naehert

  (between(d, e) = n) <-> (plus(d, n) = e)
  // between liefert das n, fuer das d+n = e

  equal(d, e) <-> (tag(d) = tag(e)) AND (monat(d) = monat(e) AND (jahr(d) = jahr(e))
  // zwei Daten sind gleich, wenn sie in allen Komponenten uebereinstimmen

  (d = e) <-> equal(d, e)
  // Operator =: Datum x Datum --> BOOL, vereinfacht mir die Schreibung der
  // Axiome, denn ich wuesste jetzt nicht, wie der "="-Operator
  // standardmaessig fuer neue Datentypen definiert ist

Preconditions: forall t,m,j:INT
  pre(mk_date(t,m,j)): t>=1 AND t<=30 AND m>=1 AND m<=12
*/

/**
 * AlgoDat II, Aufgabe 44
 * 
 * @author Christian Semrau
 * Christian.Semrau@student.uni-magdeburg.de
 */
class Datum {
  int t, m, j;
  private Datum(int t,int m,int j) { this.t=t; this.m=m; this.j=j; }  
  public static int between(Datum d1,Datum d2) {
    return (d2.j-d1.j)*360+(d2.m-d1.m)*30+(d2.t-d1.t); }
  public static boolean equal (Datum d1,Datum d2) {
    return d1.t==d2.t && d1.m==d2.m && d1.j==d2.j; }
  public static boolean is_before (Datum d1,Datum d2) {
    return between(d1,d2)<0;
  }  
  public static int jahr(Datum d) { return d.j; }  
  // Testmethode
  public static void main(String args[]) {
    Datum d4;
    System.out.println("between(1.1.2000, 1.1.2001) = "+
        between(mk_date(1,1,2000),mk_date(1,1,2001)));
    d4=plus(50,mk_date(1,1,2000));
    System.out.println("1.1.2000 + 50 Tage = "+d4);
    System.out.println("between(1.1.2000, "+d4+") = "+
        between(mk_date(1,1,2000),d4));
    System.out.println(d4+" - 20 Tage = "+plus(-20,d4));
    System.out.println("30.2.1999 == 1.3.1999 = "+
        equal(mk_date(30,2,1999), mk_date(1,3,1999)));
    System.out.println("28.2.1998 + 1 = "+next(mk_date(28,2,1998)));
    System.out.println("1.1.2001 - 1 ="+previous(mk_date(1,1,2001)));
    System.out.println("16.4.2000 < "+d4+" = "+
        is_before(mk_date(16,4,2000), d4));
  }  
  public static Datum mk_date(int t,int m,int j) {
    if (t<1 || t>30 || m<1 || m>30)
        throw new IllegalArgumentException(t+"."+m+"."+j);
    return new Datum(t,m,j);
  }  
  public static int monat(Datum d) { return d.m; }  
  public static Datum next(Datum d) {
    if (d.t<30) return mk_date(d.t+1,d.m,d.j);
    if (d.t==30 && d.m<12) return mk_date(1,d.m+1,d.j);   
    else return mk_date(1,1,d.j+1);
  }  
  public static Datum plus (int n,Datum d) {
    if (n==0) return d;
    int t = d.t + n, m = d.m, j = d.j;
    if (n>0) {
        m += (t-1)/30; t = (t-1)%30+1;  j += (m-1)/12; m = (m-1)%12+1;
    }else{
        while (t<1){ t += 30; m -= 1; }  while (m<1){ m += 12; j -= 1; }       
    }
    return mk_date(t,m,j);
  }  
  public static Datum previous(Datum d) {
    if (d.t>1) return mk_date(d.t-1,d.m,d.j);
    if (d.t==1 && d.m>1) return mk_date(30,d.m-1,d.j);   
    else return mk_date(30,12,d.j-1);
  }  
  public static int tag(Datum d) { return d.t; }  
  public String toString() { return (t+"."+ m +"."+ j); }  
}