LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
cartesianproducts [2007/10/05 01:48]
philippe.suter 		cartesianproducts [2015/04/21 17:42]
wikiadmin [Using sets]
Line 17: Line 17:
  
 We would have the following properties on the corresponding sets: We would have the following properties on the corresponding sets:
-\[ Node \subseteq Tree \] +\begin{equation*} ​Node \subseteq Tree \end{equation*} 
-\[ Leaf \subseteq Tree \] +\begin{equation*} ​Leaf \subseteq Tree \end{equation*} 
-\[ Node \cup Leaf = Tree \] +\begin{equation*} ​Node \cup Leaf = Tree \end{equation*} 
-\[ Node \cap Leaf = \emptyset \]+\begin{equation*} ​Node \cap Leaf = \emptyset \end{equation*}
  
 === Extractors === === Extractors ===
Line 38: Line 38:
  
 ...would have their corresponding sets: ...would have their corresponding sets:
-\[ ENode \subseteq Node \] +\begin{equation*} ​ENode \subseteq Node \end{equation*} 
-\[ ELeaf \subseteq Leaf \]+\begin{equation*} ​ELeaf \subseteq Leaf \end{equation*}
  
 Now, a user could want to indicate that ENode not only matches Node'​s,​ but actually matches **all** of them (same for ELeaf of Leaf'​s). He would **need** to specify the following constraints:​ Now, a user could want to indicate that ENode not only matches Node'​s,​ but actually matches **all** of them (same for ELeaf of Leaf'​s). He would **need** to specify the following constraints:​
-\[ ENode \supseteq Node \] +\begin{equation*} ​ENode \supseteq Node \end{equation*} 
-\[ ELeaf \supseteq Leaf \]+\begin{equation*} ​ELeaf \supseteq Leaf \end{equation*}
  
 (Note that we then have equality between the sets of the extractors and their corresponding types. This is the situation we have with case classes.) (Note that we then have equality between the sets of the extractors and their corresponding types. This is the situation we have with case classes.)
Line 65: Line 65:
  
 This is readily expressible thanks to the set operators: This is readily expressible thanks to the set operators:
-\[EvenNode \cap OddNode = \emptyset \] +\begin{equation*}EvenNode \cap OddNode = \emptyset \end{equation*} 
-\[EvenNode \cup OddNode = Node \]+\begin{equation*}EvenNode \cup OddNode = Node \end{equation*}
  
 ==== Analyzing patterns ==== ==== Analyzing patterns ====
Line 173: Line 173:
  
 Both these approaches are conservative:​ they may prompt unnecessary warnings due to false negatives, but won't let any incomplete or non-disjoint expression go through unnoticed. Both these approaches are conservative:​ they may prompt unnecessary warnings due to false negatives, but won't let any incomplete or non-disjoint expression go through unnoticed.
 +
  
  
Line 180: Line 181:
 Nested pattern matching seem to occur frequently enough in practice (at least in the world of case classes in Scala, possibly in OCaml as well) to give it a thought. The potential problem if we analyze nested pattern with taking only into consideration the type of the scrutinee, is that we miss a substantial part of the information about the __shape__ of the scrutinee. Indeed, by the simple fact that it matched the pattern where it is nested is a crucial fact. Viktor gave the following example: Nested pattern matching seem to occur frequently enough in practice (at least in the world of case classes in Scala, possibly in OCaml as well) to give it a thought. The potential problem if we analyze nested pattern with taking only into consideration the type of the scrutinee, is that we miss a substantial part of the information about the __shape__ of the scrutinee. Indeed, by the simple fact that it matched the pattern where it is nested is a crucial fact. Viktor gave the following example:
  
-<​code>​+<​code ​ocaml>
 match t with match t with
 | Leaf -> ... | Leaf -> ...
Line 196: Line 197:
 In the following example: In the following example:
  
-<​code ​language="​java">+<code java>
 t: Tree match { t: Tree match {
   case Node(Node(_,​_,​_),​ _, _) => t match {   case Node(Node(_,​_,​_),​ _, _) => t match {
Line 207: Line 208:
  
 We would build the two sets: We would build the two sets:
 +
 $P_1 = Node \times Node \times Leaf$ and $P_1 = Node \times Node \times Leaf$ and
-$P_2 = Node \times Node \times Node$ for the patterns of the nested expression, and the set+ 
 +$P_2 = Node \times Node \times Node$ for the patterns of the nested expression, 
 + 
 +and the set 
 $P_0 = Node \times Node \times Tree$ for the outer pattern. $P_0 = Node \times Node \times Tree$ for the outer pattern.
  
Line 214: Line 220:
  
 This approach works for expressions which use more and less restrictive patterns alike. We can also generalize the approach to expressions nested more deeply: when computing the cartesian products, we take into account all the patterns which had to be followed to reach the expression we're analyzing, then we use the intersection of the ones which are not part of that expression as the set of values for the scrutinee. This approach works for expressions which use more and less restrictive patterns alike. We can also generalize the approach to expressions nested more deeply: when computing the cartesian products, we take into account all the patterns which had to be followed to reach the expression we're analyzing, then we use the intersection of the ones which are not part of that expression as the set of values for the scrutinee.
 +
 +=== In "​if"​ expressions ===
 +
 +So far, our only plan for "​if"​ expressions is to use whatever information we find about the __type__ of the scrutinee as an axiom for the analysis.