Skip to content

contificate/match

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

23 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Implementation of the match compilation algorithm described in Maranget's Compiling Pattern Matching to Good Decision Trees with DAG construction inspired by Pettersson's A Term Pattern-Match Compiler Inspired by Finite Automata Theory.


The algorithm processes (typed) patterns into a pattern matrix and continually specialises the matrix based on the constructors present in the left-most column. Each specialisation corresponds to adding an edge in the decision tree (labelled with the associated constructor's tag). To avoid duplication, the decision "tree" is really constructed as a DAG by means of hash consing.


Examples

match v with
| Some (Nil, _) -> 0
| Some (_, Nil) -> 1
| Some (Cons (x, xs), Cons (y, xs)) -> 2
| None -> 3

first decision dag

match v with
| (_, False, True) -> 0
| (False, True, _) -> 1
| (_, _, False)-> 2
| (_, _, True) -> 3

second decision dag

match v with
| (Black, T (Red, T (Red, a, x, b), y, c), z, d) -> 0
| (Black, T (Red, a, x, T (Red, b, y, c)), z, d) -> 1
| (Black, a, x, T (Red, T (Red, b, y, c), z, d)) -> 2
| (Black, a, x, T (Red, b, y, T (Red, c, z, d))) -> 3
| _ -> 4

third decision dag


user interface tool