fix compilation issues

.gitignore

@@ -1,16 +1,16 @@
 # generated code
-src/Lex.hs
-src/Parse.hs
-src/dist-newstyle
+src/Act/Lex.hs
+src/Act/Parse.hs
+dist-newstyle/
 tests/**/*.out
 
 # build results
 bin/
 result*
 
 # cabal
-**/*.cabal.local
-**/cabal.project.local*
+*.cabal.local
+cabal.project.local*
 src/dist/
 
 # coq

Makefile

@@ -1,20 +1,20 @@
 .DEFAULT_GOAL := compiler
 .PHONY: parser compiler docs
 
-parser: src/Lex.hs src/Parse.hs
+parser: src/Act/Lex.hs src/Act/Parse.hs
 
-src/Parse.hs: src/Parse.y src/Syntax/Untyped.hs
-	happy src/Parse.y
+src/Act/Parse.hs: src/Act/Parse.y src/Act/Syntax/Untyped.hs
+	happy src/Act/Parse.y
 
-src/Lex.hs: src/Lex.x
-	alex src/Lex.x
+src/Act/Lex.hs: src/Act/Lex.x
+	alex src/Act/Lex.x
 
 # builds the rest of the haskell files (compiler)
-bin/act: src/*.hs src/*/*.hs
-	cd src && cabal v2-install --installdir=../bin --overwrite-policy=always && cd ..
+bin/act: src/CLI/*.hs src/Act/*.hs
+	cabal v2-install --installdir=bin --overwrite-policy=always
 
-repl: src/Lex.hs src/Parse.hs
-	cd src && cabal v2-repl
+repl: src/Act/Lex.hs src/Act/Parse.hs
+	cabal v2-repl
 
 compiler: bin/act
 

act.cabal

@@ -11,6 +11,8 @@ flag ci
     manual:      True
 
 common deps
+  default-extensions:
+    ImportQualifiedPost
   build-depends: base               >= 4.9 && < 5,
                  aeson              >= 1.0,
                  containers         >= 0.5,
@@ -41,15 +43,33 @@ common deps
 library
   import:             deps
   build-tool-depends: happy:happy, alex:alex
-  hs-source-dirs:     .
+  hs-source-dirs:     src
   default-language:   Haskell2010
-  exposed-modules:    CLI Error Print SMT Syntax.Annotated Syntax.TimeAgnostic
-  other-modules:      Lex Parse Coq Syntax Syntax.Untyped Syntax.Typed Syntax.Types Syntax.Timing Type Enrich Dev HEVM Consistency
+  exposed-modules:
+    Act.CLI
+    Act.Error
+    Act.Print
+    Act.SMT
+    Act.Syntax.Annotated
+    Act.Syntax.TimeAgnostic
+    Act.Lex
+    Act.Parse
+    Act.Coq
+    Act.Syntax
+    Act.Syntax.Untyped
+    Act.Syntax.Typed
+    Act.Syntax.Types
+    Act.Syntax.Timing
+    Act.Type
+    Act.Enrich
+    Act.Dev
+    Act.HEVM
+    Act.Consistency
 
 executable act
   import:             deps
   main-is:            Main.hs
-  hs-source-dirs:     main
+  hs-source-dirs:     src/CLI
   default-language:   Haskell2010
   build-depends:      act
   if os(darwin)
@@ -59,8 +79,8 @@ Test-Suite test
   import:           deps
   type:             exitcode-stdio-1.0
   default-language: Haskell2010
-  main-is:          Test.hs
-  hs-source-dirs:   test
+  main-is:          Main.hs
+  hs-source-dirs:   src/Test
   build-depends:    act,
                     pretty-simple          >= 2.2,
                     quickcheck-instances   >= 0.3,

src/Act/hie.yaml → hie.yaml

@@ -1,8 +1,8 @@
 cradle:
   cabal:
-    - path: "."
+    - path: "src/Act"
       component: "lib:act"
-    - path: "./Main.hs"
+    - path: "src/CLI"
       component: "exe:act"
-    - path: "./test"
+    - path: "src/test"
       component: "test:test"

src/Act/CLI.hs

@@ -10,7 +10,7 @@
 {-# LANGUAGE ApplicativeDo #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
-module CLI (main, compile, proceed) where
+module Act.CLI (main, compile, proceed) where
 
 import Data.Aeson hiding (Bool, Number, json)
 import GHC.Generics
@@ -24,26 +24,27 @@ import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
 import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import GHC.Natural
+import Options.Generic
 
 
 import qualified Data.ByteString.Lazy.Char8 as B
 import qualified Data.ByteString as BS
+import Data.ByteString (ByteString)
 
 import Control.Monad
 import Control.Lens.Getter
 
-import Error
-import Lex (lexer, AlexPosn(..))
-import Options.Generic
-import Parse
-import Syntax.Annotated
-import Enrich
-import SMT
-import Type
-import Coq hiding (indent)
-import HEVM
-import Consistency
-import Print
+import Act.Error
+import Act.Lex (lexer, AlexPosn(..))
+import Act.Parse
+import Act.Syntax.Annotated
+import Act.Enrich
+import Act.SMT as SMT
+import Act.Type
+import Act.Coq hiding (indent)
+import Act.HEVM
+import Act.Consistency
+import Act.Print
 
 import EVM.SymExec
 import qualified EVM.Solvers as Solvers
@@ -203,7 +204,7 @@ coq' :: FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
 coq' f solver' smttimeout' debug' = do
   contents <- readFile f
   proceed contents (enrich <$> compile contents) $ \claims -> do
-    checkCases claims solver' smttimeout' debug' 
+    checkCases claims solver' smttimeout' debug'
     TIO.putStr $ coq claims
 
 

src/Act/Consistency.hs

@@ -6,7 +6,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# Language RecordWildCards #-}
 
-module Consistency (
+module Act.Consistency (
   checkCases
 ) where
 
@@ -18,11 +18,11 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import System.Exit (exitFailure)
 import Data.Maybe
 
-import Syntax
-import Syntax.Annotated
-import SMT
-import Syntax.Untyped (makeIface)
-import Print
+import Act.Syntax
+import Act.Syntax.Annotated
+import Act.SMT as SMT
+import Act.Syntax.Untyped (makeIface)
+import Act.Print
 
 import qualified EVM.Solvers as Solvers
 

src/Act/Coq.hs

@@ -15,7 +15,7 @@
 {-# Language DataKinds #-}
 
 
-module Coq where
+module Act.Coq where
 
 import Prelude hiding (GT, LT)
 
@@ -27,8 +27,8 @@ import Data.List (groupBy)
 import Control.Monad.State
 
 import EVM.ABI
-import Syntax
-import Syntax.Annotated
+import Act.Syntax
+import Act.Syntax.Annotated
 
 type Fresh = State Int
 

src/Act/Dev.hs

@@ -1,10 +1,10 @@
-module Dev where
+module Act.Dev where
 
 
-import CLI
-import Coq (coq)
-import Enrich
-import Consistency
+import Act.CLI
+import Act.Coq (coq)
+import Act.Enrich
+import Act.Consistency
 import qualified EVM.Solvers as Solvers
 
 import qualified Data.Text as T

src/Act/Enrich.hs

@@ -1,14 +1,14 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE DataKinds #-}
 
-module Enrich (enrich, mkStorageBounds) where
+module Act.Enrich (enrich, mkStorageBounds) where
 
 import Data.Maybe
 import Data.List (nub)
 
-import Syntax
-import Syntax.Annotated
-import Type (defaultStore)
+import Act.Syntax
+import Act.Syntax.Annotated
+import Act.Type (defaultStore)
 
 -- | Adds extra preconditions to non constructor behaviours based on the types of their variables
 enrich :: Act -> Act

src/Act/Error.hs

@@ -1,7 +1,4 @@
 {-# LANGUAGE OverloadedLists #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
@@ -16,16 +13,16 @@ and keep track of a 'Pn' for every error it logs. There is also some infrastruct
 around modified chaining/branching behaviours.
 -}
 
-module Error (module Error) where
+module Act.Error (module Act.Error) where
 
 import Data.List (find)
 import Data.List.NonEmpty as NE
-import Data.Validation as Error
+import Data.Validation as Act.Error
 
-import Syntax.Untyped (Pn)
+import Act.Syntax.Untyped (Pn)
 
 -- Reexport NonEmpty so that we can use `-XOverloadedLists` without thinking.
-import Data.List.NonEmpty as Error (NonEmpty)
+import Data.List.NonEmpty as Act.Error (NonEmpty)
 
 type Error e = Validation (NonEmpty (Pn,e))
 
@@ -37,7 +34,7 @@ assert err b = if b then pure () else throw err
 
 foldValidation :: (b -> a -> Error err b) -> b -> [a] -> Error err b
 foldValidation _ b [] = pure b
-foldValidation f b (a:as) = f b a `bindValidation` \b' -> foldValidation f b' as 
+foldValidation f b (a:as) = f b a `bindValidation` \b' -> foldValidation f b' as
 
 infixr 1 <==<, >==>
 

src/Act/HEVM.hs

@@ -13,7 +13,7 @@
 {-# LANGUAGE OverloadedRecordDot #-}
 
 
-module HEVM where
+module Act.HEVM where
 
 import qualified Data.Map as M
 import Data.List
@@ -23,6 +23,7 @@ import qualified Data.Text.IO as TIO
 import qualified Data.Text.Lazy.IO as TL
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as B8 (pack)
+import Data.ByteString (ByteString)
 import Data.Text.Encoding (encodeUtf8)
 import Control.Concurrent.Async
 import Control.Monad
@@ -31,9 +32,9 @@ import Data.Maybe
 import System.Exit ( exitFailure )
 import Control.Monad.ST (stToIO)
 
-import Syntax.Annotated
-import Syntax.Untyped (makeIface)
-import Syntax
+import Act.Syntax.Annotated as Act
+import Act.Syntax.Untyped (makeIface)
+import Act.Syntax
 
 import EVM.ABI (Sig(..))
 import qualified EVM.Types as EVM hiding (Contract(..), FrameState(..))
@@ -265,10 +266,10 @@ toProp layout = \case
   (Or _ e1 e2) -> pop2 EVM.POr e1 e2
   (Impl _ e1 e2) -> pop2 EVM.PImpl e1 e2
   (Neg _ e1) -> EVM.PNeg (toProp layout e1)
-  (Syntax.Annotated.LT _ e1 e2) -> op2 EVM.PLT e1 e2
+  (Act.LT _ e1 e2) -> op2 EVM.PLT e1 e2
   (LEQ _ e1 e2) -> op2 EVM.PLEq e1 e2
   (GEQ _ e1 e2) -> op2 EVM.PGEq e1 e2
-  (Syntax.Annotated.GT _ e1 e2) -> op2 EVM.PGT e1 e2
+  (Act.GT _ e1 e2) -> op2 EVM.PGT e1 e2
   (LitBool _ b) -> EVM.PBool b
   (Eq _ SInteger e1 e2) -> op2 EVM.PEq e1 e2
   (Eq _ SBoolean e1 e2) -> op2 EVM.PEq e1 e2
@@ -296,10 +297,10 @@ toExpr layout = \case
   (Or _ e1 e2) -> op2 EVM.Or e1 e2
   (Impl _ e1 e2) -> op2 (\x y -> EVM.Or (EVM.Not x) y) e1 e2
   (Neg _ e1) -> EVM.Not (toExpr layout e1)
-  (Syntax.Annotated.LT _ e1 e2) -> op2 EVM.LT e1 e2
+  (Act.LT _ e1 e2) -> op2 EVM.LT e1 e2
   (LEQ _ e1 e2) -> op2 EVM.LEq e1 e2
   (GEQ _ e1 e2) -> op2 EVM.GEq e1 e2
-  (Syntax.Annotated.GT _ e1 e2) -> op2 EVM.GT e1 e2
+  (Act.GT _ e1 e2) -> op2 EVM.GT e1 e2
   (LitBool _ b) -> EVM.Lit (fromIntegral $ fromEnum $ b)
   -- integers
   (Add _ e1 e2) -> op2 EVM.Add e1 e2

src/Act/Lex.x

@@ -1,5 +1,5 @@
 {
-module Lex
+module Act.Lex
   ( LEX (..)
   , Lexeme (..)
   , AlexPosn (..)
@@ -98,9 +98,9 @@ tokens :-
   ")"                                   { mk RPAREN }
   "["                                   { mk LBRACK }
   "]"                                   { mk RBRACK }
-  "="                                   { mk Lex.EQ }
-  ">"                                   { mk Lex.GT }
-  "<"                                   { mk Lex.LT }
+  "="                                   { mk Act.Lex.EQ }
+  ">"                                   { mk Act.Lex.GT }
+  "<"                                   { mk Act.Lex.LT }
   ":"                                   { mk COLON }
   "+"                                   { mk PLUS }
   "-"                                   { mk MINUS }

src/Act/Parse.y

@@ -1,12 +1,12 @@
 {
-module Parse (module Parse, showposn) where
+module Act.Parse (module Act.Parse, showposn) where
 import Prelude hiding (EQ, GT, LT)
-import Lex
+import Data.Validation
 import EVM.ABI
 import qualified Data.List.NonEmpty as NonEmpty
-import Syntax.Untyped
-import Error
-import Data.Validation
+import Act.Lex
+import Act.Syntax.Untyped
+import Act.Error
 }
 
 %name parse