Matcher

Matches a quoted tree against a quoted pattern tree. A quoted pattern tree may have type and term holes in addition to normal terms.

Semantics:

We use '{..} for expression, '[..] for types and ⟨..⟩ for patterns nested in expressions. The semantics are defined as a list of reduction rules that are tried one by one until one matches.

Operations: - s =?= p checks if a scrutinee s matches the pattern p while accumulating extracted parts of the code. - isColosedUnder(x1, .., xn)('{e}) returns true if and only if all the references in e to names defined in the patttern are contained in the set {x1, ... xn}. - lift(x1, .., xn)('{e}) returns (y1, ..., yn) => [xi = $yi]'{e} where yi is an Expr of the type of xi. - withEnv(x1 -> y1, ..., xn -> yn)(matching) evaluates mathing recording that xi is equivalent to yi. - matched denotes that the the match succedded and matched('{e}) denotes that a matech succeded and extracts '{e} - &&& matches if both sides match. Concatenates the extracted expressions of both sides.

Note: that not all quoted terms bellow are valid expressions

/* Term hole */
'{ e } =?= '{ hole[T] }  &&  typeOf('{e}) <:< T && isColosedUnder()('{e})  ===>   matched('{e})

/* Higher order term hole */
'{ e } =?= '{ hole[(T1, ..., Tn) => T](x1, ..., xn) }  &&  isColosedUnder(x1, ... xn)('{e})  ===>   matched(lift(x1, ..., xn)('{e}))

/* Match literal */
'{ lit } =?= '{ lit }   ===>   matched

/* Match type ascription (a) */
'{ e: T } =?= '{ p }   ===>   '{e} =?= '{p}

/* Match type ascription (b) */
'{ e } =?= '{ p: P }   ===>   '{e} =?= '{p}

/* Match selection */
'{ e.x } =?= '{ p.x }   ===>   '{e} =?= '{p}

/* Match reference */
'{ x } =?= '{ x }   ===>   matched

/* Match application */
'{e0(e1, ..., en)} =?= '{p0(p1, ..., p2)}   ===>   '{e0} =?= '{p0} &&& '{e1} =?= '{p1} &&& ... %% '{en} =?= '{pn}

/* Match type application */
'{e[T1, ..., Tn]} =?= '{p[P1, ..., Pn]}   ===>   '{e} =?= '{p} &&& '[T1] =?= '{P1} &&& ... %% '[Tn] =?= '[Pn]

/* Match block flattening */
'{ {e0; e1; ...; en}; em } =?= '{ {p0; p1; ...; pm}; em }   ===>   '{ e0; {e1; ...; en; em} } =?= '{ p0; {p1; ...; pm; em} }

/* Match block */
'{ e1; e2 } =?= '{ p1; p2 }   ===>   '{e1} =?= '{p1} &&& '{e2} =?= '{p2}

/* Match def block */
'{ e1; e2 } =?= '{ p1; p2 }   ===>   withEnv(symOf(e1) -> symOf(p1))('{e1} =?= '{p1} &&& '{e2} =?= '{p2})

/* Match if */
'{ if e0 then e1 else e2 } =?= '{ if p0 then p1 else p2 }   ===>  '{e0} =?= '{p0} &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2}

/* Match while */
'{ while e0 do e1 } =?= '{ while p0 do p1 }   ===>  '{e0} =?= '{p0} &&& '{e1} =?= '{p1}

/* Match assign */
'{ e0 = e1 } =?= '{ p0 = p1 }   ==>   '{e0} =?= '{p0} &&& '{e1} =?= '{p1}

/* Match new */
'{ new T } =?= '{ new T }   ===>   matched

/* Match this */
'{ C.this } =?= '{ C.this }   ===>   matched

/* Match super */
'{ e.super } =?= '{ p.super }   ===>   '{e} =?= '{p}

/* Match varargs */
'{ e: _* } =?= '{ p: _* }   ===>   '{e} =?= '{p}

/* Match val */
'{ val x: T = e1; e2 } =?= '{ val y: P = p1; p2 }   ===>   withEnv(x -> y)('[T] =?= '[P] &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2})

/* Match def */
'{ def x0(x1: T1, ..., xn: Tn): T0 = e1; e2 } =?= '{ def y0(y1: P1, ..., yn: Pn): P0 = p1; p2 }   ===>   withEnv(x0 -> y0, ..., xn -> yn)('[T0] =?= '[P0] &&& ... &&& '[Tn] =?= '[Pn] &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2})

// Types

/* Match type */
'[T] =?= '[P] && T <:< P   ===>   matched

Supertypes

Members