diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/Language/Expression.hs b/Language/Expression.hs new file mode 100644 --- /dev/null +++ b/Language/Expression.hs @@ -0,0 +1,529 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| +Implements higher-ranked equivalents of 'Functor', 'Monad', 'Foldable' and +'Traversable'. +-} +module Language.Expression where + +import Control.Applicative (Alternative, (<|>)) +import Control.Monad ((<=<), (>=>)) +import Data.Monoid (Alt (..)) +import Data.Typeable (Typeable) + +import Control.Monad.Trans.Reader (ReaderT (..)) +import Control.Monad.Trans.Except (ExceptT (..)) +import qualified Control.Monad.Trans.State.Lazy as L +import qualified Control.Monad.Trans.State.Strict as S +import qualified Control.Monad.Trans.Writer.Lazy as L +import qualified Control.Monad.Trans.Writer.Strict as S + +import Data.Functor.Compose (Compose (..)) +import Data.Functor.Const (Const (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Functor.Product (Product (..)) +import Data.Functor.Reverse (Reverse (..)) +import Data.Functor.Sum (Sum (..)) + +infixr 1 ^>>= + +-------------------------------------------------------------------------------- +-- Functor / Monad +-------------------------------------------------------------------------------- + +{-| +Higher-ranked analogue of 'Functor'. +-} +class HFunctor (h :: (u -> *) -> u -> *) where + {-| + Higher-ranked analogue of 'fmap'. Has a default implementation in terms of + 'htraverse' for @'HTraversable' h@. + -} + hmap :: (forall b. t b -> t' b) -> h t a -> h t' a + + default hmap :: (HTraversable h) => (forall b. t b -> t' b) -> h t a -> h t' a + hmap f = runIdentity . htraverse (Identity . f) + +{-| +Half of the higher-ranked analogue of 'Monad'. +-} +class HPointed h where + {-| + Higher-ranked analogue of 'pure' or 'return'. + -} + hpure :: t a -> h t a + +{-| +Half of the higher-ranked analogue of 'Monad'. +-} +class HBind h where + {-| + Higher-ranked analogue of '>>='. + -} + (^>>=) :: h t a -> (forall b. t b -> h t' b) -> h t' a + +{-| + +Higher-ranked analogue of 'Monad'. + +NB there's no such thing as 'HApplicative' for a reason. Consider @f :: h t a -> +h t' a -> h ('Product' t t') a@, i.e. the higher-ranked analogue of @liftA2 (,) +:: f a -> f b -> f (a, b)@. Unfortunately @f@ can't exist, because @'Product'@ +pairs up values /of the same type/, and in our constructions, @h@ potentially +contains values of many types; @a@ just happens to be the one at the top level. +There's no guarantee that the two structures will have the same types inside to +pair together. +-} +class (HFunctor h, HPointed h, HBind h) => HMonad h + +{-| +Implements 'hmap' from just an 'HPointed' and 'HBind' instance. Can be used to +implement 'HFunctor' for your 'HMonad's that aren't 'HTraversable'. +-} +hliftM :: (HPointed h, HBind h) => (forall b. t b -> t' b) -> h t a -> h t' a +hliftM f x = x ^>>= hpure . f + +{-| +Higher-ranked analogue of 'Control.Monad.join'. +-} +hjoin :: (HBind h) => h (h t) a -> h t a +hjoin x = x ^>>= id + +-------------------------------------------------------------------------------- +-- Traversable +-------------------------------------------------------------------------------- + +{-| +Higher-ranked analogue of 'Traversable'. +-} +class (HFunctor h) => HTraversable h where + {-# MINIMAL htraverse | hsequence #-} + + {-| + Higher-ranked analogue of 'traverse'. + -} + htraverse + :: (Applicative f) + => (forall b. t b -> f (t' b)) -> h t a -> f (h t' a) + htraverse f = hsequence . hmap (Compose . f) + + {-| + Higher-ranked analogue of 'sequenceA'. + -} + hsequence + :: (Applicative f) + => h (Compose f t) a -> f (h t a) + hsequence = htraverse getCompose + +-- | An 'HTraversable' instance lets you do something similar to 'foldMap'. For +-- a more flexible operation, see 'hfoldMap'. +hfoldMapMonoid + :: (HTraversable h, Monoid m) + => (forall b. t b -> m) -> h t a -> m +hfoldMapMonoid f = getConst . htraverse (Const . f) + +hbindTraverse + :: (HTraversable h, HMonad h, Applicative f) + => (forall b. t b -> f (h t' b)) + -> h t a + -> f (h t' a) +hbindTraverse f = fmap hjoin . htraverse f + +-------------------------------------------------------------------------------- +-- Binary Classes +-------------------------------------------------------------------------------- + +{-| +Higher-ranked analogue of 'Data.Bifunctor.Bifunctor'. +-} +class HBifunctor (h :: (k -> *) -> (k -> *) -> k -> *) where + {-| + Higher-ranked analogue of 'Data.Bifunctor.bimap'. + -} + hbimap :: (forall b. s b -> s' b) + -> (forall b. t b -> t' b) + -> h s t a + -> h s' t' a + hfirst :: (forall b. s b -> s' b) -> h s t a -> h s' t a + hsecond :: (forall b. t b -> t' b) -> h s t a -> h s t' a + + default hbimap + :: (HBitraversable h) + => (forall b. s b -> s' b) + -> (forall b. t b -> t' b) + -> h s t a + -> h s' t' a + hbimap f g = runIdentity . hbitraverse (Identity . f) (Identity . g) + + hfirst f = hbimap f id + hsecond = hbimap id + +class (HBifunctor h) => HBitraversable h where + hbitraverse + :: (Applicative f) + => (forall b. s b -> f (s' b)) + -> (forall b. t b -> f (t' b)) + -> h s t a -> f (h s' t' a) + +hbifoldMapMonoid + :: (Monoid m, HBitraversable h) + => (forall b. s b -> m) -> (forall b. t b -> m) -> h s t a -> m +hbifoldMapMonoid f g = getConst . hbitraverse (Const . f) (Const . g) + +-------------------------------------------------------------------------------- +-- (Even) Higher-Ranked Binary Classes +-------------------------------------------------------------------------------- + +class HDuofunctor (h :: ((u -> *) -> u -> *) -> (u -> *) -> u -> *) where + hduomap + :: (forall g g' b. (forall c. g c -> g' c) -> s g b -> s' g' b) + -> (forall b. t b -> t' b) + -> h s t a + -> h s' t' a + + default hduomap + :: (HDuotraversable h) + => (forall g g' b. (forall c. g c -> g' c) -> s g b -> s' g' b) + -> (forall b. t b -> t' b) + -> h s t a + -> h s' t' a + hduomap f g = + runIdentity . + hduotraverse (\h -> Identity . f (runIdentity . h)) (Identity . g) + +hduomapFirst + :: HDuofunctor h + => (forall g g' b. (forall c. g c -> g' c) -> s g b -> s' g' b) + -> h s t a + -> h s' t a +hduomapFirst f = hduomap f id + +hduomapFirst' + :: (HDuofunctor h, HFunctor s) + => (forall g b. s g b -> s' g b) -> h s t a -> h s' t a +hduomapFirst' f = hduomapFirst (\g -> f . hmap g) + +hduomapSecond + :: (HDuofunctor h, HFunctor s) + => (forall b. t b -> t' b) -> h s t a -> h s t' a +hduomapSecond = hduomap hmap + +class HDuofunctor h => HDuotraversable h where + hduotraverse + :: (Applicative f) + => (forall g g' b. (forall c. g c -> f (g' c)) -> s g b -> f (s' g' b)) + -> (forall b. t b -> f (t' b)) + -> h s t a + -> f (h s' t' a) + +hduotraverseFirst + :: (HDuotraversable h, Applicative f) + => (forall g g' b. (forall c. g c -> f (g' c)) -> s g b -> f (s' g' b)) + -> h s t a + -> f (h s' t a) +hduotraverseFirst f = hduotraverse f pure + +hduotraverseFirst' + :: (HDuotraversable h, HTraversable s, Monad f) + => (forall g b. s g b -> f (s' g b)) -> h s t a -> f (h s' t a) +hduotraverseFirst' f = hduotraverseFirst (\g -> f <=< htraverse g) + +hduotraverseSecond + :: (HDuotraversable h, HTraversable s, Applicative f) + => (forall b. t b -> f (t' b)) -> h s t a -> f (h s t' a) +hduotraverseSecond = hduotraverse htraverse + +-------------------------------------------------------------------------------- +-- Folding +-------------------------------------------------------------------------------- + +{-| +This is a more flexible, higher-ranked version of 'Foldable'. While 'Foldable' +only allows you to fold into a 'Monoid', 'HFoldable' allows you to fold into +some arbitrary type constructor @k@. This means that the instance can take +advantage of additional structure inside @k@ and @h@, to combine internal +results in different ways, rather than just the 'mappend' available to +'foldMap'. + +Notice that if you have + +@ +instance ('Monoid' m) => 'HFoldableAt' ('Const' m) h +@ + +then 'hfoldMap' behaves very much like regular 'foldMap'. +-} +class HFoldableAt k h where + hfoldMap :: (forall b. t b -> k b) -> h t a -> k a + +{-| +For 'HFunctor's, provides an implementation of 'hfoldMap' in terms of a simple +'hfold'-like function. +-} +implHfoldMap + :: (HFunctor h) + => (h k a -> k a) + -> (forall b. t b -> k b) -> h t a -> k a +implHfoldMap g f = g . hmap f + +-- | A helper function for implementing instances with the general form @'Monad' +-- m => 'HFoldableAt' ('Compose' m t) h@. I.e. folding that requires a monadic +-- context of some kind. +implHfoldMapCompose + :: (HTraversable h, Monad m) + => (h k a -> m (k a)) + -> (forall b. t b -> Compose m k b) -> h t a -> Compose m k a +implHfoldMapCompose f = implHfoldMap (Compose . (htraverse getCompose >=> f)) + + +{-| +Higher-ranked equivalent of 'Data.Foldable.fold'. +-} +hfold :: HFoldableAt t h => h t a -> t a +hfold = hfoldMap id + + +-- | Fold in an applicative context. +hfoldA :: (HFoldableAt (Compose f t) h, Applicative f) => h t a -> f (t a) +hfoldA = hfoldMapA pure + + +-- | Fold in an applicative context. +hfoldMapA :: (HFoldableAt (Compose f k) h, Applicative f) => (forall b. t b -> f (k b)) -> h t a -> f (k a) +hfoldMapA f = getCompose . hfoldMap (Compose . f) + + +-- | 'hfoldTraverse' is to 'hfoldMap' as 'htraverse' is to 'hmap'. +hfoldTraverse + :: (HFoldableAt k h, HTraversable h, Applicative f) + => (forall b. t b -> f (k b)) + -> h t a + -> f (k a) +hfoldTraverse f = fmap hfold . htraverse f + + +class HBifoldableAt k h where + hbifoldMap :: (forall b. f b -> k b) -> (forall b. g b -> k b) -> h f g a -> k a + +hbifold :: (HBifoldableAt k h) => h k k a -> k a +hbifold = hbifoldMap id id + + +class HDuofoldableAt k h where + hduofoldMap + :: (HTraversable s) + => (forall g b. (forall c. g c -> k c) -> s g b -> k b) + -> (forall b. t b -> k b) + -> h s t a + -> k a + + +implHduofoldMap + :: (HDuofunctor h, HFunctor s) + => ((forall g b. (forall c. g c -> k c) -> s g b -> k b) -> h s k a -> k a) + -> (forall g b. (forall c. g c -> k c) -> s g b -> k b) + -> (forall b. t b -> k b) + -> h s t a + -> k a +implHduofoldMap h f g = h f . hduomap hmap g + + +implHduofoldMapCompose + :: (HDuotraversable h, HTraversable s, Monad m) + => ((forall g b. (forall c. g c -> m (k c)) -> s g b -> m (k b)) -> h s k a -> m (k a)) + -> (forall g b. (forall c. g c -> Compose m k c) -> s g b -> Compose m k b) + -> (forall b. t b -> Compose m k b) + -> h s t a + -> Compose m k a +implHduofoldMapCompose f = + implHduofoldMap + (\g -> + Compose . + (hduotraverseSecond getCompose >=> + f (\h -> getCompose . g (Compose . h)))) + +-------------------------------------------------------------------------------- +-- Free Monads +-------------------------------------------------------------------------------- + +{-| +@'HFree' h@ is a higher-ranked free monad over the higher-ranked functor @h@. +That means that given @'HFunctor' h@, we get @'HMonad' ('HFree' h)@ for free. +-} +data HFree h t a + = HPure (t a) + | HWrap (h (HFree h t) a) + deriving (Typeable) + +instance HFunctor h => HFunctor (HFree h) where + hmap = hliftM + +instance HPointed (HFree h) where + hpure = HPure + +instance HFunctor h => HBind (HFree h) where + HPure x ^>>= f = f x + HWrap x ^>>= f = HWrap (hmap (^>>= f) x) + +instance HFunctor h => HMonad (HFree h) + + +instance (HFoldableAt k h) => HFoldableAt k (HFree h) where + hfoldMap f = \case + HPure x -> f x + HWrap x -> hfoldMap (hfoldMap f) x + + +instance HDuofoldableAt k HFree where + hduofoldMap g f = \case + HPure x -> f x + HWrap x -> g (hduofoldMap g f) x + + +instance HTraversable h => HTraversable (HFree h) where + htraverse f = \case + HPure x -> HPure <$> f x + HWrap x -> HWrap <$> htraverse (htraverse f) x + + +instance HDuofunctor HFree +instance HDuotraversable HFree where + hduotraverse g f = \case + HPure x -> HPure <$> f x + HWrap x -> HWrap <$> g (hduotraverse g f) x + +-------------------------------------------------------------------------------- +-- Higher-ranked instances for standard functors +-------------------------------------------------------------------------------- + +-- 'Compose' lifts a regular 'Functor'/'Monad'/etc into the higher-ranked +-- version + +instance (Functor f) => HFunctor (Compose f) where + hmap f = Compose . fmap f . getCompose + +instance (Applicative f) => HPointed (Compose f) where + hpure = Compose . pure + +instance (Monad f) => HBind (Compose f) where + Compose x ^>>= f = Compose (x >>= getCompose . f) + +instance (Traversable f) => HTraversable (Compose f) where + htraverse f = fmap Compose . traverse f . getCompose + +-- | e.g. @('Monoid' m, 'Foldable' f) => 'HFoldableAt' ('Const' m) ('Compose' f)@ +instance (Alternative g, Foldable f) => HFoldableAt g (Compose f) where + hfoldMap f = getAlt . foldMap (Alt . f) . getCompose + + +-------------------------------------------------------------------------------- +-- 'Product' + +instance HFunctor (Product f) +instance HTraversable (Product f) where + htraverse f (Pair x y) = Pair x <$> f y + +instance HBifunctor Product +instance HBitraversable Product where + hbitraverse f g (Pair x y) = Pair <$> f x <*> g y + +instance (Alternative k) => HBifoldableAt k Product where + hbifoldMap f g (Pair x y) = f x <|> g y + +instance (Alternative k) => HFoldableAt k (Product k) where + hfoldMap = hbifoldMap id + +-------------------------------------------------------------------------------- +-- 'Reverse' (note there's nothing for the instances to reverse) + +instance HFunctor Reverse +instance HTraversable Reverse where + htraverse f (Reverse x) = Reverse <$> f x + +instance HPointed Reverse where + hpure = Reverse + +instance HBind Reverse where + Reverse x ^>>= f = f x + +instance HMonad Reverse + +instance HFoldableAt k Reverse where + hfoldMap f (Reverse x) = f x + +-------------------------------------------------------------------------------- +-- 'Sum' + +instance HFunctor (Sum f) +instance HTraversable (Sum f) where + htraverse _ (InL x) = pure (InL x) + htraverse f (InR y) = InR <$> f y + +instance HBifunctor Sum +instance HBitraversable Sum where + hbitraverse f _ (InL x) = InL <$> f x + hbitraverse _ g (InR y) = InR <$> g y + +instance HPointed (Sum f) where + hpure = InR + +instance HBind (Sum f) where + InL x ^>>= _ = InL x + InR y ^>>= f = f y + +instance HMonad (Sum f) + +instance HBifoldableAt k Sum where + hbifoldMap f _ (InL x) = f x + hbifoldMap _ g (InR y) = g y + +instance HFoldableAt k (Sum k) where + hfoldMap = hbifoldMap id + +-------------------------------------------------------------------------------- +-- 'StateT' + +instance HFunctor (S.StateT s) where + hmap f (S.StateT k) = S.StateT (f . k) + +instance HFunctor (L.StateT s) where + hmap f (L.StateT k) = L.StateT (f . k) + +-------------------------------------------------------------------------------- +-- 'WriterT' + +instance HFunctor (S.WriterT w) where + hmap f (S.WriterT x) = S.WriterT (f x) + +instance HFunctor (L.WriterT w) where + hmap f (L.WriterT x) = L.WriterT (f x) + +-------------------------------------------------------------------------------- +-- 'ReaderT' + +instance HFunctor (ReaderT r) where + hmap f (ReaderT k) = ReaderT (f . k) + +instance HPointed (ReaderT r) where + hpure = ReaderT . const + +instance HBind (ReaderT r) where + ReaderT k ^>>= f = ReaderT (\r -> runReaderT (f (k r)) r) + +instance HMonad (ReaderT r) + +-------------------------------------------------------------------------------- +-- ExceptT + +instance HFunctor (ExceptT e) where + hmap f (ExceptT x) = ExceptT (f x) diff --git a/Language/Expression/Choice.hs b/Language/Expression/Choice.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Choice.hs @@ -0,0 +1,228 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Language.Expression.Choice where + -- ( + -- -- * Expressions + -- HFree'(..) + -- , _EVar' + -- , _EOp' + -- , squashExpression + -- , eop' + + -- -- * HTraversable union + -- , OpChoice(..) + -- , ChooseOp(..) + -- , SubsetOp(..) + -- ) where + +import Data.Data + +-- import Data.Functor.Classes + +import Data.Union + +import Control.Lens hiding (op) + +import Language.Expression + +-------------------------------------------------------------------------------- +-- Operator List Union +-------------------------------------------------------------------------------- + +-- | Form the union of a list of operators. This creates an operator which is a +-- choice from one of its constituents. +-- +-- For example, @'OpChoice' '[NumOp, EqOp]@ is an operator that can either +-- represent an arithmetic operation or an equality comparison. +data OpChoice ops (t :: * -> *) a where + OpThis :: op t a -> OpChoice (op : ops) t a + OpThat :: OpChoice ops t a -> OpChoice (op : ops) t a + deriving (Typeable) + +_OpThis :: Prism' (OpChoice (op : ops) t a) (op t a) +_OpThis = prism' OpThis $ \case + OpThis x -> Just x + OpThat _ -> Nothing + +_OpThat :: Prism' (OpChoice (op : ops) t a) (OpChoice ops t a) +_OpThat = prism' OpThat $ \case + OpThis _ -> Nothing + OpThat x -> Just x + +noOps :: OpChoice '[] t a -> x +noOps = \case + +instance HFunctor (OpChoice '[]) where + hmap _ = noOps + +instance HTraversable (OpChoice '[]) where + htraverse _ = noOps + +instance HFoldableAt k (OpChoice '[]) where + hfoldMap _ = noOps + +-- instance HEq (OpChoice '[]) where +-- liftHEq _ _ _ = noOps + +instance (HFunctor op, HFunctor (OpChoice ops)) => + HFunctor (OpChoice (op : ops)) where + + hmap f = \case + OpThis x -> OpThis (hmap f x) + OpThat x -> OpThat (hmap f x) + +instance (HTraversable op, HTraversable (OpChoice ops)) => + HTraversable (OpChoice (op : ops)) where + + htraverse f = \case + OpThis x -> OpThis <$> htraverse f x + OpThat x -> OpThat <$> htraverse f x + +instance (HFoldableAt k op, HFoldableAt k (OpChoice ops)) => + HFoldableAt k (OpChoice (op : ops)) where + + hfoldMap f = \case + OpThis x -> hfoldMap f x + OpThat x -> hfoldMap f x + +-- instance (HEq op, HEq (OpChoice ops)) => +-- HEq (OpChoice (op : ops)) where + +-- liftHEq le eq (OpThis x) (OpThis y) = liftHEq le eq x y +-- liftHEq le eq (OpThat x) (OpThat y) = liftHEq le eq x y +-- liftHEq _ _ _ _ = False + + +-- instance (HEq (OpChoice ops), Eq1 t) => Eq1 (OpChoice ops t) where +-- liftEq = liftLiftEq +-- instance (Eq1 (OpChoice ops t), Eq a) => Eq (OpChoice ops t a) where +-- (==) = liftEq (==) + + +newtype AsOp (t :: * -> *) a op = AsOp (op t a) + +makeWrapped ''AsOp + +choiceToUnion :: OpChoice ops t a -> Union (AsOp t a) ops +choiceToUnion = \case + OpThis x -> This (AsOp x) + OpThat x -> That (choiceToUnion x) + +unionToChoice :: Union (AsOp t a) ops -> OpChoice ops t a +unionToChoice = \case + This (AsOp x) -> OpThis x + That x -> OpThat (unionToChoice x) + +_OpChoice + :: Iso (OpChoice ops t a) (OpChoice ops' t' a') + (Union (AsOp t a) ops) (Union (AsOp t' a') ops') +_OpChoice = iso choiceToUnion unionToChoice + + +-- | This class provides a low-boilerplate way of lifting individual operators +-- into a union, and extracting operators from a union. +class ChooseOp op ops where + -- | Project a single operator from a union which contains it. + chooseOp :: Prism' (OpChoice ops t a) (op t a) + +instance UElem op ops i => ChooseOp op ops where + chooseOp = _OpChoice . uprism . _Wrapped + + +class SubsetOp ops1 ops2 where + subsetOp :: Prism' (OpChoice ops2 t a) (OpChoice ops1 t a) + +instance USubset ops1 ops2 is => SubsetOp ops1 ops2 where + subsetOp = _OpChoice . usubset . from _OpChoice + +-------------------------------------------------------------------------------- +-- Expressions over a choice of operators +-------------------------------------------------------------------------------- + +-- | @'HFree'' ops v a@ is a higher-order free monad over the list of operators +-- @ops@ with variables in the type @v@ and it represents a value of type @a@. +-- +-- Intuitively, it represents an expression which may contain operations from +-- any of the operators in the list @ops@. +newtype HFree' ops v a = HFree' { getHFree' :: HFree (OpChoice ops) v a } + deriving (Typeable) + +deriving instance + (Data (HFree (OpChoice ops) v a), Typeable (HFree' ops v a)) => + Data (HFree' ops v a) + +-- instance (HEq (OpChoice ops)) => HEq (HFree' ops) where +-- liftHEq le eq (HFree' x) (HFree' y) = liftHEq le eq x y + +-- instance (Eq1 v, HEq (OpChoice ops)) => Eq1 (HFree' ops v) where +-- liftEq = liftLiftEq + +-- instance (Eq1 v, HEq (OpChoice ops), Eq a) => Eq (HFree' ops v a) where +-- (==) = eq1 + + +-- TODO: Figure out type roles so these instances can be derived by +-- GeneralizedNewtypeDeriving + +instance (HFunctor (OpChoice ops)) => HFunctor (HFree' ops) where + hmap f = HFree' . hmap f . getHFree' + +instance (HTraversable (OpChoice ops)) => HTraversable (HFree' ops) where + htraverse f = fmap HFree' . htraverse f . getHFree' + +instance HPointed (HFree' ops) where + hpure = HFree' . hpure + +instance (HFunctor (OpChoice ops)) => HBind (HFree' ops) where + x ^>>= f = (HFree' . (^>>= (getHFree' . f)) . getHFree') x + +instance (HFunctor (OpChoice ops)) => HMonad (HFree' ops) where + +instance (HFoldableAt k (OpChoice ops), HFunctor (OpChoice ops)) => + HFoldableAt k (HFree' ops) where + hfoldMap f (HFree' x) = hfoldMap f x + +-- | Squash a composition of expressions over different operators into a +-- single-layered expression over a choice of the two operators. +squashExpression + :: (HFunctor op1, + HFunctor op2, + HFunctor (OpChoice ops), + ChooseOp op1 ops, + ChooseOp op2 ops) + => HFree op1 (HFree op2 v) a -> HFree' ops v a +squashExpression + = HFree' + . hjoin + . hmap (hduomapFirst' (review chooseOp)) + . hduomapFirst' (review chooseOp) + -- (review chooseOp) + +hwrap' + :: (HFunctor op, HFunctor (OpChoice ops), ChooseOp op ops) + => op (HFree' ops v) a -> HFree' ops v a +hwrap' = HFree' . HWrap . review chooseOp . hmap getHFree' + +-------------------------------------------------------------------------------- +-- Lenses +-------------------------------------------------------------------------------- + +makeWrapped ''HFree' diff --git a/Language/Expression/Example.hs b/Language/Expression/Example.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Example.hs @@ -0,0 +1,422 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +{-# OPTIONS_GHC -fno-warn-unused-imports #-} + +{-| +"Language.Expression" provides a way of forming strongly types expression +languages from /operators/, via 'HFree'. This module is an explanation of how +that works, via a simple example. + +This module is intended to be read via Haddock. +-} +module Language.Expression.Example where + +import Data.Functor.Identity (Identity (..)) + +import Control.Monad.State + +import Data.Map (Map) +import qualified Data.Map as Map + +import Data.SBV (EqSymbolic (..), OrdSymbolic (..), + Predicate, SBV, Symbolic, isTheorem, + ite, literal, symbolic) + +import Language.Expression + +-------------------------------------------------------------------------------- +-- * Operators + +{-$ +An /operator/ is a type constructor @op@ of kind @(* -> *) -> * -> *@. @op t +a@ should be seen as a way of combining @t@-objects which has a result type +@a@. + +'SimpleOp' is an example of an operator type. +-} + + +{-| +An operator type has two arguments. @t@ is a type constructor used to refer to +expressions. @a@ is the semantic type of the expression formed by the operator. +-} +data SimpleOp t a where + -- | Given two int expressions, we may add them. Notice how we refer to expressions + -- recursively with the type constructor parameter @t@. + Add :: t Integer -> t Integer -> SimpleOp t Integer + + -- | Given two int expressions, we may compare them for equality. Notice the + -- types of the arguments to the operator do not appear in the result type at + -- all. + Equal :: t Integer -> t Integer -> SimpleOp t Bool + + -- | Operator constructors can have any number of arguments, and you can mix + -- argument types. + IfThenElse :: t Bool -> t Integer -> t Integer -> SimpleOp t Integer + + -- | An operator does not have to actually combine expressions. It may produce an + -- expression from a basic value, i.e. a literal int. 'HFree' itself does + -- /not/ provide literals so they must be encoded in operators. + Literal :: Integer -> SimpleOp t Integer + +-- ** Type Classes + +{-$ +Most useful operators are instances of 'HFunctor' (which provides 'hmap') and +'HTraversable' (which provides 'htraverse'). These are higher-ranked analogues +of 'Functor' and 'Traversable' from @base@. Compare the type signatures of +'fmap' and 'hmap': + +@ +'fmap' :: ('Functor' f) => (a -> b) -> f a -> f b +'hmap' :: ('HFunctor' h) => (forall b. s b -> t b) -> h s a -> h t a +@ + +'fmap' transforms the @*@-kinded type argument to @f@, while 'hmap' transforms +the @(* -> *)@-kinded type constructor argument to @h@. + +So in order for an operator to have an instance of 'HFunctor', it must be +possible to swap out sub-expressions inside it. This is the case for our +'SimpleOp'. + +'HTraversable' has a similar relationship with 'Traversable'. 'htraverse' +adds an applicative context to 'hmap'\'s transformations: + +@ +'traverse' :: ('Traversable' t, 'Applicative' f) => (a -> f b) -> t a -> f (t b) +'htraverse' :: ('HTraversable' h, 'Applicative' f) => (forall b. s b -> f (t b)) -> h s a -> f (h t a) +@ + +There is a default implementation of 'hmap' in terms of 'htraverse'. +-} + +instance HFunctor SimpleOp +instance HTraversable SimpleOp where + htraverse f = \case + Add x y -> Add <$> f x <*> f y + Equal x y -> Equal <$> f x <*> f y + IfThenElse x y z -> IfThenElse <$> f x <*> f y <*> f z + Literal x -> pure (Literal x) + +-------------------------------------------------------------------------------- +-- * Variables + +{-$ +As well as operators, expressions contain variables. Variables are also strongly +typed. A variable type @v@ has kind @* -> *@. The type parameter tells us the +type of the value that the variable is meant to represent. +-} + + +{-| +Notice that @a@ is a phantom type here (and it will be for most variable type +constructors). It is only used to restrict the type of values that are +representable by these variables. In this case, we only want to be able to store +integers so the only constructor has return type 'Integer'. It also contains a +'String' to be used as the variable name. +-} +data SimpleVar a where + SimpleVar :: String -> SimpleVar Integer + +-------------------------------------------------------------------------------- +-- * Expressions + +{-| +Now that we have defined our operators and variables, @'HFree' 'SimpleOp' +'SimpleVar' a@ is a syntax tree for a strongly typed expresson language. +-} +type SimpleExpr = HFree SimpleOp SimpleVar + +-------------------------------------------------------------------------------- +-- * A DSL + +{-$ +We can write simple wrapper functions to form a DSL for our expression language. +-} + +{-| + +@ +var = 'hpure' . 'SimpleVar' +@ + +-} +var :: String -> SimpleExpr Integer +var = hpure . SimpleVar + +{-| + +@ +x ^+ y = 'HWrap' ('Add' x y) +@ + +-} +(^+) :: SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer +x ^+ y = HWrap (Add x y) + +{-| + +@ +x ^== y = 'HWrap' ('Equal' x y) +@ + +-} +(^==) :: SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Bool +x ^== y = HWrap (Equal x y) + +{-| + +@ +ifThenElse x y z = 'HWrap' ('IfThenElse' x y z) +@ + +-} +ifThenElse :: SimpleExpr Bool -> SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer +ifThenElse x y z = HWrap (IfThenElse x y z) + +{-| + +@ +lit = 'HWrap' . 'Literal' +@ + +-} +lit :: Integer -> SimpleExpr Integer +lit = HWrap . Literal + +-------------------------------------------------------------------------------- +-- ** Example Expression + +{-| +Here's an example of expression written using this DSL. + +@ +exampleExpr = 'ifThenElse' ('var' "x" '.==' 'lit' 10) ('var' "y") ('var' "y" '.+' 'lit' 5) +exampleExpr ~ if (x = 10) then y else y + 5 +@ +-} +exampleExpr :: SimpleExpr Integer +exampleExpr = ifThenElse (var "x" ^== lit 10) (var "y") (var "y" ^+ lit 5) + +-------------------------------------------------------------------------------- +-- * Expression Manipulation + +{-$ +If @op@ is an 'HFunctor', then @'HFree' op@ is an 'HMonad'. 'HMonad' defines +'hpure' (c.f. 'pure' or 'return'): + +@ +'hpure' :: ('HMonad' h) => t a -> h t a +'return' :: ('Monad' m) => a -> m a +@ + +and '^>>=' (c.f. '>>='): + +@ +('>>=') :: ('Monad' m) => m a -> (a -> m b) -> m b +('^>>=') :: ('HMonad' h) => h s a -> (forall b. s b -> h t b) -> h t a +@ + +In the case of @'HFree' op@, 'hpure' produces an expression containing a single +variable: + +@ +'hpure' :: v a -> 'HFree' op v a +@ +-} + +-- ** Substitution + +{-$ +'^>>=' substitutes variables inside expressions. +-} + +{-| +'exampleExpr', with @x@ replaced by @z + 5@. + +@ +exampleExpr2 = + exampleExpr '^>>=' \v@('SimpleVar' nm) -> + if nm == "x" then 'var' "x" '^+' 'lit' 5 else 'hpure' v + +exampleExpr2 ~ if ((z + 5) = 10) then y else y + 5 +@ + +-} +exampleExpr2 :: SimpleExpr Integer +exampleExpr2 = + exampleExpr ^>>= \v@(SimpleVar nm) -> + if nm == "x" then var "z" ^+ lit 5 else hpure v + +-- ** Traversal + +{-$ +When @op@ is an 'HTraversable', 'HFree' is also an 'HTraversable'. This can be +used, for example, to evaluate variables in an expression. +-} + +{-| +This is a function that knows the value of variables with certain names. It will +return 'Nothing' if it doesn't know how to evaluate a particular variable. + +@ +evalXOrY ('SimpleVar' "x") = 'Just' 1 +evalXOrY ('SimpleVar' "y") = 'Just' 2 +evalXOrY _ = 'Nothing' +@ + +It might seem strange that we can return @'Just' ('Identity' 1)@ when the +function says it returns a @'Maybe' ('Identity' a)@ for polymorphic @a@. This +works because the constructor 'SimpleVar' must be 'Integer'-valued, so when we match +on it, GHC generates the constraint @a ~ 'Integer'@ and it will happily accept an +'Integer'. + +Notice that, for @s ~ 'SimpleVar'@, @t ~ 'Identity'@ and @f ~ 'Maybe'@, + +@ +evalXOrY :: forall a. s a -> f (t a) +@ + +This means that we can traverse using this function: + +>>> htraverse evalXOrY exampleExpr +htraverse evalXOrY exampleExpr :: Maybe (HFree SimpleOp Identity Integer) +htraverse evalXOrY exampleExpr ~ Just (if (1 = 10) then 2 else 2 + 5) + +>>> htraverse evalXOrY exampleExpr2 +htraverse evalXOrY exampleExpr2 :: Maybe (HFree SimpleOp Identity Integer) +htraverse evalXOrY exampleExpr2 ~ Nothing + +There was a variable (@z@) that @evalXOrY@ didn't know how to evaluate, so the +traversal resulted in 'Nothing'! + +-} +evalXOrY :: SimpleVar a -> Maybe (Identity a) +evalXOrY (SimpleVar "x") = Just (Identity 1) +evalXOrY (SimpleVar "y") = Just (Identity 2) +evalXOrY _ = Nothing + +-------------------------------------------------------------------------------- +-- * Evaluating Expressions + +{-$ +The 'HFoldableAt' type class provides the mechanism for evaluating operators, +and hence expressions. + +@ +'hfoldMap' :: ('HFoldableAt' k h) => (forall b. t b -> k b) -> h t b -> k b +@ + +Implemented in terms of this is + +@ +'hfoldTraverse' + :: ('HFoldableAt' k h, 'HTraversable' h, 'Applicative' f) + => (forall b. t b -> f (k b)) + -> h t a + -> f (k a) +'hfoldTraverse' f = 'fmap' ('hfoldMap' 'id') . 'htraverse' f +@ + +This function will allow us to evaluate our expressions to ground values: + +>>> hfoldTraverse evalXOrY exampleExpr +Just (Identity 7) + +>>> hfoldTraverse evalXOrY exampleExpr2 +Nothing + +-} + +instance HFoldableAt Identity SimpleOp where + hfoldMap f s = case s of + Add x y -> (+) <$> f x <*> f y + Equal x y -> (==) <$> f x <*> f y + IfThenElse x y z -> + let ite' c a b = if c then a else b + in ite' <$> f x <*> f y <*> f z + Literal x -> pure x + +-------------------------------------------------------------------------------- +-- ** Evaluating Variables Symbolically + +{-$ +With the help of @sbv@, we can evaluate expressions symbolically in order to +prove things about them. +-} + +{-| +Here's a function that converts variables in 'SimpleVar' to symbolic values. It +needs a @'Map' 'String' ('SBV' 'Integer')@ stateful environment in order to +remember variables that already have symbolic values, because 'SBV' will give +you different variables on two different calls of @'symbolic' x@ for the same +@x@. +-} +evalVarSymbolic :: SimpleVar a -> StateT (Map String (SBV Integer)) Symbolic (SBV a) +evalVarSymbolic (SimpleVar nm) = do + existingSymbol <- gets (Map.lookup nm) + case existingSymbol of + Just x -> return x + Nothing -> do + newSymbol <- lift (symbolic nm) + modify (Map.insert nm newSymbol) + return newSymbol + +-------------------------------------------------------------------------------- +-- ** Evaluating Expressions Symbolically + +{-$ +We need an instance of @'HFoldableAt' 'SBV' 'SimpleOp'@ to do symbolic +evaluation, implemented like so: + +@ +instance 'HFoldableAt' 'SBV' 'SimpleOp' where + 'hfoldMap' = 'implHfoldMap' $ \s -> case s of + 'Add' x y -> x '+' y + 'Equal' x y -> x '.==' y + 'IfThenElse' x y z -> 'ite' x y z + 'Literal' x -> 'literal' x +@ +-} + +instance HFoldableAt SBV SimpleOp where + hfoldMap = implHfoldMap $ \s -> case s of + Add x y -> x + y + Equal x y -> x .== y + IfThenElse x y z -> ite x y z + Literal x -> literal x + +{-| +Now we can evaluate expressions symbolically and use @sbv@ to prove things about +them. + +@ +evalSimpleExprSymbolic = 'hfoldTraverse' 'evalVarSymbolic' +@ +-} +evalSimpleExprSymbolic :: SimpleExpr a -> StateT (Map String (SBV Integer)) Symbolic (SBV a) +evalSimpleExprSymbolic = hfoldTraverse evalVarSymbolic + +{-| + +Let's ask @sbv@ to prove that our expression always returns a value no less than +the variable @y@. + +@ +examplePredicate = 'flip' 'evalStateT' 'mempty' $ do + expr <- 'evalSimpleExprSymbolic' 'exampleExpr' + y <- 'evalSimpleExprSymbolic' ('var' "y") + 'return' ('expr' '.>=' y) +@ + +>>> isTheorem examplePredicate +True + +-} +examplePredicate :: Predicate +examplePredicate = flip evalStateT mempty $ do + expr <- evalSimpleExprSymbolic exampleExpr + y <- evalSimpleExprSymbolic (var "y") + return (expr .>= y) diff --git a/Language/Expression/GeneralOp.hs b/Language/Expression/GeneralOp.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/GeneralOp.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +module Language.Expression.GeneralOp where + +-- import Data.Typeable + +import Data.Vinyl +-- import Data.Vinyl.Functor +-- import Data.Vinyl.TypeLevel + +import Language.Expression +import Language.Expression.Pretty + +data GeneralOp op t a where + Op :: op as r -> Rec t as -> GeneralOp op t r + +class EvalOpAt k op where + evalMany :: op as r -> Rec k as -> k r + +-- class EqOpMany op where +-- liftEqMany +-- :: op as a -> op bs b + +-- -> (forall xs. (AllConstrained Eq xs, RecApplicative xs) => +-- Rec f xs -> Rec g xs -> Bool) + +-- -> Rec f as -> Rec g bs -> Bool + + +class PrettyOp op where + prettysPrecOp :: Pretty1 t => Int -> op as a -> Rec t as -> ShowS + +instance HFunctor (GeneralOp op) where + +instance HTraversable (GeneralOp op) where + htraverse f = \case + Op o args -> Op o <$> rtraverse f args + + +instance (EvalOpAt k op) => HFoldableAt k (GeneralOp op) where + hfoldMap f = \case + Op o args -> evalMany o (rmap f args) + + +-- instance EqOpMany op => HEq (GeneralOp op) where +-- liftHEq le _ (Op o1 (xs :: Rec f as)) (Op o2 (ys :: Rec g bs)) = +-- liftEqMany o1 o2 liftEqAll xs ys + +-- where +-- liftEqAll +-- :: (AllConstrained Eq xs, RecApplicative xs) +-- => Rec f xs -> Rec g xs -> Bool +-- liftEqAll (xs' :: Rec f xs) ys' = +-- let +-- eqList :: Rec (Lift (->) f (Lift (->) g (Const Bool))) xs +-- eqList = rpureConstrained (Proxy :: Proxy Eq) +-- (Lift $ \x -> Lift $ Const . le (==) x) +-- in and . recordToList $ eqList <<*>> xs' <<*>> ys' + +instance PrettyOp op => Pretty2 (GeneralOp op) where + prettys2Prec p = \case + Op op args -> prettysPrecOp p op args diff --git a/Language/Expression/Pretty.hs b/Language/Expression/Pretty.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Pretty.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-| + +Pretty printing for expressions. + +-} +module Language.Expression.Pretty + ( + -- * Classes + Pretty(..) + , prettys + , Pretty1(..) + , prettys1 + , Pretty2(..) + , prettys2 + , Pretty3(..) + , prettys3 + -- * Combinators + , putPretty + , prettys1PrecBinop + , prettys1PrecUnop + ) where + +import Data.Functor.Const +import Data.List (intersperse) +import Data.Monoid (Endo (..)) + +import Language.Expression +import Language.Expression.Choice +import Language.Expression.Scope + +-------------------------------------------------------------------------------- +-- Convenience +-------------------------------------------------------------------------------- + +putPretty :: Pretty a => a -> IO () +putPretty = putStrLn . pretty + +-------------------------------------------------------------------------------- +-- Combinators +-------------------------------------------------------------------------------- + +prettys1PrecUnop :: Pretty1 t => Int -> String -> Int -> t a -> ShowS +prettys1PrecUnop opPrec opStr p x = + showParen (p > opPrec) $ showString opStr . prettys1Prec (opPrec + 1) x + +prettys1PrecBinop + :: (Pretty1 f, Pretty1 g) + => Int -> String -> Int -> f a -> g b -> ShowS +prettys1PrecBinop opPrec opStr p x y = + showParen (p > opPrec) $ + prettys1Prec (opPrec + 1) x . showString opStr . prettys1Prec (opPrec + 1) y + +-------------------------------------------------------------------------------- +-- Pretty typeclasses +-------------------------------------------------------------------------------- + +prettys :: Pretty a => a -> ShowS +prettys = prettysPrec 0 + +prettys1 :: Pretty1 t => t a -> ShowS +prettys1 = prettys1Prec 0 + +prettys2 :: (Pretty2 op, Pretty1 t) => op t a -> ShowS +prettys2 = prettys2Prec 0 + +prettys3 :: (Pretty3 h, Pretty2 s, Pretty1 t) => h s t a -> ShowS +prettys3 = prettys3Prec 0 + +class Pretty a where + {-# MINIMAL pretty | prettysPrec #-} + + pretty :: a -> String + prettysPrec :: Int -> a -> ShowS + + pretty x = prettys x "" + prettysPrec _ x s = pretty x ++ s + +class Pretty1 t where + {-# MINIMAL pretty1 | prettys1Prec #-} + + pretty1 :: t a -> String + pretty1 x = prettys1 x "" + + prettys1Prec :: Int -> t a -> ShowS + prettys1Prec _ x s = pretty1 x ++ s + +class Pretty2 op where + {-# MINIMAL pretty2 | prettys2Prec #-} + + pretty2 :: (Pretty1 t) => op t a -> String + pretty2 x = prettys2 x "" + + prettys2Prec :: (Pretty1 t) => Int -> op t a -> ShowS + prettys2Prec _ x s = pretty2 x ++ s + +class Pretty3 h where + {-# MINIMAL pretty3 | prettys3Prec #-} + + pretty3 :: (Pretty2 s, Pretty1 t) => h s t a -> String + pretty3 x = prettys3 x "" + + prettys3Prec :: (Pretty2 s, Pretty1 t) => Int -> h s t a -> ShowS + prettys3Prec _ x s = pretty3 x ++ s + +-------------------------------------------------------------------------------- +-- Combinatory instances +-------------------------------------------------------------------------------- + +instance {-# OVERLAPPABLE #-} (Pretty1 t) => Pretty (t a) where + prettysPrec = prettys1Prec + +instance {-# OVERLAPPABLE #-} (Pretty2 f, Pretty1 t) => Pretty1 (f t) where + prettys1Prec = prettys2Prec + +instance {-# OVERLAPPABLE #-} (Pretty3 h, Pretty2 s) => Pretty2 (h s) where + prettys2Prec = prettys3Prec + +instance Pretty1 (Const String) where + pretty1 (Const x) = x + +instance (Pretty2 op) => Pretty2 (HFree op) where + prettys2Prec p = \case + HPure x -> prettys1Prec p x + HWrap op -> prettys2Prec p op + +instance (Pretty1 t) => Pretty2 (BV t) where + prettys2Prec p = foldBV (prettys1Prec p) (prettys1Prec p) + +instance (Pretty2 h, Pretty1 t) => Pretty2 (Scope t h) where + prettys2Prec p (Scope x) = prettys2Prec p x + +instance (Pretty2 h, Pretty1 t) => Pretty2 (Scoped h t) where + prettys2Prec p (Scoped x) = prettys2Prec p x + + +instance (Pretty3 h) => Pretty2 (SFree h) where + prettys2Prec p = \case + SPure x -> prettys1Prec p x + SWrap x -> prettys3Prec p x + + +instance (Pretty2 (OpChoice ops)) => Pretty2 (HFree' ops) where + prettys2Prec p = prettys2Prec p . getHFree' + +instance (Pretty2 (OpChoice '[])) where + pretty2 = noOps + + +instance (Pretty2 op, Pretty2 (OpChoice ops)) => + Pretty2 (OpChoice (op : ops)) where + prettys2Prec p = \case + OpThis x -> prettys2Prec p x + OpThat x -> prettys2Prec p x + +instance {-# OVERLAPPING #-} Pretty String where + pretty = id + +instance {-# OVERLAPPING #-} Pretty a => Pretty [a] where + prettysPrec _ xs = (appEndo . mconcat . map Endo) ( + showString "[ " : (intersperse (showString "\n, ") . map prettys) xs) . + showString "\n]" + +instance {-# OVERLAPPING #-} Pretty a => Pretty (Maybe a) where + prettysPrec p (Just x) = prettysPrec p x + prettysPrec _ Nothing = \r -> "" ++ r + +instance Pretty () where + pretty = show diff --git a/Language/Expression/Prop.hs b/Language/Expression/Prop.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Prop.hs @@ -0,0 +1,170 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{-| + +Propositions and combinators for conveniently constructing them. + +-} +module Language.Expression.Prop + ( + -- * Proposition Types + Prop + , Prop' + -- * DSL + , expr + , plit + , pnot + , (*&&) + , (*||) + , (*->) + , (*<->) + , propAnd + , propOr + -- * HTraversable + , LogicOp(..) + ) where + +import Control.Applicative (liftA2) +import Data.List (foldl') +-- import Data.Typeable + +-- import Data.Functor.Classes +import Data.Functor.Identity + +import Data.SBV + +import Language.Expression +import Language.Expression.Choice +import Language.Expression.Pretty +import Language.Expression.Util + +-- | Propositions over general expressions. +type Prop = HFree LogicOp + +-- | Propositions over expressions with the given list of operators. +type Prop' ops v = Prop (HFree' ops v) + +-------------------------------------------------------------------------------- +-- DSL +-------------------------------------------------------------------------------- + +infixl 3 *&& +infixl 2 *|| +infixr 1 *-> +infix 1 *<-> + +-- | Lift an expression into the land of propositions. +expr :: expr a -> Prop expr a +expr = HPure + +plit :: Bool -> Prop expr Bool +plit = HWrap . LogLit + +pnot :: Prop expr Bool -> Prop expr Bool +pnot = HWrap . LogNot + +(*&&) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool +(*&&) = HWrap ... LogAnd + +(*||) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool +(*||) = HWrap ... LogOr + +(*->) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool +(*->) = HWrap ... LogImpl + +(*<->) :: Prop expr Bool -> Prop expr Bool -> Prop expr Bool +(*<->) = HWrap ... LogEquiv + +propAnd :: [Prop expr Bool] -> Prop expr Bool +propAnd [] = plit True +propAnd (x : xs) = foldl' (*&&) x xs + +propOr :: [Prop expr Bool] -> Prop expr Bool +propOr [] = plit False +propOr (x : xs) = foldl' (*||) x xs + + +-------------------------------------------------------------------------------- +-- The HTraversable +-------------------------------------------------------------------------------- + +-- | Logical operations +data LogicOp t a where + LogLit :: Bool -> LogicOp t Bool + LogNot :: t Bool -> LogicOp t Bool + LogAnd :: t Bool -> t Bool -> LogicOp t Bool + LogOr :: t Bool -> t Bool -> LogicOp t Bool + LogImpl :: t Bool -> t Bool -> LogicOp t Bool + LogEquiv :: t Bool -> t Bool -> LogicOp t Bool + +instance HFunctor LogicOp +instance HTraversable LogicOp where + htraverse f = \case + LogLit b -> pure $ LogLit b + LogNot x -> LogNot <$> f x + LogAnd x y -> LogAnd <$> f x <*> f y + LogOr x y -> LogOr <$> f x <*> f y + LogImpl x y -> LogImpl <$> f x <*> f y + LogEquiv x y -> LogEquiv <$> f x <*> f y + +instance HFoldableAt Identity LogicOp where + hfoldMap = implHfoldMap $ \case + LogLit b -> pure b + LogNot x -> not <$> x + LogAnd x y -> liftA2 (&&) x y + LogOr x y -> liftA2 (||) x y + LogImpl x y -> liftA2 (==>) x y + LogEquiv x y -> liftA2 (<=>) x y + +instance HFoldableAt SBV LogicOp where + hfoldMap = implHfoldMap $ \case + LogLit b -> fromBool b + LogNot x -> bnot x + LogAnd x y -> x &&& y + LogOr x y -> x ||| y + LogImpl x y -> x ==> y + LogEquiv x y -> x <=> y + +-- instance HEq LogicOp where +-- liftHEq _ _ (LogLit x) (LogLit y) = x == y +-- liftHEq le _ (LogNot x) (LogNot y) = le svEq x y +-- liftHEq le _ (LogAnd x1 x2) (LogAnd y1 y2) = le svEq x1 y1 && le svEq x2 y2 +-- liftHEq le _ (LogOr x1 x2) (LogOr y1 y2) = le svEq x1 y1 && le svEq x2 y2 +-- liftHEq le _ (LogImpl x1 x2) (LogImpl y1 y2) = le svEq x1 y1 && le svEq x2 y2 +-- liftHEq le _ (LogEquiv x1 x2) (LogEquiv y1 y2) = le svEq x1 y1 && le svEq x2 y2 +-- liftHEq _ _ _ _ = False + +-- instance (Eq1 t) => Eq1 (LogicOp t) where liftEq = liftLiftEq + +-- instance (Eq a, Eq1 t) => Eq (LogicOp t a) where (==) = eq1 + +instance Pretty2 LogicOp where + prettys2Prec p = \case + LogLit True -> \r -> "T" ++ r + LogLit False -> \r -> "F" ++ r + LogNot x -> showParen (p > 8) $ showString "¬ " . prettys1Prec 9 x + LogAnd x y -> + showParen (p > 3) $ prettys1Prec 4 x . showString " ∧ " . prettys1Prec 4 y + LogOr x y -> + showParen (p > 2) $ prettys1Prec 3 x . showString " ∨ " . prettys1Prec 3 y + LogImpl x y -> + showParen (p > 1) $ prettys1Prec 2 x . showString " -> " . prettys1Prec 2 y + LogEquiv x y -> + showParen (p > 0) $ prettys1Prec 1 x . showString " <-> " . prettys1Prec 1 y + +-------------------------------------------------------------------------------- +-- Internal Combinators +-------------------------------------------------------------------------------- + +-- svEq :: (Typeable a, Typeable b, Eq a) => a -> b -> Bool +-- svEq (x :: a) (y :: b) +-- | Just Refl <- eqT :: Maybe (a :~: b) = x == y +-- | otherwise = False diff --git a/Language/Expression/Scope.hs b/Language/Expression/Scope.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Scope.hs @@ -0,0 +1,190 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +module Language.Expression.Scope where + +import Control.Lens + +import Language.Expression + +-------------------------------------------------------------------------------- +-- Classes +-------------------------------------------------------------------------------- + +class HBound k where + (^>>>=) :: (HMonad h) => k h t a -> (forall b. t b -> h t' b) -> k h t' a + +-------------------------------------------------------------------------------- +-- Bound or free variables +-------------------------------------------------------------------------------- + +data BV g f a where + -- | Bound variable + B :: g a -> BV g f a + -- | Free variable + F :: f a -> BV g f a + +instance HFunctor (BV g) where + hmap = hliftM + +instance HPointed (BV g) where + hpure = F + +instance HBind (BV g) where + B x ^>>= _ = B x + F x ^>>= f = f x + +instance HMonad (BV g) + +-- instance (HFoldableAt k g) => HFoldableAt k (BV g) where +-- hfoldMap = hbifoldMap . hfoldMap + +instance HTraversable (BV g) where + htraverse = hbitraverseBV pure + +foldBV :: (w a -> r) -> (v a -> r) -> BV w v a -> r +foldBV f g = \case + B x -> f x + F y -> g y + +instance HBifunctor BV where + hbimap = hbimapBV + +instance HBitraversable BV where + hbitraverse = hbitraverseBV + +hbitraverseBV :: (Functor t) => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b) +hbitraverseBV f g = foldBV (fmap B . f) (fmap F . g) + +hbimapBV :: (g a -> g' b) -> (f a -> f' b) -> BV g f a -> BV g' f' b +hbimapBV f g = foldBV (B . f) (F . g) + +instance HBifoldableAt k BV where + hbifoldMap = foldBV + +-------------------------------------------------------------------------------- +-- Scopes +-------------------------------------------------------------------------------- + +newtype Scope g h f a = Scope { unscope :: h (BV g (h f)) a } + +_Scope :: Iso (Scope g h f a) (Scope g' h' f' a') (h (BV g (h f)) a) (h' (BV g' (h' f')) a') +_Scope = iso unscope Scope + +instance HFunctor h => HFunctor (Scope g h) where + hmap f = from _Scoped %~ hfirst f + +instance HPointed h => HPointed (Scope g h) where + hpure = Scope . hpure . hpure . hpure + +instance HTraversable h => HTraversable (Scope g h) where + htraverse f = _Scope %%~ htraverse (htraverse (htraverse f)) + + +instance HDuofunctor (Scope g) where + hduomap g f = _Scope %~ g (hmap (g f)) + +instance HDuotraversable (Scope g) where + hduotraverse g f = _Scope %%~ g (htraverse (g f)) + + +instance HBound (Scope g) where + Scope x ^>>>= f = Scope (x ^>>= foldBV (hpure . B) (hmap (F . f))) + + +hbitraverseScope + :: (Applicative t, HTraversable h) + => (forall b. g b -> t (g' b)) + -> (forall b. f b -> t (f' b)) + -> Scope g h f a + -> t (Scope g' h f' a) +hbitraverseScope g f = from _Scoped %%~ hbitraverse f g + + +freeVar :: (HPointed h) => f a -> Scope g h f a +freeVar = Scope . hpure . hpure . hpure + + +boundVar :: (HPointed h) => g a -> Scope g h f a +boundVar = Scope . hpure . B + + +liftScope :: (HFunctor h, HPointed h) => h f a -> Scope g h f a +liftScope = Scope . hmap (hpure . hpure) + + +abstractTraverse :: (HMonad h, HTraversable h, Applicative t) => (forall b. f b -> t (Maybe (g b))) -> h f a -> t (Scope g h f a) +abstractTraverse f = fmap Scope . htraverse (\y -> maybe ((hpure . hpure) y) B <$> f y) + + +abstract :: (HMonad h) => (forall b. f b -> Maybe (g b)) -> h f a -> Scope g h f a +abstract f = Scope . hmap (\y -> maybe ((hpure . hpure) y) B $ f y) + + +-- instantiate :: (Substitutive op, Applicative f) => (forall b. w b -> f (op v b)) -> Scope g h f a -> f (op v a) +-- instantiate f (Scope x) = bindVars (foldBV f pure) x + +-- | Sometimes it's convenient to move around the type arguments to 'Scope'. +newtype Scoped h f g a = Scoped { unscoped :: Scope g h f a } + +_Scoped :: Iso (Scoped h f g a) (Scoped h' f' g' a') (Scope g h f a) (Scope g' h' f' a') +_Scoped = iso unscoped Scoped + +instance HFunctor h => HFunctor (Scoped h f) where + hmap = hsecond + +instance HFunctor h => HBifunctor (Scoped h) where + hbimap f g = _Scoped . _Scope %~ hmap (hbimap g (hmap f)) + +instance HTraversable h => HBitraversable (Scoped h) where + hbitraverse f g = _Scoped . _Scope %%~ htraverse (hbitraverse g (htraverse f)) + +instance HTraversable h => HTraversable (Scoped h f) where + htraverse = hbitraverse pure + +-------------------------------------------------------------------------------- +-- Scoped Free Monads +-------------------------------------------------------------------------------- + +data SFree h f a + = SPure (f a) + | SWrap (h (Scoped (SFree h) f) (SFree h f) a) + +instance HDuofunctor h => HFunctor (SFree h) where + hmap = hliftM + +instance HPointed (SFree h) where + hpure = SPure + +instance HDuofunctor h => HBind (SFree h) where + SPure x ^>>= f = f x + SWrap x ^>>= f = SWrap (hduomap (\g -> (\(Scoped y) -> Scoped (y ^>>>= f)) . hmap g) (^>>= f) x) + +instance HDuofunctor h => HMonad (SFree h) + +instance (HDuotraversable h) => HTraversable (SFree h) where + htraverse f = \case + SPure x -> SPure <$> f x + SWrap x -> SWrap <$> hduotraverse (hbitraverse f) (htraverse f) x + + +instance HDuofoldableAt k (Scope k) where + hduofoldMap f g = f (hbifoldMap id (f g)) . view _Scope + +instance (HFunctor h, HFoldableAt k h) => HBifoldableAt k (Scoped h) where + hbifoldMap f g = hfoldMap (hbifoldMap g (hfoldMap f)) . view (_Scoped . _Scope) + +instance (HDuotraversable h, HDuofoldableAt k h) => HFoldableAt k (SFree h) where + hfoldMap f = \case + SPure x -> f x + SWrap x -> + hduofoldMap + (\g -> hduofoldMap hfoldMap f . view _Scoped . hsecond g) + (hfoldMap f) + x diff --git a/Language/Expression/Util.hs b/Language/Expression/Util.hs new file mode 100644 --- /dev/null +++ b/Language/Expression/Util.hs @@ -0,0 +1,4 @@ +module Language.Expression.Util where + +(...) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d) +(f ... g) x y = f (g x y) diff --git a/Language/Verification.hs b/Language/Verification.hs new file mode 100644 --- /dev/null +++ b/Language/Verification.hs @@ -0,0 +1,44 @@ +{-| + +Strongly-typed utilities to aid in automatic verification (e.g. of programs) +using an SMT solver. + +This is mainly just a wrapper around "Data.SBV" that allows for inspection and +manipulation of symbolic values, especially variable substitution. + +-} +module Language.Verification + ( + -- * The verification monad + Verifier + , runVerifier + , runVerifierWith + , VerifierError(..) + + -- * The query monad + , Query + , query + + -- * Verifiable variables + , VerifiableVar(..) + + -- * Verifier actions + , evalProp + , evalProp' + , evalPropSimple + + -- * Miscellaneous combinators + , subVar + + -- * Expressions + , module Expression + + -- * SBV re-exports + , SMTConfig(..) + , defaultSMTCfg + ) where + +import Data.SBV (SMTConfig (..), defaultSMTCfg) + +import Language.Expression as Expression +import Language.Verification.Core diff --git a/Language/Verification/Conditions.hs b/Language/Verification/Conditions.hs new file mode 100644 --- /dev/null +++ b/Language/Verification/Conditions.hs @@ -0,0 +1,254 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} + +{- | + +Combinators for generating verification conditions for programs. + +-} +module Language.Verification.Conditions + ( + -- * Types + Assignment(..) + , AnnSeq(..) + , Triplet + + -- * Generating Verification Conditions + , skipVCs + , assignVCs + , sequenceVCs + , ifVCs + , multiIfVCs + , whileVCs + + -- * Combinators + , subAssignment + , chainSub + , joinAnnSeq + , JoinAnnSeq(..) + , joiningAnnSeq + , emptyAnnSeq + , propAnnSeq + , cmdAnnSeq + + -- * Propositions + , module Language.Expression.Prop + ) where + +import Data.List (intersperse) +import Data.Semigroup (Semigroup(..)) +import Data.Monoid (Endo (..)) + +import Control.Monad.Writer (MonadWriter (tell)) + +import Language.Expression.Pretty +import Language.Expression.Prop +import Language.Verification + +-------------------------------------------------------------------------------- +-- Exposed Types +-------------------------------------------------------------------------------- + +-- | An assignment of a particular expression to a particular variable. +data Assignment expr var where + Assignment :: var a -> expr var a -> Assignment expr var + +instance (Pretty1 var, Pretty2 expr) => Pretty (Assignment expr var) where + prettysPrec p (Assignment v e) = showParen (p > 9) $ + prettys1Prec 10 v . showString " := " . prettys2Prec 10 e + +-- | An annotated sequence. Consists of runs of assignments, with other commands +-- separated by annotations. +data AnnSeq expr var cmd + = JustAssign [Assignment expr var] + -- ^ Just a series of assignments without annotations + | CmdAssign cmd [Assignment expr var] + -- ^ A command followed by a series of assignments + | Annotation (AnnSeq expr var cmd) (Prop (expr var) Bool) (AnnSeq expr var cmd) + -- ^ An initial sequence, followed by an annotation, then another sequence + deriving (Functor, Foldable, Traversable) + +instance (Pretty2 expr, Pretty1 var, Pretty cmd) => Pretty (AnnSeq expr var cmd) where + prettysPrec _ (JustAssign as) + = appEndo . mconcat + . intersperse (Endo (showString "; ")) + . map (Endo . prettysPrec 10) + $ as + + prettysPrec _ (CmdAssign cmd as) + = appEndo . mconcat + . intersperse (Endo (showString "; ")) + . (Endo (prettysPrec 10 cmd) :) + . map (Endo . prettysPrec 10) + $ as + + prettysPrec _ (Annotation l p r) + = prettysPrec 10 l + . showString "; {" + . prettysPrec 10 p + . showString "}" + . prettysPrec 10 r + +-------------------------------------------------------------------------------- +-- Combinators +-------------------------------------------------------------------------------- + +-- | Substitutes variables in the given proposition based on the given +-- assignment. +subAssignment + :: (HMonad expr, VerifiableVar v) + => Assignment expr v -> Prop (expr v) a -> Prop (expr v) a +subAssignment (Assignment targetVar newExpr) = hmap (^>>= subVar newExpr targetVar) + + +-- | Chains substitutions, substituting using each assignment in the given list +-- in turn. +chainSub + :: (HMonad expr, VerifiableVar v) + => Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool +chainSub prop [] = prop +chainSub prop (a : as) = subAssignment a (chainSub prop as) + + +-- | Joins two annotations together without a Hoare annotation in between. Fails +-- if this would place two non-assignment commands after each other, because +-- these need an annotation. +joinAnnSeq :: AnnSeq expr var cmd -> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd) +joinAnnSeq (JustAssign xs) (JustAssign ys) = return $ JustAssign (xs ++ ys) +joinAnnSeq (CmdAssign cmd xs) (JustAssign ys) = return $ CmdAssign cmd (xs ++ ys) +joinAnnSeq s (JustAssign []) = return s +joinAnnSeq (JustAssign []) s = return s +joinAnnSeq (Annotation l p r) r' = Annotation l p <$> joinAnnSeq r r' +joinAnnSeq l' (Annotation l p r) = (\l'' -> Annotation l'' p r) <$> joinAnnSeq l' l +joinAnnSeq _ _ = Nothing + + +emptyAnnSeq :: AnnSeq expr var cmd +emptyAnnSeq = JustAssign [] + +propAnnSeq :: Prop (expr var) Bool -> AnnSeq expr var cmd +propAnnSeq p = Annotation emptyAnnSeq p emptyAnnSeq + +cmdAnnSeq :: cmd -> AnnSeq expr var cmd +cmdAnnSeq c = CmdAssign c [] + + +-- | 'JoinAnnSeq' forms a 'Monoid' out of 'AnnSeq' by propagating failure to +-- join arising from 'joinAnnSeq'. +newtype JoinAnnSeq expr var cmd = JoinAnnSeq { tryJoinAnnSeq :: Maybe (AnnSeq expr var cmd) } + +joiningAnnSeq :: AnnSeq expr var cmd -> JoinAnnSeq expr var cmd +joiningAnnSeq = JoinAnnSeq . Just + +instance Semigroup (JoinAnnSeq expr var cmd) where + JoinAnnSeq (Just x) <> JoinAnnSeq (Just y) = JoinAnnSeq (x `joinAnnSeq` y) + _ <> _ = JoinAnnSeq Nothing + +instance Monoid (JoinAnnSeq expr var cmd) where + mempty = JoinAnnSeq (Just emptyAnnSeq) + mappend = (<>) + +-------------------------------------------------------------------------------- +-- Generating verification conditions +-------------------------------------------------------------------------------- + +type MonadGenVCs expr var = MonadWriter [Prop (expr var) Bool] + +type Triplet expr var a = (Prop (expr var) Bool, Prop (expr var) Bool, a) + +-- | Generates verification conditions for a skip statement. +skipVCs + :: (HMonad expr, MonadGenVCs expr var m) + => Triplet expr var () -> m () +skipVCs (precond, postcond, ()) = tell [precond *-> postcond] + + +-- | Generates verification conditions for an assignment. +assignVCs + :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v) + => Triplet expr v (Assignment expr v) -> m () +assignVCs (precond, postcond, assignment) = do + let postcond' = subAssignment assignment postcond + tell [precond *-> postcond'] + + +-- | Generates verification conditions for a sequence of commands. +sequenceVCs + :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v) + => (Triplet expr v cmd -> m a) + -> Triplet expr v (AnnSeq expr v cmd) -> m [a] +sequenceVCs cmdVCs (precond, postcond, annSeq) = + case annSeq of + -- A sequence of assignments can be verified by checking the precondition + -- implies the postcondition, after substitutions are performed by the + -- assignments. + JustAssign as -> do + tell [precond *-> chainSub postcond as] + return [] + + -- A command followed by a sequence of assignments can be verified by + -- substituting based on the assignments in the postcondition, then verifying + -- the command with the new postcondition and original precondition. + CmdAssign cmd as -> + let postcond' = chainSub postcond as + in (: []) <$> cmdVCs (precond, postcond', cmd) + + -- To verify @{P} C_1 ; {R} C_2 {Q}@, verify @{P} C_1 {R}@ and @{R} C_2 {Q}@. + Annotation l midcond r -> do + (++) <$> sequenceVCs cmdVCs (precond, midcond, l) + <*> sequenceVCs cmdVCs (midcond, postcond, r) + + +-- | Generates verification conditions for a two-branch if command. +ifVCs + :: (HMonad expr, MonadGenVCs expr v m) + => (Triplet expr v cmd -> m a) + -> (cond -> Prop (expr v) Bool) + -> Triplet expr v (cond, cmd, cmd) -> m (a, a) +ifVCs cmdVCs condToProp (precond, postcond, (cond, cmd1, cmd2)) = do + let condProp = condToProp cond + return (,) <*> cmdVCs ((precond *&& condProp), postcond, cmd1) + <*> cmdVCs ((precond *&& pnot condProp), postcond, cmd2) + + +-- | Generates verification conditions for a multi-branch if-then-else-... +-- command. +multiIfVCs + :: (HMonad expr, Monad m) + => (Triplet expr v cmd -> m ()) + -> (cond -> Prop (expr v) Bool) + -> Triplet expr v [(Maybe cond, cmd)] -> m () +multiIfVCs cmdVCs condToProp (precond, postcond, branches) = go precond branches + where + go precond' ((branchCond, branchCmd) : rest) = + case branchCond of + Just bc -> do + let bc' = condToProp bc + cmdVCs ((precond' *&& bc'), postcond, branchCmd) + go (precond' *&& pnot bc') rest + Nothing -> do + cmdVCs (precond', postcond, branchCmd) + go _ [] = return () + + +-- | Generates verification conditions for a while loop. +whileVCs + :: (HMonad expr, MonadGenVCs expr v m) + => (Triplet expr v cmd -> m ()) + -> (cond -> Prop (expr v) Bool) + -> Prop (expr v) Bool -- ^ Loop invariant + -> Triplet expr v (cond, cmd) -> m () +whileVCs cmdVCs condToProp invariant (precond, postcond, (cond, body)) = do + let condProp = condToProp cond + -- Assert that the invariant is maintained over the loop body + cmdVCs ((invariant *&& condProp), invariant, body) + -- Assert that the invariant is implied by precondition, and at the end of the + -- loop the invariant implies the postcondition + tell [precond *-> invariant, (invariant *&& pnot condProp) *-> postcond] diff --git a/Language/Verification/Core.hs b/Language/Verification/Core.hs new file mode 100644 --- /dev/null +++ b/Language/Verification/Core.hs @@ -0,0 +1,223 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +module Language.Verification.Core where + +import Control.Exception +import Data.Typeable ((:~:) (..), Typeable) +import Data.Functor.Compose + +import Control.Lens hiding ((.>)) +import Control.Monad.Except +import Control.Monad.Reader +import Control.Monad.State + +import Data.Map (Map) +import Data.SBV hiding (OrdSymbolic (..), ( # )) + +import Language.Expression +import Language.Expression.Prop (LogicOp, Prop) + +-------------------------------------------------------------------------------- +-- Variables +-------------------------------------------------------------------------------- + +class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where + type VarKey v + type VarSym v :: * -> * + type VarEnv v :: * + + symForVar :: v a -> VarEnv v -> Symbolic (VarSym v a) + varKey :: v a -> VarKey v + + eqVarTypes :: v a -> v b -> Maybe (a :~: b) + + castVarSym :: v a -> VarSym v b -> Maybe (VarSym v a) + +-------------------------------------------------------------------------------- +-- Verifier Monad +-------------------------------------------------------------------------------- + +data VerifierError v + = VEMismatchedSymbolType (VarKey v) + -- ^ The same variable was used for two different symbol types + | VESbvException String String + -- ^ When running a query, SBV threw an exception + +deriving instance Show (VarKey v) => Show (VerifierError v) +deriving instance Typeable (VarKey v) => Typeable (VerifierError v) + +instance (Typeable v, l ~ VarKey v, Show l, Typeable l) => + Exception (VerifierError v) where + + displayException = \case + VEMismatchedSymbolType l -> + "variable " ++ show l ++ " was used at two different types" + + VESbvException message (_ {- location -}) -> + "exception from SBV:\n" ++ message + +newtype Verifier v a = + Verifier + { getVerifier :: ReaderT SMTConfig (ExceptT (VerifierError v) IO) a + } + deriving ( Functor + , Applicative + , Monad + , MonadIO + , MonadReader SMTConfig + , MonadError (VerifierError v) + ) + +runVerifierWith + :: (VerifiableVar v) + => SMTConfig + -> Verifier v a + -> IO (Either (VerifierError v) a) +runVerifierWith config (Verifier action) = runExceptT (runReaderT action config) + +runVerifier + :: VerifiableVar v + => Verifier v a -> IO (Either (VerifierError v) a) +runVerifier = runVerifierWith defaultSMTCfg + +-------------------------------------------------------------------------------- +-- Query Monad +-------------------------------------------------------------------------------- + +data SomeSym v where + SomeSym :: VarSym v a -> SomeSym v + +type QueryState v = Map (VarKey v) (SomeSym v) + +newtype Query v a = + Query + { getQuery :: ReaderT (VarEnv v) ( + StateT (QueryState v) Symbolic) a + } + deriving ( Functor + , Applicative + , Monad + , MonadIO + ) + +query :: (VerifiableVar v) => Query v SBool -> VarEnv v -> Verifier v Bool +query (Query action) env = do + cfg <- ask + let predicate = evalStateT (runReaderT action env) mempty + smtResult = + (Right <$> isTheoremWith cfg predicate) `catches` + [ Handler (\ex -> return (Left ex)) + , Handler (\(ErrorCallWithLocation message location) -> + return (Left (VESbvException message location))) + ] + + liftIO smtResult >>= either throwError return + +-------------------------------------------------------------------------------- +-- Query actions +-------------------------------------------------------------------------------- + +evalProp + :: ( HMonad expr + , HTraversable expr + , VerifiableVar v + , Exception (VerifierError v) + , HFoldableAt k expr + , HFoldableAt k LogicOp + , Monad m + ) + => (forall a. Query v a -> m a) + -> (forall a. VarSym v a -> m (k a)) + -> Prop (expr v) b + -> m (k b) +evalProp liftQuery liftVar = hfoldTraverse (hfoldTraverse (liftVar <=< liftQuery . symbolVar)) + +evalProp' + :: ( HMonad expr + , HTraversable expr + , VerifiableVar v + , Exception (VerifierError v) + , HFoldableAt (Compose m k) expr + , HFoldableAt (Compose m k) LogicOp + , Monad m + ) + => (forall a. Query v a -> m a) + -> (forall a. VarSym v a -> m (k a)) + -> Prop (expr v) b + -> m (k b) +evalProp' liftQuery liftVar = hfoldMapA (hfoldMapA (liftVar <=< liftQuery . symbolVar)) + +evalPropSimple + :: ( HMonad expr + , HTraversable expr + , VerifiableVar v + , Exception (VerifierError v) + , HFoldableAt SBV expr + , VarSym v ~ SBV + ) + => Prop (expr v) b + -> Query v (SBV b) +evalPropSimple = evalProp id pure + +-------------------------------------------------------------------------------- +-- Combinators +-------------------------------------------------------------------------------- + +-- | If the two variables match in both type and name, return the given +-- expression. Otherwise, return an expression just containing this variable. +-- +-- This is substitution into an expression, where the old expression is just a +-- variable. +subVar + :: (HPointed expr, VerifiableVar v, Eq (VarKey v)) + => expr v a + -> v a + -> v b + -> expr v b +subVar newExpr targetVar thisVar = + let targetName = varKey targetVar + thisName = varKey thisVar + in case eqVarTypes thisVar targetVar of + Just Refl | thisName == targetName -> newExpr + _ -> hpure thisVar + +-------------------------------------------------------------------------------- +-- Internal Functions +-------------------------------------------------------------------------------- + +liftSymbolic :: Symbolic a -> Query v a +liftSymbolic = Query . lift . lift + +throwQuery :: (Exception (VerifierError v)) => VerifierError v -> Query v a +throwQuery = liftIO . throwIO + +symbolVar :: (VerifiableVar v, Exception (VerifierError v)) => v a -> Query v (VarSym v a) +symbolVar theVar = do + let varLoc = varKey theVar + storedSymbol <- Query $ use (at varLoc) + + case storedSymbol of + Just (SomeSym x) -> case castVarSym theVar x of + Just y -> return y + Nothing -> throwQuery (VEMismatchedSymbolType varLoc) + Nothing -> do + newSymbol <- liftSymbolic . symForVar theVar =<< Query ask + Query $ at varLoc .= Just (SomeSym newSymbol) + return newSymbol diff --git a/Language/While/Hoare.hs b/Language/While/Hoare.hs new file mode 100644 --- /dev/null +++ b/Language/While/Hoare.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeFamilies #-} + +module Language.While.Hoare where + +import Control.Monad.Writer + +import Language.While.Syntax + +import Language.Expression.Prop +import Language.Expression.Pretty +import Language.Verification +import Language.Verification.Conditions + +type WhileProp l = Prop (WhileExpr l) + +data PropAnn l a = PropAnn (WhileProp l Bool) a + +type AnnCommand l a = Command l (PropAnn l a) + +instance (Pretty l, Pretty a) => Pretty (PropAnn l a) where + prettysPrec _ (PropAnn prop ann) = prettysPrec 10 prop . showString " , " . prettysPrec 10 ann + +type MonadGen l = WriterT [WhileProp l Bool] Maybe + +-------------------------------------------------------------------------------- +-- Exposed Functions +-------------------------------------------------------------------------------- + +-- | Generate verification conditions to prove that the given Hoare partial +-- correctness triple holds. +generateVCs + :: (VerifiableVar (WhileVar l)) + => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a + -> Maybe [WhileProp l Bool] +generateVCs precond postcond cmd = + execWriterT $ generateVCs' (precond, postcond, cmd) + + +generateVCs' + :: (VerifiableVar (WhileVar l)) + => Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a) -> MonadGen l () +generateVCs' (precond, postcond, cmd) = case cmd of + CAnn (PropAnn prop _) command -> + generateVCs' ((prop *&& precond), postcond, command) + + c@(CSeq _ _) -> do + s <- lift (splitSeq c) + void $ sequenceVCs generateVCs' (precond, postcond, s) + + CSkip -> skipVCs (precond, postcond, ()) + + CAssign loc e -> + assignVCs (precond, postcond, (Assignment (WhileVar loc) e)) + + CIf cond c1 c2 -> + void $ ifVCs generateVCs' expr (precond, postcond, (cond, c1, c2)) + + CWhile cond (CAnn (PropAnn invariant _) body) -> + whileVCs generateVCs' + expr + invariant + (precond, postcond, (cond, body)) + + -- If this falls through, the command is not sufficiently annotated + _ -> mzero + +-------------------------------------------------------------------------------- +-- Internal +-------------------------------------------------------------------------------- + +-- | Split the command into all the top-level sequenced commands, interspersed +-- with annotations. Returns 'Nothing' if the command's sequences are not +-- sufficiently annotated. +splitSeq :: AnnCommand l a -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)) +splitSeq = \case + CSeq c1 (CAnn (PropAnn midcond _) c2) -> + do a1 <- splitSeq c1 + a2 <- splitSeq c2 + return $ Annotation a1 midcond a2 + CSeq c1 (CAssign loc e) -> + do a1 <- splitSeq c1 + a1 `joinAnnSeq` JustAssign [Assignment (WhileVar loc) e] + CSeq c1 c2 -> + do a1 <- splitSeq c1 + a2 <- splitSeq c2 + a1 `joinAnnSeq` a2 + CAssign loc e -> return $ JustAssign [Assignment (WhileVar loc) e] + c -> return $ CmdAssign c [] diff --git a/Language/While/Hoare/Prover.hs b/Language/While/Hoare/Prover.hs new file mode 100644 --- /dev/null +++ b/Language/While/Hoare/Prover.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeFamilies #-} + +module Language.While.Hoare.Prover where + +import Data.SBV (SBV) + +import Language.Expression.Prop +import Language.Verification + +import Language.While.Hoare +import Language.While.Syntax + + +checkPartialHoare + :: (VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV) + => WhileProp l Bool + -> WhileProp l Bool + -> AnnCommand l a + -> Query (WhileVar l) (SBV Bool) +checkPartialHoare precond postcond cmd = + do vcs <- case generateVCs precond postcond cmd of + Just x -> return x + Nothing -> fail "Command not sufficiently annotated" + + let bigVC = foldr (*&&) (plit True) vcs + + evalPropSimple bigVC + +provePartialHoare + :: (VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV, VarEnv (WhileVar l) ~ ()) + => WhileProp l Bool + -> WhileProp l Bool + -> AnnCommand l a + -> IO (Either (VerifierError (WhileVar l)) Bool) +provePartialHoare precond postcond cmd = + runVerifier . flip query () $ checkPartialHoare precond postcond cmd diff --git a/Language/While/Syntax.hs b/Language/While/Syntax.hs new file mode 100644 --- /dev/null +++ b/Language/While/Syntax.hs @@ -0,0 +1,285 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} + + +module Language.While.Syntax where + +import Data.String (IsString (..)) +import Data.Typeable ((:~:) (..)) + +import Data.SBV +import Data.SBV.Internals (SBV (..)) +import Data.Vinyl (Rec (RNil)) +import Data.Vinyl.Curry + +import Control.Lens hiding ((...), (.>)) +import Control.Monad.State +import Data.Map (Map) +import qualified Data.Map as Map + +import Language.Expression +import Language.Expression.GeneralOp +import Language.Expression.Pretty +import Language.Expression.Util +import Language.Verification + +-------------------------------------------------------------------------------- +-- Operator kind +-------------------------------------------------------------------------------- + +data WhileOpKind as r where + OpLit :: AlgReal -> WhileOpKind '[] AlgReal + OpAdd, OpSub, OpMul :: WhileOpKind '[AlgReal, AlgReal] AlgReal + OpEq, OpLT, OpLE, OpGT, OpGE :: WhileOpKind '[AlgReal, AlgReal] Bool + OpAnd, OpOr :: WhileOpKind '[Bool , Bool] Bool + OpNot :: WhileOpKind '[Bool] Bool + + +instance EvalOpAt Identity WhileOpKind where + + evalMany = \case + OpLit x -> \_ -> pure x + + OpAdd -> runcurryA' (+) + OpSub -> runcurryA' (-) + OpMul -> runcurryA' (*) + + OpEq -> runcurryA' (==) + OpLT -> runcurryA' (<) + OpLE -> runcurryA' (<=) + OpGT -> runcurryA' (>) + OpGE -> runcurryA' (>=) + + OpAnd -> runcurryA' (&&) + OpOr -> runcurryA' (||) + + OpNot -> runcurryA' not + +instance EvalOpAt SBV WhileOpKind where + evalMany = \case + OpLit x -> \_ -> literal x + + OpAdd -> runcurry (+) + OpSub -> runcurry (-) + OpMul -> runcurry (*) + + OpEq -> runcurry (.==) + OpLT -> runcurry (.<) + OpLE -> runcurry (.<=) + OpGT -> runcurry (.>) + OpGE -> runcurry (.>=) + + OpAnd -> runcurry (&&&) + OpOr -> runcurry (|||) + + OpNot -> runcurry bnot + +-- instance EqOpMany WhileOpKind where +-- liftEqMany (OpLit x) (OpLit y) _ = \_ _ -> x == y +-- liftEqMany OpAdd OpAdd k = k +-- liftEqMany OpSub OpSub k = k +-- liftEqMany OpMul OpMul k = k +-- liftEqMany OpEq OpEq k = k +-- liftEqMany OpLT OpLT k = k +-- liftEqMany OpLE OpLE k = k +-- liftEqMany OpGT OpGT k = k +-- liftEqMany OpGE OpGE k = k +-- liftEqMany OpAnd OpAnd k = k +-- liftEqMany OpOr OpOr k = k +-- liftEqMany OpNot OpNot k = k +-- liftEqMany _ _ _ = \_ _ -> False + +prettys1Binop :: + (Pretty1 t) => + Int -> String -> (Int -> t a -> t b -> ShowS) +prettys1Binop prec opStr = \p x y -> + showParen (p > prec) $ prettys1Prec (prec + 1) x + . showString opStr + . prettys1Prec (prec + 1) y + +instance PrettyOp WhileOpKind where + prettysPrecOp = flip $ \case + OpAdd -> runcurry . prettys1Binop 5 " + " + OpSub -> runcurry . prettys1Binop 5 " - " + OpMul -> runcurry . prettys1Binop 6 " * " + + OpEq -> runcurry . prettys1Binop 4 " = " + + OpLT -> runcurry . prettys1Binop 4 " < " + OpLE -> runcurry . prettys1Binop 4 " <= " + OpGT -> runcurry . prettys1Binop 4 " > " + OpGE -> runcurry . prettys1Binop 4 " >= " + + OpNot -> + \p -> + runcurry $ \x -> showParen (p > 8) $ showString "! " . prettys1Prec 9 x + OpAnd -> runcurry . prettys1Binop 3 " && " + OpOr -> runcurry . prettys1Binop 2 " || " + + OpLit x -> \_ _ -> shows x + +-------------------------------------------------------------------------------- +-- Operators +-------------------------------------------------------------------------------- + +type WhileOp = GeneralOp WhileOpKind + +-------------------------------------------------------------------------------- +-- Variables +-------------------------------------------------------------------------------- + +data WhileVar l a where + WhileVar :: l -> WhileVar l AlgReal + +instance Pretty l => Pretty1 (WhileVar l) where + pretty1 (WhileVar l) = pretty l + +instance VerifiableVar (WhileVar String) where + type VarKey (WhileVar String) = String + type VarSym (WhileVar String) = SBV + type VarEnv (WhileVar String) = () + + symForVar (WhileVar x) = const $ symbolic x + varKey (WhileVar x) = x + eqVarTypes (WhileVar _) (WhileVar _) = Just Refl + castVarSym (WhileVar _) (SBV x) = Just (SBV x) + +-------------------------------------------------------------------------------- +-- Expressions +-------------------------------------------------------------------------------- + +type WhileExpr l = HFree WhileOp (WhileVar l) + +instance Num (WhileExpr l AlgReal) where + fromInteger x = HWrap (Op (OpLit (fromInteger x)) RNil) + + (+) = HWrap ... rcurry (Op OpAdd) + (*) = HWrap ... rcurry (Op OpMul) + (-) = HWrap ... rcurry (Op OpSub) + abs = error "can't take abs of expressions" + signum = error "can't take signum of expressions" + +instance IsString s => IsString (WhileExpr s AlgReal) where + fromString = HPure . WhileVar . fromString + +-------------------------------------------------------------------------------- +-- Commands +-------------------------------------------------------------------------------- + +data Command l a + = CAnn a (Command l a) + | CSeq (Command l a) (Command l a) + | CSkip + | CAssign l (WhileExpr l AlgReal) + | CIf (WhileExpr l Bool) (Command l a) (Command l a) + | CWhile (WhileExpr l Bool) (Command l a) + +instance (Pretty l, Pretty a) => Pretty (Command l a) where + prettysPrec p = \case + CAnn ann c -> + showParen (p > 10) $ showString "{ " + . prettys ann + . showString " }\n" + . prettys c + CSeq c1 c2 -> + showParen (p > 10) $ prettys c1 . showString ";\n" . prettys c2 + CSkip -> showString "()" + CAssign v e -> + showParen (p > 10) $ prettys v . showString " := " . prettys e + CIf cond c1 c2 -> + showParen (p > 10) $ showString "if " + . prettysPrec 11 cond + . showString " then\n" + . prettysPrec 11 c1 + . showString "\nelse\n" + . prettysPrec 11 c2 + CWhile cond body -> + showParen (p > 10) $ showString "while " + . prettysPrec 11 cond + . showString " do\n" + . prettysPrec 11 body + +-------------------------------------------------------------------------------- +-- Running Commands +-------------------------------------------------------------------------------- + +data StepResult a + = Terminated + | Failed + | Progress a + deriving (Functor) + +evalWhileExpr + :: (Applicative f) + => (forall x. WhileVar l x -> f x) + -> WhileExpr l a -> f a +evalWhileExpr f + = fmap runIdentity + . hfoldTraverse (fmap Identity . f) + +oneStep + :: (Ord l) + => Command l a + -> State (Map l AlgReal) (StepResult (Command l a)) +oneStep = \case + CAnn ann c -> fmap (CAnn ann) <$> oneStep c + + CSeq c1 c2 -> + do s <- oneStep c1 + case s of + Terminated -> return (Progress c2) + Failed -> return Failed + Progress c1' -> return (Progress (c1' `CSeq` c2)) + + CSkip -> return Terminated + + CAssign loc expr -> + do env <- get + if Map.member loc env then + case evalWhileExpr (lookupVar env) expr of + Just val -> + do at loc .= Just val + return Terminated + Nothing -> return Failed + -- Can't assign a memory location that doesn't exist + else return Failed + + CIf cond c1 c2 -> + do env <- get + case evalWhileExpr (lookupVar env) cond of + Just True -> return (Progress c1) + Just False -> return (Progress c2) + _ -> return Failed + + CWhile cond body -> + do env <- get + case evalWhileExpr (lookupVar env) cond of + Just True -> return (Progress (body `CSeq` (CWhile cond body))) + Just False -> return Terminated + _ -> return Failed + + +runCommand :: (Ord l) => Command l a -> State (Map l AlgReal) Bool +runCommand command = + do s <- oneStep command + case s of + Terminated -> return True + Failed -> return False + Progress command' -> runCommand command' + +-------------------------------------------------------------------------------- +-- Combinators +-------------------------------------------------------------------------------- + +lookupVar :: (Ord l) => Map l AlgReal -> WhileVar l a -> Maybe a +lookupVar env (WhileVar s) = Map.lookup s env diff --git a/Language/While/Syntax/Sugar.hs b/Language/While/Syntax/Sugar.hs new file mode 100644 --- /dev/null +++ b/Language/While/Syntax/Sugar.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Language.While.Syntax.Sugar where + +import Data.SBV (AlgReal) + +import Data.Vinyl.Curry + +import Language.Expression +import Language.Expression.GeneralOp +import Language.Expression.Util +import Language.While.Hoare +import Language.While.Syntax + +infix 1 .=. +infixr 0 \\ +infix 3 ^^^ +infix 8 .< +infix 8 .<= +infix 8 .> +infix 8 .>= +infixr 7 .&& +infixr 6 .|| + +(.=.) :: l -> WhileExpr l AlgReal -> Command l a +(.=.) = CAssign + +(\\) :: Command l a -> Command l a -> Command l a +(\\) = CSeq + +(^^^) :: WhileProp l Bool -> AnnCommand l () -> AnnCommand l () +prop ^^^ command = CAnn (PropAnn prop ()) command + +(.==) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool +(.==) = HWrap ... rcurry (Op OpEq) + +(.<) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool +(.<) = HWrap ... rcurry (Op OpLT) + +(.>) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool +(.>) = HWrap ... rcurry (Op OpGT) + +(.<=) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool +(.<=) = HWrap ... rcurry (Op OpLE) + +(.>=) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool +(.>=) = HWrap ... rcurry (Op OpGE) + +(.&&) :: WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool +(.&&) = HWrap ... rcurry (Op OpAnd) + +(.||) :: WhileExpr l Bool -> WhileExpr l Bool -> WhileExpr l Bool +(.||) = HWrap ... rcurry (Op OpOr) + +wenot :: WhileExpr l Bool -> WhileExpr l Bool +wenot = HWrap . rcurry (Op OpNot) diff --git a/Language/While/Test.hs b/Language/While/Test.hs new file mode 100644 --- /dev/null +++ b/Language/While/Test.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-unused-imports #-} + +module Language.While.Test where + +import Language.Expression.Pretty +import Language.Expression.Prop +import Language.Verification + +import Language.While.Hoare +import Language.While.Hoare.Prover +import Language.While.Syntax +import Language.While.Syntax.Sugar + +import Data.SBV (SMTConfig (..), defaultSMTCfg) + +testCommandAnn :: Command String (PropAnn String ()) +testCommandAnn = + "Q" .=. 0 \\ (expr ("R" .== "x") *&& expr ("Q" .== 0)) ^^^ + CWhile ("Y" .<= "R") + ((expr ("x" .== ("R" + "Y" * "Q"))) ^^^ + ( "R" .=. "R" - "Y" + \\ "Q" .=. "Q" + 1 + )) + +testPrecond :: WhileProp String Bool +testPrecond = expr ("R" .== "x") + +testPostcond :: WhileProp String Bool +testPostcond = + expr ("x" .== ("R" + "Y" * "Q")) *&& + expr ("R" .< "Y") + +testConfig :: SMTConfig +testConfig = defaultSMTCfg { verbose = False } + +testVcs :: Maybe [WhileProp String Bool] +testVcs = generateVCs testPrecond testPostcond testCommandAnn + +test :: IO (Either (VerifierError (WhileVar String)) Bool) +test = runVerifierWith testConfig $ flip query () $ + checkPartialHoare testPrecond testPostcond testCommandAnn diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/verifiable-expressions.cabal b/verifiable-expressions.cabal new file mode 100644 --- /dev/null +++ b/verifiable-expressions.cabal @@ -0,0 +1,49 @@ +-- This file has been generated from package.yaml by hpack version 0.20.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: dff4863bb87472933f3daa41b069320c635d14714d46d778116a53854de0e95c + +name: verifiable-expressions +version: 0.4.0 +synopsis: An intermediate language for Hoare logic style verification. +description: A typed intermediate language for Hoare logic style verification. It defines the intermediate language and combinators to interact it. +category: Language +author: Bradley Hardy +maintainer: bch29@cam.ac.uk +license: Apache-2.0 +license-file: LICENSE +build-type: Simple +cabal-version: >= 1.10 + +library + ghc-options: -Wall + build-depends: + base >=4.9 && <5 + , containers >=0.5.7 && <0.6 + , lens >=4.16.1 && <5 + , mtl >=2.0 && <3 + , sbv >=7.0 && <8 + , transformers >=0.5 && <0.6 + , union >=0.1.1 && <0.2 + , vinyl >=0.8.1 && <0.9 + exposed-modules: + Language.Expression + Language.Expression.Example + Language.Expression.Choice + Language.Expression.Scope + Language.Expression.GeneralOp + Language.Expression.Prop + Language.Expression.Pretty + Language.Expression.Util + Language.Verification + Language.Verification.Conditions + Language.Verification.Core + Language.While.Hoare + Language.While.Hoare.Prover + Language.While.Syntax + Language.While.Syntax.Sugar + Language.While.Test + other-modules: + Paths_verifiable_expressions + default-language: Haskell2010