From 96b7ccb82652ad5ff7b6bcbf77ff28b54083566d Mon Sep 17 00:00:00 2001 From: Johannes Waldmann Date: Fri, 5 Mar 2021 19:13:47 +0100 Subject: [PATCH] for #19 --- Language/SMTLib2/Internals/Embed.hs | 1 + Language/SMTLib2/Internals/Evaluate.hs | 1 + Language/SMTLib2/Internals/Proof/Verify.hs | 1 + Language/SMTLib2/Internals/Type/List.hs | 1 + Language/SMTLib2/Internals/Type/Struct.hs | 1 + .../Language/SMTLib2/Composite/Array.hs | 1 + .../SMTLib2/Composite/Array/Bounded.hs | 7 +++++-- .../SMTLib2/Composite/Array/Composite.hs | 1 + .../SMTLib2/Composite/Array/Static.hs | 1 + .../Language/SMTLib2/Composite/Choice.hs | 11 ++++++----- .../Language/SMTLib2/Composite/Class.hs | 5 +++++ .../Language/SMTLib2/Composite/Container.hs | 15 +++++++++------ .../Language/SMTLib2/Composite/Domains.hs | 9 +++++---- .../Language/SMTLib2/Composite/Either.hs | 1 + .../Language/SMTLib2/Composite/Expression.hs | 3 ++- .../Language/SMTLib2/Composite/Linear.hs | 7 ++++--- .../Language/SMTLib2/Composite/List.hs | 1 + .../Language/SMTLib2/Composite/Map.hs | 1 + .../Language/SMTLib2/Composite/Singleton.hs | 3 +++ .../Language/SMTLib2/Composite/Stack.hs | 19 ++++++++++--------- .../Language/SMTLib2/Composite/Tuple.hs | 9 +++++---- .../Language/SMTLib2/ModulusEmulator.hs | 1 + .../quickcheck/Language/SMTLib2/QuickCheck.hs | 3 ++- smtlib2.cabal | 4 ++-- stack.yaml | 1 + 25 files changed, 71 insertions(+), 37 deletions(-) diff --git a/Language/SMTLib2/Internals/Embed.hs b/Language/SMTLib2/Internals/Embed.hs index 77294e3..f44c2dd 100644 --- a/Language/SMTLib2/Internals/Embed.hs +++ b/Language/SMTLib2/Internals/Embed.hs @@ -13,6 +13,7 @@ import Control.Monad.State import Control.Monad.Except import Control.Monad.Writer import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import qualified Data.Dependent.Map as DMap diff --git a/Language/SMTLib2/Internals/Evaluate.hs b/Language/SMTLib2/Internals/Evaluate.hs index 5214e81..0b81725 100644 --- a/Language/SMTLib2/Internals/Evaluate.hs +++ b/Language/SMTLib2/Internals/Evaluate.hs @@ -9,6 +9,7 @@ import qualified Language.SMTLib2.Internals.Type.List as List import Data.GADT.Compare import Data.GADT.Show +import Data.Type.Equality ((:~:)(Refl)) import Data.List (genericLength) import Data.Bits import Data.Dependent.Map (DMap) diff --git a/Language/SMTLib2/Internals/Proof/Verify.hs b/Language/SMTLib2/Internals/Proof/Verify.hs index 1f69666..b784b90 100644 --- a/Language/SMTLib2/Internals/Proof/Verify.hs +++ b/Language/SMTLib2/Internals/Proof/Verify.hs @@ -8,6 +8,7 @@ import Language.SMTLib2 import qualified Language.SMTLib2.Internals.Expression as E import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Control.Monad.State import Control.Monad.Except diff --git a/Language/SMTLib2/Internals/Type/List.hs b/Language/SMTLib2/Internals/Type/List.hs index b6cbb22..f45d551 100644 --- a/Language/SMTLib2/Internals/Type/List.hs +++ b/Language/SMTLib2/Internals/Type/List.hs @@ -4,6 +4,7 @@ import Language.SMTLib2.Internals.Type.Nat import Prelude hiding (head,tail,length,mapM,insert,drop,take,last,reverse,map,traverse,concat,replicate) import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Language.Haskell.TH diff --git a/Language/SMTLib2/Internals/Type/Struct.hs b/Language/SMTLib2/Internals/Type/Struct.hs index 2f1e35a..509e055 100644 --- a/Language/SMTLib2/Internals/Type/Struct.hs +++ b/Language/SMTLib2/Internals/Type/Struct.hs @@ -6,6 +6,7 @@ import qualified Language.SMTLib2.Internals.Type.List as List import Prelude hiding (mapM,insert) import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Data.Functor.Identity diff --git a/extras/composite/Language/SMTLib2/Composite/Array.hs b/extras/composite/Language/SMTLib2/Composite/Array.hs index ca33028..310dcec 100644 --- a/extras/composite/Language/SMTLib2/Composite/Array.hs +++ b/extras/composite/Language/SMTLib2/Composite/Array.hs @@ -13,6 +13,7 @@ import qualified Language.SMTLib2.Internals.Type.List as List import Data.GADT.Show import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.Functor.Identity import Control.Monad.Reader import Control.Monad.Except diff --git a/extras/composite/Language/SMTLib2/Composite/Array/Bounded.hs b/extras/composite/Language/SMTLib2/Composite/Array/Bounded.hs index ad8fb90..198418b 100644 --- a/extras/composite/Language/SMTLib2/Composite/Array/Bounded.hs +++ b/extras/composite/Language/SMTLib2/Composite/Array/Bounded.hs @@ -1,3 +1,5 @@ +{-# language UndecidableInstances #-} + module Language.SMTLib2.Composite.Array.Bounded where import Language.SMTLib2 hiding (select,store) @@ -6,6 +8,7 @@ import Language.SMTLib2.Composite.Domains import Data.Monoid import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Prelude hiding (Bounded) @@ -90,7 +93,7 @@ instance (IsArray arr idx,IsRanged idx,IsNumSingleton idx) then return AlwaysError else do ridx <- compositeFromValue idx' - Just errCond <- compositeGEQ ridx (bound arr) + errCond <- unJust $ compositeGEQ ridx (bound arr) return $ SometimesError errCond instance (IsArray arr idx,IsRanged idx,IsNumSingleton idx) @@ -107,7 +110,7 @@ instance (IsArray arr idx,IsRanged idx,IsNumSingleton idx) else if nullRange insideRange then return AlwaysError else do - Just errCond <- compositeGEQ idx (bound arr) + errCond <- unJust $ compositeGEQ idx (bound arr) return $ SometimesError errCond arraySize arr = return $ bound arr diff --git a/extras/composite/Language/SMTLib2/Composite/Array/Composite.hs b/extras/composite/Language/SMTLib2/Composite/Array/Composite.hs index fb2a6d2..816b2fd 100644 --- a/extras/composite/Language/SMTLib2/Composite/Array/Composite.hs +++ b/extras/composite/Language/SMTLib2/Composite/Array/Composite.hs @@ -14,6 +14,7 @@ import Control.Monad.State import Data.Functor.Identity import Data.GADT.Show import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) data AnyList (e :: Type -> *) = forall tps. AnyList (List e tps) diff --git a/extras/composite/Language/SMTLib2/Composite/Array/Static.hs b/extras/composite/Language/SMTLib2/Composite/Array/Static.hs index 016817c..911773d 100644 --- a/extras/composite/Language/SMTLib2/Composite/Array/Static.hs +++ b/extras/composite/Language/SMTLib2/Composite/Array/Static.hs @@ -7,6 +7,7 @@ import Language.SMTLib2.Composite.Domains import Data.Map (Map) import qualified Data.Map as Map import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Text.Show import Data.Functor.Identity diff --git a/extras/composite/Language/SMTLib2/Composite/Choice.hs b/extras/composite/Language/SMTLib2/Composite/Choice.hs index 7a1c915..500c607 100644 --- a/extras/composite/Language/SMTLib2/Composite/Choice.hs +++ b/extras/composite/Language/SMTLib2/Composite/Choice.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds,GADTs,TypeFamilies,ExistentialQuantification,ScopedTypeVariables,RankNTypes #-} +{-# LANGUAGE DataKinds,GADTs,TypeFamilies,ExistentialQuantification,ScopedTypeVariables,RankNTypes, LambdaCase #-} module Language.SMTLib2.Composite.Choice (Choice(..),ChoiceEncoding(..),RevChoice(..), -- * Encodings @@ -119,7 +119,7 @@ data RevChoice enc c t where RevChoiceElement :: {-# UNPACK #-} !Int -> !(RevComp c tp) -> RevChoice enc c tp instance (Composite c) => Composite (Choice enc c) where - type RevComp (Choice enc a) = RevChoice enc a + type RevComp (Choice enc c) = RevChoice enc c foldExprs f (ChoiceSingleton x) = do nx <- foldExprs (\rev -> f (RevChoiceElement 0 rev) ) x @@ -411,12 +411,13 @@ instance (Composite c,GShow e) => Show (Choice enc c e) where gshowsPrec 11 e instance CompositeExtract c => CompositeExtract (Choice enc c) where - type CompExtract (Choice enc a) = CompExtract a + type CompExtract (Choice enc c) = CompExtract c compExtract f (ChoiceSingleton x) = compExtract f x compExtract f (ChoiceBool lst) = do nlst <- mapM (\(v,cond) -> do - BoolValue res <- f cond - return (v,res) + f cond >>= \ case + BoolValue res -> + return (v,res) ) lst case [ v | (v,True) <- Vec.toList nlst ] of [] -> error "Choice: No value selected." diff --git a/extras/composite/Language/SMTLib2/Composite/Class.hs b/extras/composite/Language/SMTLib2/Composite/Class.hs index ec16a5b..de44832 100644 --- a/extras/composite/Language/SMTLib2/Composite/Class.hs +++ b/extras/composite/Language/SMTLib2/Composite/Class.hs @@ -1,9 +1,12 @@ +{-# language LambdaCase #-} + module Language.SMTLib2.Composite.Class where import Language.SMTLib2 import Language.SMTLib2.Internals.Embed import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Data.Proxy import Data.Functor.Identity @@ -162,3 +165,5 @@ defaultEq descr x y = do f <- lift false tell [f] return undefined + +unJust m = m >>= \ case Just x -> return x diff --git a/extras/composite/Language/SMTLib2/Composite/Container.hs b/extras/composite/Language/SMTLib2/Composite/Container.hs index 8eb0aea..6aa478b 100644 --- a/extras/composite/Language/SMTLib2/Composite/Container.hs +++ b/extras/composite/Language/SMTLib2/Composite/Container.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE PolyKinds, LambdaCase #-} + module Language.SMTLib2.Composite.Container ( -- * Container class Container(..), @@ -286,17 +287,19 @@ withMuxer' :: (Embed m e,Monad m) Muxed bs e -> st -> m (Muxed bs e,st)) -> m (a e,st) withMuxer' NoMux x st f = do - (NoMuxed,nst) <- f NilPaths [] NoMuxed st - return (x,nst) + f NilPaths [] NoMuxed st >>= \ case + (NoMuxed,nst) -> + return (x,nst) withMuxer' (Mux acc accs) x st f = case accessorHead acc of Nothing -> return (x,st) Just (path,cond,acc') -> do el <- pathGet path x (x1,(nel,nst)) <- withMuxer' accs x (el,st) $ \paths cond' muxed (el,st) -> do - (Muxed nel nmuxed,nst) <- f (Paths path paths) (cond++cond') - (Muxed el muxed) st - return (nmuxed,(nel,nst)) + f (Paths path paths) (cond++cond') + (Muxed el muxed) st >>= \ case + (Muxed nel nmuxed,nst) -> + return (nmuxed,(nel,nst)) x2 <- pathSet path x1 nel withMuxer' (Mux acc' accs) x2 nst f diff --git a/extras/composite/Language/SMTLib2/Composite/Domains.hs b/extras/composite/Language/SMTLib2/Composite/Domains.hs index 23a6014..f1b5f19 100644 --- a/extras/composite/Language/SMTLib2/Composite/Domains.hs +++ b/extras/composite/Language/SMTLib2/Composite/Domains.hs @@ -9,6 +9,7 @@ import Data.List (sortBy,sort) import Data.Ord (comparing) import Data.Functor.Identity import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Data.Foldable import Data.Maybe (catMaybes) @@ -257,7 +258,7 @@ byteReadITE ((r,c):rs) = do Just full1 -> case fullRead rest of Nothing -> return $ Just full1 Just full2 -> do - Just nfull <- compITE c full1 full2 + nfull <- unJust $ compITE c full1 full2 return $ Just nfull imprec <- maybeITE c (readImprecision r) (readImprecision rest) return $ ByteRead over outside full imprec @@ -269,7 +270,7 @@ byteReadITE ((r,c):rs) = do -> m (Map Integer (a e,e BoolType)) merge c notc x y = sequence $ Map.mergeWithKey (\_ (el1,c1) (el2,c2) -> Just $ do - Just nel <- compITE c el1 el2 + nel <- unJust $ compITE c el1 el2 cond <- c .&. (c1 .|. c2) return (nel,cond)) (fmap (\(el,c') -> do @@ -293,7 +294,7 @@ byteWriteITE ((w,c):ws) = do Just full1 -> case fullWrite rest of Nothing -> return $ Just full1 Just full2 -> do - Just nfull <- compITE c full1 full2 + nfull <- unJust $ compITE c full1 full2 return $ Just nfull imprec <- maybeITE c (writeImprecision w) (writeImprecision rest) return $ ByteWrite over outside full imprec @@ -307,7 +308,7 @@ byteWriteITE ((w,c):ws) = do merge c notc ((xrest,xcond):xs) ((yrest,ycond):ys) = case compCompare xrest yrest of EQ -> do - Just nrest <- compITE c xrest yrest + nrest <- unJust $ compITE c xrest yrest ncond <- (c .&. xcond) .|. (notc .&. ycond) ns <- merge c notc xs ys return $ (nrest,ncond):ns diff --git a/extras/composite/Language/SMTLib2/Composite/Either.hs b/extras/composite/Language/SMTLib2/Composite/Either.hs index 41cb6d3..cd802e6 100644 --- a/extras/composite/Language/SMTLib2/Composite/Either.hs +++ b/extras/composite/Language/SMTLib2/Composite/Either.hs @@ -6,6 +6,7 @@ import Language.SMTLib2.Composite.Container import Data.GADT.Show import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) newtype CompEither a b (e :: Type -> *) = CompEither { compEither :: Either (a e) (b e) } diff --git a/extras/composite/Language/SMTLib2/Composite/Expression.hs b/extras/composite/Language/SMTLib2/Composite/Expression.hs index 0aa2aa9..570a4a1 100644 --- a/extras/composite/Language/SMTLib2/Composite/Expression.hs +++ b/extras/composite/Language/SMTLib2/Composite/Expression.hs @@ -15,7 +15,8 @@ import Control.Monad.State import Control.Monad.Reader import Data.GADT.Compare as GComp import Data.GADT.Show -import Data.Dependent.Map (DMap,DSum(..)) +import Data.Dependent.Map (DMap) +import Data.Dependent.Sum (DSum(..)) import qualified Data.Dependent.Map as DMap import Data.Functor.Identity import Data.Proxy diff --git a/extras/composite/Language/SMTLib2/Composite/Linear.hs b/extras/composite/Language/SMTLib2/Composite/Linear.hs index 518037e..51b800e 100644 --- a/extras/composite/Language/SMTLib2/Composite/Linear.hs +++ b/extras/composite/Language/SMTLib2/Composite/Linear.hs @@ -1,3 +1,5 @@ +{-# language UndecidableInstances, LambdaCase #-} + module Language.SMTLib2.Composite.Linear where import Language.SMTLib2 @@ -27,11 +29,10 @@ delinear lin = do const' <- mapExprs constant (linConst lin) ps <- mapM (\(c,x) -> do c' <- mapExprs constant c - Just r <- compositeMult c' x + r <- unJust $ compositeMult c' x return r ) $ linear lin - Just res <- compositeSum $ const':ps - return res + unJust $ compositeSum (const':ps) delinearType :: (IsNumeric c,GetType e) => Linear c e -> c Repr delinearType lin = runIdentity $ delinear (compType lin) diff --git a/extras/composite/Language/SMTLib2/Composite/List.hs b/extras/composite/Language/SMTLib2/Composite/List.hs index c82c287..b2bd4bd 100644 --- a/extras/composite/Language/SMTLib2/Composite/List.hs +++ b/extras/composite/Language/SMTLib2/Composite/List.hs @@ -11,6 +11,7 @@ import Data.Vector (Vector) import qualified Data.Vector as Vec import Data.Maybe (catMaybes) import Data.GADT.Show +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Compare import Text.Show import Data.Foldable diff --git a/extras/composite/Language/SMTLib2/Composite/Map.hs b/extras/composite/Language/SMTLib2/Composite/Map.hs index c092487..2475e4b 100644 --- a/extras/composite/Language/SMTLib2/Composite/Map.hs +++ b/extras/composite/Language/SMTLib2/Composite/Map.hs @@ -8,6 +8,7 @@ import Language.SMTLib2.Composite.Null import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.GADT.Show +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Compare import Text.Show import Data.List (foldl') diff --git a/extras/composite/Language/SMTLib2/Composite/Singleton.hs b/extras/composite/Language/SMTLib2/Composite/Singleton.hs index a3ccb6d..cc277d3 100644 --- a/extras/composite/Language/SMTLib2/Composite/Singleton.hs +++ b/extras/composite/Language/SMTLib2/Composite/Singleton.hs @@ -1,3 +1,5 @@ +{-# language UndecidableInstances #-} + module Language.SMTLib2.Composite.Singleton where import Language.SMTLib2 @@ -9,6 +11,7 @@ import Language.SMTLib2.Composite.Domains import Language.SMTLib2.Composite.Null import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Data.Maybe import Data.Constraint diff --git a/extras/composite/Language/SMTLib2/Composite/Stack.hs b/extras/composite/Language/SMTLib2/Composite/Stack.hs index 2dff63a..49bceb5 100644 --- a/extras/composite/Language/SMTLib2/Composite/Stack.hs +++ b/extras/composite/Language/SMTLib2/Composite/Stack.hs @@ -12,6 +12,7 @@ import Language.SMTLib2.Composite.Convert import Language.SMTLib2.Internals.Embed import Data.GADT.Compare +import Data.Type.Equality ((:~:)) import Data.GADT.Show import Data.Monoid import qualified Data.Vector as Vec @@ -253,11 +254,11 @@ instance IsStack StackList StackListIndex where case cond++pushCond of [] -> return (i+1,el) [c] -> do - Just nel <- compITE c el (els Vec.! (i+1)) + nel <- unJust $ compITE c el (els Vec.! (i+1)) return (i+1,nel) cs -> do c <- and' cs - Just nel <- compITE c el (els Vec.! (i+1)) + nel <- unJust $ compITE c el (els Vec.! (i+1)) return (i+1,nel) ) existing let els1 = els Vec.// upd @@ -270,7 +271,7 @@ instance IsStack StackList StackListIndex where [] -> return top1 cs -> do c <- and' cs - Just res <- compITE c top1 top + res <- unJust $ compITE c top1 top return res return $ Stack (StackList (CompList els2)) (StackListIndex top2) stackPop popCond (Stack (StackList (CompList els)) (StackListIndex top)) = do @@ -284,7 +285,7 @@ instance IsStack StackList StackListIndex where [] -> return top1 cs -> do c <- and' cs - Just res <- compITE c top1 top + res <- unJust $ compITE c top1 top return res let nels = if null popCond then case find (\(NoComp i,cond) -> i==sz-1 && null cond) lst of @@ -326,7 +327,7 @@ instance (Num (Value tp)) => IsStack StackList (StackArrayIndex tp) where rc <- case pushCond of [] -> return c _ -> and' (c:pushCond) - Just nel <- compITE rc el cel + nel <- unJust $ compITE rc el cel return nel ) els topTp <- fmap (\tp -> tp top) $ embedTypeOf @@ -397,7 +398,7 @@ instance (Num (Value tp)) => IsStack (StackArray tp) (StackArrayIndex tp) where [] -> return Nothing [c] -> return $ Just c cs -> fmap Just $ and' cs - Just narr <- storeArrayCond rcond arr (top:::Nil) el + narr <- unJust $ storeArrayCond rcond arr (top:::Nil) el return $ Stack (StackArray narr) (StackArrayIndex (Comp ntop)) stackPop popCond (Stack arr (StackArrayIndex (Comp top))) = do topTp <- fmap (\tp -> tp top) $ embedTypeOf @@ -453,7 +454,7 @@ instance (Num (Value tp)) => IsStack (StackArray tp) StackListIndex where [] -> return top1 cs -> do c <- and' cs - Just res <- compITE c top1 top + res <- unJust $ compITE c top1 top return res ch <- getChoices top narr <- foldlM (\carr (NoComp i,cond) -> do @@ -462,7 +463,7 @@ instance (Num (Value tp)) => IsStack (StackArray tp) StackListIndex where [c] -> return $ Just c cs -> fmap Just $ and' cs ri <- constant $ fromIntegral $ i+1 - Just narr <- storeArrayCond rcond carr (ri:::Nil) el + narr <- unJust $ storeArrayCond rcond carr (ri:::Nil) el return narr ) arr ch return $ Stack (StackArray narr) (StackListIndex top2) @@ -475,7 +476,7 @@ instance (Num (Value tp)) => IsStack (StackArray tp) StackListIndex where [] -> return top1 cs -> do c <- and' cs - Just res <- compITE c top1 top + res <- unJust $ compITE c top1 top return res return $ Stack arr (StackListIndex top2) stackTop = return . _stackTop diff --git a/extras/composite/Language/SMTLib2/Composite/Tuple.hs b/extras/composite/Language/SMTLib2/Composite/Tuple.hs index c7ac3cc..f80f6a7 100644 --- a/extras/composite/Language/SMTLib2/Composite/Tuple.hs +++ b/extras/composite/Language/SMTLib2/Composite/Tuple.hs @@ -7,6 +7,7 @@ import Language.SMTLib2.Composite.Container import Data.GADT.Show import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.Proxy import qualified Data.Map as Map @@ -238,8 +239,7 @@ instance (ByteWidth a idx,ByteWidth b idx) => ByteWidth (CompTuple2 a b) idx whe byteWidth (CompTuple2 x y) r = do wx <- byteWidth x r wy <- byteWidth y r - Just r <- compositePlus wx wy - return r + unJust $ compositePlus wx wy instance (StaticByteWidth a,StaticByteAccess a el,StaticByteAccess b el,CanConcat el) => StaticByteAccess (CompTuple2 a b) el where @@ -289,7 +289,7 @@ instance (StaticByteWidth a,ByteAccess a idx el,ByteAccess b idx el,CanConcat el let wx = staticByteWidth x Just vwx = compositeFromInteger wx (compType idx) wx' <- mapExprs constant vwx - Just nidx <- compositeMinus idx wx' + nidx <- unJust $ compositeMinus idx wx' ry <- byteRead y nidx sz return [(ry,cond)] byteReadITE (reads1++reads2++reads3) @@ -323,10 +323,11 @@ instance (StaticByteWidth a,ByteAccess a idx el,ByteAccess b idx el,CanConcat el let szx = staticByteWidth x Just vszx = compositeFromInteger szx (compType idx) szx' <- mapExprs constant vszx - Just nidx <- compositeMinus idx szx' + nidx <- unJust $ compositeMinus idx szx' wy <- byteWrite y nidx el return [(wy { fullWrite = case fullWrite wy of Nothing -> Nothing Just y' -> Just $ CompTuple2 x y' },cond)] byteWriteITE (writes1++writes2++writes3) + diff --git a/extras/emulated-modulus/Language/SMTLib2/ModulusEmulator.hs b/extras/emulated-modulus/Language/SMTLib2/ModulusEmulator.hs index 94af7fc..b9cf8a8 100644 --- a/extras/emulated-modulus/Language/SMTLib2/ModulusEmulator.hs +++ b/extras/emulated-modulus/Language/SMTLib2/ModulusEmulator.hs @@ -12,6 +12,7 @@ import Language.SMTLib2.Internals.Type.List (List(..)) import Data.Foldable import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Data.GADT.Show import Data.Functor.Identity diff --git a/extras/quickcheck/Language/SMTLib2/QuickCheck.hs b/extras/quickcheck/Language/SMTLib2/QuickCheck.hs index 727add2..43e2547 100644 --- a/extras/quickcheck/Language/SMTLib2/QuickCheck.hs +++ b/extras/quickcheck/Language/SMTLib2/QuickCheck.hs @@ -8,7 +8,7 @@ import Language.SMTLib2.Internals.Type.List (List(..)) import qualified Language.SMTLib2.Internals.Type.List as List import Language.SMTLib2.Internals.Type.Nat -import Test.QuickCheck hiding (Args) +import Test.QuickCheck hiding (Args, Function, Fun) import Test.QuickCheck.Monadic import Data.Dependent.Map (DMap) import qualified Data.Dependent.Map as DMap @@ -18,6 +18,7 @@ import Data.Proxy import Data.Functor.Identity import Data.GADT.Show import Data.GADT.Compare +import Data.Type.Equality ((:~:)(Refl)) import Control.Monad.State.Strict import qualified GHC.TypeLits as TL diff --git a/smtlib2.cabal b/smtlib2.cabal index b167bac..bc3f2b2 100644 --- a/smtlib2.cabal +++ b/smtlib2.cabal @@ -18,8 +18,8 @@ Source-Repository head Library Build-Depends: base >= 4 && < 5, - constraints, mtl, containers, template-haskell, dependent-map, - dependent-sum>0.7, some + constraints, mtl, containers, template-haskell, + dependent-map, dependent-sum, some Extensions: GADTs FlexibleContexts diff --git a/stack.yaml b/stack.yaml index 74e2b69..cee697f 100644 --- a/stack.yaml +++ b/stack.yaml @@ -12,6 +12,7 @@ packages: extra-deps: - dependent-map-0.4.0.0 - dependent-sum-0.7.1.0 +- some-1.0.2 - constraints-extras-0.3.0.2 - cabal-test-quickcheck-0.1.8.2 - git: https://github.com/jwaldmann/atto-lisp