0 | module Data.DiffList
  1 |
  2 | import Control.Relation
  3 | import Data.List
  4 | import Data.Nat
  5 |
  6 | public export
  7 | data IsSuffixOf : (xs, ys : List a) -> Type where
  8 |     SuffixRefl : xs `IsSuffixOf` xs
  9 |     ConsSuffix : xs `IsSuffixOf` ys -> xs `IsSuffixOf` (y :: ys)
 10 |
 11 | export
 12 | Reflexive (List a) IsSuffixOf where
 13 |     reflexive = SuffixRefl
 14 |
 15 | export
 16 | Transitive (List a) IsSuffixOf where
 17 |     transitive prf1 SuffixRefl = prf1
 18 |     transitive prf1 (ConsSuffix prf2) = ConsSuffix (transitive prf1 prf2)
 19 |
 20 | export
 21 | Preorder (List a) IsSuffixOf where
 22 |
 23 | -- export
 24 | -- Antisymmetric (List a) IsSuffixOf where
 25 | --     antisymmetric SuffixRefl _ = Refl
 26 | --     antisymmetric _ SuffixRefl = Refl
 27 | --     antisymmetric {x = x :: xs, y = y :: ys} (ConsSuffix a) (ConsSuffix b) = absurd $ antimsymmetricLemma1 [] a b
 28 |
 29 | export
 30 | appendIsSuffix : (xs, ys : List a) -> ys `IsSuffixOf` xs ++ ys
 31 | appendIsSuffix [] ys = SuffixRefl
 32 | appendIsSuffix (x :: xs) ys = ConsSuffix (appendIsSuffix xs ys)
 33 |
 34 | export
 35 | suffixLengthLTE : (xs, ys : List a) -> xs `IsSuffixOf` ys -> length xs `LTE` length ys
 36 | suffixLengthLTE xs xs SuffixRefl = reflexive
 37 | suffixLengthLTE xs (y :: ys) (ConsSuffix x) = lteSuccRight (suffixLengthLTE xs ys x)
 38 |
 39 | ||| A diff-list takes a list, and appends new elements on the front
 40 | ||| This allows for cheap concatenation, no matter how it is associated
 41 | |||
 42 | ||| This implementation includes a proof that the function can only append
 43 | ||| elements to the front
 44 | public export
 45 | record DiffList a where
 46 |     constructor MkDiffList
 47 |     append : List a -> List a
 48 |     0 isSuffix : (rest : List a) -> rest `IsSuffixOf` append rest
 49 |
 50 | public export
 51 | Nil : DiffList a
 52 | Nil = MkDiffList id (\_ => reflexive)
 53 |
 54 | public export
 55 | (::) : a -> DiffList a -> DiffList a
 56 | x :: xs = MkDiffList
 57 |     (\ys => x :: xs.append ys)
 58 |     (\rest => ConsSuffix (xs.isSuffix rest))
 59 |
 60 | public export %inline
 61 | toList : DiffList a -> List a
 62 | toList xs = xs.append []
 63 |
 64 | export
 65 | diffAppendIsSuffix :
 66 |     (xs, ys : DiffList a) ->
 67 |     (rest : List a) ->
 68 |     rest `IsSuffixOf` xs.append (ys.append rest)
 69 |
 70 | public export %inline
 71 | Semigroup (DiffList a) where
 72 |     xs <+> ys = MkDiffList
 73 |         (\zs => xs.append (ys.append zs))
 74 |         (\rest =>
 75 |             let ysPrf = ys.isSuffix _
 76 |                 xsPrf = xs.isSuffix _
 77 |              in transitive ysPrf xsPrf)
 78 |
 79 | public export %inline
 80 | Monoid (DiffList a) where
 81 |     neutral = Nil
 82 |
 83 | public export %inline
 84 | singleton : a -> DiffList a
 85 | singleton x = MkDiffList (\xs => x :: xs) (\rest => ConsSuffix SuffixRefl)
 86 |
 87 | public export %inline
 88 | fromList : List a -> DiffList a
 89 | fromList xs = MkDiffList (\ys => xs ++ ys) (\rest => appendIsSuffix xs rest)
 90 |
 91 | -- Non-empty
 92 | {-
 93 | public export 0
 94 | NonEmpty : DiffList a -> Type
 95 | NonEmpty xs = (rest : List a) -> length (xs.append rest) `GT` length rest
 96 |
 97 | export
 98 | singletonIsNonEmpty : (x : _) -> NonEmpty (DiffList.singleton x)
 99 | singletonIsNonEmpty x rest = LTESucc reflexive
100 |
101 | export
102 | nonEmptyRightNonEmpty : (xs, ys : DiffList a) -> NonEmpty ys -> NonEmpty (xs <+> ys)
103 | nonEmptyRightNonEmpty xs ys prf rest = ?foo -- transitive ?one ?two
104 | -- 
105 |
106 | export
107 | nonEmptyLeftNonEmpty : (xs, ys : DiffList a) -> NonEmpty xs -> NonEmpty (xs <+> ys)
108 | nonEmptyLeftNonEmpty xs ys f rest =
109 |     let
110 |         isSuffix = ?wot -- diffAppendIsSuffix xs ys rest
111 |         prf1 = f rest
112 |         prf2 = suffixLengthLTE (xs.append rest) (xs.append (ys.append rest)) isSuffix
113 |      in transitive prf1 prf2
114 |
115 | -}
116 |
117 | -- Proofs
118 |
119 | ||| Equality of `DiffList`s is represented as equality of `DiffList.toList` of each side
120 | public export
121 | DiffListEq : (xs, ys : DiffList a) -> Type
122 | DiffListEq xs ys = toList xs === toList ys
123 |
124 | infix 6 .==
125 |
126 | public export
127 | (.==) : (xs, ys : DiffList a) -> Type
128 | (.==) = DiffListEq
129 |
130 | export
131 | semigroupAssoc : (xs, ys, zs : DiffList a) -> ((xs <+> ys) <+> zs) .== (xs <+> (ys <+> zs))
132 | semigroupAssoc xs ys zs = Refl
133 |
134 | export
135 | toListFromListId : (xs : List a) -> DiffList.toList (DiffList.fromList xs) === xs
136 | toListFromListId xs = appendNilRightNeutral xs
137 |
138 | export
139 | semigroupNilRightNeutral : (xs : DiffList a) -> (xs <+> Nil) .== xs
140 | semigroupNilRightNeutral xs = Refl
141 |
142 | export
143 | semigroupNilLeftNeutral : (xs : DiffList a) -> (Nil <+> xs) .== xs
144 | semigroupNilLeftNeutral xs = Refl
145 |