-
Notifications
You must be signed in to change notification settings - Fork 0
/
Gen.hs
69 lines (62 loc) · 2.24 KB
/
Gen.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
68
69
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE BangPatterns #-}
module Language.BV.Gen where
import Data.Map (Map)
import qualified Data.Map as Map
import Language.BV.Types
import Language.BV.Util
import Language.BV.Simplifier (isNotRedundant)
type State = Map Int [BVExpr]
genExpr :: [String] -> Int -> [BVExpr]
genExpr !ops size = concat $ Map.elems r3 where
BVOpTags { .. } = opTagsFromList ops
(_r1, _r2, r3) = go size undefined
-- 1 -> exprs without fold with x, y, z ids
-- 2 -> exprs without fold with x ids
-- 3 -> exprs with fold with x ids
go :: Int -> (State, State, State) -> (State, State, State)
go 1 _states =
(Map.singleton 1 [Zero, One, Id 'x', Id 'y', Id 'z'],
Map.singleton 1 [Zero, One, Id 'x'],
Map.singleton 1 [Zero, One, Id 'x'])
go !i states =
let (!s1, !s2, !s3) = go (pred i) states
go0 m = filter (isNotRedundant ops) $ concat [op1s, op2s, ifs] where
op1s = [ Op1 op1 x
| op1 <- bvOp1s
, x <- m Map.! pred i
]
op2s = [ Op2 op2 x y
| op2 <- bvOp2s
, (j, k) <- partitions2 (pred i)
, x <- m Map.! j
, y <- m Map.! k
]
ifs = [ if_ x y z
| if_ <- bvIfs
, (j, k, l) <- partitions3 (pred i)
, x <- m Map.! j
, y <- m Map.! k
, z <- m Map.! l
]
go1 = go0 s1
go2 = go0 s2
go3 = filter (isNotRedundant ops) $
go0 s3 ++
[ f e1 e2 e3
| f <- bvFolds
, (j, k, l) <- partitions3 (i - 2)
, e1 <- s1 Map.! j
, e2 <- s2 Map.! k
, e3 <- s2 Map.! l
] ++
[ f e1 e2
| f <- bvTFolds
, (j, k) <- partitions2 (i - 3)
, e1 <- s1 Map.! j
, e2 <- s2 Map.! k
]
in (Map.insert i go1 s1,
Map.insert i go2 s2,
Map.insert i go3 s3)
{-# INLINE genExpr #-}