-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Instantiate structural induction schemas for algebraic data types
--
@package structural-induction
@version 0.2
-- | 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 Terms from the proof Obligations 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
-- | Subterm induction: the induction hypotheses will contain the proper
-- subterms of the conclusion.
subtermInduction :: Ord c => TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t]
-- | Does case analysis on a list of typed variables. This function is
-- equal to removing all the hypotheses from subtermInduction.
caseAnalysis :: TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t]
-- | Quantifier lists are represented as tuples of variables and their
-- type.
--
-- Example:
--
--
-- Obligation
-- { implicit = [(x,t1),(y,t2)]
-- , hypotheses = [([],[htm1,htm2])
-- ,([(z,t3)],[htm3,htm4])
-- ]
-- , conclusion = [tm1,tm2]
-- }
--
--
-- Corresponds to the formula:
--
-- forall (x : t1) (y : t2) . (P(htm1,htm2) & (forall (z : t3) .
-- P(htm3,htm4)) => P(tm1,tm2))
--
-- The implicit variables (x and y) can be viewed as
-- skolemised, and use these three formulae instead:
--
-- P(htm1,htm2).
--
-- forall (z : t3) . P(htm3,htm4).
--
-- ~ P(tm1,tm2).
data Obligation c v t
Obligation :: [(v, t)] -> [Hypothesis c v t] -> Predicate c v -> Obligation c v t
-- | Implicitly quantified variables (skolemised)
implicit :: Obligation c v t -> [(v, t)]
-- | Hypotheses, with explicitly quantified variables
hypotheses :: Obligation c v t -> [Hypothesis c v t]
-- | The induction conclusion
conclusion :: Obligation c v t -> Predicate c v
-- | Obligations with tagged variables (see Tagged and unTag)
type TaggedObligation c v t = Obligation c (Tagged v) t
-- | A list of terms.
--
-- Example: [tm1,tm2] corresponds to the formula
-- P(tm1,tm2)
type Predicate c v = [Term c v]
-- | Quantifier lists are represented as tuples of variables and their
-- type.
--
-- Example:
--
--
-- ([(x,t1),(y,t2)],[tm1,tm2])
--
--
-- corresponds to the formula
--
-- forall (x : t1) (y : t2) . P(tm1,tm2)
type Hypothesis c v t = ([(v, t)], Predicate c v)
-- | The simple term language only includes variables, constructors and
-- functions.
data Term c v
Var :: v -> Term c v
Con :: c -> [Term c v] -> Term c v
-- | Induction on exponential data types yield assumptions with functions
Fun :: v -> [Term c v] -> Term c v
-- | Given a type, return either that you cannot do induction on is type
-- (Nothing), or Just the constructors and a description of
-- their arguments (see Arg).
--
-- The function should instantiate type variables. For instance,
-- if you look up the type [Nat], you should return the cons
-- constructor with arguments Nat and [Nat] (see
-- Arg).
--
-- Examples of types not possible to do induction on are function spaces
-- and type variables. For these, return Nothing.
type TyEnv c t = t -> Maybe [(c, [Arg t])]
-- | An argument to a constructor can be recursive (Rec) or
-- non-recursive (NonRec). Induction hypotheses will be asserted
-- for Rec arguments.
--
-- For instance, when doing induction on [a], then (:)
-- has two arguments, NonRec a and Rec [a]. On the
-- other hand, if doing induction on [Nat], then (:)
-- has NonRec Nat and Rec [Nat].
--
-- Data types can also be exponential. Consider
--
--
-- data Ord = Zero | Succ Ord | Lim (Nat -> Ord)
--
--
-- Here, the Lim constructor is exponential. If we describe
-- types and constructors with strings, the constructors for this data
-- type is:
--
--
-- [ ("Zero",[])
-- , ("Succ",[Rec "Ord"])
-- , ("Lim",[Exp ("Nat -> Ord") ["Nat"])
-- ]
--
--
-- The first argument to Exp is the type of the function, and the
-- second argument are the arguments to the function.
data Arg t
Rec :: t -> Arg t
NonRec :: t -> Arg t
Exp :: t -> [t] -> Arg t
-- | Cheap way of introducing fresh variables. The Eq and Ord
-- instances only uses the Integer tag.
data Tagged v
(:~) :: v -> Integer -> Tagged v
-- | The Integer tag
tag :: Tagged v -> Integer
-- | Removing tagged (fresh) variables
unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t]
-- | Removing tagged (fresh) variables in a monad. The remove function is
-- exectued at every occurence of a tagged variable. This is
-- useful if you want to sync it with your own name supply monad.
unTagM :: Applicative m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t]
-- | Remove tagged (fresh) variables in a monad. The remove function is
-- exectued only once for each tagged variable, and a Map
-- of renamings is returned. This is useful if you want to sync it with
-- your own name supply monad.
unTagMapM :: (Functor m, Monad m) => (Tagged v -> m v') -> [TaggedObligation c v t] -> m ([Obligation c v' t], Map (Tagged v) v')
-- | Linearises a list of Obligation, using a given Style.
linObligations :: Style c v t -> [Obligation c v t] -> Doc
-- | Linearises an Obligation using a given Style. The output
-- format is inspired by TPTP, but with typed quantifiers.
linObligation :: Style c v t -> Obligation c v t -> Doc
-- | Linearises a Term using a given Style.
linTerm :: Style c v t -> Term c v -> Doc
-- | Functions for linearising constructors (linc), variables
-- (linv) and types (lint).
data Style c v t
Style :: (c -> Doc) -> (v -> Doc) -> (t -> Doc) -> Style c v t
linc :: Style c v t -> c -> Doc
linv :: Style c v t -> v -> Doc
lint :: Style c v t -> t -> Doc
-- | An example style where constructors, variables and types are
-- represented as String.
strStyle :: Style String String String
-- | Render the Doc to a String using the default Style.
render :: Doc -> String
-- | A document of height 1 containing a literal string. text
-- satisfies the following laws:
--
--
--
-- The side condition on the last law is necessary because
-- text "" has height 1, while empty has no
-- height.
text :: String -> Doc