<commit_before>package wyil.util.type;

import static wyil.lang.Type.*;

import java.util.ArrayList;

import wyautl.lang.*;
import wyautl.util.BinaryMatrix;
import wyil.lang.NameID;
import wyil.lang.Type;

public class SubtypeOperator implements Relation {
	protected final Automata from;
	protected final Automata to;
	private final BinaryMatrix intersections;
	
	public SubtypeOperator(Automata from, Automata to) {
		this.from = from;
		this.to = to;
		// matrix is twice the size to accommodate positive and negative signs 
		this.intersections = new BinaryMatrix(from.size()*2,to.size()*2,true);
	}
	
	public final Automata from() {
		return from;
	}
	
	public final Automata to() {
		return to;
	}
	
	public final boolean update(int fromIndex, int toIndex) {
		boolean oldTrueTrue = intersection(fromIndex,true,toIndex,true);
		boolean oldFalseTrue = intersection(fromIndex,false,toIndex,true);
		boolean oldTrueFalse = intersection(fromIndex,true,toIndex,false);
		boolean oldFalseFalse = intersection(fromIndex,false,toIndex,false);
		
		boolean newTrueTrue = isIntersection(fromIndex,true,toIndex,true);
		boolean newFalseTrue = isIntersection(fromIndex,false,toIndex,true);
		boolean newTrueFalse = isIntersection(fromIndex,true,toIndex,false);
		boolean newFalseFalse = isIntersection(fromIndex,false,toIndex,false);
		
		setIntersection(fromIndex,true,toIndex,true,newTrueTrue);
		setIntersection(fromIndex,false,toIndex,true,newFalseTrue);
		setIntersection(fromIndex,true,toIndex,false,newTrueFalse);
		setIntersection(fromIndex,false,toIndex,false,newFalseFalse);
		
		return oldTrueTrue != newTrueTrue || oldFalseTrue != newFalseTrue
				|| oldTrueFalse != newTrueFalse
				|| oldFalseFalse != newFalseFalse; 
	}
	
	public final boolean isRelated(int fromIndex, int toIndex) {
		return intersection(fromIndex,true,toIndex,true);
	}
	
	/**
	 * Test whether <code>from</code> :> <code>to</code>
	 * @param fromIndex
	 * @param toIndex
	 * @return
	 */
	public final boolean isSubtype(int fromIndex, int toIndex) {
		return !intersection(fromIndex,false,toIndex,true);
	}
	
	/**
	 * Test whether <code>from</code> <: <code>to</code>
	 * @param fromIndex
	 * @param toIndex
	 * @return
	 */
	public final boolean isSupertype(int fromIndex, int toIndex) {
		return !intersection(fromIndex,true,toIndex,false);
	}
	
	/**
	 * Determine whether there is a non-empty intersection between the state
	 * rooted at <code>fromIndex</code> and that rooted at <code>toIndex</code>.
	 * 
	 * @param fromIndex
	 *            --- index of from state
	 * @param toIndex
	 *            --- index of to state
	 * @return --- true if such an intersection exists, false otherwise.
	 */
	public final boolean isIntersection(int fromIndex, int toIndex) {
		return intersection(fromIndex,true,toIndex,true);
	}

	/**
	 * Determine whether there is a non-empty intersection between the state
	 * rooted at <code>fromIndex</code> and that rooted at <code>toIndex</code>.
	 * The signs indicate whether or not the state should be taken as its
	 * <i>inverse</i>.
	 * 
	 * @param fromIndex
	 *            --- index of from state
	 * @param fromSign
	 *            --- sign of from state (true = normal, false = inverted).
	 * @param toIndex
	 *            --- index of to state
	 * @param toSign
	 *            --- sign of from state (true = normal, false = inverted).
	 * @return --- true if such an intersection exists, false otherwise.
	 */
	public boolean isIntersection(int fromIndex, boolean fromSign, int toIndex,
			boolean toSign) {
		
		Automata.State fromState = from.states[fromIndex];
		Automata.State toState = to.states[toIndex];
		int fromKind = fromState.kind;
		int toKind = toState.kind;
		
		if(fromKind == toKind) {			
			switch(fromKind) {
			case K_VOID:
				return !fromSign && !toSign;
			case K_ANY:
				return fromSign && toSign;
			// === Leaf States First ===
			case K_EXISTENTIAL:
				NameID nid1 = (NameID) fromState.data;
				NameID nid2 = (NameID) toState.data;				
				return fromSign == toSign && nid1.equals(nid2);			
			// === Homogenous Compound States ===
			case K_SET:
			case K_LIST:
				// != below not ||. This is because lists and sets can intersect
				// on the empty list/set.
				if(fromSign != toSign) {					
					// nary nodes
					int fromChild = fromState.children[0];
					int toChild = toState.children[0];
					if (!intersection(fromChild, fromSign, toChild, toSign)) {
						return false;					
					}
				}
				return true;
			case K_PROCESS:
			case K_DICTIONARY:
			case K_TUPLE:  {				
				if(fromSign || toSign) {					
					// nary nodes
					int[] fromChildren = fromState.children;
					int[] toChildren = toState.children;
					if (fromChildren.length != toChildren.length) {
						return false;
					}
					boolean andChildren = true;
					boolean orChildren = false;
					for (int i = 0; i < fromChildren.length; ++i) {
						int fromChild = fromChildren[i];
						int toChild = toChildren[i];
						boolean v = intersection(fromChild, fromSign, toChild,
								toSign);	
						andChildren &= v;
						orChildren |= v;						
					}
					if(!fromSign || !toSign) {
						return orChildren;
					} else {
						return andChildren;
					}
				}
				return true;
			}
			case K_RECORD: {				
				if(fromSign || toSign) {					
					int[] fromChildren = fromState.children;
					int[] toChildren = toState.children;
					if (fromChildren.length != toChildren.length) {
						return !fromSign || !toSign;
					}				
					ArrayList<String> fromFields = (ArrayList<String>) fromState.data;
					ArrayList<String> toFields = (ArrayList<String>) toState.data;				
					boolean andChildren = true;
					boolean orChildren = false;
					for (int i = 0; i != fromFields.size(); ++i) {
						String e1 = fromFields.get(i);
						String e2 = toFields.get(i);
						if(!e1.equals(e2)) { return !fromSign || !toSign; }
						int fromChild = fromChildren[i];
						int toChild = toChildren[i];
						boolean v = intersection(fromChild, fromSign, toChild,
								toSign);
						andChildren &= v;
						orChildren |= v;
					}
					if(!fromSign || !toSign) {
						return orChildren;
					} else {
						return andChildren;
					}
				}
				return true;
			}
			case K_NEGATION: 
			case K_UNION : 
			case K_INTERSECTION:
					// let these cases fall through to if-statements after
					// switch.
				break;
			// === Heterogenous Compound States ===
			case K_FUNCTION:
			case K_HEADLESS:
			case K_METHOD:
				if(fromSign || toSign) {
					// nary nodes
					int[] fromChildren = fromState.children;
					int[] toChildren = toState.children;
					if(fromChildren.length != toChildren.length){
						return false;
					}
					
					int recIndex = fromKind == Type.K_METHOD ? 0 : -1;					
					int retIndex = fromKind == Type.K_METHOD ? 1 : 0;
					boolean andChildren = true;
					boolean orChildren = false;					
					for(int i=0;i<fromChildren.length;++i) {
						boolean v;
						if(i == recIndex) {
							// receiver type is invariant
							// FIXME: make receiver invariant!
							v = intersection(fromChildren[i], !fromSign,
									toChildren[i], !toSign);
						} else if(i == retIndex) {
							// return type is co-variant
							v = intersection(fromChildren[i], fromSign,
									toChildren[i], toSign);
						} else {
							// parameter type(s) are contra-variant
							v = intersection(fromChildren[i], !fromSign,
								toChildren[i], !toSign);
						}
						andChildren &= v;
						orChildren |= v;
					}
					if(!fromSign || !toSign) {
						return orChildren;
					} else {
						return andChildren;
					}
				}
				return true;
			default:
				return fromSign == toSign;
			}
		} 
		
		if(fromKind == K_NEGATION) {
			int fromChild = fromState.children[0];
			return intersection(fromChild,!fromSign,toIndex,toSign);
		} else if(toKind == K_NEGATION) {
			int toChild = toState.children[0];
			return intersection(fromIndex,fromSign,toChild,!toSign);			
		}
		
		// using invert helps reduce the number of cases to consider.
		fromKind = invert(fromKind,fromSign);
		toKind = invert(toKind,toSign);		
				
		if(fromKind == K_VOID || toKind == K_VOID){
			return false;
		} else if(fromKind == K_UNION) {			
			int[] fromChildren = fromState.children;		
			for(int i : fromChildren) {				
				if(intersection(i,fromSign,toIndex,toSign)) {
					return true;
				}								
			}
			return false;	
		} else if(toKind == K_UNION) {
			int[] toChildren = toState.children;		
			for(int j : toChildren) {
				if(intersection(fromIndex,fromSign,j,toSign)) {
					return true;
				}											
			}
			return false;	
		} else if(fromKind == K_INTERSECTION) {
			int[] fromChildren = fromState.children;			
			for (int i : fromChildren) {				
				if(!intersection(i,fromSign,toIndex,toSign)) {
					return false;
				}											
			}
			return true;	
		} else if(toKind == K_INTERSECTION) {
			int[] toChildren = toState.children;					
			for (int j : toChildren) {				
				if(!intersection(fromIndex,fromSign,j,toSign)) {
					return false;
				}											
			}			
			return true;	
		} else if(fromKind == K_ANY || toKind == K_ANY){
			return true;
		}  
		
		return !fromSign || !toSign;		
	}
	
	private int invert(int kind, boolean sign) {
		if(sign) {
			return kind;
		}
		switch(kind) {
			case K_ANY:
				return K_VOID;
			case K_VOID:
				return K_ANY;
			case K_UNION:
				return K_INTERSECTION;
			case K_INTERSECTION:
				return K_UNION;
			default:
				return kind;
		}		
	}
	
	private boolean intersection(int fromIndex, boolean fromSign, int toIndex, boolean toSign) {
		if(fromSign) {
			fromIndex += from.size();
		}
		if(toSign) {
			toIndex += to.size();
		}
		
		return intersections.get(fromIndex,toIndex);
	}
		
	private void setIntersection(int fromIndex, boolean fromSign,
			int toIndex, boolean toSign, boolean value) {
		if(fromSign) {
			fromIndex += from.size();
		}
		if(toSign) {
			toIndex += to.size();
		}
		<commit_msg>Added some documentation for the subtype operator.  Begun the process of fixing the way it works with respect to assumptions.<commit_after>package wyil.util.type;

import static wyil.lang.Type.*;

import java.util.ArrayList;

import wyautl.lang.*;
import wyautl.util.BinaryMatrix;
import wyil.lang.NameID;
import wyil.lang.Type;

/**
 * <p>
 * The subtype operator implements the algorithm for determining whether or not
 * one type is a <i>subtype</i> of another. For the most part, one can take
 * subtype to mean <i>subset</i> (this analogy breaks down with function types,
 * however). Following this analogy, <code>T1</code> is a subtype of
 * <code>T2</code> (denoted <code>T1 <: T2</code>) if the set of values
 * represented by <code>T1</code> is a subset of those represented by
 * <code>T2</code>.
 * </p>
 * <p>
 * The algorithm actually operates by computing the <i>intersection</i> relation
 * for two types (i.e. whether or not an intersection exists between their set
 * of values). Subtyping is closely related to intersection and, in fact, we
 * have that <code>T1 :> T2</code> iff <code>!(!T1 & T2)</code> (where
 * <code>&</code> is the intersection relation). The choice to compute
 * intersections, rather than subtypes, was for simplicity. Namely, it was
 * considered conceptually easier to think about intersections rather than
 * subtypes.
 * </p>
 * <p>
 * <b>NOTE:</b> for this algorithm to return correct results in all cases, both
 * types must have been normalised first.
 * </p>
 * <h3>References</h3>
 * <ul>
 * <li><p><NAME> and <NAME>. Structural and Flow-Sensitive Types for
 * Whiley. Technical Report, Victoria University of Wellington, 2010.</p></li>
 * <li><p><NAME>, <NAME>, and <NAME>. Semantic subtyping. In
 * Proceedings of the <i>Symposium on Logic in Computer Science</i>, pages
 * 137--146. IEEE Computer Society Press, 2002.</p></li>
 * <li><p><NAME>, <NAME>, and <NAME>. Efficient
 * recursive subtyping. In <i>Proceedings of the ACM Conference on Principles of
 * Programming Languages</i>, pages 419--428, 1993.</p></li>
 * <li><p><NAME> and <NAME>. Subtyping recursive types. <i>ACM
 * Transactions on Programming Languages and Systems</i>,
 * 15:575--631, 1993.</p></li>
 * </ul>
 * 
 * @author djp
 * 
 */
public class SubtypeOperator {
	protected final Automata from; 
	protected final Automata to;
	private final BinaryMatrix intersections;
	
	public SubtypeOperator(Automata from, Automata to) {
		this.from = from;
		this.to = to;
		// matrix is twice the size to accommodate positive and negative signs 
		this.intersections = new BinaryMatrix(from.size()*2,to.size()*2,true);
	}
	
	/**
	 * Test whether <code>from</code> :> <code>to</code>
	 * @param fromIndex
	 * @param toIndex
	 * @return
	 */
	public final boolean isSubtype(int fromIndex, int toIndex) {
		return !isIntersection(fromIndex,false,toIndex,true);
	}
	
	/**
	 * Test whether <code>from</code> <: <code>to</code>
	 * @param fromIndex
	 * @param toIndex
	 * @return
	 */
	public final boolean isSupertype(int fromIndex, int toIndex) {
		return !isIntersection(fromIndex,true,toIndex,false);
	}	

	/**
	 * Determine whether there is a non-empty intersection between the state
	 * rooted at <code>fromIndex</code> and that rooted at <code>toIndex</code>.
	 * The signs indicate whether or not the state should be taken as its
	 * <i>inverse</i>.
	 * 
	 * @param fromIndex
	 *            --- index of from state
	 * @param fromSign
	 *            --- sign of from state (true = normal, false = inverted).
	 * @param toIndex
	 *            --- index of to state
	 * @param toSign
	 *            --- sign of from state (true = normal, false = inverted).
	 * @return --- true if such an intersection exists, false otherwise.
	 */
	private boolean isIntersection(int fromIndex, boolean fromSign, int toIndex,
			boolean toSign) {
		
	}
	
	private boolean isIntersectionInner(int fromIndex, boolean fromSign, int toIndex,
			boolean toSign) {
		
		Automata.State fromState = from.states[fromIndex];
		Automata.State toState = to.states[toIndex];
		int fromKind = fromState.kind;
		int toKind = toState.kind;
		
		if(fromKind == toKind) {			
			switch(fromKind) {
			case K_VOID:
				return !fromSign && !toSign;
			case K_ANY:
				return fromSign && toSign;
			// === Leaf States First ===
			case K_EXISTENTIAL:
				NameID nid1 = (NameID) fromState.data;
				NameID nid2 = (NameID) toState.data;				
				return fromSign == toSign && nid1.equals(nid2);			
			// === Homogenous Compound States ===
			case K_SET:
			case K_LIST:
				// != below not ||. This is because lists and sets can intersect
				// on the empty list/set.
				if(fromSign != toSign) {					
					// nary nodes
					int fromChild = fromState.children[0];
					int toChild = toState.children[0];
					if (!intersection(fromChild, fromSign, toChild, toSign)) {
						return false;					
					}
				}
				return true;
			case K_PROCESS:
			case K_DICTIONARY:
			case K_TUPLE:  {				
				if(fromSign || toSign) {					
					// nary nodes
					int[] fromChildren = fromState.children;
					int[] toChildren = toState.children;
					if (fromChildren.length != toChildren.length) {
						return false;
					}
					boolean andChildren = true;
					boolean orChildren = false;
					for (int i = 0; i < fromChildren.length; ++i) {
						int fromChild = fromChildren[i];
						int toChild = toChildren[i];
						boolean v = intersection(fromChild, fromSign, toChild,
								toSign);	
						andChildren &= v;
						orChildren |= v;						
					}
					if(!fromSign || !toSign) {
						return orChildren;
					} else {
						return andChildren;
					}
				}
				return true;
			}
			case K_RECORD: {				
				if(fromSign || toSign) {					
					int[] fromChildren = fromState.children;
					int[] toChildren = toState.children;
					if (fromChildren.length != toChildren.length) {
						return !fromSign || !toSign;
					}				
					ArrayList<String> fromFields = (ArrayList<String>) fromState.data;
					ArrayList<String> toFields = (ArrayList<String>) toState.data;				
					boolean andChildren = true;
					boolean orChildren = false;
					for (int i = 0; i != fromFields.size(); ++i) {
						String e1 = fromFields.get(i);
						String e2 = toFields.get(i);
						if(!e1.equals(e2)) { return !fromSign || !toSign; }
						int fromChild = fromChildren[i];
						int toChild = toChildren[i];
						boolean v = intersection(fromChild, fromSign, toChild,
								toSign);
						andChildren &= v;
						orChildren |= v;
					}
					if(!fromSign || !toSign) {
						return orChildren;
					} else {
						return andChildren;
					}
				}
				return true;
			}
			case K_NEGATION: 
			case K_UNION : 
			case K_INTERSECTION:
					// let these cases fall through to if-statements after
					// switch.
				break;
			// === Heterogenous Compound States ===
			case K_FUNCTION:
			case K_HEADLESS:
			case K_METHOD:
				if(fromSign || toSign) {
					// nary nodes
					int[] fromChildren = fromState.children;
					int[] toChildren = toState.children;
					if(fromChildren.length != toChildren.length){
						return false;
					}
					
					int recIndex = fromKind == Type.K_METHOD ? 0 : -1;					
					int retIndex = fromKind == Type.K_METHOD ? 1 : 0;
					boolean andChildren = true;
					boolean orChildren = false;					
					for(int i=0;i<fromChildren.length;++i) {
						boolean v;
						if(i == recIndex) {
							// receiver type is invariant
							// FIXME: make receiver invariant!
							v = intersection(fromChildren[i], !fromSign,
									toChildren[i], !toSign);
						} else if(i == retIndex) {
							// return type is co-variant
							v = intersection(fromChildren[i], fromSign,
									toChildren[i], toSign);
						} else {
							// parameter type(s) are contra-variant
							v = intersection(fromChildren[i], !fromSign,
								toChildren[i], !toSign);
						}
						andChildren &= v;
						orChildren |= v;
					}
					if(!fromSign || !toSign) {
						return orChildren;
					} else {
						return andChildren;
					}
				}
				return true;
			default:
				return fromSign == toSign;
			}
		} 
		
		if(fromKind == K_NEGATION) {
			int fromChild = fromState.children[0];
			return intersection(fromChild,!fromSign,toIndex,toSign);
		} else if(toKind == K_NEGATION) {
			int toChild = toState.children[0];
			return intersection(fromIndex,fromSign,toChild,!toSign);			
		}
		
		// using invert helps reduce the number of cases to consider.
		fromKind = invert(fromKind,fromSign);
		toKind = invert(toKind,toSign);		
				
		if(fromKind == K_VOID || toKind == K_VOID){
			return false;
		} else if(fromKind == K_UNION) {			
			int[] fromChildren = fromState.children;		
			for(int i : fromChildren) {				
				if(intersection(i,fromSign,toIndex,toSign)) {
					return true;
				}								
			}
			return false;	
		} else if(toKind == K_UNION) {
			int[] toChildren = toState.children;		
			for(int j : toChildren) {
				if(intersection(fromIndex,fromSign,j,toSign)) {
					return true;
				}											
			}
			return false;	
		} else if(fromKind == K_INTERSECTION) {
			int[] fromChildren = fromState.children;			
			for (int i : fromChildren) {				
				if(!intersection(i,fromSign,toIndex,toSign)) {
					return false;
				}											
			}
			return true;	
		} else if(toKind == K_INTERSECTION) {
			int[] toChildren = toState.children;					
			for (int j : toChildren) {				
				if(!intersection(fromIndex,fromSign,j,toSign)) {
					return false;
				}											
			}			
			return true;	
		} else if(fromKind == K_ANY || toKind == K_ANY){
			return true;
		}  
		
		return !fromSign || !toSign;		
	}
	
	private int invert(int kind, boolean sign) {
		if(sign) {
			return kind;
		}
		switch(kind) {
			case K_ANY:
				return K_VOID;
			case K_VOID:
				return K_ANY;
			case K_UNION:
				return K_INTERSECTION;
			case K_INTERSECTION:
				return K_UNION;
			default:
				return kind;
		}		
	}
	
	private void setIntersection(int fromIndex, boolean fromSign,
			int toIndex, boolean toSign, boolean value) {
		if(fromSign) {
			fromIndex += from.size();
		}
		if(toSign) {
			toIndex += to.size();
		}
		
{'fraction_non_alphanumeric': 0.11816181618161817, 'fraction_numerical': 0.004500450045004501, 'mean_word_length': 2.795596887454925, 'pattern_counts': {'":': 0, '<': 116, '<?xml version=': 0, '>': 112, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2875392', 'n_tokens_mistral': 8159, 'n_tokens_neox': 6275, 'n_words': 1702}