Copyright	Copyright (c) 2016 the Hakaru team
License	BSD3
Maintainer	wren@community.haskell.org
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Syntax.DatumCase

Contents

External API
Internal API

Description

Reduction of case analysis on user-defined data types.

Synopsis

External API

data MatchResult ast abt a Source #

Constructors

GotStuck

Our DatumEvaluator failed (perhaps in a nested pattern), thus preventing us from continuing case-reduction.

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 ast which is defined by the DatumEvaluator used; it is not necessarily abt '[]! However, the body is definitely abt '[] since thats what a Branch stores after we account for the pattern-bound variables.

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.

Instances

(Show1 Hakaru ast, Show2 Hakaru [Hakaru] abt) => Show1 Hakaru (MatchResult ast abt) Source #
Methods showsPrec1 :: Int -> a i -> ShowS Source # show1 :: a i -> String Source #
(Show1 Hakaru ast, Show2 Hakaru [Hakaru] abt) => Show (MatchResult ast abt a) Source #
Methods showsPrec :: Int -> MatchResult ast abt a -> ShowS # show :: MatchResult ast abt a -> String # showList :: [MatchResult ast abt a] -> ShowS #

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.

Constructors

GotStuck_	Our `DatumEvaluator` failed (perhaps in a nested pattern), thus preventing us from continuing case-reduction.
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.

Instances

Show1 Hakaru ast => Show (MatchState ast vars) Source #
Methods showsPrec :: Int -> MatchState ast vars -> ShowS # show :: MatchState ast vars -> String # showList :: [MatchState ast vars] -> ShowS #

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.

viewDatum :: ABT Term abt => abt '[] (HData' t) -> Maybe (Datum (abt '[]) (HData' t)) Source #

A trivial "evaluation function". If the term is already a Datum_, then we extract the Datum value; otherwise we fail. You can return the result to turn this into an DatumEvaluator.