(*
 * This file contains some initial investigations on what nice things can
 * happen with the rule T = {T}, for any type T.
 *
 * SUPER FLASH: where-clause instantiation must DISABLE subtype polymorphism,
 * since it fundamentally alters the subtype.  Consider the example below,
 * where IntStack < Stack.  In this case, an Instack no longer shares a rep
 * with Stack, since we've changed it with the where clause.  Looking at what
 * happens to a selector, with and without where clause, can help clarify
 * things.
 * 
 * WITH WHERE:

    obj Stack =  es:Elem*;
    obj IntStack < Stack where: Elem = IntElem end;
    op Top(ist:IntStack)->IntElem =
	ist.e[1]

 *
 * Here the type of ist.es[1] is IntElem, due to the generic instantiation.
 * I.e., the type of ist.es is now IntElem*, again, due to the generic
 * instantiation.  Further, the type of ist.es CANNOT be interpreted as Elem*
 * anymore (as it is in the parent Stack class) since this would allow Elem's
 * to mascarade as IntElem's, via a violation of subtype poly.  I.e., since
 * IntElem < Elem, we cannot bind Elem's to vars of type IntElem, and with
 * generic where-clause instantiation, ist.es is a list of such vars.  Hence,
 * the where-clause instantiation has led to a severing of the subclass
 * relationship between Stack and IntStack, as far as any subsequent type
 * checking is concerned.  Bitchin.
 *
 * WITHOUT WHERE:

    obj Stack =  es:Elem*;
    obj IntStack < Stack
    op Top(ist:IntStack)->IntElem =
	ist.es[1]?<IntElem ist.es[1].<IntElem;

 * Here, the type of ist.es[1] is Elem, which cannot be returned as type
 * IntElem with a safe extraction using the check and get instance ops.
 *)



obj Elem;
obj Stack =  e:Elem*;

(*
 * obj IntStack < Stack
 *     where: Elem = IntElem;
 * end;
 *
 * Next def replaces preceding to give semantics of not-yet-implemented generic
 * instantiation.
 *)
obj IntStack =  e:IntElem* and;


obj IntElem < Elem =  integer
    description: (*
	To get a generic instantion of an integer stack, we might be tempted to
	say

	    obj integer < Elem;

	which, as we know, we cannot do, if for no other reason than it over
	defines integer.  But, with our nice new T = {T} rule, we can get the
	effect that we'd like to a large extent with this def, since we'll get
	stacks that look like they have plain ints on them.  See usage examples
	below.
    *);
end;

obj StrStack < Stack
    where: Elem = StrElem;
end;
obj StrElem < Elem =  string;


op Push(Stack,Elem)->Stack;
op Push(IntStack,IntElem)->IntStack;
    (* This op should be automatically def'd by generic instantiation. *)
op Push(StrStack,StrElem)->IntStack;	(* Ibid re. auto def. *)
op Pop(Stack)->Elem;
op Pop(ist:IntStack)->IntElem =		(* Ibid. *)
   ist.e[1];				(*   (Imple obviously not auto) *)
op Pop(StrStack)->StrElem;		(* Ibid. *)


op main(s:Stack,ist:IntStack,i:integer,ie:IntElem,se:StrElem) = (
    Push(ist,i);	(* Works by T = {T} rule. *)
    Push(ist,10);	(* Ibid. *)
    Push(s,ie);		(* Works, since IntElem < Elem *)
    Push(s, i);		(* ERROR, since int !< Elem, and T={T} cant help *)
    Push(ist,se)	(* ERROR, per new superflash rule. *)
			(* Same as next line before constructor ops work *)
--    Push(ist,StrElem("abc"))(* Potentially problematic; see discussion below.*)
);



(*
 * The superflash above effectively trashes the entire discussion that follows
 * (starting in the next comment block).  We'll leave the discussion for
 * posterity.  With the new rule that generic instantiations are not subtypes,
 * the potentially problematic line just above, viz.  Push(ist,StrElem("abc")),
 * will no longer type check.  The reason it type checks without this new rule
 * is that IntStack is still < Stack, so that when the resolution to
 * Push_IntStack_IntElem fails, we can look at Push_Stack_Elem, via subtype
 * poly.  HOWEVER, the new rule says that subtype poly is out now.  Hence,
 * since there is no explicit def of Push(IntStack, StrElem) or Push(IntStack,
 * Elem), there can be no resolution of the problematic call.  Bitchin again.
 *
 * One way to look at the new rule (gen instantiations are not subtypes) is
 * that it implements automatically, and in the right places, the notion of
 * strict inheritance introduced below, but below required invention of a new
 * operator.  Can I have one more bitchin, please?
 *)


(*
 *
 * TRASHED DISCUSSION FOLLOWS.
 *
 * Here's an interesting position we might be finding ourselves in.  If both
 * int and string are subtypes of Elem, then we get in the situation where the
 * following might be type safe, even though we dont want it to be:
 *
 *     Push(IntStack(nil), "abc")
 *
 * The reason it might be type safe is as follows: since IntStack<Stack, the
 * preceding call could resolve to Push_Stack_Elem, after it fails to resolve
 * to Push_IntStack_IntElem.  We're saved here, since "abc" is a string lit
 * that wont bind directly to an Elem, so we can't reslove to Push_Stack_Elem.
 *
 * However, consider
 *
 *     Push(IntStack(nil), StrElem("abc"))
 *
 * Here, since StrElem<Elem, StrElem("abc") will bind to Elem.  So, when this
 * call fails to resolve to Push_IntStack_IntElem, it can now safely resolve to
 * Push_Stack_Elem.  The result is that we get a StrElem pushed onto an
 * IntStack, which may not be what we want if we had a homogeneous IntStack in
 * mind.
 *
 * So, the $64K question here is, can we get a truely homogeneous IntStack at
 * all in RSL, without having to hand duplicate all of the ops?  I.e., we want
 * to use inheritance-based generic instantiaion, but still get a homogeneous
 * IntStack.  The answer seems to be no in 3.1.
 *
 * One thing we might say is that we really don't care about this seemingly
 * unwanted heterogeneity, since we couldn't ever get strings directly off of
 * an IntStack, even though we could put them there.  This is because the only
 * non-generic selector we have for an IntStack returns an int, not a string.
 * Reasoning things out, consider the following example:
 *)

op main(s:Stack,ist:IntStack,ss:StrStack,i:integer,ie:IntElem,str:string) = (
    str = Pop(ss);
    i = Pop(ist);
    str = Pop(ist)	(* ERROR, since there's no Pop_IntStack->StrElem *)
);


(*
 * But, if we really want to solve the problem "properly", it's on to 4.0, in
 * which, among other things, we'll have the notion of strict inheritance, with
 * a new symbol to boot.  Here's the deal ... .  Normally, if T1 < T2, then
 * values of type T1 can be bound to vars of T2, but not vice versa (of
 * course).  With strict inheritance, which we'll denote T1 <!= T2 (verbosely
 * "T1 strict extends T2", where, we hope, the symbol '<!=' has the
 * mnemonic suggestion of "less than but not equal to"), the normal rule of
 * subtype binding does not apply.  Viz., if T1 <!= T2, values of type T1
 * canNOT be bound to vars of type T2.
 *
 * This acutally seems pretty cute, and even orthogonal  It will solve the
 * IntStack homogeneity problem (example below).  It would be nice if we could
 * find some other useful example(s) where it was helpful as well.
 *
 * What we should do here to cap off this disucssion, in addition to finding
 * some additional useful examples for strict inheritance, with a discussion of
 * why this particular problem seems not to show up in C++, at least not in
 * exactly the same way.  One reason is probably because ops *belong to*
 * objects, and all that biz.  Also, templates will figure in, since we're
 * talking about that kind of generics here.
 *)

(*
 * obj StrictlyIntStack < Stack
 *     where: Elem = IntElem;
 * end;
 *
 * Next def replaces preceding to give semantics of not-yet-implemented generic
 * instantiation.
 *)
obj StrictlyIntStack =  e:IntElem* and;

op Push(StrictlyIntStack,IntElem)->StrictlyIntStack;
    (* This op should be automatically def'd by generic instantiation. *)

op main1(s:Stack,ist:StrictlyIntStack,i:integer,ie:IntElem,se:StrElem) = (
    Push(ist,i);
    Push(s,ie);
    Push(ist,10);
    Push(ist,se)	(* Should be ERROR because of strict inheritance. *)
);