TypeAligned

(source)

Type-aligned sequences.  Transitive closures of (binary) relations that also provide fast reflection / destruction.

Reexports

import public Data.Linear.Notation
import public TypeAligned.ZeroOne

Definitions

data TypeAligned1 : Rel a -> Rel a

  1 or more, transitive closure of a relationship.  Name is in the pattern of `List1`.

Totality: total
Visibility: export
Constructors:

One : p x y -@ TypeAligned1 p x y
Ton : Multiple p x y -@ TypeAligned1 p x y

Hints:

Reflexive a p => Reflexive a (TypeAligned1 p)
Show (p x y) => Show (TypeAligned1 p x y)
Transitive a (TypeAligned1 p)

data TypeAligned : Rel a -> Rel a

  Reflexive, transition closure of a relationship

Totality: total
Visibility: export
Constructors:

None : (0 _ : x = y) -> TypeAligned p x y
Some : TypeAligned1 p x y -@ TypeAligned p x y

Hints:

Reflexive a (TypeAligned p)
Show (p x y) => Show (TypeAligned p x y)
Transitive a (TypeAligned p)

0 .x : TypeAligned1 p w z -> a

  Synthetic accesssor; second index

Totality: total
Visibility: export

0 .y : TypeAligned1 p w z -> a

  Synthetic accessor; second-last index

Totality: total
Visibility: export

0 .x : TypeAligned p w z -> a

  Synthetic accesssor; second index

Totality: total
Visibility: export

0 .y : TypeAligned p w z -> a

  Synthetic accessor; second-last index

Totality: total
Visibility: export

.head : (ne : TypeAligned1 p w z) -> p w (ne .x)

  Synthetic accessor

Totality: total
Visibility: export

head : (ne : TypeAligned1 p w z) -> p w (ne .x)

  Synthetic accessor

Totality: total
Visibility: export

.last : (ne : TypeAligned1 p w z) -> p (ne .y) z

  Synthetic accessor

Totality: total
Visibility: export

last : (ne : TypeAligned1 p w z) -> p (ne .y) z

  Synthetic accessor

Totality: total
Visibility: export

Nil : TypeAligned p x x

  List and SnocList empty syntax

Totality: total
Visibility: export

Lin : TypeAligned p x x

  List and SnocList empty syntax

Totality: total
Visibility: export

nonEmptyOnce : TypeAligned p x y -@ ZeroOne (TypeAligned1 p) x y

  Linear `nonEmpty`

Totality: total
Visibility: export

nonEmpty : TypeAligned p x y -> ZeroOne (TypeAligned1 p) x y

  Determine if a possibly empty sequence is non-empty.

Totality: total
Visibility: export

fromNonEmptyOnce : TypeAligned1 p x y -@ TypeAligned p x y

  Linear `fromNonEmpty`

Totality: total
Visibility: export

fromNonEmpty : TypeAligned1 p x y -> TypeAligned p x y

  Treat a non-empty sequence as possibly empty

Totality: total
Visibility: export

singletonce : (1 _ : p x y) -> TypeAligned1 p x y

  Linear `singleton`

Totality: total
Visibility: export

singletonce : (1 _ : p x y) -> TypeAligned p x y

  Linear `singleton`

Totality: total
Visibility: export

singleton : p x y -> TypeAligned1 p x y

  Single-relationsip non-empty sequence

Totality: total
Visibility: export

singleton : p x y -> TypeAligned p x y

  Single-relations sequence

Totality: total
Visibility: export

consOnce : p x y -@ (TypeAligned1 p y z -@ TypeAligned1 p x z)

  Linear `cons`

Totality: total
Visibility: export

cons1Once : (1 _ : p x y) -> TypeAligned p y z -@ TypeAligned1 p x z

  Linear `cons1`

Totality: total
Visibility: export

consOnce : (1 _ : p x y) -> TypeAligned p y z -@ TypeAligned p x z

  Linear `cons`

Totality: total
Visibility: export

cons : p x y -> TypeAligned1 p y z -> TypeAligned1 p x z

  Add one relationship to the beginning

Totality: total
Visibility: export

(::) : p x y -> TypeAligned1 p y z -> TypeAligned1 p x z

  Add one relationship to the beginning

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

cons1 : p x y -> TypeAligned p y z -> TypeAligned1 p x z

  cons is non-empty

Totality: total
Visibility: export

cons : p x y -> TypeAligned p y z -> TypeAligned p x z

  Add one relationship to the beginning

Totality: total
Visibility: export

(::) : p x y -> TypeAligned p y z -> TypeAligned p x z

  Add one relationship to the beginning

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

unconsOnce : (1 ne : TypeAligned1 p w z) -> LPair (p w (ne .x)) (TypeAligned p (ne .x) z)

  Linear `uncons`

Totality: total
Visibility: export

unconsOnce : (1 ta : TypeAligned p w z) -> LEither (w = z) (LPair (p w (ta .x)) (TypeAligned p (ta .x) z))

  Instead of Nothing, failure to uncons proves index equality

Totality: total
Visibility: export

uncons : (ne : TypeAligned1 p w z) -> (p w (ne .x), TypeAligned p (ne .x) z)

  View/remove the leftmost (first) primitive

Totality: total
Visibility: export

tail : (ne : TypeAligned1 p w z) -> TypeAligned p (ne .x) z

  Drop the first primitive

Totality: total
Visibility: export

uncons : (ta : TypeAligned p w z) -> Either (w = z) (p w (ta .x), TypeAligned p (ta .x) z)

  Instead of Nothing, failure to uncons proves index equality

Totality: total
Visibility: export

head : (ta : TypeAligned p w z) -> Either (w = z) (p w (ta .x))

  Extract the first primitive, if none prove index equality

Totality: total
Visibility: export

tail : (ta : TypeAligned p w z) -> Either (w = z) (TypeAligned p (ta .x) z)

  Drop the first prinitive, if none prove index equality

Totality: total
Visibility: export

heqCons : (p w x -> p y z -> Bool) -> TypeAligned1 p w x -> TypeAligned1 p y z -> Bool

  Equality test like a non-empty list

Totality: total
Visibility: export

heqCons : (p w x -> p y z -> Bool) -> TypeAligned p w x -> TypeAligned p y z -> Bool

  Equality test like a list

Totality: total
Visibility: export

snocOnce : TypeAligned1 p x y -@ (p y z -@ TypeAligned1 p x z)

  Linear `snoc`

Totality: total
Visibility: export

snoc1Once : TypeAligned p x y -@ (p y z -@ TypeAligned1 p x z)

  Linear `snoc1`

Totality: total
Visibility: export

snocOnce : TypeAligned p x y -@ (p y z -@ TypeAligned p x z)

  Linear `snoc`

Totality: total
Visibility: export

snoc : TypeAligned1 p x y -> p y z -> TypeAligned1 p x z

  Add one relationship to the right

Totality: total
Visibility: export

(:<) : TypeAligned1 p x y -> p y z -> TypeAligned1 p x z

  Add one relationship to the right

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 7

snoc1 : TypeAligned p x y -> p y z -> TypeAligned1 p x z

  snoc guarantees a non-empty result

Totality: total
Visibility: export

snoc : TypeAligned p x y -> p y z -> TypeAligned p x z

  Add one relationship to the right

Totality: total
Visibility: export

(:<) : TypeAligned p x y -> p y z -> TypeAligned p x z

  Add one relationship to the right

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 7

unsnocOnce : (1 ne : TypeAligned1 p w z) -> LPair (TypeAligned p w (ne .y)) (p (ne .y) z)

  Linear `unsnoc`

Totality: total
Visibility: export

unsnocOnce : (1 ta : TypeAligned p w z) -> LEither (w = z) (LPair (TypeAligned p w (ta .y)) (p (ta .y) z))

  Linear `unsnoc`

Totality: total
Visibility: export

unsnoc : (ne : TypeAligned1 p w z) -> (TypeAligned p w (ne .y), p (ne .y) z)

  View/remove rightmost (last) relationship

Totality: total
Visibility: export

init : (ne : TypeAligned1 p w z) -> TypeAligned p w (ne .y)

  Drop last relationship

Totality: total
Visibility: export

unsnoc : (ta : TypeAligned p w z) -> Either (w = z) (TypeAligned p w (ta .y), p (ta .y) z)

  Rather than Nothing, failure to unsnoc proves index equality.

Totality: total
Visibility: export

init : (ta : TypeAligned p w z) -> Either (w = z) (TypeAligned p w (ta .y))

  Drop last relationship, if none prove index equality.

Totality: total
Visibility: export

last : (ta : TypeAligned p w z) -> Either (w = z) (p (ta .y) z)

  Extract last relationship, if none prove index equality.

Totality: total
Visibility: export

heqSnoc : (p w x -> p y z -> Bool) -> TypeAligned1 p w x -> TypeAligned1 p y z -> Bool

  Equality test like a non-empty snoc list

Totality: total
Visibility: export

heqSnoc : (p w x -> p y z -> Bool) -> TypeAligned p w x -> TypeAligned p y z -> Bool

  Equality test like a snoc list

Totality: total
Visibility: export

appendOnce : TypeAligned p x y -@ (TypeAligned p y z -@ TypeAligned p x z)

  Linear `append`

Totality: total
Visibility: export

appendOnce : TypeAligned1 p x y -@ (TypeAligned1 p y z -@ TypeAligned1 p x z)

  Linear `append`

Totality: total
Visibility: export

append : TypeAligned1 p x y -> TypeAligned1 p y z -> TypeAligned1 p x z

  Join two TypeAligned1 sequences

Totality: total
Visibility: export

(++) : TypeAligned1 p x y -> TypeAligned1 p y z -> TypeAligned1 p x z

  Join two TypeAligned1 sequences

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

append : TypeAligned p x y -> TypeAligned p y z -> TypeAligned p x z

  Join two TypeAligned sequences

Totality: total
Visibility: export

(++) : TypeAligned p x y -> TypeAligned p y z -> TypeAligned p x z

  Join two TypeAligned sequences

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

mapReduceOnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q x y -@ (q y z -@ q x z) -> TypeAligned1 p x y -@ q (f x) (f y)

  Linear `mapReduce`

Totality: total
Visibility: export

mapReduceLOnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q x y -@ (q y z -@ q x z) -> q (f x) (f x) -> TypeAligned p x y -@ q (f x) (f y)

  Linear `mapReduceL`

Totality: total
Visibility: export

mapReduceROnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q x y -@ (q y z -@ q x z) -> q (f y) (f y) -> TypeAligned p x y -@ q (f x) (f y)

  Linear `mapReduceR`

Totality: total
Visibility: export

mapReduce : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> (q x y -> q y z -> q x z) -> TypeAligned1 p x y -> q (f x) (f y)

  Reduce while transforming to a different primitive.

Totality: total
Visibility: export

mapReduceL : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> (q x y -> q y z -> q x z) -> q (f x) (f x) -> TypeAligned p x y -> q (f x) (f y)

  Reduce from the left while transforming.

Totality: total
Visibility: export

mapReduceR : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> (q x y -> q y z -> q x z) -> q (f y) (f y) -> TypeAligned p x y -> q (f x) (f y)

  Reduce from the right while transforming.

Totality: total
Visibility: export

mapOnce : {0 f : a -> b} -> p x y -@ q (f x) (f y) -> TypeAligned p x y -@ TypeAligned q (f x) (f y)

  Linear `map`

Totality: total
Visibility: export

mapOnce : {0 f : a -> b} -> p x y -@ q (f x) (f y) -> TypeAligned1 p x y -@ TypeAligned1 q (f x) (f y)

  Linear `map`

Totality: total
Visibility: export

map : {0 f : a -> b} -> (p x y -> q (f x) (f y)) -> TypeAligned p x y -> TypeAligned q (f x) (f y)

  Change inner relation

Totality: total
Visibility: export

map : {0 f : a -> b} -> (p x y -> q (f x) (f y)) -> TypeAligned1 p x y -> TypeAligned1 q (f x) (f y)

  Change inner relation

Totality: total
Visibility: export

reduceOnce : p x y -@ (p y z -@ p x z) -> TypeAligned1 p x y -@ p x y

  Linear `reduce`

Totality: total
Visibility: export

reduceLOnce : p x y -@ (p y z -@ p x z) -> p x x -> TypeAligned p x y -@ p x y

  Linear `reduceL`

Totality: total
Visibility: export

reduceROnce : p x y -@ (p y z -@ p x z) -> p y y -> TypeAligned p x y -@ p x y

  Linear `reduceR`

Totality: total
Visibility: export

reduce : (p x y -> p y z -> p x z) -> TypeAligned1 p x y -> p x y

  Reduce to a single primitive.

Totality: total
Visibility: export

reduceL : (p x y -> p y z -> p x z) -> p x x -> TypeAligned p x y -> p x y

  Reduce from the left.

Totality: total
Visibility: export

reduceR : (p x y -> p y z -> p x z) -> p y y -> TypeAligned p x y -> p x y

  Reduce from the right.

Totality: total
Visibility: export