
   0 | module Data.List.Suffix
   1 | 
   2 | import Control.Relation
   3 | import public Data.Bool.Rewrite
   4 | 
   5 | %default total
   6 | 
   7 | ||| Proof that a list is a (possibly strict) suffix of another list.
   8 | |||
   9 | ||| Performance: Values of this type are optimized to integers at runtime.
  10 | public export
  11 | data Suffix : (strict : Bool) -> (xs,ys : List a) -> Type where
  12 |   ||| Every list is a (non-strict) suffix of itself.
  13 |   Same   : Suffix False xs xs
  14 | 
  15 |   ||| If a non-empty list `xs` is a suffix of `ys`, then the tail of
  16 |   ||| `xs` is a strict suffix of `ys`.
  17 |   Uncons : Suffix b (h :: t) cs -> Suffix b2 t cs
  18 | 
  19 | %builtin Natural Suffix
  20 | 
  21 | export
  22 | Uninhabited (Suffix b (h :: t) []) where
  23 |   uninhabited Same impossible
  24 |   uninhabited (Uncons x) = uninhabited x
  25 | 
  26 | export
  27 | Uninhabited (Suffix True xs []) where
  28 |   uninhabited (Uncons x) = uninhabited x
  29 | 
  30 | ||| Strict version of `Uncons`
  31 | public export %inline
  32 | uncons : Suffix b (h::t) cs -> Suffix True t cs
  33 | uncons = Uncons
  34 | 
  35 | --------------------------------------------------------------------------------
  36 | --          Conversions
  37 | --------------------------------------------------------------------------------
  38 | 
  39 | ||| Converts a `Suffix` to a natural number, representing
  40 | ||| the number of items dropped from the original list.
  41 | |||
  42 | ||| Performance: This is the identity function at runtime.
  43 | public export
  44 | toNat : Suffix b xs ys -> Nat
  45 | toNat Same       = Z
  46 | toNat (Uncons x) = S $toNat x
  47 | 
  48 | public export %inline
  49 | Cast (Suffix b xs ys) Nat where cast = toNat
  50 | 
  51 | public export
  52 | swapOr : {0 x,y : _} -> Suffix (x || y) xs ys -> Suffix (y || x) xs ys
  53 | swapOr = swapOr (\k => Suffix k xs ys)
  54 | 
  55 | public export %inline
  56 | orSame : {0 x : _} -> Suffix (x || x) xs ys -> Suffix x xs ys
  57 | orSame = orSame (\k => Suffix k xs ys)
  58 | 
  59 | public export %inline
  60 | orTrue : {0 x : _} -> Suffix (x || True) xs ys -> Suffix True xs ys
  61 | orTrue = orTrue (\k => Suffix k xs ys)
  62 | 
  63 | public export %inline
  64 | orFalse : {0 x : _} -> Suffix (x || False) xs ys -> Suffix x xs ys
  65 | orFalse = orFalse (\k => Suffix k xs ys)
  66 | 
  67 | public export %inline
  68 | swapAnd : {0 x,y : _} -> Suffix (x && y) xs ys -> Suffix (y && x) xs ys
  69 | swapAnd = swapAnd (\k => Suffix k xs ys)
  70 | 
  71 | public export %inline
  72 | andSame : {0 x : _} -> Suffix (x && x) xs ys -> Suffix x xs ys
  73 | andSame = andSame (\k => Suffix k xs ys)
  74 | 
  75 | public export %inline
  76 | andTrue : {0 x : _} -> Suffix (x && True) xs ys -> Suffix x xs ys
  77 | andTrue = andTrue (\k => Suffix k xs ys)
  78 | 
  79 | public export %inline
  80 | andFalse : {0 x : _} -> Suffix (x && False) xs ys -> Suffix False xs ys
  81 | andFalse = andFalse (\k => Suffix k xs ys)
  82 | 
  83 | ||| Every `Suffix` can be converted to a non-strict one.
  84 | |||
  85 | ||| Performance: This is the identity function at runtime.
  86 | public export
  87 | weaken : Suffix b xs ys -> Suffix False xs ys
  88 | weaken Same       = Same
  89 | weaken (Uncons x) = Uncons x
  90 | 
  91 | ||| A strict `Suffix` can be converted to a non-strict one.
  92 | |||
  93 | ||| Performance: This is the identity function at runtime.
  94 | public export
  95 | weakens : Suffix True xs ys -> Suffix b xs ys
  96 | weakens (Uncons x) = Uncons x
  97 | weakens Same impossible
  98 | 
  99 | public export
 100 | unconsBoth : Suffix b (y :: ys) (x :: xs) -> Suffix False ys xs
 101 | unconsBoth Same       = Same
 102 | unconsBoth (Uncons z) = Uncons $ unconsBoth z
 103 | 
 104 | public export
 105 | unconsRight : Suffix True ys (x :: xs) -> Suffix False ys xs
 106 | unconsRight (Uncons x) = unconsBoth x
 107 | 
 108 | public export
 109 | and1 : Suffix b1 xs ys -> Suffix (b1 && b2) xs ys
 110 | and1 Same       = Same
 111 | and1 (Uncons x) = Uncons x
 112 | 
 113 | public export
 114 | and2 : Suffix b2 xs ys -> Suffix (b1 && b2) xs ys
 115 | and2 s = swapAnd (and1 s)
 116 | 
 117 | --------------------------------------------------------------------------------
 118 | --          Relations
 119 | --------------------------------------------------------------------------------
 120 | 
 121 | ||| `Suffix` is a reflexive and transitive relation.
 122 | |||
 123 | ||| Performance: This is integer addition at runtime.
 124 | public export
 125 | trans : Suffix b1 xs ys -> Suffix b2 ys cs -> Suffix (b1 || b2) xs cs
 126 | trans Same y       = y
 127 | trans (Uncons x) t = Uncons $ trans x t
 128 | 
 129 | %inline
 130 | transp : Suffix b1 xs ys -> Suffix b2 ys cs -> Suffix (b1 || b2) xs cs
 131 | transp x y =  believe_me (toNat x + toNat y)
 132 | 
 133 | %transform "suffixTransPlus" Suffix.trans = Suffix.transp
 134 | 
 135 | ||| `Suffix False` is a reflexive relation on lists.
 136 | public export %inline
 137 | Reflexive (List a) (Suffix False) where
 138 |   reflexive = Same
 139 | 
 140 | ||| `Suffix False` is a transitive relation on lists.
 141 | public export %inline
 142 | Transitive (List a) (Suffix False) where
 143 |   transitive = trans
 144 | 
 145 | ||| `Suffix True` is a transitive relation on lists.
 146 | public export %inline
 147 | Transitive (List a) (Suffix True) where
 148 |   transitive = trans
 149 | 
 150 | --------------------------------------------------------------------------------
 151 | --          SuffixAcc
 152 | --------------------------------------------------------------------------------
 153 | 
 154 | public export
 155 | data SuffixAcc : (ts : List t) -> Type where
 156 |   SA :
 157 |        {0 t  : Type}
 158 |     -> {0 ts : List t}
 159 |     -> ({0 ys : List t} -> {auto p : Suffix True ys ts} -> SuffixAcc ys)
 160 |     -> SuffixAcc ts
 161 | 
 162 | sa :
 163 |      {0 t  : Type}
 164 |   -> {0 ts : List t}
 165 |   -> ({0 ys : List t} -> (p : Suffix True ys ts) -> SuffixAcc ys)
 166 |   -> SuffixAcc ts
 167 | sa f = SA $ f %search
 168 | 
 169 | acc' : (ts : List t) -> Suffix False qs ts -> SuffixAcc qs
 170 | acc' []        Same       = sa $ \v => absurd v
 171 | acc' []        (Uncons x) = absurd x
 172 | acc' (x :: xs) tt         = sa $ \v => acc' xs (unconsRight $ trans v tt)
 173 | 
 174 | export
 175 | suffixAcc : {ts : List t} -> SuffixAcc ts
 176 | suffixAcc = acc' ts Same
 177 | 
 178 | --------------------------------------------------------------------------------
 179 | --          Suffix Chains
 180 | --------------------------------------------------------------------------------
 181 | 
 182 | ||| Syntactic sugar for describing transitive chains of suffixes.
 183 | public export
 184 | data Link : (xs,ys : List a) -> Type where
 185 |   F : {0 ys : _} -> (0 xs : _) -> {auto 0 p : Suffix False xs ys} -> Link xs ys
 186 |   T : {0 ys : _} -> (0 xs : _) -> {auto 0 p : Suffix True xs ys} -> Link xs ys
 187 | 
 188 | public export
 189 | any : {b : _} -> Suffix b xs ys -> Link xs ys
 190 | any {b = True}  _ = T xs
 191 | any {b = False} _ = F xs
 192 | 
 193 | ||| Syntactic sugar for describing transitive chains of suffixes.
 194 | public export
 195 | data Chain : (xs,ys : List a) -> Type where
 196 |   Nil  : {0 xs : List a} -> Chain xs xs
 197 |   (::) :
 198 |        {0 xs,ys,zs : List a}
 199 |     -> (0 link : Link xs ys)
 200 |     -> (0 ch   : Chain ys zs)
 201 |     -> Chain xs zs
 202 | 
 203 | public export
 204 | data IsStrict : Chain xs ys -> Type where
 205 |   Here : IsStrict (T xs @{p} :: ys)
 206 |   There : IsStrict c -> IsStrict (l :: c)
 207 | 
 208 | public export
 209 | 0 weak : Chain xs ys -> Suffix False xs ys
 210 | weak []               = Same
 211 | weak (F _ @{p} :: ch) = trans p $ weak ch
 212 | weak (T _ @{p} :: ch) = weaken $ trans p (weak ch)
 213 | 
 214 | public export
 215 | 0 strict : (c : Chain xs ys) -> {auto p : IsStrict c} -> Suffix True xs ys
 216 | strict (T _ @{q} :: c) @{Here}    = trans q $ weak c
 217 | strict (T _ @{q} :: c) @{There _} = trans q $ weak c
 218 | strict (F _ @{q} :: c) @{There _} = trans q $ strict c
 219 | 
 220 | --------------------------------------------------------------------------------
 221 | --          Utilities
 222 | --------------------------------------------------------------------------------
 223 | 
 224 | public export
 225 | takePrefix : (ys : List t) -> Suffix b xs ys -> List t
 226 | takePrefix ys Same            = []
 227 | takePrefix (y::ys) (Uncons p) = y :: takePrefix ys (unconsBoth p)
 228 | takePrefix []      (Uncons p) = absurd p
 229 | 
 230 | public export %inline
 231 | packPrefix : {cs : List Char} -> Suffix b xs cs -> String
 232 | packPrefix = pack . takePrefix cs
 233 |