{- |

This package aims to perform the fiddly details of instantiating induction
schemas for algebraic data types. The library is parameterised over
the type of variables (@v@), constructors (@c@) and types (@t@).

Let's see how it looks if you instantiate all these three with String and want
to do induction over natural numbers. First, one needs to create a type
environment, a `TyEnv`. For every type (we only have one), we need to list its
constructors. For each constructor, we need to list its arguments and whether
they are recursive or not.

>testEnv :: TyEnv String String
>testEnv "Nat" = Just [ ("zero",[]) , ("succ",[Rec "Nat"]) ]
>testEnv _ = Nothing

Now, we can use the `subtermInduction` to get induction hypotheses which are
just subterms of the conclusion. Normally, you would translate the `Term`s from
the proof `Obligation`s to some other representation, but there is also
linearisation functions included (`linObligations`, for instance.)

>natInd :: [String] -> [Int] -> IO ()
>natInd vars coords = putStrLn
>    $ render
>    $ linObligations strStyle
>    $ unTag (\(x :~ i) -> x ++ show i)
>    $ subtermInduction testEnv typed_vars coords
>  where
>    typed_vars = zip vars (repeat "Nat")

The library will create fresh variables for you (called `Tagged` variables),
but you need to remove them, using for instance `unTag`. If you want to sync
it with your own name supply, use `unTagM` or `unTagMapM`.

An example invocation:

>*Mini> natInd ["X"] [0]
>P(zero).
>! [X1 : Nat] : (P(X1) => P(succ(X1))).

This means to do induction on the zeroth coord (hence the @0@), and the variable
is called "X". When using the library, it is up to you to translate the
abstract @P@ predicate to something meaningful.

We can also do induction on several variables:

>*Mini> natInd ["X","Y"] [0,1]
>P(zero,zero).
>! [Y3 : Nat] : (P(zero,Y3) => P(zero,succ(Y3))).
>! [X1 : Nat] : (P(X1,zero) => P(succ(X1),zero)).
>! [X1 : Nat,Y3 : Nat] :
>    (P(X1,Y3) &
>    P(X1,succ(Y3)) &
>    P(succ(X1),Y3)
>     => P(succ(X1),succ(Y3))).

In the last step case, all proper subterms of @succ(X1),succ(Y3)@ are used as
hypotheses.

A bigger example is in @example/Example.hs@ in the distribution.

-}
module Induction.Structural (
    module Induction.Structural.Subterms,
    module Induction.Structural.Types,
    module Induction.Structural.Linearise
) where

import Induction.Structural.Subterms
import Induction.Structural.Types
import Induction.Structural.Linearise

{-# ANN module "HLint: ignore Use import/export shortcut" #-}