verifiable-expressions (empty) → 0.4.0

raw patch · 19 files changed

+3083/−0 lines, 19 filesdep +basedep +containersdep +lenssetup-changed

Dependencies added: base, containers, lens, mtl, sbv, transformers, union, vinyl

Files

• LICENSE +202/−0
• Language/Expression.hs +529/−0
• Language/Expression/Choice.hs +228/−0
• Language/Expression/Example.hs +422/−0
• Language/Expression/GeneralOp.hs +71/−0
• Language/Expression/Pretty.hs +179/−0
• Language/Expression/Prop.hs +170/−0
• Language/Expression/Scope.hs +190/−0
• Language/Expression/Util.hs +4/−0
• Language/Verification.hs +44/−0
• Language/Verification/Conditions.hs +254/−0
• Language/Verification/Core.hs +223/−0
• Language/While/Hoare.hs +95/−0
• Language/While/Hoare/Prover.hs +38/−0
• Language/While/Syntax.hs +285/−0
• Language/While/Syntax/Sugar.hs +56/−0
• Language/While/Test.hs +42/−0
• Setup.hs +2/−0
• verifiable-expressions.cabal +49/−0

@@ -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.

@@ -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)

@@ -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'

@@ -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)

@@ -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

@@ -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 -> "<nothing>" ++ r++instance Pretty () where+  pretty = show

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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]

@@ -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

@@ -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 []

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -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