packages feed

aterm-utils (empty) → 0.1.0.0

raw patch · 7 files changed

+569/−0 lines, 7 filesdep +atermdep +aterm-utilsdep +basesetup-changed

Dependencies added: aterm, aterm-utils, base, transformers, wl-pprint

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2012, Galois, Inc++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Jason Dagit nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ aterm-utils.cabal view
@@ -0,0 +1,49 @@+name:                aterm-utils+version:             0.1.0.0+synopsis:            Utility functions for working with aterms as generated by Minitermite+-- description:         +license:             BSD3+license-file:        LICENSE+author:              Jason Dagit+maintainer:          dagit@galois.com+copyright:           (c) 2012 Galois, Inc +category:            Language+build-type:          Simple+cabal-version:       >=1.8+homepage:            https://github.com/GaloisInc/aterm-utils++executable ppaterm+  hs-source-dirs:    src+  Main-is:           PPATerm.hs++  Build-depends:       base < 5+                     , aterm+                     , aterm-utils+                     , transformers+                     , wl-pprint++  ghc-options: -O2 -Wall+  if impl(ghc >= 7.0.1)+    ghc-prof-options: -rtsopts+  ghc-prof-options: -prof -auto-all -caf-all++library++  exposed-modules:   ATerm.Utilities+                   , ATerm.Matching+                   , ATerm.Pretty++  Build-depends:       base < 5+                     , aterm+                     , transformers+                     , wl-pprint++  hs-source-dirs:      src+  ghc-options: -O2 -Wall+  if impl(ghc >= 7.0.1)+    ghc-prof-options: -rtsopts+  ghc-prof-options: -prof -auto-all -caf-all++source-repository head+  type:     git+  location: git://github.com/GaloisInc/aterm-utils.git
+ src/ATerm/Matching.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE PatternGuards #-}+module ATerm.Matching+( -- * Types+  Binding(..)+-- * Combinators+, exactlyS+, exactlyI+, exactlyL+, exactlyA+, exactlyNamed+, contains+, containsL+, containsA+, containsChildren+, bindT+, bindL+, bindI+, bindS+, bindA+) where++import ATerm.AbstractSyntax+import qualified ATerm.Utilities as U+import Control.Monad -- For MonadPlus++-- | Binding type gives you back the parts of the ATerm that+-- that match.+data Binding = BoundTerm Int     -- ^ The index into the ATermTable of the matching ATerm+             | BoundList [Int]   -- ^ The list of indexes into the ATermTable that match+             | BoundInt  Integer -- ^ The matching Integer+             | BoundStr  String  -- ^ The matching String+             | BoundAppl Int     -- ^ The index into the ATermTable for the ShAAppl term+  deriving (Eq, Read, Show, Ord)++-- | Turns anything with an Eq instance into a+-- matcher by using (==). No binding is generated.+exactly :: (MonadPlus m, Eq a) => a -> a -> m ()+exactly a b = guard (a == b) >> return ()++-- * ATermMatcher Combinators++---------------------------------------------------------------------+-- ** Exact matchers, no binding generated when they match+---------------------------------------------------------------------++-- | Matches exactly the string 's' within the ATerm+exactlyS :: MonadPlus m => String -> ATermTable -> m ()+exactlyS s t = case getATerm t of+  ShAAppl s' [] _ -> exactly s s'+  _               -> mzero++-- | Matches exactly the integer 'i' within the ATerm+exactlyI :: MonadPlus m => Integer -> ATermTable -> m ()+exactlyI i t = case getATerm t of+  ShAInt i' _ -> exactly i i'+  _           -> mzero++-- | Matches exactly the list 'xs' within the ATerm+exactlyL :: MonadPlus m => [ATermTable -> m a] -> ATermTable -> m [a]+exactlyL ms t = case getATerm t of+  ShAList ls _ -> do+    _ <- guard (length ms == length ls)+    sequence (zipWith (\m i -> m (getATermByIndex1 i t)) ms ls)+  _ -> mzero++-- | Matches the string exactly+exactlyA :: MonadPlus m => String -> [ATermTable -> m a] -> ATermTable -> m [a]+exactlyA s ms t = case getATerm t of+  ShAAppl s' ls _ -> do+    _ <- exactly s s'+    _ <- guard (length ms == length ls)+    sequence (zipWith (\m i -> U.app m t i) ms ls)+  _ -> mzero++-- | Looks for an Appl with name 's' and any children+exactlyNamed :: MonadPlus m => String -> ATermTable -> m ()+exactlyNamed s t = case getATerm t of+  ShAAppl s' _ _ -> do+    _ <- exactly s s'+    return ()+  _ -> mzero++---------------------------------------------------------------------+-- ** Partial matchers, ie., they just specify part of the structure+---------------------------------------------------------------------++containsChildren :: Monad m+                 => m (ATermTable -> b) -> m Int -> ATermTable -> m b+containsChildren ms is t = do+  i <- is+  m <- ms+  return (m (getATermByIndex1 i t))++-- | Matches a partial specification against the children. The+-- matching is maximised so that if the pattern occurs more than+-- once it is matched each time it appears.+contains :: [ATermTable -> a] -> ATermTable -> [a]+contains ms t = case getATerm t of+  ShAAppl _ ls _ -> containsChildren ms ls t+  ShAList   ls _ -> containsChildren ms ls t+  _              -> mzero++-- | Matches a partial specification of a sub aterm List. The+-- matching is maximised so that if the pattern occurs more than+-- once it is matched each time it appears.+containsL :: [ATermTable -> a] -> ATermTable -> [a]+containsL ms t = case getATerm t of+  ShAList ls _ -> containsChildren ms ls t+  _            -> mzero++-- | Matches a partial specification of an Appl. The matching is+-- maximised so that if the pattern occurs more than once it is match+-- each time it appears.+containsA :: String -> [ATermTable -> a] -> ATermTable -> [a]+containsA s ams t = case getATerm t of+  ShAAppl s' ls _ -> do+    _ <- exactly s s'+    containsChildren ams ls t+  _               -> mzero++---------------------------------------------------------------------+-- ** Wildcard matchers, these create bindings when they match+---------------------------------------------------------------------++-- | Matches any ATerm and generates a binding to that term+bindT :: MonadPlus m => ATermTable -> m Binding+bindT t = return (BoundTerm (getTopIndex t))+  +-- | Matches any list and generates a binding to that list+bindL :: MonadPlus m => ATermTable -> m Binding+bindL t = case getATerm t of+  ShAList ls _ -> return (BoundList ls)+  _            -> mzero++-- | Matches any integer and generates a binding to that integer+bindI :: MonadPlus m => ATermTable -> m Binding+bindI t = case getATerm t of+  ShAInt i _ -> return (BoundInt i)+  _          -> mzero++-- | Matches any string and generates a binding to that string+-- Strings have the form (Appl somestring [] []).+-- Not to be confused with matching the the string part of an Appl.+bindS :: MonadPlus m => ATermTable -> m Binding+bindS t = case getATerm t of+  ShAAppl s [] [] -> return (BoundStr s)+  _               -> mzero++-- | Matches any Appl and generates a binding to that Appl+bindA :: MonadPlus m => ATermTable -> m Binding+bindA t = case getATerm t of+  ShAAppl _ _ _ -> return (BoundAppl (getTopIndex t))+  _             -> mzero
+ src/ATerm/Pretty.hs view
@@ -0,0 +1,41 @@+module ATerm.Pretty+(+  ppATerm+)+where++import Text.PrettyPrint.Leijen+import ATerm.AbstractSyntax++ppATerm :: ATermTable -> Doc+ppATerm t = case getATerm t of+  ShAAppl s [] [] -> text s -- this will already have double quotes in this case+  ShAAppl s is _  -> nestAppl t s is+  ShAList   is _  -> nestList t is+  ShAInt  i    _  -> integer i++ppAList :: ATermTable -> [Int] -> [Doc]+ppAList t is = map (\i -> ppATerm (getATermByIndex1 i t)) is++nestList :: ATermTable -> [Int] -> Doc+nestList t is = children ds+  where+  children []  = lbracket <> rbracket+  children [d] = lbracket <> d <> rbracket+  children _   =+    lbracket                                                          <$>+      indent 2 (align (cat (zipWith (<>) (empty : repeat comma) ds))) <$>+    rbracket+  ds = ppAList t is+++nestAppl :: ATermTable -> String -> [Int] -> Doc+nestAppl t s is = children ds+  where+  children []  = text s <> lparen <> rparen+  children [d] = text s <> lparen <> d <> rparen+  children _   = text s <>+    lparen                                                               <$>+      indent 2 (align (cat (zipWith (<>) (text " " : repeat comma) ds))) <$>+    (indent 1 rparen)+  ds = ppAList t is
+ src/ATerm/Utilities.hs view
@@ -0,0 +1,240 @@+{-# LANGUAGE PatternGuards #-}+-- | Functions for working with the ATerms that ROSE produces.+module ATerm.Utilities+( -- * Utility functions+  app             -- (ATermTable -> a) -> ATermTable -> Int -> a+, foldr           -- (ATermTable -> a -> a) -> a -> ATermTable -> a+, foldl           -- (a -> ATermTable -> a) -> a -> ATermTable -> a+, foldl'          -- (a -> ATermTable -> a) -> a -> ATermTable -> a+, foldM           -- (a -> ATermTable -> m a) -> a -> ATermTable -> m a+, mapM            -- (ATermTable -> m b) -> ATermTable -> m [b]+, mapM_           -- (ATermTable -> m b) -> ATermTable -> m ()+, map             -- (ATermTable -> a) -> ATermTable -> [a]+, concatMap       -- (ATermTable -> [a]) -> ATermTable -> [a]+-- * Check Monad+, CheckM+, appM            -- (ATermTable -> a) -> Int -> CheckM log state m a+, currentTerm     -- CheckM log state m ATermTable+, withCurrentTerm -- ATermTable -> CheckM log state m a -> CheckM log state m a+, childrenM       -- CheckM log state m [Int]+, satisfy         -- (ATermTable -> Bool) -> CheckM log st m a -> CheckM log st m (Maybe a)+, inSubtree       -- CheckM log state m a -> CheckM log state m [[a]]+, inSubtree_      -- CheckM log state m a -> CheckM log state m ()+, everywhere      -- CheckM log state m a -> CheckM log state m [a]+, everywhere_     -- CheckM log state m a -> CheckM log state m ()+-- * Extractions+, extractString   -- ATermTable -> Maybe String+, extractInteger  -- ATermTable -> Maybe Integer+, extractFileInfo -- ATermTable -> Maybe (String, Integer, Integer)+, isNamed         -- String -> ATermTable -> Bool+, showATerm       -- ATermTable -> String+, children        -- ATermTable -> [Int]+-- * Read and write+, readATerm+, writeSharedATerm+-- * Misc+, getATermFromTable+) where++import ATerm.ReadWrite+import ATerm.SimpPretty+import ATerm.AbstractSyntax++import Control.Monad.Trans.RWS.Strict+import Control.Monad ( liftM )+import qualified Control.Monad as M+import Data.Monoid++import qualified Data.List as L ( foldl' )+import Prelude hiding (foldr, foldl, map, mapM_, mapM, concatMap)+import qualified Prelude as P++---------------------------------------------------------------------+-- Working with ATerms (eg., ATermTable)+---------------------------------------------------------------------++-- | Turns a normal function of ATermTable into a function that+-- works on the hash value instead.+app :: (ATermTable -> a) -> ATermTable -> Int -> a+app f t i = f (getATermByIndex1 i t)++-- | Standard foldr, but for ATermTables+foldr :: (ATermTable -> a -> a) -> a -> ATermTable -> a+foldr k z at = go at+  where+  go t = t `k` P.foldr k' z (children t)+  k' i acc = app (foldr k acc) at i++-- | Standard foldl, but for ATermTables+foldl :: (a -> ATermTable -> a) -> a -> ATermTable -> a+foldl k z at = go at+  where+  go t = k (P.foldl k' z (children t)) t+  k' acc i = app (foldl k acc) at i++-- | Standard foldl', but for ATermTables+foldl' :: (a -> ATermTable -> a) -> a -> ATermTable -> a+foldl' k z at = go at+  where+  go t = let z' = L.foldl' k' z (children t) in z' `seq` k z' t+  k' acc i = app (foldl' k acc) at i++-- | Standard foldM, but for ATermTables+foldM :: (Monad m) => (a -> ATermTable -> m a) -> a -> ATermTable -> m a+foldM k z at = go at+  where+  go t = k z t >>= \a -> M.foldM k' a (children t)+  k' acc i = app (foldM k acc) at i++-- | Standard mapM, but for ATermTables+mapM :: (Monad m) => (ATermTable -> m b) -> ATermTable -> m [b]+mapM f = foldM action []+  where+  action acc x = do+    x' <- f x+    return (x' : acc)++-- | Standard mapM_, but for ATermTables+mapM_ :: (Monad m) => (ATermTable -> m b) -> ATermTable -> m ()+mapM_ f = foldM action ()+  where+  action _ x = do+    _ <- f x+    return ()++-- | Standard map, but for ATermTables+map :: (ATermTable -> a) -> ATermTable -> [a]+map f at = foldr ((:) . f) [] at++-- | Standard concatMap, but for ATermTables+concatMap :: (ATermTable -> [a]) -> ATermTable -> [a]+concatMap f at = foldr ((++) . f) [] at++---------------------------------------------------------------------+-- Checker Monad+---------------------------------------------------------------------++-- | The checker monad. For now the environment is the current ATerm, in the+-- future we may also store the path from the root to the current ATerm, so use+-- 'currentTerm' instead of ask to get the current ATerm+type CheckM log state m a = RWST ATermTable log state m a++-- | Like 'app' but lifts the result into the CheckM monad+appM :: (Monoid log, Monad m) => (ATermTable -> a) -> Int -> CheckM log state m a+appM f i = do+  t <- currentTerm+  return (f (getATermByIndex1 i t))++-- | Use this instead of 'ask' so that we can refactor+-- the environment later without impacting existing code.+currentTerm :: (Monoid log, Monad m) => CheckM log state m ATermTable+currentTerm = ask++-- | Use this instead of 'local' so that we can refactor+-- the environment later without impacting existing code.+withCurrentTerm :: (Monoid log, Monad m)+                => ATermTable -> CheckM log state m a -> CheckM log state m a+withCurrentTerm t = local (const t)++-- | Return the hashes of the current term's children into the monad+childrenM :: (Monad m, Monoid log) => CheckM log state m [Int]+childrenM = children `liftM` currentTerm++-- | Use this when the current node must satisfy a specific property.+-- Note: Using Maybe here is a bit of a hack. Refactor to support MonadPlus style guards?+satisfy :: (Monad m, Monoid log)+        => (ATermTable -> Bool) -> CheckM log st m a -> CheckM log st m (Maybe a)+satisfy p m = do+  t <- currentTerm+  case p t of+    True  -> Just `liftM` m+    False -> return Nothing++-- | Applies a traversal in a subtree of the current ATerm. Differs from 'everywhere'+-- in that it does not apply the traversal to the current term (only its children and+-- their children).+inSubtree :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m [[a]]+inSubtree c = do+  ks <- childrenM+  at <- currentTerm+  let kids = P.map (`getATermByIndex1` at) ks+  P.mapM (`withCurrentTerm` (everywhere c)) kids++-- Like 'inSubtree_' but throws away the result.+inSubtree_ :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m ()+inSubtree_ c = do+  ks <- childrenM+  at <- currentTerm+  let kids = P.map (`getATermByIndex1` at) ks+  P.mapM_ (`withCurrentTerm` (everywhere c)) kids++-- | Applies a traversal over the tree defined by the current node (including root node).+everywhere :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m [a]+everywhere c = currentTerm >>= mapM (\at -> withCurrentTerm at c)++-- | Like 'everywhere' but throws away the result.+everywhere_ :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m ()+everywhere_ c = currentTerm >>= mapM_ (\at -> withCurrentTerm at c)++{-+-- Left here as a lesson: This doesn't seem to do the intended thing+everywhere' :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m [a]+everywhere' c = currentTerm >>= mapM (const c)+-}++---------------------------------------------------------------------+-- Turn ATerms into normal values, we make assumptions+-- about the format that ROSE emits ATerms in.+---------------------------------------------------------------------++-- | Extracts the label of Application nodes+extractString :: ATermTable -> Maybe String+extractString at =+  case getATerm at of+  ShAAppl s _ _ -> Just s+  _             -> Nothing++-- | Extract the integer of Int nodes+extractInteger :: ATermTable -> Maybe Integer+extractInteger at =+  case getATerm at of+  ShAInt i _ -> Just i+  _          -> Nothing++-- | Extracts the filename, line number, and colunm number from+-- file_info nodes.+extractFileInfo :: ATermTable -> Maybe (String, Integer, Integer)+extractFileInfo at =+  case getATerm at of+  ShAAppl s [fp,line,col] _+    | s == "file_info"+    , Just f <- extractString  (getATermByIndex1 fp   at)+    , Just l <- extractInteger (getATermByIndex1 line at)+    , Just c <- extractInteger (getATermByIndex1 col  at) -> Just (f,l,c)+  _                                                       -> Nothing++-- | Equality test on the label of an Application node+isNamed :: String -> ATermTable -> Bool+isNamed name t =+  case getATerm t of+  ShAAppl s _ _ -> s == name+  _             -> False ++-- | It's not acually pretty, but that's not our fault.+showATerm :: ATermTable -> String+showATerm = render . writeSharedATermSDoc++-- | This pattern comes up in most traversals.  Simply return the stable names+-- so we don't break sharing.+children :: ATermTable -> [Int]+children t =+  case getATerm t of+  ShAAppl _ l _ -> l+  ShAList   l _ -> l+  ShAInt  _   _ -> []++---------------------------------------------------------------------+-- Misc+---------------------------------------------------------------------+getATermFromTable :: ATermTable -> Int -> ATermTable+getATermFromTable = flip getATermByIndex1
+ src/PPATerm.hs view
@@ -0,0 +1,54 @@+module Main where++import System.Console.GetOpt+import System.Environment ( getArgs )++import Control.Applicative+import Control.Monad ( when )+import Data.List ( foldl', isSuffixOf )++-- Project specific imports+import ATerm.Pretty ( ppATerm )+import qualified ATerm.Utilities as U++---------------------------------------------------------------------+-- Command Line options+---------------------------------------------------------------------+data Options = Options+  { optSource :: Maybe FilePath -- ^ Nothing means read from stdin+                                --   otherwise read this file+  }+  deriving (Read, Show, Eq)++options :: [ OptDescr (Options -> Options) ]+options =+  [ Option "s" ["source"]+      (ReqArg (\arg opt -> opt { optSource = Just arg }) "FILE")+      "ATerm file to pretty print"+  ]++defaultOptions :: Options+defaultOptions = Options { optSource = Nothing }++header :: String+header = unlines+  [ "usage: [-s FILE]"+  , "  If no file is given, input is taken from stdin"+  ]++---------------------------------------------------------------------+-- Main program+---------------------------------------------------------------------+main :: IO ()+main = do+  args <- getArgs+  let (flags, _, errors) = getOpt RequireOrder options args+      opts = foldl' (.) id flags defaultOptions+  when (not (null errors)) $ error (concat errors ++ usageInfo header options)+  cs <- removeTrailingDot <$> maybe getContents readFile (optSource opts)+  let aterms = U.readATerm cs+  print (ppATerm aterms)+  where+  removeTrailingDot s+    | length s >= 2 && ".\n" `isSuffixOf` s = init (init s)+    | otherwise = s