never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Function.Function1DPartial ( function1DPartial ) where
4
5 -- conjure
6 import Conjure.Prelude
7 import Conjure.Language
8 import Conjure.Language.ZeroVal ( zeroVal, EnumerateDomain )
9 import Conjure.Representations.Internal
10 import Conjure.Representations.Common
11 import Conjure.Representations.Function.Function1D ( domainValues )
12
13 -- unordered-containers
14 import qualified Data.HashMap.Strict as M
15
16
17 function1DPartial :: forall m . (MonadFailDoc m, NameGen m, EnumerateDomain m) => Representation m
18 function1DPartial = Representation chck downD structuralCons downC up symmetryOrdering
19
20 where
21
22 chck :: TypeOf_ReprCheck m
23 chck f (DomainFunction _
24 attrs@(FunctionAttr _ PartialityAttr_Partial _)
25 innerDomainFr
26 innerDomainTo) | domainCanIndexMatrix innerDomainFr = do
27 innerDomainFr' <- f innerDomainFr
28 innerDomainTo' <- f innerDomainTo
29 return [ DomainFunction Function_1DPartial attrs fr to
30 | fr <- innerDomainFr'
31 , to <- innerDomainTo'
32 ]
33 chck _ _ = return []
34
35 nameFlags = mkOutName (Just "Flags")
36 nameValues = mkOutName (Just "Values")
37
38 downD :: TypeOf_DownD m
39 downD (name, domain@(DomainFunction Function_1DPartial
40 (FunctionAttr _ PartialityAttr_Partial _)
41 innerDomainFr
42 innerDomainTo)) | domainCanIndexMatrix innerDomainFr = return $ Just
43 [ ( nameFlags domain name
44 , DomainMatrix
45 (forgetRepr innerDomainFr)
46 DomainBool
47 )
48 , ( nameValues domain name
49 , DomainMatrix
50 (forgetRepr innerDomainFr)
51 innerDomainTo
52 )
53 ]
54 downD _ = na "{downD} Function1DPartial"
55
56 structuralCons :: TypeOf_Structural m
57 structuralCons f downX1
58 (DomainFunction Function_1DPartial
59 (FunctionAttr sizeAttr PartialityAttr_Partial jectivityAttr)
60 innerDomainFr
61 innerDomainTo) | domainCanIndexMatrix innerDomainFr = do
62
63 let injectiveCons flags values = do
64 (iPat, i) <- quantifiedVar
65 (jPat, j) <- quantifiedVar
66 return $ return $ -- list
67 [essence|
68 and([ &values[&i] != &values[&j]
69 | &iPat : &innerDomainFr
70 , &jPat : &innerDomainFr
71 , &i .< &j
72 , &flags[&i]
73 , &flags[&j]
74 ])
75 |]
76
77 let surjectiveCons flags values = do
78 (iPat, i) <- quantifiedVar
79 (jPat, j) <- quantifiedVar
80 return $ return $ -- list
81 [essence|
82 forAll &iPat : &innerDomainTo .
83 exists &jPat : &innerDomainFr .
84 &flags[&j] /\ &values[&j] = &i
85 |]
86
87 let jectivityCons flags values = case jectivityAttr of
88 JectivityAttr_None -> return []
89 JectivityAttr_Injective -> injectiveCons flags values
90 JectivityAttr_Surjective -> surjectiveCons flags values
91 JectivityAttr_Bijective -> (++) <$> injectiveCons flags values
92 <*> surjectiveCons flags values
93
94 let cardinality flags = do
95 (iPat, i) <- quantifiedVar
96 return [essence| sum &iPat : &innerDomainFr . toInt(&flags[&i]) |]
97
98 let dontCareInactives flags values = do
99 (iPat, i) <- quantifiedVar
100 return $ return $ -- list
101 [essence|
102 forAll &iPat : &innerDomainFr . &flags[&i] = false ->
103 dontCare(&values[&i])
104 |]
105
106 let innerStructuralCons flags values = do
107 (iPat, i) <- quantifiedVarOverDomain (forgetRepr innerDomainFr)
108 let activeZone b = [essence| forAll &iPat : &innerDomainFr . &flags[&i] -> &b |]
109
110 -- preparing structural constraints for the inner guys
111 innerStructuralConsGen <- f innerDomainTo
112
113 let inLoop = [essence| &values[&i] |]
114 outs <- innerStructuralConsGen inLoop
115 return (map activeZone outs)
116
117 return $ \ func -> do
118 refs <- downX1 func
119 case refs of
120 [flags,values] ->
121 concat <$> sequence
122 [ jectivityCons flags values
123 , dontCareInactives flags values
124 , mkSizeCons sizeAttr <$> cardinality flags
125 , innerStructuralCons flags values
126 ]
127 _ -> na "{structuralCons} Function1DPartial"
128
129 structuralCons _ _ _ = na "{structuralCons} Function1DPartial"
130
131 downC :: TypeOf_DownC m
132 downC ( name
133 , domain@(DomainFunction Function_1DPartial
134 (FunctionAttr _ PartialityAttr_Partial _)
135 innerDomainFr
136 innerDomainTo)
137 , viewConstantFunction -> Just vals_
138 ) | domainCanIndexMatrix innerDomainFr = do
139 let vals = M.fromList vals_
140 z <- zeroVal innerDomainTo
141 froms <- domainValues innerDomainFr
142 (flagsOut, valsOut) <- unzip <$> sequence
143 [ val
144 | fr <- froms
145 , let val = case M.lookup fr vals of
146 Nothing -> return (ConstantBool False, z)
147 Just v -> return (ConstantBool True , v)
148 ]
149 return $ Just
150 [ ( nameFlags domain name
151 , DomainMatrix
152 (forgetRepr innerDomainFr)
153 DomainBool
154 , ConstantAbstract $ AbsLitMatrix
155 (forgetRepr innerDomainFr)
156 flagsOut
157 )
158 , ( nameValues domain name
159 , DomainMatrix
160 (forgetRepr innerDomainFr)
161 innerDomainTo
162 , ConstantAbstract $ AbsLitMatrix
163 (forgetRepr innerDomainFr)
164 valsOut
165 )
166 ]
167 downC (name, domain, constant) = na $ vcat [ "{downC} Function1DPartial"
168 , "name:" <+> pretty name
169 , "domain:" <+> pretty domain
170 , "constant:" <+> pretty constant
171 ]
172
173 up :: TypeOf_Up m
174 up ctxt (name, domain@(DomainFunction Function_1DPartial
175 (FunctionAttr _ PartialityAttr_Partial _)
176 innerDomainFr _)) =
177 case (lookup (nameFlags domain name) ctxt, lookup (nameValues domain name) ctxt) of
178 ( Just (ConstantAbstract (AbsLitMatrix _ flagMatrix)) ,
179 Just (ConstantAbstract (AbsLitMatrix _ valuesMatrix)) ) -> do
180 froms <- domainValues innerDomainFr
181 functionValues <- forM (zip3 flagMatrix froms valuesMatrix) $ \ (flag, from, to) ->
182 case viewConstantBool flag of
183 Just b -> return $ if b then Just (from,to) else Nothing
184 Nothing -> failDoc $ vcat [ "Expected a boolean, but got:" <++> pretty flag
185 , "When working on:" <+> pretty name
186 , "With domain:" <+> pretty domain
187 ]
188 return ( name, ConstantAbstract $ AbsLitFunction $ catMaybes functionValues )
189 (Nothing, _) -> failDoc $ vcat $
190 [ "(in Function1DPartial up 1)"
191 , "No value for:" <+> pretty (nameFlags domain name)
192 , "When working on:" <+> pretty name
193 , "With domain:" <+> pretty domain
194 ] ++
195 ("Bindings in context:" : prettyContext ctxt)
196 (_, Nothing) -> failDoc $ vcat $
197 [ "(in Function1DPartial up 2)"
198 , "No value for:" <+> pretty (nameValues domain name)
199 , "When working on:" <+> pretty name
200 , "With domain:" <+> pretty domain
201 ] ++
202 ("Bindings in context:" : prettyContext ctxt)
203 _ -> failDoc $ vcat $
204 [ "Expected matrix literals for:" <+> pretty (nameFlags domain name)
205 <+> "and" <+> pretty (nameValues domain name)
206 , "When working on:" <+> pretty name
207 , "With domain:" <+> pretty domain
208 ] ++
209 ("Bindings in context:" : prettyContext ctxt)
210 up _ _ = na "{up} Function1DPartial"
211
212 symmetryOrdering :: TypeOf_SymmetryOrdering m
213 symmetryOrdering innerSO downX1 inp domain = do
214 [flags, values] <- downX1 inp
215 Just [_, (_, DomainMatrix innerDomainFr innerDomainTo)] <- downD ("SO", domain)
216 (iPat, i) <- quantifiedVar
217 soValues <- innerSO downX1 [essence| &values[&i] |] innerDomainTo
218 return
219 [essence|
220 [ ( -toInt(&flags[&i])
221 , &soValues
222 )
223 | &iPat : &innerDomainFr
224 ]
225 |]
226