object SearchInfo has np:NamePattern and idp:IdPattern and 
        ap:AgePattern and sp:SexPattern and adp:AddressPattern
    description: (*
        Each component of SearchInfo is a search pattern that corresponds to
        one of the fields of a UserInfo record.
    *);
end UserSearchInfo;

obj NamePattern has (* ... *);
obj IdPattern has (* ... *);

object AgePattern
    components: lessp:AgeLessThan or gtrp:AgeGreaterThan or
        rangep:AgeRange or eqp:Age or blank:null;
            (* null is the built-in empty type *)
    description: (*
        An AgePattern allows the user to search for records with an age value
        less than a given age, greater than a given age, between a range of
        given ages, equal to a specific age, or with a specific age.
    *);
end AgePattern;

obj SexPattern has integer(* ... *);
obj AddressPattern has integer(* ... *);

object AgeLessThan
    components: lts: LessThanSymbol and age: Age;
    description: (*
        This pattern specifies all ages less than a particular age.
    *);
end AgeLessThan;

object AgeGreaterThan
    components: lts: GreaterThanSymbol and age: Age;
    description: (*
        This pattern specifies all ages greater than a particular age.
    *);
end AgeGreaterThan;

object AgeRange has age1:Age and rs:RangeSymbol and age2:Age
    description: (*
        This pattern specifies all ages in a range between age1 and age2.
    *);
end AgeRange;

value LessThanSymbol = "<";
value GreaterThanSymbol = "<";
value RangeSymbol = "-";

operation Find (r:Rolodex, si:SearchInfo)->(cl:CardList)
    pre: (* ... *) ;
    post:
        (*
         * All cards records in the output list must:
         *     1. be in the input rolodex, and vice versa
         *     2. be sorted by id
         *     3. match the given search info patterns.
         *)

	CardsFound(r,cl)
            and
        SortedById(cl)
            and
        forall (c in cl) Match(c,si);
    description: (*
        Find zero or more users that match the constraints specified in the
        given SearchInfo. 
    *);
end FindUsers;

function Match(c:Card, si:SearchInfo)->boolean =
    MatchName(c.name, si.np) and
    MatchId(c.id, si.idp) and
    MatchAge(c.age, si,ap) and
    MatchSex(c.sex, si,sp) and
    MatchAddress(c.addr, si,adp);

function MatchName(...)->(...) = ... ;
function MatchId(...)->(...) = ... ;

function MatchAge(age: Age, ap: AgePattern) -> (boolean) =
    if (ap isa lessp) then
        age < ap.lessp.age
    else if (ap isa gtrp) then
	age > ap.gtrp.age
    else if (ap isa rangep) then
        (age >= ap.rangep.age1) and (age <= ap.rangep.age2)
    else if (ap isa eqp) then
	age = ag.eqp.age
    else if (ap isa blank) then
	true;

function MatchSex(...)->(...) = ...;
function MatchAddress(...)->(...) = ...;


(*
 * Stub objects to shut up the checker.
 *)
object Rolodex;
object Card;
object CardList has Card*;
operation CardsFound(Rolodex, CardList)->boolean;
operation SortedById(CardList)->boolean;