never executed always true always false
1 {-# LANGUAGE QuasiQuotes #-}
2
3 module Conjure.Representations.Common where
4
5 -- conjure
6 import Conjure.Prelude
7 import Conjure.Language.Definition
8 import Conjure.Language.Domain
9 import Conjure.Language.TH
10
11 -- containers
12 import Data.Set as S ( toList )
13
14
15 mkSizeCons :: SizeAttr Expression -> Expression -> [Expression]
16 mkSizeCons sizeAttr cardinality =
17 case sizeAttr of
18 SizeAttr_None -> []
19 SizeAttr_Size x -> return [essence| &x = &cardinality |]
20 SizeAttr_MinSize x -> return [essence| &x <= &cardinality |]
21 SizeAttr_MaxSize y -> return [essence| &cardinality <= &y |]
22 SizeAttr_MinMaxSize x y -> [ [essence| &x <= &cardinality |]
23 , [essence| &cardinality <= &y |]
24 ]
25
26 mkBinRelCons :: NameGen m => BinaryRelationAttrs -> Domain r Expression -> Expression -> m [Expression]
27 mkBinRelCons (BinaryRelationAttrs binRelAttrs) dom rel = do
28 (xP, x) <- quantifiedVar
29 (yP, y) <- quantifiedVar
30 (zP, z) <- quantifiedVar
31
32 let
33 one BinRelAttr_Reflexive = return [essence| forAll &xP : &dom . &rel(&x,&x) |]
34 one BinRelAttr_Irreflexive = return [essence| forAll &xP : &dom . !(&rel(&x,&x)) |]
35 one BinRelAttr_Coreflexive = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> &x=&y |]
36 one BinRelAttr_Symmetric = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> &rel(&y,&x) |]
37 one BinRelAttr_AntiSymmetric = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) /\ &rel(&y,&x) -> &x=&y |]
38 one BinRelAttr_ASymmetric = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> !&rel(&y,&x) |]
39 one BinRelAttr_Transitive = return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&y,&z) -> &rel(&x,&z) |]
40 one BinRelAttr_Total = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) \/ &rel(&y,&x) |]
41 one BinRelAttr_Connex = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) \/ &rel(&y,&x) \/ (&x = &y) |]
42 one BinRelAttr_Euclidean = return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&x,&z) -> &rel(&y,&z) |]
43 one BinRelAttr_LeftTotal = return [essence| forAll &xP : &dom . exists &yP : &dom . &rel(&x,&y) |]
44 one BinRelAttr_RightTotal = return [essence| forAll &yP : &dom . exists &xP : &dom . &rel(&x,&y) |]
45
46 one BinRelAttr_Serial = one BinRelAttr_LeftTotal
47 one BinRelAttr_Equivalence = one BinRelAttr_Reflexive ++ one BinRelAttr_Symmetric ++ one BinRelAttr_Transitive
48 one BinRelAttr_LinearOrder = one BinRelAttr_Total ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
49 one BinRelAttr_WeakOrder = one BinRelAttr_Total ++ one BinRelAttr_Transitive
50 one BinRelAttr_PreOrder = one BinRelAttr_Reflexive ++ one BinRelAttr_Transitive
51 one BinRelAttr_PartialOrder = one BinRelAttr_Reflexive ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
52 one BinRelAttr_StrictPartialOrder = one BinRelAttr_Irreflexive ++ one BinRelAttr_ASymmetric ++ one BinRelAttr_Transitive
53
54 return $ concatMap one (S.toList binRelAttrs)
55
56
57 mkBinRelConsSoft :: NameGen m => Expression -> Expression -> BinaryRelationAttrs -> Domain r Expression -> Expression -> m [Expression]
58 mkBinRelConsSoft maxNum divisor (BinaryRelationAttrs binRelAttrs) dom rel = do
59 -- maxNum: if the property holds this many times, we perfectly satisfy this condition
60 -- divisor: 2,4,8
61 -- 2: satisfy the property at least half the time
62 -- 4: satisfy the property at least one quarter of the time
63 -- 8: satisfy the property at least 1/8th of the time
64 (xP, x) <- quantifiedVar
65 (yP, y) <- quantifiedVar
66 (zP, z) <- quantifiedVar
67
68 let
69 one BinRelAttr_Reflexive = return [essence| &maxNum / &divisor <= sum &xP : &dom . toInt(&rel(&x,&x)) |]
70 one BinRelAttr_Irreflexive = return [essence| &maxNum / &divisor <= sum &xP : &dom . toInt(!(&rel(&x,&x))) |]
71 one BinRelAttr_Coreflexive = return [essence| &maxNum / &divisor <= sum &xP, &yP : &dom . toInt(&rel(&x,&y) -> &x=&y) |]
72 one BinRelAttr_Symmetric = return [essence| &maxNum / &divisor <= sum &xP, &yP : &dom . toInt(&rel(&x,&y) -> &rel(&y,&x)) |]
73 one BinRelAttr_AntiSymmetric = return [essence| &maxNum / &divisor <= sum &xP, &yP : &dom . toInt(&rel(&x,&y) /\ &rel(&y,&x) -> &x=&y) |]
74 one BinRelAttr_ASymmetric = return [essence| &maxNum / &divisor <= sum &xP, &yP : &dom . toInt(&rel(&x,&y) -> !(&rel(&y,&x))) |]
75 one BinRelAttr_Transitive = return [essence| &maxNum / &divisor <= sum &xP, &yP, &zP : &dom . toInt(&rel(&x,&y) /\ &rel(&y,&z) -> &rel(&x,&z)) |]
76 one BinRelAttr_Total = return [essence| &maxNum / &divisor <= sum &xP, &yP : &dom . toInt(&rel(&x,&y) \/ &rel(&y,&x)) |]
77 one BinRelAttr_Connex = return [essence| &maxNum / &divisor <= sum &xP, &yP : &dom . toInt(&rel(&x,&y) \/ &rel(&y,&x) \/ (&x = &y)) |]
78 one BinRelAttr_Euclidean = return [essence| &maxNum / &divisor <= sum &xP, &yP, &zP : &dom . toInt(&rel(&x,&y) /\ &rel(&x,&z) -> &rel(&y,&z)) |]
79 one BinRelAttr_LeftTotal = return [essence| &maxNum / &divisor <= sum &xP : &dom . sum &yP : &dom . toInt(&rel(&x,&y)) |]
80 one BinRelAttr_RightTotal = return [essence| &maxNum / &divisor <= sum &yP : &dom . sum &xP : &dom . toInt(&rel(&x,&y)) |]
81
82 one BinRelAttr_Serial = one BinRelAttr_LeftTotal
83 one BinRelAttr_Equivalence = one BinRelAttr_Reflexive ++ one BinRelAttr_Symmetric ++ one BinRelAttr_Transitive
84 one BinRelAttr_LinearOrder = one BinRelAttr_Total ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
85 one BinRelAttr_WeakOrder = one BinRelAttr_Total ++ one BinRelAttr_Transitive
86 one BinRelAttr_PreOrder = one BinRelAttr_Reflexive ++ one BinRelAttr_Transitive
87 one BinRelAttr_PartialOrder = one BinRelAttr_Reflexive ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
88 one BinRelAttr_StrictPartialOrder = one BinRelAttr_Irreflexive ++ one BinRelAttr_ASymmetric ++ one BinRelAttr_Transitive
89
90
91
92 return $ concatMap one (S.toList binRelAttrs)
93
94
95 -- reflexive, the diagonal is full
96 -- irreflexive, the diagonal is empty
97 -- coreflexive, only the diagonal is full
98 -- symmetric, if R(x,y) then R(y,x)
99 -- anti-symmetric, both R(x,y) and R(y,x) are never full at the same time (we say nothing about the the diagonal)
100 -- a-symmetric, anti-symmetric + irreflexive
101 -- transitive xy + yz -> xz
102 -- total: either R(x,y) or R(y,x). implies reflexive
103 -- connex: total, but doesn't imply reflexive (we say nothing about the diagonal)
104 -- left-total: every x is related to some y -- R(x,y)
105 -- right-total: every y is related to some x -- R(x,y)
106 -- Euclidean: xy + xz -> yz
107
108 -- some properties
109 -- total implies reflexive. connex doesn't.
110 -- aSymmetric implies irreflexive and antiSymmetric
111
112 -- derived definitions
113 -- serial: left-total
114 -- equivalance: reflexive + symmetric + transitive
115 -- linearOrder: antiSymmetric + total + transitive
116 -- weakOrder; total + transitive
117 -- preOrder: reflexive + transitive
118 -- partialOrder: reflexive + antiSymmetric + transitive
119 -- strictPartialOrder: irreflexive + transitive (implied aSymmetric)
120