-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Practical typed lazy contracts.
--   
--   Contracts describe properties of expressions (esp. functions) that are
--   checked at run-time. For example, a contract states that an expression
--   is a natural number, a list has at least one element or a function
--   requires a natural number and a non-empty list of natural numbers as
--   arguments and will produce a natural number as result. Thus these
--   properties are both documented and enforced. Contracts are more
--   expressive than static types. If a contract is violated, then an
--   informative exception is raised. See homepage or Olaf Chitil:
--   <a>Practical Typed Lazy Contracts</a>, ICFP 2012, ACM.
@package Contract
@version 0.1


-- | Practical typed lazy contracts. Author: Olaf Chitil. Version: July
--   2012.
--   
--   Contracts describe properties of expressions (esp. functions) that are
--   checked at run-time. Thus these properties are both documented and
--   enforced. Contracts are more expressive than static types. If a
--   contract is violated, then an informative exception is raised.
--   
--   Example uses:
--   
--   <pre>
--   head' = $attach head (pNotNil &gt;-&gt; true)
--   </pre>
--   
--   <pre>
--   nat :: (Integral a, Flat a) =&gt; Contract a
--   nat = prop (&gt;=0)
--   fibs = $assert (list nat) (0 : 1 : zipWith (+) fibs (tail fibs))
--   </pre>
--   
--   <pre>
--   conjNF = $(p ’And) conjNF conjNF |&gt; disj
--   disj   = $(p ’Or)  disj disj |&gt; lit
--   lit    = $(p ’Not) atom |&gt; atom
--   atom   = $(p ’Atom) true
--   clausalNF' = $attach clausalNF (conjNF &amp; right &gt;-&gt; list (list lit))
--   </pre>
--   
--   See <a>http://www.cs.kent.ac.uk/~oc/contracts.html</a> or Olaf Chitil:
--   Practical Typed Lazy Contracts, ICFP 2012, ACM.
--   
--   Any user module will need Template Haskell. They will also need
--   DeriveDataTypeable, if they use the deriving combinators for algebraic
--   data types: <a>p</a>, <a>pNot</a> or <a>deriveContracts</a>.
module Development.Contract

-- | The contract type.
data Contract a

-- | The exception raised when a contact fails.
data ContractFailed
ContractFailed :: Partner -> Loc -> String -> ContractFailed
culprit :: ContractFailed -> Partner
loc :: ContractFailed -> Loc
explanation :: ContractFailed -> String

-- | Different contract partners. For any violated contract a partner is
--   blamed.
data Partner
Server :: Partner
Client :: Partner
Contract :: Partner

-- | Connect a contract with an expression. The resulting expression is the
--   same except that the contract is monitored for it at runtime. assert
--   splices in code that adds the current location in the module file.
--   
--   <pre>
--   $assert :: Contract a -&gt; a -&gt; a
--   </pre>
assert :: Q Exp

-- | Same as assert with arguments swapped. Useful for attaching contracts
--   in simple variable definitions: fun' = $attach fun contract
--   
--   <pre>
--   $attach :: a -&gt; Contract a -&gt; a
--   </pre>
attach :: Q Exp

-- | Conjunction of two contracts.
(&) :: Contract a -> Contract a -> Contract a

-- | Disjunction of contracts, given priority to first.
(|>) :: Contract a -> Contract a -> Contract a

-- | Function contract combinator, taking contracts for pre- and
--   post-condition.
(>->) :: Contract a -> Contract b -> Contract (a -> b)

-- | Dependent function contract combinator. The post-condition also takes
--   the function argument. Warning: This combinator does <i>not</i>
--   protect laziness!
(>>->) :: Contract a -> (a -> Contract b) -> Contract (a -> b)

-- | Contract that always succeeds.
true :: Contract a

-- | Contract that always fails, blaming the client.
false :: Contract a

-- | Class of all flat types, for which contract prop works.
--   
--   A type is flat if its only partial value is bottom / undefined. In
--   other words: an expression of the type is either unevaluted or fully
--   evaluated, never properly partially evaluated.
class Show a => Flat a where prop p = C (\ b l e x -> if p x then Right x else cFail b (show x))
prop :: Flat a => (a -> Bool) -> Contract a

-- | Pattern contract for given constructor. The argument must be the name
--   of a data constructor. E.g. $(p 'Left)
p :: Name -> ExpQ

-- | Negated pattern contract for a given constructor. The argument must be
--   the name of a data constructor. E.g. $(pNot 'Left)
pNot :: Name -> ExpQ

-- | For a given algebraic data type declare pattern contracts for all
--   constructors. The argument must be the name of an algebraic data type.
--   E.g. $(deriveContracts ''Either)
deriveContracts :: Name -> Q [Dec]

-- | Drop context information in a contract to avoid unbound context
--   growth. Can be wrapped around any context.
dropContext :: Contract a -> Contract a

-- | Contract for empty list.
pNil :: Contract [a]

-- | Contract combinator for non-empty list. Cf. (:) :: a -&gt; [a] -&gt;
--   [a]
pCons :: Contract a -> Contract [a] -> Contract [a]

-- | Alternative name for <a>pCons</a>.
(=:) :: Contract a -> Contract [a] -> Contract [a]

-- | Contract for non-empty list.
pNotNil :: Contract [a]

-- | Contract for not non-empty list, i.e., empty list.
pNotCons :: Contract [a]

-- | Contract combinator for list with elements meeting given contract.
list :: Contract a -> Contract [a]

-- | Contract combinator for IO-monad with return value meeting given
--   contract.
io :: Contract a -> Contract (IO a)

-- | Contract for empty tuple.
pTuple0 :: Contract ()

-- | Contract combinator for tuple with values meeting given contracts.
pTuple2 :: Contract a -> Contract b -> Contract (a, b)

-- | Contract combinator for 3-tuple with values meeting given contracts.
pTuple3 :: Contract a -> Contract b -> Contract c -> Contract (a, b, c)

-- | Contract combinator for 4-tuple with values meeting given contracts.
pTuple4 :: Contract a -> Contract b -> Contract c -> Contract d -> Contract (a, b, c, d)

-- | Contract for data constructor <a>Nothing</a>.
pNothing :: Contract (Maybe a)

-- | Contract combinator for data constructor <a>Just</a> with value
--   meeting given contract.
pJust :: Contract a -> Contract (Maybe a)

-- | Contract for non-<a>Nothing</a> value.
pNotNothing :: Contract (Maybe a)

-- | Contract for non-<a>Just</a> value.
pNotJust :: Contract (Maybe a)

-- | Contract combinator for type <a>Maybe</a> given contract for possible
--   argument value.
maybe :: Contract a -> Contract (Maybe a)
instance Typeable ContractFailed
instance Flat Bool
instance Flat Char
instance Flat Double
instance Flat Float
instance Flat Integer
instance Flat Int
instance Lift Loc
instance Show Partner
instance Exception ContractFailed
instance Show ContractFailed