Copyright | Copyright (c) 2016 the Hakaru team |
---|---|

License | BSD3 |

Maintainer | wren@community.haskell.org |

Stability | experimental |

Portability | GHC-only |

Safe Haskell | None |

Language | Haskell2010 |

Reduction of case analysis on user-defined data types.

- data MatchResult ast abt a
- type DatumEvaluator ast m = forall t. ast (HData' t) -> m (Maybe (Datum ast (HData' t)))
- matchBranches :: (ABT Term abt, Monad m) => DatumEvaluator ast m -> ast a -> [Branch a abt b] -> m (Maybe (MatchResult ast abt b))
- matchBranch :: (ABT Term abt, Monad m) => DatumEvaluator ast m -> ast a -> Branch a abt b -> m (Maybe (MatchResult ast abt b))
- data MatchState ast vars
- matchTopPattern :: Monad m => DatumEvaluator ast m -> ast a -> Pattern vars a -> List1 Variable vars -> m (Maybe (MatchState ast '[]))
- matchPattern :: Monad m => DatumEvaluator ast m -> ast a -> Pattern vars1 a -> List1 Variable (vars1 ++ vars2) -> m (Maybe (MatchState ast vars2))
- viewDatum :: ABT Term abt => abt '[] (HData' t) -> Maybe (Datum (abt '[]) (HData' t))

# External API

data MatchResult ast abt a Source #

GotStuck | Our |

Matched !(Assocs ast) !(abt '[] a) | We successfully matched everything. The first argument
gives the substitution for all the pattern variables. The
second argument gives the body of the branch matched. N.B.,
the substitution maps variables to some type N.B., because the substitution may not have the right type (and because we are lazy), we do not perform substitution. Thus, the body has "free" variables which are defined/bound in the association list. It's up to callers to perform the substitution, push the assocs onto the heap, or whatever. |

type DatumEvaluator ast m = forall t. ast (HData' t) -> m (Maybe (Datum ast (HData' t))) Source #

A function for trying to extract a `Datum`

from an arbitrary
term. This function is called every time we enter the `matchPattern`

function. If this function returns `Nothing`

then the final
`MatchResult`

will be `GotStuck`

; otherwise, this function returns
`Just`

some `Datum`

that we can take apart to continue matching.

We don't care anything about the monad `m`

, we just order the
effects in a top-down left-to-right manner as we traverse the
pattern. However, do note that we may end up calling this evaluator
repeatedly on the same argument, so it should be sufficiently
idempotent to work under those conditions. In particular,
`matchBranches`

will call it once on the top-level scrutinee for
each branch. (We should fix that, but it'll require using pattern
automata rather than a list of patterns/branches.)

TODO: we could change this from returning `Maybe`

to returning
`Either`

, that way the evaluator could give some reason for its
failure (we would store it in the `GotStuck`

constructor).

matchBranches :: (ABT Term abt, Monad m) => DatumEvaluator ast m -> ast a -> [Branch a abt b] -> m (Maybe (MatchResult ast abt b)) Source #

Walk through a list of branches and try matching against them
in order. We just call `matchBranches`

repeatedly, and return
the first non-failure.

matchBranch :: (ABT Term abt, Monad m) => DatumEvaluator ast m -> ast a -> Branch a abt b -> m (Maybe (MatchResult ast abt b)) Source #

Try matching against a single branch. This function is a thin
wrapper around `matchTopPattern`

; we just take apart the `Branch`

to extract the pattern, list of variables to bind, and the body
of the branch.

# Internal API

data MatchState ast vars Source #

The internal version of `MatchResult`

for giving us the properly
generalized inductive hypothesis.

GotStuck_ | Our |

Matched_ (DList (Assoc ast)) (List1 Variable vars) | We successfully matched everything (so far). The first argument gives the bindings for all the pattern variables we've already checked. The second argument gives the pattern variables remaining to be bound by checking the rest of the pattern. |

matchTopPattern :: Monad m => DatumEvaluator ast m -> ast a -> Pattern vars a -> List1 Variable vars -> m (Maybe (MatchState ast '[])) Source #

Try matching against a (top-level) pattern. This function is
a thin wrapper around `matchPattern`

in order to restrict the
type.

matchPattern :: Monad m => DatumEvaluator ast m -> ast a -> Pattern vars1 a -> List1 Variable (vars1 ++ vars2) -> m (Maybe (MatchState ast vars2)) Source #

Try matching against a (potentially nested) pattern. This
function generalizes `matchTopPattern`

, which is necessary for
being able to handle nested patterns correctly. You probably
don't ever need to call this function.