-- |
-- Module      :  Cryptol.REPL.Command
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.REPL.Command (
    -- * Commands
    Command(..), CommandDescr(..), CommandBody(..), CommandResult(..)
  , parseCommand
  , runCommand
  , splitCommand
  , findCommand
  , findCommandExact
  , findNbCommand
  , commandList
  , emptyCommandResult

  , moduleCmd, loadCmd, loadPrelude, setOptionCmd

    -- Parsing
  , interactiveConfig
  , replParseExpr

    -- Evaluation and Typechecking
  , replEvalExpr
  , replCheckExpr

    -- Check, SAT, and prove
  , TestReport(..)
  , qcExpr, qcCmd, QCMode(..)
  , satCmd
  , proveCmd
  , onlineProveSat
  , offlineProveSat

    -- Check docstrings
  , checkDocStrings
  , SubcommandResult(..)
  , DocstringResult(..)

    -- Misc utilities
  , handleCtrlC
  , sanitize
  , withRWTempFile

    -- To support Notebook interface (might need to refactor)
  , replParse
  , liftModuleCmd
  , moduleCmdResult
  ) where

import Cryptol.REPL.Monad
import Cryptol.REPL.Trie
import Cryptol.REPL.Browse
import Cryptol.REPL.Help

import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Interface as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M
    (RenamerWarning(SymbolShadowed, PrefixAssocChanged))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.ModuleSystem.Env as M
import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString)

import           Cryptol.Backend.FloatHelpers as FP
import qualified Cryptol.Backend.Monad as E
import qualified Cryptol.Backend.SeqMap as E
import Cryptol.Backend.Concrete ( Concrete(..) )
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Env as E
import           Cryptol.Eval.FFI
import           Cryptol.Eval.FFI.GenHeader
import qualified Cryptol.Eval.Type as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Eval.Reference as R
import Cryptol.Testing.Random
import qualified Cryptol.Testing.Random  as TestR
import Cryptol.Parser
    (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
    ,parseModName,parseHelpName,parseImpName)
import           Cryptol.Parser.Position (Position(..),Range(..),HasLoc(..))
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Error as T
import qualified Cryptol.TypeCheck.Parseable as T
import qualified Cryptol.TypeCheck.Subst as T
import           Cryptol.TypeCheck.Solve(defaultReplExpr)
import           Cryptol.TypeCheck.PP (dump)
import qualified Cryptol.Utils.Benchmark as Bench
import           Cryptol.Utils.PP hiding ((</>))
import           Cryptol.Utils.Panic(panic)
import           Cryptol.Utils.RecordMap
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Transform.Specialize as S
import Cryptol.Symbolic
  ( ProverCommand(..), QueryType(..)
  , ProverStats,ProverResult(..),CounterExampleType(..)
  )
import qualified Cryptol.Symbolic.SBV as SBV
import qualified Cryptol.Symbolic.What4 as W4
import Cryptol.Version (displayVersion)

import qualified Control.Exception as X
import Control.Monad hiding (mapM, mapM)
import qualified Control.Monad.Catch as Ex
import Control.Monad.IO.Class(liftIO)
import Text.Read (readMaybe)
import Control.Applicative ((<|>))
import qualified Data.Set as Set
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BS8
import Data.Bits (shiftL, (.&.), (.|.))
import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii)
import Data.Function (on)
import Data.List (intercalate, nub, isPrefixOf)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe,mapMaybe,isNothing)
import System.Environment (lookupEnv)
import System.Exit (ExitCode(ExitSuccess))
import System.Process (shell,createProcess,waitForProcess)
import qualified System.Process as Process(runCommand)
import System.FilePath((</>), (-<.>), isPathSeparator)
import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist
                       ,getTemporaryDirectory,setPermissions,removeFile
                       ,emptyPermissions,setOwnerReadable)
import System.IO
         (Handle,hFlush,stdout,openTempFile,hClose,openFile
         ,IOMode(..),hGetContents,hSeek,SeekMode(..))
import qualified System.Random.TF as TF
import qualified System.Random.TF.Instances as TFI
import Numeric (showFFloat)
import qualified Data.Text as T
import Data.IORef(newIORef, readIORef, writeIORef, modifyIORef)

import GHC.Float (log1p, expm1)

import Prelude ()
import Prelude.Compat

import qualified Data.SBV.Internals as SBV (showTDiff)
import Data.Foldable (foldl')



-- Commands --------------------------------------------------------------------

-- | Commands.
data Command
  = Command (Int -> Maybe FilePath -> REPL CommandResult) -- ^ Successfully parsed command
  | Ambiguous String [String] -- ^ Ambiguous command, list of conflicting
                              --   commands
  | Unknown String            -- ^ The unknown command

-- | Command builder.
data CommandDescr = CommandDescr
  { CommandDescr -> [[Char]]
cNames    :: [String]
  , CommandDescr -> [[Char]]
cArgs     :: [String]
  , CommandDescr -> CommandBody
cBody     :: CommandBody
  , CommandDescr -> [Char]
cHelp     :: String
  , CommandDescr -> [Char]
cLongHelp :: String
  }

instance Show CommandDescr where
  show :: CommandDescr -> [Char]
show = [[Char]] -> [Char]
forall a. Show a => a -> [Char]
show ([[Char]] -> [Char])
-> (CommandDescr -> [[Char]]) -> CommandDescr -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandDescr -> [[Char]]
cNames

instance Eq CommandDescr where
  == :: CommandDescr -> CommandDescr -> Bool
(==) = [[Char]] -> [[Char]] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([[Char]] -> [[Char]] -> Bool)
-> (CommandDescr -> [[Char]])
-> CommandDescr
-> CommandDescr
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CommandDescr -> [[Char]]
cNames

instance Ord CommandDescr where
  compare :: CommandDescr -> CommandDescr -> Ordering
compare = [[Char]] -> [[Char]] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([[Char]] -> [[Char]] -> Ordering)
-> (CommandDescr -> [[Char]])
-> CommandDescr
-> CommandDescr
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CommandDescr -> [[Char]]
cNames

data CommandBody
  = ExprArg     (String   -> (Int,Int) -> Maybe FilePath -> REPL CommandResult)
  | FileExprArg (FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult)
  | DeclsArg    (String   -> REPL CommandResult)
  | ExprTypeArg (String   -> REPL CommandResult)
  | ModNameArg  (String   -> REPL CommandResult)
  | FilenameArg (FilePath -> REPL CommandResult)
  | OptionArg   (String   -> REPL CommandResult)
  | ShellArg    (String   -> REPL CommandResult)
  | HelpArg     (String   -> REPL CommandResult)
  | NoArg       (REPL CommandResult)

data CommandResult = CommandResult
  { CommandResult -> Maybe [Char]
crType :: Maybe String -- ^ type output for relevant commands
  , CommandResult -> Maybe [Char]
crValue :: Maybe String -- ^ value output for relevant commands
  , CommandResult -> Bool
crSuccess :: Bool -- ^ indicator that command successfully performed its task
  }
  deriving (Int -> CommandResult -> ShowS
[CommandResult] -> ShowS
CommandResult -> [Char]
(Int -> CommandResult -> ShowS)
-> (CommandResult -> [Char])
-> ([CommandResult] -> ShowS)
-> Show CommandResult
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CommandResult -> ShowS
showsPrec :: Int -> CommandResult -> ShowS
$cshow :: CommandResult -> [Char]
show :: CommandResult -> [Char]
$cshowList :: [CommandResult] -> ShowS
showList :: [CommandResult] -> ShowS
Show)

emptyCommandResult :: CommandResult
emptyCommandResult :: CommandResult
emptyCommandResult = CommandResult
  { crType :: Maybe [Char]
crType = Maybe [Char]
forall a. Maybe a
Nothing
  , crValue :: Maybe [Char]
crValue = Maybe [Char]
forall a. Maybe a
Nothing
  , crSuccess :: Bool
crSuccess = Bool
True
  }

-- | REPL command parsing.
commands :: CommandMap
commands :: CommandMap
commands  = (CommandMap -> CommandDescr -> CommandMap)
-> CommandMap -> [CommandDescr] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CommandMap -> CommandDescr -> CommandMap
insert CommandMap
forall a. Trie a
emptyTrie [CommandDescr]
commandList
  where
  insert :: CommandMap -> CommandDescr -> CommandMap
insert CommandMap
m CommandDescr
d = (CommandMap -> [Char] -> CommandMap)
-> CommandMap -> [[Char]] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CommandDescr -> CommandMap -> [Char] -> CommandMap
forall {a}. a -> Trie a -> [Char] -> Trie a
insertOne CommandDescr
d) CommandMap
m (CommandDescr -> [[Char]]
cNames CommandDescr
d)
  insertOne :: a -> Trie a -> [Char] -> Trie a
insertOne a
d Trie a
m [Char]
name = [Char] -> a -> Trie a -> Trie a
forall a. [Char] -> a -> Trie a -> Trie a
insertTrie [Char]
name a
d Trie a
m

-- | Notebook command parsing.
nbCommands :: CommandMap
nbCommands :: CommandMap
nbCommands  = (CommandMap -> CommandDescr -> CommandMap)
-> CommandMap -> [CommandDescr] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CommandMap -> CommandDescr -> CommandMap
insert CommandMap
forall a. Trie a
emptyTrie [CommandDescr]
nbCommandList
  where
  insert :: CommandMap -> CommandDescr -> CommandMap
insert CommandMap
m CommandDescr
d = (CommandMap -> [Char] -> CommandMap)
-> CommandMap -> [[Char]] -> CommandMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CommandDescr -> CommandMap -> [Char] -> CommandMap
forall {a}. a -> Trie a -> [Char] -> Trie a
insertOne CommandDescr
d) CommandMap
m (CommandDescr -> [[Char]]
cNames CommandDescr
d)
  insertOne :: a -> Trie a -> [Char] -> Trie a
insertOne a
d Trie a
m [Char]
name = [Char] -> a -> Trie a -> Trie a
forall a. [Char] -> a -> Trie a -> Trie a
insertTrie [Char]
name a
d Trie a
m

-- | A subset of commands safe for Notebook execution
nbCommandList :: [CommandDescr]
nbCommandList :: [CommandDescr]
nbCommandList  =
  [ [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":t", [Char]
":type" ] [[Char]
"EXPR"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
typeOfCmd)
    [Char]
"Check the type of an expression."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":b", [Char]
":browse" ] [[Char]
"[ MODULE ]"] (([Char] -> REPL CommandResult) -> CommandBody
ModNameArg [Char] -> REPL CommandResult
browseCmd)
    [Char]
"Display information about loaded modules."
    ([[Char]] -> [Char]
unlines
       [ [Char]
"With no arguent, :browse shows information about the names in scope."
       , [Char]
"With an argument M, shows information about the names exported from M"
       ]
    )
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":version"] [] (REPL CommandResult -> CommandBody
NoArg REPL CommandResult
versionCmd)
    [Char]
"Display the version of this Cryptol executable"
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":?", [Char]
":help" ] [[Char]
"[ TOPIC ]"] (([Char] -> REPL CommandResult) -> CommandBody
HelpArg [Char] -> REPL CommandResult
helpCmd)
    [Char]
"Display a brief description of a function, type, or command. (e.g. :help :help)"
    ([[Char]] -> [Char]
unlines
      [ [Char]
"TOPIC can be any of:"
      , [Char]
" * Specific REPL colon-commands (e.g. :help :prove)"
      , [Char]
" * Functions (e.g. :help join)"
      , [Char]
" * Infix operators (e.g. :help +)"
      , [Char]
" * Type constructors (e.g. :help Z)"
      , [Char]
" * Type constraints (e.g. :help fin)"
      , [Char]
" * :set-able options (e.g. :help :set base)" ])
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":s", [Char]
":set" ] [[Char]
"[ OPTION [ = VALUE ] ]"] (([Char] -> REPL CommandResult) -> CommandBody
OptionArg [Char] -> REPL CommandResult
setOptionCmd)
    [Char]
"Set an environmental option (:set on its own displays current values)."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":check" ] [[Char]
"[ EXPR ]"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg (QCMode
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
qcCmd QCMode
QCRandom))
    [Char]
"Use random testing to check that the argument always returns true.\n(If no argument, check all properties.)"
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":exhaust" ] [[Char]
"[ EXPR ]"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg (QCMode
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
qcCmd QCMode
QCExhaust))
    [Char]
"Use exhaustive testing to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":prove" ] [[Char]
"[ EXPR ]"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
proveCmd)
    [Char]
"Use an external solver to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":sat" ] [[Char]
"[ EXPR ]"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
satCmd)
    [Char]
"Use a solver to find a satisfying assignment for which the argument\nreturns true. (If no argument, find an assignment for all properties.)"
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":safe" ] [[Char]
"[ EXPR ]"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
safeCmd)
    [Char]
"Use an external solver to prove that an expression is safe\n(does not encounter run-time errors) for all inputs."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":debug_specialize" ] [[Char]
"EXPR"](([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
specializeCmd)
    [Char]
"Do type specialization on a closed expression."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":eval" ] [[Char]
"EXPR"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
refEvalCmd)
    [Char]
"Evaluate an expression with the reference evaluator."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":ast" ] [[Char]
"EXPR"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
astOfCmd)
    [Char]
"Print out the pre-typechecked AST of a given term."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":extract-coq" ] [] (REPL CommandResult -> CommandBody
NoArg REPL CommandResult
extractCoqCmd)
    [Char]
"Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":time" ] [[Char]
"EXPR"] (([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
ExprArg [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
timeCmd)
    [Char]
"Measure the time it takes to evaluate the given expression."
    ([[Char]] -> [Char]
unlines
      [ [Char]
"The expression will be evaluated many times to get accurate results."
      , [Char]
"Note that the first evaluation of a binding may take longer due to"
      , [Char]
"  laziness, and this may affect the reported time. If this is not"
      , [Char]
"  desired then make sure to evaluate the expression once first before"
      , [Char]
"  running :time."
      , [Char]
"The amount of time to spend collecting measurements can be changed"
      , [Char]
"  with the timeMeasurementPeriod option."
      , [Char]
"Reports the average wall clock time, CPU time, and cycles."
      , [Char]
"  (Cycles are in unspecified units that may be CPU cycles.)"
      , [Char]
"Binds the result to"
      , [Char]
"  it : { avgTime : Float64"
      , [Char]
"       , avgCpuTime : Float64"
      , [Char]
"       , avgCycles : Integer }" ])

  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":set-seed" ] [[Char]
"SEED"] (([Char] -> REPL CommandResult) -> CommandBody
OptionArg [Char] -> REPL CommandResult
seedCmd)
      [Char]
"Seed the random number generator for operations using randomness"
      ([[Char]] -> [Char]
unlines
        [ [Char]
"A seed takes the form of either a single integer or a 4-tuple"
        , [Char]
"of unsigned 64-bit integers.  Examples of commands using randomness"
        , [Char]
"are dumpTests and check."
        ])
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":new-seed"] [] (REPL CommandResult -> CommandBody
NoArg REPL CommandResult
newSeedCmd)
      [Char]
"Randomly generate and set a new seed for the random number generator"
      [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":check-docstrings" ] [] (([Char] -> REPL CommandResult) -> CommandBody
ModNameArg [Char] -> REPL CommandResult
checkDocStringsCmd)
      [Char]
"Run the REPL code blocks in the module's docstring comments"
      [Char]
""
  ]

commandList :: [CommandDescr]
commandList :: [CommandDescr]
commandList  =
  [CommandDescr]
nbCommandList [CommandDescr] -> [CommandDescr] -> [CommandDescr]
forall a. [a] -> [a] -> [a]
++
  [ [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":q", [Char]
":quit" ] [] (REPL CommandResult -> CommandBody
NoArg REPL CommandResult
quitCmd)
    [Char]
"Exit the REPL."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":l", [Char]
":load" ] [[Char]
"FILE"] (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg [Char] -> REPL CommandResult
loadCmd)
    [Char]
"Load a module by filename."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":r", [Char]
":reload" ] [] (REPL CommandResult -> CommandBody
NoArg REPL CommandResult
reloadCmd)
    [Char]
"Reload the currently loaded module."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":e", [Char]
":edit" ] [[Char]
"[ FILE ]"] (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg [Char] -> REPL CommandResult
editCmd)
    [Char]
"Edit FILE or the currently loaded module."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":!" ] [[Char]
"COMMAND"] (([Char] -> REPL CommandResult) -> CommandBody
ShellArg [Char] -> REPL CommandResult
runShellCmd)
    [Char]
"Execute a command in the shell."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":cd" ] [[Char]
"DIR"] (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg [Char] -> REPL CommandResult
cdCmd)
    [Char]
"Set the current working directory."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":m", [Char]
":module" ] [[Char]
"[ MODULE ]"] (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg [Char] -> REPL CommandResult
moduleCmd)
    [Char]
"Load a module by its name."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":f", [Char]
":focus" ] [[Char]
"[ MODULE ]"] (([Char] -> REPL CommandResult) -> CommandBody
ModNameArg [Char] -> REPL CommandResult
focusCmd)
    [Char]
"Focus name scope inside a loaded module."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":w", [Char]
":writeByteArray" ] [[Char]
"FILE", [Char]
"EXPR"] (([Char]
 -> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
FileExprArg [Char]
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
writeFileCmd)
    [Char]
"Write data of type 'fin n => [n][8]' to a file."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":readByteArray" ] [[Char]
"FILE"] (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg [Char] -> REPL CommandResult
readFileCmd)
    [Char]
"Read data from a file as type 'fin n => [n][8]', binding\nthe value to variable 'it'."
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":dumptests" ] [[Char]
"FILE", [Char]
"EXPR"] (([Char]
 -> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult)
-> CommandBody
FileExprArg [Char]
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
dumpTestsCmd)
    ([[Char]] -> [Char]
unlines [ [Char]
"Dump a tab-separated collection of tests for the given"
             , [Char]
"expression into a file. The first column in each line is"
             , [Char]
"the expected output, and the remainder are the inputs. The"
             , [Char]
"number of tests is determined by the \"tests\" option."
             ])
    [Char]
""
  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":generate-foreign-header" ] [[Char]
"FILE"] (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg [Char] -> REPL CommandResult
genHeaderCmd)
    [Char]
"Generate a C header file from foreign declarations in a Cryptol file."
    ([[Char]] -> [Char]
unlines
      [ [Char]
"Converts all foreign declarations in the given Cryptol file into C"
      , [Char]
"function declarations, and writes them to a file with the same name"
      , [Char]
"but with a .h extension." ])


  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":file-deps" ] [ [Char]
"FILE" ]
    (([Char] -> REPL CommandResult) -> CommandBody
FilenameArg (Bool -> [Char] -> REPL CommandResult
moduleInfoCmd Bool
True))
    [Char]
"Show information about the dependencies of a file"
    [Char]
""

  , [[Char]]
-> [[Char]] -> CommandBody -> [Char] -> [Char] -> CommandDescr
CommandDescr [ [Char]
":module-deps" ] [ [Char]
"MODULE" ]
    (([Char] -> REPL CommandResult) -> CommandBody
ModNameArg (Bool -> [Char] -> REPL CommandResult
moduleInfoCmd Bool
False))
    [Char]
"Show information about the dependencies of a module"
    [Char]
""
  ]

genHelp :: [CommandDescr] -> [String]
genHelp :: [CommandDescr] -> [[Char]]
genHelp [CommandDescr]
cs = (CommandDescr -> [Char]) -> [CommandDescr] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map CommandDescr -> [Char]
cmdHelp [CommandDescr]
cs
  where
  cmdHelp :: CommandDescr -> [Char]
cmdHelp CommandDescr
cmd  = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [ [Char]
"  ", CommandDescr -> [Char]
cmdNames CommandDescr
cmd, ShowS
forall {t :: * -> *} {a}. Foldable t => t a -> [Char]
pad (CommandDescr -> [Char]
cmdNames CommandDescr
cmd),
                            [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate ([Char]
"\n  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Any] -> [Char]
forall {t :: * -> *} {a}. Foldable t => t a -> [Char]
pad []) ([Char] -> [[Char]]
lines (CommandDescr -> [Char]
cHelp CommandDescr
cmd)) ]
  cmdNames :: CommandDescr -> [Char]
cmdNames CommandDescr
cmd = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (CommandDescr -> [[Char]]
cNames CommandDescr
cmd)
  padding :: Int
padding      = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((CommandDescr -> Int) -> [CommandDescr] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Char] -> Int) -> (CommandDescr -> [Char]) -> CommandDescr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandDescr -> [Char]
cmdNames) [CommandDescr]
cs)
  pad :: t a -> [Char]
pad t a
n        = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int
padding Int -> Int -> Int
forall a. Num a => a -> a -> a
- t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
n)) Char
' '


-- Command Evaluation ----------------------------------------------------------

-- | Run a command.
runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandResult
runCommand :: Int -> Maybe [Char] -> Command -> REPL CommandResult
runCommand Int
lineNum Maybe [Char]
mbBatch Command
c = case Command
c of

  Command Int -> Maybe [Char] -> REPL CommandResult
cmd -> Int -> Maybe [Char] -> REPL CommandResult
cmd Int
lineNum Maybe [Char]
mbBatch REPL CommandResult
-> (REPLException -> REPL CommandResult) -> REPL CommandResult
forall a. REPL a -> (REPLException -> REPL a) -> REPL a
`Cryptol.REPL.Monad.catch` REPLException -> REPL CommandResult
forall {a}. PP a => a -> REPL CommandResult
handler
    where
    handler :: a -> REPL CommandResult
handler a
re = do
      [Char] -> REPL ()
rPutStrLn [Char]
""
      Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (a -> Doc
forall a. PP a => a -> Doc
pp a
re)
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult { crSuccess = False }

  Unknown [Char]
cmd -> do
    [Char] -> REPL ()
rPutStrLn ([Char]
"Unknown command: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
cmd)
    CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult { crSuccess = False }

  Ambiguous [Char]
cmd [[Char]]
cmds -> do
    [Char] -> REPL ()
rPutStrLn ([Char]
cmd [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" is ambiguous, it could mean one of:")
    [Char] -> REPL ()
rPutStrLn ([Char]
"\t" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
cmds)
    CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult { crSuccess = False }


evalCmd :: String -> Int -> Maybe FilePath -> REPL CommandResult
evalCmd :: [Char] -> Int -> Maybe [Char] -> REPL CommandResult
evalCmd [Char]
str Int
lineNum Maybe [Char]
mbBatch = do
  ReplInput PName
ri <- [Char] -> Int -> Maybe [Char] -> REPL (ReplInput PName)
replParseInput [Char]
str Int
lineNum Maybe [Char]
mbBatch
  case ReplInput PName
ri of
    P.ExprInput Expr PName
expr -> do
      (Value
val,Type
_ty) <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
      PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
      Doc
valDoc <- Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEvalRethrow (Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppOpts Value
val)

      -- This is the point where the value gets forced. We deepseq the
      -- pretty-printed representation of it, rather than the value
      -- itself, leaving it up to the pretty-printer to determine how
      -- much of the value to force
      --out <- io $ rethrowEvalError
      --          $ return $!! show $ pp $ E.WithBase ppOpts val

      let value :: [Char]
value = Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
valDoc
      [Char] -> REPL ()
rPutStrLn [Char]
value
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crValue = Just value }

    P.LetInput [Decl PName]
ds -> do
      -- explicitly make this a top-level declaration, so that it will
      -- be generalized if mono-binds is enabled
      [Decl PName] -> REPL ()
replEvalDecls [Decl PName]
ds
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

    ReplInput PName
P.EmptyInput ->
      -- comment or empty input does nothing
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

  -- parsing and evaluating expressions can fail in many different ways
  REPL CommandResult
-> (REPLException -> REPL CommandResult) -> REPL CommandResult
forall a. REPL a -> (REPLException -> REPL a) -> REPL a
`catch` \REPLException
e -> do
      [Char] -> REPL ()
rPutStrLn [Char]
""
      Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (REPLException -> Doc
forall a. PP a => a -> Doc
pp REPLException
e)
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }

printCounterexample :: CounterExampleType -> Doc -> [Concrete.Value] -> REPL ()
printCounterexample :: CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
cexTy Doc
exprDoc [Value]
vs =
  do PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
     -- NB: Use a precedence of 1 here, as `vs` will be pretty-printed as
     -- arguments to the function in `exprDoc`. This ensures that arguments
     -- are parenthesized as needed.
     [Doc]
docs <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> PPOpts -> Int -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> Int -> GenValue sym -> SEval sym Doc
E.ppValuePrec Concrete
Concrete PPOpts
ppOpts Int
1) [Value]
vs
     let cexRes :: [Doc]
cexRes = case CounterExampleType
cexTy of
           CounterExampleType
SafetyViolation    -> [[Char] -> Doc
text [Char]
"~> ERROR"]
           CounterExampleType
PredicateFalsified -> [[Char] -> Doc
text [Char]
"= False"]
     Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc
exprDoc] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
docs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
cexRes))

printSatisfyingModel :: Doc -> [Concrete.Value] -> REPL ()
printSatisfyingModel :: Doc -> [Value] -> REPL ()
printSatisfyingModel Doc
exprDoc [Value]
vs =
  do PPOpts
ppOpts <- REPL PPOpts
getPPValOpts
     [Doc]
docs <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppOpts) [Value]
vs
     Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc
exprDoc] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
docs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> Doc
text [Char]
"= True"]))


dumpTestsCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
dumpTestsCmd :: [Char]
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
dumpTestsCmd [Char]
outFile [Char]
str (Int, Int)
pos Maybe [Char]
fnm =
  do Expr PName
expr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
     (Value
val, Type
ty) <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
     PPOpts
ppopts <- REPL PPOpts
getPPValOpts
     Int
testNum <- [Char] -> REPL Int
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"tests" :: REPL Int
     TypeEnv
tenv <- GenEvalEnv Concrete -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
E.envTypes (GenEvalEnv Concrete -> TypeEnv)
-> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynamicEnv -> GenEvalEnv Concrete
M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL DynamicEnv
getDynEnv
     let tyv :: TValue
tyv = TypeEnv -> Type -> TValue
E.evalValType TypeEnv
tenv Type
ty
     [Integer -> TFGen -> (Eval Value, TFGen)]
gens <-
       case TValue -> Maybe [Gen TFGen Concrete]
forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
TestR.dumpableType TValue
tyv of
         Maybe [Gen TFGen Concrete]
Nothing -> REPLException -> REPL [Integer -> TFGen -> (Eval Value, TFGen)]
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)
         Just [Gen TFGen Concrete]
gens -> [Integer -> TFGen -> (Eval Value, TFGen)]
-> REPL [Integer -> TFGen -> (Eval Value, TFGen)]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return [Integer -> TFGen -> (Eval Value, TFGen)]
[Gen TFGen Concrete]
gens
     [([Value], Value)]
tests <- (TFGen -> REPL ([([Value], Value)], TFGen))
-> REPL [([Value], Value)]
forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen (\TFGen
g -> IO ([([Value], Value)], TFGen) -> REPL ([([Value], Value)], TFGen)
forall a. IO a -> REPL a
io (IO ([([Value], Value)], TFGen)
 -> REPL ([([Value], Value)], TFGen))
-> IO ([([Value], Value)], TFGen)
-> REPL ([([Value], Value)], TFGen)
forall a b. (a -> b) -> a -> b
$ TFGen
-> [Gen TFGen Concrete]
-> Value
-> Int
-> IO ([([Value], Value)], TFGen)
forall g.
RandomGen g =>
g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
TestR.returnTests' TFGen
g [Integer -> TFGen -> (Eval Value, TFGen)]
[Gen TFGen Concrete]
gens Value
val Int
testNum)
     [[Char]]
out <- [([Value], Value)]
-> (([Value], Value) -> REPL [Char]) -> REPL [[Char]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [([Value], Value)]
tests ((([Value], Value) -> REPL [Char]) -> REPL [[Char]])
-> (([Value], Value) -> REPL [Char]) -> REPL [[Char]]
forall a b. (a -> b) -> a -> b
$
            \([Value]
args, Value
x) ->
              do [Doc]
argOut <- (Value -> REPL Doc) -> [Value] -> REPL [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Eval Doc -> REPL Doc) -> (Value -> Eval Doc) -> Value -> REPL Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppopts) [Value]
args
                 Doc
resOut <- Eval Doc -> REPL Doc
forall a. Eval a -> REPL a
rEval (Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
E.ppValue Concrete
Concrete PPOpts
ppopts Value
x)
                 [Char] -> REPL [Char]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> [Char]
renderOneLine Doc
resOut [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\t" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\t" ((Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> [Char]
renderOneLine [Doc]
argOut) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
     Either SomeException ()
writeResult <- IO (Either SomeException ()) -> REPL (Either SomeException ())
forall a. IO a -> REPL a
io (IO (Either SomeException ()) -> REPL (Either SomeException ()))
-> IO (Either SomeException ()) -> REPL (Either SomeException ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO (Either SomeException ())
forall e a. Exception e => IO a -> IO (Either e a)
X.try ([Char] -> [Char] -> IO ()
writeFile [Char]
outFile ([[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]]
out))
     case Either SomeException ()
writeResult of
       Right{} -> CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult
       Left SomeException
e ->
         do [Char] -> REPL ()
rPutStrLn (SomeException -> [Char]
forall e. Exception e => e -> [Char]
X.displayException (SomeException
e :: X.SomeException))
            CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }


data QCMode = QCRandom | QCExhaust deriving (QCMode -> QCMode -> Bool
(QCMode -> QCMode -> Bool)
-> (QCMode -> QCMode -> Bool) -> Eq QCMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QCMode -> QCMode -> Bool
== :: QCMode -> QCMode -> Bool
$c/= :: QCMode -> QCMode -> Bool
/= :: QCMode -> QCMode -> Bool
Eq, Int -> QCMode -> ShowS
[QCMode] -> ShowS
QCMode -> [Char]
(Int -> QCMode -> ShowS)
-> (QCMode -> [Char]) -> ([QCMode] -> ShowS) -> Show QCMode
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QCMode -> ShowS
showsPrec :: Int -> QCMode -> ShowS
$cshow :: QCMode -> [Char]
show :: QCMode -> [Char]
$cshowList :: [QCMode] -> ShowS
showList :: [QCMode] -> ShowS
Show)


-- | Randomly test a property, or exhaustively check it if the number
-- of values in the type under test is smaller than the @tests@
-- environment variable, or we specify exhaustive testing.
qcCmd :: QCMode -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
qcCmd :: QCMode
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
qcCmd QCMode
qcMode [Char]
"" (Int, Int)
_pos Maybe [Char]
_fnm =
  do ([(Name, IfaceDecl)]
xs,NameDisp
disp) <- REPL ([(Name, IfaceDecl)], NameDisp)
getPropertyNames
     let nameStr :: a -> [Char]
nameStr a
x = Doc -> [Char]
forall a. Show a => a -> [Char]
show (NameDisp -> Doc -> Doc
fixNameDisp NameDisp
disp (a -> Doc
forall a. PP a => a -> Doc
pp a
x))
     if [(Name, IfaceDecl)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, IfaceDecl)]
xs
        then do
          [Char] -> REPL ()
rPutStrLn [Char]
"There are no properties in scope."
          CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
        else do
          let evalProp :: Bool -> (Name, IfaceDecl) -> REPL Bool
evalProp Bool
result (Name
x,IfaceDecl
d) =
               do let str :: [Char]
str = Name -> [Char]
forall {a}. PP a => a -> [Char]
nameStr Name
x
                  [Char] -> REPL ()
rPutStr ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"property " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
str [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" "
                  let texpr :: Expr
texpr = Name -> Expr
T.EVar Name
x
                  let schema :: Schema
schema = IfaceDecl -> Schema
M.ifDeclSig IfaceDecl
d
                  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
                  let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
texpr)
                  TestReport
testReport <- QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcExpr QCMode
qcMode Doc
doc Expr
texpr Schema
schema
                  Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> REPL Bool) -> Bool -> REPL Bool
forall a b. (a -> b) -> a -> b
$! Bool
result Bool -> Bool -> Bool
&& TestResult -> Bool
isPass (TestReport -> TestResult
reportResult TestReport
testReport)
          Bool
success <- (Bool -> (Name, IfaceDecl) -> REPL Bool)
-> Bool -> [(Name, IfaceDecl)] -> REPL Bool
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Bool -> (Name, IfaceDecl) -> REPL Bool
evalProp Bool
True [(Name, IfaceDecl)]
xs
          CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = success }

qcCmd QCMode
qcMode [Char]
str (Int, Int)
pos Maybe [Char]
fnm =
  do Expr PName
expr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
     (Expr Name
_,Expr
texpr,Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr
     NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
     let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr PName
expr) -- function application has precedence 3
     TestReport
testReport <- QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcExpr QCMode
qcMode Doc
doc Expr
texpr Schema
schema
     CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = isPass (reportResult testReport) }


data TestReport = TestReport
  { TestReport -> Doc
reportExpr :: Doc
  , TestReport -> TestResult
reportResult :: TestResult
  , TestReport -> Integer
reportTestsRun :: Integer
  , TestReport -> Maybe Integer
reportTestsPossible :: Maybe Integer
  }

qcExpr ::
  QCMode ->
  Doc ->
  T.Expr ->
  T.Schema ->
  REPL TestReport
qcExpr :: QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcExpr QCMode
qcMode Doc
exprDoc Expr
texpr Schema
schema =
  do (Value
val,Type
ty) <- Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
texpr Schema
schema REPL (Maybe (Value, Type))
-> (Maybe (Value, Type) -> REPL (Value, Type))
-> REPL (Value, Type)
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe (Value, Type)
mb_res -> case Maybe (Value, Type)
mb_res of
       Just (Value, Type)
res -> (Value, Type) -> REPL (Value, Type)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value, Type)
res
       -- If instance is not found, doesn't necessarily mean that there is no instance.
       -- And due to nondeterminism in result from the solver (for finding solution to
       -- numeric type constraints), `:check` can get to this exception sometimes, but
       -- successfully find an instance and test with it other times.
       Maybe (Value, Type)
Nothing -> REPLException -> REPL (Value, Type)
forall a. REPLException -> REPL a
raise (Schema -> REPLException
InstantiationsNotFound Schema
schema)
     Integer
testNum <- (Int -> Integer
forall a. Integral a => a -> Integer
toInteger :: Int -> Integer) (Int -> Integer) -> REPL Int -> REPL Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> REPL Int
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"tests"
     TypeEnv
tenv <- GenEvalEnv Concrete -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
E.envTypes (GenEvalEnv Concrete -> TypeEnv)
-> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynamicEnv -> GenEvalEnv Concrete
M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL DynamicEnv
getDynEnv
     let tyv :: TValue
tyv = TypeEnv -> Type -> TValue
E.evalValType TypeEnv
tenv Type
ty
     -- tv has already had polymorphism instantiated
     IORef (Maybe [Char])
percentRef <- IO (IORef (Maybe [Char])) -> REPL (IORef (Maybe [Char]))
forall a. IO a -> REPL a
io (IO (IORef (Maybe [Char])) -> REPL (IORef (Maybe [Char])))
-> IO (IORef (Maybe [Char])) -> REPL (IORef (Maybe [Char]))
forall a b. (a -> b) -> a -> b
$ Maybe [Char] -> IO (IORef (Maybe [Char]))
forall a. a -> IO (IORef a)
newIORef Maybe [Char]
forall a. Maybe a
Nothing
     IORef Integer
testsRef <- IO (IORef Integer) -> REPL (IORef Integer)
forall a. IO a -> REPL a
io (IO (IORef Integer) -> REPL (IORef Integer))
-> IO (IORef Integer) -> REPL (IORef Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0

     case TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen TFGen Concrete])
forall g.
RandomGen g =>
TValue
-> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
testableType TValue
tyv of
       Just (Just Integer
sz,[TValue]
tys,[[Value]]
vss,[Gen TFGen Concrete]
_gens) | QCMode
qcMode QCMode -> QCMode -> Bool
forall a. Eq a => a -> a -> Bool
== QCMode
QCExhaust Bool -> Bool -> Bool
|| Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
testNum -> do
            [Char] -> REPL ()
rPutStrLn [Char]
"Using exhaustive testing."
            [Char] -> REPL ()
prt [Char]
testingMsg
            (TestResult
res,Integer
num) <-
                  REPL (TestResult, Integer)
-> (SomeException -> REPL (TestResult, Integer))
-> REPL (TestResult, Integer)
forall e a.
(HasCallStack, Exception e) =>
REPL a -> (e -> REPL a) -> REPL a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
Ex.catch ((Integer -> REPL ())
-> Value -> [[Value]] -> REPL (TestResult, Integer)
forall (m :: * -> *).
MonadIO m =>
(Integer -> m ()) -> Value -> [[Value]] -> m (TestResult, Integer)
exhaustiveTests (\Integer
n -> IORef (Maybe [Char])
-> IORef Integer -> Integer -> Integer -> REPL ()
forall {a}.
(Show a, Integral a) =>
IORef (Maybe [Char]) -> IORef a -> a -> a -> REPL ()
ppProgress IORef (Maybe [Char])
percentRef IORef Integer
testsRef Integer
n Integer
sz)
                                            Value
val [[Value]]
vss)
                         (\SomeException
ex -> do [Char] -> REPL ()
rPutStrLn [Char]
"\nTest interrupted..."
                                    Integer
num <- IO Integer -> REPL Integer
forall a. IO a -> REPL a
io (IO Integer -> REPL Integer) -> IO Integer -> REPL Integer
forall a b. (a -> b) -> a -> b
$ IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
testsRef
                                    let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
Pass Integer
num (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz)
                                    [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
False TestReport
report
                                    [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> [Char]
interruptedExhaust Integer
num Integer
sz
                                    SomeException -> REPL (TestResult, Integer)
forall e a. (HasCallStack, Exception e) => e -> REPL a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
Ex.throwM (SomeException
ex :: Ex.SomeException))
            let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
res Integer
num (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
sz)
            REPL ()
delProgress
            REPL ()
delTesting
            [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
True TestReport
report
            TestReport -> REPL TestReport
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return TestReport
report

       Just (Maybe Integer
sz,[TValue]
tys,[[Value]]
_,[Gen TFGen Concrete]
gens) | QCMode
qcMode QCMode -> QCMode -> Bool
forall a. Eq a => a -> a -> Bool
== QCMode
QCRandom -> do
            [Char] -> REPL ()
rPutStrLn [Char]
"Using random testing."
            [Char] -> REPL ()
prt [Char]
testingMsg
            (TestResult
res,Integer
num) <-
              (TFGen -> REPL ((TestResult, Integer), TFGen))
-> REPL (TestResult, Integer)
forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen
                ((Integer -> REPL ())
-> Integer
-> Value
-> [Gen TFGen Concrete]
-> TFGen
-> REPL ((TestResult, Integer), TFGen)
forall (m :: * -> *) g.
(MonadIO m, RandomGen g) =>
(Integer -> m ())
-> Integer
-> Value
-> [Gen g Concrete]
-> g
-> m ((TestResult, Integer), g)
randomTests' (\Integer
n -> IORef (Maybe [Char])
-> IORef Integer -> Integer -> Integer -> REPL ()
forall {a}.
(Show a, Integral a) =>
IORef (Maybe [Char]) -> IORef a -> a -> a -> REPL ()
ppProgress IORef (Maybe [Char])
percentRef IORef Integer
testsRef Integer
n Integer
testNum)
                                      Integer
testNum Value
val [Gen TFGen Concrete]
gens)
              REPL (TestResult, Integer)
-> (SomeException -> REPL (TestResult, Integer))
-> REPL (TestResult, Integer)
forall e a.
(HasCallStack, Exception e) =>
REPL a -> (e -> REPL a) -> REPL a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\SomeException
ex -> do [Char] -> REPL ()
rPutStrLn [Char]
"\nTest interrupted..."
                                    Integer
num <- IO Integer -> REPL Integer
forall a. IO a -> REPL a
io (IO Integer -> REPL Integer) -> IO Integer -> REPL Integer
forall a b. (a -> b) -> a -> b
$ IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
testsRef
                                    let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
Pass Integer
num Maybe Integer
sz
                                    [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
False TestReport
report
                                    case Maybe Integer
sz of
                                      Just Integer
n -> [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> [Char]
coverageString Integer
num Integer
n
                                      Maybe Integer
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                    SomeException -> REPL (TestResult, Integer)
forall e a. (HasCallStack, Exception e) => e -> REPL a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
Ex.throwM (SomeException
ex :: Ex.SomeException))
            let report :: TestReport
report = Doc -> TestResult -> Integer -> Maybe Integer -> TestReport
TestReport Doc
exprDoc TestResult
res Integer
num Maybe Integer
sz
            REPL ()
delProgress
            REPL ()
delTesting
            [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
tys Bool
False TestReport
report
            case Maybe Integer
sz of
              Just Integer
n | TestResult -> Bool
isPass TestResult
res -> [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> [Char]
coverageString Integer
testNum Integer
n
              Maybe Integer
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            TestReport -> REPL TestReport
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return TestReport
report
       Maybe (Maybe Integer, [TValue], [[Value]], [Gen TFGen Concrete])
_ -> REPLException -> REPL TestReport
forall a. REPLException -> REPL a
raise (Type -> REPLException
TypeNotTestable Type
ty)

  where
  testingMsg :: [Char]
testingMsg = [Char]
"Testing... "

  interruptedExhaust :: Integer -> Integer -> [Char]
interruptedExhaust Integer
testNum Integer
sz =
     let percent :: Double
percent = (Double
100.0 :: Double) Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
testNum) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
sz
         showValNum :: [Char]
showValNum
            | Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
20::Integer) =
              [Char]
"2^^" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer -> Integer
lg2 Integer
sz)
            | Bool
otherwise = Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
sz
      in [Char]
"Test coverage: "
            [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2) Double
percent [Char]
"% ("
            [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
testNum [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" of "
            [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
showValNum
            [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" values)"

  coverageString :: Integer -> Integer -> [Char]
coverageString Integer
testNum Integer
sz =
     let (Double
percent, Double
expectedUnique) = Integer -> Integer -> (Double, Double)
expectedCoverage Integer
testNum Integer
sz
         showValNum :: [Char]
showValNum
           | Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
20::Integer) =
             [Char]
"2^^" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer -> Integer
lg2 Integer
sz)
           | Bool
otherwise = Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
sz
     in [Char]
"Expected test coverage: "
       [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2) Double
percent [Char]
"% ("
       [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0) Double
expectedUnique [Char]
" of "
       [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
showValNum
       [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" values)"

  totProgressWidth :: Int
totProgressWidth = Int
4    -- 100%

  lg2 :: Integer -> Integer
  lg2 :: Integer -> Integer
lg2 Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
1024::Int) = Integer
1024 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer
lg2 (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
1024::Int))
        | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0       = Integer
0
        | Bool
otherwise    = let valNumD :: Double
valNumD = Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
x :: Double
                         in Double -> Integer
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Double -> Integer) -> Double -> Integer
forall a b. (a -> b) -> a -> b
$ Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 Double
valNumD :: Integer

  prt :: [Char] -> REPL ()
prt [Char]
msg   = [Char] -> REPL ()
rPutStr [Char]
msg REPL () -> REPL () -> REPL ()
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO () -> REPL ()
forall a. IO a -> REPL a
io (Handle -> IO ()
hFlush Handle
stdout)

  ppProgress :: IORef (Maybe [Char]) -> IORef a -> a -> a -> REPL ()
ppProgress IORef (Maybe [Char])
percentRef IORef a
testsRef a
this a
tot =
    do IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
testsRef a
this
       let percent :: [Char]
percent = a -> [Char]
forall a. Show a => a -> [Char]
show (a -> a -> a
forall a. Integral a => a -> a -> a
div (a
100 a -> a -> a
forall a. Num a => a -> a -> a
* a
this) a
tot) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"%"
           width :: Int
width   = [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
percent
           pad :: [Char]
pad     = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
totProgressWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
width) Char
' '
       REPL () -> REPL ()
unlessBatch (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
         do Maybe [Char]
oldPercent <- IO (Maybe [Char]) -> REPL (Maybe [Char])
forall a. IO a -> REPL a
io (IO (Maybe [Char]) -> REPL (Maybe [Char]))
-> IO (Maybe [Char]) -> REPL (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ IORef (Maybe [Char]) -> IO (Maybe [Char])
forall a. IORef a -> IO a
readIORef IORef (Maybe [Char])
percentRef
            case Maybe [Char]
oldPercent of
              Maybe [Char]
Nothing ->
                do IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe [Char]) -> Maybe [Char] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe [Char])
percentRef ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
percent)
                   [Char] -> REPL ()
prt ([Char]
pad [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
percent)
              Just [Char]
p | [Char]
p [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
percent ->
                do IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe [Char]) -> Maybe [Char] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe [Char])
percentRef ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
percent)
                   REPL ()
delProgress
                   [Char] -> REPL ()
prt ([Char]
pad [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
percent)
              Maybe [Char]
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  del :: Int -> REPL ()
del Int
n       = REPL () -> REPL ()
unlessBatch
              (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char] -> REPL ()
prt (Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
n Char
'\BS' [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
n Char
' ' [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
n Char
'\BS')
  delTesting :: REPL ()
delTesting  = Int -> REPL ()
del ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
testingMsg)
  delProgress :: REPL ()
delProgress = Int -> REPL ()
del Int
totProgressWidth


ppReport :: [E.TValue] -> Bool -> TestReport -> REPL ()
ppReport :: [TValue] -> Bool -> TestReport -> REPL ()
ppReport [TValue]
_tys Bool
isExhaustive (TestReport Doc
_exprDoc TestResult
Pass Integer
testNum Maybe Integer
_testPossible) =
    do [Char] -> REPL ()
rPutStrLn ([Char]
"Passed " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
testNum [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" tests.")
       Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isExhaustive ([Char] -> REPL ()
rPutStrLn [Char]
"Q.E.D.")
ppReport [TValue]
tys Bool
_ (TestReport Doc
exprDoc TestResult
failure Integer
_testNum Maybe Integer
_testPossible) =
    do [TValue] -> Doc -> TestResult -> REPL ()
ppFailure [TValue]
tys Doc
exprDoc TestResult
failure

ppFailure :: [E.TValue] -> Doc -> TestResult -> REPL ()
ppFailure :: [TValue] -> Doc -> TestResult -> REPL ()
ppFailure [TValue]
tys Doc
exprDoc TestResult
failure = do
    ~(EnvBool Bool
showEx) <- [Char] -> REPL EnvVal
getUser [Char]
"showExamples"

    [Value]
vs <- case TestResult
failure of
            FailFalse [Value]
vs ->
              do [Char] -> REPL ()
rPutStrLn [Char]
"Counterexample"
                 Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showEx (CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
PredicateFalsified Doc
exprDoc [Value]
vs)
                 [Value] -> REPL [Value]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs
            FailError EvalErrorEx
err [Value]
vs
              | [Value] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Value]
vs Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
showEx ->
                do [Char] -> REPL ()
rPutStrLn [Char]
"ERROR"
                   Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (EvalErrorEx -> Doc
forall a. PP a => a -> Doc
pp EvalErrorEx
err)
                   [Value] -> REPL [Value]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs
              | Bool
otherwise ->
                do [Char] -> REPL ()
rPutStrLn [Char]
"ERROR for the following inputs:"
                   CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
SafetyViolation Doc
exprDoc [Value]
vs
                   Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (EvalErrorEx -> Doc
forall a. PP a => a -> Doc
pp EvalErrorEx
err)
                   [Value] -> REPL [Value]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Value]
vs

            TestResult
Pass -> [Char] -> [[Char]] -> REPL [Value]
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.REPL.Command" [[Char]
"unexpected Test.Pass"]

    -- bind the 'it' variable
    case ([TValue]
tys,[Value]
vs) of
      ([TValue
t],[Value
v]) -> TValue -> Value -> REPL ()
bindItVariableVal TValue
t Value
v
      ([TValue], [Value])
_ -> let fs :: [Ident]
fs = [ [Char] -> Ident
M.packIdent ([Char]
"arg" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
i::Int)) | Int
i <- [ Int
1 .. ] ]
               t :: TValue
t = RecordMap Ident TValue -> TValue
E.TVRec ([(Ident, TValue)] -> RecordMap Ident TValue
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([Ident] -> [TValue] -> [(Ident, TValue)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fs [TValue]
tys))
               v :: Value
v = RecordMap Ident (SEval Concrete Value) -> Value
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
E.VRecord ([(Ident, Eval Value)] -> RecordMap Ident (Eval Value)
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([Ident] -> [Eval Value] -> [(Ident, Eval Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
fs ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
forall (m :: * -> *) a. Monad m => a -> m a
return [Value]
vs)))
           in TValue -> Value -> REPL ()
bindItVariableVal TValue
t Value
v


-- | This function computes the expected coverage percentage and
-- expected number of unique test vectors when using random testing.
--
-- The expected test coverage proportion is:
--  @1 - ((n-1)/n)^k@
--
-- This formula takes into account the fact that test vectors are chosen
-- uniformly at random _with replacement_, and thus the same vectors
-- may be generated multiple times.  If the test vectors were chosen
-- randomly without replacement, the proportion would instead be @k/n@.
--
-- We compute raising to the @k@ power in the log domain to improve
-- numerical precision. The equivalant comptutation is:
--   @-expm1( k * log1p (-1/n) )@
--
-- Where @expm1(x) = exp(x) - 1@ and @log1p(x) = log(1 + x)@.
--
-- However, if @sz@ is large enough, even carefully preserving
-- precision may not be enough to get sensible results.  In such
-- situations, we expect the naive approximation @k/n@ to be very
-- close to accurate and the expected number of unique values is
-- essentially equal to the number of tests.
expectedCoverage :: Integer -> Integer -> (Double, Double)
expectedCoverage :: Integer -> Integer -> (Double, Double)
expectedCoverage Integer
testNum Integer
sz =
    -- If the Double computation has enough precision, use the
    --  "with replacement" formula.
    if Integer
testNum Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& Double
proportion Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0 then
       (Double
100.0 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
proportion, Double
szD Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
proportion)
    else
       (Double
100.0 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
naiveProportion, Double
numD)

  where
   szD :: Double
   szD :: Double
szD = Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
sz

   numD :: Double
   numD :: Double
numD = Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
testNum

   naiveProportion :: Double
naiveProportion = Double
numD Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
szD

   proportion :: Double
proportion = Double -> Double
forall a. Num a => a -> a
negate (Double -> Double
forall a. Floating a => a -> a
expm1 (Double
numD Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double -> Double
forall a. Floating a => a -> a
log1p (Double -> Double
forall a. Num a => a -> a
negate (Double -> Double
forall a. Fractional a => a -> a
recip Double
szD))))

satCmd, proveCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
satCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
satCmd = Bool -> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
cmdProveSat Bool
True
proveCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
proveCmd = Bool -> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
cmdProveSat Bool
False

showProverStats :: Maybe String -> ProverStats -> REPL ()
showProverStats :: Maybe [Char] -> ProverStats -> REPL ()
showProverStats Maybe [Char]
mprover ProverStats
stat = [Char] -> REPL ()
rPutStrLn [Char]
msg
  where

  msg :: [Char]
msg = [Char]
"(Total Elapsed Time: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ProverStats -> [Char]
SBV.showTDiff ProverStats
stat [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
        [Char] -> ShowS -> Maybe [Char] -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"" (\[Char]
p -> [Char]
", using " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
p) Maybe [Char]
mprover [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

rethrowErrorCall :: REPL a -> REPL a
rethrowErrorCall :: forall a. REPL a -> REPL a
rethrowErrorCall REPL a
m = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
r -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
r IO a -> [Handler a] -> IO a
forall a. IO a -> [Handler a] -> IO a
`X.catches` [Handler a]
forall {a}. [Handler a]
hs)
  where
    hs :: [Handler a]
hs =
      [ (ErrorCall -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((ErrorCall -> IO a) -> Handler a)
-> (ErrorCall -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ (X.ErrorCallWithLocation [Char]
s [Char]
_) -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO ([Char] -> REPLException
SBVError [Char]
s)
      , (SBVException -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((SBVException -> IO a) -> Handler a)
-> (SBVException -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ SBVException
e -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (SBVException -> REPLException
SBVException SBVException
e)
      , (SBVPortfolioException -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((SBVPortfolioException -> IO a) -> Handler a)
-> (SBVPortfolioException -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ SBVPortfolioException
e -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (SBVPortfolioException -> REPLException
SBVPortfolioException SBVPortfolioException
e)
      , (W4Exception -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
X.Handler ((W4Exception -> IO a) -> Handler a)
-> (W4Exception -> IO a) -> Handler a
forall a b. (a -> b) -> a -> b
$ \ W4Exception
e -> REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (W4Exception -> REPLException
W4Exception W4Exception
e)
      ]

-- | Attempts to prove the given term is safe for all inputs
safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
safeCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
safeCmd [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
  [Char]
proverName <- [Char] -> REPL [Char]
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"prover"
  [Char]
fileName   <- [Char] -> REPL [Char]
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"smtFile"
  let mfile :: Maybe [Char]
mfile = if [Char]
fileName [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"-" then Maybe [Char]
forall a. Maybe a
Nothing else [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
fileName
  Expr PName
pexpr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  let exprDoc :: Doc
exprDoc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr PName
pexpr) -- function application has precedence 3

  let rng :: Range
rng = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe ((Int, Int) -> Maybe [Char] -> Range
mkInteractiveRange (Int, Int)
pos Maybe [Char]
fnm) (Expr PName -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr PName
pexpr)
  (Expr Name
_,Expr
texpr,Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
pexpr

  if [Char]
proverName [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]
"offline",[Char]
"sbv-offline",[Char]
"w4-offline"] then
    do Bool
success <- [Char] -> QueryType -> Expr -> Schema -> Maybe [Char] -> REPL Bool
offlineProveSat [Char]
proverName QueryType
SafetyQuery Expr
texpr Schema
schema Maybe [Char]
mfile
       CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = success }
  else
     do (Maybe [Char]
firstProver,ProverResult
result,ProverStats
stats) <- REPL (Maybe [Char], ProverResult, ProverStats)
-> REPL (Maybe [Char], ProverResult, ProverStats)
forall a. REPL a -> REPL a
rethrowErrorCall ([Char]
-> QueryType
-> Expr
-> Schema
-> Maybe [Char]
-> REPL (Maybe [Char], ProverResult, ProverStats)
onlineProveSat [Char]
proverName QueryType
SafetyQuery Expr
texpr Schema
schema Maybe [Char]
mfile)
        CommandResult
cmdResult <- case ProverResult
result of
          ProverResult
EmptyResult         ->
            [Char] -> [[Char]] -> REPL CommandResult
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"REPL.Command" [ [Char]
"got EmptyResult for online prover query" ]

          ProverError [Char]
msg ->
            do [Char] -> REPL ()
rPutStrLn [Char]
msg
               CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }

          ThmResult [TValue]
_ts ->
            do [Char] -> REPL ()
rPutStrLn [Char]
"Safe"
               CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

          CounterExample CounterExampleType
cexType SatResult
tevs -> do
            [Char] -> REPL ()
rPutStrLn [Char]
"Counterexample"
            let tes :: [(TValue, Expr)]
tes = ((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
t,Expr
e,Value
_) -> (TValue
t,Expr
e)) SatResult
tevs
                vs :: [Value]
vs  = ((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
_,Expr
_,Value
v) -> Value
v)     SatResult
tevs

            (TValue
t,Expr
e) <- [Char]
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult [Char]
"counterexample" Range
rng Bool
False ([(TValue, Expr)] -> Either [TValue] [(TValue, Expr)]
forall a b. b -> Either a b
Right [(TValue, Expr)]
tes)

            ~(EnvBool Bool
yes) <- [Char] -> REPL EnvVal
getUser [Char]
"showExamples"
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
cexType Doc
exprDoc [Value]
vs
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> Schema -> [Value] -> REPL ()
printSafetyViolation Expr
texpr Schema
schema [Value]
vs

            REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
t Expr
e

            CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }

          AllSatResult [SatResult]
_ -> do
            [Char] -> [[Char]] -> REPL CommandResult
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"REPL.Command" [[Char]
"Unexpected AllSAtResult for ':safe' call"]

        Bool
seeStats <- REPL Bool
getUserShowProverStats
        Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
seeStats (Maybe [Char] -> ProverStats -> REPL ()
showProverStats Maybe [Char]
firstProver ProverStats
stats)
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
cmdResult


-- | Console-specific version of 'proveSat'. Prints output to the
-- console, and binds the @it@ variable to a record whose form depends
-- on the expression given. See ticket #66 for a discussion of this
-- design.
cmdProveSat :: Bool -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
cmdProveSat :: Bool -> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
cmdProveSat Bool
isSat [Char]
"" (Int, Int)
_pos Maybe [Char]
_fnm =
  do ([(Name, IfaceDecl)]
xs,NameDisp
disp) <- REPL ([(Name, IfaceDecl)], NameDisp)
getPropertyNames
     let nameStr :: a -> [Char]
nameStr a
x = Doc -> [Char]
forall a. Show a => a -> [Char]
show (NameDisp -> Doc -> Doc
fixNameDisp NameDisp
disp (a -> Doc
forall a. PP a => a -> Doc
pp a
x))
     if [(Name, IfaceDecl)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, IfaceDecl)]
xs
        then do
          [Char] -> REPL ()
rPutStrLn [Char]
"There are no properties in scope."
          CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
        else do
          let check :: Bool -> (Name, IfaceDecl) -> REPL Bool
check Bool
acc (Name
x,IfaceDecl
d) = do
                let str :: [Char]
str = Name -> [Char]
forall {a}. PP a => a -> [Char]
nameStr Name
x
                if Bool
isSat
                  then [Char] -> REPL ()
rPutStr ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
":sat "   [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
str [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\t"
                  else [Char] -> REPL ()
rPutStr ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
":prove " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
str [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\t"
                let texpr :: Expr
texpr = Name -> Expr
T.EVar Name
x
                let schema :: Schema
schema = IfaceDecl -> Schema
M.ifDeclSig IfaceDecl
d
                NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
                let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
texpr)
                Bool
success <- Bool -> Range -> Doc -> Expr -> Schema -> REPL Bool
proveSatExpr Bool
isSat (Name -> Range
M.nameLoc Name
x) Doc
doc Expr
texpr Schema
schema
                Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> REPL Bool) -> Bool -> REPL Bool
forall a b. (a -> b) -> a -> b
$! Bool
acc Bool -> Bool -> Bool
&& Bool
success
          Bool
success <- (Bool -> (Name, IfaceDecl) -> REPL Bool)
-> Bool -> [(Name, IfaceDecl)] -> REPL Bool
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Bool -> (Name, IfaceDecl) -> REPL Bool
check Bool
True [(Name, IfaceDecl)]
xs
          CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = success }


cmdProveSat Bool
isSat [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
  Expr PName
pexpr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  NameDisp
nd <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  let doc :: Doc
doc = NameDisp -> Doc -> Doc
fixNameDisp NameDisp
nd (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr PName
pexpr) -- function application has precedence 3
  (Expr Name
_,Expr
texpr,Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
pexpr
  let rng :: Range
rng = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe ((Int, Int) -> Maybe [Char] -> Range
mkInteractiveRange (Int, Int)
pos Maybe [Char]
fnm) (Expr PName -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr PName
pexpr)
  Bool
success <- Bool -> Range -> Doc -> Expr -> Schema -> REPL Bool
proveSatExpr Bool
isSat Range
rng Doc
doc Expr
texpr Schema
schema
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = success }

proveSatExpr ::
  Bool ->
  Range ->
  Doc ->
  T.Expr ->
  T.Schema ->
  REPL Bool
proveSatExpr :: Bool -> Range -> Doc -> Expr -> Schema -> REPL Bool
proveSatExpr Bool
isSat Range
rng Doc
exprDoc Expr
texpr Schema
schema = do
  let cexStr :: [Char]
cexStr | Bool
isSat = [Char]
"satisfying assignment"
             | Bool
otherwise = [Char]
"counterexample"
  QueryType
qtype <- if Bool
isSat then SatNum -> QueryType
SatQuery (SatNum -> QueryType) -> REPL SatNum -> REPL QueryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL SatNum
getUserSatNum else QueryType -> REPL QueryType
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QueryType
ProveQuery
  [Char]
proverName <- [Char] -> REPL [Char]
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"prover"
  [Char]
fileName   <- [Char] -> REPL [Char]
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"smtFile"
  let mfile :: Maybe [Char]
mfile = if [Char]
fileName [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"-" then Maybe [Char]
forall a. Maybe a
Nothing else [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
fileName

  if [Char]
proverName [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]
"offline",[Char]
"sbv-offline",[Char]
"w4-offline"] then
     [Char] -> QueryType -> Expr -> Schema -> Maybe [Char] -> REPL Bool
offlineProveSat [Char]
proverName QueryType
qtype Expr
texpr Schema
schema Maybe [Char]
mfile
  else
     do (Maybe [Char]
firstProver,ProverResult
result,ProverStats
stats) <- REPL (Maybe [Char], ProverResult, ProverStats)
-> REPL (Maybe [Char], ProverResult, ProverStats)
forall a. REPL a -> REPL a
rethrowErrorCall ([Char]
-> QueryType
-> Expr
-> Schema
-> Maybe [Char]
-> REPL (Maybe [Char], ProverResult, ProverStats)
onlineProveSat [Char]
proverName QueryType
qtype Expr
texpr Schema
schema Maybe [Char]
mfile)
        Bool
success <- case ProverResult
result of
          ProverResult
EmptyResult         ->
            [Char] -> [[Char]] -> REPL Bool
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"REPL.Command" [ [Char]
"got EmptyResult for online prover query" ]

          ProverError [Char]
msg -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn [Char]
msg

          ThmResult [TValue]
ts -> do
            [Char] -> REPL ()
rPutStrLn (if Bool
isSat then [Char]
"Unsatisfiable" else [Char]
"Q.E.D.")
            (TValue
t, Expr
e) <- [Char]
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult [Char]
cexStr Range
rng (Bool -> Bool
not Bool
isSat) ([TValue] -> Either [TValue] [(TValue, Expr)]
forall a b. a -> Either a b
Left [TValue]
ts)
            REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
t Expr
e
            Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool
not Bool
isSat)

          CounterExample CounterExampleType
cexType SatResult
tevs -> do
            [Char] -> REPL ()
rPutStrLn [Char]
"Counterexample"
            let tes :: [(TValue, Expr)]
tes = ((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
t,Expr
e,Value
_) -> (TValue
t,Expr
e)) SatResult
tevs
                vs :: [Value]
vs  = ((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map ( \(TValue
_,Expr
_,Value
v) -> Value
v)     SatResult
tevs

            (TValue
t,Expr
e) <- [Char]
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult [Char]
cexStr Range
rng Bool
isSat ([(TValue, Expr)] -> Either [TValue] [(TValue, Expr)]
forall a b. b -> Either a b
Right [(TValue, Expr)]
tes)

            ~(EnvBool Bool
yes) <- [Char] -> REPL EnvVal
getUser [Char]
"showExamples"
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ CounterExampleType -> Doc -> [Value] -> REPL ()
printCounterexample CounterExampleType
cexType Doc
exprDoc [Value]
vs

            -- if there's a safety violation, evalute the counterexample to
            -- find and print the actual concrete error
            case CounterExampleType
cexType of
              CounterExampleType
SafetyViolation -> Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> Schema -> [Value] -> REPL ()
printSafetyViolation Expr
texpr Schema
schema [Value]
vs
              CounterExampleType
_ -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

            REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
t Expr
e
            Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

          AllSatResult [SatResult]
tevss -> do
            [Char] -> REPL ()
rPutStrLn [Char]
"Satisfiable"
            let tess :: [[(TValue, Expr)]]
tess = (SatResult -> [(TValue, Expr)])
-> [SatResult] -> [[(TValue, Expr)]]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> (TValue, Expr))
 -> SatResult -> [(TValue, Expr)])
-> ((TValue, Expr, Value) -> (TValue, Expr))
-> SatResult
-> [(TValue, Expr)]
forall a b. (a -> b) -> a -> b
$ \(TValue
t,Expr
e,Value
_) -> (TValue
t,Expr
e)) [SatResult]
tevss
                vss :: [[Value]]
vss  = (SatResult -> [Value]) -> [SatResult] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (((TValue, Expr, Value) -> Value) -> SatResult -> [Value])
-> ((TValue, Expr, Value) -> Value) -> SatResult -> [Value]
forall a b. (a -> b) -> a -> b
$ \(TValue
_,Expr
_,Value
v) -> Value
v)     [SatResult]
tevss
            [(TValue, Expr)]
resultRecs <- ([(TValue, Expr)] -> REPL (TValue, Expr))
-> [[(TValue, Expr)]] -> REPL [(TValue, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Char]
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult [Char]
cexStr Range
rng Bool
isSat (Either [TValue] [(TValue, Expr)] -> REPL (TValue, Expr))
-> ([(TValue, Expr)] -> Either [TValue] [(TValue, Expr)])
-> [(TValue, Expr)]
-> REPL (TValue, Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TValue, Expr)] -> Either [TValue] [(TValue, Expr)]
forall a b. b -> Either a b
Right) [[(TValue, Expr)]]
tess
            let collectTes :: [(a, b)] -> (a, [b])
collectTes [(a, b)]
tes = (a
t, [b]
es)
                  where
                    ([a]
ts, [b]
es) = [(a, b)] -> ([a], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, b)]
tes
                    t :: a
t = case [a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
ts of
                          [a
t'] -> a
t'
                          [a]
_ -> [Char] -> [[Char]] -> a
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"REPL.Command.onlineProveSat"
                                 [ [Char]
"satisfying assignments with different types" ]
                (TValue
ty, [Expr]
exprs) =
                  case [(TValue, Expr)]
resultRecs of
                    [] -> [Char] -> [[Char]] -> (TValue, [Expr])
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"REPL.Command.onlineProveSat"
                            [ [Char]
"no satisfying assignments after mkSolverResult" ]
                    [(TValue
t, Expr
e)] -> (TValue
t, [Expr
e])
                    [(TValue, Expr)]
_        -> [(TValue, Expr)] -> (TValue, [Expr])
forall {a} {b}. Eq a => [(a, b)] -> (a, [b])
collectTes [(TValue, Expr)]
resultRecs

            ~(EnvBool Bool
yes) <- [Char] -> REPL EnvVal
getUser [Char]
"showExamples"
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
yes (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ [[Value]] -> ([Value] -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[Value]]
vss (Doc -> [Value] -> REPL ()
printSatisfyingModel Doc
exprDoc)

            let numModels :: Int
numModels = [SatResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SatResult]
tevss
            Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
numModels Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) ([Char] -> REPL ()
rPutStrLn ([Char]
"Models found: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
numModels))

            case [Expr]
exprs of
              [Expr
e] -> REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
ty Expr
e
              [Expr]
_   -> TValue -> [Expr] -> REPL ()
bindItVariables TValue
ty [Expr]
exprs

            Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

        Bool
seeStats <- REPL Bool
getUserShowProverStats
        Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
seeStats (Maybe [Char] -> ProverStats -> REPL ()
showProverStats Maybe [Char]
firstProver ProverStats
stats)
        Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
success


printSafetyViolation :: T.Expr -> T.Schema -> [E.GenValue Concrete] -> REPL ()
printSafetyViolation :: Expr -> Schema -> [Value] -> REPL ()
printSafetyViolation Expr
texpr Schema
schema [Value]
vs =
    REPL () -> (REPLException -> REPL ()) -> REPL ()
forall a. REPL a -> (REPLException -> REPL a) -> REPL a
catch
      (do Value
fn <- Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
texpr Schema
schema REPL (Maybe (Value, Type))
-> (Maybe (Value, Type) -> REPL Value) -> REPL Value
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe (Value, Type)
mb_res -> case Maybe (Value, Type)
mb_res of
            Just (Value
fn, Type
_) -> Value -> REPL Value
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
fn
            Maybe (Value, Type)
Nothing -> REPLException -> REPL Value
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
schema)
          Eval () -> REPL ()
forall a. Eval a -> REPL a
rEval (Value -> Eval ()
Value -> SEval Concrete ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
E.forceValue (Value -> Eval ()) -> Eval Value -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Value -> Value -> Eval Value) -> Value -> [Value] -> Eval Value
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Value
f Value
v -> Concrete -> Value -> SEval Concrete Value -> SEval Concrete Value
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
E.fromVFun Concrete
Concrete Value
f (Value -> Eval Value
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v)) Value
fn [Value]
vs))
      (\case
          EvalError EvalErrorEx
eex -> [Char] -> REPL ()
rPutStrLn (Doc -> [Char]
forall a. Show a => a -> [Char]
show (EvalErrorEx -> Doc
forall a. PP a => a -> Doc
pp EvalErrorEx
eex))
          REPLException
ex -> REPLException -> REPL ()
forall a. REPLException -> REPL a
raise REPLException
ex)

onlineProveSat ::
  String ->
  QueryType ->
  T.Expr ->
  T.Schema ->
  Maybe FilePath ->
  REPL (Maybe String,ProverResult,ProverStats)
onlineProveSat :: [Char]
-> QueryType
-> Expr
-> Schema
-> Maybe [Char]
-> REPL (Maybe [Char], ProverResult, ProverStats)
onlineProveSat [Char]
proverName QueryType
qtype Expr
expr Schema
schema Maybe [Char]
mfile = do
  Bool
verbose <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"debug"
  Bool
modelValidate <- REPL Bool
getUserProverValidate
  Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
expr
  Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
schema
  [DeclGroup]
decls <- (DynamicEnv -> [DeclGroup]) -> REPL DynamicEnv -> REPL [DeclGroup]
forall a b. (a -> b) -> REPL a -> REPL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DynamicEnv -> [DeclGroup]
M.deDecls REPL DynamicEnv
getDynEnv
  IORef ProverStats
timing <- IO (IORef ProverStats) -> REPL (IORef ProverStats)
forall a. IO a -> REPL a
io (ProverStats -> IO (IORef ProverStats)
forall a. a -> IO (IORef a)
newIORef ProverStats
0)
  ~(EnvBool Bool
ignoreSafety) <- [Char] -> REPL EnvVal
getUser [Char]
"ignoreSafety"
  ~(EnvNum Int
timeoutSec) <- [Char] -> REPL EnvVal
getUser [Char]
"proverTimeout"
  let cmd :: ProverCommand
cmd = ProverCommand {
          pcQueryType :: QueryType
pcQueryType    = QueryType
qtype
        , pcProverName :: [Char]
pcProverName   = [Char]
proverName
        , pcVerbose :: Bool
pcVerbose      = Bool
verbose
        , pcValidate :: Bool
pcValidate     = Bool
modelValidate
        , pcProverStats :: IORef ProverStats
pcProverStats  = IORef ProverStats
timing
        , pcExtraDecls :: [DeclGroup]
pcExtraDecls   = [DeclGroup]
decls
        , pcSmtFile :: Maybe [Char]
pcSmtFile      = Maybe [Char]
mfile
        , pcExpr :: Expr
pcExpr         = Expr
expr
        , pcSchema :: Schema
pcSchema       = Schema
schema
        , pcIgnoreSafety :: Bool
pcIgnoreSafety = Bool
ignoreSafety
        }
  (Maybe [Char]
firstProver, ProverResult
res) <- REPL (Either SBVProverConfig W4ProverConfig)
getProverConfig REPL (Either SBVProverConfig W4ProverConfig)
-> (Either SBVProverConfig W4ProverConfig
    -> REPL (Maybe [Char], ProverResult))
-> REPL (Maybe [Char], ProverResult)
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Left SBVProverConfig
sbvCfg -> ModuleCmd (Maybe [Char], ProverResult)
-> REPL (Maybe [Char], ProverResult)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe [Char], ProverResult)
 -> REPL (Maybe [Char], ProverResult))
-> ModuleCmd (Maybe [Char], ProverResult)
-> REPL (Maybe [Char], ProverResult)
forall a b. (a -> b) -> a -> b
$ SBVProverConfig
-> Int -> ProverCommand -> ModuleCmd (Maybe [Char], ProverResult)
SBV.satProve SBVProverConfig
sbvCfg Int
timeoutSec ProverCommand
cmd
       Right W4ProverConfig
w4Cfg ->
         do ~(EnvBool Bool
hashConsing) <- [Char] -> REPL EnvVal
getUser [Char]
"hashConsing"
            ~(EnvBool Bool
warnUninterp) <- [Char] -> REPL EnvVal
getUser [Char]
"warnUninterp"
            ModuleCmd (Maybe [Char], ProverResult)
-> REPL (Maybe [Char], ProverResult)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe [Char], ProverResult)
 -> REPL (Maybe [Char], ProverResult))
-> ModuleCmd (Maybe [Char], ProverResult)
-> REPL (Maybe [Char], ProverResult)
forall a b. (a -> b) -> a -> b
$ W4ProverConfig
-> Bool
-> Bool
-> Int
-> ProverCommand
-> ModuleCmd (Maybe [Char], ProverResult)
W4.satProve W4ProverConfig
w4Cfg Bool
hashConsing Bool
warnUninterp Int
timeoutSec ProverCommand
cmd

  ProverStats
stas <- IO ProverStats -> REPL ProverStats
forall a. IO a -> REPL a
io (IORef ProverStats -> IO ProverStats
forall a. IORef a -> IO a
readIORef IORef ProverStats
timing)
  (Maybe [Char], ProverResult, ProverStats)
-> REPL (Maybe [Char], ProverResult, ProverStats)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char]
firstProver,ProverResult
res,ProverStats
stas)

offlineProveSat :: String -> QueryType -> T.Expr -> T.Schema -> Maybe FilePath -> REPL Bool
offlineProveSat :: [Char] -> QueryType -> Expr -> Schema -> Maybe [Char] -> REPL Bool
offlineProveSat [Char]
proverName QueryType
qtype Expr
expr Schema
schema Maybe [Char]
mfile = do
  Bool
verbose <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"debug"
  Bool
modelValidate <- REPL Bool
getUserProverValidate

  [DeclGroup]
decls <- (DynamicEnv -> [DeclGroup]) -> REPL DynamicEnv -> REPL [DeclGroup]
forall a b. (a -> b) -> REPL a -> REPL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DynamicEnv -> [DeclGroup]
M.deDecls REPL DynamicEnv
getDynEnv
  IORef ProverStats
timing <- IO (IORef ProverStats) -> REPL (IORef ProverStats)
forall a. IO a -> REPL a
io (ProverStats -> IO (IORef ProverStats)
forall a. a -> IO (IORef a)
newIORef ProverStats
0)
  ~(EnvBool Bool
ignoreSafety) <- [Char] -> REPL EnvVal
getUser [Char]
"ignoreSafety"
  let cmd :: ProverCommand
cmd = ProverCommand {
          pcQueryType :: QueryType
pcQueryType    = QueryType
qtype
        , pcProverName :: [Char]
pcProverName   = [Char]
proverName
        , pcVerbose :: Bool
pcVerbose      = Bool
verbose
        , pcValidate :: Bool
pcValidate     = Bool
modelValidate
        , pcProverStats :: IORef ProverStats
pcProverStats  = IORef ProverStats
timing
        , pcExtraDecls :: [DeclGroup]
pcExtraDecls   = [DeclGroup]
decls
        , pcSmtFile :: Maybe [Char]
pcSmtFile      = Maybe [Char]
mfile
        , pcExpr :: Expr
pcExpr         = Expr
expr
        , pcSchema :: Schema
pcSchema       = Schema
schema
        , pcIgnoreSafety :: Bool
pcIgnoreSafety = Bool
ignoreSafety
        }

  [Char] -> IO ()
put <- REPL ([Char] -> IO ())
getPutStr
  let putLn :: [Char] -> IO ()
putLn [Char]
x = [Char] -> IO ()
put ([Char]
x [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
  let displayMsg :: IO ()
displayMsg =
        do let filename :: [Char]
filename = [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"standard output" Maybe [Char]
mfile
           let satWord :: [Char]
satWord = case QueryType
qtype of
                           SatQuery SatNum
_  -> [Char]
"satisfiability"
                           QueryType
ProveQuery  -> [Char]
"validity"
                           QueryType
SafetyQuery -> [Char]
"safety"
           [Char] -> IO ()
putLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$
               [Char]
"Writing to SMT-Lib file " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
filename [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"..."
           [Char] -> IO ()
putLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$
             [Char]
"To determine the " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
satWord [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
             [Char]
" of the expression, use an external SMT solver."

  REPL (Either SBVProverConfig W4ProverConfig)
getProverConfig REPL (Either SBVProverConfig W4ProverConfig)
-> (Either SBVProverConfig W4ProverConfig -> REPL Bool)
-> REPL Bool
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left SBVProverConfig
sbvCfg ->
      do Either [Char] [Char]
result <- ModuleCmd (Either [Char] [Char]) -> REPL (Either [Char] [Char])
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Either [Char] [Char]) -> REPL (Either [Char] [Char]))
-> ModuleCmd (Either [Char] [Char]) -> REPL (Either [Char] [Char])
forall a b. (a -> b) -> a -> b
$ SBVProverConfig
-> ProverCommand -> ModuleCmd (Either [Char] [Char])
SBV.satProveOffline SBVProverConfig
sbvCfg ProverCommand
cmd
         case Either [Char] [Char]
result of
           Left [Char]
msg -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn [Char]
msg
           Right [Char]
smtlib -> do
             IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ IO ()
displayMsg
             case Maybe [Char]
mfile of
               Just [Char]
path -> IO () -> REPL ()
forall a. IO a -> REPL a
io (IO () -> REPL ()) -> IO () -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> IO ()
writeFile [Char]
path [Char]
smtlib
               Maybe [Char]
Nothing -> [Char] -> REPL ()
rPutStr [Char]
smtlib
             Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

    Right W4ProverConfig
_w4Cfg ->
      do ~(EnvBool Bool
hashConsing) <- [Char] -> REPL EnvVal
getUser [Char]
"hashConsing"
         ~(EnvBool Bool
warnUninterp) <- [Char] -> REPL EnvVal
getUser [Char]
"warnUninterp"
         Maybe [Char]
result <- ModuleCmd (Maybe [Char]) -> REPL (Maybe [Char])
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Maybe [Char]) -> REPL (Maybe [Char]))
-> ModuleCmd (Maybe [Char]) -> REPL (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> ProverCommand
-> ((Handle -> IO ()) -> IO ())
-> ModuleCmd (Maybe [Char])
W4.satProveOffline Bool
hashConsing Bool
warnUninterp ProverCommand
cmd (((Handle -> IO ()) -> IO ()) -> ModuleCmd (Maybe [Char]))
-> ((Handle -> IO ()) -> IO ()) -> ModuleCmd (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ \Handle -> IO ()
f ->
                     do IO ()
displayMsg
                        case Maybe [Char]
mfile of
                          Just [Char]
path ->
                            IO Handle -> (Handle -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
X.bracket ([Char] -> IOMode -> IO Handle
openFile [Char]
path IOMode
WriteMode) Handle -> IO ()
hClose Handle -> IO ()
f
                          Maybe [Char]
Nothing ->
                            [Char] -> (Handle -> IO ()) -> IO ()
forall a. [Char] -> (Handle -> IO a) -> IO a
withRWTempFile [Char]
"smtOutput.tmp" ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h ->
                              do Handle -> IO ()
f Handle
h
                                 Handle -> SeekMode -> Integer -> IO ()
hSeek Handle
h SeekMode
AbsoluteSeek Integer
0
                                 Handle -> IO [Char]
hGetContents Handle
h IO [Char] -> ([Char] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Char] -> IO ()
put

         case Maybe [Char]
result of
           Just [Char]
msg -> [Char] -> REPL ()
rPutStrLn [Char]
msg
           Maybe [Char]
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True


rIdent :: M.Ident
rIdent :: Ident
rIdent  = [Char] -> Ident
M.packIdent [Char]
"result"

-- | Make a type/expression pair that is suitable for binding to @it@
-- after running @:sat@ or @:prove@
mkSolverResult ::
  String ->
  Range ->
  Bool ->
  Either [E.TValue] [(E.TValue, T.Expr)] ->
  REPL (E.TValue, T.Expr)
mkSolverResult :: [Char]
-> Range
-> Bool
-> Either [TValue] [(TValue, Expr)]
-> REPL (TValue, Expr)
mkSolverResult [Char]
thing Range
rng Bool
result Either [TValue] [(TValue, Expr)]
earg =
  do PrimMap
prims <- REPL PrimMap
getPrimMap
     let addError :: TValue -> (TValue, Expr)
addError TValue
t = (TValue
t, Range -> Expr -> Expr
T.ELocated Range
rng (PrimMap -> Type -> [Char] -> Expr
T.eError PrimMap
prims (TValue -> Type
E.tValTy TValue
t) ([Char]
"no " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
thing [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" available")))

         argF :: [((Ident, TValue), (Ident, Expr))]
argF = case Either [TValue] [(TValue, Expr)]
earg of
                  Left [TValue]
ts   -> [(TValue, Expr)] -> [((Ident, TValue), (Ident, Expr))]
forall {b} {b}. [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs ((TValue -> (TValue, Expr)) -> [TValue] -> [(TValue, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map TValue -> (TValue, Expr)
addError [TValue]
ts)
                  Right [(TValue, Expr)]
tes -> [(TValue, Expr)] -> [((Ident, TValue), (Ident, Expr))]
forall {b} {b}. [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs [(TValue, Expr)]
tes

         eTrue :: Expr
eTrue  = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
prims (Text -> PrimIdent
M.prelPrim Text
"True")
         eFalse :: Expr
eFalse = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
prims (Text -> PrimIdent
M.prelPrim Text
"False")
         resultE :: Expr
resultE = if Bool
result then Expr
eTrue else Expr
eFalse

         rty :: TValue
rty = RecordMap Ident TValue -> TValue
E.TVRec ([(Ident, TValue)] -> RecordMap Ident TValue
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([(Ident, TValue)] -> RecordMap Ident TValue)
-> [(Ident, TValue)] -> RecordMap Ident TValue
forall a b. (a -> b) -> a -> b
$ [(Ident
rIdent, TValue
E.TVBit)] [(Ident, TValue)] -> [(Ident, TValue)] -> [(Ident, TValue)]
forall a. [a] -> [a] -> [a]
++ (((Ident, TValue), (Ident, Expr)) -> (Ident, TValue))
-> [((Ident, TValue), (Ident, Expr))] -> [(Ident, TValue)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ident, TValue), (Ident, Expr)) -> (Ident, TValue)
forall a b. (a, b) -> a
fst [((Ident, TValue), (Ident, Expr))]
argF)
         re :: Expr
re  = RecordMap Ident Expr -> Expr
T.ERec ([(Ident, Expr)] -> RecordMap Ident Expr
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([(Ident, Expr)] -> RecordMap Ident Expr)
-> [(Ident, Expr)] -> RecordMap Ident Expr
forall a b. (a -> b) -> a -> b
$ [(Ident
rIdent, Expr
resultE)] [(Ident, Expr)] -> [(Ident, Expr)] -> [(Ident, Expr)]
forall a. [a] -> [a] -> [a]
++ (((Ident, TValue), (Ident, Expr)) -> (Ident, Expr))
-> [((Ident, TValue), (Ident, Expr))] -> [(Ident, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Ident, TValue), (Ident, Expr)) -> (Ident, Expr)
forall a b. (a, b) -> b
snd [((Ident, TValue), (Ident, Expr))]
argF)

     (TValue, Expr) -> REPL (TValue, Expr)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (TValue
rty, Expr
re)
  where
  mkArgs :: [(b, b)] -> [((Ident, b), (Ident, b))]
mkArgs [(b, b)]
tes = (Int -> (b, b) -> ((Ident, b), (Ident, b)))
-> [Int] -> [(b, b)] -> [((Ident, b), (Ident, b))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> (b, b) -> ((Ident, b), (Ident, b))
forall {p} {b} {b}.
Show p =>
p -> (b, b) -> ((Ident, b), (Ident, b))
mkArg [Int
1 :: Int ..] [(b, b)]
tes
    where
    mkArg :: p -> (b, b) -> ((Ident, b), (Ident, b))
mkArg p
n (b
t,b
e) =
      let argName :: Ident
argName = [Char] -> Ident
M.packIdent ([Char]
"arg" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ p -> [Char]
forall a. Show a => a -> [Char]
show p
n)
       in ((Ident
argName,b
t),(Ident
argName,b
e))

specializeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
specializeCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
specializeCmd [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
  Expr PName
parseExpr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  (Expr Name
_, Expr
expr, Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
parseExpr
  Expr
spexpr <- Expr -> REPL Expr
replSpecExpr Expr
expr
  [Char] -> REPL ()
rPutStrLn  [Char]
"Expression type:"
  Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint    (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
schema
  [Char] -> REPL ()
rPutStrLn  [Char]
"Original expression:"
  [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ Expr -> [Char]
forall a. PP (WithNames a) => a -> [Char]
dump Expr
expr
  [Char] -> REPL ()
rPutStrLn  [Char]
"Specialized expression:"
  let value :: [Char]
value = Expr -> [Char]
forall a. PP (WithNames a) => a -> [Char]
dump Expr
spexpr
  [Char] -> REPL ()
rPutStrLn [Char]
value
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crValue = Just value }

refEvalCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
refEvalCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
refEvalCmd [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
  Expr PName
parseExpr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  (Expr Name
_, Expr
expr, Schema
schema) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
parseExpr
  Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
expr
  Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
schema
  E Value
val <- ModuleCmd (E Value) -> REPL (E Value)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (IO (ModuleRes (E Value)) -> IO (ModuleRes (E Value))
forall a. IO a -> IO a
rethrowEvalError (IO (ModuleRes (E Value)) -> IO (ModuleRes (E Value)))
-> ModuleCmd (E Value) -> ModuleCmd (E Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ModuleCmd (E Value)
R.evaluate Expr
expr)
  PPOpts
opts <- REPL PPOpts
getPPValOpts
  let value :: [Char]
value = Doc -> [Char]
forall a. Show a => a -> [Char]
show (PPOpts -> E Value -> Doc
R.ppEValue PPOpts
opts E Value
val)
  [Char] -> REPL ()
rPutStrLn [Char]
value
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crValue = Just value }

astOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
astOfCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
astOfCmd [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
 Expr PName
expr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
 (Expr Name
re,Expr
_,Schema
_) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr (Expr PName -> Expr PName
forall t. NoPos t => t -> t
P.noPos Expr PName
expr)
 Expr Int -> REPL ()
forall a. Show a => a -> REPL ()
rPrint ((Name -> Int) -> Expr Name -> Expr Int
forall a b. (a -> b) -> Expr a -> Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Int
M.nameUnique Expr Name
re)
 CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

extractCoqCmd :: REPL CommandResult
extractCoqCmd :: REPL CommandResult
extractCoqCmd = do
  ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
  Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc Void -> REPL ()) -> Doc Void -> REPL ()
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> Doc Void
forall t. ShowParseable t => t -> Doc Void
T.showParseable ([DeclGroup] -> Doc Void) -> [DeclGroup] -> Doc Void
forall a b. (a -> b) -> a -> b
$ (Module -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
T.mDecls ([Module] -> [DeclGroup]) -> [Module] -> [DeclGroup]
forall a b. (a -> b) -> a -> b
$ ModuleEnv -> [Module]
M.loadedModules ModuleEnv
me
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

typeOfCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
typeOfCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
typeOfCmd [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do

  Expr PName
expr         <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  (Expr Name
_re,Expr
def,Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr

  -- XXX need more warnings from the module system
  REPL () -> REPL ()
whenDebug ([Char] -> REPL ()
rPutStrLn (Expr -> [Char]
forall a. PP (WithNames a) => a -> [Char]
dump Expr
def))
  NameDisp
fDisp <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  -- type annotation ':' has precedence 2
  let output :: [Char]
output = Doc Void -> [Char]
forall a. Show a => a -> [Char]
show (Doc Void -> [Char]) -> Doc Void -> [Char]
forall a b. (a -> b) -> a -> b
$ NameDisp -> Doc -> Doc Void
runDoc NameDisp
fDisp (Doc -> Doc Void) -> Doc -> Doc Void
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
group (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Int -> Doc -> Doc
hang
                 (Int -> Expr PName -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
2 Expr PName
expr Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":") Int
2 (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
sig)

  [Char] -> REPL ()
rPutStrLn [Char]
output
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crType = Just output }

timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult
timeCmd :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
timeCmd [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
  Int
period <- [Char] -> REPL Int
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"timeMeasurementPeriod" :: REPL Int
  Bool
quiet <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"timeQuiet"
  Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
    [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Measuring for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
period [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" seconds"
  Expr PName
pExpr <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  (Expr Name
_, Expr
def, Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
pExpr
  Expr -> Schema -> REPL (Maybe ([(TParam, Type)], Expr))
replPrepareCheckedExpr Expr
def Schema
sig REPL (Maybe ([(TParam, Type)], Expr))
-> (Maybe ([(TParam, Type)], Expr) -> REPL ()) -> REPL ()
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe ([(TParam, Type)], Expr)
Nothing -> REPLException -> REPL ()
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
sig)
    Just ([(TParam, Type)]
_, Expr
expr) -> do
      Bench.BenchmarkStats {Double
Int64
benchAvgTime :: Double
benchAvgCpuTime :: Double
benchAvgCycles :: Int64
benchAvgTime :: BenchmarkStats -> Double
benchAvgCpuTime :: BenchmarkStats -> Double
benchAvgCycles :: BenchmarkStats -> Int64
..} <- ModuleCmd BenchmarkStats -> REPL BenchmarkStats
forall a. ModuleCmd a -> REPL a
liftModuleCmd
        (IO (ModuleRes BenchmarkStats) -> IO (ModuleRes BenchmarkStats)
forall a. IO a -> IO a
rethrowEvalError (IO (ModuleRes BenchmarkStats) -> IO (ModuleRes BenchmarkStats))
-> ModuleCmd BenchmarkStats -> ModuleCmd BenchmarkStats
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Expr -> ModuleCmd BenchmarkStats
M.benchmarkExpr (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
period) Expr
expr)
      Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
        [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Avg time: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
Bench.secs Double
benchAvgTime
             [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"    Avg CPU time: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
Bench.secs Double
benchAvgCpuTime
             [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"    Avg cycles: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int64 -> [Char]
forall a. Show a => a -> [Char]
show Int64
benchAvgCycles
      let mkStatsRec :: b -> b -> b -> RecordMap a b
mkStatsRec b
time b
cpuTime b
cycles = [(a, b)] -> RecordMap a b
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields
            [(a
"avgTime", b
time), (a
"avgCpuTime", b
cpuTime), (a
"avgCycles", b
cycles)]
          itType :: TValue
itType = RecordMap Ident TValue -> TValue
E.TVRec (RecordMap Ident TValue -> TValue)
-> RecordMap Ident TValue -> TValue
forall a b. (a -> b) -> a -> b
$ TValue -> TValue -> TValue -> RecordMap Ident TValue
forall {a} {b}.
(Show a, Ord a, IsString a) =>
b -> b -> b -> RecordMap a b
mkStatsRec TValue
E.tvFloat64 TValue
E.tvFloat64 TValue
E.TVInteger
          itVal :: Value
itVal = RecordMap Ident (SEval Concrete Value) -> Value
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
E.VRecord (RecordMap Ident (SEval Concrete Value) -> Value)
-> RecordMap Ident (SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ SEval Concrete Value
-> SEval Concrete Value
-> SEval Concrete Value
-> RecordMap Ident (SEval Concrete Value)
forall {a} {b}.
(Show a, Ord a, IsString a) =>
b -> b -> b -> RecordMap a b
mkStatsRec
            (Value -> SEval Concrete Value
forall a. a -> SEval Concrete a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SEval Concrete Value) -> Value -> SEval Concrete Value
forall a b. (a -> b) -> a -> b
$ SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
E.VFloat (SFloat Concrete -> Value) -> SFloat Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Double -> BF
FP.floatFromDouble Double
benchAvgTime)
            (Value -> SEval Concrete Value
forall a. a -> SEval Concrete a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SEval Concrete Value) -> Value -> SEval Concrete Value
forall a b. (a -> b) -> a -> b
$ SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
E.VFloat (SFloat Concrete -> Value) -> SFloat Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Double -> BF
FP.floatFromDouble Double
benchAvgCpuTime)
            (Value -> SEval Concrete Value
forall a. a -> SEval Concrete a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SEval Concrete Value) -> Value -> SEval Concrete Value
forall a b. (a -> b) -> a -> b
$ SInteger Concrete -> Value
forall sym. SInteger sym -> GenValue sym
E.VInteger (SInteger Concrete -> Value) -> SInteger Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
benchAvgCycles)
      TValue -> Value -> REPL ()
bindItVariableVal TValue
itType Value
itVal
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult -- TODO: gather timing outputs

readFileCmd :: FilePath -> REPL CommandResult
readFileCmd :: [Char] -> REPL CommandResult
readFileCmd [Char]
fp = do
  Maybe ByteString
bytes <- [Char]
-> (SomeException -> REPL (Maybe ByteString))
-> REPL (Maybe ByteString)
replReadFile [Char]
fp (\SomeException
err -> [Char] -> REPL ()
rPutStrLn (SomeException -> [Char]
forall a. Show a => a -> [Char]
show SomeException
err) REPL () -> REPL (Maybe ByteString) -> REPL (Maybe ByteString)
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe ByteString -> REPL (Maybe ByteString)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ByteString
forall a. Maybe a
Nothing)
  case Maybe ByteString
bytes of
    Maybe ByteString
Nothing -> CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult { crSuccess = False }
    Just ByteString
bs ->
      do PrimMap
pm <- REPL PrimMap
getPrimMap
         let val :: Integer
val = ByteString -> Integer
byteStringToInteger ByteString
bs
         let len :: Int
len = ByteString -> Int
BS.length ByteString
bs
         let split :: Expr
split = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
pm (Text -> PrimIdent
M.prelPrim Text
"split")
         let number :: Expr
number = PrimMap -> PrimIdent -> Expr
T.ePrim PrimMap
pm (Text -> PrimIdent
M.prelPrim Text
"number")
         let f :: Expr
f = Expr -> Expr
T.EProofApp ((Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
T.ETApp Expr
split [Int -> Type
forall a. Integral a => a -> Type
T.tNum Int
len, Integer -> Type
forall a. Integral a => a -> Type
T.tNum (Integer
8::Integer), Type
T.tBit])
         let t :: Type
t = Type -> Type
T.tWord (Integer -> Type
forall a. Integral a => a -> Type
T.tNum (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
8))
         let x :: Expr
x = Expr -> Expr
T.EProofApp (Expr -> Type -> Expr
T.ETApp (Expr -> Type -> Expr
T.ETApp Expr
number (Integer -> Type
forall a. Integral a => a -> Type
T.tNum Integer
val)) Type
t)
         let expr :: Expr
expr = Expr -> Expr -> Expr
T.EApp Expr
f Expr
x
         REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable (Integer -> TValue -> TValue
E.TVSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len) (Integer -> TValue -> TValue
E.TVSeq Integer
8 TValue
E.TVBit)) Expr
expr
         CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

-- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer'
-- with @8*n@ bits. This function uses a balanced binary fold to
-- achieve /O(n log n)/ total memory allocation and run-time, in
-- contrast to the /O(n^2)/ that would be required by a naive
-- left-fold.
byteStringToInteger :: BS.ByteString -> Integer
-- byteStringToInteger = BS.foldl' (\a b -> a `shiftL` 8 .|. toInteger b) 0
byteStringToInteger :: ByteString -> Integer
byteStringToInteger ByteString
bs
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
  | Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (HasCallStack => ByteString -> Word8
ByteString -> Word8
BS.head ByteString
bs)
  | Bool
otherwise = Integer
x1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
l2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
x2
  where
    l :: Int
l = ByteString -> Int
BS.length ByteString
bs
    l1 :: Int
l1 = Int
l Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    l2 :: Int
l2 = Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l1
    (ByteString
bs1, ByteString
bs2) = Int -> ByteString -> (ByteString, ByteString)
BS.splitAt Int
l1 ByteString
bs
    x1 :: Integer
x1 = ByteString -> Integer
byteStringToInteger ByteString
bs1
    x2 :: Integer
x2 = ByteString -> Integer
byteStringToInteger ByteString
bs2

writeFileCmd :: FilePath -> String -> (Int,Int) -> Maybe FilePath -> REPL CommandResult
writeFileCmd :: [Char]
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
writeFileCmd [Char]
file [Char]
str (Int, Int)
pos Maybe [Char]
fnm = do
  Expr PName
expr         <- [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int, Int)
pos Maybe [Char]
fnm
  (Value
val,Type
ty)     <- Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr
  if Bool -> Bool
not (Type -> Bool
tIsByteSeq Type
ty)
    then do
      Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc -> REPL ()) -> Doc -> REPL ()
forall a b. (a -> b) -> a -> b
$ Doc
"Cannot write expression of types other than [n][8]."
              Doc -> Doc -> Doc
<+> Doc
"Type was: " Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
ty
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
    else do
      ByteString
bytes <- Value -> REPL ByteString
serializeValue Value
val
      [Char] -> ByteString -> REPL CommandResult
replWriteFile [Char]
file ByteString
bytes
 where
  tIsByteSeq :: Type -> Bool
tIsByteSeq Type
x = Bool -> ((Type, Type) -> Bool) -> Maybe (Type, Type) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
                       (Type -> Bool
tIsByte (Type -> Bool) -> ((Type, Type) -> Type) -> (Type, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> b
snd)
                       (Type -> Maybe (Type, Type)
T.tIsSeq Type
x)
  tIsByte :: Type -> Bool
tIsByte    Type
x = Bool -> ((Type, Type) -> Bool) -> Maybe (Type, Type) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
                       (\(Type
n,Type
b) -> Type -> Bool
T.tIsBit Type
b Bool -> Bool -> Bool
&& Type -> Maybe Integer
T.tIsNum Type
n Maybe Integer -> Maybe Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
8)
                       (Type -> Maybe (Type, Type)
T.tIsSeq Type
x)
  serializeValue :: Value -> REPL ByteString
serializeValue (E.VSeq Integer
n SeqMap Concrete Value
vs) = do
    [BV]
ws <- Eval [BV] -> REPL [BV]
forall a. Eval a -> REPL a
rEval
            ((Eval Value -> Eval BV) -> [Eval Value] -> Eval [BV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Eval Value -> (Value -> Eval BV) -> Eval BV
forall a b. Eval a -> (a -> Eval b) -> Eval b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Concrete -> [Char] -> Value -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> [Char] -> GenValue sym -> SEval sym (SWord sym)
E.fromVWord Concrete
Concrete [Char]
"serializeValue") ([Eval Value] -> Eval [BV]) -> [Eval Value] -> Eval [BV]
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
E.enumerateSeqMap Integer
n SeqMap Concrete Value
vs)
    ByteString -> REPL ByteString
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> REPL ByteString) -> ByteString -> REPL ByteString
forall a b. (a -> b) -> a -> b
$ [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
forall a b. (a -> b) -> a -> b
$ (BV -> Word8) -> [BV] -> [Word8]
forall a b. (a -> b) -> [a] -> [b]
map BV -> Word8
forall {b}. Num b => BV -> b
serializeByte [BV]
ws
  serializeValue Value
_             =
    [Char] -> [[Char]] -> REPL ByteString
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.REPL.Command.writeFileCmd"
      [[Char]
"Impossible: Non-VSeq value of type [n][8]."]
  serializeByte :: BV -> b
serializeByte (Concrete.BV Integer
_ Integer
v) = Integer -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
0xFF)


rEval :: E.Eval a -> REPL a
rEval :: forall a. Eval a -> REPL a
rEval Eval a
m = IO a -> REPL a
forall a. IO a -> REPL a
io (CallStack -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty Eval a
m)

rEvalRethrow :: E.Eval a -> REPL a
rEvalRethrow :: forall a. Eval a -> REPL a
rEvalRethrow Eval a
m = IO a -> REPL a
forall a. IO a -> REPL a
io (IO a -> REPL a) -> IO a -> REPL a
forall a b. (a -> b) -> a -> b
$ IO a -> IO a
forall a. IO a -> IO a
rethrowEvalError (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ CallStack -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty Eval a
m

reloadCmd :: REPL CommandResult
reloadCmd :: REPL CommandResult
reloadCmd  = do
  Maybe LoadedModule
mb <- REPL (Maybe LoadedModule)
getLoadedMod
  case Maybe LoadedModule
mb of
    Just LoadedModule
lm  ->
      case LoadedModule -> ModulePath
lPath LoadedModule
lm of
        M.InFile [Char]
f -> [Char] -> REPL CommandResult
loadCmd [Char]
f
        ModulePath
_ -> CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult
    Maybe LoadedModule
Nothing -> CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult


editCmd :: String -> REPL CommandResult
editCmd :: [Char] -> REPL CommandResult
editCmd [Char]
path =
  do Maybe [Char]
mbE <- REPL (Maybe [Char])
getEditPath
     Maybe LoadedModule
mbL <- REPL (Maybe LoadedModule)
getLoadedMod
     if Bool -> Bool
not ([Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
path)
        then do Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe LoadedModule -> Bool
forall a. Maybe a -> Bool
isNothing Maybe LoadedModule
mbL)
                  (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ LoadedModule -> REPL ()
setLoadedMod LoadedModule { lFocus :: Maybe (ImpName Name)
lFocus = Maybe (ImpName Name)
forall a. Maybe a
Nothing
                                              , lPath :: ModulePath
lPath = [Char] -> ModulePath
M.InFile [Char]
path }
                [Char] -> REPL CommandResult
doEdit [Char]
path
        else case [Maybe ModulePath] -> Maybe ModulePath
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ [Char] -> ModulePath
M.InFile ([Char] -> ModulePath) -> Maybe [Char] -> Maybe ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Char]
mbE, LoadedModule -> ModulePath
lPath (LoadedModule -> ModulePath)
-> Maybe LoadedModule -> Maybe ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LoadedModule
mbL ] of
               Maybe ModulePath
Nothing ->
                do [Char] -> REPL ()
rPutStrLn [Char]
"No filed to edit."
                   CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
               Just ModulePath
p  ->
                  case ModulePath
p of
                    M.InFile [Char]
f   -> [Char] -> REPL CommandResult
doEdit [Char]
f
                    M.InMem [Char]
l ByteString
bs -> do
                      Bool
_ <- [Char] -> ByteString -> ([Char] -> REPL Bool) -> REPL Bool
forall a. [Char] -> ByteString -> ([Char] -> REPL a) -> REPL a
withROTempFile [Char]
l ByteString
bs [Char] -> REPL Bool
replEdit
                      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult
  where
  doEdit :: [Char] -> REPL CommandResult
doEdit [Char]
p =
    do [Char] -> REPL ()
setEditPath [Char]
p
       Bool
_ <- [Char] -> REPL Bool
replEdit [Char]
p
       REPL CommandResult
reloadCmd

withRWTempFile :: String -> (Handle -> IO a) -> IO a
withRWTempFile :: forall a. [Char] -> (Handle -> IO a) -> IO a
withRWTempFile [Char]
name Handle -> IO a
k =
  IO ([Char], Handle)
-> (([Char], Handle) -> IO ())
-> (([Char], Handle) -> IO a)
-> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
X.bracket
    (do [Char]
tmp <- IO [Char]
getTemporaryDirectory
        let esc :: Char -> Char
esc Char
c = if Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAlphaNum Char
c then Char
c else Char
'_'
        [Char] -> [Char] -> IO ([Char], Handle)
openTempFile [Char]
tmp ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
esc [Char]
name))
    (\([Char]
nm,Handle
h) -> Handle -> IO ()
hClose Handle
h IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Char] -> IO ()
removeFile [Char]
nm)
    (Handle -> IO a
k (Handle -> IO a)
-> (([Char], Handle) -> Handle) -> ([Char], Handle) -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char], Handle) -> Handle
forall a b. (a, b) -> b
snd)

withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a
withROTempFile :: forall a. [Char] -> ByteString -> ([Char] -> REPL a) -> REPL a
withROTempFile [Char]
name ByteString
cnt [Char] -> REPL a
k =
  do ([Char]
path,Handle
h) <- REPL ([Char], Handle)
mkTmp
     do [Char] -> Handle -> REPL ()
forall {m :: * -> *}. MonadIO m => [Char] -> Handle -> m ()
mkFile [Char]
path Handle
h
        [Char] -> REPL a
k [Char]
path
      REPL a -> REPL () -> REPL a
forall a b. REPL a -> REPL b -> REPL a
`finally` IO () -> REPL ()
forall a. IO a -> REPL a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (do Handle -> IO ()
hClose Handle
h
                           [Char] -> IO ()
removeFile [Char]
path)
  where
  mkTmp :: REPL ([Char], Handle)
mkTmp =
    IO ([Char], Handle) -> REPL ([Char], Handle)
forall a. IO a -> REPL a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ([Char], Handle) -> REPL ([Char], Handle))
-> IO ([Char], Handle) -> REPL ([Char], Handle)
forall a b. (a -> b) -> a -> b
$
    do [Char]
tmp <- IO [Char]
getTemporaryDirectory
       let esc :: Char -> Char
esc Char
c = if Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAlphaNum Char
c then Char
c else Char
'_'
       [Char] -> [Char] -> IO ([Char], Handle)
openTempFile [Char]
tmp ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
esc [Char]
name [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
".cry")

  mkFile :: [Char] -> Handle -> m ()
mkFile [Char]
path Handle
h =
    IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$
    do Handle -> ByteString -> IO ()
BS8.hPutStrLn Handle
h ByteString
cnt
       Handle -> IO ()
hFlush Handle
h
       [Char] -> Permissions -> IO ()
setPermissions [Char]
path (Bool -> Permissions -> Permissions
setOwnerReadable Bool
True Permissions
emptyPermissions)



moduleCmd :: String -> REPL CommandResult
moduleCmd :: [Char] -> REPL CommandResult
moduleCmd [Char]
modString
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
modString = CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult
  | Bool
otherwise      = do
    case [Char] -> Maybe ModName
parseModName [Char]
modString of
      Just ModName
m ->
        do ModulePath
mpath <- ModuleCmd ModulePath -> REPL ModulePath
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModName -> ModuleCmd ModulePath
M.findModule ModName
m)
           case ModulePath
mpath of
             M.InFile [Char]
file ->
               do [Char] -> REPL ()
setEditPath [Char]
file
                  LoadedModule -> REPL ()
setLoadedMod LoadedModule { lFocus :: Maybe (ImpName Name)
lFocus = ImpName Name -> Maybe (ImpName Name)
forall a. a -> Maybe a
Just (ModName -> ImpName Name
forall name. ModName -> ImpName name
P.ImpTop ModName
m), lPath :: ModulePath
lPath = ModulePath
mpath }
                  ModuleCmd (ModulePath, TCTopEntity) -> REPL CommandResult
loadHelper ([Char] -> ModuleCmd (ModulePath, TCTopEntity)
M.loadModuleByPath [Char]
file)
             M.InMem {} -> ModuleCmd (ModulePath, TCTopEntity) -> REPL CommandResult
loadHelper (ModName -> ModuleCmd (ModulePath, TCTopEntity)
M.loadModuleByName ModName
m)
      Maybe ModName
Nothing ->
        do [Char] -> REPL ()
rPutStrLn [Char]
"Invalid module name."
           CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }


focusCmd :: String -> REPL CommandResult
focusCmd :: [Char] -> REPL CommandResult
focusCmd [Char]
modString
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
modString =
   do Maybe LoadedModule
mb <- REPL (Maybe LoadedModule)
getLoadedMod
      case Maybe LoadedModule
mb of
        Maybe LoadedModule
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just LoadedModule
lm ->
          case LoadedModule -> Maybe ModName
lName LoadedModule
lm of
            Maybe ModName
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Just ModName
name -> do
              let top :: ImpName name
top = ModName -> ImpName name
forall name. ModName -> ImpName name
P.ImpTop ModName
name
              ModuleCmd () -> REPL ()
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleInput IO
-> ModuleM ()
-> IO (Either ModuleError ((), ModuleEnv), [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
`M.runModuleM` ImpName Name -> ModuleM ()
M.setFocusedModule ImpName Name
forall {name}. ImpName name
top)
              LoadedModule -> REPL ()
setLoadedMod LoadedModule
lm { lFocus = Just top }
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

  | Bool
otherwise =
    case [Char] -> Maybe (ImpName PName)
parseImpName [Char]
modString of
      Maybe (ImpName PName)
Nothing ->
        do [Char] -> REPL ()
rPutStrLn [Char]
"Invalid module name."
           CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
    
      Just ImpName PName
pimpName -> do
        ImpName Name
impName <- ModuleCmd (ImpName Name) -> REPL (ImpName Name)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ImpName PName -> ModuleCmd (ImpName Name)
setFocusedModuleCmd ImpName PName
pimpName)
        Maybe LoadedModule
mb <- REPL (Maybe LoadedModule)
getLoadedMod
        case Maybe LoadedModule
mb of
          Maybe LoadedModule
Nothing -> () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Just LoadedModule
lm -> LoadedModule -> REPL ()
setLoadedMod LoadedModule
lm { lFocus = Just impName }
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

setFocusedModuleCmd :: P.ImpName P.PName -> M.ModuleCmd (P.ImpName T.Name)
setFocusedModuleCmd :: ImpName PName -> ModuleCmd (ImpName Name)
setFocusedModuleCmd ImpName PName
pimpName ModuleInput IO
i = ModuleInput IO
-> ModuleM (ImpName Name)
-> IO
     (Either ModuleError (ImpName Name, ModuleEnv), [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleM ModuleInput IO
i (ModuleM (ImpName Name)
 -> IO
      (Either ModuleError (ImpName Name, ModuleEnv), [ModuleWarning]))
-> ModuleM (ImpName Name)
-> IO
     (Either ModuleError (ImpName Name, ModuleEnv), [ModuleWarning])
forall a b. (a -> b) -> a -> b
$
 do ImpName Name
impName <- ImpName PName -> ModuleM (ImpName Name)
M.renameImpNameInCurrentEnv ImpName PName
pimpName
    ImpName Name -> ModuleM ()
M.setFocusedModule ImpName Name
impName
    ImpName Name -> ModuleM (ImpName Name)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ImpName Name
impName

loadPrelude :: REPL ()
loadPrelude :: REPL ()
loadPrelude  = REPL CommandResult -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL CommandResult -> REPL ()) -> REPL CommandResult -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char] -> REPL CommandResult
moduleCmd ([Char] -> REPL CommandResult) -> [Char] -> REPL CommandResult
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
M.preludeName

loadCmd :: FilePath -> REPL CommandResult
loadCmd :: [Char] -> REPL CommandResult
loadCmd [Char]
path
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
path = CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult

  -- when `:load`, the edit and focused paths become the parameter
  | Bool
otherwise = do [Char] -> REPL ()
setEditPath [Char]
path
                   LoadedModule -> REPL ()
setLoadedMod LoadedModule { lFocus :: Maybe (ImpName Name)
lFocus = Maybe (ImpName Name)
forall a. Maybe a
Nothing
                                             , lPath :: ModulePath
lPath = [Char] -> ModulePath
M.InFile [Char]
path
                                             }
                   ModuleCmd (ModulePath, TCTopEntity) -> REPL CommandResult
loadHelper ([Char] -> ModuleCmd (ModulePath, TCTopEntity)
M.loadModuleByPath [Char]
path)

loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL CommandResult
loadHelper :: ModuleCmd (ModulePath, TCTopEntity) -> REPL CommandResult
loadHelper ModuleCmd (ModulePath, TCTopEntity)
how =
  do REPL ()
clearLoadedMod
     (ModulePath
path,TCTopEntity
ent) <- ModuleCmd (ModulePath, TCTopEntity)
-> REPL (ModulePath, TCTopEntity)
forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd (ModulePath, TCTopEntity)
how

     REPL () -> REPL ()
whenDebug ([Char] -> REPL ()
rPutStrLn (TCTopEntity -> [Char]
forall a. PP (WithNames a) => a -> [Char]
dump TCTopEntity
ent))
     LoadedModule -> REPL ()
setLoadedMod LoadedModule
        { lFocus :: Maybe (ImpName Name)
lFocus = ImpName Name -> Maybe (ImpName Name)
forall a. a -> Maybe a
Just (ModName -> ImpName Name
forall name. ModName -> ImpName name
P.ImpTop (TCTopEntity -> ModName
T.tcTopEntitytName TCTopEntity
ent))
        , lPath :: ModulePath
lPath = ModulePath
path
        }
     -- after a successful load, the current module becomes the edit target
     case ModulePath
path of
       M.InFile [Char]
f -> [Char] -> REPL ()
setEditPath [Char]
f
       M.InMem {} -> REPL ()
clearEditPath
     DynamicEnv -> REPL ()
setDynEnv DynamicEnv
forall a. Monoid a => a
mempty
     CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

genHeaderCmd :: FilePath -> REPL CommandResult
genHeaderCmd :: [Char] -> REPL CommandResult
genHeaderCmd [Char]
path
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
path = CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult
  | Bool
otherwise = do
    (ModulePath
mPath, TCTopEntity
m) <- ModuleCmd (ModulePath, TCTopEntity)
-> REPL (ModulePath, TCTopEntity)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (ModulePath, TCTopEntity)
 -> REPL (ModulePath, TCTopEntity))
-> ModuleCmd (ModulePath, TCTopEntity)
-> REPL (ModulePath, TCTopEntity)
forall a b. (a -> b) -> a -> b
$ [Char] -> ModuleCmd (ModulePath, TCTopEntity)
M.checkModuleByPath [Char]
path
    let decls :: [(Name, FFIFunType)]
decls = case TCTopEntity
m of
                   T.TCTopModule Module
mo -> Module -> [(Name, FFIFunType)]
forall mname. ModuleG mname -> [(Name, FFIFunType)]
findForeignDecls Module
mo
                   T.TCTopSignature {} -> []
    if [(Name, FFIFunType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, FFIFunType)]
decls
      then do
        [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"No foreign declarations in " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ModulePath -> [Char]
forall {a}. PP a => a -> [Char]
pretty ModulePath
mPath
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
      else do
        let header :: [Char]
header = [(Name, FFIFunType)] -> [Char]
generateForeignHeader [(Name, FFIFunType)]
decls
        case ModulePath
mPath of
          M.InFile [Char]
p -> do
            let hPath :: [Char]
hPath = [Char]
p [Char] -> ShowS
-<.> [Char]
"h"
            [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Writing header to " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
hPath
            [Char] -> [Char] -> REPL CommandResult
replWriteFileString [Char]
hPath [Char]
header
          M.InMem [Char]
_ ByteString
_ ->
            do [Char] -> REPL ()
rPutStrLn [Char]
header
               CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

versionCmd :: REPL CommandResult
versionCmd :: REPL CommandResult
versionCmd = do
  ([Char] -> REPL ()) -> REPL ()
forall (m :: * -> *). Monad m => ([Char] -> m ()) -> m ()
displayVersion [Char] -> REPL ()
rPutStrLn
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

quitCmd :: REPL CommandResult
quitCmd :: REPL CommandResult
quitCmd  = do
  REPL ()
stop
  CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

browseCmd :: String -> REPL CommandResult
browseCmd :: [Char] -> REPL CommandResult
browseCmd [Char]
input
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
input =
    do ModContext
fe <- REPL ModContext
getFocusedEnv
       Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (BrowseHow -> ModContext -> Doc Void
browseModContext BrowseHow
BrowseInScope ModContext
fe)
       CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult
  | Bool
otherwise =
    case [Char] -> Maybe (ImpName PName)
parseImpName [Char]
input of
      Maybe (ImpName PName)
Nothing -> do
        [Char] -> REPL ()
rPutStrLn [Char]
"Invalid module name"
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
      Just ImpName PName
pimpName -> do
        ImpName Name
impName <- ModuleCmd (ImpName Name) -> REPL (ImpName Name)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleInput IO
-> ModuleM (ImpName Name)
-> IO
     (Either ModuleError (ImpName Name, ModuleEnv), [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
`M.runModuleM` ImpName PName -> ModuleM (ImpName Name)
M.renameImpNameInCurrentEnv ImpName PName
pimpName)
        Maybe ModContext
mb <- ImpName Name -> ModuleEnv -> Maybe ModContext
M.modContextOf ImpName Name
impName (ModuleEnv -> Maybe ModContext)
-> REPL ModuleEnv -> REPL (Maybe ModContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModuleEnv
getModuleEnv
        case Maybe ModContext
mb of
          Maybe ModContext
Nothing -> do
            [Char] -> REPL ()
rPutStrLn ([Char]
"Module " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
input [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" is not loaded")
            CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
          Just ModContext
fe -> do
            Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (BrowseHow -> ModContext -> Doc Void
browseModContext BrowseHow
BrowseExported ModContext
fe)
            CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult


setOptionCmd :: String -> REPL CommandResult
setOptionCmd :: [Char] -> REPL CommandResult
setOptionCmd [Char]
str
  | Just [Char]
value <- Maybe [Char]
mbValue = [Char] -> [Char] -> REPL Bool
setUser [Char]
key [Char]
value REPL Bool -> (Bool -> REPL CommandResult) -> REPL CommandResult
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
success -> CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = success }
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
key              = (OptionDescr -> REPL CommandResult) -> [OptionDescr] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> REPL CommandResult
describe ([Char] -> REPL CommandResult)
-> (OptionDescr -> [Char]) -> OptionDescr -> REPL CommandResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OptionDescr -> [Char]
optName) (Trie OptionDescr -> [OptionDescr]
forall a. Trie a -> [a]
leaves Trie OptionDescr
userOptions) REPL () -> REPL CommandResult -> REPL CommandResult
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult
  | Bool
otherwise             = [Char] -> REPL CommandResult
describe [Char]
key
  where
  ([Char]
before,[Char]
after) = (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'=') [Char]
str
  key :: [Char]
key   = ShowS
trim [Char]
before
  mbValue :: Maybe [Char]
mbValue = case [Char]
after of
              Char
_ : [Char]
stuff -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just (ShowS
trim [Char]
stuff)
              [Char]
_         -> Maybe [Char]
forall a. Maybe a
Nothing

  describe :: [Char] -> REPL CommandResult
describe [Char]
k = do
    Maybe EnvVal
ev <- [Char] -> REPL (Maybe EnvVal)
tryGetUser [Char]
k
    case Maybe EnvVal
ev of
      Just EnvVal
v  -> do [Char] -> REPL ()
rPutStrLn ([Char]
k [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvVal -> [Char]
showEnvVal EnvVal
v)
                    CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult
      Maybe EnvVal
Nothing -> do [Char] -> REPL ()
rPutStrLn ([Char]
"Unknown user option: `" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
k [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"`")
                    Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace [Char]
k) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do
                      let ([Char]
k1, [Char]
k2) = (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace [Char]
k
                      [Char] -> REPL ()
rPutStrLn ([Char]
"Did you mean: `:set " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
k1 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" =" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
k2 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"`?")
                    CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }

showEnvVal :: EnvVal -> String
showEnvVal :: EnvVal -> [Char]
showEnvVal EnvVal
ev =
  case EnvVal
ev of
    EnvString [Char]
s   -> [Char]
s
    EnvProg [Char]
p [[Char]]
as  -> [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " ([Char]
p[Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:[[Char]]
as)
    EnvNum Int
n      -> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n
    EnvBool Bool
True  -> [Char]
"on"
    EnvBool Bool
False -> [Char]
"off"

-- XXX at the moment, this can only look at declarations.
helpCmd :: String -> REPL CommandResult
helpCmd :: [Char] -> REPL CommandResult
helpCmd [Char]
cmd
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
cmd  = CommandResult
emptyCommandResult CommandResult -> REPL () -> REPL CommandResult
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> REPL ()) -> [[Char]] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> REPL ()
rPutStrLn ([CommandDescr] -> [[Char]]
genHelp [CommandDescr]
commandList)
  | [Char]
cmd0 : [[Char]]
args <- [Char] -> [[Char]]
words [Char]
cmd, [Char]
":" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
cmd0 =
    case [Char] -> [CommandDescr]
findCommandExact [Char]
cmd0 of
      []  -> Int -> Maybe [Char] -> Command -> REPL CommandResult
runCommand Int
1 Maybe [Char]
forall a. Maybe a
Nothing ([Char] -> Command
Unknown [Char]
cmd0)
      [CommandDescr
c] -> CommandDescr -> [[Char]] -> REPL CommandResult
showCmdHelp CommandDescr
c [[Char]]
args
      [CommandDescr]
cs  -> Int -> Maybe [Char] -> Command -> REPL CommandResult
runCommand Int
1 Maybe [Char]
forall a. Maybe a
Nothing ([Char] -> [[Char]] -> Command
Ambiguous [Char]
cmd0 ((CommandDescr -> [[Char]]) -> [CommandDescr] -> [[Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CommandDescr -> [[Char]]
cNames [CommandDescr]
cs))
  | Bool
otherwise =
    Bool -> CommandResult
wrapResult (Bool -> CommandResult) -> REPL Bool -> REPL CommandResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    case [Char] -> Maybe PName
parseHelpName [Char]
cmd of
      Just PName
qname -> Bool
True Bool -> REPL Bool -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ PName -> REPL Bool
helpForNamed PName
qname
      Maybe PName
Nothing    -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn ([Char]
"Unable to parse name: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
cmd)

  where
  wrapResult :: Bool -> CommandResult
wrapResult Bool
success = CommandResult
emptyCommandResult { crSuccess = success }

  showCmdHelp :: CommandDescr -> [[Char]] -> REPL CommandResult
showCmdHelp CommandDescr
c [[Char]
arg] | [Char]
":set" [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` CommandDescr -> [[Char]]
cNames CommandDescr
c = Bool -> CommandResult
wrapResult (Bool -> CommandResult) -> REPL Bool -> REPL CommandResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> REPL Bool
showOptionHelp [Char]
arg
  showCmdHelp CommandDescr
c [[Char]]
_args =
    do [Char] -> REPL ()
rPutStrLn ([Char]
"\n    " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (CommandDescr -> [[Char]]
cNames CommandDescr
c) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " (CommandDescr -> [[Char]]
cArgs CommandDescr
c))
       [Char] -> REPL ()
rPutStrLn [Char]
""
       [Char] -> REPL ()
rPutStrLn (CommandDescr -> [Char]
cHelp CommandDescr
c)
       [Char] -> REPL ()
rPutStrLn [Char]
""
       Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (CommandDescr -> [Char]
cLongHelp CommandDescr
c)) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$ do
         [Char] -> REPL ()
rPutStrLn (CommandDescr -> [Char]
cLongHelp CommandDescr
c)
         [Char] -> REPL ()
rPutStrLn [Char]
""
       CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

  showOptionHelp :: [Char] -> REPL Bool
showOptionHelp [Char]
arg =
    case [Char] -> Trie OptionDescr -> [OptionDescr]
forall a. [Char] -> Trie a -> [a]
lookupTrieExact [Char]
arg Trie OptionDescr
userOptions of
      [OptionDescr
opt] ->
        do let k :: [Char]
k = OptionDescr -> [Char]
optName OptionDescr
opt
           Maybe EnvVal
ev <- [Char] -> REPL (Maybe EnvVal)
tryGetUser [Char]
k
           [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"\n    " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
k [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> (EnvVal -> [Char]) -> Maybe EnvVal -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"???" EnvVal -> [Char]
showEnvVal Maybe EnvVal
ev
           [Char] -> REPL ()
rPutStrLn [Char]
""
           [Char] -> REPL ()
rPutStrLn ([Char]
"Default value: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvVal -> [Char]
showEnvVal (OptionDescr -> EnvVal
optDefault OptionDescr
opt))
           [Char] -> REPL ()
rPutStrLn [Char]
""
           [Char] -> REPL ()
rPutStrLn (OptionDescr -> [Char]
optHelp OptionDescr
opt)
           [Char] -> REPL ()
rPutStrLn [Char]
""
           Bool -> REPL Bool
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      [] -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn ([Char]
"Unknown setting name `" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
arg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"`")
      [OptionDescr]
_  -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn ([Char]
"Ambiguous setting name `" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
arg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"`")


runShellCmd :: String -> REPL CommandResult
runShellCmd :: [Char] -> REPL CommandResult
runShellCmd [Char]
cmd
  = IO CommandResult -> REPL CommandResult
forall a. IO a -> REPL a
io (IO CommandResult -> REPL CommandResult)
-> IO CommandResult -> REPL CommandResult
forall a b. (a -> b) -> a -> b
$ do ProcessHandle
h <- [Char] -> IO ProcessHandle
Process.runCommand [Char]
cmd
            ExitCode
_ <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
h
            CommandResult -> IO CommandResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CommandResult
emptyCommandResult -- This could check for exit code 0

cdCmd :: FilePath -> REPL CommandResult
cdCmd :: [Char] -> REPL CommandResult
cdCmd [Char]
f | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
f = do [Char] -> REPL ()
rPutStrLn ([Char] -> REPL ()) -> [Char] -> REPL ()
forall a b. (a -> b) -> a -> b
$ [Char]
"[error] :cd requires a path argument"
                      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
        | Bool
otherwise = do
  Bool
exists <- IO Bool -> REPL Bool
forall a. IO a -> REPL a
io (IO Bool -> REPL Bool) -> IO Bool -> REPL Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> IO Bool
doesDirectoryExist [Char]
f
  if Bool
exists
    then CommandResult
emptyCommandResult CommandResult -> REPL () -> REPL CommandResult
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IO () -> REPL ()
forall a. IO a -> REPL a
io ([Char] -> IO ()
setCurrentDirectory [Char]
f)
    else REPLException -> REPL CommandResult
forall a. REPLException -> REPL a
raise (REPLException -> REPL CommandResult)
-> REPLException -> REPL CommandResult
forall a b. (a -> b) -> a -> b
$ [Char] -> REPLException
DirectoryNotFound [Char]
f

-- C-c Handlings ---------------------------------------------------------------

-- XXX this should probably do something a bit more specific.
handleCtrlC :: a -> REPL a
handleCtrlC :: forall a. a -> REPL a
handleCtrlC a
a = do [Char] -> REPL ()
rPutStrLn [Char]
"Ctrl-C"
                   REPL ()
resetTCSolver
                   a -> REPL a
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- Utilities -------------------------------------------------------------------

-- | Lift a parsing action into the REPL monad.
replParse :: (String -> Either ParseError a) -> String -> REPL a
replParse :: forall a. ([Char] -> Either ParseError a) -> [Char] -> REPL a
replParse [Char] -> Either ParseError a
parse [Char]
str = case [Char] -> Either ParseError a
parse [Char]
str of
  Right a
a -> a -> REPL a
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  Left ParseError
e  -> REPLException -> REPL a
forall a. REPLException -> REPL a
raise (ParseError -> REPLException
ParseError ParseError
e)

replParseInput :: String -> Int -> Maybe FilePath -> REPL (P.ReplInput P.PName)
replParseInput :: [Char] -> Int -> Maybe [Char] -> REPL (ReplInput PName)
replParseInput [Char]
str Int
lineNum Maybe [Char]
fnm = ([Char] -> Either ParseError (ReplInput PName))
-> [Char] -> REPL (ReplInput PName)
forall a. ([Char] -> Either ParseError a) -> [Char] -> REPL a
replParse (Config -> Text -> Either ParseError (ReplInput PName)
parseReplWith Config
cfg (Text -> Either ParseError (ReplInput PName))
-> ([Char] -> Text)
-> [Char]
-> Either ParseError (ReplInput PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
T.pack) [Char]
str
  where
  cfg :: Config
cfg = case Maybe [Char]
fnm of
          Maybe [Char]
Nothing -> Config
interactiveConfig{ cfgStart = Position lineNum 1 }
          Just [Char]
f  -> Config
defaultConfig
                     { cfgSource = f
                     , cfgStart  = Position lineNum 1
                     }

replParseExpr :: String -> (Int,Int) -> Maybe FilePath -> REPL (P.Expr P.PName)
replParseExpr :: [Char] -> (Int, Int) -> Maybe [Char] -> REPL (Expr PName)
replParseExpr [Char]
str (Int
l,Int
c) Maybe [Char]
fnm = ([Char] -> Either ParseError (Expr PName))
-> [Char] -> REPL (Expr PName)
forall a. ([Char] -> Either ParseError a) -> [Char] -> REPL a
replParse (Config -> Text -> Either ParseError (Expr PName)
parseExprWith Config
cfg(Text -> Either ParseError (Expr PName))
-> ([Char] -> Text) -> [Char] -> Either ParseError (Expr PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
T.pack) [Char]
str
  where
  cfg :: Config
cfg = case Maybe [Char]
fnm of
          Maybe [Char]
Nothing -> Config
interactiveConfig{ cfgStart = Position l c }
          Just [Char]
f  -> Config
defaultConfig
                     { cfgSource = f
                     , cfgStart  = Position l c
                     }

mkInteractiveRange :: (Int,Int) -> Maybe FilePath -> Range
mkInteractiveRange :: (Int, Int) -> Maybe [Char] -> Range
mkInteractiveRange (Int
l,Int
c) Maybe [Char]
mb = Position -> Position -> [Char] -> Range
Range Position
p Position
p [Char]
src
  where
  p :: Position
p = Int -> Int -> Position
Position Int
l Int
c
  src :: [Char]
src = case Maybe [Char]
mb of
          Maybe [Char]
Nothing -> [Char]
"<interactive>"
          Just [Char]
b  -> [Char]
b

interactiveConfig :: Config
interactiveConfig :: Config
interactiveConfig = Config
defaultConfig { cfgSource = "<interactive>" }

getPrimMap :: REPL M.PrimMap
getPrimMap :: REPL PrimMap
getPrimMap  = ModuleCmd PrimMap -> REPL PrimMap
forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd PrimMap
M.getPrimMap

liftModuleCmd :: M.ModuleCmd a -> REPL a
liftModuleCmd :: forall a. ModuleCmd a -> REPL a
liftModuleCmd ModuleCmd a
cmd =
  do IO EvalOpts
evo <- REPL (IO EvalOpts)
getEvalOptsAction
     ModuleEnv
env <- REPL ModuleEnv
getModuleEnv
     Bool
callStacks <- REPL Bool
getCallStacks
     Solver
tcSolver <- REPL Solver
getTCSolver
     let minp :: ModuleInput IO
minp =
             M.ModuleInput
                { minpCallStacks :: Bool
minpCallStacks = Bool
callStacks
                , minpEvalOpts :: IO EvalOpts
minpEvalOpts   = IO EvalOpts
evo
                , minpByteReader :: [Char] -> IO ByteString
minpByteReader = [Char] -> IO ByteString
BS.readFile
                , minpModuleEnv :: ModuleEnv
minpModuleEnv  = ModuleEnv
env
                , minpTCSolver :: Solver
minpTCSolver   = Solver
tcSolver
                }
     ModuleRes a -> REPL a
forall a. ModuleRes a -> REPL a
moduleCmdResult (ModuleRes a -> REPL a) -> REPL (ModuleRes a) -> REPL a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (ModuleRes a) -> REPL (ModuleRes a)
forall a. IO a -> REPL a
io (ModuleCmd a
cmd ModuleInput IO
minp)

-- TODO: add filter for my exhaustie prop guards warning here

moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult :: forall a. ModuleRes a -> REPL a
moduleCmdResult (Either ModuleError (a, ModuleEnv)
res,[ModuleWarning]
ws0) = do
  Bool
warnDefaulting  <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"warnDefaulting"
  Bool
warnShadowing   <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"warnShadowing"
  Bool
warnPrefixAssoc <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"warnPrefixAssoc"
  Bool
warnNonExhConGrds <- [Char] -> REPL Bool
forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"warnNonExhaustiveConstraintGuards"
  -- XXX: let's generalize this pattern
  let isShadowWarn :: RenamerWarning -> Bool
isShadowWarn (M.SymbolShadowed {}) = Bool
True
      isShadowWarn RenamerWarning
_                     = Bool
False

      isPrefixAssocWarn :: RenamerWarning -> Bool
isPrefixAssocWarn (M.PrefixAssocChanged {}) = Bool
True
      isPrefixAssocWarn RenamerWarning
_                         = Bool
False

      filterRenamer :: Bool
-> (RenamerWarning -> Bool) -> ModuleWarning -> Maybe ModuleWarning
filterRenamer Bool
True RenamerWarning -> Bool
_ ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w
      filterRenamer Bool
_ RenamerWarning -> Bool
check (M.RenamerWarnings [RenamerWarning]
xs) =
        case (RenamerWarning -> Bool) -> [RenamerWarning] -> [RenamerWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (RenamerWarning -> Bool) -> RenamerWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RenamerWarning -> Bool
check) [RenamerWarning]
xs of
          [] -> Maybe ModuleWarning
forall a. Maybe a
Nothing
          [RenamerWarning]
ys -> ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ([RenamerWarning] -> ModuleWarning
M.RenamerWarnings [RenamerWarning]
ys)
      filterRenamer Bool
_ RenamerWarning -> Bool
_ ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w

      -- ignore certain warnings during typechecking
      filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning
      filterTypecheck :: ModuleWarning -> Maybe ModuleWarning
filterTypecheck (M.TypeCheckWarnings NameMap
nameMap [(Range, Warning)]
xs) =
        case ((Range, Warning) -> Bool)
-> [(Range, Warning)] -> [(Range, Warning)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
allow (Warning -> Bool)
-> ((Range, Warning) -> Warning) -> (Range, Warning) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range, Warning) -> Warning
forall a b. (a, b) -> b
snd) [(Range, Warning)]
xs of
          [] -> Maybe ModuleWarning
forall a. Maybe a
Nothing
          [(Range, Warning)]
ys -> ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just (NameMap -> [(Range, Warning)] -> ModuleWarning
M.TypeCheckWarnings NameMap
nameMap [(Range, Warning)]
ys)
          where
            allow :: T.Warning -> Bool
            allow :: Warning -> Bool
allow = \case
              T.DefaultingTo TVarInfo
_ Type
_ | Bool -> Bool
not Bool
warnDefaulting -> Bool
False
              T.NonExhaustivePropGuards Name
_ | Bool -> Bool
not Bool
warnNonExhConGrds -> Bool
False
              Warning
_ -> Bool
True
      filterTypecheck ModuleWarning
w = ModuleWarning -> Maybe ModuleWarning
forall a. a -> Maybe a
Just ModuleWarning
w

  let ws :: [ModuleWarning]
ws = (ModuleWarning -> Maybe ModuleWarning)
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Bool
-> (RenamerWarning -> Bool) -> ModuleWarning -> Maybe ModuleWarning
filterRenamer Bool
warnShadowing RenamerWarning -> Bool
isShadowWarn)
         ([ModuleWarning] -> [ModuleWarning])
-> ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning]
-> [ModuleWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleWarning -> Maybe ModuleWarning)
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Bool
-> (RenamerWarning -> Bool) -> ModuleWarning -> Maybe ModuleWarning
filterRenamer Bool
warnPrefixAssoc RenamerWarning -> Bool
isPrefixAssocWarn)
         ([ModuleWarning] -> [ModuleWarning])
-> ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning]
-> [ModuleWarning]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleWarning -> Maybe ModuleWarning)
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ModuleWarning -> Maybe ModuleWarning
filterTypecheck
         ([ModuleWarning] -> [ModuleWarning])
-> [ModuleWarning] -> [ModuleWarning]
forall a b. (a -> b) -> a -> b
$ [ModuleWarning]
ws0
  NameDisp
names <- ModContext -> NameDisp
M.mctxNameDisp (ModContext -> NameDisp) -> REPL ModContext -> REPL NameDisp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
  (ModuleWarning -> REPL ()) -> [ModuleWarning] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Doc Void -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc Void -> REPL ())
-> (ModuleWarning -> Doc Void) -> ModuleWarning -> REPL ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameDisp -> Doc -> Doc Void
runDoc NameDisp
names (Doc -> Doc Void)
-> (ModuleWarning -> Doc) -> ModuleWarning -> Doc Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleWarning -> Doc
forall a. PP a => a -> Doc
pp) [ModuleWarning]
ws
  case Either ModuleError (a, ModuleEnv)
res of
    Right (a
a,ModuleEnv
me') -> ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me' REPL () -> REPL a -> REPL a
forall a b. REPL a -> REPL b -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> REPL a
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    Left ModuleError
err      ->
      do ModuleError
e <- case ModuleError
err of
                M.ErrorInFile (M.InFile [Char]
file) ModuleError
e ->
                  -- on error, the file with the error becomes the edit
                  -- target.  Note, however, that the focused module is not
                  -- changed.
                  do [Char] -> REPL ()
setEditPath [Char]
file
                     ModuleError -> REPL ModuleError
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleError
e
                ModuleError
_ -> ModuleError -> REPL ModuleError
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleError
err
         REPLException -> REPL a
forall a. REPLException -> REPL a
raise (NameDisp -> ModuleError -> REPLException
ModuleSystemError NameDisp
names ModuleError
e)


replCheckExpr :: P.Expr P.PName -> REPL (P.Expr M.Name,T.Expr,T.Schema)
replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
e = ModuleCmd (Expr Name, Expr, Schema)
-> REPL (Expr Name, Expr, Schema)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd (Expr Name, Expr, Schema)
 -> REPL (Expr Name, Expr, Schema))
-> ModuleCmd (Expr Name, Expr, Schema)
-> REPL (Expr Name, Expr, Schema)
forall a b. (a -> b) -> a -> b
$ Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
M.checkExpr Expr PName
e

-- | Check declarations as though they were defined at the top-level.
replCheckDecls :: [P.Decl P.PName] -> REPL [T.DeclGroup]
replCheckDecls :: [Decl PName] -> REPL [DeclGroup]
replCheckDecls [Decl PName]
ds = do

  -- check the decls
  [Decl PName]
npds        <- ModuleCmd [Decl PName] -> REPL [Decl PName]
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([Decl PName] -> ModuleCmd [Decl PName]
forall a. RemovePatterns a => a -> ModuleCmd a
M.noPat [Decl PName]
ds)

  let mkTop :: Decl name -> TopDecl name
mkTop Decl name
d = TopLevel (Decl name) -> TopDecl name
forall name. TopLevel (Decl name) -> TopDecl name
P.Decl P.TopLevel { tlExport :: ExportType
P.tlExport = ExportType
P.Public
                                  , tlDoc :: Maybe (Located Text)
P.tlDoc    = Maybe (Located Text)
forall a. Maybe a
Nothing
                                  , tlValue :: Decl name
P.tlValue  = Decl name
d }
  (NamingEnv
names,[DeclGroup]
ds',Map Name TySyn
tyMap) <- ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
-> REPL (NamingEnv, [DeclGroup], Map Name TySyn)
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([TopDecl PName]
-> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
M.checkDecls ((Decl PName -> TopDecl PName) -> [Decl PName] -> [TopDecl PName]
forall a b. (a -> b) -> [a] -> [b]
map Decl PName -> TopDecl PName
forall {name}. Decl name -> TopDecl name
mkTop [Decl PName]
npds))

  -- extend the naming env and type synonym maps
  DynamicEnv
denv        <- REPL DynamicEnv
getDynEnv
  DynamicEnv -> REPL ()
setDynEnv DynamicEnv
denv { M.deNames  = names `M.shadowing` M.deNames denv
                 , M.deTySyns = tyMap <> M.deTySyns denv
                 }
  [DeclGroup] -> REPL [DeclGroup]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return [DeclGroup]
ds'

replSpecExpr :: T.Expr -> REPL T.Expr
replSpecExpr :: Expr -> REPL Expr
replSpecExpr Expr
e = ModuleCmd Expr -> REPL Expr
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleCmd Expr -> REPL Expr) -> ModuleCmd Expr -> REPL Expr
forall a b. (a -> b) -> a -> b
$ Expr -> ModuleCmd Expr
S.specialize Expr
e

replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replEvalExpr Expr PName
expr =
  do (Expr Name
_,Expr
def,Schema
sig) <- Expr PName -> REPL (Expr Name, Expr, Schema)
replCheckExpr Expr PName
expr
     Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
def Schema
sig REPL (Maybe (Value, Type))
-> (Maybe (Value, Type) -> REPL (Value, Type))
-> REPL (Value, Type)
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just (Value, Type)
res -> (Value, Type) -> REPL (Value, Type)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value, Type)
res
       Maybe (Value, Type)
Nothing -> REPLException -> REPL (Value, Type)
forall a. REPLException -> REPL a
raise (Schema -> REPLException
EvalPolyError Schema
sig)

replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type))
replEvalCheckedExpr :: Expr -> Schema -> REPL (Maybe (Value, Type))
replEvalCheckedExpr Expr
def Schema
sig =
  Expr -> Schema -> REPL (Maybe ([(TParam, Type)], Expr))
replPrepareCheckedExpr Expr
def Schema
sig REPL (Maybe ([(TParam, Type)], Expr))
-> (Maybe ([(TParam, Type)], Expr) -> REPL (Maybe (Value, Type)))
-> REPL (Maybe (Value, Type))
forall a b. REPL a -> (a -> REPL b) -> REPL b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    (([(TParam, Type)], Expr) -> REPL (Value, Type))
-> Maybe ([(TParam, Type)], Expr) -> REPL (Maybe (Value, Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse \([(TParam, Type)]
tys, Expr
def1) -> do
      let su :: Subst
su = [(TParam, Type)] -> Subst
T.listParamSubst [(TParam, Type)]
tys
      let ty :: Type
ty = Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
T.apSubst Subst
su (Schema -> Type
T.sType Schema
sig)
      REPL () -> REPL ()
whenDebug ([Char] -> REPL ()
rPutStrLn (Expr -> [Char]
forall a. PP (WithNames a) => a -> [Char]
dump Expr
def1))

      TypeEnv
tenv <- GenEvalEnv Concrete -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
E.envTypes (GenEvalEnv Concrete -> TypeEnv)
-> (DynamicEnv -> GenEvalEnv Concrete) -> DynamicEnv -> TypeEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynamicEnv -> GenEvalEnv Concrete
M.deEnv (DynamicEnv -> TypeEnv) -> REPL DynamicEnv -> REPL TypeEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL DynamicEnv
getDynEnv
      let tyv :: TValue
tyv = TypeEnv -> Type -> TValue
E.evalValType TypeEnv
tenv Type
ty

      -- add "it" to the namespace via a new declaration
      Name
itVar <- TValue -> Expr -> REPL Name
bindItVariable TValue
tyv Expr
def1

      let itExpr :: Expr
itExpr = case Expr -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr
def of
                      Maybe Range
Nothing  -> Name -> Expr
T.EVar Name
itVar
                      Just Range
rng -> Range -> Expr -> Expr
T.ELocated Range
rng (Name -> Expr
T.EVar Name
itVar)

      -- evaluate the it variable
      Value
val <- ModuleCmd Value -> REPL Value
forall a. ModuleCmd a -> REPL a
liftModuleCmd (IO (ModuleRes Value) -> IO (ModuleRes Value)
forall a. IO a -> IO a
rethrowEvalError (IO (ModuleRes Value) -> IO (ModuleRes Value))
-> ModuleCmd Value -> ModuleCmd Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ModuleCmd Value
M.evalExpr Expr
itExpr)
      (Value, Type) -> REPL (Value, Type)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value
val,Type
ty)

-- | Check that we are in a valid evaluation context and apply defaulting.
replPrepareCheckedExpr :: T.Expr -> T.Schema ->
  REPL (Maybe ([(T.TParam, T.Type)], T.Expr))
replPrepareCheckedExpr :: Expr -> Schema -> REPL (Maybe ([(TParam, Type)], Expr))
replPrepareCheckedExpr Expr
def Schema
sig = do
  Expr -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Expr
def
  Schema -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext Schema
sig

  Solver
s <- REPL Solver
getTCSolver
  Maybe ([(TParam, Type)], Expr)
mbDef <- IO (Maybe ([(TParam, Type)], Expr))
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. IO a -> REPL a
io (Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
defaultReplExpr Solver
s Expr
def Schema
sig)

  case Maybe ([(TParam, Type)], Expr)
mbDef of
    Maybe ([(TParam, Type)], Expr)
Nothing -> Maybe ([(TParam, Type)], Expr)
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([(TParam, Type)], Expr)
forall a. Maybe a
Nothing
    Just ([(TParam, Type)]
tys, Expr
def1) -> do
      [(TParam, Type)] -> REPL ()
forall {a}. PP a => [(TParam, a)] -> REPL ()
warnDefaults [(TParam, Type)]
tys
      Maybe ([(TParam, Type)], Expr)
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ([(TParam, Type)], Expr)
 -> REPL (Maybe ([(TParam, Type)], Expr)))
-> Maybe ([(TParam, Type)], Expr)
-> REPL (Maybe ([(TParam, Type)], Expr))
forall a b. (a -> b) -> a -> b
$ ([(TParam, Type)], Expr) -> Maybe ([(TParam, Type)], Expr)
forall a. a -> Maybe a
Just ([(TParam, Type)]
tys, Expr
def1)
  where
  warnDefaults :: [(TParam, a)] -> REPL ()
warnDefaults [(TParam, a)]
ts =
    case [(TParam, a)]
ts of
      [] -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      [(TParam, a)]
_  -> do [Char] -> REPL ()
rPutStrLn [Char]
"Showing a specific instance of polymorphic result:"
               ((TParam, a) -> REPL ()) -> [(TParam, a)] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TParam, a) -> REPL ()
forall {a}. PP a => (TParam, a) -> REPL ()
warnDefault [(TParam, a)]
ts

  warnDefault :: (TParam, a) -> REPL ()
warnDefault (TParam
x,a
t) =
    Doc -> REPL ()
forall a. Show a => a -> REPL ()
rPrint (Doc
"  *" Doc -> Doc -> Doc
<+> Int -> Doc -> Doc
nest Int
2  (Doc
"Using" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (a -> Doc
forall a. PP a => a -> Doc
pp a
t) Doc -> Doc -> Doc
<+> Doc
"for" Doc -> Doc -> Doc
<+>
                                TypeSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
T.tvarDesc (TParam -> TVarInfo
T.tpInfo TParam
x))))

itIdent :: M.Ident
itIdent :: Ident
itIdent  = [Char] -> Ident
M.packIdent [Char]
"it"

replWriteFile :: FilePath -> BS.ByteString -> REPL CommandResult
replWriteFile :: [Char] -> ByteString -> REPL CommandResult
replWriteFile = ([Char] -> ByteString -> IO ())
-> [Char] -> ByteString -> REPL CommandResult
forall a.
([Char] -> a -> IO ()) -> [Char] -> a -> REPL CommandResult
replWriteFileWith [Char] -> ByteString -> IO ()
BS.writeFile

replWriteFileString :: FilePath -> String -> REPL CommandResult
replWriteFileString :: [Char] -> [Char] -> REPL CommandResult
replWriteFileString = ([Char] -> [Char] -> IO ())
-> [Char] -> [Char] -> REPL CommandResult
forall a.
([Char] -> a -> IO ()) -> [Char] -> a -> REPL CommandResult
replWriteFileWith [Char] -> [Char] -> IO ()
writeFile

replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a -> REPL CommandResult
replWriteFileWith :: forall a.
([Char] -> a -> IO ()) -> [Char] -> a -> REPL CommandResult
replWriteFileWith [Char] -> a -> IO ()
write [Char]
fp a
contents =
 do Either SomeException ()
x <- IO (Either SomeException ()) -> REPL (Either SomeException ())
forall a. IO a -> REPL a
io (IO () -> IO (Either SomeException ())
forall e a. Exception e => IO a -> IO (Either e a)
X.try ([Char] -> a -> IO ()
write [Char]
fp a
contents))
    case Either SomeException ()
x of
      Left SomeException
e ->
        do [Char] -> REPL ()
rPutStrLn (SomeException -> [Char]
forall a. Show a => a -> [Char]
show (SomeException
e :: X.SomeException))
           CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
      Right ()
_ ->
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

replReadFile :: FilePath -> (X.SomeException -> REPL (Maybe BS.ByteString)) -> REPL (Maybe BS.ByteString)
replReadFile :: [Char]
-> (SomeException -> REPL (Maybe ByteString))
-> REPL (Maybe ByteString)
replReadFile [Char]
fp SomeException -> REPL (Maybe ByteString)
handler =
 do Either SomeException ByteString
x <- IO (Either SomeException ByteString)
-> REPL (Either SomeException ByteString)
forall a. IO a -> REPL a
io (IO (Either SomeException ByteString)
 -> REPL (Either SomeException ByteString))
-> IO (Either SomeException ByteString)
-> REPL (Either SomeException ByteString)
forall a b. (a -> b) -> a -> b
$ IO (Either SomeException ByteString)
-> (SomeException -> IO (Either SomeException ByteString))
-> IO (Either SomeException ByteString)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
X.catch (ByteString -> Either SomeException ByteString
forall a b. b -> Either a b
Right (ByteString -> Either SomeException ByteString)
-> IO ByteString -> IO (Either SomeException ByteString)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Char] -> IO ByteString
BS.readFile [Char]
fp) (\SomeException
e -> Either SomeException ByteString
-> IO (Either SomeException ByteString)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SomeException ByteString
 -> IO (Either SomeException ByteString))
-> Either SomeException ByteString
-> IO (Either SomeException ByteString)
forall a b. (a -> b) -> a -> b
$ SomeException -> Either SomeException ByteString
forall a b. a -> Either a b
Left SomeException
e)
    (SomeException -> REPL (Maybe ByteString))
-> (ByteString -> REPL (Maybe ByteString))
-> Either SomeException ByteString
-> REPL (Maybe ByteString)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SomeException -> REPL (Maybe ByteString)
handler (Maybe ByteString -> REPL (Maybe ByteString)
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ByteString -> REPL (Maybe ByteString))
-> (ByteString -> Maybe ByteString)
-> ByteString
-> REPL (Maybe ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just) Either SomeException ByteString
x

-- | Creates a fresh binding of "it" to the expression given, and adds
-- it to the current dynamic environment.  The fresh name generated
-- is returned.
bindItVariable :: E.TValue -> T.Expr -> REPL T.Name
bindItVariable :: TValue -> Expr -> REPL Name
bindItVariable TValue
ty Expr
expr = do
  Name
freshIt <- Ident -> NameSource -> REPL Name
freshName Ident
itIdent NameSource
M.UserName
  let schema :: Schema
schema = T.Forall { sVars :: [TParam]
T.sVars  = []
                        , sProps :: [Type]
T.sProps = []
                        , sType :: Type
T.sType  = TValue -> Type
E.tValTy TValue
ty
                        }
      decl :: Decl
decl = T.Decl { dName :: Name
T.dName       = Name
freshIt
                    , dSignature :: Schema
T.dSignature  = Schema
schema
                    , dDefinition :: DeclDef
T.dDefinition = Expr -> DeclDef
T.DExpr Expr
expr
                    , dPragmas :: [Pragma]
T.dPragmas    = []
                    , dInfix :: Bool
T.dInfix      = Bool
False
                    , dFixity :: Maybe Fixity
T.dFixity     = Maybe Fixity
forall a. Maybe a
Nothing
                    , dDoc :: Maybe Text
T.dDoc        = Maybe Text
forall a. Maybe a
Nothing
                    }
  ModuleCmd () -> REPL ()
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([DeclGroup] -> ModuleCmd ()
M.evalDecls [Decl -> DeclGroup
T.NonRecursive Decl
decl])
  DynamicEnv
denv <- REPL DynamicEnv
getDynEnv
  let nenv' :: NamingEnv
nenv' = Namespace -> PName -> Name -> NamingEnv
M.singletonNS Namespace
M.NSValue (Ident -> PName
P.UnQual Ident
itIdent) Name
freshIt
                           NamingEnv -> NamingEnv -> NamingEnv
`M.shadowing` DynamicEnv -> NamingEnv
M.deNames DynamicEnv
denv
  DynamicEnv -> REPL ()
setDynEnv (DynamicEnv -> REPL ()) -> DynamicEnv -> REPL ()
forall a b. (a -> b) -> a -> b
$ DynamicEnv
denv { M.deNames = nenv' }
  Name -> REPL Name
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
freshIt


-- | Extend the dynamic environment with a fresh binding for "it",
-- as defined by the given value.  If we cannot determine the definition
-- of the value, then we don't bind `it`.
bindItVariableVal :: E.TValue -> Concrete.Value -> REPL ()
bindItVariableVal :: TValue -> Value -> REPL ()
bindItVariableVal TValue
ty Value
val =
  do PrimMap
prims   <- REPL PrimMap
getPrimMap
     Maybe Expr
mb      <- Eval (Maybe Expr) -> REPL (Maybe Expr)
forall a. Eval a -> REPL a
rEval (PrimMap -> TValue -> Value -> Eval (Maybe Expr)
Concrete.toExpr PrimMap
prims TValue
ty Value
val)
     case Maybe Expr
mb of
       Maybe Expr
Nothing   -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       Just Expr
expr -> REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
ty Expr
expr


-- | Creates a fresh binding of "it" to a finite sequence of
-- expressions of the same type, and adds that sequence to the current
-- dynamic environment
bindItVariables :: E.TValue -> [T.Expr] -> REPL ()
bindItVariables :: TValue -> [Expr] -> REPL ()
bindItVariables TValue
ty [Expr]
exprs = REPL Name -> REPL ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (REPL Name -> REPL ()) -> REPL Name -> REPL ()
forall a b. (a -> b) -> a -> b
$ TValue -> Expr -> REPL Name
bindItVariable TValue
seqTy Expr
seqExpr
  where
    len :: Int
len = [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
exprs
    seqTy :: TValue
seqTy = Integer -> TValue -> TValue
E.TVSeq (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len) TValue
ty
    seqExpr :: Expr
seqExpr = [Expr] -> Type -> Expr
T.EList [Expr]
exprs (TValue -> Type
E.tValTy TValue
ty)

replEvalDecls :: [P.Decl P.PName] -> REPL ()
replEvalDecls :: [Decl PName] -> REPL ()
replEvalDecls [Decl PName]
ds = do
  [DeclGroup]
dgs <- [Decl PName] -> REPL [DeclGroup]
replCheckDecls [Decl PName]
ds
  [DeclGroup] -> REPL ()
forall a. FreeVars a => a -> REPL ()
validEvalContext [DeclGroup]
dgs
  REPL () -> REPL ()
whenDebug ((DeclGroup -> REPL ()) -> [DeclGroup] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\DeclGroup
dg -> ([Char] -> REPL ()
rPutStrLn (DeclGroup -> [Char]
forall a. PP (WithNames a) => a -> [Char]
dump DeclGroup
dg))) [DeclGroup]
dgs)
  ModuleCmd () -> REPL ()
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([DeclGroup] -> ModuleCmd ()
M.evalDecls [DeclGroup]
dgs)

replEdit :: String -> REPL Bool
replEdit :: [Char] -> REPL Bool
replEdit [Char]
file = do
  Maybe [Char]
mb <- IO (Maybe [Char]) -> REPL (Maybe [Char])
forall a. IO a -> REPL a
io ([Char] -> IO (Maybe [Char])
lookupEnv [Char]
"EDITOR")
  let editor :: [Char]
editor = [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"vim" Maybe [Char]
mb
  IO Bool -> REPL Bool
forall a. IO a -> REPL a
io (IO Bool -> REPL Bool) -> IO Bool -> REPL Bool
forall a b. (a -> b) -> a -> b
$ do
    (Maybe Handle
_,Maybe Handle
_,Maybe Handle
_,ProcessHandle
ph) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess ([Char] -> CreateProcess
shell ([[Char]] -> [Char]
unwords [[Char]
editor, [Char]
file]))
    ExitCode
exit       <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
    Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode
exit ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== ExitCode
ExitSuccess)

type CommandMap = Trie CommandDescr

newSeedCmd :: REPL CommandResult
newSeedCmd :: REPL CommandResult
newSeedCmd =
  do  (Word64, Word64, Word64, Word64)
seed <- REPL (Word64, Word64, Word64, Word64)
createAndSetSeed
      [Char] -> REPL ()
rPutStrLn [Char]
"Seed initialized to:"
      let value :: [Char]
value = (Word64, Word64, Word64, Word64) -> [Char]
forall a. Show a => a -> [Char]
show (Word64, Word64, Word64, Word64)
seed
      [Char] -> REPL ()
rPutStrLn [Char]
value
      CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crValue = Just value }
  where
    createAndSetSeed :: REPL (Word64, Word64, Word64, Word64)
createAndSetSeed =
      (TFGen -> REPL ((Word64, Word64, Word64, Word64), TFGen))
-> REPL (Word64, Word64, Word64, Word64)
forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen ((TFGen -> REPL ((Word64, Word64, Word64, Word64), TFGen))
 -> REPL (Word64, Word64, Word64, Word64))
-> (TFGen -> REPL ((Word64, Word64, Word64, Word64), TFGen))
-> REPL (Word64, Word64, Word64, Word64)
forall a b. (a -> b) -> a -> b
$ \TFGen
g0 ->
        let (Word64
s1, TFGen
g1) = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g0
            (Word64
s2, TFGen
g2) = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g1
            (Word64
s3, TFGen
g3) = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g2
            (Word64
s4, TFGen
_)  = TFGen -> (Word64, TFGen)
forall g. RandomGen g => g -> (Word64, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
TFI.random TFGen
g3
            seed :: (Word64, Word64, Word64, Word64)
seed = (Word64
s1, Word64
s2, Word64
s3, Word64
s4)
        in  ((Word64, Word64, Word64, Word64), TFGen)
-> REPL ((Word64, Word64, Word64, Word64), TFGen)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Word64, Word64, Word64, Word64)
seed, (Word64, Word64, Word64, Word64) -> TFGen
TF.seedTFGen (Word64, Word64, Word64, Word64)
seed)

seedCmd :: String -> REPL CommandResult
seedCmd :: [Char] -> REPL CommandResult
seedCmd [Char]
s =
  do Bool
success <- case Maybe TFGen
mbGen of
       Maybe TFGen
Nothing -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn [Char]
"Could not parse seed argument - expecting an integer or 4-tuple of integers."
       Just TFGen
gen -> Bool
True Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TFGen -> REPL ()
setRandomGen TFGen
gen
     CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = success }

  where
    mbGen :: Maybe TFGen
mbGen =
          (Int -> TFGen
TF.mkTFGen (Int -> TFGen) -> Maybe Int -> Maybe TFGen
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> Maybe Int
forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
s)
      Maybe TFGen -> Maybe TFGen -> Maybe TFGen
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Word64, Word64, Word64, Word64) -> TFGen
TF.seedTFGen ((Word64, Word64, Word64, Word64) -> TFGen)
-> Maybe (Word64, Word64, Word64, Word64) -> Maybe TFGen
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> Maybe (Word64, Word64, Word64, Word64)
forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
s)

-- Command Parsing -------------------------------------------------------------

-- | Strip leading space.
sanitize :: String -> String
sanitize :: ShowS
sanitize  = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace

-- | Strip trailing space.
sanitizeEnd :: String -> String
sanitizeEnd :: ShowS
sanitizeEnd = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
sanitize ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse

trim :: String -> String
trim :: ShowS
trim = ShowS
sanitizeEnd ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
sanitize

-- | Split at the first word boundary.
splitCommand :: String -> Maybe (Int,String,String)
splitCommand :: [Char] -> Maybe (Int, [Char], [Char])
splitCommand = Int -> [Char] -> Maybe (Int, [Char], [Char])
go Int
0
  where
   go :: Int -> [Char] -> Maybe (Int, [Char], [Char])
go !Int
len (Char
c  : [Char]
more)
      | Char -> Bool
isSpace Char
c = Int -> [Char] -> Maybe (Int, [Char], [Char])
go (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Char]
more

   go !Int
len (Char
':': [Char]
more)
      | ([Char]
as,[Char]
bs) <- (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Char
x -> Char -> Bool
isPunctuation Char
x Bool -> Bool -> Bool
|| Char -> Bool
isSymbol Char
x) [Char]
more
      , ([Char]
ws,[Char]
cs) <- (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace [Char]
bs
      , Bool -> Bool
not ([Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
as) = (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a. a -> Maybe a
Just (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+[Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
asInt -> Int -> Int
forall a. Num a => a -> a -> a
+[Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
ws, Char
':' Char -> ShowS
forall a. a -> [a] -> [a]
: [Char]
as, [Char]
cs)

      | ([Char]
as,[Char]
bs) <- (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace [Char]
more
      , ([Char]
ws,[Char]
cs) <- (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace [Char]
bs
      , Bool -> Bool
not ([Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
as) = (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a. a -> Maybe a
Just (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+[Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
asInt -> Int -> Int
forall a. Num a => a -> a -> a
+[Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
ws, Char
':' Char -> ShowS
forall a. a -> [a] -> [a]
: [Char]
as, [Char]
cs)

      | Bool
otherwise = Maybe (Int, [Char], [Char])
forall a. Maybe a
Nothing

   go !Int
len [Char]
expr
      | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
expr = Maybe (Int, [Char], [Char])
forall a. Maybe a
Nothing
      | Bool
otherwise = (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a. a -> Maybe a
Just (Int
lenInt -> Int -> Int
forall a. Num a => a -> a -> a
+[Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
expr, [Char]
expr, [])

-- | Uncons a list.
uncons :: [a] -> Maybe (a,[a])
uncons :: forall a. [a] -> Maybe (a, [a])
uncons [a]
as = case [a]
as of
  a
a:[a]
rest -> (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
a,[a]
rest)
  [a]
_      -> Maybe (a, [a])
forall a. Maybe a
Nothing

-- | Lookup a string in the command list.
findCommand :: String -> [CommandDescr]
findCommand :: [Char] -> [CommandDescr]
findCommand [Char]
str = [Char] -> CommandMap -> [CommandDescr]
forall a. [Char] -> Trie a -> [a]
lookupTrie [Char]
str CommandMap
commands

-- | Lookup a string in the command list, returning an exact match
-- even if it's the prefix of another command.
findCommandExact :: String -> [CommandDescr]
findCommandExact :: [Char] -> [CommandDescr]
findCommandExact [Char]
str = [Char] -> CommandMap -> [CommandDescr]
forall a. [Char] -> Trie a -> [a]
lookupTrieExact [Char]
str CommandMap
commands

-- | Lookup a string in the notebook-safe command list.
findNbCommand :: Bool -> String -> [CommandDescr]
findNbCommand :: Bool -> [Char] -> [CommandDescr]
findNbCommand Bool
True  [Char]
str = [Char] -> CommandMap -> [CommandDescr]
forall a. [Char] -> Trie a -> [a]
lookupTrieExact [Char]
str CommandMap
nbCommands
findNbCommand Bool
False [Char]
str = [Char] -> CommandMap -> [CommandDescr]
forall a. [Char] -> Trie a -> [a]
lookupTrie      [Char]
str CommandMap
nbCommands

-- | Parse a line as a command.
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
parseCommand :: ([Char] -> [CommandDescr]) -> [Char] -> Maybe Command
parseCommand [Char] -> [CommandDescr]
findCmd [Char]
line = do
  (Int
cmdLen,[Char]
cmd,[Char]
args) <- [Char] -> Maybe (Int, [Char], [Char])
splitCommand [Char]
line
  let args' :: [Char]
args' = ShowS
sanitizeEnd [Char]
args
  case [Char] -> [CommandDescr]
findCmd [Char]
cmd of
    [CommandDescr
c] -> case CommandDescr -> CommandBody
cBody CommandDescr
c of
      ExprArg     [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
l Maybe [Char]
fp -> ([Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
body [Char]
args' (Int
l,Int
cmdLenInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Maybe [Char]
fp))
      DeclsArg    [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body [Char]
args'))
      ExprTypeArg [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body [Char]
args'))
      ModNameArg  [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body [Char]
args'))
      FilenameArg [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body ([Char] -> REPL CommandResult) -> REPL [Char] -> REPL CommandResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Char] -> REPL [Char]
expandHome [Char]
args'))
      OptionArg   [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body [Char]
args'))
      ShellArg    [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body [Char]
args'))
      HelpArg     [Char] -> REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> ([Char] -> REPL CommandResult
body [Char]
args'))
      NoArg       REPL CommandResult
body -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
_ Maybe [Char]
_ -> REPL CommandResult
body)
      FileExprArg [Char]
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
body ->
           do (Int
fpLen,[Char]
fp,[Char]
expr) <- [Char] -> Maybe (Int, [Char], [Char])
extractFilePath [Char]
args'
              Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command \Int
l Maybe [Char]
fp' -> do let col :: Int
col = Int
cmdLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
fpLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                                         [Char]
hm <- [Char] -> REPL [Char]
expandHome [Char]
fp
                                         [Char]
-> [Char] -> (Int, Int) -> Maybe [Char] -> REPL CommandResult
body [Char]
hm [Char]
expr (Int
l,Int
col) Maybe [Char]
fp')
    [] -> case [Char] -> Maybe (Char, [Char])
forall a. [a] -> Maybe (a, [a])
uncons [Char]
cmd of
      Just (Char
':',[Char]
_) -> Command -> Maybe Command
forall a. a -> Maybe a
Just ([Char] -> Command
Unknown [Char]
cmd)
      Just (Char, [Char])
_       -> Command -> Maybe Command
forall a. a -> Maybe a
Just ((Int -> Maybe [Char] -> REPL CommandResult) -> Command
Command ([Char] -> Int -> Maybe [Char] -> REPL CommandResult
evalCmd [Char]
line))
      Maybe (Char, [Char])
_            -> Maybe Command
forall a. Maybe a
Nothing

    [CommandDescr]
cs -> Command -> Maybe Command
forall a. a -> Maybe a
Just ([Char] -> [[Char]] -> Command
Ambiguous [Char]
cmd ((CommandDescr -> [[Char]]) -> [CommandDescr] -> [[Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CommandDescr -> [[Char]]
cNames [CommandDescr]
cs))

  where
  expandHome :: [Char] -> REPL [Char]
expandHome [Char]
path =
    case [Char]
path of
      Char
'~' : Char
c : [Char]
more | Char -> Bool
isPathSeparator Char
c -> do [Char]
dir <- IO [Char] -> REPL [Char]
forall a. IO a -> REPL a
io IO [Char]
getHomeDirectory
                                               [Char] -> REPL [Char]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
dir [Char] -> ShowS
</> [Char]
more)
      [Char]
_ -> [Char] -> REPL [Char]
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
path

  extractFilePath :: [Char] -> Maybe (Int, [Char], [Char])
extractFilePath [Char]
ipt =
    let quoted :: a -> [a] -> (Int, [a], [a])
quoted a
q = (\([a]
a,[a]
b) -> ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2, [a]
a, Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
1 [a]
b)) (([a], [a]) -> (Int, [a], [a]))
-> ([a] -> ([a], [a])) -> [a] -> (Int, [a], [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
q)
    in case [Char]
ipt of
        [Char]
""        -> Maybe (Int, [Char], [Char])
forall a. Maybe a
Nothing
        Char
'\'':[Char]
rest -> (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a. a -> Maybe a
Just ((Int, [Char], [Char]) -> Maybe (Int, [Char], [Char]))
-> (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a b. (a -> b) -> a -> b
$ Char -> [Char] -> (Int, [Char], [Char])
forall {a}. Eq a => a -> [a] -> (Int, [a], [a])
quoted Char
'\'' [Char]
rest
        Char
'"':[Char]
rest  -> (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a. a -> Maybe a
Just ((Int, [Char], [Char]) -> Maybe (Int, [Char], [Char]))
-> (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a b. (a -> b) -> a -> b
$ Char -> [Char] -> (Int, [Char], [Char])
forall {a}. Eq a => a -> [a] -> (Int, [a], [a])
quoted Char
'"' [Char]
rest
        [Char]
_         -> let ([Char]
a,[Char]
b) = (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace [Char]
ipt in
                     if [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
a then Maybe (Int, [Char], [Char])
forall a. Maybe a
Nothing else (Int, [Char], [Char]) -> Maybe (Int, [Char], [Char])
forall a. a -> Maybe a
Just ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
a, [Char]
a, [Char]
b)



moduleInfoCmd :: Bool -> String -> REPL CommandResult
moduleInfoCmd :: Bool -> [Char] -> REPL CommandResult
moduleInfoCmd Bool
isFile [Char]
name
  | Bool
isFile = (ModulePath, FileInfo) -> REPL CommandResult
showInfo ((ModulePath, FileInfo) -> REPL CommandResult)
-> REPL (ModulePath, FileInfo) -> REPL CommandResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleCmd (ModulePath, FileInfo) -> REPL (ModulePath, FileInfo)
forall a. ModuleCmd a -> REPL a
liftModuleCmd ([Char] -> ModuleCmd (ModulePath, FileInfo)
M.getFileDependencies [Char]
name)
  | Bool
otherwise =
    case [Char] -> Maybe ModName
parseModName [Char]
name of
      Just ModName
m  -> (ModulePath, FileInfo) -> REPL CommandResult
showInfo ((ModulePath, FileInfo) -> REPL CommandResult)
-> REPL (ModulePath, FileInfo) -> REPL CommandResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleCmd (ModulePath, FileInfo) -> REPL (ModulePath, FileInfo)
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModName -> ModuleCmd (ModulePath, FileInfo)
M.getModuleDependencies ModName
m)
      Maybe ModName
Nothing -> do [Char] -> REPL ()
rPutStrLn [Char]
"Invalid module name."
                    CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }

  where
  showInfo :: (ModulePath, FileInfo) -> REPL CommandResult
showInfo (ModulePath
p,FileInfo
fi) =
    do [Char] -> REPL ()
rPutStr [Char]
"{ \"source\": "
       case ModulePath
p of
         M.InFile [Char]
f  -> [Char] -> REPL ()
rPutStrLn (ShowS
forall a. Show a => a -> [Char]
show [Char]
f)
         M.InMem [Char]
l ByteString
_ -> [Char] -> REPL ()
rPutStrLn ([Char]
"{ \"internal\": " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
l [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" }")

       [Char] -> REPL ()
rPutStrLn ([Char]
", \"fingerprint\": \"0x" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                       Fingerprint -> [Char]
fingerprintHexString (FileInfo -> Fingerprint
M.fiFingerprint FileInfo
fi) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\"")

       let depList :: (t -> [Char]) -> [Char] -> [t] -> REPL ()
depList t -> [Char]
f [Char]
x [t]
ys =
             do [Char] -> REPL ()
rPutStr ([Char]
", " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show ([Char]
x :: String) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":")
                case [t]
ys of
                  [] -> [Char] -> REPL ()
rPutStrLn [Char]
" []"
                  t
i : [t]
is ->
                    do [Char] -> REPL ()
rPutStrLn [Char]
""
                       [Char] -> REPL ()
rPutStrLn ([Char]
"     [ " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [Char]
f t
i)
                       (t -> REPL ()) -> [t] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\t
j -> [Char] -> REPL ()
rPutStrLn ([Char]
"     , " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [Char]
f t
j)) [t]
is
                       [Char] -> REPL ()
rPutStrLn [Char]
"     ]"

       ShowS -> [Char] -> [[Char]] -> REPL ()
forall {t}. (t -> [Char]) -> [Char] -> [t] -> REPL ()
depList ShowS
forall a. Show a => a -> [Char]
show               [Char]
"includes" (Set [Char] -> [[Char]]
forall a. Set a -> [a]
Set.toList (FileInfo -> Set [Char]
M.fiIncludeDeps FileInfo
fi))
       (ModName -> [Char]) -> [Char] -> [ModName] -> REPL ()
forall {t}. (t -> [Char]) -> [Char] -> [t] -> REPL ()
depList (ShowS
forall a. Show a => a -> [Char]
show ShowS -> (ModName -> [Char]) -> ModName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> (ModName -> Doc) -> ModName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> Doc
forall a. PP a => a -> Doc
pp) [Char]
"imports"  (Set ModName -> [ModName]
forall a. Set a -> [a]
Set.toList (FileInfo -> Set ModName
M.fiImportDeps  FileInfo
fi))
       (([Char], Bool) -> [Char]) -> [Char] -> [([Char], Bool)] -> REPL ()
forall {t}. (t -> [Char]) -> [Char] -> [t] -> REPL ()
depList ([Char], Bool) -> [Char]
forall a. Show a => a -> [Char]
show               [Char]
"foreign"  (Map [Char] Bool -> [([Char], Bool)]
forall k a. Map k a -> [(k, a)]
Map.toList (FileInfo -> Map [Char] Bool
M.fiForeignDeps FileInfo
fi))

       [Char] -> REPL ()
rPutStrLn [Char]
"}"
       CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

-- | Extract the code blocks from the body of a docstring.
--
-- A single code block starts with at least 3 backticks followed by an
-- optional language specifier of "cryptol". This allowed other kinds
-- of code blocks to be included (and ignored) in docstrings. Longer
-- backtick sequences can be used when a code block needs to be able to
-- contain backtick sequences.
--
-- @
-- /**
--  * A docstring example
--  *
--  * ```cryptol
--  * :check example
--  * ```
--  */
-- @
extractCodeBlocks :: T.Text -> [[T.Text]]
extractCodeBlocks :: Text -> [[Text]]
extractCodeBlocks Text
raw = [[Text]] -> [Text] -> [[Text]]
go [] (Text -> [Text]
T.lines Text
raw)
  where
    go :: [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished [] = [[Text]] -> [[Text]]
forall a. [a] -> [a]
reverse [[Text]]
finished
    go [[Text]]
finished (Text
x:[Text]
xs)
      | (Text
spaces, Text
x1) <- (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x
      , (Text
ticks, Text
x2) <- (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
'`' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x1
      , Int
3 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Text -> Int
T.length Text
ticks
      , Bool -> Bool
not (Char -> Text -> Bool
T.elem Char
'`' Text
x2)
      , let info :: Text
info = Text -> Text
T.strip Text
x2
      = if Text
info Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text
"", Text
"repl"] -- supported languages "unlabeled" and repl
        then [[Text]] -> Int -> Int -> [Text] -> [Text] -> [[Text]]
keep [[Text]]
finished (Text -> Int
T.length Text
spaces) (Text -> Int
T.length Text
ticks) [] [Text]
xs
        else [[Text]] -> Text -> [Text] -> [[Text]]
skip [[Text]]
finished Text
ticks [Text]
xs
      | Bool
otherwise = [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished [Text]
xs

    -- process a code block that we're keeping
    keep :: [[Text]] -> Int -> Int -> [Text] -> [Text] -> [[Text]]
keep [[Text]]
finished Int
_ Int
_ [Text]
acc [] = [[Text]] -> [Text] -> [[Text]]
go ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
acc [Text] -> [[Text]] -> [[Text]]
forall a. a -> [a] -> [a]
: [[Text]]
finished) [] -- unterminated code fences are defined to be terminated by github
    keep [[Text]]
finished Int
indentLen Int
ticksLen [Text]
acc (Text
x:[Text]
xs)
      | Text
x1 <- (Char -> Bool) -> Text -> Text
T.dropWhile (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x
      , (Text
ticks, Text
x2) <- (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
'`' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x1
      , Int
ticksLen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Text -> Int
T.length Text
ticks
      , (Char -> Bool) -> Text -> Bool
T.all (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x2
      = [[Text]] -> [Text] -> [[Text]]
go ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
acc [Text] -> [[Text]] -> [[Text]]
forall a. a -> [a] -> [a]
: [[Text]]
finished) [Text]
xs

      | Bool
otherwise =
        let x' :: Text
x' =
              case (Char -> Bool) -> Text -> (Text, Text)
T.span (Char
' ' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) Text
x of
                (Text
spaces, Text
x1)
                  | Text -> Int
T.length Text
spaces Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
indentLen -> Text
x1
                  | Bool
otherwise -> Int -> Text -> Text
T.drop Int
indentLen Text
x
        in [[Text]] -> Int -> Int -> [Text] -> [Text] -> [[Text]]
keep [[Text]]
finished Int
indentLen Int
ticksLen (Text
x' Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
acc) [Text]
xs

    -- process a code block that we're skipping
    skip :: [[Text]] -> Text -> [Text] -> [[Text]]
skip [[Text]]
finished Text
_ [] = [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished []
    skip [[Text]]
finished Text
close (Text
x:[Text]
xs)
      | Text
close Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
x = [[Text]] -> [Text] -> [[Text]]
go [[Text]]
finished [Text]
xs
      | Bool
otherwise = [[Text]] -> Text -> [Text] -> [[Text]]
skip [[Text]]
finished Text
close [Text]
xs

data SubcommandResult = SubcommandResult
  { SubcommandResult -> Text
srInput :: T.Text
  , SubcommandResult -> CommandResult
srResult :: CommandResult
  , SubcommandResult -> [Char]
srLog :: String
  }

-- | Check a single code block from inside a docstring.
--
-- The result will contain the results of processing the commands up to
-- the first failure.
--
-- Execution of the commands is run in an isolated REPL environment.
checkBlock ::
  [T.Text] {- ^ lines of the code block -} ->
  REPL [SubcommandResult]
checkBlock :: [Text] -> REPL [SubcommandResult]
checkBlock = REPL [SubcommandResult] -> REPL [SubcommandResult]
forall a. REPL a -> REPL a
isolated (REPL [SubcommandResult] -> REPL [SubcommandResult])
-> ([Text] -> REPL [SubcommandResult])
-> [Text]
-> REPL [SubcommandResult]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> REPL [SubcommandResult]
go
  where
    go :: [Text] -> REPL [SubcommandResult]
go [] = [SubcommandResult] -> REPL [SubcommandResult]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go (Text
line:[Text]
block) =
      case ([Char] -> [CommandDescr]) -> [Char] -> Maybe Command
parseCommand (Bool -> [Char] -> [CommandDescr]
findNbCommand Bool
True) (Text -> [Char]
T.unpack Text
line) of
        Maybe Command
Nothing -> do
          [SubcommandResult] -> REPL [SubcommandResult]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SubcommandResult
            { srInput :: Text
srInput = Text
line
            , srLog :: [Char]
srLog = [Char]
"Failed to parse command"
            , srResult :: CommandResult
srResult = CommandResult
emptyCommandResult { crSuccess = False }
            }]
        Just Ambiguous{} -> do
          [SubcommandResult] -> REPL [SubcommandResult]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SubcommandResult
            { srInput :: Text
srInput = Text
line
            , srLog :: [Char]
srLog = [Char]
"Ambiguous command"
            , srResult :: CommandResult
srResult = CommandResult
emptyCommandResult { crSuccess = False }
            }]
        Just Unknown{} -> do
          [SubcommandResult] -> REPL [SubcommandResult]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SubcommandResult
            { srInput :: Text
srInput = Text
line
            , srLog :: [Char]
srLog = [Char]
"Unknown command"
            , srResult :: CommandResult
srResult = CommandResult
emptyCommandResult { crSuccess = False }
            }]
        Just (Command Int -> Maybe [Char] -> REPL CommandResult
cmd) -> do
          ([Char]
logtxt, Either REPLException CommandResult
eresult) <- REPL (Either REPLException CommandResult)
-> REPL ([Char], Either REPLException CommandResult)
forall a. REPL a -> REPL ([Char], a)
captureLog (REPL CommandResult -> REPL (Either REPLException CommandResult)
forall a. REPL a -> REPL (Either REPLException a)
Cryptol.REPL.Monad.try (Int -> Maybe [Char] -> REPL CommandResult
cmd Int
0 Maybe [Char]
forall a. Maybe a
Nothing))
          case Either REPLException CommandResult
eresult of
            Left REPLException
e -> do
              let result :: SubcommandResult
result = SubcommandResult
                    { srInput :: Text
srInput = Text
line
                    , srLog :: [Char]
srLog = [Char]
logtxt [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (REPLException -> Doc
forall a. PP a => a -> Doc
pp REPLException
e) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
                    , srResult :: CommandResult
srResult = CommandResult
emptyCommandResult { crSuccess = False }
                    }
              [SubcommandResult] -> REPL [SubcommandResult]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SubcommandResult
result]
            Right CommandResult
result -> do
              let subresult :: SubcommandResult
subresult = SubcommandResult
                    { srInput :: Text
srInput = Text
line
                    , srLog :: [Char]
srLog = [Char]
logtxt
                    , srResult :: CommandResult
srResult = CommandResult
result
                    }
              [SubcommandResult]
subresults <- [Text] -> REPL [SubcommandResult]
checkBlock [Text]
block
              [SubcommandResult] -> REPL [SubcommandResult]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SubcommandResult
subresult SubcommandResult -> [SubcommandResult] -> [SubcommandResult]
forall a. a -> [a] -> [a]
: [SubcommandResult]
subresults)

captureLog :: REPL a -> REPL (String, a)
captureLog :: forall a. REPL a -> REPL ([Char], a)
captureLog REPL a
m = do
  Logger
previousLogger <- REPL Logger
getLogger
  IORef [[Char]]
outputsRef <- IO (IORef [[Char]]) -> REPL (IORef [[Char]])
forall a. IO a -> REPL a
io ([[Char]] -> IO (IORef [[Char]])
forall a. a -> IO (IORef a)
newIORef [])
  ([Char] -> IO ()) -> REPL ()
setPutStr (\[Char]
str -> IORef [[Char]] -> ([[Char]] -> [[Char]]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [[Char]]
outputsRef ([Char]
str[Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:))
  a
result <- REPL a
m REPL a -> REPL () -> REPL a
forall a b. REPL a -> REPL b -> REPL a
`finally` Logger -> REPL ()
setLogger Logger
previousLogger
  [[Char]]
outputs <- IO [[Char]] -> REPL [[Char]]
forall a. IO a -> REPL a
io (IORef [[Char]] -> IO [[Char]]
forall a. IORef a -> IO a
readIORef IORef [[Char]]
outputsRef)
  let output :: [Char]
output = ShowS
interpretControls ([[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Char]] -> [[Char]]
forall a. [a] -> [a]
reverse [[Char]]
outputs))
  ([Char], a) -> REPL ([Char], a)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
output, a
result)

-- | Apply control character semantics to the result of the logger
interpretControls :: String -> String
interpretControls :: ShowS
interpretControls (Char
'\b' : [Char]
xs) = ShowS
interpretControls [Char]
xs
interpretControls (Char
_ : Char
'\b' : [Char]
xs) = ShowS
interpretControls [Char]
xs
interpretControls (Char
x : [Char]
xs) = Char
x Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
interpretControls [Char]
xs
interpretControls [] = []

-- | The result of running a docstring as attached to a definition
data DocstringResult = DocstringResult
  { DocstringResult -> DocFor
drName   :: T.DocFor -- ^ The associated definition of the docstring
  , DocstringResult -> [[SubcommandResult]]
drFences :: [[SubcommandResult]] -- ^ list of fences in this definition's docstring
  }

-- | Check all the code blocks in a given docstring.
checkDocItem :: T.DocItem -> REPL DocstringResult
checkDocItem :: DocItem -> REPL DocstringResult
checkDocItem DocItem
item =
 do [[SubcommandResult]]
xs <- case (Text -> [[Text]]) -> [Text] -> [[[Text]]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Text -> [[Text]]
extractCodeBlocks (DocItem -> [Text]
T.docText DocItem
item) of
            [] -> [[SubcommandResult]] -> REPL [[SubcommandResult]]
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] -- optimization
            [[[Text]]]
bs ->
              REPL (Maybe (ImpName Name))
-> (Maybe (ImpName Name) -> REPL ())
-> (Maybe (ImpName Name) -> REPL [[SubcommandResult]])
-> REPL [[SubcommandResult]]
forall (m :: * -> *) a c b.
(HasCallStack, MonadMask m) =>
m a -> (a -> m c) -> (a -> m b) -> m b
Ex.bracket
                (ModuleCmd (Maybe (ImpName Name)) -> REPL (Maybe (ImpName Name))
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleInput IO
-> ModuleM (Maybe (ImpName Name))
-> IO
     (Either ModuleError (Maybe (ImpName Name), ModuleEnv),
      [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
`M.runModuleM` (ModuleM (Maybe (ImpName Name))
M.getFocusedModule ModuleM (Maybe (ImpName Name))
-> ModuleM () -> ModuleM (Maybe (ImpName Name))
forall a b. ModuleT IO a -> ModuleT IO b -> ModuleT IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ImpName Name -> ModuleM ()
M.setFocusedModule (DocItem -> ImpName Name
T.docModContext DocItem
item))))
                (\Maybe (ImpName Name)
mb -> ModuleCmd () -> REPL ()
forall a. ModuleCmd a -> REPL a
liftModuleCmd (ModuleInput IO
-> ModuleM ()
-> IO (Either ModuleError ((), ModuleEnv), [ModuleWarning])
forall a.
ModuleInput IO
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
`M.runModuleM` Maybe (ImpName Name) -> ModuleM ()
M.setMaybeFocusedModule Maybe (ImpName Name)
mb))
                (\Maybe (ImpName Name)
_ -> ([Text] -> REPL [SubcommandResult])
-> [[Text]] -> REPL [[SubcommandResult]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse [Text] -> REPL [SubcommandResult]
checkBlock ([[[Text]]] -> [[Text]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Text]]]
bs))
    DocstringResult -> REPL DocstringResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DocstringResult
      { drName :: DocFor
drName = DocItem -> DocFor
T.docFor DocItem
item
      , drFences :: [[SubcommandResult]]
drFences = [[SubcommandResult]]
xs
      }

-- | Check all of the docstrings in the given module.
--
-- The outer list elements correspond to the code blocks from the
-- docstrings in file order. Each inner list corresponds to the
-- REPL commands inside each of the docstrings.
checkDocStrings :: M.LoadedModule -> REPL [DocstringResult]
checkDocStrings :: LoadedModule -> REPL [DocstringResult]
checkDocStrings LoadedModule
m = do
  let dat :: Module
dat = LoadedModuleData -> Module
M.lmdModule (LoadedModule -> LoadedModuleData
forall a. LoadedModuleG a -> a
M.lmData LoadedModule
m)
  let ds :: [DocItem]
ds = Map Name (ImpName Name) -> Module -> [DocItem]
T.gatherModuleDocstrings (Iface -> Map Name (ImpName Name)
M.ifaceNameToModuleMap (LoadedModule -> Iface
M.lmInterface LoadedModule
m)) Module
dat
  (DocItem -> REPL DocstringResult)
-> [DocItem] -> REPL [DocstringResult]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DocItem -> REPL DocstringResult
checkDocItem [DocItem]
ds

-- | Evaluate all the docstrings in the specified module.
--
-- This command succeeds when:
-- * the module can be found
-- * the docstrings can be parsed for code blocks
-- * all of the commands in the docstrings succeed
checkDocStringsCmd ::
  String {- ^ module name -} ->
  REPL CommandResult
checkDocStringsCmd :: [Char] -> REPL CommandResult
checkDocStringsCmd [Char]
input
  | [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
input = do
    Maybe LoadedModule
mb <- REPL (Maybe LoadedModule)
getLoadedMod
    case LoadedModule -> Maybe ModName
lName (LoadedModule -> Maybe ModName)
-> Maybe LoadedModule -> Maybe ModName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe LoadedModule
mb of
      Maybe ModName
Nothing -> do
        [Char] -> REPL ()
rPutStrLn [Char]
"No current module"
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
      Just ModName
mn -> ModName -> REPL CommandResult
checkModName ModName
mn
  | Bool
otherwise =
    case [Char] -> Maybe ModName
parseModName [Char]
input of
      Maybe ModName
Nothing -> do
        [Char] -> REPL ()
rPutStrLn [Char]
"Invalid module name"
        CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }
      Just ModName
mn -> ModName -> REPL CommandResult
checkModName ModName
mn

  where

    countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int)
    countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int)
countOutcomes = ((Int, Int, Int) -> [SubcommandResult] -> (Int, Int, Int))
-> (Int, Int, Int) -> [[SubcommandResult]] -> (Int, Int, Int)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Int, Int) -> [SubcommandResult] -> (Int, Int, Int)
forall {b} {a} {c}.
(Num b, Num a, Num c) =>
(a, b, c) -> [SubcommandResult] -> (a, b, c)
countOutcomes1 (Int
0, Int
0, Int
0)
      where
        countOutcomes1 :: (a, b, c) -> [SubcommandResult] -> (a, b, c)
countOutcomes1 (a
successes, b
nofences, c
failures) []
          = (a
successes, b
nofences b -> b -> b
forall a. Num a => a -> a -> a
+ b
1, c
failures)
        countOutcomes1 (a, b, c)
acc [SubcommandResult]
result = ((a, b, c) -> SubcommandResult -> (a, b, c))
-> (a, b, c) -> [SubcommandResult] -> (a, b, c)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (a, b, c) -> SubcommandResult -> (a, b, c)
forall {a} {c} {b}.
(Num a, Num c) =>
(a, b, c) -> SubcommandResult -> (a, b, c)
countOutcomes2 (a, b, c)
acc [SubcommandResult]
result

        countOutcomes2 :: (a, b, c) -> SubcommandResult -> (a, b, c)
countOutcomes2 (a
successes, b
nofences, c
failures) SubcommandResult
result
          | CommandResult -> Bool
crSuccess (SubcommandResult -> CommandResult
srResult SubcommandResult
result) = (a
successes a -> a -> a
forall a. Num a => a -> a -> a
+ a
1, b
nofences, c
failures)
          | Bool
otherwise = (a
successes, b
nofences, c
failures c -> c -> c
forall a. Num a => a -> a -> a
+ c
1)


    checkModName :: P.ModName -> REPL CommandResult
    checkModName :: ModName -> REPL CommandResult
checkModName ModName
mn = do
        Maybe LoadedModule
mb <- ModName -> ModuleEnv -> Maybe LoadedModule
M.lookupModule ModName
mn (ModuleEnv -> Maybe LoadedModule)
-> REPL ModuleEnv -> REPL (Maybe LoadedModule)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModuleEnv
getModuleEnv
        case Maybe LoadedModule
mb of
          Maybe LoadedModule
Nothing -> do
            [Char] -> REPL ()
rPutStrLn ([Char]
"Module " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
input [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" is not loaded")
            CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = False }

          Just LoadedModule
fe
            | Module -> Bool
forall mname. ModuleG mname -> Bool
T.isParametrizedModule (LoadedModuleData -> Module
M.lmdModule (LoadedModule -> LoadedModuleData
forall a. LoadedModuleG a -> a
M.lmData LoadedModule
fe)) -> do
              [Char] -> REPL ()
rPutStrLn [Char]
"Skipping docstrings on parameterized module"
              CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult

            | Bool
otherwise -> do
              [DocstringResult]
results <- LoadedModule -> REPL [DocstringResult]
checkDocStrings LoadedModule
fe
              let (Int
successes, Int
nofences, Int
failures) = [[SubcommandResult]] -> (Int, Int, Int)
countOutcomes [[[SubcommandResult]] -> [SubcommandResult]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (DocstringResult -> [[SubcommandResult]]
drFences DocstringResult
r) | DocstringResult
r <- [DocstringResult]
results]

              [DocstringResult] -> (DocstringResult -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [DocstringResult]
results ((DocstringResult -> REPL ()) -> REPL ())
-> (DocstringResult -> REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \DocstringResult
dr ->
                Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[SubcommandResult]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DocstringResult -> [[SubcommandResult]]
drFences DocstringResult
dr)) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
                 do [Char] -> REPL ()
rPutStrLn [Char]
""
                    [Char] -> REPL ()
rPutStrLn ([Char]
"\nChecking " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (DocFor -> Doc
forall a. PP a => a -> Doc
pp (DocstringResult -> DocFor
drName DocstringResult
dr)))
                    [[SubcommandResult]] -> ([SubcommandResult] -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (DocstringResult -> [[SubcommandResult]]
drFences DocstringResult
dr) (([SubcommandResult] -> REPL ()) -> REPL ())
-> ([SubcommandResult] -> REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \[SubcommandResult]
fence ->
                      [SubcommandResult] -> (SubcommandResult -> REPL ()) -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SubcommandResult]
fence ((SubcommandResult -> REPL ()) -> REPL ())
-> (SubcommandResult -> REPL ()) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \SubcommandResult
line -> do
                        [Char] -> REPL ()
rPutStrLn [Char]
""
                        [Char] -> REPL ()
rPutStrLn (Text -> [Char]
T.unpack (SubcommandResult -> Text
srInput SubcommandResult
line))
                        [Char] -> REPL ()
rPutStr (SubcommandResult -> [Char]
srLog SubcommandResult
line)

              [Char] -> REPL ()
rPutStrLn [Char]
""
              [Char] -> REPL ()
rPutStrLn ([Char]
"Successes: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
successes [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", No fences: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
nofences [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", Failures: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
failures)

              CommandResult -> REPL CommandResult
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandResult
emptyCommandResult { crSuccess = failures == 0 }