Data.List.Shift

Definitions

data Shift : Bool -> (t : Type) -> SnocList t -> List t -> SnocList t -> List t -> Type

  Witness that a pair of a snoclist and a list
  is the result of shifting values from the head of
  an initial list to the tail of an initial snoclist.
  
  This data type is a witness for what a lexer does:
  taking a finite number of elements from the head of a
  list and appending them to the tail of a snoclist.
  
  By carrying around such a proof, we guarantee that no
  character is lost during lexing, and that the order of
  characters does not change during lexing.
  
  @ strict : `True` if at least one element was shifted
  @ sx     : the current snoclist
  @ xs     : the current list
  @ giro   : the initial snoclist
  @ orig   : the initial list

Totality: total
Visibility: public export
Constructors:

Same : Shift False t sx xs sx xs

  Doing nothing results in a non-strict `Shift`

SH : Shift b1 t sx (x :: xs) sy ys -> Shift b2 t (sx :< x) xs sy ys

  We arrive at a new result by shifting one more value.

Hint: 

Cast (Shift b t sx xs sy ys) Nat

shift : Shift b t sc (x :: xs) giro orig -> Shift True t (sc :< x) xs giro orig

  Strict alias for `SH`

Totality: total
Visibility: public export

toNat : Shift b t sx xs sy ys -> Nat

  Converts a `Shift` to a natural number, representing
  the number of items dropped from the original list.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

swapOr : Shift (x || Delay y) t sx xs sy ys -> Shift (y || Delay x) t sx xs sy ys

Totality: total
Visibility: public export

orSame : Shift (x || Delay x) t sx xs sy ys -> Shift x t sx xs sy ys

Totality: total
Visibility: public export

orTrue : Shift (x || Delay True) t sx xs sy ys -> Shift True t sx xs sy ys

Totality: total
Visibility: public export

orFalse : Shift (x || Delay False) t sx xs sy ys -> Shift x t sx xs sy ys

Totality: total
Visibility: public export

swapAnd : Shift (x && Delay y) t sx xs sy ys -> Shift (y && Delay x) t sx xs sy ys

Totality: total
Visibility: public export

andSame : Shift (x && Delay x) t sx xs sy ys -> Shift x t sx xs sy ys

Totality: total
Visibility: public export

andTrue : Shift (x && Delay True) t sx xs sy ys -> Shift x t sx xs sy ys

Totality: total
Visibility: public export

andFalse : Shift (x && Delay False) t sx xs sy ys -> Shift False t sx xs sy ys

Totality: total
Visibility: public export

weaken : Shift b t sx xs sy ys -> Shift False t sx xs sy ys

  Every `Shift` can be converted to a non-strict one.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

weakens : Shift True t sx xs sy ys -> Shift b t sx xs sy ys

  A strict `Shift` can be converted to a non-strict one.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

suffix : Shift b t sx xs sy ys -> Suffix b xs ys

  A `Shift` can be converted to a `Suffix`.
  
  Performance: This is the identity function at runtime.

Totality: total
Visibility: public export

and1 : Shift b1 t sx xs sy ys -> Shift (b1 && b2) t sx xs sy ys

Totality: total
Visibility: public export

and2 : Shift b2 t sx xs sy ys -> Shift (b1 && Delay b2) t sx xs sy ys

Totality: total
Visibility: public export

trans : Shift b1 t sx xs sy ys -> Shift b2 t sy ys sz zs -> Shift (b1 || Delay b2) t sx xs sz zs

  `Shift` is a reflexive and transitive relation.
  
  Performance: This is integer addition at runtime.

Totality: total
Visibility: public export