diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for language-sally + +## 0.1.0.0 -- 2017-06-02 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/language-sally.cabal b/language-sally.cabal new file mode 100644 --- /dev/null +++ b/language-sally.cabal @@ -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 + 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 diff --git a/src/Language/Sally.hs b/src/Language/Sally.hs new file mode 100644 --- /dev/null +++ b/src/Language/Sally.hs @@ -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 diff --git a/src/Language/Sally/Expr.hs b/src/Language/Sally/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Language/Sally/Expr.hs @@ -0,0 +1,357 @@ +-- | +-- Module : Language.Sally.Expr +-- Description : Smart constructors for Sally AST types +-- Copyright : Benjamin Jones 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 diff --git a/src/Language/Sally/PPrint.hs b/src/Language/Sally/PPrint.hs new file mode 100644 --- /dev/null +++ b/src/Language/Sally/PPrint.hs @@ -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 diff --git a/src/Language/Sally/SExpPP.hs b/src/Language/Sally/SExpPP.hs new file mode 100644 --- /dev/null +++ b/src/Language/Sally/SExpPP.hs @@ -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 ";;" diff --git a/src/Language/Sally/Types.hs b/src/Language/Sally/Types.hs new file mode 100644 --- /dev/null +++ b/src/Language/Sally/Types.hs @@ -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"