cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Add support for or-patterns

Open charguer opened this issue 6 years ago • 0 comments

A famous example of a very useful or-pattern is the following balance function from Okasaki's presentation of red-black trees:

   let balance = function
     | (Black, Node (Red, Node (Red, a, x, b), y, c), z, d)
     | (Black, Node (Red, a, x, Node (Red, b, y, c)), z, d) 
     | (Black, a, x, Node (Red, Node (Red, b, y, c), z, d))
     | (Black, a, x, Node (Red, b, y, Node (Red, c, z, d))) ->
       Node (Red, Node (Black, a, x, b), y, Node (Black, c, z, d))
     | (c,a,x,y) -> Node (c,a,x,y)

The encoding of such top-level or-pattern using a function is less pretty:

   let balance t = 
    let k a x b y c z d = Node (Red, Node (Black, a, x, b), y, Node (Black, c, z, d)) in
    match t with
     | (Black, Node (Red, Node (Red, a, x, b), y, c), z, d) -> k a x b y c z d
     | (Black, Node (Red, a, x, Node (Red, b, y, c)), z, d) -> k a x b y c z d
     | (Black, a, x, Node (Red, Node (Red, b, y, c), z, d)) -> k a x b y c z d
     | (Black, a, x, Node (Red, b, y, Node (Red, c, z, d))) -> k a x b y c z d
     | (c,a,x,y) -> Node (c,a,x,y)

In-depth or-patterns are much less frequent in practice. Main use case that I know of is to deal with symmetries. E.g. the pattern (None, Some x) | (Some x, None) occuring in depth. I beleive it is fine to either not support those, or to encode them in a naive manner by lifting the disjunction to the top level (documenting clearly that in the worst case this is exponential in the number of or-clauses appearing in parallel within the same pattern).

charguer avatar Jul 02 '19 14:07 charguer