git.iko.soy/laop
on master help sign in
Added power transpose functions / point / pointAp / toBool
f047a9cArmando Santos
src/LAoP/Matrix/Internal.hs+10−1
compare with master
unifiedsplit
@@ -137,13 +137,14 @@ module LAoP.Matrix.Internal
137 fromFRel,
137 fromFRel,
138 fromFRel',
138 fromFRel',
139 toRel,
139 toRel,
140+ negateM,
140 orM,
141 orM,
141 andM,
142 andM,
142 subM
143 subM
143 )
144 )
144 where
145 where
145
146
146−import LAoP.Utils
147+import LAoP.Utils.Internal
147import Data.Bool
148import Data.Bool
148import Data.Kind
149import Data.Kind
149import Data.List
150import Data.List
@@ -797,6 +798,14 @@ fromBool :: Bool -> Natural 0 1
797fromBool True = nat 1
798fromBool True = nat 1
798fromBool False = nat 0
799fromBool False = nat 0
799
800
801+-- | Relational negation
802+negateM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
803+negateM Empty = Empty
804+negateM (One (Nat 0)) = One (Nat 1)
805+negateM (One (Nat 1)) = One (Nat 0)
806+negateM (Junc a b) = Junc (negateM a) (negateM b)
807+negateM (Split a b) = Split (negateM a) (negateM b)
808+
800-- | Relational addition
809-- | Relational addition
801orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
810orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
802orM Empty Empty = Empty
811orM Empty Empty = Empty
src/LAoP/Relation.hs+6
@@ -51,10 +51,13 @@ module LAoP.Relation
51 toRel,
51 toRel,
52 toLists,
52 toLists,
53 toList,
53 toList,
54+ toBool,
55+ pt,
54 relationBuilder,
56 relationBuilder,
55 zeros,
57 zeros,
56 ones,
58 ones,
57 bang,
59 bang,
60+ point,
58
61
59 -- * Relational operations
62 -- * Relational operations
60 conv,
63 conv,
@@ -123,6 +126,9 @@ module LAoP.Relation
123 fromF,
126 fromF,
124 fromF',
127 fromF',
125
128
129+ -- ** Relational application
130+ pointAp,
131+
126 -- * Matrix printing
132 -- * Matrix printing
127 pretty,
133 pretty,
128 prettyPrint
134 prettyPrint
src/LAoP/Relation/Internal.hs+64−8
@@ -27,7 +27,7 @@
27
27
28module LAoP.Relation.Internal
28module LAoP.Relation.Internal
29 ( -- | This definition makes use of the fact that 'Void' is
29 ( -- | This definition makes use of the fact that 'Void' is
30− -- isomorphic to 0 and '()' to 1 and captures matrix
30+ -- isomorphic to 0 and 'One' to 1 and captures matrix
31 -- dimensions as stacks of 'Either's.
31 -- dimensions as stacks of 'Either's.
32 --
32 --
33 -- There exists two type families that make it easier to write
33 -- There exists two type families that make it easier to write
@@ -60,10 +60,13 @@ module LAoP.Relation.Internal
60 toRel,
60 toRel,
61 toLists,
61 toLists,
62 toList,
62 toList,
63+ toBool,
64+ pt,
63 relationBuilder,
65 relationBuilder,
64 zeros,
66 zeros,
65 ones,
67 ones,
66 bang,
68 bang,
69+ point,
67
70
68 -- * Relational operations
71 -- * Relational operations
69 conv,
72 conv,
@@ -132,6 +135,9 @@ module LAoP.Relation.Internal
132 fromF,
135 fromF,
133 fromF',
136 fromF',
134
137
138+ -- ** Relational application
139+ pointAp,
140+
135 -- * Matrix printing
141 -- * Matrix printing
136 pretty,
142 pretty,
137 prettyPrint
143 prettyPrint
@@ -140,7 +146,7 @@ module LAoP.Relation.Internal
140
146
141import Data.Void
147import Data.Void
142import qualified LAoP.Matrix.Internal as I
148import qualified LAoP.Matrix.Internal as I
143−import LAoP.Utils
149+import LAoP.Utils.Internal
144import Control.DeepSeq
150import Control.DeepSeq
145import qualified Control.Category as C
151import qualified Control.Category as C
146import Data.Bool
152import Data.Bool
@@ -174,6 +180,8 @@ instance Num (Relation a b) where
174 -- | Matrix multiplication becomes Boolean matrix conjunction
180 -- | Matrix multiplication becomes Boolean matrix conjunction
175 (R a) * (R b) = R (I.andM a b)
181 (R a) * (R b) = R (I.andM a b)
176
182
183+ negate (R a) = R (I.negateM a)
184+
177-- Type alias
185-- Type alias
178type Zero = Void
186type Zero = Void
179type One = ()
187type One = ()
@@ -289,6 +297,30 @@ toLists (R m) = I.toLists m
289toList :: Relation a b -> [Boolean]
297toList :: Relation a b -> [Boolean]
290toList (R m) = I.toList m
298toList (R m) = I.toList m
291
299
300+-- | Converts a well typed @'Relation'@ to @'Bool'@.
301+toBool :: Relation One One -> Bool
302+toBool r = case toList r of
303+ [Nat 0] -> False
304+ _ -> True
305+
306+-- | Power transpose
307+pt ::
308+ ( Bounded a,
309+ Bounded b,
310+ Enum a,
311+ Enum b,
312+ Eq a,
313+ Eq b,
314+ KnownNat (I.Count (I.Normalize a)),
315+ KnownNat (I.Count (I.Normalize b)),
316+ I.FromLists Boolean (I.Normalize a) One,
317+ I.FromLists Boolean (I.Normalize b) One
318+ )
319+ => Relation a b -> (a -> [b])
320+pt r a =
321+ let lb = [minBound .. maxBound]
322+ in [ b | b <- lb, toBool (pointAp a b r) ]
323+
292-- Zeros Matrix
324-- Zeros Matrix
293
325
294-- | The zero matrix. A matrix wholly filled with zeros.
326-- | The zero matrix. A matrix wholly filled with zeros.
@@ -311,11 +343,20 @@ ones = relationBuilder (const (nat 1))
311
343
312-- | The T (Top) row vector matrix.
344-- | The T (Top) row vector matrix.
313bang ::
345bang ::
314− forall a.
315− (I.FromLists Boolean (I.Normalize a) (), KnownNat (I.Count (I.Normalize a))) =>
346+ (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
316 Relation a One
347 Relation a One
317bang = ones
348bang = ones
318
349
350+-- | Point constant relation
351+point ::
352+ ( Bounded a,
353+ Enum a,
354+ Eq a,
355+ KnownNat (I.Count (I.Normalize a)),
356+ I.FromLists Boolean (I.Normalize a) One
357+ ) => a -> Relation One a
358+point a = fromF' (const a)
359+
319-- Identity Matrix
360-- Identity Matrix
320
361
321-- | Identity matrix
362-- | Identity matrix
@@ -325,9 +366,24 @@ identity ::
325identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
366identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
326
367
327-- | Relational composition
368-- | Relational composition
328−comp :: forall a b c . Relation b c -> Relation a b -> Relation a c
369+comp :: Relation b c -> Relation a b -> Relation a c
329comp (R a) (R b) = R (I.compRel a b)
370comp (R a) (R b) = R (I.compRel a b)
330
371
372+-- | Relational application
373+pointAp ::
374+ ( Bounded a,
375+ Bounded b,
376+ Enum a,
377+ Enum b,
378+ Eq a,
379+ Eq b,
380+ KnownNat (I.Count (I.Normalize a)),
381+ KnownNat (I.Count (I.Normalize b)),
382+ I.FromLists Boolean (I.Normalize a) One,
383+ I.FromLists Boolean (I.Normalize b) One
384+ ) => a -> b -> Relation a b -> Relation One One
385+pointAp a b r = conv (point b) `comp` r `comp` point a
386+
331-- | Relational converse
387-- | Relational converse
332conv :: Relation a b -> Relation b a
388conv :: Relation a b -> Relation b a
333conv (R a) = R (I.tr a)
389conv (R a) = R (I.tr a)
@@ -337,12 +393,12 @@ sse :: Relation a b -> Relation a b -> Bool
337sse a b = a <= b
393sse a b = a <= b
338
394
339-- | Relational implication (the same as @'sse'@)
395-- | Relational implication (the same as @'sse'@)
340−implies :: Relation a b -> Relation a b -> Bool
396+implies :: Relation a b -> Relation a b -> Relation a b
341−implies = sse
397+implies r s = negate r `union` s
342
398
343-- | Relational bi-implication
399-- | Relational bi-implication
344iff :: Relation a b -> Relation a b -> Bool
400iff :: Relation a b -> Relation a b -> Bool
345−iff r s = (r `implies` s) && (s `implies` r)
401+iff r s = r == s
346
402
347-- | Relational intersection
403-- | Relational intersection
348--
404--
src/LAoP/Utils/Internal.hs+1−1
@@ -78,7 +78,7 @@ module LAoP.Utils.Internal
78 -- @
78 -- @
79 --
79 --
80 -- * 'Natural' data type
80 -- * 'Natural' data type
81− Natural,
81+ Natural(..),
82 nat,
82 nat,
83
83
84 -- * Coerce auxiliar functions to help promote 'Int' typed functions to
84 -- * Coerce auxiliar functions to help promote 'Int' typed functions to