|
1 | 1 | module Data.HeytingAlgebra |
2 | | - ( class HeytingAlgebra, tt, ff, implies, conj, disj, not |
3 | | - , (&&), (||) |
| 2 | + ( class HeytingAlgebra, tt, ff, implies, conj, disj, not, (&&), (||) |
| 3 | + , class HeytingAlgebraRecord, ffRecord, ttRecord, impliesRecord, conjRecord, disjRecord, notRecord |
4 | 4 | ) where |
5 | 5 |
|
| 6 | +import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol) |
6 | 7 | import Data.Unit (Unit, unit) |
| 8 | +import Prim.Row as Row |
| 9 | +import Prim.RowList as RL |
| 10 | +import Record.Unsafe (unsafeGet, unsafeSet) |
| 11 | +import Type.Data.Row (RProxy(..)) |
| 12 | +import Type.Data.RowList (RLProxy(..)) |
7 | 13 |
|
8 | 14 | -- | The `HeytingAlgebra` type class represents types that are bounded lattices with |
9 | 15 | -- | an implication operator such that the following laws hold: |
@@ -65,6 +71,80 @@ instance heytingAlgebraFunction :: HeytingAlgebra b => HeytingAlgebra (a -> b) w |
65 | 71 | disj f g a = f a || g a |
66 | 72 | not f a = not (f a) |
67 | 73 |
|
| 74 | +instance heytingAlgebraRecord :: (RL.RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra (Record row) where |
| 75 | + ff = ffRecord (RLProxy :: RLProxy list) (RProxy :: RProxy row) |
| 76 | + tt = ttRecord (RLProxy :: RLProxy list) (RProxy :: RProxy row) |
| 77 | + conj = conjRecord (RLProxy :: RLProxy list) |
| 78 | + disj = disjRecord (RLProxy :: RLProxy list) |
| 79 | + implies = impliesRecord (RLProxy :: RLProxy list) |
| 80 | + not = notRecord (RLProxy :: RLProxy list) |
| 81 | + |
68 | 82 | foreign import boolConj :: Boolean -> Boolean -> Boolean |
69 | 83 | foreign import boolDisj :: Boolean -> Boolean -> Boolean |
70 | 84 | foreign import boolNot :: Boolean -> Boolean |
| 85 | + |
| 86 | +-- | A class for records where all fields have `HeytingAlgebra` instances, used |
| 87 | +-- | to implement the `HeytingAlgebra` instance for records. |
| 88 | +class HeytingAlgebraRecord rowlist row subrow | rowlist -> subrow where |
| 89 | + ffRecord :: RLProxy rowlist -> RProxy row -> Record subrow |
| 90 | + ttRecord :: RLProxy rowlist -> RProxy row -> Record subrow |
| 91 | + impliesRecord :: RLProxy rowlist -> Record row -> Record row -> Record subrow |
| 92 | + disjRecord :: RLProxy rowlist -> Record row -> Record row -> Record subrow |
| 93 | + conjRecord :: RLProxy rowlist -> Record row -> Record row -> Record subrow |
| 94 | + notRecord :: RLProxy rowlist -> Record row -> Record subrow |
| 95 | + |
| 96 | +instance heytingAlgebraRecordNil :: HeytingAlgebraRecord RL.Nil row () where |
| 97 | + conjRecord _ _ _ = {} |
| 98 | + disjRecord _ _ _ = {} |
| 99 | + ffRecord _ _ = {} |
| 100 | + impliesRecord _ _ _ = {} |
| 101 | + notRecord _ _ = {} |
| 102 | + ttRecord _ _ = {} |
| 103 | + |
| 104 | +instance heytingAlgebraRecordCons |
| 105 | + :: ( IsSymbol key |
| 106 | + , Row.Cons key focus subrowTail subrow |
| 107 | + , HeytingAlgebraRecord rowlistTail row subrowTail |
| 108 | + , HeytingAlgebra focus |
| 109 | + ) |
| 110 | + => HeytingAlgebraRecord (RL.Cons key focus rowlistTail) row subrow where |
| 111 | + conjRecord _ ra rb = insert (conj (get ra) (get rb)) tail |
| 112 | + where |
| 113 | + key = reflectSymbol (SProxy :: SProxy key) |
| 114 | + get = unsafeGet key :: Record row -> focus |
| 115 | + insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow |
| 116 | + tail = conjRecord (RLProxy :: RLProxy rowlistTail) ra rb |
| 117 | + |
| 118 | + disjRecord _ ra rb = insert (disj (get ra) (get rb)) tail |
| 119 | + where |
| 120 | + key = reflectSymbol (SProxy :: SProxy key) |
| 121 | + get = unsafeGet key :: Record row -> focus |
| 122 | + insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow |
| 123 | + tail = disjRecord (RLProxy :: RLProxy rowlistTail) ra rb |
| 124 | + |
| 125 | + impliesRecord _ ra rb = insert (implies (get ra) (get rb)) tail |
| 126 | + where |
| 127 | + key = reflectSymbol (SProxy :: SProxy key) |
| 128 | + get = unsafeGet key :: Record row -> focus |
| 129 | + insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow |
| 130 | + tail = impliesRecord (RLProxy :: RLProxy rowlistTail) ra rb |
| 131 | + |
| 132 | + ffRecord _ row = insert ff tail |
| 133 | + where |
| 134 | + key = reflectSymbol (SProxy :: SProxy key) |
| 135 | + insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow |
| 136 | + tail = ffRecord (RLProxy :: RLProxy rowlistTail) row |
| 137 | + |
| 138 | + notRecord _ row |
| 139 | + = insert (not (get row)) tail |
| 140 | + where |
| 141 | + key = reflectSymbol (SProxy :: SProxy key) |
| 142 | + get = unsafeGet key :: Record row -> focus |
| 143 | + insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow |
| 144 | + tail = notRecord (RLProxy :: RLProxy rowlistTail) row |
| 145 | + |
| 146 | + ttRecord _ row = insert tt tail |
| 147 | + where |
| 148 | + key = reflectSymbol (SProxy :: SProxy key) |
| 149 | + insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow |
| 150 | + tail = ttRecord (RLProxy :: RLProxy rowlistTail) row |
0 commit comments