structural-induction 0.1 → 0.1.1

raw patch · 2 files changed

+15/−17 lines, 2 filesdep +genifunctors

Dependencies added: genifunctors

Files

• Induction/Structural/Types.hs +13/−16
• structural-induction.cabal +2/−1

@@ -1,3 +1,4 @@+{-# LANGUAGE TemplateHaskell #-} -- | Types module Induction.Structural.Types     (@@ -17,11 +18,16 @@       unTag, unTagM, unTagMapM     ) where +import Data.Generics.Genifunctors+ import Control.Monad.Identity import Control.Monad.State+import Control.Applicative  import Data.Function (on) +import Data.Traversable (traverse)+ import Data.Map (Map) import qualified Data.Map as M @@ -142,24 +148,15 @@ -- | Obligations with tagged variables (see `Tagged` and `unTag`) type TaggedObligation c v t = Obligation c (Tagged v) t +-- | Tri-traverse of Obligation+trObligation :: Applicative f => (c -> f c') -> (v -> f v') -> (t -> f t') -> Obligation c v t -> f (Obligation c' v' t')+trObligation = $(genTraverse ''Obligation)+ -- | 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+unTagM :: Applicative m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t]+unTagM f = traverse (trObligation pure f pure)  -- | Removing tagged (fresh) variables unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t]@@ -169,7 +166,7 @@ -- 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]+unTagMapM :: (Functor m,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

@@ -1,6 +1,6 @@ name:               structural-induction category:           Theorem Provers, Logic-version:            0.1+version:            0.1.1 license:            LGPL-3 license-file:       LICENSE author:             Dan Rosén@@ -38,6 +38,7 @@    build-depends:     base                      >= 4 && < 5,+    genifunctors,     mtl,     containers,     pretty,