tip-lib-0.2.2: tons of inductive problems - support library and tools

Safe HaskellNone
LanguageHaskell2010

Tip.Lint

Description

Check that a theory is well-typed.

Invariants:

  • No shadowing---checked by scope monad.
  • Each local is bound before it's used.
  • All expressions are well-typed.
  • The result of each constructor should be a value of that datatype.
  • Default case comes first. No duplicate cases.
  • Expressions and formulas not mixed.

Synopsis

Documentation

lint :: (PrettyVar a, Ord a) => String -> Theory a -> Theory a Source

Crashes if the theory is malformed

lintM :: (PrettyVar a, Ord a, Monad m) => String -> Theory a -> m (Theory a) Source

Same as lint, but returns in a monad, for convenience

lintTheory :: (PrettyVar a, Ord a) => Theory a -> Maybe Doc Source

Returns the error if the theory is malformed

lintEither :: (PrettyVar a, Ord a) => String -> Theory a -> Either Doc (Theory a) Source

Returns a Left if the theory is malformed