(*
 * 25nov07: This was moved here from work/calendar/specifications/ideas.  It
 * has some pretty cool stuff in it, which should result in its codification
 * both in the ref man, and back in calendar/specification, the latter being as
 * a real part of the spec.
 *)

obj Duration = minutes:integer and hours:integer;

(* The maximum duration value is defined to be 1000 hours.  This sounds
   reasonable enough.   Note that the intention here is to define the max
   duration as 1000 hours total, i.e., the sum of the hours and minutes for any
   Duration is <= 1000. *)
value MAX_DURATION:Duration = {1000,0};

(* SIDE NOTE: See below about the following decl not causing an error.
     value MAX_DURATION = {1000,0}; *)

(*
 * The value range for item duration is 0 to MAX_DURATION, the latter being a
 * constant with some reasonable value.  Allowing a value of 0 means that a
 * scheduled item can be a one-shot deal, like picking someone up somewhere.
 *)
axiom DurationBounds =
    forall (d:Duration)
	d.hours >= 0 and
        d.minutes >= 0 and
        (d.hours + d.minutes) <
            MAX_DURATION.hours + MAX_DURATION.minutes;

(* FIX THIS:
            MAX_DURATION.hoursxxx + MAX_DURATION.minutes;
                              ^^^ not an error when MAX_DURATION is
   declared as value MAX_DURATION = {1000, 0};, i.e., without the
   :Duration type decl. *)

(*
   25nov07 Update to the discussion below.

   Instead of the somewhat round-about notion of having to bind a value to a
   variable at runtime, we might just say that axioms are not evaluated until
   runtime, what entities their expressions contain as operands.  Hence, it is
   not necessar to assign a BAD_DURATION (see below for def) to a var to have
   the axiom apply, but simply "wait" until runtime.  But then, obviously, we
   have to define what in fact it means to wait like this.  This leads I think
   to a (much) more general notion of when *is* runtime, compared to compile
   time?  This is in fact an important issue to be resolved fully.

   Pre-25nov07 discussion starts here.

   Very curious stuff going on here.  If we say that global axioms apply to all
   vars and vals declared of the quantified type, then we have a circularity in
   the above axiom.  It is that the axiom should apply to the declaration of
   value decl MAX_DURATION:DurationBounds, but it can't, because the decl has
   to be processed before we can type check the subexper MAX_DURATION.hours.

   Hmm, what we may have to say is that global axioms apply to all variables
   declared of a particular type, but not to values.  This seems a bit funky at
   first glance, but turns out to be OK.  Read on ... .

   The reason it's arguably OK is that we can say that the meaning of an axiom
   is a run-time thing, applying only during the execution of a program that
   implements a spec.  If this is in fact the case, then by their definition,
   axioms do not, and in the case above cannot, apply to compile-time constant
   decls.

   However, the news is not really that bad here, since the axiom will apply at
   run-time to a constant value, if it's ever bound to a variable of the
   constant's type.  So, in the above example, the following declaration

       value BAD_DURATION:Duration = {2000, 0}

   is not erroneous at compile-time.  However, the following run-time
   expression violates the axiom:

       var d:Duration = BAD_DURATION;

    So I think we're cool here, if only by dumb luck.

    And to conclude a bit further ... .  A universally-quantified axiom of the
    form

        forall (x:t) p(x)

    applies at the point of variable binding, with the appro def of fmsl
    "variable", i.e., parm, let var, declared var, tuple component, list
    component, and possibly other things that need to be fully enumerated.
*)