never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
3 {-# HLINT ignore "Use camelCase" #-}
4
5 module Conjure.Rules.DontCare where
6
7 import Conjure.Rules.Import
8 import Conjure.Process.Enumerate ( EnumerateDomain )
9
10
11 rule_Bool :: Rule
12 rule_Bool = "dontCare-bool" `namedRule` theRule where
13 theRule p = do
14 x <- match opDontCare p
15 DomainBool <- domainOf x
16 return
17 ( "dontCare value for bools is false."
18 , return $ make opEq x (fromBool False)
19 )
20
21
22 rule_Int :: Rule
23 rule_Int = "dontCare-int" `namedRule` theRule where
24 theRule p = do
25 x <- match opDontCare p
26 xDomain <- domainOf x
27 val <- minOfDomain xDomain
28 return
29 ( "dontCare value for this integer is" <+> pretty val
30 , return $ make opEq x val
31 )
32
33
34 rule_Unnamed :: Rule
35 rule_Unnamed = "dontCare-unnamed" `namedRule` theRule where
36 theRule p = do
37 x <- match opDontCare p
38 ty <- typeOf x
39 case ty of
40 TypeInt (TagUnnamed _) -> return ()
41 _ -> na "rule_Unnamed"
42 return
43 ( "dontCare value for this unnamed integer is 1"
44 , return $ make opEq x 1
45 )
46
47
48 rule_Tuple :: Rule
49 rule_Tuple = "dontCare-tuple" `namedRule` theRule where
50 theRule p = do
51 x <- match opDontCare p
52 TypeTuple{} <- typeOf x
53 xs <- downX1 x
54 return
55 ( "dontCare handling for tuple"
56 , return $ make opAnd $ fromList $ map (make opDontCare) xs
57 )
58
59
60 rule_Record :: Rule
61 rule_Record = "dontCare-record" `namedRule` theRule where
62 theRule p = do
63 x <- match opDontCare p
64 TypeRecord{} <- typeOf x
65 xs <- downX1 x
66 return
67 ( "dontCare handling for record"
68 , return $ make opAnd $ fromList $ map (make opDontCare) xs
69 )
70
71
72 rule_Variant :: Rule
73 rule_Variant = "dontCare-variant" `namedRule` theRule where
74 theRule p = do
75 x <- match opDontCare p
76 TypeVariant{} <- typeOf x
77 xs <- downX1 x
78 return
79 ( "dontCare handling for variant"
80 , return $ make opAnd $ fromList $ map (make opDontCare) xs
81 )
82
83
84 rule_Matrix :: Rule
85 rule_Matrix = "dontCare-matrix" `namedRule` theRule where
86 theRule p = do
87 x <- match opDontCare p
88 indices <- indexDomainsOf x
89 when (null indices) $ na "rule_Matrix"
90 return
91 ( "dontCare handling for matrix"
92 , do
93 triplets <- forM indices $ \ index -> do
94 (iPat, i) <- quantifiedVar
95 return (iPat, i, index)
96 let gens = [Generator (GenDomainNoRepr iPat index) | (iPat, _, index) <- triplets]
97 return $ make opAnd $ Comprehension (make opDontCare (make opMatrixIndexing x [i | (_, i, _) <- triplets])) gens
98 )
99
100 rule_Permutation :: Rule
101 rule_Permutation = "dontCare-permutation" `namedRule` theRule where
102 theRule p = do
103 x <- match opDontCare p
104 DomainPermutation _ _ inner <- domainOf x
105 return
106 ( "dontCare handling for permutation"
107 , do
108 (iPat, i) <- quantifiedVar
109 return [essence| forAll &iPat : &inner . image(&x,&i) = &i |]
110 )
111
112
113
114 rule_Abstract :: Rule
115 rule_Abstract = "dontCare-abstract" `namedRule` theRule where
116 theRule p = do
117 x <- match opDontCare p
118 ty <- typeOf x
119 case ty of
120 TypeSet {} -> return ()
121 TypeMSet {} -> return ()
122 TypeSequence {} -> return ()
123 TypeFunction {} -> return ()
124 TypeRelation {} -> return ()
125 TypePartition{} -> return ()
126 _ -> na "not a known abstract domain"
127 hasRepresentation x
128 xs <- downX1 x
129 return
130 ( "dontCare handling for an abstract domain"
131 , return $ make opAnd $ fromList $ map (make opDontCare) xs
132 )
133
134
135 handleDontCares ::
136 MonadFailDoc m =>
137 NameGen m =>
138 EnumerateDomain m =>
139 (?typeCheckerMode :: TypeCheckerMode) =>
140 Expression -> m Expression
141 handleDontCares p =
142 case match opDontCare p of
143 Nothing -> return p
144 Just x -> do
145 typX <- typeOf x
146 case typX of
147 TypeBool -> return (make opEq x (fromBool False))
148 TypeInt _ -> do
149 domX <- domainOf x
150 let raiseBug = bug ("dontCare on domain:" <+> pretty domX)
151 let val = case domX of
152 DomainInt _ [] -> raiseBug
153 DomainInt _ (r:_) -> case r of
154 RangeOpen -> raiseBug
155 RangeSingle v -> v
156 RangeLowerBounded v -> v
157 RangeUpperBounded v -> v
158 RangeBounded v _ -> v
159 DomainIntE _ v -> [essence| min(&v) |]
160 _ -> raiseBug
161 return $ make opEq x val
162 TypeTuple{} -> do
163 xs <- downX1 x
164 xs' <- mapM (handleDontCares . make opDontCare) xs
165 return $ make opAnd $ fromList xs'
166 TypeRecord{} -> do
167 xs <- downX1 x
168 xs' <- mapM (handleDontCares . make opDontCare) xs
169 return $ make opAnd $ fromList xs'
170 TypeVariant{} -> do
171 xs <- downX1 x
172 xs' <- mapM (handleDontCares . make opDontCare) xs
173 return $ make opAnd $ fromList xs'
174 TypeMatrix{} -> do
175 domX <- domainOf x
176 case domX of
177 DomainMatrix index _ -> do
178 (iPat@(Single nm), _) <- quantifiedVar
179 -- direct name resolution
180 let i = Reference nm (Just (DeclNoRepr Find nm index NoRegion))
181 inner <- handleDontCares [essence| dontCare(&x[&i]) |]
182 return [essence| forAll &iPat : &index . &inner |]
183 _ -> bug ("dontCare on domain, expecting matrix, but got:" <+> pretty domX)
184 _ -> do
185 case representationOf x of
186 Nothing -> failDoc "doesn't seem to have a representation, during handleDontCares"
187 Just _ -> do
188 xs <- downX1 x
189 xs' <- mapM (handleDontCares . make opDontCare) xs
190 return $ make opAnd $ fromList xs'
191