\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4\generic GSub \extends G ;defined in: genericRules.key Line: 11 Offset :4\generic C;defined in: genericRules.key Line: 13 Offset :4\generic CSub \extends C ;defined in: genericRules.key Line: 14 Offset :4firstOfPair {
\find ( first ( pair ( t , t1 )))
\replacewith ( t )
\heuristics (concrete )
};defined in: genericRules.key Line: 47 Offset :4secondOfPair {
\find ( second ( pair ( t , t1 )))
\replacewith ( t1 )
\heuristics (concrete )
};defined in: genericRules.key Line: 53 Offset :4instanceof_static_type {
\schemaVar \term any a ;
\find ( G :: instance ( a ))
\varcond \replacewith ( TRUE )
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof static supertype"
};defined in: genericRules.key Line: 61 Offset :4instanceof_static_type_2 {
\schemaVar \term any a , a2 ;
\assumes ( a2 = a ==> )
\find ( G :: instance ( a ))
\sameUpdateLevel
\varcond \replacewith ( TRUE )
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof static supertype"
};defined in: genericRules.key Line: 70 Offset :4instanceof_not_compatible {
\schemaVar \term any a ;
\find ( G :: instance ( a )= TRUE )
\varcond \replacewith ( a = null )
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof disjoint type"
};defined in: genericRules.key Line: 81 Offset :4instanceof_not_compatible_2 {
\schemaVar \term any a ;
\find ( G :: instance ( a )= FALSE )
\varcond \replacewith ( ! ( a = null ))
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof disjoint type"
};defined in: genericRules.key Line: 90 Offset :4instanceof_not_compatible_3 {
\schemaVar \term any a ;
\find ( G :: instance ( a )= TRUE )
\varcond \replacewith ( false )
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof disjoint type"
};defined in: genericRules.key Line: 99 Offset :4instanceof_not_compatible_4 {
\schemaVar \term any a ;
\find ( G :: instance ( a )= FALSE )
\varcond \replacewith ( true )
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof disjoint type"
};defined in: genericRules.key Line: 108 Offset :4instanceof_not_compatible_5 {
\schemaVar \term any a ;
\assumes ( H :: instance ( a )= TRUE ==> )
\find ( G :: instance ( a )= TRUE )
\varcond \replacewith ( a = null )
\heuristics (concrete , evaluate_instanceof )
\displayname "instanceof disjoint type"
};defined in: genericRules.key Line: 120 Offset :4instanceof_known_dynamic_type {
\schemaVar \term any a ;
\assumes ( G :: exactInstance ( a )= TRUE ==> )
\find ( H :: instance ( a ))
\sameUpdateLevel
\varcond \replacewith ( TRUE )
\heuristics (simplify , evaluate_instanceof )
};defined in: genericRules.key Line: 130 Offset :4instanceof_known_dynamic_type_2 {
\schemaVar \term any a ;
\assumes ( G :: exactInstance ( a )= TRUE ==> )
\find ( H :: instance ( a ))
\sameUpdateLevel
\varcond \replacewith ( FALSE )
\heuristics (simplify , evaluate_instanceof )
};defined in: genericRules.key Line: 140 Offset :4exact_instance_known_dynamic_type {
\schemaVar \term any a ;
\assumes ( G :: exactInstance ( a )= TRUE ==> )
\find ( H :: exactInstance ( a ))
\sameUpdateLevel
\varcond \replacewith ( FALSE )
\heuristics (simplify , evaluate_instanceof )
};defined in: genericRules.key Line: 150 Offset :4typeEqDerived {
\assumes ( s = t1 ==> )
\find ( H :: instance ( s ))
\sameUpdateLevel
\replacewith ( TRUE )
\heuristics (simplify , concrete )
\displayname "typeEq"
};defined in: genericRules.key Line: 168 Offset :4typeEqDerived2 {
\assumes ( s = t1 ==> )
\find ( G :: instance ( t1 ))
\sameUpdateLevel
\replacewith ( TRUE )
\heuristics (simplify , concrete )
\displayname "typeEq"
};defined in: genericRules.key Line: 177 Offset :4castAdd {
\schemaVar \term [ strict ]C strictCTerm2 ;
\assumes ( CSub :: instance ( strictCTerm2 )= TRUE ==> )
\find ( strictCTerm2 )
\sameUpdateLevel
\replacewith ( (CSub ) strictCTerm2 )
\displayname "narrow type"
};defined in: genericRules.key Line: 193 Offset :4castAdd2 {
\schemaVar \term C cs ;
\schemaVar \term G gt ;
\assumes ( cs = gt ==> )
\find ( gt )
\sameUpdateLevel
\varcond \replacewith ( (C ) gt )
\displayname "castAdd"
};defined in: genericRules.key Line: 205 Offset :4castDel {
\schemaVar \term C castedTerm ;
\find ( (C ) castedTerm )
\replacewith ( castedTerm )
\heuristics (simplify , cast_deletion )
\displayname "castDel"
};defined in: genericRules.key Line: 217 Offset :4castDel2 {
\schemaVar \term CSub cs ;
\schemaVar \term G gt ;
\assumes ( cs = gt ==> )
\find ( (C ) gt )
\sameUpdateLevel
\replacewith ( cs )
\displayname "castDel"
};defined in: genericRules.key Line: 225 Offset :4closeType {
\assumes ( ==> G :: instance ( t1 )= TRUE )
\find ( GSub :: instance ( t1 )= TRUE ==> )
\closegoal
\heuristics (closure )
\displayname "closeType"
};defined in: genericRules.key Line: 252 Offset :4closeTypeSwitched {
\assumes ( GSub :: instance ( t1 )= TRUE ==> )
\find ( ==> G :: instance ( t1 )= TRUE )
\closegoal
\heuristics (closure )
\displayname "closeType"
};defined in: genericRules.key Line: 260 Offset :4ineffectiveCast {
\assumes ( H :: instance ( t )= TRUE ==> )
\find ( (H ) t )
\sameUpdateLevel
\add ( (H ) t = t ==> )
\heuristics (inReachableStateImplication )
};defined in: genericRules.key Line: 267 Offset :4ineffectiveCast3 {
\assumes ( H :: exactInstance ( t )= TRUE ==> )
\find ( (H ) t )
\sameUpdateLevel
\add ( (H ) t = t ==> )
\heuristics (inReachableStateImplication )
};defined in: genericRules.key Line: 292 Offset :4ineffectiveCast2 {
\schemaVar \term CSub cs ;
\schemaVar \term G gt ;
\assumes ( cs = gt ==> )
\find ( (C ) gt )
\sameUpdateLevel
\add ( (C ) gt = gt ==> )
\heuristics (inReachableStateImplication )
};defined in: genericRules.key Line: 300 Offset :4sortsDisjointModuloNull {
\schemaVar \term G x ;
\schemaVar \term H y ;
\find ( x = y )
\varcond \replacewith ( x = null & y = null )
\heuristics (simplify )
};defined in: genericRules.key Line: 316 Offset :4sortsDisjoint1 {
\schemaVar \term G x ;
\schemaVar \term H y ;
\find ( x = y )
\varcond \replacewith ( false )
\heuristics (concrete )
};defined in: genericRules.key Line: 327 Offset :4sortsDisjoint2 {
\schemaVar \term G x ;
\schemaVar \term H y ;
\find ( x = y )
\varcond \replacewith ( false )
\heuristics (concrete )
};defined in: genericRules.key Line: 338 Offset :4