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


-- | Compile time checks that a computation considers producing data through all possible constructors
--   
--   For a brief tutorial to <tt>exhaustive</tt>, check out the
--   documentation for <a>Control.Exhaustive</a>, which contains a small
--   example.
@package exhaustive
@version 1.1.6


-- | <tt>exhaustive</tt> is a library that guarantees that when building a
--   parser, or some other computation that produces data, <i>all</i>
--   possible constructors in a data type are considered. You can think of
--   this library as providing a symmetry to GHC's built in
--   <tt>-fwarn-incomplete-patterns</tt> compile time warning, although
--   this library is stricter in that it produces compile time errors if a
--   constructor is omitted.
--   
--   Usage of this library is intended to be straightforward, though
--   admittedly the types might have you think the opposite! To understand
--   this library, an example may be helpful.
--   
--   To begin with, consider a simple data type for a "boolean expressions"
--   language:
--   
--   <pre>
--   import qualified <a>GHC.Generics</a> as GHC
--   
--   data Expr
--     = ETrue
--     | EFalse
--     | EIf Expr Expr Expr
--     deriving (<a>Eq</a>, GHC.<a>Generic</a>)
--   instance <a>Generic</a> Expr
--   </pre>
--   
--   Note that we have to make our data type an instance of both
--   <a>GHC.Generics</a>.<a>Generic</a> <i>and</i>
--   <a>Generics.SOP</a>.<a>Generic</a>, though this only requires
--   boiler-plate code.
--   
--   Next, we would like to build a parser for this language. Let's assume
--   that we have access to a <tt>parsec</tt>-like library, where we have
--   one basic combinator:
--   
--   <ul>
--   <li><pre>symbol :: <a>String</a> -&gt; Parser <a>String</a></pre></li>
--   </ul>
--   
--   Ordinarily, we would write our parser as
--   
--   <pre>
--   parseExpr :: Parser Expr
--   parseExpr = <a>msum</a> [ETrue <a>&lt;$</a> symbol "True"
--                    ,EFalse <a>&lt;$</a> symbol "False"
--                    ,EIf <a>&lt;$&gt;</a> symbol "if" <a>*&gt;</a> parseExpr
--                         <a>&lt;*&gt;</a> symbol "then" <a>*&gt;</a> parseExpr
--                         <a>&lt;*&gt;</a> symbol "else" <a>*&gt;</a> parseExpr
--                    ]
--   </pre>
--   
--   However, nothing is making sure that we actually considered all
--   constructors in <tt>Expr</tt>. We could just as well write
--   
--   <pre>
--   parseExpr :: Parser Expr
--   parseExpr = <a>msum</a> [ETrue <a>&lt;$</a> symbol "True"
--                    ,EFalse <a>&lt;$</a> symbol "False"]
--   </pre>
--   
--   Although this is significantly less useful!
--   
--   Using <tt>exhaustive</tt>, we can get exhaustivity checks that we are
--   at least considering all constructors:
--   
--   <pre>
--   <a>makeExhaustive</a> ''Expr
--   
--   parseExpr :: Parser Expr
--   parseExpr =
--     <a>produceFirst</a> <a>$</a>
--       $(<a>con</a> 'ETrue) <a>&lt;$</a> symbol "True" <a>&amp;:</a>
--       $(<a>con</a> 'EFalse) <a>&lt;$</a> symbol "False" <a>&amp;:</a>
--       $(<a>con</a> 'EIf) <a>&lt;$&gt;</a> (symbol "if" <a>*&gt;</a> parseExpr)
--                   <a>&lt;*&gt;</a> (symbol "then" <a>*&gt;</a> parseExpr)
--                   <a>&lt;*&gt;</a> (symbol "else" <a>*&gt;</a> parseExpr) <a>&amp;:</a>
--       <a>finish</a>
--   </pre>
--   
--   As you can hopefully see, <tt>exhaustive</tt> requires only minimal
--   changes to an existing parser. Specifically, we need to:
--   
--   <ol>
--   <li>Use <a>produceFirst</a> instead of <a>msum</a></li>
--   <li>Wrap each constructor application with the Template Haskell
--   function <a>con</a>. Note that you also need to quote the name of the
--   constructor with a single <tt>'</tt>.</li>
--   <li>Use <a>&amp;:</a> to combine constructors, rather than list
--   notation.</li>
--   <li>Explicitly state you are <a>finish</a>ed.</li>
--   <li>Add a call to <a>makeExhaustive</a> on our original data
--   type.</li>
--   </ol>
module Control.Exhaustive

-- | <a>con</a> builds a <a>Construction</a> for a single constructor of a
--   data type. Unfortunately, as this function is used via Template
--   Haskell, the type is not particularly informative -- though you can
--   think of the produced function having roughly the same type as the
--   original constructor. To clarify this, it's helpful to look at the
--   type of <a>con</a> applications:
--   
--   <pre>
--   $(<a>con</a> '<a>Nothing</a>) :: Construction 1 '[]
--   $(<a>con</a> '<a>Just</a>) :: a -&gt; Construction 2 '[a]
--   
--   data Record = Record { a :: String, b :: Int, c :: Char }
--   $(<a>con</a> 'Record) :: String -&gt; Int -&gt; Char -&gt; Construction 1 '[String, Int, Char]
--   </pre>
--   
--   For more examples of <a>con</a>, see the module documentation at the
--   top of this page.
con :: Name -> Q Exp

-- | Combine multiple <a>Construction</a>s into a list of constructions for
--   a data type. This function is a lot like <tt>:</tt> for lists, but the
--   types carry considerably more information.
--   
--   The type <tt>n</tt> is used to carry the index of the constructor in
--   the list of constructors in the data type, while <tt>xs</tt> is a list
--   of types that are the fields of that constructor.
--   
--   The constraint on this function forces <a>&amp;:</a> to be used to
--   produce in-order constructors. It may help to see this function
--   through an example:
--   
--   Given <tt>data Bool = True | False</tt>, we have two constructors.
--   <tt>True</tt> has index 1, while the <i>code</i> for this data type
--   has length 2 (as there are two constructors in total). Therefore after
--   using the <tt>True</tt> constructor we have to use one more
--   constructor. When we construct using <tt>False</tt> we are done, as
--   the only way to satisfy the equation <tt>2 + x = 2</tt> is to provide
--   <tt>x = 0</tt> -- the empty list.
(&:) :: (Functor f, Length code ~ (n + Length xs)) => f (Construction n x) -> NP (ConstructorApplication f code) xs -> NP (ConstructorApplication f code) (x : xs)
infixr 3 &:

-- | Assert that you have now used all constructors and are finished. If
--   you've made mistake, be prepared for a rather impressive type error!
finish :: NP f '[]

-- | Build a list of computations, one for each constructor in a data type.
produceM :: (code ~ Code a, Generic a, Applicative f) => NP (ConstructorApplication f code) code -> [f a]

-- | Keep attempting to construct a data type until a constructor succeeds.
--   The first constructor to successfully be constructed (in the order
--   defined in the original data type) will be returned, or <a>empty</a>
--   if all constructions fail.
produceFirst :: (code ~ Code a, Generic a, Alternative f) => NP (ConstructorApplication f code) code -> f a

-- | Produce all successful constructions of a data-type. If any
--   constructors fail, they will not be included in the resulting list. If
--   all constructors fail, this will return <a>pure</a> <tt>[]</tt>.
produceAll :: (code ~ Code a, Generic a, Alternative f) => NP (ConstructorApplication f code) code -> f [a]

-- | Signify that you will be performing exhaustive construction of a
--   specific data type:
--   
--   <pre>
--   data Expr = ETrue | EFalse
--   makeExhaustive ''Expr
--   </pre>
--   
--   <a>makeExhaustive</a> doesn't introduce any new symbols into scope,
--   but it forces an environment change, allowing you to write <tt>$(con
--   'ETrue)</tt>. If you are already using other Template Haskell routines
--   (such as <tt>makeLenses</tt>) then you can omit this call.
makeExhaustive :: Name -> Q [a]

-- | A <a>ConstructorApplication</a> is a lifted function (in the terms of
--   <tt>generics-sop</tt>) that instantiates a particular constructor of a
--   data type, possibly using the side-effects provided by <tt>f</tt>.
--   
--   To create and use <a>ConstructorApplication</a>s, use <a>&amp;:</a>.
type ConstructorApplication f code = Injection (NP I) code -.-> K (f (NS (NP I) code))

-- | A <a>Construction</a> is an internal representation of a data type
--   constructor. This type is indexed by a natural number, which
--   represents the constructor number, and the list of types of fields of
--   this constructor.
--   
--   To create a <a>Construction</a>, use <a>con</a>.
data Construction :: Nat -> [*] -> *

-- | Compute the length of a type level list.
