verifiable-expressions 0.4.0 → 0.5.0
raw patch · 1 files changed
+22/−15 lines, 1 filesdep ~containersnew-uploaderPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: containers
API changes (from Hackage documentation)
- Language.Expression: instance forall u (k :: u -> *). Language.Expression.HDuofoldableAt k Language.Expression.HFree
- Language.Expression.Choice: instance Language.Expression.Choice.AsOp t1 a1 op1 ~ t2 => Control.Lens.Wrapped.Rewrapped (Language.Expression.Choice.AsOp t3 a2 op2) t2
- Language.Expression.Choice: instance Language.Expression.Choice.HFree' ops1 v1 a1 ~ t => Control.Lens.Wrapped.Rewrapped (Language.Expression.Choice.HFree' ops2 v2 a2) t
- Language.Expression.Pretty: instance Language.Expression.Pretty.Pretty a => Language.Expression.Pretty.Pretty (GHC.Base.Maybe a)
- Language.Verification.Conditions: instance Data.Semigroup.Semigroup (Language.Verification.Conditions.JoinAnnSeq expr var cmd)
- Language.Verification.Core: instance (Data.Typeable.Internal.Typeable v, l ~ Language.Verification.Core.VarKey v, GHC.Show.Show l, Data.Typeable.Internal.Typeable l) => GHC.Exception.Exception (Language.Verification.Core.VerifierError v)
+ Language.Expression: infixr 1 ^>>=
+ Language.Expression: instance forall k1 (k2 :: k1 -> *). Language.Expression.HDuofoldableAt k2 Language.Expression.HFree
+ Language.Expression.Choice: instance (Language.Expression.Choice.AsOp t1 a1 op1 Data.Type.Equality.~ t2) => Control.Lens.Wrapped.Rewrapped (Language.Expression.Choice.AsOp t3 a2 op2) t2
+ Language.Expression.Choice: instance (Language.Expression.Choice.HFree' ops1 v1 a1 Data.Type.Equality.~ t) => Control.Lens.Wrapped.Rewrapped (Language.Expression.Choice.HFree' ops2 v2 a2) t
+ Language.Expression.Pretty: instance Language.Expression.Pretty.Pretty a => Language.Expression.Pretty.Pretty (GHC.Maybe.Maybe a)
+ Language.Verification.Conditions: instance GHC.Base.Semigroup (Language.Verification.Conditions.JoinAnnSeq expr var cmd)
+ Language.Verification.Core: instance (Data.Typeable.Internal.Typeable v, l Data.Type.Equality.~ Language.Verification.Core.VarKey v, GHC.Show.Show l, Data.Typeable.Internal.Typeable l) => GHC.Exception.Type.Exception (Language.Verification.Core.VerifierError v)
- Language.Expression: HPure :: (t a) -> HFree h t a
+ Language.Expression: HPure :: t a -> HFree h t a
- Language.Expression: HWrap :: (h (HFree h t) a) -> HFree h t a
+ Language.Expression: HWrap :: h (HFree h t) a -> HFree h t a
- Language.Expression: hbifold :: (HBifoldableAt k h) => h k k a -> k a
+ Language.Expression: hbifold :: HBifoldableAt k h => h k k a -> k a
- Language.Expression: hbimap :: (HBifunctor h, (HBitraversable h)) => (forall b. s b -> s' b) -> (forall b. t b -> t' b) -> h s t a -> h s' t' a
+ Language.Expression: hbimap :: (HBifunctor h, HBitraversable h) => (forall b. s b -> s' b) -> (forall b. t b -> t' b) -> h s t a -> h s' t' a
- Language.Expression: hbitraverse :: (HBitraversable h, (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)
+ Language.Expression: hbitraverse :: (HBitraversable h, 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)
- Language.Expression: hduofoldMap :: (HDuofoldableAt k h, (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
+ Language.Expression: hduofoldMap :: (HDuofoldableAt k h, 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
- Language.Expression: hduomap :: (HDuofunctor h, (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
+ Language.Expression: hduomap :: (HDuofunctor h, 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
- Language.Expression: hduotraverse :: (HDuotraversable h, (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)
+ Language.Expression: hduotraverse :: (HDuotraversable h, 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)
- Language.Expression: hjoin :: (HBind h) => h (h t) a -> h t a
+ Language.Expression: hjoin :: HBind h => h (h t) a -> h t a
- Language.Expression: hmap :: (HFunctor h, (HTraversable h)) => (forall b. t b -> t' b) -> h t a -> h t' a
+ Language.Expression: hmap :: (HFunctor h, HTraversable h) => (forall b. t b -> t' b) -> h t a -> h t' a
- Language.Expression: hsequence :: (HTraversable h, (Applicative f)) => h (Compose f t) a -> f (h t a)
+ Language.Expression: hsequence :: (HTraversable h, Applicative f) => h (Compose f t) a -> f (h t a)
- Language.Expression: htraverse :: (HTraversable h, (Applicative f)) => (forall b. t b -> f (t' b)) -> h t a -> f (h t' a)
+ Language.Expression: htraverse :: (HTraversable h, Applicative f) => (forall b. t b -> f (t' b)) -> h t a -> f (h t' a)
- Language.Expression: implHfoldMap :: (HFunctor h) => (h k a -> k a) -> (forall b. t b -> k b) -> h t a -> k a
+ Language.Expression: implHfoldMap :: HFunctor h => (h k a -> k a) -> (forall b. t b -> k b) -> h t a -> k a
- Language.Expression.Choice: AsOp :: (op t a) -> AsOp a op
+ Language.Expression.Choice: AsOp :: op t a -> AsOp a op
- Language.Expression.Pretty: pretty2 :: (Pretty2 op, (Pretty1 t)) => op t a -> String
+ Language.Expression.Pretty: pretty2 :: (Pretty2 op, Pretty1 t) => op t a -> String
- Language.Expression.Pretty: prettys2Prec :: (Pretty2 op, (Pretty1 t)) => Int -> op t a -> ShowS
+ Language.Expression.Pretty: prettys2Prec :: (Pretty2 op, Pretty1 t) => Int -> op t a -> ShowS
- Language.Expression.Scope: (^>>>=) :: (HBound k, (HMonad h)) => k h t a -> (forall b. t b -> h t' b) -> k h t' a
+ Language.Expression.Scope: (^>>>=) :: (HBound k, HMonad h) => k h t a -> (forall b. t b -> h t' b) -> k h t' a
- Language.Expression.Scope: SPure :: (f a) -> SFree h f a
+ Language.Expression.Scope: SPure :: f a -> SFree h f a
- Language.Expression.Scope: SWrap :: (h (Scoped (SFree h) f) (SFree h f) a) -> SFree h f a
+ Language.Expression.Scope: SWrap :: h (Scoped (SFree h) f) (SFree h f) a -> SFree h f a
- Language.Expression.Scope: abstract :: (HMonad h) => (forall b. f b -> Maybe (g b)) -> h f a -> Scope g h f a
+ Language.Expression.Scope: abstract :: HMonad h => (forall b. f b -> Maybe (g b)) -> h f a -> Scope g h f a
- Language.Expression.Scope: boundVar :: (HPointed h) => g a -> Scope g h f a
+ Language.Expression.Scope: boundVar :: HPointed h => g a -> Scope g h f a
- Language.Expression.Scope: freeVar :: (HPointed h) => f a -> Scope g h f a
+ Language.Expression.Scope: freeVar :: HPointed h => f a -> Scope g h f a
- Language.Expression.Scope: hbitraverseBV :: (Functor t) => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
+ Language.Expression.Scope: hbitraverseBV :: Functor t => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
- Language.Expression.Util: (...) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
+ Language.Expression.Util: (...) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
- Language.Verification: VEMismatchedSymbolType :: (VarKey v) -> VerifierError v
+ Language.Verification: VEMismatchedSymbolType :: VarKey v -> VerifierError v
- Language.Verification: data SMTConfig :: *
+ Language.Verification: data SMTConfig
- Language.Verification: query :: (VerifiableVar v) => Query v SBool -> VarEnv v -> Verifier v Bool
+ Language.Verification: query :: VerifiableVar v => Query v SBool -> VarEnv v -> Verifier v Bool
- Language.Verification: runVerifierWith :: (VerifiableVar v) => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
+ Language.Verification: runVerifierWith :: VerifiableVar v => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
- Language.Verification.Conditions: Annotation :: (AnnSeq expr var cmd) -> (Prop (expr var) Bool) -> (AnnSeq expr var cmd) -> AnnSeq expr var cmd
+ Language.Verification.Conditions: Annotation :: AnnSeq expr var cmd -> Prop (expr var) Bool -> AnnSeq expr var cmd -> AnnSeq expr var cmd
- Language.Verification.Core: VEMismatchedSymbolType :: (VarKey v) -> VerifierError v
+ Language.Verification.Core: VEMismatchedSymbolType :: VarKey v -> VerifierError v
- Language.Verification.Core: query :: (VerifiableVar v) => Query v SBool -> VarEnv v -> Verifier v Bool
+ Language.Verification.Core: query :: VerifiableVar v => Query v SBool -> VarEnv v -> Verifier v Bool
- Language.Verification.Core: runVerifierWith :: (VerifiableVar v) => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
+ Language.Verification.Core: runVerifierWith :: VerifiableVar v => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
- Language.Verification.Core: throwQuery :: (Exception (VerifierError v)) => VerifierError v -> Query v a
+ Language.Verification.Core: throwQuery :: Exception (VerifierError v) => VerifierError v -> Query v a
- Language.While.Hoare: PropAnn :: (WhileProp l Bool) -> a -> PropAnn l a
+ Language.While.Hoare: PropAnn :: WhileProp l Bool -> a -> PropAnn l a
- Language.While.Hoare: generateVCs :: (VerifiableVar (WhileVar l)) => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool]
+ Language.While.Hoare: generateVCs :: VerifiableVar (WhileVar l) => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool]
- Language.While.Hoare: generateVCs' :: (VerifiableVar (WhileVar l)) => Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a) -> MonadGen l ()
+ Language.While.Hoare: generateVCs' :: VerifiableVar (WhileVar l) => Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a) -> MonadGen l ()
- Language.While.Syntax: CAnn :: a -> (Command l a) -> Command l a
+ Language.While.Syntax: CAnn :: a -> Command l a -> Command l a
- Language.While.Syntax: CAssign :: l -> (WhileExpr l AlgReal) -> Command l a
+ Language.While.Syntax: CAssign :: l -> WhileExpr l AlgReal -> Command l a
- Language.While.Syntax: CIf :: (WhileExpr l Bool) -> (Command l a) -> (Command l a) -> Command l a
+ Language.While.Syntax: CIf :: WhileExpr l Bool -> Command l a -> Command l a -> Command l a
- Language.While.Syntax: CSeq :: (Command l a) -> (Command l a) -> Command l a
+ Language.While.Syntax: CSeq :: Command l a -> Command l a -> Command l a
- Language.While.Syntax: CWhile :: (WhileExpr l Bool) -> (Command l a) -> Command l a
+ Language.While.Syntax: CWhile :: WhileExpr l Bool -> Command l a -> Command l a
- Language.While.Syntax: evalWhileExpr :: (Applicative f) => (forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a
+ Language.While.Syntax: evalWhileExpr :: Applicative f => (forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a
- Language.While.Syntax: lookupVar :: (Ord l) => Map l AlgReal -> WhileVar l a -> Maybe a
+ Language.While.Syntax: lookupVar :: Ord l => Map l AlgReal -> WhileVar l a -> Maybe a
- Language.While.Syntax: oneStep :: (Ord l) => Command l a -> State (Map l AlgReal) (StepResult (Command l a))
+ Language.While.Syntax: oneStep :: Ord l => Command l a -> State (Map l AlgReal) (StepResult (Command l a))
- Language.While.Syntax: prettys1Binop :: (Pretty1 t) => Int -> String -> (Int -> t a -> t b -> ShowS)
+ Language.While.Syntax: prettys1Binop :: Pretty1 t => Int -> String -> Int -> t a -> t b -> ShowS
- Language.While.Syntax: runCommand :: (Ord l) => Command l a -> State (Map l AlgReal) Bool
+ Language.While.Syntax: runCommand :: Ord l => Command l a -> State (Map l AlgReal) Bool
Files
- verifiable-expressions.cabal +22/−15
verifiable-expressions.cabal view
@@ -1,32 +1,29 @@--- This file has been generated from package.yaml by hpack version 0.20.0.+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.1. -- -- see: https://github.com/sol/hpack ----- hash: dff4863bb87472933f3daa41b069320c635d14714d46d778116a53854de0e95c+-- hash: ce4006a4eb6cc4997fc47936009d3e9b564b686fb2d70bab60d3a536d8c65df7 name: verifiable-expressions-version: 0.4.0+version: 0.5.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+homepage: https://github.com/camfort/verifiable-expressions#readme+bug-reports: https://github.com/camfort/verifiable-expressions/issues author: Bradley Hardy-maintainer: bch29@cam.ac.uk+maintainer: madgenhetic@gmail.com license: Apache-2.0 license-file: LICENSE build-type: Simple-cabal-version: >= 1.10 +source-repository head+ type: git+ location: https://github.com/camfort/verifiable-expressions+ 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@@ -46,4 +43,14 @@ Language.While.Test other-modules: Paths_verifiable_expressions+ ghc-options: -Wall+ build-depends:+ base >=4.9 && <5+ , containers >=0.5.7 && <0.7+ , 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 default-language: Haskell2010