In this section, we outline how we do intensional analysis of residual code. We provide a high-level pattern matching based interface. Code patterns can be constructed by placing brackets around code. For example a pattern that matches the literal 5 can be constructed by:
-| fun is5 <5> = true
| is5 _ = false;
val is5 = fn : <int> -> bool
-| is5 (lift (1+4));
val it = true : bool
-| is5 <0>;
val it = false : bool
The function is5 matches its argument to the constant pattern <5> if it succeeds it returns true else false. Pattern variables in code patterns are indicated by escaping variables in the code pattern.
-| fun parts < ~x + ~y > = SOME(x,y)
| parts _ = NONE;
val parts = fn : <int> -> (<int> * <int>) option
-| parts <6 + 7>;
val it = SOME (<6>,<7>) : (<int> * <int>) option
-| parts <2>;
val it = NONE : (<int> * <int>) option
The function parts matches its argument against the pattern
< x + y >. If its argument is a piece of code which
is the sum of two sub terms, it binds the pattern variable
x to the left subterm and the pattern variable y to the right
subterm.
We use higher-order pattern variables[22, 21] for code patterns that contain binding occurrences, such as lambda expressions, let expressions, do expressions, or functions.
For example, a high-order pattern that matches the code of a function <fn x => ...>, of type <'a -> 'b> is written in eta-expanded form <fn x => (g <x>)>. When the pattern matches, the matching binds the higher-order pattern variable g to a function with type <'a> -> <'b>
Every higher order pattern variable must be in fully saturated form, by applying it to all the bound variables of the code pattern. For example if g is a higher-order pattern variable with type <'a> -> <'b> -> <'c> then we must write (g <x> <y>). The arguments to the higher-order pattern variable must be explicit bracketed variables, one for each variable bound in the code pattern at the context where the higher-order pattern appears. A higher-order pattern variable is used like a function on the right-hand side of a matching construct.
For example functions which implement the three monad axioms are written as follows:
fun monad1
<do mswo
{ x <- return mswo ~e
; ~(z <x>) }>
= z e
fun monad2 <do mswo { x <- ~m; return x }> = m
fun monad3
<do mswo
{ x <- do mswo {y <- ~a
; ~(b <y>)}
; ~(c <x> }>
= <do mswo { y' <- ~a
; do mswo { z <- ~(b <y'>)
; ~(c <z>) }}>
When the function monad1 is applied to the code <do mswo {a <- returm mswo (g 3); h(a + 2)}>, the pattern variable e is bound to the function fn x => <h(x + 2)> which has the type <int> -> <int M>. The right-hand side of monad1 rebuilds a new code fragment, substituting formal parameter x of e by <g 3>, constructing the code <h((g 3)+ 2)>.
This technique can be used to build optimizations, or to translate a residual program into a target language.