never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Function.Function1D
4 ( function1D
5 , domainValues
6 ) where
7
8 -- conjure
9 import Conjure.Prelude
10 import Conjure.Language.Definition
11 import Conjure.Language.Domain
12 import Conjure.Language.Type
13 import Conjure.Language.Constant
14 import Conjure.Language.DomainSizeOf
15 import Conjure.Language.Expression.DomainSizeOf ()
16 import Conjure.Language.TH
17 import Conjure.Language.Pretty
18 import Conjure.Representations.Internal
19 import Conjure.Representations.Common
20
21 -- unordered-containers
22 import qualified Data.HashMap.Strict as M
23
24
25 function1D :: forall m . (MonadFailDoc m, NameGen m, ?typeCheckerMode :: TypeCheckerMode) => Representation m
26 function1D = Representation chck downD structuralCons downC up symmetryOrdering
27
28 where
29
30 chck :: TypeOf_ReprCheck m
31 chck f (DomainFunction _
32 attrs@(FunctionAttr _ PartialityAttr_Total _)
33 innerDomainFr
34 innerDomainTo) | domainCanIndexMatrix innerDomainFr = do
35 innerDomainFr' <- f innerDomainFr
36 innerDomainTo' <- f innerDomainTo
37 return [ DomainFunction Function_1D attrs fr to
38 | fr <- innerDomainFr'
39 , to <- innerDomainTo'
40 ]
41 chck _ _ = return []
42
43 outName :: Domain HasRepresentation x -> Name -> Name
44 outName = mkOutName Nothing
45
46 downD :: TypeOf_DownD m
47 downD (name, domain@(DomainFunction Function_1D
48 (FunctionAttr _ PartialityAttr_Total _)
49 innerDomainFr
50 innerDomainTo)) | domainCanIndexMatrix innerDomainFr = return $ Just
51 [ ( outName domain name
52 , DomainMatrix
53 (forgetRepr innerDomainFr)
54 innerDomainTo
55 ) ]
56 downD _ = na "{downD} Function1D"
57
58 structuralCons :: TypeOf_Structural m
59 structuralCons f downX1
60 (DomainFunction Function_1D
61 (FunctionAttr sizeAttr PartialityAttr_Total jectivityAttr)
62 innerDomainFr
63 innerDomainTo) | domainCanIndexMatrix innerDomainFr = do
64
65 let
66 injectiveCons :: Expression -> m [Expression]
67 injectiveCons m = do
68 tyTo <- typeOfDomain innerDomainTo
69 let canAllDiff = case tyTo of
70 TypeBool{} -> True
71 TypeInt{} -> True
72 TypeEnum{} -> True
73 _ -> False
74 if canAllDiff
75 then
76 return $ return $ -- list
77 [essence| allDiff(&m) |]
78 else do
79 (iPat, i) <- quantifiedVar
80 (jPat, j) <- quantifiedVar
81 return $ return $ -- list
82 [essence|
83 forAll &iPat, &jPat : &innerDomainFr .
84 &i .< &j -> &m[&i] != &m[&j]
85 |]
86
87 surjectiveCons :: Expression -> m [Expression]
88 surjectiveCons m = do
89 (iPat, i) <- quantifiedVar
90 (jPat, j) <- quantifiedVar
91 return $ return $ -- list
92 [essence|
93 forAll &iPat : &innerDomainTo .
94 exists &jPat : &innerDomainFr .
95 &m[&j] = &i
96 |]
97
98 jectivityCons :: Expression -> m [Expression]
99 jectivityCons m = case jectivityAttr of
100 JectivityAttr_None -> return []
101 JectivityAttr_Injective -> injectiveCons m
102 JectivityAttr_Surjective -> surjectiveCons m
103 JectivityAttr_Bijective -> (++) <$> injectiveCons m <*> surjectiveCons m
104
105 cardinality <- domainSizeOf innerDomainFr
106
107 let innerStructuralCons m = do
108 (iPat, i) <- quantifiedVarOverDomain (forgetRepr innerDomainFr)
109 let activeZone b = [essence| forAll &iPat : &innerDomainFr . &b |]
110
111 -- preparing structural constraints for the inner guys
112 innerStructuralConsGen <- f innerDomainTo
113
114 let inLoop = [essence| &m[&i] |]
115 outs <- innerStructuralConsGen inLoop
116 return (map activeZone outs)
117
118 return $ \ func -> do
119 refs <- downX1 func
120 case refs of
121 [m] ->
122 concat <$> sequence
123 [ jectivityCons m
124 , return (mkSizeCons sizeAttr cardinality)
125 , innerStructuralCons m
126 ]
127 _ -> na "{structuralCons} Function1D"
128
129 structuralCons _ _ _ = na "{structuralCons} Function1D"
130
131 downC :: TypeOf_DownC m
132 downC ( name
133 , domain@(DomainFunction Function_1D
134 (FunctionAttr _ PartialityAttr_Total _)
135 innerDomainFr
136 innerDomainTo)
137 , viewConstantFunction -> Just vals_
138 ) | domainCanIndexMatrix innerDomainFr = do
139 let vals = M.fromList vals_
140 froms <- domainValues innerDomainFr
141 valsOut <- sequence
142 [ val
143 | fr <- froms
144 , let val = case M.lookup fr vals of
145 Nothing -> failDoc $ vcat [ "No value for" <+> pretty fr
146 , "In:" <+> pretty (AbsLitFunction vals_)
147 ]
148 Just v -> return v
149 ]
150 return $ Just
151 [ ( outName domain name
152 , DomainMatrix (forgetRepr innerDomainFr) innerDomainTo
153 , ConstantAbstract $ AbsLitMatrix (forgetRepr innerDomainFr) valsOut
154 ) ]
155 downC _ = na "{downC} Function1D"
156
157 up :: TypeOf_Up m
158 up ctxt (name, domain@(DomainFunction Function_1D
159 (FunctionAttr _ PartialityAttr_Total _)
160 innerDomainFr _)) =
161 case lookup (outName domain name) ctxt of
162 Nothing -> failDoc $ vcat $
163 [ "(in Function1D up)"
164 , "No value for:" <+> pretty (outName domain name)
165 , "When working on:" <+> pretty name
166 , "With domain:" <+> pretty domain
167 ] ++
168 ("Bindings in context:" : prettyContext ctxt)
169 Just constant ->
170 case viewConstantMatrix constant of
171 Just (_, vals) -> do
172 froms <- domainValues innerDomainFr
173 return ( name
174 , ConstantAbstract $ AbsLitFunction $ zip froms vals
175 )
176 _ -> failDoc $ vcat
177 [ "Expecting a matrix literal for:" <+> pretty (outName domain name)
178 , "But got:" <+> pretty constant
179 , "When working on:" <+> pretty name
180 , "With domain:" <+> pretty domain
181 ]
182 up _ _ = na "{up} Function1D"
183
184 symmetryOrdering :: TypeOf_SymmetryOrdering m
185 symmetryOrdering innerSO downX1 inp domain = do
186 [inner] <- downX1 inp
187 Just [(_, innerDomain)] <- downD ("SO", domain)
188 innerSO downX1 inner innerDomain
189
190
191
192 domainValues :: (MonadFailDoc m, Pretty r) => Domain r Constant -> m [Constant]
193 domainValues dom =
194 case dom of
195 DomainBool -> return [ConstantBool False, ConstantBool True]
196 DomainInt t rs -> map (ConstantInt t) <$> valuesInIntDomain rs
197 _ -> failDoc ("domainValues, not supported:" <+> pretty dom)
198