
   0 | module Data.List.Shift
   1 | 
   2 | import Data.Bool.Rewrite
   3 | import Data.List.Suffix
   4 | import Data.Nat
   5 | 
   6 | %default total
   7 | 
   8 | ||| Witness that a pair of a snoclist and a list
   9 | ||| is the result of shifting values from the head of
  10 | ||| an initial list to the tail of an initial snoclist.
  11 | |||
  12 | ||| This data type is a witness for what a lexer does:
  13 | ||| taking a finite number of elements from the head of a
  14 | ||| list and appending them to the tail of a snoclist.
  15 | |||
  16 | ||| By carrying around such a proof, we guarantee that no
  17 | ||| character is lost during lexing, and that the order of
  18 | ||| characters does not change during lexing.
  19 | |||
  20 | ||| @ strict : `True` if at least one element was shifted
  21 | ||| @ sx     : the current snoclist
  22 | ||| @ xs     : the current list
  23 | ||| @ giro   : the initial snoclist
  24 | ||| @ orig   : the initial list
  25 | public export
  26 | data Shift :
  27 |      (strict : Bool)
  28 |   -> (t      : Type)
  29 |   -> (sx     : SnocList t)
  30 |   -> (xs     : List t)
  31 |   -> (giro   : SnocList t)
  32 |   -> (orig   : List t)
  33 |   -> Type where
  34 |   [search strict xs giro orig]
  35 | 
  36 |   ||| Doing nothing results in a non-strict `Shift`
  37 |   Same : 
  38 |        {0 t : Type}
  39 |     -> {0 sx : SnocList t}
  40 |     -> {0 xs : List t}
  41 |     -> Shift False t sx xs sx xs
  42 | 
  43 |   ||| We arrive at a new result by shifting one more value.
  44 |   SH   :
  45 |        {0 t : Type}
  46 |     -> {0 b1,b2 : Bool}
  47 |     -> {0 x : t}
  48 |     -> {0 sx,sy : SnocList t}
  49 |     -> {0 xs,ys : List t}
  50 |     -> Shift b1 t sx (x :: xs) sy ys
  51 |     -> Shift b2 t (sx :< x) xs sy ys
  52 | 
  53 | ||| Strict alias for `SH`
  54 | public export %inline
  55 | shift : Shift b t sc (x::xs) giro orig -> Shift True t (sc :< x) xs giro orig
  56 | shift = SH
  57 | 
  58 | --------------------------------------------------------------------------------
  59 | --          Conversions
  60 | --------------------------------------------------------------------------------
  61 | 
  62 | ||| Converts a `Shift` to a natural number, representing
  63 | ||| the number of items dropped from the original list.
  64 | |||
  65 | ||| Performance: This is the identity function at runtime.
  66 | public export
  67 | toNat : {0 b : Bool} -> Shift b t sx xs sy ys -> Nat
  68 | toNat Same   = Z
  69 | toNat (SH x) = S $ toNat x
  70 | 
  71 | public export %inline
  72 | Cast (Shift b t sx xs sy ys) Nat where cast = toNat
  73 | 
  74 | public export
  75 | swapOr :
  76 |      {0 x,y : _}
  77 |   -> Shift (x || y) t sx xs sy ys
  78 |   -> Shift (y || x) t sx xs sy ys
  79 | swapOr = swapOr (\k => Shift k t sx xs sy ys)
  80 | 
  81 | public export %inline
  82 | orSame : {0 x : _} -> Shift (x || x) t sx xs sy ys -> Shift x t sx xs sy ys
  83 | orSame = orSame (\k => Shift k t sx xs sy ys)
  84 | 
  85 | public export %inline
  86 | orTrue :
  87 |      {0 x : _}
  88 |   -> Shift (x || True) t sx xs sy ys
  89 |   -> Shift True t sx xs sy ys
  90 | orTrue = orTrue (\k => Shift k t sx xs sy ys)
  91 | 
  92 | public export %inline
  93 | orFalse :
  94 |      {0 x : _}
  95 |   -> Shift (x || False) t sx xs sy ys
  96 |   -> Shift x t sx xs sy ys
  97 | orFalse = orFalse (\k => Shift k t sx xs sy ys)
  98 | 
  99 | public export %inline
 100 | swapAnd :
 101 |      {0 x,y : _}
 102 |   -> Shift (x && y) t sx xs sy ys
 103 |   -> Shift (y && x) t sx xs sy ys
 104 | swapAnd = swapAnd (\k => Shift k t sx xs sy ys)
 105 | 
 106 | public export %inline
 107 | andSame :
 108 |      {0 x : _}
 109 |   -> Shift (x && x) t sx xs sy ys
 110 |   -> Shift x t sx xs sy ys
 111 | andSame = andSame (\k => Shift k t sx xs sy ys)
 112 | 
 113 | public export %inline
 114 | andTrue :
 115 |      {0 x : _}
 116 |   -> Shift (x && True) t sx xs sy ys
 117 |   -> Shift x t sx xs sy ys
 118 | andTrue = andTrue (\k => Shift k t sx xs sy ys)
 119 | 
 120 | public export %inline
 121 | andFalse :
 122 |      {0 x : _}
 123 |   -> Shift (x && False) t sx xs sy ys
 124 |   -> Shift False t sx xs sy ys
 125 | andFalse = andFalse (\k => Shift k t sx xs sy ys)
 126 | 
 127 | ||| Every `Shift` can be converted to a non-strict one.
 128 | |||
 129 | ||| Performance: This is the identity function at runtime.
 130 | public export
 131 | weaken : {0 b : Bool} -> Shift b t sx xs sy ys -> Shift False t sx xs sy ys
 132 | weaken Same   = Same
 133 | weaken (SH x) = SH x
 134 | 
 135 | ||| A strict `Shift` can be converted to a non-strict one.
 136 | |||
 137 | ||| Performance: This is the identity function at runtime.
 138 | public export
 139 | weakens : {0 b : Bool} -> Shift True t sx xs sy ys -> Shift b t sx xs sy ys
 140 | weakens (SH x) = SH x
 141 | weakens Same impossible
 142 | 
 143 | ||| A `Shift` can be converted to a `Suffix`.
 144 | |||
 145 | ||| Performance: This is the identity function at runtime.
 146 | public export
 147 | suffix : {0 b : Bool} -> Shift b t sx xs sy ys -> Suffix b xs ys
 148 | suffix Same   = Same
 149 | suffix (SH x) = Uncons $ suffix x
 150 | 
 151 | public export
 152 | and1 : Shift b1 t sx xs sy ys -> Shift (b1 && b2) t sx xs sy ys
 153 | and1 Same   = Same
 154 | and1 (SH x) = SH x
 155 | 
 156 | public export
 157 | and2 : Shift b2 t sx xs sy ys -> Shift (b1 && b2) t sx xs sy ys
 158 | and2 s = swapAnd (and1 s)
 159 | 
 160 | ||| `Shift` is a reflexive and transitive relation.
 161 | |||
 162 | ||| Performance: This is integer addition at runtime.
 163 | public export
 164 | trans :
 165 |      Shift b1 t sx xs sy ys
 166 |   -> Shift b2 t sy ys sz zs
 167 |   -> Shift (b1 || b2) t sx xs sz zs
 168 | trans Same y   = y
 169 | trans (SH x) y = SH $ trans x y
 170 | 
 171 | %inline
 172 | transp :
 173 |      Shift b1 t sx xs sy ys
 174 |   -> Shift b2 t sy ys sz zs
 175 |   -> Shift (b1 || b2) t sx xs sz zs
 176 | transp x y = believe_me (toNat x + toNat y)
 177 | 
 178 | %transform "shiftTransPlus" Shift.trans = Shift.transp
 179 |