never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2 {-# LANGUAGE Rank2Types #-}
3
4 module Conjure.Representations.Function.FunctionAsRelation ( functionAsRelation ) where
5
6 -- conjure
7 import Conjure.Prelude
8 import Conjure.Language.Definition
9 import Conjure.Language.Domain
10 import Conjure.Language.Constant
11 import Conjure.Language.TH
12 import Conjure.Language.Pretty
13 import Conjure.Representations.Internal
14
15
16 functionAsRelation
17 :: forall m . (MonadFailDoc m, NameGen m)
18 => (forall x . DispatchFunction m x)
19 -> (forall r x . ReprOptionsFunction m r x)
20 -> Representation m
21 functionAsRelation dispatch reprOptions = Representation chck downD structuralCons downC up symmetryOrdering
22
23 where
24
25 chck :: TypeOf_ReprCheck m
26 chck _ dom1@(DomainFunction _ attrs _ _) = do
27 dom2 <- outDomain_ dom1
28 dom3 <- reprOptions dom2
29 return [ DomainFunction (Function_AsRelation r) attrs innerDomainFr innerDomainTo
30 | DomainRelation r _ [innerDomainFr, innerDomainTo] <- dom3
31 ]
32 chck _ _ = return []
33
34 outName :: Domain HasRepresentation x -> Name -> Name
35 outName = mkOutName Nothing
36
37 outDomain_ :: Pretty x => Domain () x -> m (Domain () x)
38 outDomain_ (DomainFunction ()
39 (FunctionAttr sizeAttr _partilityAttr _jectivityAttr)
40 innerDomainFr innerDomainTo) =
41 return (DomainRelation () (RelationAttr sizeAttr def) [innerDomainFr, innerDomainTo])
42 outDomain_ domain = na $ vcat [ "{outDomain_} FunctionAsRelation"
43 , "domain:" <+> pretty domain
44 ]
45
46 outDomain :: Pretty x => Domain HasRepresentation x -> m (Domain HasRepresentation x)
47 outDomain (DomainFunction (Function_AsRelation repr)
48 (FunctionAttr sizeAttr _partilityAttr _jectivityAttr)
49 innerDomainFr innerDomainTo) =
50 return (DomainRelation repr (RelationAttr sizeAttr def) [innerDomainFr, innerDomainTo])
51 outDomain domain = na $ vcat [ "{outDomain} FunctionAsRelation"
52 , "domain:" <+> pretty domain
53 ]
54
55 downD :: TypeOf_DownD m
56 downD (name, inDom) = do
57 outDom <- outDomain inDom
58 return $ Just [ ( outName inDom name , outDom ) ]
59
60 structuralCons :: TypeOf_Structural m
61 structuralCons f downX1
62 inDom@(DomainFunction _
63 (FunctionAttr _ partilityAttr jectivityAttr)
64 innerDomainFr innerDomainTo) = return $ \ func -> do
65 refs <- downX1 func
66 let
67 partialityCons rel =
68 case partilityAttr of
69 PartialityAttr_Partial -> do
70 (iPat, i) <- quantifiedVar
71 (jPat, j) <- quantifiedVar
72 return $ return $ -- list
73 [essence|
74 $ enforcing that it is indeed a function
75 forAll {&iPat, &jPat} subsetEq toSet(&rel) .
76 &i[1] != &j[1]
77 |]
78 PartialityAttr_Total -> do
79 (iPat, i) <- quantifiedVar
80 (jPat, j) <- quantifiedVar
81 return $ return $ -- list
82 [essence|
83 forAll &iPat : &innerDomainFr .
84 1 = sum([ 1
85 | &jPat <- &rel
86 , &j[1] = &i
87 ])
88 |]
89
90 jectivityCons rel = case jectivityAttr of
91 JectivityAttr_None -> return []
92 JectivityAttr_Injective -> injectiveCons rel
93 JectivityAttr_Surjective -> surjectiveCons rel
94 JectivityAttr_Bijective -> (++) <$> injectiveCons rel <*> surjectiveCons rel
95
96 injectiveCons rel = do
97 (iPat, i) <- quantifiedVar
98 (jPat, j) <- quantifiedVar
99 return $ return $ -- list
100 [essence|
101 and([ &i[1] .< &j[1] -> &i[2] != &j[2]
102 | &iPat <- &rel
103 , &jPat <- &rel
104 ])
105 |]
106
107 surjectiveCons rel = do
108 (iPat, i) <- quantifiedVar
109 (jPat, j) <- quantifiedVar
110 return $ return $ -- list
111 [essence|
112 forAll &iPat : &innerDomainTo .
113 exists &jPat in &rel .
114 &j[2] = &i
115 |]
116
117 case refs of
118 [rel] -> do
119 outDom <- outDomain inDom
120 innerStructuralConsGen <- f outDom
121 concat <$> sequence
122 [ innerStructuralConsGen rel
123 , partialityCons rel
124 , jectivityCons rel
125 ]
126 _ -> na $ vcat [ "{structuralCons} FunctionAsRelation"
127 , pretty inDom
128 ]
129 structuralCons _ _ inDom =
130 na $ vcat [ "{structuralCons} FunctionAsRelation"
131 , pretty inDom
132 ]
133
134 downC :: TypeOf_DownC m
135 downC ( name
136 , inDom
137 , viewConstantFunction -> Just vals
138 ) = do
139 outDom <- outDomain inDom
140 rDownC
141 (dispatch outDom)
142 ( outName inDom name
143 , outDom
144 , ConstantAbstract $ AbsLitRelation $ map (\ (a,b) -> [a,b] ) vals
145 )
146 downC (name, domain, constant) = na $ vcat [ "{downC} FunctionAsRelation"
147 , "name:" <+> pretty name
148 , "domain:" <+> pretty domain
149 , "constant:" <+> pretty constant
150 ]
151
152 up :: TypeOf_Up m
153 up ctxt (name, domain@(DomainFunction Function_AsRelation{} _ _ _)) =
154 case lookup (outName domain name) ctxt of
155 Just (viewConstantRelation -> Just pairs) -> do
156 let pairOut [a,b] = return (a,b)
157 pairOut c = failDoc $ "Expecting a 2-tuple, but got:" <++> prettyList prParens "," c
158 vals <- mapM pairOut pairs
159 return (name, ConstantAbstract (AbsLitFunction vals))
160 Nothing -> failDoc $ vcat $
161 [ "(in FunctionAsRelation up)"
162 , "No value for:" <+> pretty (outName domain name)
163 , "When working on:" <+> pretty name
164 , "With domain:" <+> pretty domain
165 ] ++
166 ("Bindings in context:" : prettyContext ctxt)
167 Just constant -> failDoc $ vcat $
168 [ "Incompatible value for:" <+> pretty (outName domain name)
169 , "When working on:" <+> pretty name
170 , "With domain:" <+> pretty domain
171 , "Expected a set value, but got:" <++> pretty constant
172 ] ++
173 ("Bindings in context:" : prettyContext ctxt)
174 up _ (name, domain) = na $ vcat [ "{up} FunctionAsRelation"
175 , "name:" <+> pretty name
176 , "domain:" <+> pretty domain
177 ]
178
179 symmetryOrdering :: TypeOf_SymmetryOrdering m
180 symmetryOrdering innerSO downX1 inp domain = do
181
182 [rel] <- downX1 inp
183 Just [(_, relDomain)] <- downD ("SO", domain)
184 innerSO downX1 rel relDomain