Safe Haskell	Safe
Language	Haskell2010

Otter.Rule

Synopsis

newtype Rule a b = Rule {
- unRule :: Maybe (Either b (a -> Rule a b))
}
type ProperRule a b = a -> Rule a b
match :: (a -> Maybe b) -> Rule a b
apply :: ProperRule a b -> a -> ([b], [ProperRule a b])
arrowDimap :: (a -> b) -> (c -> d) -> (b -> c) -> a -> d
relDimap :: (a -> b) -> (c -> d) -> Rule b c -> Rule a d

Documentation

newtype Rule a b Source #

An inference rule schema is just a curried n-ary function where n is an unbounded, unspecified number of input premises, possibly zero (in that case, the rule is an axiom). A Rule element may represent three possible situations:

A failing computation which produces nothing; this is the degenerate case of a rule schema that always fails to match, and also what enables to make Rule an instance of Alternative, MonadPlus, and MonadFail.
A successful computation that produces a 0-ary function, i.e. an axiom;
A successful computation that produces a unary function, that is, a function accepting one argument and possibly returning a new Rule. Applying such a function to an input corresponds to "matching" the first premise of the rule schema against a candidate input. The result is either a matching failure or a new, partially applied rule.

Constructors

Rule
Fields unRule :: Maybe (Either b (a -> Rule a b))

Instances

Monad (Rule a) Source #
Instance details Defined in Otter.Rule Methods (>>=) :: Rule a a0 -> (a0 -> Rule a b) -> Rule a b # (>>) :: Rule a a0 -> Rule a b -> Rule a b # return :: a0 -> Rule a a0 # fail :: String -> Rule a a0 #
Functor (Rule a) Source #
Instance details Defined in Otter.Rule Methods fmap :: (a0 -> b) -> Rule a a0 -> Rule a b # (<$) :: a0 -> Rule a b -> Rule a a0 #
MonadFail (Rule a) Source #
Instance details Defined in Otter.Rule Methods fail :: String -> Rule a a0 #
Applicative (Rule a) Source #
Instance details Defined in Otter.Rule Methods pure :: a0 -> Rule a a0 # (<>) :: Rule a (a0 -> b) -> Rule a a0 -> Rule a b # liftA2 :: (a0 -> b -> c) -> Rule a a0 -> Rule a b -> Rule a c # (>) :: Rule a a0 -> Rule a b -> Rule a b # (<*) :: Rule a a0 -> Rule a b -> Rule a a0 #
Alternative (Rule a) Source #
Instance details Defined in Otter.Rule Methods empty :: Rule a a0 # (<\|>) :: Rule a a0 -> Rule a a0 -> Rule a a0 # some :: Rule a a0 -> Rule a [a0] # many :: Rule a a0 -> Rule a [a0] #
MonadPlus (Rule a) Source #
Instance details Defined in Otter.Rule Methods mzero :: Rule a a0 # mplus :: Rule a a0 -> Rule a a0 -> Rule a a0 #

type ProperRule a b = a -> Rule a b Source #

match :: (a -> Maybe b) -> Rule a b Source #

Constructs a single-premise rule from a matching function.

apply :: ProperRule a b -> a -> ([b], [ProperRule a b]) Source #

arrowDimap :: (a -> b) -> (c -> d) -> (b -> c) -> a -> d Source #

relDimap :: (a -> b) -> (c -> d) -> Rule b c -> Rule a d Source #