DIRECTORY
BigCardinals USING [BigFromSmall, BigSubtract, FirstOneBit],
BigIntegers USING [Abs, BigINT, RopeFromBig, Sgn],
IO USING [PutFR, rope],
SaffronATDef USING [ExpNode],
SaffronBaseDef USING [ChangeType, CompilerStateNode, ContextTreeNode, FieldListNode, LocalContextNode, MakeTrash, RetrieveIntegerValue, RopeFromValue, Static, Type, ValueNode],
SaffronContextPrivateTypes USING [AtomTGN, ElementTGNBody, IntegerElementType, NamedTGN, RealTGN, TypeGraphNodeNodeBody],
SaffronErrorHandling USING [Error, InternalError];

SaffronTypeConformanceImpl: CEDAR PROGRAM
IMPORTS BigCardinals, BigIntegers, IO, SaffronBaseDef, SaffronErrorHandling
EXPORTS SaffronATDef, SaffronBaseDef
~ BEGIN

OPEN BD: SaffronBaseDef, PT: SaffronContextPrivateTypes;

BigINT: TYPE ~ BigIntegers.BigINT;

TypeGraphNodeNode: TYPE ~ REF TypeGraphNodeNodeBody;
TypeGraphNodeNodeBody: PUBLIC TYPE ~ PT.TypeGraphNodeNodeBody;
CompileAndTypeCheckExpression: PUBLIC PROC[exp: SaffronATDef.ExpNode, ct: BD.ContextTreeNode, cs: BD.CompilerStateNode, targetType: TypeGraphNodeNode] RETURNS[BD.ValueNode, BD.ContextTreeNode] ~ BEGIN
i: BD.ValueNode;
iType: TypeGraphNodeNode;
ctr: BD.ContextTreeNode;
conform: BOOLEAN;
conversionProc: ConversionProc;
[i, ctr] _ exp.procs.CompileExpression[exp, ct, cs, targetType];
iType _ BD.Type[i];
[conform, conversionProc] _ Conform[iType, targetType];
IF NOT conform THEN {
SIGNAL SaffronErrorHandling.Error[0,
IO.PutFR["%g has incorrect type (expected %g).",
IO.rope[BD.RopeFromValue[i]],
IO.rope["<type>"]]];
RETURN[BD.MakeTrash[targetType], ctr];
};
i _ conversionProc[i, targetType];
IF TRUE THEN i _ RangeCheck[i, targetType]; -- should test range-check flag in cs
RETURN[i, ctr];
END;

EvaluateAndTypeCheckExpression: PUBLIC PROC[exp: SaffronATDef.ExpNode, lc: BD.LocalContextNode, fl: BD.FieldListNode, cs: BD.CompilerStateNode, targetType: TypeGraphNodeNode] RETURNS[BD.ValueNode] ~ BEGIN
i: BD.ValueNode;
iType: TypeGraphNodeNode;
conform: BOOLEAN;
conversionProc: ConversionProc;
i _ exp.procs.EvaluateExpression[exp, lc, fl, cs, targetType];
iType _ BD.Type[i];
[conform, conversionProc] _ Conform[iType, targetType];
IF NOT conform THEN {
SIGNAL SaffronErrorHandling.Error[0,
IO.PutFR["%g has incorrect type (expected %g).",
IO.rope[BD.RopeFromValue[i]],
IO.rope["<type>"]]];
RETURN[BD.MakeTrash[targetType]];
};
i _ conversionProc[i, targetType];
IF TRUE THEN i _ RangeCheck[i, targetType]; -- should test range-check flag in cs
RETURN[i];
END;


DemandNumber: PUBLIC PROC[i: BD.ValueNode] RETURNS[BD.ValueNode] ~ BEGIN
type: TypeGraphNodeNode _ BD.Type[i];
WHILE ISTYPE[type.body, PT.NamedTGN] DO
type _ NARROW[type.body, PT.NamedTGN].type;
ENDLOOP; -- ugghh
IF ISTYPE[type.body, REF integer base PT.ElementTGNBody] 
OR ISTYPE[type.body, REF integer base PT.ElementTGNBody]
THEN RETURN[i]
ELSE {
SIGNAL SaffronErrorHandling.Error[0,
IO.PutFR["%g has incorrect type (expected a number).",
IO.rope[BD.RopeFromValue[i]]]];
RETURN[BD.MakeTrash[NIL]];
};
END;

ConformsToInteger: PUBLIC PROC[i: TypeGraphNodeNode] RETURNS[BOOLEAN] ~ BEGIN
RETURN[TRUE];
END;

DemandBoolean: PUBLIC PROC[i: BD.ValueNode] RETURNS[BD.ValueNode] ~ BEGIN
type: TypeGraphNodeNode _ BD.Type[i];
WHILE ISTYPE[type.body, PT.NamedTGN] DO
type _ NARROW[type.body, PT.NamedTGN].type;
ENDLOOP; -- ugghh
IF ISTYPE[type.body, REF boolean base PT.ElementTGNBody]
THEN RETURN[i]
ELSE {
SIGNAL SaffronErrorHandling.Error[0,
IO.PutFR["%g has incorrect type (expected a boolean value).",
IO.rope[BD.RopeFromValue[i]]]];
RETURN[BD.MakeTrash[NIL]];
};
END;
Equivalent: PROC [t1, t2: TypeGraphNodeNode] RETURNS [BOOLEAN] ~ BEGIN
WHILE ISTYPE[t1.body, PT.NamedTGN] DO
t1 _ NARROW[t1.body, PT.NamedTGN].type;
ENDLOOP;
WHILE ISTYPE[t2.body, PT.NamedTGN] DO
t2 _ NARROW[t2.body, PT.NamedTGN].type;
ENDLOOP;
RETURN [
WITH t1.body SELECT FROM
u: PT.AtomTGN	=> EquivalentAtomBaseType[u, t2],
u: REF boolean base PT.ElementTGNBody	=> EquivalentBooleanBaseType[u, t2],
u: REF integer base PT.ElementTGNBody	=> EquivalentIntegerBaseType[u, t2],
ENDCASE =>
ERROR SaffronErrorHandling.InternalError["Unrecognized type passed as first argument to SaffronTypeConformanceImpl.Equivalent"]
];
END;
EquivalentAtomBaseType: PROC [u: PT.AtomTGN, t2: TypeGraphNodeNode] RETURNS [BOOLEAN] ~ BEGIN
RETURN[ISTYPE[t2.body, PT.AtomTGN]];
END;

EquivalentBooleanBaseType: PROC [u: REF boolean base PT.ElementTGNBody, t2: TypeGraphNodeNode] RETURNS [BOOLEAN] ~ BEGIN
RETURN[ISTYPE[t2.body, REF boolean base PT.ElementTGNBody]];
END;

EquivalentIntegerBaseType: PROC [u: REF integer base PT.ElementTGNBody, t2: TypeGraphNodeNode] RETURNS [BOOLEAN] ~ BEGIN
IF ISTYPE[t2.body, REF integer base PT.ElementTGNBody]
THEN {
u2: REF integer base PT.ElementTGNBody _ NARROW[t2.body];
RETURN[(u.body.signed = u2.body.signed) AND (u.body.nBits = u2.body.nBits) AND (u.body.nUnusedBits = u2.body.nUnusedBits)];
}
ELSE RETURN[FALSE];
END;



FreelyConform: PROC [t1, t2: TypeGraphNodeNode] RETURNS [BOOLEAN] ~ BEGIN
WHILE ISTYPE[t1.body, PT.NamedTGN] DO
t1 _ NARROW[t1.body, PT.NamedTGN].type;
ENDLOOP;
WHILE ISTYPE[t2.body, PT.NamedTGN] DO
t2 _ NARROW[t2.body, PT.NamedTGN].type;
ENDLOOP;
IF Equivalent[t1, t2] THEN RETURN[TRUE];
RETURN [
WITH t1.body SELECT FROM
u: PT.AtomTGN	=> FALSE,
u: REF boolean base PT.ElementTGNBody	=> FALSE,
u: REF integer base PT.ElementTGNBody	=> FALSE,
ENDCASE =>
ERROR SaffronErrorHandling.InternalError["Unrecognized type passed as first argument to SaffronTypeConformanceImpl.FreelyConform"]
];
END;
ConversionProc: TYPE = PROC[instance: BD.ValueNode, type: TypeGraphNodeNode] RETURNS[BD.ValueNode];
IdentityConversion: ConversionProc = {RETURN[instance]};
MeaninglessConversion: ConversionProc = {
ERROR SaffronErrorHandling.InternalError["You shouldn't have called this proc."] };

Conform: PROC [t1, t2: TypeGraphNodeNode] RETURNS [conform: BOOLEAN, conversionProc: ConversionProc] ~ BEGIN
WHILE ISTYPE[t1.body, PT.NamedTGN] DO
t1 _ NARROW[t1.body, PT.NamedTGN].type;
ENDLOOP;
WHILE ISTYPE[t2.body, PT.NamedTGN] DO
t2 _ NARROW[t2.body, PT.NamedTGN].type;
ENDLOOP;
IF FreelyConform[t1, t2] THEN RETURN[TRUE, IdentityConversion];
[conform, conversionProc] _ 
WITH t1.body SELECT FROM
u: PT.AtomTGN	=> NoConform[],
u: REF boolean base PT.ElementTGNBody	=> NoConform[],
u: REF integer base PT.ElementTGNBody	=> ConformIntegerBaseType[u, t2],
ENDCASE =>
ERROR SaffronErrorHandling.InternalError["Unrecognized type passed as first argument to SaffronTypeConformanceImpl.Conform"]
;
END;
NoConform: PROC RETURNS [BOOLEAN, ConversionProc] ~ BEGIN
RETURN[FALSE, MeaninglessConversion];
END;

ConformIntegerBaseType: PROC [u: REF integer base PT.ElementTGNBody, t2: TypeGraphNodeNode] RETURNS [BOOLEAN, ConversionProc] ~ BEGIN
conform: BOOLEAN _ ISTYPE[t2.body, REF integer base PT.ElementTGNBody] OR ISTYPE[t2.body, PT.RealTGN];
RETURN[conform, IF conform THEN IntegerConvert ELSE MeaninglessConversion];
END;

IntegerConvert: ConversionProc ~ BEGIN
RETURN[BD.ChangeType[instance, type]];
END;

ConformRealBaseType: PROC [u: PT.RealTGN, t2: TypeGraphNodeNode] RETURNS [BOOLEAN, ConversionProc] ~ BEGIN
RETURN[
ISTYPE[t2.body, PT.RealTGN],
IdentityConversion
];
END;

RangeCheck: PROC [i: BD.ValueNode, targetType: TypeGraphNodeNode] RETURNS [BD.ValueNode] ~ BEGIN
t1: TypeGraphNodeNode _ BD.Type[i];
t2: TypeGraphNodeNode _ targetType;

IF NOT FreelyConform[t1, t2] THEN ERROR SaffronErrorHandling.InternalError["Arguments to SaffronTypeRangeCheckanceImpl.RangeCheck do not freely conform."];

WHILE ISTYPE[t1.body, PT.NamedTGN] DO
t1 _ NARROW[t1.body, PT.NamedTGN].type;
ENDLOOP;
WHILE ISTYPE[t2.body, PT.NamedTGN] DO
t2 _ NARROW[t2.body, PT.NamedTGN].type;
ENDLOOP;

RETURN [
WITH t2.body SELECT FROM
u: PT.AtomTGN		=> i,
u: REF boolean base PT.ElementTGNBody	=> i,
u: REF integer base PT.ElementTGNBody	=> RangeCheckIntegerBaseType[i, t2],
ENDCASE =>
ERROR SaffronErrorHandling.InternalError["Unrecognized type passed as first argument to SaffronTypeRangeCheckanceImpl.RangeCheck"]
];
END;
RangeCheckIntegerBaseType: PROC [i: BD.ValueNode, targetType: TypeGraphNodeNode] RETURNS [BD.ValueNode] ~ BEGIN
IF BD.Static[i]
THEN BEGIN
value: BigINT _ BD.RetrieveIntegerValue[i];
IF CanCastIntegerValue[value, targetType]
THEN RETURN[i]
ELSE {
SIGNAL SaffronErrorHandling.Error[0, IO.PutFR[
"Integer value %g out of range of type %g",
IO.rope[BigIntegers.RopeFromBig[value]],
IO.rope["<type>"]]];
RETURN[BD.MakeTrash[targetType]];
};
END
ELSE BEGIN
RETURN[i];
END;
END;

CanCastIntegerValue: PUBLIC PROC [value: BigINT, type: TypeGraphNodeNode] RETURNS [BOOLEAN] ~ BEGIN
baseType: PT.IntegerElementType;
WHILE ISTYPE[type.body, PT.NamedTGN] DO  -- bletch! do I have to do this everywhere?
type _ NARROW[type.body, PT.NamedTGN].type;
ENDLOOP;
baseType _ NARROW[type.body, REF integer base PT.ElementTGNBody].body;
IF baseType.signed
THEN {
nValueBits: INT _ BigCardinals.FirstOneBit[BigCardinals.BigSubtract[
BigIntegers.Abs[value], BigCardinals.BigFromSmall[IF BigIntegers.Sgn[value] = minus THEN 1 ELSE 0]]] + 1;
IF (nValueBits + 1) > baseType.nBits THEN RETURN[FALSE];
}
ELSE {
nValueBits: INT _ BigCardinals.FirstOneBit[BigIntegers.Abs[value]] + 1;
IF BigIntegers.Sgn[value] = minus THEN RETURN[FALSE];
IF nValueBits > baseType.nBits THEN RETURN[FALSE];
};
RETURN[TRUE];
END;



END.
#ςSaffronTypeConformanceImpl.Mesa
Copyright Σ 1988 by Xerox Corporation.  All rights reserved.
James Rauen, June 30, 1988 1:37:56 pm PDT
Last edited by: James Rauen August 17, 1988 7:39:55 pm PDT

This module defines the three basic relationships among Cedar types:  equivalence, free conformance, and conformance.  It exports procedures which perform type checking and (optionally) range checking based upon these relationships.  

Borrowed Types
Public Procedures
The following procedure is exported to SaffronATDef.  Should "Compatible" actually be an istype, taking instance & type.  what about range checking?  what about coercions (INT -> REAL, for instance)?

WHILE ISTYPE[targetType.body, PT.IdentifierTGN] DO
ugghhh!!!  think of a better way.  please!!
targetType _ BD.LookupTypeNameInLocalContext[lc, NARROW[targetType.body, PT.IdentifierTGN].id];
ENDLOOP;
WHILE ISTYPE[iType.body, PT.IdentifierTGN] DO
ugghhh!!!  think of a better way.  please!!
iType _ BD.LookupTypeNameInLocalContext[lc, NARROW[iType.body, PT.IdentifierTGN].id];
ENDLOOP;
note that EvaluateExpression doesn't seem to modify lc, so we really don't need to return an lc.  On the other hand, I haven't given EvaluateExpression much thought yet, and it probably does need to modify lc.
WHILE ISTYPE[targetType.body, PT.IdentifierTGN] DO
ugghhh!!!  think of a better way.  please!!
targetType _ BD.LookupTypeNameInLocalContext[lc, NARROW[targetType.body, PT.IdentifierTGN].id];
ENDLOOP;
WHILE ISTYPE[iType.body, PT.IdentifierTGN] DO
ugghhh!!!  think of a better way.  please!!
iType _ BD.LookupTypeNameInLocalContext[lc, NARROW[iType.body, PT.IdentifierTGN].id];
ENDLOOP;
The following procedures are exported to SaffronBaseDef.  They are used to perform type checking by some of the polymorphic operators.  (we'll need name lookup sooner or later)   needs a cs argument.(to get a type to return...)
type2: TypeGraphNodeNode _ LookupAnyNamedTypes[type]
type2: TypeGraphNodeNode _ LookupAnyNamedTypes[type]
Equivalence
Discussion
(Mesa manual, section 2.4.7):  "If two types are completely interchangeable, they are said to be equivalent.  A value having a given type is acceptable in any context requiring a value of any other type equivalent to it; there is no operational difference between two equivalent types."
Type equivalence is the strictest relationship among types.  It is reflexive, commutative, and transitive.  It also implies the other two relations:  If t1 and t2 are equivalent, then t1 freely conforms to t2, t2 freely conforms to t1, t1 conforms to t2, and t2 conforms to t1.
Dispatch Procedure
Look up all the top level names NOW!
Since equivalence is commutative, we can dispatch on either argument.
u: PT.SpecialTGN		=> EquivalentSpecial[u, t2],
u: PT.SubrangeTGN		=> EquivalentSubrange[u, t2], 
u: PT.RecordTGN		=> EquivalentRecord[u, t2], 
u: PT.PointerTGN		=> EquivalentPointer[u, t2], 
u: PT.RefTGN		=> EquivalentRef[u, t2], 
u: PT.VarTGN		=> EquivalentVar[u, t2], 
u: PT.RelativeTGN		=> EquivalentRelative[u, t2], 
u: PT.ReferentTGN		=> EquivalentReferent[u, t2], 
u: PT.ListTGN		=> EquivalentList[u, t2], 
u: PT.EnumTGN		=> EquivalentEnum[u, t2], 
u: PT.VariantPartTGN		=> EquivalentVariantPart[u, t2], 
u: PT.SequenceTGN		=> EquivalentSequence[u, t2], 
u: PT.ArrayTGN		=> EquivalentArray[u, t2], 
u: PT.DescriptorTGN		=> EquivalentDescriptor[u, t2], 
u: PT.TransferTGN		=> EquivalentTransfer[u, t2], 
u: PT.ZoneTGN		=> EquivalentZone[u, t2], 
u: PT.LongTGN		=> EquivalentLong[u, t2], 
u: PT.InterfaceTGN		=> EquivalentInterface[u, t2], 
u: PT.LinkTGN		=> EquivalentLink[u, t2], 
u: PT.FrameTGN		=> EquivalentFrame[u, t2], 
u: PT.SpecianatedTGN		=> EquivalentSpecianated[u, t2], 
u: PT.OpaqueTGN		=> EquivalentOpaque[u, t2], 
Methods

Free Conformance
Discussion
(Mesa manual, section 3.5.3):  "The relationship of free conformace...is defined so that it can be computed recursively.  Loosely speaking, one type freely conforms to another if a value of the first can always be used as a value of the second without any computation or run-time check of validity. "
Free conformance is less strict than equivalence, but more strict than conformance.  It is reflexive and commutative, but not transitive.  It is implied by equivalence:  t1 and t2 are equivalent => t1 freely conforms to t2, and t2 freely conforms to t1 .  It implies conformace:  t1 freely conforms to t2 => t1 conforms to t2.
Dispatch Procedure
Look up all the top level names NOW!
Equivalence implies free conformance.
u: PT.SpecialTGN		=> FreelyConformSpecial[u, t2],
u: PT.SubrangeTGN		=> FreelyConformSubrange[u, t2], 
u: PT.RecordTGN		=> FreelyConformRecord[u, t2], 
u: PT.PointerTGN		=> FreelyConformPointer[u, t2], 
u: PT.RefTGN		=> FreelyConformRef[u, t2], 
u: PT.VarTGN		=> FreelyConformVar[u, t2], 
u: PT.RelativeTGN		=> FreelyConformRelative[u, t2], 
u: PT.ReferentTGN		=> FreelyConformReferent[u, t2], 
u: PT.ListTGN		=> FreelyConformList[u, t2], 
u: PT.EnumTGN		=> FreelyConformEnum[u, t2], 
u: PT.VariantPartTGN		=> FreelyConformVariantPart[u, t2], 
u: PT.SequenceTGN		=> FreelyConformSequence[u, t2], 
u: PT.ArrayTGN		=> FreelyConformArray[u, t2], 
u: PT.DescriptorTGN		=> FreelyConformDescriptor[u, t2], 
u: PT.TransferTGN		=> FreelyConformTransfer[u, t2], 
u: PT.ZoneTGN		=> FreelyConformZone[u, t2], 
u: PT.LongTGN		=> FreelyConformLong[u, t2], 
u: PT.InterfaceTGN		=> FreelyConformInterface[u, t2], 
u: PT.LinkTGN		=> FreelyConformLink[u, t2], 
u: PT.FrameTGN		=> FreelyConformFrame[u, t2], 
u: PT.SpecianatedTGN		=> FreelyConformSpecianated[u, t2], 
u: PT.OpaqueTGN		=> FreelyConformOpaque[u, t2], 
Methods
Conformance
Discussion
(Mesa manual, section 2.4.7):  "One type is said to conform to another if any value of the first type can be assigned to a variable of the second type...In more interesting cases, an automatic application of a conversion function may be required prior to the assignment."
Conformance is the loosest relationship among types.  It is reflexive and commutative, but not transitive.  It is implied by the other two relations:  t1 and t2 are equivalent => t1 and t2 freely conform; t1 freely conforms to t2 => t1 conforms to t2.
The Conform[t1, t2] procedure returns two values:
(1) A boolean value which indicates whether or not the two types conform.  
(2) A procedure which takes two arguments.  The first argument, i, must be an instance of type t1; the second must be type type t2.  (no upward funargs, mutter, grumble, grumble)  This procedure returns a new instance whose type freely conforms with t2 and whose value is the (possibly converted) value of i.  The conversions which might be performed are listed in section 3.5.1 of the Mesa manual.
Note that if the procedure (2) can detect a conversion error while playing around with static instances, it will raise an error and return a trash instance of the correct type.
Dispatch Procedure
Look up all the top level names NOW!
If t1 and t2 freely conform, then they conform.
Otherwise, they don't freely conform.  Dispatch...
u: PT.SpecialTGN		=> ConformSpecial[u, t2],
u: PT.SubrangeTGN		=> ConformSubrange[u, t2], 
u: PT.RecordTGN		=> ConformRecord[u, t2], 
u: PT.PointerTGN		=> ConformPointer[u, t2], 
u: PT.RefTGN		=> ConformRef[u, t2], 
u: PT.VarTGN		=> ConformVar[u, t2], 
u: PT.RelativeTGN		=> ConformRelative[u, t2], 
u: PT.ReferentTGN		=> ConformReferent[u, t2], 
u: PT.ListTGN		=> ConformList[u, t2], 
u: PT.EnumTGN		=> ConformEnum[u, t2], 
u: PT.VariantPartTGN		=> ConformVariantPart[u, t2], 
u: PT.SequenceTGN		=> ConformSequence[u, t2], 
u: PT.ArrayTGN		=> ConformArray[u, t2], 
u: PT.DescriptorTGN		=> ConformDescriptor[u, t2], 
u: PT.TransferTGN		=> ConformTransfer[u, t2], 
u: PT.ZoneTGN		=> ConformZone[u, t2], 
u: PT.LongTGN		=> ConformLong[u, t2], 
u: PT.InterfaceTGN		=> ConformInterface[u, t2], 
u: PT.LinkTGN		=> ConformLink[u, t2], 
u: PT.FrameTGN		=> ConformFrame[u, t2], 
u: PT.SpecianatedTGN		=> ConformSpecianated[u, t2], 
u: PT.OpaqueTGN		=> ConformOpaque[u, t2], 
Methods
Range Checking
Discussion
Foo
Dispatch Procedure
Requires: FreelyConform[Type[i], targetType]
Look up all the top level names NOW!
Dispatch on the target type
u: PT.SpecialTGN		=> RangeCheckSpecial[u, t2],
u: PT.SubrangeTGN		=> RangeCheckSubrange[u, t2], 
u: PT.RecordTGN		=> RangeCheckRecord[u, t2], 
u: PT.PointerTGN		=> RangeCheckPointer[u, t2], 
u: PT.RefTGN		=> RangeCheckRef[u, t2], 
u: PT.VarTGN		=> RangeCheckVar[u, t2], 
u: PT.RelativeTGN		=> RangeCheckRelative[u, t2], 
u: PT.ReferentTGN		=> RangeCheckReferent[u, t2], 
u: PT.ListTGN		=> RangeCheckList[u, t2], 
u: PT.EnumTGN		=> RangeCheckEnum[u, t2], 
u: PT.VariantPartTGN		=> RangeCheckVariantPart[u, t2], 
u: PT.SequenceTGN		=> RangeCheckSequence[u, t2], 
u: PT.ArrayTGN		=> RangeCheckArray[u, t2], 
u: PT.DescriptorTGN		=> RangeCheckDescriptor[u, t2], 
u: PT.TransferTGN		=> RangeCheckTransfer[u, t2], 
u: PT.ZoneTGN		=> RangeCheckZone[u, t2], 
u: PT.LongTGN		=> RangeCheckLong[u, t2], 
u: PT.InterfaceTGN		=> RangeCheckInterface[u, t2], 
u: PT.LinkTGN		=> RangeCheckLink[u, t2], 
u: PT.FrameTGN		=> RangeCheckFrame[u, t2], 
u: PT.SpecianatedTGN		=> RangeCheckSpecianated[u, t2], 
u: PT.OpaqueTGN		=> RangeCheckOpaque[u, t2], 
Methods
add range checking code
Κj˜™Icode™<Kšœ&Οk™)Kš
œ:™:K™—Ibody™κ
L™š
	˜	Kšœ
œ*˜<Kšœœ!˜2Kšœ
œ˜Kšœ
œ˜Kšœœœ
˜°
KšœœY˜yKšœœ˜2K˜—šΟnœœ
˜)Kšœœ&˜KKšœ˜$Kšœ˜K˜Kšœ
œœ˜8K˜—
head™Kšœœ˜"K˜Kšœœœ˜4Kšœœ
œœ˜>—š
Οz™šœzΟb2Πbk ‘ ™Η
L™šžœœ
œ œœ3œœ˜Θ
Kš
œ˜Kš
œ˜Kšœœ˜Kšœ	œ
˜K˜šœ
œœ™2K™+Kšœ
œ"œœ™_Kšœ
™—Kš
œ@˜@Kšœœ	˜šœ
œ
œ™-K™+Kšœœ"œ
œ™UKšœ
™—Kš
œ7˜7šœ
œ	œ˜šœ˜$šœ.˜0Kšœœ˜Kšœ˜——Kšœ
œ˜&K˜—Kš
œ"˜"Kšœ
œ
œ Οc%˜QKšœ	˜Kšœ
˜K˜—šžœœ
œ œœœ3œ
œ˜Μ
K™Ρ
Kš
œ˜Kš
œ˜Kšœ	œ
˜K˜šœ
œœ™2K™+Kšœ
œ"œœ™_Kšœ
™—Kš
œ>˜>Kšœœ	˜šœ
œ
œ™-K™+Kšœœ"œ
œ™UKšœ
™—Kš
œ7˜7šœ
œ	œ˜šœ˜$šœ.˜0Kšœœ˜Kšœ˜——Kšœ
œ˜!K˜—Kš
œ"˜"Kšœ
œ
œ ’%˜QKšœ˜
Kšœ
˜K˜—Lš
œγ
™γ
—˜š	žœœ
œœ˜HKšœœ	˜%šœ
œœ˜'Kšœœœ˜+Kšœ’˜—K™4šœ
œœœœ
œœœ˜rKšœ
œ˜šœ˜šœ˜$šœ4˜6Kšœœ˜——Kšœ
œœ˜K˜——Kšœ
˜K˜—šžœœ
œœ
œ˜MKšœ
œ˜
Kšœ
˜—K˜š	ž
œœ
œœ˜IKšœœ	˜%šœ
œœ˜'Kšœœœ˜+Kšœ’˜—K™4šœ
œœœ˜8Kšœ
œ˜šœ˜šœ˜$šœ;˜=Kšœœ˜——Kšœ
œœ˜K˜——Kšœ
˜———™™
LšœaΟi
œ³
™žLšœš
Οd
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ
™•—™š	ž
œœœœ˜FK™$šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—Kš
œE™Ešœ˜šœ	œ
˜Kšœœ*˜/Kšœœœ4˜JKšœœœ4˜JKšœœ)™.Kšœœ,™1Kšœœ(™-Kšœœ*™/Kšœœ"™'Kšœœ"™'Kšœœ,™1Kšœœ,™1Kšœœ$™)Kšœœ$™)Kšœœ2™7Kšœœ,™1Kšœœ&™+Kšœœ0™5Kšœœ,™1Kšœœ$™)Kšœœ$™)Kšœœ.™3Kšœœ$™)Kšœœ&™+Kšœœ2™7Kšœœ(™-šœ˜
Kšœz˜——K˜—Kšœ
˜——™šžœœœ!œœ˜]Kšœ
œ
œ˜$Kšœ
˜K˜—š
žœœœ	œ(œœ˜xKšœ
œ
œœ˜<Kšœ
˜K˜—š
žœœœœ(œœ˜xšœ
œ
œœ˜6šœ˜Kšœœœœ
˜9Kšœ"œ œ-˜{K˜
—Kšœ
œ
œ˜—Kšœ
˜K˜—˜K˜—M™——™™
Lš
œ¬™¬Lšœ«
€
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ
™Ζ—™š	ž
œœœœ˜IK™$šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—J™%Jšœœ
œ
œ˜(šœ˜šœ	œ
˜Kšœœ
˜Kšœœœœ
˜/Kšœœ	œœ
˜/Kšœœ,™1Kšœœ/™4Kšœœ+™0Kšœœ-™2Kšœœ%™*Kšœœ%™*Kšœœ/™4Kšœœ/™4Kšœœ'™,Kšœœ'™,Kšœœ5™:Kšœœ/™4Kšœœ)™.Kšœœ3™8Kšœœ/™4Kšœœ'™,Kšœœ'™,Kšœœ1™6Kšœœ'™,Kšœœ)™.Kšœœ5™:Kšœœ+™0šœ˜
Kšœ}˜‚
——K˜—Kšœ
˜——M™—™™
Lš
œ™Lšœ˜
€
œ€
œ€
œ€
œ€
œ€
œ€
œ€
œ
™ϋ
šœ œ&™1Lš
œK™KLšœ†
+œέ
™Ž—L™°
—™Kšœœœ2œ˜cKšžœœ˜8šžœ˜)KšœN˜S—K˜š	žœœœœ$˜lK™$šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—Kš
œ/™/Kšœœ
œ
œ˜?K™2š
œ˜šœ	œ
˜Kšœœ˜Kšœœ	œ˜5Kšœœ	œ1˜GKšœœ&™+Kšœœ)™.Kšœœ%™*Kšœœ'™,Kšœœ™$Kšœœ™$Kšœœ)™.Kšœœ)™.Kšœœ!™&Kšœœ!™&Kšœœ/™4Kšœœ)™.Kšœœ#™(Kšœœ-™2Kšœœ)™.Kšœœ!™&Kšœœ!™&Kšœœ+™0Kšœœ!™&Kšœœ#™(Kšœœ/™4Kšœœ%™*šœ˜
Kšœw˜|—K˜
——Kšœ
˜——™š	ž	œœ
œœ˜9Kšœ
œ˜%Kšœ
˜K˜—š
žœœœ	œ(œœ˜…
Kšœ	œœ
œœœ
œ
œ
˜fKšœ
œ	œœ˜KKšœ
˜K˜—šžœ˜&Kšœ
œ˜&Kšœ
˜K˜—šžœœœ!œ	œ˜jšœ
˜Kšœ
œ
˜K˜K˜—Kšœ
˜K˜———™™
L™—™šž
œœœ+œœ˜`Kšœœ	˜#Kš
œ#˜#K˜K™,Kšœ
œœ
œt˜›
K˜K™$šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—šœ
œ
œ˜%Kšœœ
œ˜'Kšœ
˜—J˜J™šœ˜šœ	œ
˜Kšœœ˜Kšœœœ˜+Kšœœœ4˜JKšœœ)™.Kšœœ,™1Kšœœ(™-Kšœœ*™/Kšœœ"™'Kšœœ"™'Kšœœ,™1Kšœœ,™1Kšœœ$™)Kšœœ$™)Kšœœ2™7Kšœœ,™1Kšœœ&™+Kšœœ0™5Kšœœ,™1Kšœœ$™)Kšœœ$™)Kšœœ.™3Kšœœ$™)Kšœœ&™+Kšœœ2™7Kšœœ(™-šœ˜
Kšœ}˜‚
——K˜—Kšœ
˜——™šžœœ2œ˜ošœ
œ
˜šœ
˜
Kšœœ˜+šœ'˜)Kšœ
œ˜šœ˜šœœ˜.K˜+Kšœ&˜(Kšœ˜—Kšœ
œ˜!K˜——Kš
˜—šœ
˜
K™Kšœ˜
Kšœ
˜——Kšœ
˜K˜—š	žœœ*œœ˜cJšœ
œ˜ š	œ
œœœ’+˜TJšœœœ˜+Jšœ
˜—Jšœœœœ˜Fšœ˜šœ˜šœœ5˜DJšœ2œ œœ
˜i—Jšœ#œ
œ
œ˜8J˜
—šœ˜Jšœœ8˜GJšœ œ
œ
œ˜5Jšœœ
œ
œ˜2J˜——Jšœ
œ˜
Jšœ
˜J˜J˜K˜——Kšœ
˜——…—$$Z€