packages feed

structural-induction (empty) → 0.1

raw patch · 10 files changed

+1006/−0 lines, 10 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, geniplate, language-haskell-extract, mtl, pretty, safe, structural-induction, testing-feat

Files

+ Induction/Structural.hs view
@@ -0,0 +1,73 @@+{- |++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" #-}
+ Induction/Structural/Auxiliary.hs view
@@ -0,0 +1,30 @@+{-# OPTIONS_HADDOCK hide #-}+-- | Internal auxiliary functions (pertaining to general haskell types)+module Induction.Structural.Auxiliary where++import Control.Monad (liftM)+import Data.List     (sortBy, groupBy)+import Data.Function (on)+import Data.Ord      (comparing)++-- | Concatenate the results after mapM+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]+concatMapM f = liftM concat . mapM f++infixr 9 .:++-- | Function composition deluxe+--+--   @(f .: g) = \x y -> f (g x y)@+(.:) :: (b -> c) -> (a -> a' -> b) -> a -> a' -> c+(.:) = (.) . (.)++-- | /O(n log n)/ group, but destroys ordering+groupSortedOn :: Ord b => (a -> b) -> [a] -> [[a]]+groupSortedOn f = groupBy ((==) `on` f)+                . sortBy (comparing f)++-- | /O(n log n)/ nub by a comparison function. Destroys ordering+nubSortedOn :: Ord b => (a -> b) -> [a] -> [a]+nubSortedOn f = map head . groupSortedOn f+
+ Induction/Structural/Linearise.hs view
@@ -0,0 +1,93 @@+-- | Linearisation+{-# LANGUAGE RecordWildCards #-}+module Induction.Structural.Linearise+    (+    -- * Linearising (pretty-printing) obligations and terms+      linObligations,+      linObligation,+      linTerm,+      Style(..),+      strStyle,+    -- ** Convenience re-export+      render,+      text+    ) where++import Induction.Structural.Types++import Text.PrettyPrint hiding (Style)++-- | Functions for linearising constructors (`linc`), variables (`linv`) and+-- types (`lint`).+data Style c v t = Style+    { linc :: c -> Doc+    , linv :: v -> Doc+    , lint :: t -> Doc+    }++-- | An example style where constructors, variables and types are represented as `String`.+strStyle :: Style String String String+strStyle = Style+    { linc = text+    , linv = text+    , lint = text+    }++-- | Linearises a list of `Obligation`, using a given `Style`.+linObligations :: Style c v t -> [Obligation c v t] -> Doc+linObligations s = vcat . map ((<> dot) . linObligation s)++-- | 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+linObligation s@Style{..} x = case x of+    Obligation sks []   concl -> linForall sks <+> linPred concl+    Obligation sks hyps concl -> hang (linForall sks) 4 $+        cat $ parList $+            punctuate (fluff ampersand) (map linHyp hyps) +++            [space <> darrow <+> linPred concl]+  where+    linTypedVar v t = linv v <+> colon <+> lint t++    linForall [] = empty+    linForall qs =+        bang <+> brackets (csv (map (uncurry linTypedVar) qs)) <+> colon++    linPred xs = char 'P' <> parens (csv (map (linTerm s) xs))++    linHyp ([],hyp) = linPred hyp+    linHyp (qs,hyp) = parens (linForall qs <+> linPred hyp)++-- | Linearises a `Term` using a given `Style`.+linTerm :: Style c v t -> Term c v -> Doc+linTerm Style{..} = go where+    go tm = case tm of+        Var v    -> linv v+        Con c [] -> linc c+        Con c ts -> linc c <> parens (csv (map go ts))+        Fun v ts -> linv v <> parens (csv (map go ts))+++csv :: [Doc] -> Doc+csv = hcat . punctuate comma++parList :: [Doc] -> [Doc]+parList []     = [parens empty]+parList [x]    = [x]+parList (x:xs) = (lparen <> x) : init xs ++ [last xs <> rparen]++ampersand :: Doc+ampersand = char '&'++bang :: Doc+bang = char '!'++fluff :: Doc -> Doc+fluff d = space <> d <> space++darrow :: Doc+darrow = text "=>"++dot :: Doc+dot = char '.'+
+ Induction/Structural/Subterms.hs view
@@ -0,0 +1,210 @@+-- | Induction with subterms as hypotheses+{-# LANGUAGE ParallelListComp, ScopedTypeVariables #-}+module Induction.Structural.Subterms+    (+    -- * Induction with subterms as hypotheses+      subtermInduction,+    -- * Case analysis (no induction hypotheses)+      caseAnalysis+    ) where++import Control.Applicative+import Control.Arrow (first)+import Control.Monad.State++import Data.Maybe++import Induction.Structural.Auxiliary (concatMapM,nubSortedOn)+import Induction.Structural.Types+import Induction.Structural.Utils++import Safe++-- | Find the type of a variable using the index in a type environment+mfindVNote :: String -> Tagged a -> [(Tagged a,t)] -> t+mfindVNote note u = snd . headNote note . filter (\ (v,_) -> tag u == tag v)++-- We annotate constructors in the terms with the types of the arguments they+-- have to easily be able to calculate subterms+type C c t = (c,[Arg t])++-- Term and terms explicitly quantified with variables+type QuantTerm c v t = ([(Tagged v,t)],TaggedTerm (C c t) v)+type QuantTerms c v t = ([(Tagged v,t)],[TaggedTerm (C c t) v])++-- Given+--+--      [ [ all x0 . P (tx0) , all x1 . P(tx1) ]+--      , [ all y0 . P (ty0) , all y1 . P(ty1) ]+--      ]+--+-- Returns+--+--      [ all x0 y0 . P (tx0,ty0)+--      , all x0 y1 . P (tx0,ty1)+--      , all x1 y0 . P (tx1,ty0)+--      , all x1 y1 . P (tx1,ty1)+--      ]+--+-- Assumption: x0, x1, y0, y1 are all different+makeQuantTerms :: [[QuantTerm c v t]] -> [QuantTerms c v t]+makeQuantTerms qtmss =+    [ (concat qs,tms)+    | qtms <- sequence qtmss+    , let (qs,tms) = unzip qtms+    ]++-- | Instantiate a variable with a given type, returning the new variables and+--   what the term should be replaced with+inst :: forall c v t . TyEnv c t -> Tagged v -> t -> Fresh (Maybe [QuantTerm c v t])+inst env v t = case env t of+    Just ks -> Just <$> mapM (uncurry inst') ks+    Nothing -> return Nothing+  where+    inst' :: c -> [Arg t] -> Fresh (QuantTerm c v t)+    inst' k as = do+        args <- mapM (refreshTypedTagged v . argRepr) as+        return (args,Con (k,as) [ Var x | (x,_) <- args ])++-- | Induction on every variable in a term+--+-- Assumption: The variables only occur once in each term.+inductionTm :: forall c v t .+               TyEnv c t -> QuantTerm c v t -> Fresh [QuantTerm c v t]+inductionTm env (qs0,tm0) = go tm0+  where+    go :: TaggedTerm (C c t) v -> Fresh [QuantTerm c v t]+    go tm = case tm of+        Var x@(_ :~ x_idx) -> do+            let ty = headNote "inductionTm: unbound variable!"+                     [ t | (_ :~ idx,t) <- qs0, x_idx == idx ]+            fromMaybe [([(x,ty)],tm)] <$> inst env x ty+        Con c tms -> goTms (Con c) tms+        Fun f tms -> goTms (Fun f) tms++    goTms :: ([TaggedTerm (C c t) v] -> TaggedTerm (C c t) v) ->+             [TaggedTerm (C c t) v] -> Fresh [QuantTerm c v t]+    goTms mk tms0 = do+        qtmss <- mapM go tms0+        return [ (qs,mk tms) | (qs,tms) <- makeQuantTerms qtmss ]++-- | Induction several times on a variable+repeatInductionTm :: forall c v t . TyEnv c t -> v -> t -> Int -> Fresh [QuantTerm c v t]+repeatInductionTm env v t n0 = do+    vv <- newTyped v t+    go n0 [([vv],Var (fst vv))]+  where+    go :: Int -> [QuantTerm c v t] -> Fresh [QuantTerm c v t]+    go 0 qtms = return qtms+    go n qtms = concatMapM (go (n - 1) <=< inductionTm env) qtms++-- | Unroll to a given depth, but does not add any hypotheses+noHyps :: forall c v t . TyEnv c t -> [(v,t)] -> [Int]+       -> Fresh [TaggedObligation (C c t) v t]+noHyps env vars coords = do+    obligs <- sequence+        [ repeatInductionTm env v t (length (filter (ix ==) coords))+        | (v,t) <- vars+        | ix <- [0..]+        ]+    return $ makeObligations (makeQuantTerms obligs)++-- | Make Obligations: this means to add empty hypotheses to QuantTerms.+makeObligations :: [QuantTerms c v t] -> [TaggedObligation (C c t) v t]+makeObligations qtms = [ Obligation qs [] tms | (qs,tms) <- qtms ]++-- | Removes the argument type information from the constructors+removeArgs :: [Obligation (C c t) v t] -> [Obligation c v t]+removeArgs parts =+    [ Obligation skolem [ (qs,map removeArg hyp) | (qs,hyp) <- hyps ]+                        (map removeArg concl)+    | Obligation skolem hyps concl <- parts+    ]++-- | Removes the argument type information from the constructors in one Term+removeArg :: Term (C c t) v -> Term c v+removeArg = go where+    go tm = case tm of+        Var x         -> Var x+        Con (c,_) tms -> Con c (map go tms)+        Fun f     tms -> Fun f (map go tms)++-- | 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]+caseAnalysis env args = removeArgs . runFresh . noHyps env args++-- | Gets all well-typed subterms of a term, including yourself.+--+-- The first argument is always yourself.+--+-- We need terms where the constructors are associated with their arguments.+subterms :: Term (C c t) v -> [Term (C c t) v]+subterms (Var x) = [Var x]+subterms (Fun x tms) = Fun x tms : map (Fun x) (mapM subterms tms)+subterms (Con c@(_,as) tms) = direct ++ indirect+  where+    -- Starting with this constructor. This includes the term we started with.+    direct   = map (Con c) (mapM subterms tms)+    -- Well-typed subterms of the arguments to the constructor+    indirect = concat [ subterms tm | (Rec _,tm) <- zip as tms ]++-- | Does this term contain a variable somewhere?+hasVar :: Term c v -> Bool+hasVar Var{} = True+hasVar Fun{} = True+hasVar (Con _ as) = any hasVar as++-- | Adds hypotheses to an Obligation.+--+-- Important to drop 1, otherwise we get the conclusion as a hypothesis!+--+-- Hypotheses that only contain constructors (no variables) are removed.+addHypotheses :: Ord c => TaggedObligation (C c t) v t -> TaggedObligation (C c t) v t+addHypotheses (Obligation qs _ tms) = Obligation qs hyps tms+  where+    -- The empty lists denotes that we are not quantifying over any new+    -- variables in the hypotheses.+    hyps = nubSortedOn (map removeArg . snd)+                       [ ([],h)+                       | h <- drop 1 (mapM subterms tms)+                       , any hasVar h+                       ]++-- | Adds hypotheses to an Obligation, requantifying over naked variables+--+-- I.e. forall x y . P(K x,y) becomes+--      forall x y . (forall y'.P(x,y')) -> P (K x,y)+--+-- Important to drop 1, otherwise we get the conclusion as a hypothesis!+addHypothesesQ :: Ord c => TaggedObligation (C c t) v t -> Fresh (TaggedObligation (C c t) v t)+addHypothesesQ ip = do -- Obligation qs hyps tms++    let Obligation qs hyps conc = addHypotheses ip++        mk_msg = ("addHypothesesQ: " ++)+        msg_unbound  = mk_msg "Unbound variable!"+        msg_mismatch = mk_msg "Concrete hypotheses but abstract conclusion!"++        -- tm is from a hypothesis, e from the conclusion.+        -- If e is a variable, tm should be the same, and we requantify over it+        addQ tm e = case e of+            Var x@(_ :~ xi) -> case tm of+                Var (_ :~ yi)+                    | xi == yi -> do+                        let t = mfindVNote msg_unbound x qs+                        xt'@(x',_) <- refreshTypedTagged x t+                        return ([xt'],Var x')+                _ -> error msg_mismatch+            _ -> return ([],tm)++    hyps' <- forM hyps $ \ ([],tms) -> mapAndUnzipM (uncurry addQ) (zip tms conc)++    return (Obligation qs (map (first concat) hyps') conc)++-- | 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]+subtermInduction env args =+    removeArgs . runFresh . (mapM addHypothesesQ <=< noHyps env args)+
+ Induction/Structural/Types.hs view
@@ -0,0 +1,184 @@+-- | Types+module Induction.Structural.Types+    (+    -- * Obligations+      Obligation(..), TaggedObligation,+      Predicate,+      Hypothesis,+    -- ** Terms+      Term(..),+    -- * Typing environment+      TyEnv,+    -- ** Arguments+      Arg(..),+    -- * Tagged (fresh) variables+      Tagged(..), tag,+    -- ** Removing tagged variables+      unTag, unTagM, unTagMapM+    ) where++import Control.Monad.Identity+import Control.Monad.State++import Data.Function (on)++import Data.Map (Map)+import qualified Data.Map as M++-- | The simple term language only includes variables, constructors and functions.+data Term c v+    = Var v+    | Con c [Term c v]+    | Fun v [Term c v]+    -- ^ Induction on exponential data types yield assumptions with functions+  deriving (Eq,Ord)++-- Typed variables are represented as (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:+--+--+-- >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+    { implicit   :: [(v,t)]+    -- ^ Implicitly quantified variables (skolemised)+    , hypotheses :: [Hypothesis c v t]+    -- ^ Hypotheses, with explicitly quantified variables+    , conclusion :: Predicate c v+    -- ^ The induction conclusion+    }++-- | 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)+++-- | 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+    | NonRec t+    | Exp t [t]++-- | 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])]++-- | Cheap way of introducing fresh variables. The `Eq` and `Ord` instances+-- only uses the `Integer` tag.+data Tagged v = v :~ Integer++-- | The `Integer` tag+tag :: Tagged v -> Integer+tag (_ :~ t) = t++instance Eq (Tagged v) where+    (==) = (==) `on` tag++instance Ord (Tagged v) where+    compare = compare `on` tag++-- | Obligations with tagged variables (see `Tagged` and `unTag`)+type TaggedObligation c v t = Obligation c (Tagged 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 :: Monad m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t]+unTagM f = mapM $ \ (Obligation skolem hyps concl) ->+    Obligation <$> unQuant skolem+               <*> mapM (\(qs,hyp) -> (,) <$> unQuant qs <*> mapM unTm hyp) hyps+               <*> mapM unTm concl+  where+    (<$>) = liftM+    (<*>) = ap++    unQuant = mapM (\(v,t) -> (,) <$> f v <*> return t)++    unTm tm = case tm of+        Var x     -> Var <$> f x+        Con c tms -> Con c <$> mapM unTm tms+        Fun x tms -> Fun <$> f x <*> mapM unTm tms++-- | Removing tagged (fresh) variables+unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t]+unTag f = runIdentity . unTagM (return . f)++-- | 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 :: Monad m => (Tagged v -> m v') -> [TaggedObligation c v t]+         -> m ([Obligation c v' t],Map (Tagged v) v')+unTagMapM f = flip runStateT M.empty . unTagM f'+  where+    f' tv = do+        m <- get+        case M.lookup tv m of+            Just v' -> return v'+            Nothing -> do+                v' <- lift (f tv)+                modify (M.insert tv v')+                return v'+
+ Induction/Structural/Utils.hs view
@@ -0,0 +1,48 @@+{-# OPTIONS_HADDOCK hide #-}+-- | Internal utility functions (pertaining to data types in this library)+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Induction.Structural.Utils where++import Control.Applicative hiding (empty)+import Control.Monad.State++import Induction.Structural.Types++-- | Tagged terms+type TaggedTerm c v = Term c (Tagged v)++-- | Tagged hypotheses+type TaggedHypothesis c v t = Hypothesis c (Tagged v) t++-- | Get the representation of the argument+argRepr :: Arg t -> t+argRepr (Rec t)    = t+argRepr (NonRec t) = t+argRepr (Exp t _)  = t++-- Fresh variables++-- | A monad of fresh Integers+newtype Fresh a = Fresh (State Integer a)+  deriving (Functor,Applicative,Monad,MonadState Integer)++-- | Run the fresh monad+runFresh :: Fresh a -> a+runFresh (Fresh m) = evalState m 0++-- | Creating a fresh variable+newFresh :: v -> Fresh (Tagged v)+newFresh v = Fresh $ state $ \ s -> (v :~ s,s+1)++-- | Create a fresh variable that has a type+newTyped :: v -> t -> Fresh (Tagged v,t)+newTyped v t = flip (,) t <$> newFresh v++-- | Refresh variable+refreshTagged :: Tagged v -> Fresh (Tagged v)+refreshTagged (v :~ _) = newFresh v++-- | Refresh a variable that has a type+refreshTypedTagged :: Tagged v -> t -> Fresh (Tagged v,t)+refreshTypedTagged v t = flip (,) t <$> refreshTagged v+
+ LICENSE view
@@ -0,0 +1,165 @@+                  GNU LESSER GENERAL PUBLIC LICENSE+                       Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.+++  This version of the GNU Lesser General Public License incorporates+the terms and conditions of version 3 of the GNU General Public+License, supplemented by the additional permissions listed below.++  0. Additional Definitions. ++  As used herein, "this License" refers to version 3 of the GNU Lesser+General Public License, and the "GNU GPL" refers to version 3 of the GNU+General Public License.++  "The Library" refers to a covered work governed by this License,+other than an Application or a Combined Work as defined below.++  An "Application" is any work that makes use of an interface provided+by the Library, but which is not otherwise based on the Library.+Defining a subclass of a class defined by the Library is deemed a mode+of using an interface provided by the Library.++  A "Combined Work" is a work produced by combining or linking an+Application with the Library.  The particular version of the Library+with which the Combined Work was made is also called the "Linked+Version".++  The "Minimal Corresponding Source" for a Combined Work means the+Corresponding Source for the Combined Work, excluding any source code+for portions of the Combined Work that, considered in isolation, are+based on the Application, and not on the Linked Version.++  The "Corresponding Application Code" for a Combined Work means the+object code and/or source code for the Application, including any data+and utility programs needed for reproducing the Combined Work from the+Application, but excluding the System Libraries of the Combined Work.++  1. Exception to Section 3 of the GNU GPL.++  You may convey a covered work under sections 3 and 4 of this License+without being bound by section 3 of the GNU GPL.++  2. Conveying Modified Versions.++  If you modify a copy of the Library, and, in your modifications, a+facility refers to a function or data to be supplied by an Application+that uses the facility (other than as an argument passed when the+facility is invoked), then you may convey a copy of the modified+version:++   a) under this License, provided that you make a good faith effort to+   ensure that, in the event an Application does not supply the+   function or data, the facility still operates, and performs+   whatever part of its purpose remains meaningful, or++   b) under the GNU GPL, with none of the additional permissions of+   this License applicable to that copy.++  3. Object Code Incorporating Material from Library Header Files.++  The object code form of an Application may incorporate material from+a header file that is part of the Library.  You may convey such object+code under terms of your choice, provided that, if the incorporated+material is not limited to numerical parameters, data structure+layouts and accessors, or small macros, inline functions and templates+(ten or fewer lines in length), you do both of the following:++   a) Give prominent notice with each copy of the object code that the+   Library is used in it and that the Library and its use are+   covered by this License.++   b) Accompany the object code with a copy of the GNU GPL and this license+   document.++  4. Combined Works.++  You may convey a Combined Work under terms of your choice that,+taken together, effectively do not restrict modification of the+portions of the Library contained in the Combined Work and reverse+engineering for debugging such modifications, if you also do each of+the following:++   a) Give prominent notice with each copy of the Combined Work that+   the Library is used in it and that the Library and its use are+   covered by this License.++   b) Accompany the Combined Work with a copy of the GNU GPL and this license+   document.++   c) For a Combined Work that displays copyright notices during+   execution, include the copyright notice for the Library among+   these notices, as well as a reference directing the user to the+   copies of the GNU GPL and this license document.++   d) Do one of the following:++       0) Convey the Minimal Corresponding Source under the terms of this+       License, and the Corresponding Application Code in a form+       suitable for, and under terms that permit, the user to+       recombine or relink the Application with a modified version of+       the Linked Version to produce a modified Combined Work, in the+       manner specified by section 6 of the GNU GPL for conveying+       Corresponding Source.++       1) Use a suitable shared library mechanism for linking with the+       Library.  A suitable mechanism is one that (a) uses at run time+       a copy of the Library already present on the user's computer+       system, and (b) will operate properly with a modified version+       of the Library that is interface-compatible with the Linked+       Version. ++   e) Provide Installation Information, but only if you would otherwise+   be required to provide such information under section 6 of the+   GNU GPL, and only to the extent that such information is+   necessary to install and execute a modified version of the+   Combined Work produced by recombining or relinking the+   Application with a modified version of the Linked Version. (If+   you use option 4d0, the Installation Information must accompany+   the Minimal Corresponding Source and Corresponding Application+   Code. If you use option 4d1, you must provide the Installation+   Information in the manner specified by section 6 of the GNU GPL+   for conveying Corresponding Source.)++  5. Combined Libraries.++  You may place library facilities that are a work based on the+Library side by side in a single library together with other library+facilities that are not Applications and are not covered by this+License, and convey such a combined library under terms of your+choice, if you do both of the following:++   a) Accompany the combined library with a copy of the same work based+   on the Library, uncombined with any other library facilities,+   conveyed under the terms of this License.++   b) Give prominent notice with the combined library that part of it+   is a work based on the Library, and explaining where to find the+   accompanying uncombined form of the same work.++  6. Revised Versions of the GNU Lesser General Public License.++  The Free Software Foundation may publish revised and/or new versions+of the GNU Lesser General Public License from time to time. Such new+versions will be similar in spirit to the present version, but may+differ in detail to address new problems or concerns.++  Each version is given a distinguishing version number. If the+Library as you received it specifies that a certain numbered version+of the GNU Lesser General Public License "or any later version"+applies to it, you have the option of following the terms and+conditions either of that published version or of any later version+published by the Free Software Foundation. If the Library as you+received it does not specify a version number of the GNU Lesser+General Public License, you may choose any version of the GNU Lesser+General Public License ever published by the Free Software Foundation.++  If the Library as you received it specifies that a proxy can decide+whether future versions of the GNU Lesser General Public License shall+apply, that proxy's public statement of acceptance of any version is+permanent authorization for you to choose that version for the+Library.
+ Setup.hs view
@@ -0,0 +1,4 @@+import Distribution.Simple++main :: IO ()+main = defaultMain
+ structural-induction.cabal view
@@ -0,0 +1,64 @@+name:               structural-induction+category:           Theorem Provers, Logic+version:            0.1+license:            LGPL-3+license-file:       LICENSE+author:             Dan Rosén+maintainer:         Dan Rosén <danr@chalmers.se>+homepage:           http://www.github.com/danr/structural-induction+bug-reports:        http://www.github.com/danr/structural-induction/issues+build-type:         Simple+cabal-version:      >= 1.8+tested-with:        GHC == 7.4.1, GHC == 7.6.1+synopsis:           Instantiate structural induction schemas for algebraic data types+description:        See documentation for Induction.Structural++source-repository head+  type: git+  location: git://github.com/danr/structural-induction.git++flag Werror+  default: False+  manual: True++library+  ghc-options:    -Wall+  if flag(Werror)+    ghc-options: -Werror++  exposed-modules:+    Induction.Structural,+    Induction.Structural.Auxiliary,+    Induction.Structural.Utils++  other-modules:+    Induction.Structural.Types,+    Induction.Structural.Subterms,+    Induction.Structural.Linearise++  build-depends:+    base                      >= 4 && < 5,+    mtl,+    containers,+    pretty,+    safe++test-suite walk+  type:           exitcode-stdio-1.0+  main-is:        Main.hs+  hs-source-dirs: test+  ghc-options:    -Wall+  if flag(Werror)+    ghc-options: -Werror++  build-depends:+    structural-induction,+    base,+    pretty,+    QuickCheck                >= 2.4,+    mtl                       >= 2.1.2,+    language-haskell-extract,+    testing-feat              >= 0.4,+    geniplate                 >= 0.6,+    safe+
+ test/Main.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE TemplateHaskell, Rank2Types #-}+module Main where++import Control.Monad+import Control.Applicative++import Data.List+import Data.Ord++import System.Exit (exitFailure)++import Test.QuickCheck+import Test.QuickCheck.Test+import Test.Feat.Access++import Language.Haskell.Extract++import Induction.Structural++-- import Unsound++import Trace+import Env+import EnvTypes+import Walk+import Util++-- | Structural Induction Instatiator+type SII = TyEnv Con' Ty' -> [(String,Ty')] -> [Int] -> [TaggedObligation Con' String Ty']++-- | Do induction on a test case+ind :: SII -> TestCase -> [Oblig]+ind sii (TestCase types coords) =+    unTag (\ (x :~ i) -> x ++ show i) $ sii testEnv' args coords+  where+    args = zip vars types++    vars :: [String]+    vars = concat [ replicateM n ['a'..'z'] | n <- [1..] ]++data TestCase = TestCase [Ty'] [Int]+  deriving Show++unitTc :: Int -> [Int] -> TestCase+unitTc n = TestCase (replicate n (Si Unit))++boolTc :: Int -> [Int] -> TestCase+boolTc x = TestCase (replicate x (Si Bool))++natTc :: Int -> TestCase+natTc x = TestCase [Si Nat] (replicate x 0)++maybeTc :: Ty' -> Int -> Int -> TestCase+maybeTc t d i = TestCase [repeatMaybe t d] (replicate i 0)++repeatMaybe :: Ty' -> Int -> Ty'+repeatMaybe t = go+  where+    go n | n <= 0    = t+         | otherwise = case go (n - 1) of Si t' -> Si (Maybe t')++mods :: Int -> [Int] -> [Int]+mods 0 _  = []+mods x xs = map (`mod` x) xs++-- | Linear+prop_units :: SII -> NonNegative Int -> [Int] -> Property+prop_units sii (NonNegative x) xs+    = mkProp sii (unitTc x' (mods x' xs))+  where x' = min 5000 x++-- | Can't try this too far because of exponential explosion+prop_bools :: SII -> NonNegative Int -> [Int] -> Property+prop_bools sii (NonNegative x) xs+    = mkProp sii (boolTc x' (mods x' xs))+  where x' = min 10 x++-- | Linear+prop_maybe :: SII -> NonNegative Int -> NonNegative Int -> Property+prop_maybe sii (NonNegative d) (NonNegative i)+    = mkProp sii (maybeTc (Si Unit) d' i')+  where+    d' = min 100 d+    i' = min 100 i++mkPropTy :: SII -> Ty' -> Int -> Property+mkPropTy sii ty n = mkProp sii (TestCase [ty] (replicate n 0))++mkProp :: SII -> TestCase -> Property+mkProp sii tc@(TestCase tys _) =+    forAllShrink (startFromTypes tys) (mapM shrinkRepr') $ \ start ->+        forAll (makeTracer start parts) $ \ trace ->+            case loop trace of+                Just _  -> printTestCase (showOblig parts) False+                Nothing -> property True+  where parts = ind sii tc++makeTestCases :: Integer -> IO [TestCase]+makeTestCases tests = concat <$>+    forM [0..tests] (\ ix -> do+        let tys = indexWith enumTy's ix+            all_coordss = concat [ coordss (length tys - 1) d | d <- [0..4] ]+        coordss' <- head <$> sample' (shuffle all_coordss)+        let css = nub . sortBy (comparing length) . sort . take 10 $ coordss'+        return $ map (TestCase tys) css+    )++main :: IO ()+main = do+    let tests =+            -- [("structuralInductionUnsound",structuralInductionUnsound)] +++            [("subtermInduction",subtermInduction,96)+            ,("caseAnalysis",caseAnalysis,15)+            ]+    oks <- forM tests $ \ (name_sii,sii,test_depth) -> do+        putStrLn $ "== " ++ name_sii ++ " =="++        testcases <- makeTestCases test_depth+        let num_tests = length testcases++        ok_feat <- forM (zip testcases ([0..] :: [Integer])) $+            \ (tc@(TestCase tys cs),i) -> do+                putStrLn $ "(" ++ show i ++ "/" ++ show num_tests ++ ") " +++                           name_sii ++ ": " ++ show tys ++ " coords: " ++ show cs+                quickCheckResult (mkProp sii tc)++        ok_manual <- sequence $(functionExtractorMap "^prop_"+            [| \ name_prop prop -> do+                putStrLn $ name_sii ++ ": " ++ name_prop+                quickCheckResult (prop sii) |])++        return $ all isSuccess (ok_manual ++ ok_feat)++    unless (and oks) exitFailure+