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