-
Notifications
You must be signed in to change notification settings - Fork 3
/
List.hs
67 lines (61 loc) · 2.28 KB
/
List.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
{-# LANGUAGE FlexibleContexts #-}
-- |
-- Module : Grisette.Lib.Data.List
-- Copyright : (c) Sirui Lu 2021-2023
-- License : BSD-3-Clause (see the LICENSE file)
--
-- Maintainer : siruilu@cs.washington.edu
-- Stability : Experimental
-- Portability : GHC only
module Grisette.Lib.Data.List
( -- * Symbolic versions of 'Data.List' operations
(.!!),
symFilter,
symTake,
symDrop,
)
where
import Control.Exception (ArrayException (IndexOutOfBounds))
import Control.Monad.Except (MonadError (throwError))
import Grisette.Core.Control.Monad.Union (MonadUnion)
import Grisette.Core.Data.Class.Error (TransformError (transformError))
import Grisette.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Core.Data.Class.SEq (SEq ((.==)))
import Grisette.Core.Data.Class.SOrd (SOrd ((.<=)))
import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)
import Grisette.IR.SymPrim.Data.SymPrim (SymBool, SymInteger)
import Grisette.Lib.Control.Monad (mrgFmap, mrgReturn)
-- | Symbolic version of 'Data.List.!!', the result would be merged and
-- propagate the mergeable knowledge.
(.!!) ::
( MonadUnion uf,
MonadError e uf,
TransformError ArrayException e,
Mergeable a
) =>
[a] ->
SymInteger ->
uf a
l .!! p = go l p 0
where
go [] _ _ = throwError $ transformError (IndexOutOfBounds "!!~")
go (x : xs) p1 i = mrgIf (p1 .== i) (mrgReturn x) (go xs p1 $ i + 1)
-- | Symbolic version of 'Data.List.filter', the result would be merged and
-- propagate the mergeable knowledge.
symFilter :: (MonadUnion u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]
symFilter f = go
where
go [] = mrgReturn []
go (x : xs) = do
r <- go xs
mrgIf (f x) (mrgReturn (x : r)) (mrgReturn r)
-- | Symbolic version of 'Data.List.take', the result would be merged and
-- propagate the mergeable knowledge.
symTake :: (MonadUnion u, Mergeable a) => SymInteger -> [a] -> u [a]
symTake _ [] = mrgReturn []
symTake x (v : vs) = mrgIf (x .<= 0) (mrgReturn []) (mrgFmap (v :) $ symTake (x - 1) vs)
-- | Symbolic version of 'Data.List.drop', the result would be merged and
-- propagate the mergeable knowledge.
symDrop :: (MonadUnion u, Mergeable a) => SymInteger -> [a] -> u [a]
symDrop _ [] = mrgReturn []
symDrop x r@(_ : vs) = mrgIf (x .<= 0) (mrgReturn r) (symDrop (x - 1) vs)