for hgoes#19

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
 

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)

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

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
 

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
 

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

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
 

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)
 

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

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."

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

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
 

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

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) }
 

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

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)

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

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')

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

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