From 302054cfb925f364ea243a2320804928fb380afc Mon Sep 17 00:00:00 2001 From: Simon Winwood Date: Mon, 21 Aug 2023 14:29:34 -0700 Subject: [PATCH] talos: clean ups --- talos/src/Talos/Solver/ModelParser.hs | 105 +++++++++----------------- talos/src/Talos/Solver/SolverT.hs | 11 +-- 2 files changed, 40 insertions(+), 76 deletions(-) diff --git a/talos/src/Talos/Solver/ModelParser.hs b/talos/src/Talos/Solver/ModelParser.hs index a4205b40..4aa83c87 100644 --- a/talos/src/Talos/Solver/ModelParser.hs +++ b/talos/src/Talos/Solver/ModelParser.hs @@ -10,20 +10,17 @@ module Talos.Solver.ModelParser import Control.Applicative import Control.Monad (ap, guard) -import Data.ByteString (ByteString) -import qualified Data.ByteString as BS import Data.Char (isDigit) import Data.List (foldl') import Data.Map (Map) import qualified Data.Map as Map -import qualified Data.Vector as V import Data.Word import SimpleSMT (SExpr (..)) import Text.Read (readMaybe) import Daedalus.Core +import Daedalus.Panic (panic) import Daedalus.PP (showPP) -import Daedalus.Panic import qualified Daedalus.Value as I -- ----------------------------------------------------------------------------- @@ -108,52 +105,32 @@ pExact a = pAtom >>= guard . (==) a pSExpr :: ModelP a -> ModelP a pSExpr = pHead (const empty) -withSExprs :: [SExpr] -> ModelP a -> ModelP a -withSExprs ss m = ModelP $ \st -> do - r <- evalModelP' m (st { sexps = ss }) - pure (r, st) - -pArray :: Integer -> ModelP a -> ModelP a -pArray count p = do - (els, arr) <- go - let v = V.replicate (fromInteger count) arr V.// els - withSExprs (V.toList v) p - where - -- FIXME: maybe use a mutable vector here? - base :: ModelP ([(Int, SExpr)], SExpr) - base = pSExpr $ do - pExact "const" - s <- pRawHead - pure ([], s) - - go :: ModelP ([(Int, SExpr)], SExpr) - go = - base <|> - (pSExpr $ - do pExact "store" - (els, arr) <- go - i <- pNumber - s <- pRawHead - pure (if i < count then (fromInteger i, s) : els else els, arr)) - --- FIXME: do we need this? - --- getValue :: String -> ModelP SExpr --- getValue a = do --- m_sexpr <- ModelP $ asks (Map.lookup a . vEnv) --- case m_sexpr of --- Just v -> pure v --- Nothing -> do --- s <- ModelP $ asks solver --- res <- liftIO $ command s $ fun "get-value" [List [S.const a]] --- case res of --- List [List [_, v]] -> pure v --- _ -> panic (unlines --- [ "Unexpected response from the SMT solver:" --- , " Exptected: a value" --- , " Result: " ++ showsSExpr res "" --- ]) [] - +-- withSExprs :: [SExpr] -> ModelP a -> ModelP a +-- withSExprs ss m = ModelP $ \st -> do +-- r <- evalModelP' m (st { sexps = ss }) +-- pure (r, st) + +-- pArray :: Integer -> ModelP a -> ModelP a +-- pArray count p = do +-- (els, arr) <- go +-- let v = V.replicate (fromInteger count) arr V.// els +-- withSExprs (V.toList v) p +-- where +-- -- FIXME: maybe use a mutable vector here? +-- base :: ModelP ([(Int, SExpr)], SExpr) +-- base = pSExpr $ do +-- pExact "const" +-- s <- pRawHead +-- pure ([], s) + +-- go :: ModelP ([(Int, SExpr)], SExpr) +-- go = +-- base <|> +-- pSExpr (do pExact "store" +-- (els, arr) <- go +-- i <- pNumber +-- s <- pRawHead +-- pure (if i < count then (fromInteger i, s) : els else els, arr)) -------------------------------------------------------------------------------- -- Combinators @@ -161,18 +138,6 @@ pArray count p = do -- Only what is needed by the relation type generated in SymExec.hs -- (sum, product, bytes, unit) --- pTuple :: ModelP a -> ModelP b -> ModelP (a, b) --- pTuple l r = pSExpr $ do --- pExact "mk-tuple" --- (,) <$> l <*> r - --- pUnit :: ModelP () --- pUnit = pExact "unit" - --- pSum :: ModelP a -> ModelP a -> ModelP a --- pSum l r = pSExpr $ do --- (pExact "inl" *> l) <|> (pExact "inr" *> r) - pNumber :: ModelP Integer pNumber = pAtom >>= go where @@ -202,14 +167,14 @@ pNumber = pAtom >>= go pByte :: ModelP Word8 pByte = fromIntegral <$> pNumber --- This is nicer, we could use pHead directly -pList :: ModelP a -> ModelP [a] -pList p = ([] <$ pExact "nil") <|> - (pSExpr $ do pExact "insert" - (:) <$> p <*> pList p) +-- -- This is nicer, we could use pHead directly +-- pList :: ModelP a -> ModelP [a] +-- pList p = ([] <$ pExact "nil") <|> +-- (pSExpr $ do pExact "insert" +-- (:) <$> p <*> pList p) -pByteString :: ModelP ByteString -pByteString = BS.pack <$> pList pByte +-- pByteString :: ModelP ByteString +-- pByteString = BS.pack <$> pList pByte pBool :: ModelP Bool pBool = pAtom >>= go @@ -242,6 +207,8 @@ pValue ty0 = go ty0 TIterator {} -> unimplemented TUser _ut -> unimplemented TParam {} -> unimplemented + TFloat -> unimplemented + TDouble -> unimplemented unimplemented = panic "sexprToValue: Unimplemented" [ showPP ty0 ] diff --git a/talos/src/Talos/Solver/SolverT.hs b/talos/src/Talos/Solver/SolverT.hs index 92ea6349..d07e87dc 100644 --- a/talos/src/Talos/Solver/SolverT.hs +++ b/talos/src/Talos/Solver/SolverT.hs @@ -60,13 +60,10 @@ import SimpleSMT (SExpr, Solver) import Daedalus.Core hiding (freshName) import qualified Daedalus.Core as C -import Daedalus.GUID -import Daedalus.Panic -import Daedalus.PP - - --- import Text.Printf (printf) - +import Daedalus.GUID (GUID, HasGUID (..), getNextGUID) +import Daedalus.Panic (panic) +import Daedalus.PP (PP (pp), bullets, hang, showPP, + text, vcat, (<+>)) type SMTVar = String data QueuedCommand =