diff --git a/cryptol-remote-api/CHANGELOG.md b/cryptol-remote-api/CHANGELOG.md deleted file mode 100644 index 0a67cda..0000000 --- a/cryptol-remote-api/CHANGELOG.md +++ /dev/null @@ -1,5 +0,0 @@ -# Revision history for cryptol-server - -## 0.1.0.0 -- YYYY-mm-dd - -* First version. Released on an unsuspecting world. diff --git a/cryptol-remote-api/LICENSE b/cryptol-remote-api/LICENSE deleted file mode 100644 index 76ed25f..0000000 --- a/cryptol-remote-api/LICENSE +++ /dev/null @@ -1,29 +0,0 @@ -BSD 3-Clause License - -Copyright (c) 2019, Galois, Inc. -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -1. Redistributions of source code must retain the above copyright notice, this - list of conditions and the following disclaimer. - -2. Redistributions in binary form must reproduce the above copyright notice, - this list of conditions and the following disclaimer in the documentation - and/or other materials provided with the distribution. - -3. Neither the name of the copyright holder nor the names of its - contributors may be used to endorse or promote products derived from - this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" -AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR -SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER -CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, -OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/cryptol-remote-api/Setup.hs b/cryptol-remote-api/Setup.hs deleted file mode 100644 index 9a994af..0000000 --- a/cryptol-remote-api/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal deleted file mode 100644 index 97be02d..0000000 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ /dev/null @@ -1,84 +0,0 @@ -cabal-version: 2.4 -name: cryptol-remote-api -version: 0.1.0.0 -license: BSD-3-Clause -license-file: LICENSE -author: David Thrane Christiansen -maintainer: dtc@galois.com -category: Language -extra-source-files: CHANGELOG.md -data-files: test-scripts/**/*.py - test-scripts/**/*.cry - -common warnings - ghc-options: - -Weverything - -Wno-missing-exported-signatures - -Wno-missing-import-lists - -Wno-missed-specialisations - -Wno-all-missed-specialisations - -Wno-unsafe - -Wno-safe - -Wno-missing-local-signatures - -Wno-monomorphism-restriction - -Wno-implicit-prelude - -common deps - build-depends: - base >=4.11.1.0 && <4.15, - argo, - aeson >= 1.4.2, - base64-bytestring >= 1.0, - bytestring ^>= 0.10.8, - containers >=0.5.11 && <0.7, - cryptol >= 2.9.0, - directory ^>= 1.3.1, - filepath ^>= 1.4, - lens >= 4.17 && < 4.20, - scientific ^>= 0.3, - text ^>= 1.2.3, - unordered-containers ^>= 0.2, - vector ^>= 0.12, - - default-language: Haskell2010 - -library - import: deps, warnings - hs-source-dirs: src - - exposed-modules: - CryptolServer - CryptolServer.Call - CryptolServer.ChangeDir - CryptolServer.Data.Expression - CryptolServer.Data.Type - CryptolServer.EvalExpr - CryptolServer.Exceptions - CryptolServer.FocusedModule - CryptolServer.LoadModule - CryptolServer.Names - CryptolServer.Sat - CryptolServer.TypeCheck - -executable cryptol-remote-api - import: deps, warnings - main-is: Main.hs - hs-source-dirs: cryptol-remote-api - - build-depends: - cryptol-remote-api, - sbv < 8.8 - -test-suite test-cryptol-remote-api - import: deps, warnings - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Test.hs - other-modules: Paths_cryptol_remote_api - build-depends: - argo-python, - cryptol-remote-api, - quickcheck-instances ^>= 0.3.19, - tasty >= 1.2.1, - tasty-quickcheck ^>= 0.10, - tasty-script-exitcode diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs deleted file mode 100644 index 5b1332e..0000000 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PartialTypeSignatures #-} -{-# LANGUAGE ScopedTypeVariables #-} -module Main (main) where - -import qualified Data.Aeson as JSON -import Data.Text (Text) -import System.Environment (lookupEnv) -import System.FilePath (splitSearchPath) - -import Argo -import Argo.DefaultMain - - -import CryptolServer -import CryptolServer.Call -import CryptolServer.ChangeDir -import CryptolServer.EvalExpr -import CryptolServer.FocusedModule -import CryptolServer.LoadModule -import CryptolServer.Names -import CryptolServer.Sat -import CryptolServer.TypeCheck - -main :: IO () -main = - do paths <- getSearchPaths - initSt <- setSearchPath paths <$> initialState - theApp <- mkApp (const (pure initSt)) cryptolMethods - defaultMain description theApp - -description :: String -description = - "An RPC server for Cryptol that supports type checking and evaluation of Cryptol code." - -getSearchPaths :: IO [FilePath] -getSearchPaths = - maybe [] splitSearchPath <$> lookupEnv "CRYPTOLPATH" - -cryptolMethods :: [(Text, MethodType, JSON.Value -> Method ServerState JSON.Value)] -cryptolMethods = - [ ("change directory", Command, method cd) - , ("load module", Command, method loadModule) - , ("load file", Command, method loadFile) - , ("focused module", Query, method focusedModule) - , ("evaluate expression", Query, method evalExpression) - , ("call", Query, method call) - , ("visible names", Query, method visibleNames) - , ("check type", Query, method checkType) - , ("satisfy", Query, method sat) - ] diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs deleted file mode 100644 index 26be855..0000000 --- a/cryptol-remote-api/src/CryptolServer.hs +++ /dev/null @@ -1,80 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer (module CryptolServer) where - -import Control.Lens -import Control.Monad.IO.Class - -import Cryptol.Eval.Monad (EvalOpts(..), PPOpts(..), PPFloatFormat(..), PPFloatExp(..)) -import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv) -import Cryptol.ModuleSystem.Env - (getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules, - initialModuleEnv, meSearchPath, ModulePath(..)) -import Cryptol.ModuleSystem.Fingerprint -import Cryptol.Parser.AST (ModName) -import Cryptol.Utils.Logger (quietLogger) - -import Argo -import CryptolServer.Exceptions - -runModuleCmd :: ModuleCmd a -> Method ServerState a -runModuleCmd cmd = - do s <- getState - reader <- getFileReader - out <- liftIO $ cmd (theEvalOpts, reader, view moduleEnv s) - case out of - (Left x, warns) -> - raise (cryptolError x warns) - (Right (x, newEnv), _warns) -> - -- TODO: What to do about warnings when a command completes - -- successfully? - do setState (set moduleEnv newEnv s) - return x - -data LoadedModule = LoadedModule - { _loadedName :: Maybe ModName -- ^ Working on this module. - , _loadedPath :: FilePath -- ^ Working on this file. - } - -loadedName :: Lens' LoadedModule (Maybe ModName) -loadedName = lens _loadedName (\v n -> v { _loadedName = n }) - -loadedPath :: Lens' LoadedModule FilePath -loadedPath = lens _loadedPath (\v n -> v { _loadedPath = n }) - - -data ServerState = - ServerState { _loadedModule :: Maybe LoadedModule - , _moduleEnv :: ModuleEnv - } - -loadedModule :: Lens' ServerState (Maybe LoadedModule) -loadedModule = lens _loadedModule (\v n -> v { _loadedModule = n }) - -moduleEnv :: Lens' ServerState ModuleEnv -moduleEnv = lens _moduleEnv (\v n -> v { _moduleEnv = n }) - -initialState :: IO ServerState -initialState = ServerState Nothing <$> initialModuleEnv - -setSearchPath :: [FilePath] -> ServerState -> ServerState -setSearchPath paths = - over moduleEnv $ \me -> me { meSearchPath = paths ++ meSearchPath me } - -theEvalOpts :: EvalOpts -theEvalOpts = EvalOpts quietLogger (PPOpts False 10 25 10 (FloatFree AutoExponent)) - --- | Check that all of the modules loaded in the Cryptol environment --- currently have fingerprints that match those when they were loaded. -validateServerState :: ServerState -> IO Bool -validateServerState = - foldr check (return True) . getLoadedModules . meLoadedModules . view moduleEnv - where - check lm continue = - case lmFilePath lm of - InMem{} -> continue - InFile file -> - do fp <- fingerprintFile file - if fp == Just (lmFingerprint lm) - then continue - else return False diff --git a/cryptol-remote-api/src/CryptolServer/Call.hs b/cryptol-remote-api/src/CryptolServer/Call.hs deleted file mode 100644 index db04659..0000000 --- a/cryptol-remote-api/src/CryptolServer/Call.hs +++ /dev/null @@ -1,90 +0,0 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE ViewPatterns #-} -module CryptolServer.Call - ( Expression(..) - , Encoding(..) - , LetBinding(..) - , call - , CallParams(..) - ) where - -import Control.Lens hiding ((.=)) -import Control.Monad (unless) -import Control.Monad.IO.Class -import Data.Aeson as JSON hiding (Encoding, Value, decode) -import qualified Data.Aeson as JSON -import qualified Data.Set as Set -import Data.Text (Text) - -import Cryptol.IR.FreeVars (freeVars, tyDeps, valDeps) -import Cryptol.ModuleSystem (checkExpr, evalExpr, getPrimMap, meLoadedModules) -import Cryptol.ModuleSystem.Env (isLoadedParamMod, meSolverConfig) -import Cryptol.ModuleSystem.Name (NameInfo(Declared), nameInfo) -import Cryptol.Parser.AST (Expr(..), PName(..)) -import Cryptol.TypeCheck.AST (sType) -import Cryptol.TypeCheck.Solve (defaultReplExpr) -import Cryptol.TypeCheck.Subst (apSubst, listParamSubst) -import Cryptol.Utils.Ident -import Cryptol.Utils.PP (pretty) -import qualified Cryptol.TypeCheck.Solver.SMT as SMT - -import Argo - -import CryptolServer -import CryptolServer.Exceptions -import CryptolServer.Data.Expression -import CryptolServer.Data.Type - -call :: CallParams -> Method ServerState JSON.Value -call (CallParams fun rawArgs) = - do args <- traverse getExpr rawArgs - let appExpr = mkEApp (EVar (UnQual (mkIdent fun))) args - (_expr, ty, schema) <- runModuleCmd (checkExpr appExpr) - evalAllowed ty - evalAllowed schema - me <- view moduleEnv <$> getState - let cfg = meSolverConfig me - perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema) - case perhapsDef of - Nothing -> error "TODO" -- TODO: What should happen here? - Just (tys, checked) -> - do noDefaults tys - let su = listParamSubst tys - let theType = apSubst su (sType schema) - res <- runModuleCmd (evalExpr checked) - prims <- runModuleCmd getPrimMap - val <- observe $ readBack prims theType res - return (JSON.object [ "value" .= val - , "type string" .= pretty theType - , "type" .= JSONType mempty theType - ]) - where - noDefaults [] = return () - noDefaults xs@(_:_) = - raise (unwantedDefaults xs) - - evalAllowed x = - do me <- view moduleEnv <$> getState - let ds = freeVars x - badVals = foldr badName Set.empty (valDeps ds) - bad = foldr badName badVals (tyDeps ds) - badName nm bs = - case nameInfo nm of - Declared m _ - | isLoadedParamMod m (meLoadedModules me) -> Set.insert nm bs - _ -> bs - unless (Set.null bad) $ - raise (evalInParamMod (Set.toList bad)) - - -data CallParams - = CallParams Text [Expression] - -instance FromJSON CallParams where - parseJSON = - withObject "params for \"call\"" $ - \o -> CallParams <$> o .: "function" <*> o .: "arguments" diff --git a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs b/cryptol-remote-api/src/CryptolServer/ChangeDir.hs deleted file mode 100644 index b891d3b..0000000 --- a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs +++ /dev/null @@ -1,25 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.ChangeDir (cd, ChangeDirectoryParams(..)) where - -import Control.Monad.IO.Class -import Data.Aeson as JSON -import System.Directory - -import CryptolServer -import CryptolServer.Exceptions -import Argo - -cd :: ChangeDirectoryParams -> Method ServerState () -cd (ChangeDirectoryParams newDir) = - do exists <- liftIO $ doesDirectoryExist newDir - if exists - then liftIO $ setCurrentDirectory newDir - else raise (dirNotFound newDir) - -data ChangeDirectoryParams - = ChangeDirectoryParams FilePath - -instance FromJSON ChangeDirectoryParams where - parseJSON = - withObject "params for \"change directory\"" $ - \o -> ChangeDirectoryParams <$> o .: "directory" diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs deleted file mode 100644 index 0a467be..0000000 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ /dev/null @@ -1,373 +0,0 @@ -{-# OPTIONS_GHC -fno-warn-type-defaults #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE ViewPatterns #-} -module CryptolServer.Data.Expression - ( module CryptolServer.Data.Expression - ) where - -import Control.Applicative -import Control.Exception (throwIO) -import Control.Monad.IO.Class -import Data.Aeson as JSON hiding (Encoding, Value, decode) -import qualified Data.ByteString as BS -import qualified Data.ByteString.Base64 as Base64 -import Data.HashMap.Strict (HashMap) -import qualified Data.HashMap.Strict as HM -import Data.List.NonEmpty (NonEmpty(..)) -import qualified Data.Map as Map -import qualified Data.Scientific as Sc -import Data.Text (Text, pack) -import qualified Data.Text as T -import Data.Traversable -import qualified Data.Vector as V -import Data.Text.Encoding (encodeUtf8) -import Numeric (showHex) - -import Cryptol.Eval (evalSel) -import Cryptol.Eval.Monad -import Cryptol.Eval.Concrete (primTable) -import Cryptol.Eval.Concrete.Value hiding (Concrete) -import qualified Cryptol.Eval.Concrete.Value as C -import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap) -import Cryptol.Parser -import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Type(..), PName(..), Literal(..), NumInfo(..)) -import Cryptol.Parser.Position (Located(..), emptyRange) -import Cryptol.Parser.Selector --- import Cryptol.Prims.Syntax -import Cryptol.TypeCheck.AST (PrimMap) -import Cryptol.TypeCheck.SimpType (tRebuild) -import qualified Cryptol.TypeCheck.Type as TC -import Cryptol.Utils.Ident -import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields) - - -import Argo -import CryptolServer -import CryptolServer.Exceptions - -data Encoding = Base64 | Hex - deriving (Eq, Show, Ord) - -instance JSON.FromJSON Encoding where - parseJSON = - withText "encoding" $ - \case - "hex" -> pure Hex - "base64" -> pure Base64 - _ -> empty - -data LetBinding = - LetBinding - { argDefName :: !Text - , argDefVal :: !Expression - } - deriving (Eq, Ord, Show) - -instance JSON.FromJSON LetBinding where - parseJSON = - withObject "let binding" $ \o -> - LetBinding <$> o .: "name" <*> o .: "definition" - -instance JSON.ToJSON LetBinding where - toJSON (LetBinding x def) = - object [ "name" .= x - , "definition" .= def - ] - -data Expression = - Bit !Bool - | Unit - | Num !Encoding !Text !Integer -- ^ data and bitwidth - | Record !(HashMap Text Expression) - | Sequence ![Expression] - | Tuple ![Expression] - | Integer !Integer - | IntegerModulo !Integer !Integer -- ^ value, modulus - | Concrete !Text - | Let ![LetBinding] !Expression - | Application !Expression !(NonEmpty Expression) - deriving (Eq, Ord, Show) - -data ExpressionTag = - TagNum | TagRecord | TagSequence | TagTuple | TagUnit | TagLet | TagApp | TagIntMod - -instance JSON.FromJSON ExpressionTag where - parseJSON = - withText "tag" $ - \case - "bits" -> pure TagNum - "unit" -> pure TagUnit - "record" -> pure TagRecord - "sequence" -> pure TagSequence - "tuple" -> pure TagTuple - "let" -> pure TagLet - "call" -> pure TagApp - "integer modulo" -> pure TagIntMod - _ -> empty - -instance JSON.ToJSON ExpressionTag where - toJSON TagNum = "bits" - toJSON TagRecord = "record" - toJSON TagSequence = "sequence" - toJSON TagTuple = "tuple" - toJSON TagUnit = "unit" - toJSON TagLet = "let" - toJSON TagApp = "call" - toJSON TagIntMod = "integer modulo" - -instance JSON.FromJSON Expression where - parseJSON v = bool v <|> integer v <|> concrete v <|> obj v - where - bool = - withBool "boolean" $ pure . Bit - integer = - -- Note: this means that we should not expose this API to the - -- public, but only to systems that will validate input - -- integers. Otherwise, they can use this to allocate a - -- gigantic integer that fills up all memory. - withScientific "integer" $ \s -> - case Sc.floatingOrInteger s of - Left _fl -> empty - Right i -> pure (Integer i) - concrete = - withText "concrete syntax" $ pure . Concrete - - obj = - withObject "argument" $ - \o -> o .: "expression" >>= - \case - TagUnit -> pure Unit - TagNum -> - do enc <- o .: "encoding" - Num enc <$> o .: "data" <*> o .: "width" - TagRecord -> - do fields <- o .: "data" - flip (withObject "record data") fields $ - \fs -> Record <$> traverse parseJSON fs - TagSequence -> - do contents <- o .: "data" - flip (withArray "sequence") contents $ - \s -> Sequence . V.toList <$> traverse parseJSON s - TagTuple -> - do contents <- o .: "data" - flip (withArray "tuple") contents $ - \s -> Tuple . V.toList <$> traverse parseJSON s - TagLet -> - Let <$> o .: "binders" <*> o .: "body" - TagApp -> - Application <$> o .: "function" <*> o .: "arguments" - TagIntMod -> - IntegerModulo <$> o .: "integer" <*> o .: "modulus" - -instance ToJSON Encoding where - toJSON Hex = String "hex" - toJSON Base64 = String "base64" - -instance JSON.ToJSON Expression where - toJSON Unit = object [ "expression" .= TagUnit ] - toJSON (Bit b) = JSON.Bool b - toJSON (Integer i) = JSON.Number (fromInteger i) - toJSON (IntegerModulo i n) = - object [ "expression" .= TagIntMod - , "integer" .= JSON.Number (fromInteger i) - , "modulus" .= JSON.Number (fromInteger n) - ] - toJSON (Concrete expr) = toJSON expr - toJSON (Num enc dat w) = - object [ "expression" .= TagNum - , "data" .= String dat - , "encoding" .= enc - , "width" .= w - ] - toJSON (Record fields) = - object [ "expression" .= TagRecord - , "data" .= object [ fieldName .= toJSON val - | (fieldName, val) <- HM.toList fields - ] - ] - toJSON (Sequence elts) = - object [ "expression" .= TagSequence - , "data" .= Array (V.fromList (map toJSON elts)) - ] - toJSON (Tuple projs) = - object [ "expression" .= TagTuple - , "data" .= Array (V.fromList (map toJSON projs)) - ] - toJSON (Let binds body) = - object [ "expression" .= TagLet - , "binders" .= Array (V.fromList (map toJSON binds)) - , "body" .= toJSON body - ] - toJSON (Application fun args) = - object [ "expression" .= TagApp - , "function" .= fun - , "arguments" .= args - ] - - -decode :: Encoding -> Text -> Method s Integer -decode Base64 txt = - let bytes = encodeUtf8 txt - in - case Base64.decode bytes of - Left err -> - raise (invalidBase64 bytes err) - Right decoded -> return $ bytesToInt decoded -decode Hex txt = - squish <$> traverse hexDigit (T.unpack txt) - where - squish = foldl (\acc i -> (acc * 16) + i) 0 - -hexDigit :: Num a => Char -> Method s a -hexDigit '0' = pure 0 -hexDigit '1' = pure 1 -hexDigit '2' = pure 2 -hexDigit '3' = pure 3 -hexDigit '4' = pure 4 -hexDigit '5' = pure 5 -hexDigit '6' = pure 6 -hexDigit '7' = pure 7 -hexDigit '8' = pure 8 -hexDigit '9' = pure 9 -hexDigit 'a' = pure 10 -hexDigit 'A' = pure 10 -hexDigit 'b' = pure 11 -hexDigit 'B' = pure 11 -hexDigit 'c' = pure 12 -hexDigit 'C' = pure 12 -hexDigit 'd' = pure 13 -hexDigit 'D' = pure 13 -hexDigit 'e' = pure 14 -hexDigit 'E' = pure 14 -hexDigit 'f' = pure 15 -hexDigit 'F' = pure 15 -hexDigit c = raise (invalidHex c) - - -getExpr :: Expression -> Method s (Expr PName) -getExpr Unit = - return $ - ETyped - (ETuple []) - (TTuple []) -getExpr (Bit b) = - return $ - ETyped - (EVar (UnQual (mkIdent $ if b then "True" else "False"))) - TBit -getExpr (Integer i) = - return $ - ETyped - (ELit (ECNum i (DecLit (pack (show i))))) - (TUser (UnQual (mkIdent "Integer")) []) -getExpr (IntegerModulo i n) = - return $ - ETyped - (ELit (ECNum i (DecLit (pack (show i))))) - (TUser (UnQual (mkIdent "Z")) [TNum n]) -getExpr (Num enc txt w) = - do d <- decode enc txt - return $ ETyped - (ELit (ECNum d (DecLit txt))) - (TSeq (TNum w) TBit) -getExpr (Record fields) = - fmap (ERecord . recordFromFields) $ for (HM.toList fields) $ - \(recName, spec) -> - (mkIdent recName,) . (emptyRange,) <$> getExpr spec -getExpr (Sequence elts) = - EList <$> traverse getExpr elts -getExpr (Tuple projs) = - ETuple <$> traverse getExpr projs -getExpr (Concrete syntax) = - case parseExpr syntax of - Left err -> - raise (cryptolParseErr syntax err) - Right e -> pure e -getExpr (Let binds body) = - EWhere <$> getExpr body <*> traverse mkBind binds - where - mkBind (LetBinding x rhs) = - DBind . - (\bindBody -> - Bind (fakeLoc (UnQual (mkIdent x))) [] bindBody Nothing False Nothing [] True Nothing) . - fakeLoc . - DExpr <$> - getExpr rhs - - fakeLoc = Located emptyRange -getExpr (Application fun (arg :| [])) = - EApp <$> getExpr fun <*> getExpr arg -getExpr (Application fun (arg1 :| (arg : args))) = - getExpr (Application (Application fun (arg1 :| [])) (arg :| args)) - --- TODO add tests that this is big-endian --- | Interpret a ByteString as an Integer -bytesToInt :: BS.ByteString -> Integer -bytesToInt bs = - BS.foldl' (\acc w -> (acc * 256) + toInteger w) 0 bs - -typeNum :: (Alternative f, Integral a) => TC.Type -> f a -typeNum (tRebuild -> (TC.TCon (TC.TC (TC.TCNum n)) [])) = - pure $ fromIntegral n -typeNum _ = empty - -readBack :: PrimMap -> TC.Type -> Value -> Eval Expression -readBack prims ty val = - let tbl = primTable theEvalOpts in - let ?evalPrim = \i -> Map.lookup i tbl in - case TC.tNoUser ty of - TC.TRec tfs -> - Record . HM.fromList <$> - sequence [ do fv <- evalSel C.Concrete val (RecordSel f Nothing) - fa <- readBack prims t fv - return (identText f, fa) - | (f, t) <- canonicalFields tfs - ] - TC.TCon (TC.TC (TC.TCTuple _)) [] -> - pure Unit - TC.TCon (TC.TC (TC.TCTuple _)) ts -> - Tuple <$> sequence [ do v <- evalSel C.Concrete val (TupleSel n Nothing) - a <- readBack prims t v - return a - | (n, t) <- zip [0..] ts - ] - TC.TCon (TC.TC TC.TCBit) [] -> - case val of - VBit b -> pure (Bit b) - _ -> mismatchPanic - TC.TCon (TC.TC TC.TCInteger) [] -> - case val of - VInteger i -> pure (Integer i) - _ -> mismatchPanic - TC.TCon (TC.TC TC.TCIntMod) [typeNum -> Just n] -> - case val of - VInteger i -> pure (IntegerModulo i n) - _ -> mismatchPanic - TC.TCon (TC.TC TC.TCSeq) [TC.tNoUser -> len, TC.tNoUser -> contents] - | len == TC.tZero -> - return Unit - | contents == TC.TCon (TC.TC TC.TCBit) [] - , VWord _ wv <- val -> - do BV w v <- wv >>= asWordVal C.Concrete - return $ Num Hex (T.pack $ showHex v "") w - | TC.TCon (TC.TC (TC.TCNum k)) [] <- len - , VSeq _l (enumerateSeqMap k -> vs) <- val -> - Sequence <$> mapM (>>= readBack prims contents) vs - other -> liftIO $ throwIO (invalidType other) - where - mismatchPanic = - error $ "Internal error: readBack: value '" <> - show val <> - "' didn't match type '" <> - show ty <> - "'" - - -observe :: Eval a -> Method ServerState a -observe e = liftIO (runEval e) - -mkEApp :: Expr PName -> [Expr PName] -> Expr PName -mkEApp f args = foldl EApp f args diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs deleted file mode 100644 index c7ea626..0000000 --- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs +++ /dev/null @@ -1,206 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.Data.Type - ( JSONSchema(..) - , JSONType(..) - ) where - -import qualified Data.Aeson as JSON -import Data.Aeson ((.=)) -import qualified Data.Text as T - -import Cryptol.Parser.Selector (ppSelector) -import Cryptol.TypeCheck.PP (NameMap, emptyNameMap, ppWithNames) -import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..), TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf) -import Cryptol.Utils.PP (pp) -import Cryptol.Utils.RecordMap (canonicalFields) - - -newtype JSONSchema = JSONSchema Schema - -data JSONType = JSONType NameMap Type - -newtype JSONKind = JSONKind Kind - -instance JSON.ToJSON JSONSchema where - toJSON (JSONSchema (Forall vars props ty)) = - let ns = addTNames vars emptyNameMap - in JSON.object [ "forall" .= - [JSON.object - [ "name" .= show (ppWithNames ns v) - , "kind" .= JSONKind (kindOf v) - ] - | v@(TParam _uniq _k _flav _info) <- vars - ] - , "propositions" .= map (JSON.toJSON . JSONType ns) props - , "type" .= JSONType ns ty - ] - -instance JSON.ToJSON JSONKind where - toJSON (JSONKind k) = convert k - where - convert KType = "Type" - convert KNum = "Num" - convert KProp = "Prop" - convert (k1 :-> k2) = - JSON.object [ "kind" .= T.pack "arrow" - , "from" .= convert k1 - , "to" .= convert k2 - ] - -instance JSON.ToJSON JSONType where - toJSON (JSONType ns t) = convert t - where - convert (TCon (TError _ _) _) = - -- TODO: figure out what to do in this situation - error "JSON conversion of errors is not yet supported" - convert (TCon (TC tc) args) = - JSON.object $ - case (tc, args) of - (TCNum n, []) -> - [ "type" .= T.pack "number" , "value" .= n ] - (TCInf, []) -> ["type" .= T.pack "inf"] - (TCBit, []) -> ["type" .= T.pack "Bit"] - (TCInteger, []) -> ["type" .= T.pack "Integer"] - (TCIntMod, [n]) -> [ "type" .= T.pack "Z" - , "modulus" .= JSONType ns n - ] - (TCSeq, [t1, TCon (TC TCBit) []]) -> - [ "type" .= T.pack "bitvector" - , "width" .= JSONType ns t1 - ] - (TCSeq, [t1, t2]) -> - [ "type" .= T.pack "sequence" - , "length" .= JSONType ns t1 - , "contents" .= JSONType ns t2 - ] - (TCFun, [t1, t2]) -> - [ "type" .= T.pack "function" - , "domain" .= JSONType ns t1 - , "range" .= JSONType ns t2 - ] - (TCTuple _ , []) -> - [ "type" .= T.pack "unit" ] - (TCTuple _, fs) -> - [ "type" .= T.pack "tuple" - , "contents" .= map (JSONType ns) fs - ] - (TCRational, []) -> - [ "type" .= T.pack "Rational"] - (other, otherArgs) -> - [ "type" .= T.pack "unknown" - , "constructor" .= show other - , "arguments" .= show otherArgs - ] - convert (TCon (TF tf) args) = - JSON.object - [ "type" .= T.pack t' - , "arguments" .= map (JSONType ns) args - ] - where - t' = - case tf of - TCAdd -> "+" - TCSub -> "-" - TCMul -> "*" - TCDiv -> "/" - TCMod -> "%" - TCExp -> "^^" - TCWidth -> "width" - TCMin -> "min" - TCMax -> "max" - TCCeilDiv -> "/^" - TCCeilMod -> "%^" - TCLenFromThenTo -> "lengthFromThenTo" - convert (TCon (PC pc) args) = - JSON.object $ - case (pc, args) of - (PEqual, [t1, t2]) -> - [ "prop" .= T.pack "==" - , "left" .= JSONType ns t1 - , "right" .= JSONType ns t2 - ] - (PNeq, [t1, t2]) -> - [ "prop" .= T.pack "!=" - , "left" .= JSONType ns t1 - , "right" .= JSONType ns t2 - ] - (PGeq, [t1, t2]) -> - [ "prop" .= T.pack ">=" - , "greater" .= JSONType ns t1 - , "less" .= JSONType ns t2 - ] - (PFin, [t']) -> - [ "prop" .= T.pack "fin" - , "subject" .= JSONType ns t' - ] - (PHas x, [t1, t2]) -> - [ "prop" .= T.pack "has" - , "selector" .= show (ppSelector x) - , "type" .= JSONType ns t1 - , "is" .= JSONType ns t2 - ] - (PRing, [t']) -> - [ "prop" .= T.pack "Ring" - , "subject" .= JSONType ns t' - ] - (PField, [t']) -> - [ "prop" .= T.pack "Field" - , "subject" .= JSONType ns t' - ] - (PRound, [t']) -> - [ "prop" .= T.pack "Round" - , "subject" .= JSONType ns t' - ] - (PIntegral, [t']) -> - [ "prop" .= T.pack "Integral" - , "subject" .= JSONType ns t' - ] - (PCmp, [t']) -> - [ "prop" .= T.pack "Cmp" - , "subject" .= JSONType ns t' - ] - (PSignedCmp, [t']) -> - [ "prop" .= T.pack "SignedCmp" - , "subject" .= JSONType ns t' - ] - (PLiteral, [t1, t2]) -> - [ "prop" .= T.pack "Literal" - , "size" .= JSONType ns t1 - , "subject" .= JSONType ns t2 - ] - (PZero, [t']) -> - [ "prop" .= T.pack "Zero" - , "subject" .= JSONType ns t' - ] - (PLogic, [t']) -> - [ "prop" .= T.pack "Logic" - , "subject" .= JSONType ns t' - ] - (PTrue, []) -> - [ "prop" .= T.pack "True" - ] - (PAnd, [t1, t2]) -> - [ "prop" .= T.pack "And" - , "left" .= JSONType ns t1 - , "right" .= JSONType ns t2 - ] - (pc', args') -> - [ "prop" .= T.pack "unknown" - , "constructor" .= show pc' - , "arguments" .= show args' - ] - convert (TVar v) = - JSON.object - [ "type" .= T.pack "variable" - , "kind" .= JSONKind (kindOf v) - , "name" .= show (ppWithNames ns v) - ] - convert (TUser _n _args def) = convert def - convert (TRec fields) = - JSON.object - [ "type" .= T.pack "record" - , "fields" .= - JSON.object [ T.pack (show (pp f)) .= JSONType ns t' - | (f, t') <- canonicalFields fields - ] - ] diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs deleted file mode 100644 index 9523d1f..0000000 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.EvalExpr (evalExpression, EvalExprParams(..)) where - -import Control.Lens hiding ((.=)) -import Control.Monad.IO.Class -import Data.Aeson as JSON - - -import Cryptol.ModuleSystem (checkExpr, evalExpr, getPrimMap) -import Cryptol.ModuleSystem.Env (meSolverConfig) -import Cryptol.TypeCheck.AST (sType) -import Cryptol.TypeCheck.Solve (defaultReplExpr) -import Cryptol.TypeCheck.Subst (apSubst, listParamSubst) -import Cryptol.TypeCheck.Type (Schema(..)) -import qualified Cryptol.TypeCheck.Solver.SMT as SMT -import Cryptol.Utils.PP (pretty) - -import Argo -import CryptolServer -import CryptolServer.Data.Expression -import CryptolServer.Data.Type -import CryptolServer.Exceptions - -evalExpression :: EvalExprParams -> Method ServerState JSON.Value -evalExpression (EvalExprParams jsonExpr) = - do e <- getExpr jsonExpr - (_expr, ty, schema) <- runModuleCmd (checkExpr e) - -- TODO: see Cryptol REPL for how to check whether we - -- can actually evaluate things, which we can't do in - -- a parameterized module - me <- view moduleEnv <$> getState - let cfg = meSolverConfig me - perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema) - case perhapsDef of - Nothing -> - raise (evalPolyErr schema) - Just (tys, checked) -> - do -- TODO: warnDefaults here - let su = listParamSubst tys - let theType = apSubst su (sType schema) - res <- runModuleCmd (evalExpr checked) - prims <- runModuleCmd getPrimMap - val <- observe $ readBack prims theType res - return (JSON.object [ "value" .= val - , "type string" .= pretty theType - , "type" .= JSONSchema (Forall [] [] theType) - ]) - -newtype EvalExprParams = - EvalExprParams Expression - -instance JSON.FromJSON EvalExprParams where - parseJSON = - JSON.withObject "params for \"evaluate expression\"" $ - \o -> EvalExprParams <$> o .: "expression" diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs deleted file mode 100644 index 9d36476..0000000 --- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs +++ /dev/null @@ -1,209 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.Exceptions - ( dirNotFound - , invalidBase64 - , invalidHex - , invalidType - , unwantedDefaults - , evalInParamMod - , evalPolyErr - , proverError - , cryptolParseErr - , cryptolError - ) where - -import qualified Data.Aeson as JSON -import qualified Data.Text as Text -import qualified Data.Vector as Vector - -import Cryptol.ModuleSystem (ModuleError(..), ModuleWarning(..)) -import Cryptol.Utils.PP (pretty, PP) - -import Data.Aeson hiding (Encoding, Value, decode) -import Data.ByteString (ByteString) -import qualified Data.ByteString.Char8 as B8 -import Data.Text (Text) -import qualified Data.Text as T -import qualified Data.HashMap.Strict as HashMap - -import Cryptol.ModuleSystem.Name (Name) -import Cryptol.Parser -import qualified Cryptol.TypeCheck.Type as TC - -import Argo -import CryptolServer.Data.Type - -cryptolError :: ModuleError -> [ModuleWarning] -> JSONRPCException -cryptolError modErr warns = - makeJSONRPCException - errorNum - (Text.pack $ (pretty modErr) <> foldMap (\w -> "\n" <> pretty w) warns) - (Just . JSON.object $ errorData ++ [("warnings", moduleWarnings warns)]) - where - -- TODO: make sub-errors (parse, typecheck, etc.) into structured data so - -- that another client can parse them and make use of them (possible - -- locations noted below) - - (errorNum, errorData) = moduleError modErr - - moduleError err = case err of - ModuleNotFound src path -> - (20500, [ ("source", jsonPretty src) - , ("path", jsonList (map jsonString path)) - ]) - CantFindFile path -> - (20050, [ ("path", jsonString path) - ]) - BadUtf8 path ue -> - (20010, [ ("path", jsonShow path) - , ("error", jsonShow ue) - ]) - OtherIOError path exn -> - (20060, [ ("path", jsonString path) - , ("error", jsonShow exn) - ]) - ModuleParseError source message -> - (20540, [ ("source", jsonShow source) - , ("error", jsonShow message) - ]) - RecursiveModules mods -> - (20550, [ ("modules", jsonList (reverse (map jsonPretty mods))) - ]) - RenamerErrors src errs -> - -- TODO: structured error here - (20700, [ ("source", jsonPretty src) - , ("errors", jsonList (map jsonPretty errs)) - ]) - NoPatErrors src errs -> - -- TODO: structured error here - (20710, [ ("source", jsonPretty src) - , ("errors", jsonList (map jsonPretty errs)) - ]) - NoIncludeErrors src errs -> - -- TODO: structured error here - (20720, [ ("source", jsonPretty src) - , ("errors", jsonList (map jsonShow errs)) - ]) - TypeCheckingFailed src errs -> - -- TODO: structured error here - (20730, [ ("source", jsonPretty src) - , ("errors", jsonList (map jsonShow errs)) - ]) - ModuleNameMismatch expected found -> - (20600, [ ("expected", jsonPretty expected) - , ("found", jsonPretty found) - ]) - DuplicateModuleName name path1 path2 -> - (20610, [ ("name", jsonPretty name) - , ("paths", jsonList [jsonString path1, jsonString path2]) - ]) - ImportedParamModule x -> - (20630, [ ("module", jsonPretty x) - ]) - FailedToParameterizeModDefs x xs -> - (20640, [ ("module", jsonPretty x) - , ("parameters", jsonList (map (jsonString . pretty) xs)) - ]) - NotAParameterizedModule x -> - (20650, [ ("module", jsonPretty x) - ]) - OtherFailure x -> - (29999, [ ("error", jsonString x) - ]) - ErrorInFile x y -> - (n, ("path", jsonShow x) : e) - where (n, e) = moduleError y - - moduleWarnings :: [ModuleWarning] -> JSON.Value - moduleWarnings = - -- TODO: structured error here - jsonList . concatMap - (\w -> case w of - TypeCheckWarnings tcwarns -> - map (jsonPretty . snd) tcwarns - RenamerWarnings rnwarns -> - map jsonPretty rnwarns) - - -- Some little helpers for common ways of building JSON values in the above: - - jsonString :: String -> JSON.Value - jsonString = JSON.String . Text.pack - - jsonPretty :: PP a => a -> JSON.Value - jsonPretty = jsonString . pretty - - jsonShow :: Show a => a -> JSON.Value - jsonShow = jsonString . show - - jsonList :: [JSON.Value] -> JSON.Value - jsonList = JSON.Array . Vector.fromList - -dirNotFound :: FilePath -> JSONRPCException -dirNotFound dir = - makeJSONRPCException - 20051 (T.pack ("Directory doesn't exist: " <> dir)) - (Just (JSON.object ["path" .= dir])) - -invalidBase64 :: ByteString -> String -> JSONRPCException -invalidBase64 invalidData msg = - makeJSONRPCException - 20020 (T.pack msg) - (Just (JSON.object ["input" .= B8.unpack invalidData])) - -invalidHex :: Char -> JSONRPCException -invalidHex invalidData = - makeJSONRPCException - 20030 "Not a hex digit" - (Just (JSON.object ["input" .= T.singleton invalidData])) - -invalidType :: TC.Type -> JSONRPCException -invalidType ty = - makeJSONRPCException - 20040 "Can't convert Cryptol data from this type to JSON" - (Just (jsonTypeAndString ty)) - -unwantedDefaults :: [(TC.TParam, TC.Type)] -> JSONRPCException -unwantedDefaults defs = - makeJSONRPCException - 20210 "Execution would have required these defaults" - (Just (JSON.object ["defaults" .= - [ jsonTypeAndString ty <> HashMap.fromList ["parameter" .= pretty param] - | (param, ty) <- defs ] ])) - -evalInParamMod :: [Cryptol.ModuleSystem.Name.Name] -> JSONRPCException -evalInParamMod mods = - makeJSONRPCException - 20220 "Can't evaluate Cryptol in a parameterized module." - (Just (JSON.object ["modules" .= map pretty mods])) - -evalPolyErr :: - TC.Schema {- ^ the type that was too polymorphic -} -> - JSONRPCException -evalPolyErr schema = - makeJSONRPCException - 20200 "Can't evaluate at polymorphic type" - (Just (JSON.object [ "type" .= JSONSchema schema - , "type string" .= pretty schema ])) - -proverError :: String -> JSONRPCException -proverError msg = - makeJSONRPCException - 20230 "Prover error" - (Just (JSON.object ["error" .= msg])) - -cryptolParseErr :: - Text {- ^ the input that couldn't be parsed -} -> - ParseError {- ^ the parse error from Cryptol -} -> - JSONRPCException -cryptolParseErr expr err = - makeJSONRPCException - 20000 "Cryptol parse error" - (Just $ JSON.object ["input" .= expr, "error" .= show err]) - --- The standard way of presenting a type: a structured type, plus a --- human-readable string -jsonTypeAndString :: TC.Type -> JSON.Object -jsonTypeAndString ty = - HashMap.fromList - [ "type" .= JSONSchema (TC.Forall [] [] ty) - , "type string" .= pretty ty ] diff --git a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs deleted file mode 100644 index 5d8521e..0000000 --- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs +++ /dev/null @@ -1,30 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.FocusedModule (focusedModule, FocusedModParams(..)) where - -import Control.Lens hiding ((.=)) -import Data.Aeson as JSON - - -import Cryptol.ModuleSystem (meFocusedModule, meLoadedModules) -import Cryptol.ModuleSystem.Env (isLoadedParamMod) -import Cryptol.Utils.PP - -import Argo -import CryptolServer - -focusedModule :: FocusedModParams -> Method ServerState JSON.Value -focusedModule _ = - do me <- view moduleEnv <$> getState - case meFocusedModule me of - Nothing -> - return $ JSON.object [ "module" .= JSON.Null ] - Just name -> - do let parameterized = isLoadedParamMod name (meLoadedModules me) - return $ JSON.object [ "module" .= pretty name - , "parameterized" .= parameterized - ] - -data FocusedModParams = FocusedModParams - -instance JSON.FromJSON FocusedModParams where - parseJSON _ = pure FocusedModParams diff --git a/cryptol-remote-api/src/CryptolServer/LoadModule.hs b/cryptol-remote-api/src/CryptolServer/LoadModule.hs deleted file mode 100644 index 6f8a18c..0000000 --- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.LoadModule - ( loadFile - , loadModule - , LoadFileParams(..) - , LoadModuleParams(..) - ) where - -import Control.Applicative -import Data.Aeson as JSON -import qualified Data.Text as T -import Data.Functor - -import Cryptol.ModuleSystem (loadModuleByPath, loadModuleByName) -import Cryptol.Parser (parseModName) -import Cryptol.Parser.AST (ModName) - -import CryptolServer -import Argo - - -loadFile :: LoadFileParams -> Method ServerState () -loadFile (LoadFileParams fn) = - void $ runModuleCmd (loadModuleByPath fn) - -newtype LoadFileParams - = LoadFileParams FilePath - -instance JSON.FromJSON LoadFileParams where - parseJSON = - JSON.withObject "params for \"load module\"" $ - \o -> LoadFileParams <$> o .: "file" - -loadModule :: LoadModuleParams -> Method ServerState () -loadModule (LoadModuleParams mn) = - void $ runModuleCmd (loadModuleByName mn) - -newtype JSONModuleName - = JSONModuleName { unJSONModName :: ModName } - -instance JSON.FromJSON JSONModuleName where - parseJSON = - JSON.withText "module name" $ - \txt -> - case parseModName (T.unpack txt) of - Nothing -> empty - Just n -> return (JSONModuleName n) - -newtype LoadModuleParams - = LoadModuleParams ModName - -instance JSON.FromJSON LoadModuleParams where - parseJSON = - JSON.withObject "params for \"load module\"" $ - \o -> LoadModuleParams . unJSONModName <$> o .: "module name" diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs deleted file mode 100644 index d381e8e..0000000 --- a/cryptol-remote-api/src/CryptolServer/Names.hs +++ /dev/null @@ -1,61 +0,0 @@ -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.Names (visibleNames) where - -import Control.Lens hiding ((.=)) -import qualified Data.Aeson as JSON -import Data.Aeson ((.=)) -import qualified Data.Map as Map -import Data.Map (Map) -import Data.Text (unpack) - -import Cryptol.Parser.Name (PName(..)) -import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv) -import Cryptol.ModuleSystem.Interface (IfaceDecl(..), IfaceDecls(..)) -import Cryptol.ModuleSystem.Name (Name) -import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), lookupValNames, shadowing) -import Cryptol.TypeCheck.Type (Schema(..)) -import Cryptol.Utils.PP (pp) - -import Argo - -import CryptolServer -import CryptolServer.Data.Type - - -visibleNames :: JSON.Value -> Method ServerState [NameInfo] -visibleNames _ = - do me <- view moduleEnv <$> getState - let DEnv { deNames = dyNames } = meDynEnv me - let ModContext { mctxDecls = fDecls, mctxNames = fNames} = focusedEnv me - let inScope = Map.keys (neExprs $ dyNames `shadowing` fNames) - return $ concatMap (getInfo fNames (ifDecls fDecls)) inScope - -getInfo :: NamingEnv -> Map Name IfaceDecl -> PName -> [NameInfo] -getInfo rnEnv info n' = - [ case Map.lookup n info of - Nothing -> error $ "Name not found, but should have been: " ++ show n - Just i -> - let ty = ifDeclSig i - nameDocs = ifDeclDoc i - in NameInfo (show (pp n')) (show (pp ty)) ty (unpack <$> nameDocs) - | n <- lookupValNames n' rnEnv - ] - -data NameInfo = - NameInfo - { name :: String - , typeSig :: String - , schema :: Schema - , nameDocs :: Maybe String - } - -instance JSON.ToJSON NameInfo where - toJSON (NameInfo{name, typeSig, schema, nameDocs}) = - JSON.object $ - [ "name" .= name - , "type string" .= typeSig - , "type" .= JSON.toJSON (JSONSchema schema) - ] ++ - maybe [] (\d -> ["documentation" .= d]) nameDocs diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs deleted file mode 100644 index 1cc171e..0000000 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ /dev/null @@ -1,132 +0,0 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.Sat (sat, ProveSatParams(..)) where - -import Control.Applicative -import Control.Lens hiding ((.=)) -import Control.Monad.IO.Class -import Data.Aeson ((.=), (.:), FromJSON, ToJSON) -import qualified Data.Aeson as JSON -import Data.IORef -import Data.Scientific (floatingOrInteger) -import Data.Text (Text) -import qualified Data.Text as T - -import Cryptol.Eval.Concrete.Value (Value) -import Cryptol.ModuleSystem (checkExpr, getPrimMap) -import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv, meSolverConfig) -import Cryptol.Symbolic (ProverCommand(..), ProverResult(..), QueryType(..), SatNum(..)) -import Cryptol.Symbolic.SBV (proverNames, satProve, setupProver) -import Cryptol.TypeCheck.AST (Expr, Type) -import Cryptol.TypeCheck.Solve (defaultReplExpr) -import qualified Cryptol.TypeCheck.Solver.SMT as SMT - -import Argo - -import CryptolServer -import CryptolServer.Exceptions (evalPolyErr, proverError) -import CryptolServer.Data.Expression -import CryptolServer.Data.Type - -sat :: ProveSatParams -> Method ServerState SatResult -sat (ProveSatParams (Prover name) jsonExpr num) = - do e <- getExpr jsonExpr - (_expr, ty, schema) <- runModuleCmd (checkExpr e) - -- TODO validEvalContext expr, ty, schema - me <- view moduleEnv <$> getState - let decls = deDecls (meDynEnv me) - let cfg = meSolverConfig me - perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema) - case perhapsDef of - Nothing -> - raise (evalPolyErr schema) - Just (_tys, checked) -> - do timing <- liftIO $ newIORef 0 - let cmd = - ProverCommand - { pcQueryType = SatQuery num - , pcProverName = name - , pcVerbose = True -- verbose - , pcProverStats = timing - , pcExtraDecls = decls - , pcSmtFile = Nothing -- mfile - , pcExpr = checked - , pcSchema = schema - , pcValidate = False - , pcIgnoreSafety = False - } - sbvCfg <- liftIO (setupProver name) >>= \case - Left msg -> error msg - Right (_ws, sbvCfg) -> return sbvCfg - (_firstProver, res) <- runModuleCmd $ satProve sbvCfg cmd - _stats <- liftIO (readIORef timing) - case res of - ProverError msg -> raise (proverError msg) - EmptyResult -> error "got empty result for online prover!" - ThmResult _ts -> pure Unsatisfiable - AllSatResult results -> - Satisfied <$> traverse satResult results - - where - satResult :: [(Type, Expr, Value)] -> Method ServerState [(JSONType, Expression)] - satResult es = traverse result es - - result (t, _, v) = - do prims <- runModuleCmd getPrimMap - e <- observe $ readBack prims t v - return (JSONType mempty t, e) - -data SatResult = Unsatisfiable | Satisfied [[(JSONType, Expression)]] - -instance ToJSON SatResult where - toJSON Unsatisfiable = JSON.object ["result" .= ("unsatisfiable" :: Text)] - toJSON (Satisfied xs) = - JSON.object [ "result" .= ("satisfied" :: Text) - , "model" .= - [ [ JSON.object [ "type" .= t - , "expr" .= e - ] - | (t, e) <- res - ] - | res <- xs - ] - ] - - -newtype Prover = Prover String - -instance FromJSON Prover where - parseJSON = - JSON.withText "prover name" $ - \txt -> - let str = T.unpack txt - in if str `elem` proverNames - then return (Prover str) - else empty - - -data ProveSatParams = - ProveSatParams - { prover :: Prover - , expression :: Expression - , numResults :: SatNum - } - -instance FromJSON ProveSatParams where - parseJSON = - JSON.withObject "sat or prove parameters" $ - \o -> - do prover <- o .: "prover" - expression <- o .: "expression" - numResults <- (o .: "result count" >>= num) - pure ProveSatParams{prover, expression, numResults} - where - num v = ((JSON.withText "all" $ - \t -> if t == "all" then pure AllSat else empty) v) <|> - ((JSON.withScientific "count" $ - \s -> - case floatingOrInteger s of - Left (_float :: Double) -> empty - Right int -> pure (SomeSat int)) v) diff --git a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs deleted file mode 100644 index 7801504..0000000 --- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs +++ /dev/null @@ -1,36 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module CryptolServer.TypeCheck (checkType, TypeCheckParams(..)) where - -import Control.Lens hiding ((.=)) -import Data.Aeson as JSON - - -import Cryptol.ModuleSystem (checkExpr) -import Cryptol.ModuleSystem.Env (meSolverConfig) - -import Argo - -import CryptolServer -import CryptolServer.Exceptions -import CryptolServer.Data.Expression -import CryptolServer.Data.Type - -checkType :: TypeCheckParams -> Method ServerState JSON.Value -checkType (TypeCheckParams e) = - do e' <- getExpr e - (_expr, _ty, schema) <- runModuleCmd (checkExpr e') - -- FIXME: why are we running this command if the result isn't used? - _cfg <- meSolverConfig . view moduleEnv <$> getState - return (JSON.object [ "type schema" .= JSONSchema schema ]) - where - -- FIXME: Why is this check not being used? - _noDefaults [] = return () - _noDefaults xs@(_:_) = raise (unwantedDefaults xs) - -newtype TypeCheckParams = - TypeCheckParams Expression - -instance JSON.FromJSON TypeCheckParams where - parseJSON = - JSON.withObject "params for \"check type\"" $ - \o -> TypeCheckParams <$> o .: "expression" diff --git a/cryptol-remote-api/test-scripts/Foo.cry b/cryptol-remote-api/test-scripts/Foo.cry deleted file mode 100644 index 4a3dd15..0000000 --- a/cryptol-remote-api/test-scripts/Foo.cry +++ /dev/null @@ -1,17 +0,0 @@ -module Foo where - -id : {a} a -> a -id x = x - -x : [8] -x = 255 - -add : {a} (fin a) => [a] -> [a] -> [a] -add = (+) - -foo : {foo : [32], bar : [32]} -foo = {foo = 23, bar = 99} - -getFoo : {foo : [32], bar : [32]} -> [32] -getFoo x = x.foo - diff --git a/cryptol-remote-api/test-scripts/Inst.cry b/cryptol-remote-api/test-scripts/Inst.cry deleted file mode 100644 index 3e72648..0000000 --- a/cryptol-remote-api/test-scripts/Inst.cry +++ /dev/null @@ -1,4 +0,0 @@ -module Inst = - Param where - type w = 8 - diff --git a/cryptol-remote-api/test-scripts/Param.cry b/cryptol-remote-api/test-scripts/Param.cry deleted file mode 100644 index 84619d7..0000000 --- a/cryptol-remote-api/test-scripts/Param.cry +++ /dev/null @@ -1,8 +0,0 @@ -module Param where -parameter - type w : # - type constraint (fin w) - -foo : [w] -> [2 * w] -foo x = x # x - diff --git a/cryptol-remote-api/test-scripts/cryptol-api_test.py b/cryptol-remote-api/test-scripts/cryptol-api_test.py deleted file mode 100644 index 61aee20..0000000 --- a/cryptol-remote-api/test-scripts/cryptol-api_test.py +++ /dev/null @@ -1,23 +0,0 @@ -import os - -from cryptol import CryptolConnection, CryptolContext, cry -import cryptol -import cryptol.cryptoltypes - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -c = cryptol.connect("cabal new-exec --verbose=0 cryptol-remote-api") - -c.change_directory(dir_path) - -c.load_file("Foo.cry") - -val = c.evaluate_expression("x").result() - -assert c.call('add', b'\0', b'\1').result() == b'\x01' -assert c.call('add', bytes.fromhex('ff'), bytes.fromhex('03')).result() == bytes.fromhex('02') - - -cryptol.add_cryptol_module('Foo', c) -from Foo import * -assert add(b'\2', 2) == b'\4' diff --git a/cryptol-remote-api/test-scripts/cryptol-tests.py b/cryptol-remote-api/test-scripts/cryptol-tests.py deleted file mode 100644 index f21ed50..0000000 --- a/cryptol-remote-api/test-scripts/cryptol-tests.py +++ /dev/null @@ -1,175 +0,0 @@ -import os -from pathlib import Path -import signal -import subprocess -import sys -import time - -import argo.connection as argo -import cryptol -from cryptol import CryptolConnection, CryptolContext, cry - -dir_path = Path(os.path.dirname(os.path.realpath(__file__))) - -cryptol_path = dir_path.joinpath('test-data') - - - -def low_level_api_test(c): - - id_1 = c.send_message("load module", {"module name": "M", "state": None}) - reply_1 = c.wait_for_reply_to(id_1) - assert('result' in reply_1) - assert('state' in reply_1['result']) - assert('answer' in reply_1['result']) - state_1 = reply_1['result']['state'] - - id_2 = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1}) - reply_2 = c.wait_for_reply_to(id_2) - assert('result' in reply_2) - assert('answer' in reply_2['result']) - assert('value' in reply_2['result']['answer']) - assert(reply_2['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - - id_3 = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1}) - reply_3 = c.wait_for_reply_to(id_3) - assert('result' in reply_3) - assert('answer' in reply_3['result']) - assert('value' in reply_3['result']['answer']) - assert(reply_3['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - - id_4 = c.send_message("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state_1}) - reply_4 = c.wait_for_reply_to(id_4) - assert('result' in reply_4) - assert('answer' in reply_4['result']) - assert('value' in reply_4['result']['answer']) - assert(reply_4['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - - a_record = {"expression": "record", - "data": {"unit": "()", - "fifteen": {"expression": "bits", - "encoding": "hex", - "width": 4, - "data": "f"}}} - - id_5 = c.send_message("evaluate expression", {"state": state_1, "expression": a_record}) - reply_5 = c.wait_for_reply_to(id_5) - assert('result' in reply_5) - assert('answer' in reply_5['result']) - assert('value' in reply_5['result']['answer']) - assert(reply_5['result']['answer']['value'] == - {'expression': 'record', - 'data': {'fifteen': - {'data': 'f', - 'width': 4, - 'expression': 'bits', - 'encoding': 'hex'}, - 'unit': - {'expression': 'unit'}}}) - - id_6 = c.send_message("evaluate expression", - {"state": state_1, - "expression": {"expression": "let", - "binders": [{"name": "theRecord", "definition": a_record}], - "body": {"expression": "tuple", - "data": [a_record, "theRecord"]}}}) - reply_6 = c.wait_for_reply_to(id_6) - assert('result' in reply_6) - assert('answer' in reply_6['result']) - assert('value' in reply_6['result']['answer']) - assert(reply_6['result']['answer']['value'] == - {'expression': 'tuple', - 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}, - {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}]}) - - id_7 = c.send_message("evaluate expression", - {"state": state_1, - "expression": {"expression": "sequence", - "data": [a_record, a_record]}}) - reply_7 = c.wait_for_reply_to(id_7) - assert('result' in reply_7) - assert('answer' in reply_7['result']) - assert('value' in reply_7['result']['answer']) - assert(reply_7['result']['answer']['value'] == - {'expression': 'sequence', - 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}, - {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}]}) - - id_8 = c.send_message("evaluate expression", - {"state": state_1, - "expression": {"expression": "integer modulo", - "integer": 14, - "modulus": 42}}) - reply_8 = c.wait_for_reply_to(id_8) - assert('result' in reply_8) - assert('answer' in reply_8['result']) - assert('value' in reply_8['result']['answer']) - assert(reply_8['result']['answer']['value'] == - {"expression": "integer modulo", - "integer": 14, - "modulus": 42}) - - id_9 = c.send_message("evaluate expression", - {"state": state_1, - "expression": "m `{a=60}"}) - reply_9 = c.wait_for_reply_to(id_9) - assert('result' in reply_9) - assert('answer' in reply_9['result']) - assert('value' in reply_9['result']['answer']) - assert(reply_9['result']['answer']['value'] == - {"expression": "integer modulo", - "integer": 42, - "modulus": 60}) - -# Test with both sockets and stdio - -c1 = argo.ServerConnection( - cryptol.CryptolDynamicSocketProcess( - "cabal v2-exec cryptol-remote-api --verbose=0", - cryptol_path=cryptol_path)) -c2 = argo.ServerConnection( - cryptol.CryptolStdIOProcess( - "cabal v2-exec cryptol-remote-api --verbose=0 -- --stdio", - cryptol_path=cryptol_path)) - -low_level_api_test(c1) -low_level_api_test(c2) - -env = os.environ.copy() -env['CRYPTOLPATH'] = cryptol_path - -p = subprocess.Popen( - ["cabal", "v2-exec", "cryptol-remote-api", "--verbose=0", "--", "--port", "50005"], - stdout=subprocess.DEVNULL, - stdin=subprocess.DEVNULL, - stderr=subprocess.DEVNULL, - start_new_session=True, - env=env) - -time.sleep(5) -assert(p is not None) -assert(p.poll() is None) - -c3 = argo.ServerConnection( - argo.RemoteSocketProcess('localhost', 50005, ipv6=True)) - -low_level_api_test(c3) - -os.killpg(os.getpgid(p.pid), signal.SIGKILL) diff --git a/cryptol-remote-api/test-scripts/test-data/M.cry b/cryptol-remote-api/test-scripts/test-data/M.cry deleted file mode 100644 index fdfc788..0000000 --- a/cryptol-remote-api/test-scripts/test-data/M.cry +++ /dev/null @@ -1,12 +0,0 @@ -module M where -f : [8] -> [2][8] -f x = repeat x - -g : [8] -> [2][8] -g x = [x, x] - -h : [2][8] -> [2][8] -h x = x - -m : {a} (fin a, a > 42) => Z a -m = 42 diff --git a/cryptol-remote-api/test/Test.hs b/cryptol-remote-api/test/Test.hs deleted file mode 100644 index d17eb1c..0000000 --- a/cryptol-remote-api/test/Test.hs +++ /dev/null @@ -1,83 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -module Main where - -import Data.Aeson as JSON (fromJSON, toJSON, Result(..)) - -import Data.ByteString.Lazy (ByteString) -import qualified Data.HashMap.Strict as HM -import Data.List.NonEmpty(NonEmpty(..)) - -import Test.QuickCheck.Instances.ByteString -import Test.QuickCheck.Instances.Scientific -import Test.QuickCheck.Instances.Text -import Test.Tasty -import Test.Tasty.HUnit.ScriptExit -import Test.Tasty.QuickCheck - -import CryptolServer.Call - -import Debug.Trace - -import Argo.PythonBindings -import Paths_cryptol_remote_api - -main :: IO () -main = - do reqs <- getArgoPythonFile "requirements.txt" - withPython3venv (Just reqs) $ \pip python -> - do pySrc <- getArgoPythonFile "." - testScriptsDir <- getDataFileName "test-scripts/" - pip ["install", pySrc] - putStrLn "pipped" - - scriptTests <- makeScriptTests testScriptsDir [python] - - defaultMain $ - testGroup "Tests for saw-remote-api" - [ testGroup "Scripting API tests" scriptTests - , callMsgProps - ] - -instance Arbitrary Encoding where - arbitrary = oneof [pure Hex, pure Base64] - -instance Arbitrary Expression where - arbitrary = sized spec - where - spec n - | n <= 0 = - oneof [ Bit <$> arbitrary - , pure Unit - , Num <$> arbitrary <*> arbitrary <*> arbitrary - , Integer <$> arbitrary - -- NB: The following case will not generate - -- syntactically valid Cryptol. But for testing - -- round-tripping of the JSON, and coverage of various - -- functions, it's better than nothing. - , Concrete <$> arbitrary - ] - | otherwise = - choose (2, n) >>= - \len -> - let sub = n `div` len - in - oneof [ Record . HM.fromList <$> vectorOf len ((,) <$> arbitrary <*> spec sub) - , Sequence <$> vectorOf len (spec sub) - , Tuple <$> vectorOf len (spec sub) - -- NB: Will not make valid identifiers, so if we - -- ever insert validation, then this will need to - -- change. - , Let <$> vectorOf len (LetBinding <$> arbitrary <*> spec sub) <*> spec sub - , Application <$> spec sub <*> ((:|) <$> spec sub <*> vectorOf len (spec sub)) - ] - -callMsgProps :: TestTree -callMsgProps = - testGroup "QuickCheck properties for the \"call\" message" - [ testProperty "encoding and decoding arg specs is the identity" $ - \(spec :: Expression) -> - case fromJSON (toJSON spec) of - JSON.Success v -> spec == v - JSON.Error err -> False - ] diff --git a/tasty-script-exitcode/src/Test/Tasty/HUnit/ScriptExit.hs b/tasty-script-exitcode/src/Test/Tasty/HUnit/ScriptExit.hs index 53abda2..30ecda0 100644 --- a/tasty-script-exitcode/src/Test/Tasty/HUnit/ScriptExit.hs +++ b/tasty-script-exitcode/src/Test/Tasty/HUnit/ScriptExit.hs @@ -9,7 +9,9 @@ import System.Directory import System.Exit import System.FilePath import System.IO.Temp (withSystemTempDirectory) +import System.Info (os) import System.Process +import Control.Applicative import Data.List import Data.Map (Map) import qualified Data.Map as Map @@ -82,7 +84,15 @@ withPython3venv :: IO a withPython3venv requirements todo = withSystemTempDirectory "virtenv" $ \venvDir -> - do let process = proc "python3" ["-m", "venv", venvDir] + -- Some systems install Python 3 as `python3`, but some call it `python`. + do mpy3 <- findExecutable "python3" + mpy <- findExecutable "python" + pyExe <- case mpy3 <|> mpy of + Just exeName -> return exeName + Nothing -> assertFailure "Python executable not found." + let process = proc pyExe ["-m", "venv", venvDir] + binDir = if os == "mingw32" then "Scripts" else "bin" + pipInstall = proc pyExe ["-m", "pip", "install", "--upgrade", "pip"] (exitCode, stdout, stderr) <- readCreateProcessWithExitCode process "" case exitCode of ExitFailure code -> @@ -95,11 +105,11 @@ withPython3venv requirements todo = TestLang { testLangName = "Python in virtualenv" , testLangExtension = ".py" - , testLangExecutable = venvDir "bin" "python" + , testLangExecutable = venvDir binDir "python" , testLangArgsFormat = \file -> [file] } pip args = - let pipProc = proc (venvDir "bin" "pip") args in + let pipProc = proc (venvDir binDir "pip") args in readCreateProcessWithExitCode pipProc "" >>= \case (ExitFailure code, pipStdout, pipStderr) -> @@ -109,8 +119,16 @@ withPython3venv requirements todo = ":\nstdout: " <> pipStdout <> "\nstderr: " <> pipStderr (ExitSuccess, _, _) -> pure () - in do traverse (\reqPath -> pip ["install", "-r", reqPath]) requirements - todo pip venvPython + in do (exitCode, stdout, stderr) <- readCreateProcessWithExitCode pipInstall "" + case exitCode of + ExitFailure code -> + assertFailure $ + "Failed to install `pip` with code " <> + show code <> ": " <> + ":\nstdout: " <> stdout <> "\nstderr: " <> stderr + ExitSuccess -> do + traverse (\reqPath -> pip ["install", "-r", reqPath]) requirements + todo pip venvPython -- | Given a list of @TestLang@s to use and a list of possible script diff --git a/tasty-script-exitcode/tasty-script-exitcode.cabal b/tasty-script-exitcode/tasty-script-exitcode.cabal index f5c70f8..2970bc7 100644 --- a/tasty-script-exitcode/tasty-script-exitcode.cabal +++ b/tasty-script-exitcode/tasty-script-exitcode.cabal @@ -29,13 +29,13 @@ library exposed-modules: Test.Tasty.HUnit.ScriptExit -- other-modules: other-extensions: NamedFieldPuns - build-depends: base >=4.12 && <4.14, - process ^>=1.6.3.0, - filepath ^>=1.4.2.1, - directory ^>=1.3.3.0, - containers ^>=0.6.0.1, - tasty-hunit ^>= 0.10, - tasty ^>= 1.2, - temporary ^>= 1.3 + build-depends: base >=4.12, + process >=1.6.3.0, + filepath >=1.4.2.1, + directory >=1.3.3.0, + containers >=0.6.0.1, + tasty-hunit >= 0.10, + tasty >= 1.2, + temporary >= 1.3 hs-source-dirs: src default-language: Haskell2010