language-sally 0.1.0.0 → 0.1.0.1

raw patch · 4 files changed

+37/−20 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

language-sally.cabal +1/−1
src/Language/Sally.hs +23/−6
src/Language/Sally/Expr.hs +9/−9
src/Language/Sally/Types.hs +4/−4

language-sally.cabal view

@@ -1,5 +1,5 @@ name:                language-sally-version:             0.1.0.0+version:             0.1.0.1 synopsis:            AST and pretty printer for Sally description:         AST and pretty printer for the Sally                      <https://github.com/SRI-CSL/sally> input language

src/Language/Sally.hs view

@@ -7,14 +7,31 @@ -- Stability   :  experimental -- Portability :  unknown ----- This module re-exports all the definitions from Language.Sally.*+-- @language-sally@ is a package which contains a convenient AST and pretty+-- printer for the input language of SRI's Sally model checker+-- <https://github.com/SRI-CSL/sally>. --+-- The main types exported by the package defined in "Language.Sally.Types"+-- and correspond to the main block types in Sally's input language: the state+-- type, state formula, transition formula, and transition system definition.+--+-- Low-level expressions and literals may be contructed using the functions in+-- "Language.Sally.Expr", while the pretty printing mechanism is split between+-- "Language.Sally.SExpPP" (dealing with layout of S-expressions) and+-- "Language.Sally.PPrint" (dealing with the rendering of ASTs).+--+-- This module re-exports all the definitions from the submodules.+--  module Language.Sally (-  module X+    -- * re-exports+    module Language.Sally.Expr+  , module Language.Sally.PPrint+  , module Language.Sally.SExpPP+  , module Language.Sally.Types ) where -import Language.Sally.Expr   as X-import Language.Sally.PPrint as X-import Language.Sally.SExpPP as X-import Language.Sally.Types  as X+import Language.Sally.Expr+import Language.Sally.PPrint+import Language.Sally.SExpPP+import Language.Sally.Types

src/Language/Sally/Expr.hs view

@@ -106,8 +106,8 @@               else error "multExpr: non-linear arithmetic is not supported"  -- | Determine if a Sally expression is a constant for the purposes of linear--- multiplication. Note: this is an over approximation, e.g. (x + (-x))*y is a constant 0--- times y, but will not pass this predicate.+-- multiplication. Note: this is an over approximation, e.g. @(x + (-x))*y@+-- is a constant equal to @0@ times @y@, but will not pass this predicate. isMultConst :: SallyExpr -> Bool isMultConst (SELit _) = True isMultConst (SEVar _) = False@@ -121,19 +121,19 @@ eqExpr :: SallyExpr -> SallyExpr -> SallyExpr eqExpr x y = SEPre (SPEq x y) --- | @a `ltExpr` b@ represents the expression @a < b@.+-- | @a \`ltExpr\` b@ represents the expression @a \< b@. ltExpr :: SallyExpr -> SallyExpr -> SallyExpr ltExpr x y = SEPre (SPLt x y) --- | @a `leqExpr` b@ represents the expression @a <= b@.+-- | @a \`leqExpr\` b@ represents the expression @a \<= b@. leqExpr :: SallyExpr -> SallyExpr -> SallyExpr leqExpr x y = SEPre (SPLEq x y) --- | @a `gtExpr` b@ represents the expression @a > b@.+-- | @a \`gtExpr\` b@ represents the expression @a > b@. gtExpr :: SallyExpr -> SallyExpr -> SallyExpr gtExpr x y = SEPre (SPGt x y) --- | @a `geqExpr` b@ represents the expression @a >= b@.+-- | @a \`geqExpr\` b@ represents the expression @a >= b@. geqExpr :: SallyExpr -> SallyExpr -> SallyExpr geqExpr x y = SEPre (SPGEq x y) @@ -160,7 +160,7 @@                                  ++ show x)  -- | Create an if-then-else expression: @mux b x y@ represents the statement--- "if b then x else y".+-- @if b then x else y@. muxExpr :: SallyExpr -> SallyExpr -> SallyExpr -> SallyExpr muxExpr = SEMux @@ -300,7 +300,7 @@     _ -> a <| flattenOrs rest flattenOrs _ = undefined  -- make compiler happy :) --- | Top-down rewriting of 'and' terms including constant folding and+-- | Top-down rewriting of conjunctions of terms including constant folding and -- constructor reduction. simplifyAnds :: SallyPred -> SallyPred simplifyAnds p =@@ -325,7 +325,7 @@     SPGt    x y -> SPGt (constFold x) (constFold y)     SPExpr  e   -> SPExpr (constFold e) --- | Top-down rewriting of 'or' terms including constant folding and+-- | Top-down rewriting of disjunctions including constant folding and -- constructor reduction. simplifyOrs :: SallyPred -> SallyPred simplifyOrs p =

src/Language/Sally/Types.hs view

@@ -180,10 +180,10 @@                | SPImpl  SallyPred SallyPred     -- ^ implication                | SPNot   SallyPred               -- ^ logical negation                | SPEq    SallyExpr SallyExpr     -- ^ ==-               | SPLEq   SallyExpr SallyExpr     -- ^ <=-               | SPGEq   SallyExpr SallyExpr     -- ^ >=-               | SPLt    SallyExpr SallyExpr     -- ^ <-               | SPGt    SallyExpr SallyExpr     -- ^ >+               | SPLEq   SallyExpr SallyExpr     -- ^ \<=+               | SPGEq   SallyExpr SallyExpr     -- ^ \>=+               | SPLt    SallyExpr SallyExpr     -- ^ \<+               | SPGt    SallyExpr SallyExpr     -- ^ \>   deriving (Show, Eq)  instance ToSExp SallyPred where