Simpler Name Equality

g2.cabal

@@ -162,6 +162,7 @@ library
 
  , G2.Translation
  , G2.Translation.Cabal.Cabal
+ , G2.Translation.Haskell
  other-modules: G2.Config.Config
  , G2.Config.Interface
  , G2.Config.ParseConfig
@@ -178,15 +179,14 @@ library
  , G2.Solver.ParseSMT
  , G2.Solver.SMT2
 
- , G2.Translation.Haskell
  , G2.Translation.HaskellCheck
  , G2.Translation.InjectSpecials
  , G2.Translation.Interface
  , G2.Translation.PrimInject
  , G2.Translation.TransTypes
 
  build-depends: array >= 0.5.1.1 && <= 0.5.4.0 
- , Cabal >= 2.0.1.0 && < 3.1
+ , Cabal >= 3.0 && < 3.1
  , base >= 4.8 && < 5
  , bimap == 0.3.3
  , bytestring >= 0.10.8.0 && <= 0.10.12.1
@@ -308,6 +308,8 @@ executable RewriteV
  , ghc
  , text
  , unordered-containers >= 0.2 && < 0.3
+ , directory
+ , Cabal
  default-language: Haskell2010
  ghc-options: -threaded -Wall
  -- -fprof-auto "-with-rtsopts=-p"

rewritev/Main.hs

@@ -32,8 +32,21 @@ import Control.Exception
 import Data.List
 import Data.Char
 
+import System.Directory
+import Control.Monad
+
 import ZenoSuite
 
+import Distribution.Simple.BuildToolDepends
+
+import Distribution.Types.GenericPackageDescription
+import Distribution.Types.CondTree
+import Distribution.Types.Library
+import Distribution.Types.BuildInfo
+import Distribution.PackageDescription.Parsec
+import Distribution.Verbosity
+import G2.Translation.Cabal.Cabal
+
 main :: IO ()
 main = do
  as <- getArgs
@@ -69,6 +82,7 @@ runWithArgs as = do
  Just n -> read (tail_args !! (n + 1)) :: Int
 
  proj <- guessProj src
+ proj' <- fullDirs proj
 
  -- TODO for now, total as long as there's an extra arg
  -- TODO finite variables
@@ -82,7 +96,7 @@ runWithArgs as = do
  config <- getConfig as
 
  let libs = maybeToList m_mapsrc
- (init_state, bindings) <- initialStateNoStartFunc [proj] [src] libs
+ (init_state, bindings) <- initialStateNoStartFunc (proj:proj') [src] libs
  (TranslationConfig {simpl = True, load_rewrite_rules = True}) config
 
  let rule = find (\r -> tentry == ru_name r) (rewrite_rules bindings)

src/G2/Language/Naming.hs

@@ -82,15 +82,13 @@ nameLoc :: Name -> Maybe Span
 nameLoc (Name _ _ _ s) = s
 
 -- | Allows the creation of fresh `Name`s.
-data NameGen = NameGen { max_uniq :: (HM.HashMap (T.Text, Maybe T.Text) Int)
- , dc_children :: (HM.HashMap Name [Name]) }
+newtype NameGen = NameGen { max_uniq :: Int }
  deriving (Show, Eq, Read, Typeable, Data)
 
 -- nameToStr relies on NameCleaner eliminating all '_', to preserve uniqueness
 -- | Converts a name to a string, which is useful to interact with solvers.
 nameToStr :: Name -> String
-nameToStr (Name n (Just m) i _) = T.unpack n ++ "_m_" ++ T.unpack m ++ "_" ++ show i
-nameToStr (Name n Nothing i _) = T.unpack n ++ "_n__" ++ show i
+nameToStr (Name n _ i _) = T.unpack n ++ "_n__" ++ show i
 
 -- Similar to nameToStr, but converts a name to Builder
 nameToBuilder:: Name -> TB.Builder
@@ -128,11 +126,7 @@ mkNameGen nmd =
  allNames = toList $ names nmd
  in
  NameGen {
- max_uniq = HM.fromListWith max $ map (\(Name n m i _) -> ((n, m), i + 1)) allNames
- -- (foldr (\(Name n m i _) hm -> HM.insertWith max (n, m) (i + 1) hm) 
- -- HM.empty allNames
- -- )
- , dc_children = HM.empty
+ max_uniq = foldr max 1 $ map (\(Name n m i _) -> i + 1) allNames
  }
 
 -- | Returns all @Var@ Ids in an ASTContainer
@@ -893,11 +887,8 @@ freshSeededStrings :: [T.Text] -> NameGen -> ([Name], NameGen)
 freshSeededStrings t = freshSeededNames (map (\t' -> Name t' Nothing 0 Nothing) t)
 
 freshSeededName :: Name -> NameGen -> (Name, NameGen)
-freshSeededName (Name n m _ l) (NameGen { max_uniq = hm, dc_children = chm }) =
- (Name n m i' l, NameGen hm' chm)
- where 
- i' = HM.lookupDefault 0 (n, m) hm
- hm' = HM.insert (n, m) (i' + 1) hm
+freshSeededName (Name n m _ l) (NameGen { max_uniq = hm }) =
+ (Name n m hm l, NameGen (hm + 1))
 
 freshSeededNames :: [Name] -> NameGen -> ([Name], NameGen)
 freshSeededNames [] r = ([], r)
@@ -945,32 +936,11 @@ freshVar t ngen =
 -- If this is called with different length ns's, the shorter will be the prefix
 -- of the longer
 childrenNames :: Name -> [Name] -> NameGen -> ([Name], NameGen)
-childrenNames n ns ng@(NameGen { dc_children = chm }) =
- case HM.lookup n chm of
- Just ens' -> childrenNamesExisting n ns ens' ng
- Nothing -> childrenNamesNew n ns ng-- []
-
-childrenNamesExisting :: Name -> [Name] -> [Name] -> NameGen -> ([Name], NameGen)
-childrenNamesExisting n ns ens ng =
- let
- (fns, NameGen hm chm) = freshSeededNames (drop (length ens) ns) ng
- ns' = ens ++ fns
-
- chm' = HM.insert n ns' chm
- in
- case length ns `compare` length ens of
- LT -> (take (length ns) ens, ng)
- EQ -> (ens, ng)
- GT -> (ns', NameGen hm chm')
-
-childrenNamesNew :: Name -> [Name] -> NameGen -> ([Name], NameGen)
-childrenNamesNew n ns ng =
+childrenNames n ns ng =
  let
- (fns, NameGen hm chm) = freshSeededNames ns ng
- chm' = HM.insert n fns chm
+ (fns, NameGen hm) = freshSeededNames ns ng
  in
- (fns, NameGen hm chm')
-
+ (fns, NameGen hm)
 
 -- | Allows mapping, while passing a NameGen along
 mapNG :: (a -> NameGen -> (b, NameGen)) -> [a] -> NameGen -> ([b], NameGen)

src/G2/Language/Syntax.hs

@@ -43,7 +43,7 @@ data Name = Name T.Text (Maybe T.Text) Int (Maybe Span)
 
 -- | Disregards the Span
 instance Eq Name where
- Name n m i _ == Name n' m' i' _ = n == n' && m == m' && i == i'
+ Name n _ i _ == Name n' _ i' _ = n == n' && i == i'
 
 -- | Disregards the Span
 instance Ord Name where

src/G2/Translation/Cabal/Cabal.hs

@@ -1,9 +1,13 @@
 {-# LANGUAGE CPP #-}
 
-module G2.Translation.Cabal.Cabal (cabalSrcDirs) where
+module G2.Translation.Cabal.Cabal (cabalSrcDirs, fullDirs) where
 
 import Distribution.PackageDescription
 
+import qualified Distribution.ModuleName as MN
+import G2.Translation.Haskell
+import System.FilePath
+
 #if MIN_VERSION_Cabal(2,2,0)
 import Distribution.PackageDescription.Parsec
 #else
@@ -35,4 +39,23 @@ execSrcDirs :: Executable -> [FilePath]
 execSrcDirs = buildInfoSrcDirs . buildInfo
 
 buildInfoSrcDirs :: BuildInfo -> [FilePath]
-buildInfoSrcDirs (BuildInfo { hsSourceDirs = sd }) = sd
+buildInfoSrcDirs (BuildInfo { hsSourceDirs = sd }) = sd
+
+fullDirs :: FilePath -> IO [FilePath]
+fullDirs proj = do
+ cabal <- findCabal proj
+ let cab = case cabal of
+ Just c -> proj </> c
+ Nothing -> error "No Cabal"
+ gpd <- readGenericPackageDescription silent cab
+ let cn = case condLibrary gpd of
+ Just c -> c
+ Nothing -> error "No Library"
+ libs = foldr (\l acc -> l:acc) [] cn
+ modules = concat $ map exposedModules libs
+ sources = concat $ map (hsSourceDirs . libBuildInfo) libs
+ others = concat $ map (otherModules . libBuildInfo) libs
+ paths = sources ++ (map MN.toFilePath $
+ (exposedModules $ condTreeData cn) ++ modules ++ others ++
+ (otherModules $ libBuildInfo $ condTreeData cn))
+ return $ map (proj </>) paths