packages feed

structural-induction 0.2 → 0.2.0.1

raw patch · 8 files changed

+446/−10 lines, 8 files

Files

changelog view
@@ -1,3 +1,6 @@+structural-induction 0.2.0.1 (released 2015-06-10)+	* Add missing test suite files to extra-source-files.+ structural-induction 0.2 (released 2015-04-10) 	* Support GHC 7.10
structural-induction.cabal view
@@ -1,6 +1,6 @@ name:               structural-induction category:           Theorem Provers, Logic-version:            0.2+version:            0.2.0.1 license:            LGPL-3 license-file:       LICENSE author:             Dan Rosén@@ -12,20 +12,14 @@ tested-with:        GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.3, GHC == 7.10.1 synopsis:           Instantiate structural induction schemas for algebraic data types description:        See documentation for Induction.Structural-extra-source-files: changelog+extra-source-files: changelog test/Env.hs test/EnvTypes.hs test/Walk.hs test/Util.hs test/Trace.hs test/Nat.hs  source-repository head   type: git   location: git://github.com/danr/structural-induction.git -flag Werror-  default: False-  manual: True- library   ghc-options:    -Wall -fno-warn-unused-imports-  if flag(Werror)-    ghc-options: -Werror    exposed-modules:     Induction.Structural,@@ -50,8 +44,6 @@   main-is:        Main.hs   hs-source-dirs: test   ghc-options:    -Wall -fno-warn-unused-imports-  if flag(Werror)-    ghc-options: -Werror    build-depends:     structural-induction,
+ test/Env.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE GADTs, ConstraintKinds, ExplicitForAll, PatternGuards #-}+module Env where++import Test.QuickCheck+import Control.Applicative++import Induction.Structural++import EnvTypes+import Nat+import Util++type Oblig = Obligation Con' String Ty'+type Tm    = Term Con' String+type P     = Predicate Con' String+type Hyp   = Hypothesis Con' String Ty'++-- | A small test environment. No exponentials for now.+testEnv :: Repr a -> Maybe [(Con a,[Arg Ty'])]+testEnv t = case t of+    Unit      -> Just [(TT,[])]+    Nat       -> Just [(Zero,[])+                      ,(Succ,[Rec (Si Nat)])+                      ]+    PInt      -> Just [(Pos,[NonRec (Si Nat)])+                      ,(Neg,[NonRec (Si Nat)])+                      ]+    Bool      -> Just [(Tru,[]),(Fls,[])]+    List a    -> Just [(Nil a,[])+                      ,(Cons,[NonRec (Si a),Rec (Si (List a))])+                      ]+    Maybe a   -> Just [(Ntng a,[])+                      ,(Jst,[NonRec (Si a)])+                      ]+    TupTy a b -> Just [(Tup,[NonRec (Si a),NonRec (Si b)])]+    TyVar     -> Nothing++-- | Forgetting some type info+testEnv' :: TyEnv Con' Ty'+testEnv' (Si t) = case testEnv t of+    Just ksargs -> Just (map (uncurry forget) ksargs)+    Nothing -> Nothing+  where+    forget :: forall a . EqShow a => Con a -> [Arg Ty'] -> (Con',[Arg Ty'])+    forget k args = (Si k, args)++-- | Generates a random value of some type+arbFromType :: Repr a -> Gen a+arbFromType t = case t of+    Unit   -> arbitrary+    Nat    -> arbitrary+    PInt   -> arbitrary+    Bool   -> arbitrary+    List a -> halfSize $ \ s -> frequency+        [ (1, return [])+        , (s, (:) <$> arbFromType a <*> arbFromType (List a))+        ]+    Maybe a -> sized $ \ s -> frequency+        [ (1, return Nothing)+        , (s, Just <$> arbFromType a)+        ]+    TupTy a b -> (,) <$> arbFromType a <*> arbFromType b+    TyVar -> arbitrary++-- | Forget type information+arbFromType' :: Sigma Repr -> Gen (Exists Repr)+arbFromType' (Si r) = Val r <$> arbFromType r++startFromTypes :: [Ty'] -> Gen [Repr']+startFromTypes = mapM arbFromType'++-- Cannot make this well typed in a nice way+mkCon :: Con' -> [Repr'] -> Repr'+mkCon (Si c) as = case c of+    TT     -> case as of { []                -> Val Unit ()            ; _ -> ill_typed }+    Zero   -> case as of { []                -> Val Nat Z              ; _ -> ill_typed }+    Succ   -> case as of { [Val Nat n]       -> Val Nat (S n)          ; _ -> ill_typed }+    Pos    -> case as of { [Val Nat n]       -> Val PInt (P n)         ; _ -> ill_typed }+    Neg    -> case as of { [Val Nat n]       -> Val PInt (N n)         ; _ -> ill_typed }+    Fls    -> case as of { []                -> Val Bool False         ; _ -> ill_typed }+    Tru    -> case as of { []                -> Val Bool True          ; _ -> ill_typed }+    Ntng a -> case as of { []                -> Val (Maybe a) Nothing  ; _ -> ill_typed }+    Jst    -> case as of { [Val a x]         -> Val (Maybe a) (Just x) ; _ -> ill_typed }+    Tup    -> case as of { [Val a x,Val b y] -> Val (TupTy a b) (x,y)  ; _ -> ill_typed }+    Nil a  -> case as of { []                -> Val (List a) []        ; _ -> ill_typed }+    Cons   -> case as of+        [Val a x,Val (List b) xs] -> case a ==? b of+            Just Refl -> Val (List a) (x:xs)+            Nothing   -> error $ "mkCon: " ++ show as ++ " is heterogenous!"+        _ -> ill_typed+  where+    ill_typed :: a+    ill_typed = error $ "mkCon: illtyped: " ++ show (Si c) ++ " on " ++ show as++type VarMap = [(String,Repr')]++-- | Tries to match a representation to a term, returning bound variables+match :: Repr' -> Tm -> Maybe VarMap+match v tm0 = case tm0 of+    Var s -> Just [(s,v)]+    Con (Si c) tms -> case (v,c,tms) of+        (Val Unit ()            , TT     , [])   -> ok+        (Val Nat Z              , Zero   , [])   -> ok+        (Val Nat (S x)          , Succ   , [tm]) -> match (Val Nat x) tm+        (Val PInt (P x)         , Pos    , [tm]) -> match (Val Nat x) tm+        (Val PInt (N x)         , Neg    , [tm]) -> match (Val Nat x) tm+        (Val Bool True          , Tru    , [])   -> ok+        (Val Bool False         , Fls    , [])   -> ok+        (Val (Maybe a) Nothing  , Ntng b , []) | Just Refl <- a ==? b -> ok+        (Val (Maybe a) (Just x) , Jst    , [tm]) -> match (Val a x) tm+        (Val (List a) []        , Nil b  , []) | Just Refl <- a ==? b -> ok+        (Val (List a) (x:xs)    , Cons   , [t1,t2]) ->+            match (Val a x) t1 `comb` match (Val (List a) xs) t2+        (Val (TupTy a b) (x,y)  , Tup    , [t1,t2]) ->+            match (Val a x) t1 `comb` match (Val b y) t2+        _ -> Nothing+    Fun{} -> error "match: No support for exponentials!"+  where+    ok = Just []+    comb r s = (++) <$> r <*> s++-- | Show induction schema+showOblig :: [Oblig] -> String+showOblig = unlines . map ((++ ".") . render . linObligation style)++-- | The style for printing+style :: Style Con' String Ty'+style = Style (text . show) text (text . show)+
+ test/EnvTypes.hs view
@@ -0,0 +1,164 @@+{-# LANGUAGE GADTs, KindSignatures, DeriveDataTypeable,+        FlexibleInstances, ConstraintKinds,+        PatternGuards, TemplateHaskell #-}+module EnvTypes where++import Nat++import Data.Function (on)+import Data.Typeable (Typeable)++import Test.QuickCheck+import Test.Feat++type EqShow a = (Eq a,Show a,Arbitrary a)++data Sigma :: (* -> *) -> * where+    Si :: EqShow a => r a -> Sigma r++data Exists :: (* -> *) -> * where+    Val :: EqShow a => r a -> a -> Exists r++type Repr' = Exists Repr++type Ty' = Sigma Repr+++-- Representations of our types.+-- Putting Eq and Show here simplifies those instances for Repr a bit+data Repr a where+    Unit  :: Repr ()+    Nat   :: Repr Nat+    PInt  :: Repr PInt+    Bool  :: Repr Bool+    List  :: EqShow a => Repr a -> Repr [a]+    Maybe :: EqShow a => Repr a -> Repr (Maybe a)+    TupTy :: (EqShow a,EqShow b) => Repr a -> Repr b -> Repr (a,b)+    TyVar :: Repr Int+    -- ^ Should this contain more information?+  deriving Typeable++-- The more number of units, the more boring this type is to test+data URepr+    = UUnit () () ()+    | UNat+    | UPInt+    | UBool () ()+    | UList URepr+    | UMaybe URepr ()+    | UTupTy URepr URepr ()+    | UTyVar () () ()+  deriving Typeable++deriveEnumerable ''URepr++toTy :: URepr -> Ty'+toTy u = case u of+    UUnit{}      -> Si Unit+    UNat         -> Si Nat+    UPInt        -> Si PInt+    UBool{}      -> Si Bool+    UList a      | Si a' <- toTy a -> Si (List a')+    UMaybe a _   | Si a' <- toTy a -> Si (Maybe a')+    UTupTy a b _ | Si a' <- toTy a+                 , Si b' <- toTy b -> Si (TupTy a' b')+    UTyVar{}     -> Si TyVar++enumTy' :: Enumerate Ty'+enumTy' = fmap toTy enumerate++{-# ANN enumTy's "HLint: ignore Use camelCase" #-}+enumTy's :: Enumerate [Ty']+enumTy's = fmap (map toTy) enumerate++showRepr :: Repr a -> String+showRepr r = case r of+    Unit      -> "Unit"+    Nat       -> "Nat"+    PInt      -> "PInt"+    Bool      -> "Bool"+    List a    -> "List " ++ showRepr a+    Maybe a   -> "Maybe " ++ showRepr a+    TupTy a b -> "TupTy " ++ showRepr a ++ " " ++ showRepr b+    TyVar     -> "TyVar"++showRepr' :: Repr' -> String+showRepr' (Val r x) = "Val " ++ showRepr r ++ " " ++ show x++instance Show Ty' where+    show (Si r) = case r of+        Unit      -> "()"+        Nat       -> "Nat"+        PInt      -> "Int"+        Bool      -> "Bool"+        List a    -> "[" ++ show (Si a) ++ "]"+        Maybe a   -> "Maybe " ++ show (Si a)+        TupTy a b -> "(" ++ show (Si a) ++ "," ++ show (Si b) ++ ")"+        TyVar     -> "a"++type Con' = Sigma Con++data Con a where+    TT   :: Con ()+    Zero :: Con Nat+    Succ :: Con Nat+    Pos  :: Con PInt+    Neg  :: Con PInt+    Tru  :: Con Bool+    Fls  :: Con Bool+    Nil  :: EqShow a => Repr a -> Con [a]+    Cons :: Con [a]+    Jst  :: Con (Maybe a)+    Ntng :: EqShow a => Repr a -> Con (Maybe a)+    Tup  :: Con (a,b)++infoCon' :: Con' -> (Int,String)+infoCon' c = case c of+    Si TT     -> (0,"()")+    Si Zero   -> (1,"Zero")+    Si Succ   -> (2,"Succ")+    Si Nil{}  -> (3,"Nil")+    Si Cons   -> (4,"Cons")+    Si Pos    -> (5,"Pos")+    Si Neg    -> (6,"Neg")+    Si Jst    -> (7,"Just")+    Si Ntng{} -> (8,"Nothing")+    Si Tru    -> (9,"True")+    Si Fls    -> (10,"False")+    Si Tup    -> (11,"Tup")++instance Eq Con' where+    (==) = (==) `on` (fst . infoCon')++instance Ord Con' where+    compare = compare `on` (fst . infoCon')++instance Show Con' where+    show = snd . infoCon'++instance Show (Exists a) where+    show (Val _ x) = show x++shrinkRepr' :: Repr' -> [Repr']+shrinkRepr' (Val r x) = map (Val r) (shrink x)++data Equal :: * -> * -> * where+    Refl :: Equal a a++(==?) :: Repr a -> Repr b -> Maybe (Equal a b)+Unit      ==? Unit  = Just Refl+Nat       ==? Nat   = Just Refl+PInt      ==? PInt  = Just Refl+Bool      ==? Bool  = Just Refl+TyVar     ==? TyVar = Just Refl+Maybe a   ==? Maybe b   | Just Refl <- a ==? b = Just Refl+List a    ==? List b    | Just Refl <- a ==? b = Just Refl+TupTy a u ==? TupTy b v | Just Refl <- a ==? b+                        , Just Refl <- u ==? v = Just Refl+_         ==? _     = Nothing++instance Eq (Exists Repr) where+    Val s u == Val t v = case s ==? t of+        Just Refl -> u == v+        Nothing   -> False+
+ test/Nat.hs view
@@ -0,0 +1,45 @@+{-# OPTIONS_GHC -fno-warn-missing-methods #-}+{-# LANGUAGE ViewPatterns #-}+module Nat where++import Test.QuickCheck++-- A classic!+data Nat = Z | S Nat deriving (Show,Eq)++instance Arbitrary Nat where+    arbitrary = sized $ \ s -> do+        x <- choose (0,round (sqrt (toEnum s) :: Double))+        return (nats !! x)++    shrink (S n) = n : shrink n+    shrink Z     = []++nats :: [Nat]+nats = iterate S Z++-- warning: partial instance+instance Num Nat where+    fromInteger n = nats !! fromEnum n++-- Another classic!+data PInt = P Nat | N Nat+  deriving (Show,Eq)++p :: PInt -> Nat+p (P n) = n+p (N n) = n++instance Arbitrary PInt where+    arbitrary = do+        (b,x) <- arbitrary+        return $ if b then P x else N x++    shrink (p -> n ) = map P (shrink n) ++ map N (shrink n)++-- warning: partial instance+instance Num PInt where+    fromInteger x+        | x < 0     = N (fromInteger (negate (x + 1)))+        | otherwise = P (fromInteger x)+
+ test/Trace.hs view
@@ -0,0 +1,26 @@+module Trace where++import Data.List (find)+import Control.Monad (mplus,msum)++data Trace a = Fork a [Trace a]++instance Show a => Show (Trace a) where+    show = unlines . go+      where+        go (Fork x ts) = show x:bars (map go ts)++        bar :: [String] -> [String]+        bar [] = []+        bar (s:xs) = ("┣┉" ++ s):map ("┃ " ++) xs++        bars :: [[String]] -> [String]+        bars [] = []+        bars [s:xs] = ("┗┉" ++ s):map ("  " ++) xs+        bars (x:xs) = bar x ++ bars xs++loop :: Eq a => Trace a -> Maybe a+loop = go []+  where+    go vis (Fork x ts) = find (x ==) vis `mplus` msum (map (go (x:vis)) ts)+
+ test/Util.hs view
@@ -0,0 +1,15 @@+module Util where++import Test.QuickCheck++halfSize :: (Int -> Gen a) -> Gen a+halfSize m = sized $ \s -> resize (s `div` 2) (m s)++divSize :: Int -> (Int -> Gen a) -> Gen a+divSize d m = sized $ \s -> resize (s `div` d) (m s)++coordss :: Int -> Int -> [[Int]]+coordss n _ | n < 0 = [[]]+coordss 0 d = [replicate d 0]+coordss n d = concat [ map (++ replicate t n) (coordss (n-1) (d-t)) | t <- [0..d] ]+
+ test/Walk.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, FlexibleInstances #-}+module Walk where++import Test.QuickCheck+import Data.List+import Control.Monad+import Control.Applicative++import Induction.Structural++import Trace+import EnvTypes+import Env+import Util++construct :: VarMap -> Hyp -> Gen [Repr']+construct vm (hyps,tms) = mapM (construct1 hyps vm) tms++construct1 :: [(String,Ty')] -> VarMap -> Tm -> Gen Repr'+construct1 hyps vm tm = case tm of+    Var s -> case lookup s vm of+        Just u  -> return u+        Nothing -> case lookup s hyps of+            Just t  -> arbFromType' t+            -- ^ if this is missing, generate a new one with arbitrary!!+            Nothing -> error $ show s ++ " missing!" ++ show vm ++ "," ++ show hyps+    Con s tms ->  mkCon s <$> mapM (construct1 hyps vm) tms+    Fun{} -> error "exponentials not supported"++-- | We can only pick 1-2 hyps, otherwise we get crazy exponential behaviour+pickHyps :: [a] -> Gen [a]+pickHyps [] = return []+pickHyps hs = do+    let n = length hs - 1+    i <- choose (0,n)+    i' <- choose (0,n)+    two <- arbitrary+    return $ if two && i /= i' then [hs !! i,hs !! i'] else [hs !! i]++-- TODO: Can this be reorganized so we get an efficient unrolling?+makeTracer :: [Repr'] -> [Oblig] -> Gen (Trace [Repr'])+makeTracer args parts = go parts+  where+    go p = case p of+        Obligation _ hyps conc:is+            | length args == length conc -> case zipWithM match args conc of+                Nothing -> go is+                Just vms -> halfSize $ \ _ -> do+                    -- Throw away some hypotheses+                    hyps' <- pickHyps hyps+                    argss' <- mapM (construct (concat vms)) hyps'+                    forks <- mapM (`makeTracer` parts) argss'+                    return (Fork args forks)+            | otherwise -> mk_error $ "Unequal lengths (conc=" +++                intercalate "," (map (render . linTerm style) conc) ++ ")"+        _ -> mk_error "No case"+      where+        mk_error msg = error $+            "makeTracer " ++ show args ++ " : " ++ msg ++ "!" +++            "\nDetails: args = (" ++ intercalate " , " (map showRepr' args) ++ ")" +++            "\nCheck Env.match and EnvTypes.==?, or case is missing from schema:" +++            "\n" ++ showOblig parts