packages feed

language-sally (empty) → 0.1.0.0

raw patch · 9 files changed

+909/−0 lines, 9 filesdep +ansi-wl-pprintdep +basedep +bytestringsetup-changed

Dependencies added: ansi-wl-pprint, base, bytestring, containers, text

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for language-sally++## 0.1.0.0  -- 2017-06-02++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,13 @@+Copyright (c) 2017 Benjamin Jones++Permission to use, copy, modify, and/or distribute this software for any purpose+with or without fee is hereby granted, provided that the above copyright notice+and this permission notice appear in all copies.++THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND+FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS+OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER+TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF+THIS SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ language-sally.cabal view
@@ -0,0 +1,29 @@+name:                language-sally+version:             0.1.0.0+synopsis:            AST and pretty printer for Sally+description:         AST and pretty printer for the Sally+                     <https://github.com/SRI-CSL/sally> input language+license:             ISC+license-file:        LICENSE+author:              Benjamin Jones+maintainer:          bjones@galois.com+copyright:           Galois, Inc. 2017+category:            Language+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10++library+  build-depends:       base           >= 4.8   && < 5+                     , bytestring     >= 0.10+                     , containers     >= 0.5+                     , text           >= 1.2.2 && < 1.3+                     , ansi-wl-pprint >= 0.6+  hs-source-dirs:      src+  default-language:    Haskell2010+  exposed-modules:+                       Language.Sally+                       Language.Sally.Expr+                       Language.Sally.PPrint+                       Language.Sally.SExpPP+                       Language.Sally.Types
+ src/Language/Sally.hs view
@@ -0,0 +1,20 @@+-- |+-- Module      :  Language.Sally+-- Copyright   :  Benjamin Jones 2017+-- License     :  ISC+--+-- Maintainer  :  bjones@galois.com+-- Stability   :  experimental+-- Portability :  unknown+--+-- This module re-exports all the definitions from Language.Sally.*+--++module Language.Sally (+  module X+) 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
+ src/Language/Sally/Expr.hs view
@@ -0,0 +1,357 @@+-- |+-- Module      :  Language.Sally.Expr+-- Description :  Smart constructors for Sally AST types+-- Copyright   :  Benjamin Jones <bjones@galois.com> 2016-2017+-- License     :  BSD3+--+-- Maintainer  :  bjones@galois.com+-- Stability   :  experimental+-- Portability :  unknown+--+-- Better constructors for Sally expresssions and predicates than the raw ones+-- defined in "Language.Sally.Types".+--++{-# LANGUAGE ViewPatterns #-}++module Language.Sally.Expr (+    -- * better constructors+    boolExpr+  , boolPred+  , intExpr+  , zeroExpr+  , oneExpr+  , realExpr+  , addExpr+  , subExpr+  , multExpr+  , divExpr+  , notExpr+  , eqExpr+  , neqExpr+  , ltExpr+  , leqExpr+  , gtExpr+  , geqExpr+  , muxExpr+  , andExprs+  , andPreds+  , orExprs+  , varExpr+  , varExpr'+  , xorExpr+  -- * complex expression builders+  , minExpr+  , countExpr+  -- * expression rewriting+  , constFold+  , simplifyAnds+  , simplifyOrs+  , flattenAnds+  , flattenOrs+) where++import Data.Sequence (Seq, (<|), (><), viewl, ViewL(..))+import qualified Data.Sequence as Seq+import Language.Sally.Types+++-- Better Constructors ---------------------------------------------------------++-- | Create a constant boolean expression.+boolExpr :: Bool -> SallyExpr+boolExpr = SELit . SConstBool++-- | Create a constant boolean predicate.+boolPred :: Bool -> SallyPred+boolPred = SPConst++-- | Create a constant integer expression.+intExpr :: Integral a => a -> SallyExpr+intExpr = SELit . SConstInt . fromIntegral++-- | Create an expression for zero as an integer in Sally.+zeroExpr :: SallyExpr+zeroExpr = intExpr (0 :: Int)++-- | Create an expression for one as an integer in Sally.+oneExpr :: SallyExpr+oneExpr = intExpr (1 :: Int)++-- | Create a constant real expression.+realExpr :: Real a => a -> SallyExpr+realExpr = SELit . SConstReal . toRational+++-- | Better constructor for adding expressions+--   TODO maintain normal form+addExpr :: SallyExpr -> SallyExpr -> SallyExpr+addExpr x y = SEArith (SAAdd x y)++-- | Subtract two 'SallyExpr'.+subExpr :: SallyExpr -> SallyExpr -> SallyExpr+subExpr x y = SEArith (SAAdd x ny)+  where ny = multExpr (SELit (SConstInt (-1))) y++-- | Better constructor for multiplying expressions; checks that one of the+-- operands is a constant.+multExpr :: SallyExpr -> SallyExpr -> SallyExpr+multExpr x y = if isMultConst x || isMultConst y then SEArith (SAMult x y)+               else error "multExpr: non-linear arithmetic is not supported"++-- | Better constructor for dividing expressions; checks that the denominator+-- is a constant.+divExpr :: SallyExpr -> SallyExpr -> SallyExpr+divExpr x y = if isMultConst y then SEArith (SADiv x y)+              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.+isMultConst :: SallyExpr -> Bool+isMultConst (SELit _) = True+isMultConst (SEVar _) = False+isMultConst (SEPre _) = False+isMultConst (SEArith (SAAdd x y))  = isMultConst x && isMultConst y+isMultConst (SEArith (SAMult x y)) = isMultConst x && isMultConst y+isMultConst (SEArith (SAExpr _)) = False+isMultConst SEMux{} = False++-- | Create the expression equating two given expressions.+eqExpr :: SallyExpr -> SallyExpr -> SallyExpr+eqExpr x y = SEPre (SPEq x y)++-- | @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@.+leqExpr :: SallyExpr -> SallyExpr -> SallyExpr+leqExpr x y = SEPre (SPLEq x y)++-- | @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@.+geqExpr :: SallyExpr -> SallyExpr -> SallyExpr+geqExpr x y = SEPre (SPGEq x y)++-- | Create the expression that is the boolean negation of the given one.+notExpr :: SallyExpr -> SallyExpr+notExpr x = SEPre (SPNot (getPred x))++-- | Create the XOR of two Sally expressions.+xorExpr :: SallyExpr -> SallyExpr -> SallyExpr+xorExpr x y = andExprs [orExprs [x, y], notExpr (andExprs [x, y])]++-- | Create the expression representing non-equality.+neqExpr :: SallyExpr -> SallyExpr -> SallyExpr+neqExpr x y = notExpr (eqExpr x y)++-- | Turn a SallyExpr into a SallyPred (if possible)+getPred :: SallyExpr -> SallyPred+getPred x = case x of+              SEPre w   -> w+              SELit{}   -> SPExpr x+              SEVar{}   -> SPExpr x+              SEMux{}   -> SPExpr x+              SEArith{} -> error ("notExpr: cannot turn expression into predicate: "+                                 ++ show x)++-- | Create an if-then-else expression: @mux b x y@ represents the statement+-- "if b then x else y".+muxExpr :: SallyExpr -> SallyExpr -> SallyExpr -> SallyExpr+muxExpr = SEMux++-- | Form the conjunction of the given expressions (which should be+-- predicates, but this is not checked).+andExprs :: [SallyExpr] -> SallyExpr+andExprs es = SEPre $ andPreds (fmap getPred es)++-- | And over multiple predicates, doing some small inline simplification+andPreds :: [SallyPred] -> SallyPred+andPreds []  = SPConst True  -- intersection over no sets is the whole universe+andPreds [p] = p+andPreds ps = SPAnd . flattenAnds . Seq.fromList $ ps++-- | Form the disjunction of the given expressions (which should be+-- predicates, but this is not checked).+orExprs :: [SallyExpr] -> SallyExpr+orExprs es = SEPre $ orPreds (fmap getPred es)++-- | Or over multiple predicates, doing some small inline simplification+orPreds :: [SallyPred] -> SallyPred+orPreds [] = SPConst False  -- union over no sets is the empty set+orPreds [p] = p+orPreds ps = SPOr . flattenOrs . Seq.fromList $ ps++-- | Create a variable expression.+varExpr :: SallyVar -> SallyExpr+varExpr = SEVar++-- | Create a variable expression from a name.+varExpr' :: Name -> SallyExpr+varExpr' = SEVar . varFromName+++-- More Complicated expression builders ----------------------------------------++-- | Given a non-empty finite list of expressions, build an expression to+-- compute their minimum. The second argument is a special value which, if+-- present causes expressions in the list with this value to be ignored in the+-- calculation. If the input list contains only the special value, then the+-- special value itself is returned.+minExpr :: [SallyExpr] -> Maybe SallyExpr -> SallyExpr+minExpr [] _ = error "minExpr: cannot apply minExpr to empty list"+minExpr (x:rest) sp' = go sp' x rest+  where go _ m [] = m+        go Nothing m (y:more) = muxExpr (ltExpr m y)+                                        (go sp' m more)+                                        (go sp' y more)+        go (Just sp) m (y:more) = muxExpr (andExprs [ltExpr m y, neqExpr m sp])+                                          (go sp' m more)+                                          (go sp' y more)++-- | Build a Sally expression representing the number of times a particular+-- item appears in a list of expressions.+countExpr :: SallyExpr -> [SallyExpr] -> SallyExpr+countExpr _ [] = zeroExpr+countExpr x (y:rest) = muxExpr (eqExpr x y) (addExpr oneExpr (countExpr x rest))+                                            (countExpr x rest)+++-- Expression Rewriting --------------------------------------------------------++-- | A basic top-down recursive constant folding function.+constFold :: SallyExpr -> SallyExpr+constFold = simplifyExpr . constFold'+  where+    constFold' e@(SELit _) = e+    constFold' e@(SEVar _) = e+    constFold' (SEPre p) = SEPre (constFoldP p)+    constFold' (SEArith a) = SEArith (constFoldA a)+    constFold' (SEMux i t e) = constFoldM i t e++-- | Perform constant folding over a Sally predicate.+constFoldP :: SallyPred -> SallyPred+constFoldP = simplifyOrs . simplifyAnds++-- | Perform constant folding over a Sally arithmetic expression.+constFoldA :: SallyArith -> SallyArith+-- additive folding+--   add zero+constFoldA (SAAdd (SELit (SConstInt 0)) e)  = SAExpr (constFold e)+constFoldA (SAAdd e (SELit (SConstInt 0)))  = SAExpr (constFold e)+constFoldA (SAAdd (SELit (SConstReal 0)) e) = SAExpr (constFold e)+constFoldA (SAAdd e (SELit (SConstReal 0))) = SAExpr (constFold e)+--  add two constant literals+constFoldA (SAAdd (SELit (SConstInt x)) (SELit (SConstInt y))) =+  SAExpr (SELit (SConstInt (x+y)))+constFoldA (SAAdd (SELit (SConstReal x)) (SELit (SConstReal y))) =+  SAExpr (SELit (SConstReal (x+y)))+-- additive fall through case+constFoldA a@(SAAdd _ _) = a+-- multiplicitive folding:+--   mult by 1+constFoldA (SAMult (SELit (SConstInt 1)) e)  = SAExpr (constFold e)+constFoldA (SAMult e (SELit (SConstInt 1)))  = SAExpr (constFold e)+constFoldA (SAMult (SELit (SConstReal 1)) e) = SAExpr (constFold e)+constFoldA (SAMult e (SELit (SConstReal 1))) = SAExpr (constFold e)+--   mult by 0+constFoldA (SAMult (SELit (SConstInt 0)) _)  = SAExpr zeroExpr+constFoldA (SAMult _ (SELit (SConstInt 0)))  = SAExpr zeroExpr+constFoldA (SAMult (SELit (SConstReal 0)) _) = SAExpr zeroExpr+constFoldA (SAMult _ (SELit (SConstReal 0))) = SAExpr zeroExpr+--  mult two constant literals+constFoldA (SAMult (SELit (SConstInt x)) (SELit (SConstInt y))) =+  SAExpr (SELit (SConstInt (x*y)))+constFoldA (SAMult (SELit (SConstReal x)) (SELit (SConstReal y))) =+  SAExpr (SELit (SConstReal (x*y)))+--  fall through general case+constFoldA a@(SAMult _ _) = a+constFoldA (SAExpr e) = SAExpr (constFold e)++-- | Constant fold a mux expression+constFoldM :: SallyExpr ->  SallyExpr -> SallyExpr -> SallyExpr+constFoldM (SELit (SConstBool True)) t _  = constFold t+constFoldM (SELit (SConstBool False)) _ f = constFold f+constFoldM i t e = SEMux i (constFold t) (constFold e)++-- | Recursively flatten a tree of @and@ expressions into an @and@ sequence.+flattenAnds :: Seq SallyPred -> Seq SallyPred+flattenAnds (viewl -> xs) =+  case xs of+    EmptyL -> Seq.empty+    a :< rest  ->+      case a of+        SPAnd ys -> flattenAnds ys >< flattenAnds rest+        -- TODO enable rewriting here?+        -- SPConst True  -> flattenAnds rest+        -- SPConst False -> a <| Seq.empty+        _ -> a <| flattenAnds rest++-- | Recursively flatten a tree of @or@ expressions into an @or@ sequence.+flattenOrs :: Seq SallyPred -> Seq SallyPred+flattenOrs (viewl -> EmptyL) = Seq.empty+flattenOrs (viewl -> a :< rest) =+  case a of+    SPOr ys -> flattenOrs ys >< flattenOrs rest+    _ -> a <| flattenOrs rest+flattenOrs _ = undefined  -- make compiler happy :)++-- | Top-down rewriting of 'and' terms including constant folding and+-- constructor reduction.+simplifyAnds :: SallyPred -> SallyPred+simplifyAnds p =+  case p of+    -- main case+    SPAnd xs ->+      let ys = flattenAnds (fmap simplifyAnds xs) :: Seq SallyPred+      in case viewl ys of+           EmptyL  -> SPConst True           -- empty 'and'+           z :< zs -> if Seq.null zs then z  -- single elt. 'and'+                      else SPAnd ys          -- multiple+    SPExpr (SEPre q) -> simplifyAnds q       -- strip off SPExpr . SEPre+    -- other cases+    SPConst _   -> p+    SPOr    xs  -> SPOr (fmap simplifyAnds xs)+    SPImpl  x y -> SPImpl (simplifyAnds x) (simplifyAnds y)+    SPNot   x   -> SPNot (simplifyAnds x)+    SPEq    x y -> SPEq (constFold x) (constFold y)+    SPLEq   x y -> SPLEq (constFold x) (constFold y)+    SPGEq   x y -> SPGEq (constFold x) (constFold y)+    SPLt    x y -> SPLt (constFold x) (constFold y)+    SPGt    x y -> SPGt (constFold x) (constFold y)+    SPExpr  e   -> SPExpr (constFold e)++-- | Top-down rewriting of 'or' terms including constant folding and+-- constructor reduction.+simplifyOrs :: SallyPred -> SallyPred+simplifyOrs p =+  case p of+    -- main case+    SPOr xs ->+      let ys = flattenOrs (fmap simplifyOrs xs)+      in case viewl ys of+           EmptyL  -> SPConst False          -- empty disjunction+           z :< zs -> if Seq.null zs then z  -- single term+                      else SPOr ys           -- multiple terms+    SPExpr (SEPre q) -> simplifyOrs q        -- strip off SPExpr . SEPre+    -- other cases+    SPConst _   -> p+    SPAnd   xs  -> SPAnd (fmap simplifyOrs xs)+    SPImpl  x y -> SPImpl (simplifyOrs x) (simplifyOrs y)+    SPNot   x   -> SPNot (simplifyOrs x)+    SPEq    x y -> SPEq (constFold x) (constFold y)+    SPLEq   x y -> SPLEq (constFold x) (constFold y)+    SPGEq   x y -> SPGEq (constFold x) (constFold y)+    SPLt    x y -> SPLt (constFold x) (constFold y)+    SPGt    x y -> SPGt (constFold x) (constFold y)+    SPExpr  e   -> SPExpr (constFold e)++-- | Reduce SallyExpr terms by removing redundant constructors.+simplifyExpr :: SallyExpr -> SallyExpr+simplifyExpr (SEArith (SAExpr e)) = simplifyExpr e+simplifyExpr (SEPre (SPExpr e)) = simplifyExpr e+simplifyExpr e = e
+ src/Language/Sally/PPrint.hs view
@@ -0,0 +1,63 @@+-- |+-- Module      :  Language.Sally.PPrint+-- Description :  Export some pretty printer utilities+-- Copyright   :  Benjamin Jones 2017+-- License     :  ISC+--+-- Maintainer  :  bjones@galois.com+-- Stability   :  experimental+-- Portability :  unknown+--+-- Export top-level pretty printer functions taking general pretty-printable+-- values and writing them to 'stdout' or to 'String'. These functions avoid+-- the need to export the specific pretty printer library to clients.+--++module Language.Sally.PPrint (+  -- * pretty printing+    spPrint+  , pprintSystem+  , putSystem+  , putSExpCompact+  , putSystemLn+  , hPutSystem+) where++import qualified Data.Text as T+import           Data.Text (Text)+import qualified Data.Text.Encoding as E+import qualified Data.ByteString.Char8 as BS++import System.IO (Handle)+import Text.PrettyPrint.ANSI.Leijen++import Language.Sally.SExpPP+++-- TODO Rename and prune these functions.++-- | Render a value of the 'Pretty' class as a string.+spPrint :: Pretty a => a -> String+spPrint = T.unpack . pprintSystem++-- | Render a value of the 'Pretty' class as "Data.Text".+pprintSystem :: Pretty a => a -> Text+pprintSystem x = T.pack (displayS (renderPretty ribbon wid . pretty $ x) "")+  where ribbon = 72 / 80 :: Float+        wid    = 80++-- | Render a value of the pretty class to 'stdout'.+putSystem :: Pretty a => a -> IO ()+putSystem = putDoc . pretty++-- | Render a value of the pretty class in a compact fashion to 'stdout'.+putSExpCompact :: ToSExp a => a -> IO ()+putSExpCompact = putDoc . sxPrettyCompact++-- | Same as 'putSystem' but with a newline.+putSystemLn :: Pretty a => a -> IO ()+putSystemLn tr = putSystem tr >> putStrLn ""++-- | Same as 'putSystem' but takes a 'Handle'.+hPutSystem :: Pretty a => Handle -> a -> IO ()+hPutSystem h = BS.hPutStr h . E.encodeUtf8 . pprintSystem
+ src/Language/Sally/SExpPP.hs view
@@ -0,0 +1,76 @@+-- |+-- Module      :  SExpPP+-- Description :  A simple S-expression type with a pretty printable 'Doc' type+--                at the leaves+-- Copyright   :  Benjamin F Jones 2016+-- License     :  ISC+--+-- Maintainer  :  bjones@galois.com+-- Stability   :  experimental+-- Portability :  unknown+--+-- This module gives a uniform way to pretty print S-expressions through a+-- typeclass 'ToSExp'.+--++{-# LANGUAGE OverloadedStrings #-}++module Language.Sally.SExpPP (+  -- * S-expression pretty printing+    SExp(..)+  , ToSExp(..)+  , bareText+  -- * misc+  , sallyCom+) where+++import Data.Text (Text)+import qualified Data.Text as T+import Text.PrettyPrint.ANSI.Leijen+++-- | A simple S-expression datatype with 'Doc' values at the leaves.+data SExp = SXBare Doc     -- ^ bare symbol or literal represented by a 'Doc'+          | SXList [SExp]  -- ^ list of 'SExp', e.g. (foo a b)++-- | Typeclass for values that can be converted to a 'SExp'. These values can+-- then be pretty printed using the default layout scheme given by 'sxPretty'.+class ToSExp a where+  toSExp :: a -> SExp++  sxPretty :: a -> Doc+  sxPretty = sxPrettyDefault . toSExp++  sxPrettyCompact :: a -> Doc+  sxPrettyCompact = sxPrettyCompactDefault . toSExp++-- | Trivial 'ToSExp' instance for 'SExp'.+instance ToSExp SExp where+  toSExp = id++-- | Pretty print an 'SExp' using the default layout scheme.+sxPrettyDefault :: SExp -> Doc+sxPrettyDefault (SXBare x) = x+sxPrettyDefault (SXList []) = lparen <> rparen+sxPrettyDefault (SXList xs) = parens . group . align . vsep . fmap sxPretty $ xs+-- sxPrettyDefault (SXList ll@(x:_)) = case x of+--   SXBare _ -> parens (hang' (fillSep (map sxPretty ll)))+--   SXList _ -> parens (fillSep (map sxPretty ll))++-- | Pretty print an 'SExp' using the default *compact* layout scheme.+sxPrettyCompactDefault :: SExp -> Doc+sxPrettyCompactDefault (SXBare x) = x+sxPrettyCompactDefault (SXList []) = lparen <> rparen+sxPrettyCompactDefault (SXList xs) = parens . hsep . fmap sxPretty $ xs++-- | Inject a text literal as a 'SExp'.+bareText :: Text -> SExp+bareText = SXBare . text . T.unpack+++-- Misc Sally Specific Items ---------------------------------------------------++-- | A Sally comment.+sallyCom :: Doc+sallyCom = text ";;"
+ src/Language/Sally/Types.hs view
@@ -0,0 +1,344 @@+-- |+-- Module      :  Language.Sally.Types+-- Description :  AST types for the Sally input language+-- Copyright   :  Benjamin Jones 2016+-- License     :  ISC+--+-- Maintainer  :  bjones@galois.com+-- Stability   :  experimental+-- Portability :  unknown+--+-- This module defines types reflecting the basic Sally input language+-- sections and base types.+--++{-# LANGUAGE OverloadedStrings #-}++module Language.Sally.Types (+    -- * Name type+    Name+  , textFromName+  , nameFromT+  , nameFromS+  , catNamesWith+  , bangNames+  , scoreNames+  , nextName+  , stateName+  , inputName+  , varFromName+    -- * Base types+  , SallyBaseType(..)+  , SallyConst(..)+    -- * Types for defining transition systems+  , SallyState(..)+  , SallyPred(..)+  , SallyVar(..)+  , SallyArith(..)+  , SallyExpr(..)+  , ToSallyExpr(..)+  , SallyStateFormula(..)+  , SallyLet+  , SallyTransition(..)+  , SallySystem(..)+  , TrResult(..)+) where++import Data.Foldable (toList)+import Data.List (intersperse)+import Data.Ratio (numerator, denominator)+import Data.Sequence (Seq)+import Data.String+import Data.Text (Text)+import qualified Data.Text as T+import Text.PrettyPrint.ANSI.Leijen++import Language.Sally.SExpPP+++-- Name type for Sally namespaces and variables ------------------------------------++-- | A 'Name' is a wrapped up strict Text.+newtype Name = Name { textFromName :: Text {- ^ unwrap a 'Name' -} }+  deriving (Show, Eq, Ord)++instance Pretty Name where+  pretty = text . T.unpack . textFromName++instance ToSExp Name where+  toSExp = SXBare . text . T.unpack . textFromName++-- | Convert a String to a 'Name'.+nameFromS :: String -> Name+nameFromS = Name . T.pack++-- | Convert a Text to a 'Name'.+nameFromT :: Text -> Name+nameFromT = Name++instance IsString Name where+  fromString = nameFromS++-- | Concatenate names with the given seperating text in between+catNamesWith :: Text -> Name -> Name -> Name+catNamesWith sp a b = Name (textFromName a `T.append` sp `T.append` textFromName b)++-- | Concatenate names with a 'bang' separated in between+bangNames :: Name -> Name -> Name+bangNames = catNamesWith "!"++-- | Concatenate names with an 'underscore' separated in between+scoreNames :: Name -> Name -> Name+scoreNames = catNamesWith "_"++-- | Return the name of the given name in the "next" namespace+nextName :: Name -> Name+nextName = catNamesWith "" "next."++-- | Return the name of the given name in the "state" namespace+stateName :: Name -> Name+stateName = catNamesWith "" "state."++-- | Return the name of the given name in the "input" namespace+inputName :: Name -> Name+inputName = catNamesWith "" "input."+++-- Constants and base types ----------------------------------------------------++-- | A defined constant. For our purposes, a real number is represented+-- (approximated) by an exact rational number.+data SallyConst = SConstBool Bool+                | SConstInt  Integer+                | SConstReal Rational+  deriving (Show, Eq)++instance ToSExp SallyConst where+  toSExp (SConstBool b) = SXBare $ if b then text "true" else text "false"+  toSExp (SConstInt  x) =+    let bare = SXBare $ integer x+    in if x >= 0 then bare+       else SXList [bare]  -- if x < 0, enclose in parens+  toSExp (SConstReal x) =+    let nx = numerator x+        dx = denominator x+    in if dx == 1 then toSExp (SConstInt nx)  -- special case integers+                  else SXList [ SXBare "/", toSExp (SConstInt nx)+                              , toSExp (SConstInt dx) ]++-- | Base data types in Sally: Booleans, (mathematical) Integers, and+-- (mathematical) Reals+data SallyBaseType = SBool+                   | SInt+                   | SReal+  deriving (Show, Eq)++instance ToSExp SallyBaseType where+  toSExp SBool = bareText "Bool"+  toSExp SInt  = bareText "Int"+  toSExp SReal = bareText "Real"+++-- Untyped Expression AST for Sally --------------------------------------------++-- | A 'SallyVar' is a wrapped up variable name.+newtype SallyVar = SallyVar { textFromVar :: Text }+  deriving (Show, Eq)++instance ToSExp SallyVar where+  toSExp = SXBare . text . T.unpack . textFromVar++-- | Create a 'SallyVar' from a 'Name'.+varFromName :: Name -> SallyVar+varFromName = SallyVar . textFromName++-- | Expressions+data SallyExpr = SELit   SallyConst              -- ^ constant literal+               | SEVar   SallyVar                -- ^ variable+               | SEPre   SallyPred               -- ^ boolean expression+               | SEArith SallyArith              -- ^ arithmetic expression+               | SEMux   SallyExpr SallyExpr SallyExpr  -- ^ if then else+  deriving (Show, Eq)++-- | A typeclass for types that can be converted to a 'SallyExpr'.+class ToSallyExpr a where+  -- | Convert a value to a 'SallyExpr'.+  toSallyExpr :: a -> SallyExpr++instance ToSExp SallyExpr where+  toSExp (SELit x)   = SXBare (sxPretty x)+  toSExp (SEVar x)   = SXBare (sxPretty x)+  toSExp (SEPre x)   = toSExp x+  toSExp (SEArith x) = toSExp x+  toSExp (SEMux x y z) = SXList [bareText "ite", toSExp x, toSExp y, toSExp z]++-- | Predicates+data SallyPred = SPConst Bool                    -- ^ boolean constant+               | SPExpr  SallyExpr               -- ^ a boolean valued expression+               | SPAnd   (Seq SallyPred)         -- ^ and+               | SPOr    (Seq SallyPred)         -- ^ or+               | SPImpl  SallyPred SallyPred     -- ^ implication+               | SPNot   SallyPred               -- ^ logical negation+               | SPEq    SallyExpr SallyExpr     -- ^ ==+               | SPLEq   SallyExpr SallyExpr     -- ^ <=+               | SPGEq   SallyExpr SallyExpr     -- ^ >=+               | SPLt    SallyExpr SallyExpr     -- ^ <+               | SPGt    SallyExpr SallyExpr     -- ^ >+  deriving (Show, Eq)++instance ToSExp SallyPred where+  toSExp (SPConst x)   = SXBare (text (if x then "true" else "false"))+  toSExp (SPExpr  x)   = SXBare (sxPretty x)+  toSExp (SPAnd   xs)  = SXList (bareText "and" : toList (fmap toSExp xs))+  toSExp (SPOr    xs)  = SXList (bareText "or"  : toList (fmap toSExp xs))+  toSExp (SPImpl  p q) = SXList [bareText "=>", toSExp p, toSExp q]+  toSExp (SPNot   p)   = SXList [bareText "not",  toSExp p]+  toSExp (SPEq    x y) = SXList [bareText "=",  toSExp x, toSExp y]+  toSExp (SPLEq   x y) = SXList [bareText "<=", toSExp x, toSExp y]+  toSExp (SPGEq   x y) = SXList [bareText ">=", toSExp x, toSExp y]+  toSExp (SPLt    x y) = SXList [bareText "<",  toSExp x, toSExp y]+  toSExp (SPGt    x y) = SXList [bareText "<",  toSExp x, toSExp y]++-- | Arithmetic terms+data SallyArith = SAAdd   SallyExpr SallyExpr  -- ^ addition+                | SAMult  SallyExpr SallyExpr  -- ^ constant mult+                | SADiv   SallyExpr SallyExpr  -- ^ constant division+                | SAExpr  SallyExpr            -- ^ general expression+  deriving (Show, Eq)++instance ToSExp SallyArith where+  toSExp (SAAdd x y)  = SXList [bareText "+", toSExp x, toSExp y]+  toSExp (SAMult x y) = SXList [bareText "*", toSExp x, toSExp y]+  toSExp (SADiv x y)  = SXList [bareText "/", toSExp x, toSExp y]+  toSExp (SAExpr e)   = toSExp e+++-- Compound Sally Types --------------------------------------------------------++-- | The state type in Sally+--+-- This consists of 1) a name for the type, 2) a set of state variables (and+-- their associated base type) and, 3) (optionally) a set in input variabels+-- which are uninterpreted in the model; they can be thought of as varying+-- non-deterministically in any system trace.+data SallyState = SallyState+  { sName   :: Name                     -- ^ state type name+  , sVars   :: [(Name, SallyBaseType)]  -- ^ state variables+  , sInVars :: [(Name, SallyBaseType)]  -- ^ state input variables+  }+  deriving (Show, Eq)++instance ToSExp SallyState where+  toSExp SallyState {sName=sn, sVars=sv, sInVars=siv} =+    SXList $ [ bareText "define-state-type"+             , toSExp sn+             , SXList $ map (\(n,t) -> SXList [toSExp n, toSExp t]) sv+             ] +++             (if null siv then []+              else [SXList $ map (\(n,t) -> SXList [toSExp n, toSExp t]) siv])++-- | A named formula over a state type+data SallyStateFormula = SallyStateFormula+  { sfName   :: Name        -- ^ state formula name+  , sfDomain :: Name        -- ^ state formula domain+  , sfPred   :: SallyPred   -- ^ state formula predicate+  }+  deriving (Show, Eq)++instance ToSExp SallyStateFormula where+  toSExp SallyStateFormula {sfName=sn, sfDomain=sd, sfPred=sp} =+    SXList [ bareText "define-states"+           , toSExp sn+           , toSExp sd+           , toSExp sp+           ]++-- | A "let" binding: each let binds a 'SallyVar' to a Sally expression,+-- which can be a constant literal, a predicate (boolean value), or an+-- arithmetic expression.+type SallyLet = (SallyVar, SallyExpr)++-- | A transition over a given state type+data SallyTransition = SallyTransition+  { traName :: Name        -- ^ transition name+  , traDom  :: Name        -- ^ transition domain+  , traLet  :: [SallyLet]  -- ^ bindings for the transition relation+  , traPred :: SallyPred   -- ^ transition relation+  }+  deriving (Show, Eq)++instance ToSExp SallyTransition where+  toSExp SallyTransition {traName=tn, traDom=td, traLet=tl, traPred=tp} =+      SXList $ [ bareText "define-transition"+               , toSExp tn+               , toSExp td+               ] +++               (if null listOfBinds then [toSExp tp]+                else [SXList [bareText "let", SXList listOfBinds, toSExp tp]])+    where+      listOfBinds = map (\(v,e) -> SXList [toSExp v, toSExp e]) tl++-- | A transition system declaration+data SallySystem = SallySystem+  { sysNm  :: Name  -- ^ system name+  , sysSN  :: Name  -- ^ system state name+  , sysISN :: Name  -- ^ system init state name+  , sysTN  :: Name  -- ^ system transition name+  }+  deriving (Show, Eq)++-- | Pretty print a 'SallySystem'.+instance ToSExp SallySystem where+    toSExp ss = SXList [ bareText "define-transition-system"+                       , toSExp (sysNm ss)+                       , toSExp (sysSN ss)+                       , toSExp (sysISN ss)+                       , toSExp (sysTN ss)+                       ]+++-- Translation Results ---------------------------------------------------------++-- | The result of translation, a specific form of the Sally AST.+data TrResult = TrResult+  { tresState    :: SallyState           -- ^ system state variables+  , tresFormulas :: [SallyStateFormula]  -- ^ state formulas used in transitions+                                         --   and queries+  , tresConsts   :: [SallyConst]         -- ^ declared constants+  , tresInit     :: SallyStateFormula    -- ^ initialization formula+  , tresTrans    :: [SallyTransition]    -- ^ system transitions+  , tresSystem   :: SallySystem          -- ^ system definition+  }+  deriving (Show, Eq)++-- | TrResult requires a special printer since it is not an s-expression. The+-- order of the 'vcat' items is important because Sally is sensitive to names+-- being declared before they are used in a model file.+instance Pretty TrResult where+  pretty tr = vcat [ consts_comment+                   , consts+                   , state_comment+                   , sxPretty (tresState tr)+                   ] <$$>+              vcat (formulas_comment : intersperse+                                         sallyCom+                                         (map sxPretty (tresFormulas tr))) <$$>+              -- needs to come after formulas+              vcat [ init_comment+                   , sxPretty (tresInit tr)+                   ] <$$>+              -- needs to come after state, init, and formulas+              vcat (trans_comment : intersperse+                                      sallyCom+                                      (map sxPretty (tresTrans tr))) <$$>+              -- needs to come last+              vcat (system_comment : [sxPretty (tresSystem tr)])+    where+      consts = if null (tresConsts tr) then text ";; NONE"+               else vcat (map sxPretty (tresConsts tr))+      consts_comment = sallyCom <+> text "Constants"+      state_comment  = linebreak <> sallyCom <+> text "State type"+      init_comment   = linebreak <> sallyCom <+> text "Initial State"+      formulas_comment = linebreak <> sallyCom <+> text "State Formulas"+      trans_comment  = linebreak <> sallyCom <+> text "Transitions"+      system_comment = linebreak <> sallyCom <+> text "System Definition"