language-sally 0.1.0.1 → 0.1.1.0
raw patch · 2 files changed
+30/−3 lines, 2 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ Language.Sally.Types: SallyQuery :: Name -> [SallyLet] -> SallyPred -> SallyQuery
+ Language.Sally.Types: [sqLet] :: SallyQuery -> [SallyLet]
+ Language.Sally.Types: [sqName] :: SallyQuery -> Name
+ Language.Sally.Types: [sqPred] :: SallyQuery -> SallyPred
+ Language.Sally.Types: [tresQueries] :: TrResult -> [SallyQuery]
+ Language.Sally.Types: data SallyQuery
+ Language.Sally.Types: instance GHC.Classes.Eq Language.Sally.Types.SallyQuery
+ Language.Sally.Types: instance GHC.Show.Show Language.Sally.Types.SallyQuery
+ Language.Sally.Types: instance Language.Sally.SExpPP.ToSExp Language.Sally.Types.SallyQuery
- Language.Sally.Types: TrResult :: SallyState -> [SallyStateFormula] -> [SallyConst] -> SallyStateFormula -> [SallyTransition] -> SallySystem -> TrResult
+ Language.Sally.Types: TrResult :: SallyState -> [SallyStateFormula] -> [SallyConst] -> SallyStateFormula -> [SallyTransition] -> SallySystem -> [SallyQuery] -> TrResult
Files
- language-sally.cabal +1/−1
- src/Language/Sally/Types.hs +29/−2
language-sally.cabal view
@@ -1,5 +1,5 @@ name: language-sally-version: 0.1.0.1+version: 0.1.1.0 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/Types.hs view
@@ -41,6 +41,7 @@ , SallyLet , SallyTransition(..) , SallySystem(..)+ , SallyQuery(..) , TrResult(..) ) where @@ -296,7 +297,27 @@ , toSExp (sysTN ss) ] +-- | Data structure for representing queries in Sally. A query consists of an+-- optional set of let bindings, followed by a predicate over those bindings.+data SallyQuery = SallyQuery+ { sqName :: Name -- ^ system name+ , sqLet :: [SallyLet] -- ^ let bindings+ , sqPred :: SallyPred -- ^ predicate to query+ }+ deriving (Eq, Show) +instance ToSExp SallyQuery where+ toSExp sq = SXList $ bareText "query" :+ toSExp (sqName sq) :+ (if null listOfBinds+ then [pred]+ else [SXList [ bareText "let"+ , SXList listOfBinds+ , pred ]])+ where+ pred = toSExp (sqPred sq)+ listOfBinds = map (\(v,e) -> SXList [toSExp v, toSExp e]) (sqLet sq)+ -- Translation Results --------------------------------------------------------- -- | The result of translation, a specific form of the Sally AST.@@ -308,6 +329,7 @@ , tresInit :: SallyStateFormula -- ^ initialization formula , tresTrans :: [SallyTransition] -- ^ system transitions , tresSystem :: SallySystem -- ^ system definition+ , tresQueries :: [SallyQuery] } deriving (Show, Eq) @@ -331,8 +353,12 @@ vcat (trans_comment : intersperse sallyCom (map sxPretty (tresTrans tr))) <$$>- -- needs to come last- vcat (system_comment : [sxPretty (tresSystem tr)])+ -- needs to come (almost) last+ vcat (system_comment : [sxPretty (tresSystem tr)]) <$$>+ -- queries+ vcat (queries_comment : intersperse+ sallyCom+ (map sxPretty (tresQueries tr))) where consts = if null (tresConsts tr) then text ";; NONE" else vcat (map sxPretty (tresConsts tr))@@ -342,3 +368,4 @@ formulas_comment = linebreak <> sallyCom <+> text "State Formulas" trans_comment = linebreak <> sallyCom <+> text "Transitions" system_comment = linebreak <> sallyCom <+> text "System Definition"+ queries_comment = linebreak <> sallyCom <+> text "Queries"