Feature/repl step n (#501)

runtimeverification · Mar 12, 2019 · 1488993 · 1488993
1 parent 7c8fbfb
commit 1488993
Show file tree

Hide file tree

Showing 39 changed files with 1,107 additions and 368 deletions.
diff --git a/include.mk b/include.mk
@@ -21,6 +21,7 @@ KPROVE = $(K_DIST_BIN)/kprove
 KOMPILE_OPTS = --backend haskell
 KRUN_OPTS = --haskell-backend-command "$(KORE_EXEC) $(KORE_EXEC_OPTS)"
 KPROVE_OPTS = --haskell-backend-command "$(KORE_EXEC) $(KORE_EXEC_OPTS)"
+KPROVE_REPL_OPTS = --haskell-backend-command "$(KORE_REPL) $(KORE_EXEC_OPTS)"
 
 HS_TOP = $(TOP)/kore
 HS_SOURCE_DIRS = $(HS_TOP)/src $(HS_TOP)/app $(HS_TOP)/test $(HS_TOP)/bench
@@ -42,5 +43,10 @@ STACK_LOCAL_HPC_ROOT ?= $(shell $(STACK_TEST) path --local-hpc-root)
 KORE_EXEC = $(STACK_LOCAL_INSTALL_ROOT)/bin/kore-exec
 KORE_EXEC_OPTS =
 
+KORE_REPL = $(STACK_LOCAL_INSTALL_ROOT)/bin/kore-repl
+
 $(KORE_EXEC):
 	$(STACK_BUILD) $(STACK_NO_PROFILE) kore:exe:kore-exec
+
+$(KORE_REPL):
+	$(STACK_BUILD) $(STACK_NO_PROFILE) kore:exe:kore-repl
diff --git a/kore/Makefile b/kore/Makefile
@@ -1,6 +1,6 @@
 package = kore
 
-stack_yaml = STACK_YAML="../../../stack.yaml"
+stack_yaml = STACK_YAML="../stack.yaml"
 stack = $(stack_yaml) stack
 pattern = ""
 
@@ -34,6 +34,10 @@ pedantic:
 ghcid:
 	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-exec"
 
+ghcid-repl:
+	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-repl"
+
+
 # TODO(Vladimir): remove 'hyperlink-source' when we upgrade from lts-12.10 (8.4.3)
 hoogle-gen:
 	$(stack) haddock; $(stack) hoogle generate --rebuild --no-haddock-hyperlink-source  -- --local

diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
@@ -1,31 +1,22 @@
 module Main (main) where
 
-import           Control.Applicative
-                 ( Alternative (..), optional, (<$) )
-import qualified Control.Lens as Lens
-import           Data.Function
-                 ( (&) )
-import           Data.List
-                 ( intercalate )
-import qualified Data.Map as Map
-import           Data.Maybe
-                 ( fromMaybe )
-import           Data.Proxy
-                 ( Proxy (..) )
-import           Data.Semigroup
-                 ( (<>) )
-import           Data.Text
-                 ( Text )
-import           Data.Text.Prettyprint.Doc.Render.Text
-                 ( hPutDoc, putDoc )
-import           Options.Applicative
-                 ( InfoMod, Parser, argument, auto, fullDesc, header, help,
-                 long, metavar, option, progDesc, readerError, str, strOption,
-                 switch, value )
-import           System.Exit
-                 ( ExitCode (..), exitWith )
-import           System.IO
-                 ( IOMode (WriteMode), withFile )
+import Control.Applicative
+       ( Alternative (..), optional, (<$) )
+import Data.List
+       ( intercalate )
+import Data.Maybe
+       ( fromMaybe )
+import Data.Semigroup
+       ( (<>) )
+import Data.Text.Prettyprint.Doc.Render.Text
+       ( hPutDoc, putDoc )
+import Options.Applicative
+       ( InfoMod, Parser, argument, auto, fullDesc, header, help, long,
+       metavar, option, progDesc, readerError, str, strOption, value )
+import System.Exit
+       ( ExitCode (..), exitWith )
+import System.IO
+       ( IOMode (WriteMode), withFile )
 
 import           Data.Limit
                  ( Limit (..) )
@@ -35,24 +26,18 @@ import           Kore.AST.Kore
 import           Kore.AST.Pure
 import           Kore.AST.Sentence
 import           Kore.AST.Valid
-import           Kore.ASTVerifier.DefinitionVerifier
-                 ( AttributesVerification (DoNotVerifyAttributes),
-                 defaultAttributesVerification,
-                 verifyAndIndexDefinitionWithBase )
 import qualified Kore.Attribute.Axiom as Attribute
-import qualified Kore.Builtin as Builtin
 import           Kore.Error
                  ( printError )
 import           Kore.Exec
 import           Kore.IndexedModule.IndexedModule
-                 ( IndexedModule (..), VerifiedModule )
+                 ( VerifiedModule )
 import           Kore.Logger.Output
                  ( KoreLogOptions (..), parseKoreLogOptions, withLogger )
 import           Kore.Parser.Parser
-                 ( parseKoreDefinition, parseKorePattern )
+                 ( parseKorePattern )
 import           Kore.Predicate.Predicate
                  ( makePredicate )
-import qualified Kore.Repl as Repl
 import           Kore.Step.Pattern
 import           Kore.Step.Representation.ExpandedPattern
                  ( CommonExpandedPattern, Predicated (..) )
@@ -74,31 +59,6 @@ Main module to run kore-exec
 TODO: add command line argument tab-completion
 -}
 
-data KoreProveOptions =
-    KoreProveOptions
-        { specFileName :: !FilePath
-        -- ^ Name of file containing the spec to be proven
-        , specMainModule :: !ModuleName
-        -- ^ The main module of the spec to be proven
-        }
-
-parseKoreProveOptions :: Parser KoreProveOptions
-parseKoreProveOptions =
-    KoreProveOptions
-    <$> strOption
-        (  metavar "SPEC_FILE"
-        <> long "prove"
-        <> help "Kore source file representing spec to be proven.\
-                \Needs --spec-module."
-        )
-    <*> (ModuleName
-        <$> strOption
-            (  metavar "SPEC_MODULE"
-            <> long "spec-module"
-            <> help "The name of the main module in the spec to be proven."
-            )
-        )
-
 
 data KoreSearchOptions =
     KoreSearchOptions
@@ -198,7 +158,6 @@ data KoreExecOptions = KoreExecOptions
     , koreLogOptions      :: !KoreLogOptions
     , koreSearchOptions   :: !(Maybe KoreSearchOptions)
     , koreProveOptions    :: !(Maybe KoreProveOptions)
-    , koreRepl            :: !Bool
     }
 
 -- | Command Line Argument Parser
@@ -247,10 +206,6 @@ parseKoreExecOptions =
         <*> parseKoreLogOptions
         <*> pure Nothing
         <*> optional parseKoreProveOptions
-        <*> switch
-            ( long "repl"
-            <> help "Enable REPL mode for prove"
-            )
     SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig
     readSMTTimeOut = do
         i <- auto
@@ -335,7 +290,6 @@ mainWithOptions
         , koreLogOptions
         , koreSearchOptions
         , koreProveOptions
-        , koreRepl
         }
   = do
         let
@@ -345,10 +299,6 @@ mainWithOptions
                     { SMT.timeOut = smtTimeOut
                     , SMT.preludeFile = smtPrelude
                     }
-            repl =
-                if koreRepl
-                    then Repl.proveClaim
-                    else const . pure $ ()
         parsedDefinition <- parseDefinition definitionFileName
         indexedDefinition@(indexedModules, _) <-
             verifyDefinitionWithBase
@@ -391,7 +341,7 @@ mainWithOptions
             clockSomethingIO "Executing"
             $ withLogger koreLogOptions (\logger ->
                 SMT.runSMT smtConfig
-                $ evalSimplifier logger repl
+                $ evalSimplifier logger
                 $ case proveParameters of
                     Nothing -> do
                         let purePattern =
@@ -428,30 +378,6 @@ mainWithOptions
                 withFile outputFile WriteMode (\h -> hPutDoc h unparsed)
         () <$ exitWith exitCode
 
-mainModule
-    :: ModuleName
-    -> Map.Map
-        ModuleName
-        (VerifiedModule StepperAttributes Attribute.Axiom)
-    -> IO (VerifiedModule StepperAttributes Attribute.Axiom)
-mainModule name modules =
-    case Map.lookup name modules of
-        Nothing ->
-            error
-                (  "The main module, '"
-                ++ getModuleNameForError name
-                ++ "', was not found. Check the --module flag."
-                )
-        Just m -> return m
-
-{- | Parse a Kore definition from a filename.
-
-Also prints timing information; see 'mainParse'.
-
- -}
-parseDefinition :: FilePath -> IO KoreDefinition
-parseDefinition = mainParse parseKoreDefinition
-
 -- | IO action that parses a kore pattern from a filename and prints timing
 -- information.
 mainPatternParse :: String -> IO CommonKorePattern
@@ -484,100 +410,10 @@ mainParseSearchPattern indexedModule patternFileName = do
                 }
         _ -> error "Unexpected non-conjunctive pattern"
 
--- | IO action that parses a kore AST entity from a filename and prints timing
--- information.
-mainParse
-    :: (FilePath -> String -> Either String a)
-    -> String
-    -> IO a
-mainParse parser fileName = do
-    contents <-
-        clockSomethingIO "Reading the input file" (readFile fileName)
-    parseResult <-
-        clockSomething "Parsing the file" (parser fileName contents)
-    case parseResult of
-        Left err         -> error err
-        Right definition -> return definition
-
-{- | Verify the well-formedness of a Kore definition.
-
-Also prints timing information; see 'mainParse'.
-
- -}
-verifyDefinitionWithBase
-    :: Maybe
-        ( Map.Map
-            ModuleName
-            (VerifiedModule StepperAttributes Attribute.Axiom)
-        , Map.Map Text AstLocation
-        )
-    -- ^ base definition to use for verification
-    -> Bool -- ^ whether to check (True) or ignore attributes during verification
-    -> KoreDefinition -- ^ Parsed definition to check well-formedness
-    -> IO
-        ( Map.Map
-            ModuleName
-            (VerifiedModule StepperAttributes Attribute.Axiom)
-        , Map.Map Text AstLocation
-        )
-verifyDefinitionWithBase maybeBaseModule willChkAttr definition =
-    let attributesVerification =
-            if willChkAttr
-            then defaultAttributesVerification Proxy Proxy
-            else DoNotVerifyAttributes
-    in do
-      verifyResult <-
-        clockSomething "Verifying the definition"
-            (verifyAndIndexDefinitionWithBase
-                maybeBaseModule
-                attributesVerification
-                Builtin.koreVerifiers
-                definition
-            )
-      case verifyResult of
-        Left err1               -> error (printError err1)
-        Right indexedDefinition -> return indexedDefinition
-
 makePurePattern
     :: VerifiedKorePattern
     -> CommonStepPattern Object
 makePurePattern pat =
     case fromKorePattern Object pat of
         Left err -> error (printError err)
         Right objPat -> objPat
-
--- TODO (traiansf): Get rid of this.
--- The function below works around several limitations of
--- the current tool by tricking the tool into believing that
--- functions are constructors (so that function patterns can match)
--- and that @kseq@ and @dotk@ are both functional and constructor.
-constructorFunctions
-    :: VerifiedModule StepperAttributes Attribute.Axiom
-    -> VerifiedModule StepperAttributes Attribute.Axiom
-constructorFunctions ixm =
-    ixm
-        { indexedModuleObjectSymbolSentences =
-            Map.mapWithKey
-                constructorFunctions1
-                (indexedModuleObjectSymbolSentences ixm)
-        , indexedModuleObjectAliasSentences =
-            Map.mapWithKey
-                constructorFunctions1
-                (indexedModuleObjectAliasSentences ixm)
-        , indexedModuleImports = recurseIntoImports <$> indexedModuleImports ixm
-        }
-  where
-    constructorFunctions1 ident (atts, defn) =
-        ( atts
-            & lensConstructor Lens.<>~ Constructor isCons
-            & lensFunctional Lens.<>~ Functional (isCons || isInj)
-            & lensInjective Lens.<>~ Injective (isCons || isInj)
-            & lensSortInjection Lens.<>~ SortInjection isInj
-        , defn
-        )
-      where
-        isInj = getId ident == "inj"
-        isCons = elem (getId ident) ["kseq", "dotk"]
-
-    recurseIntoImports (attrs, attributes, importedModule) =
-        (attrs, attributes, constructorFunctions importedModule)
diff --git a/kore/app/parser/Main.hs b/kore/app/parser/Main.hs
@@ -127,22 +127,6 @@ main = do
             when willPrintPattern $
                 putStrLn (prettyPrintToString parsedPattern)
 
-mainModule
-    :: ModuleName
-    -> Map.Map
-        ModuleName
-        (VerifiedModule StepperAttributes Attribute.Axiom)
-    -> IO (VerifiedModule StepperAttributes Attribute.Axiom)
-mainModule name modules =
-    case Map.lookup name modules of
-        Nothing ->
-            error
-                (  "The main module, '"
-                ++ getModuleNameForError name
-                ++ "', was not found. Check the --module flag."
-                )
-        Just m -> return m
-
 -- | IO action that parses a kore definition from a filename and prints timing
 -- information.
 mainDefinitionParse :: String -> IO KoreDefinition
@@ -153,21 +137,6 @@ mainDefinitionParse = mainParse parseKoreDefinition
 mainPatternParse :: String -> IO CommonKorePattern
 mainPatternParse = mainParse parseKorePattern
 
--- | IO action that parses a kore AST entity from a filename and prints timing
--- information.
-mainParse
-    :: (FilePath -> String -> Either String a)
-    -> String
-    -> IO a
-mainParse parser fileName = do
-    contents <-
-        clockSomethingIO "Reading the input file" (readFile fileName)
-    parseResult <-
-        clockSomething "Parsing the file" (parser fileName contents)
-    case parseResult of
-        Left err         -> error err
-        Right definition -> return definition
-
 -- | IO action verifies well-formedness of Kore definition and prints
 -- timing information.
 mainVerify