Idris2Doc : FASTA.Parser

FASTA.Parser

(source)
Reexports
import public Text.ILex
Definitions
data CoordinateSystem : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ZeroBased : CoordinateSystem
  
OneBased : CoordinateSystem

  Hints:
  
Eq CoordinateSystem
  
Show CoordinateSystem
data FASTAValue : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NL : ByteString -> FASTAValue
  
HeaderStart : FASTAValue
  
HeaderValue : String -> FASTAValue
  
Adenine : Nat -> FASTAValue
  
Thymine : Nat -> FASTAValue
  
Guanine : Nat -> FASTAValue
  
Cytosine : Nat -> FASTAValue

  Hints:
  
Eq FASTAValue
  
Show FASTAValue
record FASTALine : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFASTALine : Nat -> List FASTAValue -> FASTALine

  Projections:
  
.nr : FASTALine -> Nat
  
.values : FASTALine -> List FASTAValue

  Hints:
  
Eq FASTALine
  
HasStack FSTCK (SnocList FASTALine)
  
Interpolation FASTALine
  
Show FASTALine
.nr : FASTALine -> Nat
  Totality: total
  Visibility: public export
nr : FASTALine -> Nat
  Totality: total
  Visibility: public export
.values : FASTALine -> List FASTAValue
  Totality: total
  Visibility: public export
values : FASTALine -> List FASTAValue
  Totality: total
  Visibility: public export
0 FASTA : Type
  Totality: total
  Visibility: public export
record FSTCK : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
F : (bufSize_ : Nat) -> ByteString -> IBuffer bufSize_ -> Nat -> Nat -> Ref q (LTENat bufSize_) -> Ref q (LTENat bufSize_) -> Ref q (SnocList BytePos) -> Ref q (SnocList String) -> Ref q (Maybe (BBErr Void)) -> Ref q (SnocList FASTAValue) -> Ref q (SnocList FASTALine) -> Ref q Nat -> Ref q Nat -> FSTCK q

  Projections:
  
.bufSize_ : FSTCK q -> Nat
  
.curOffset_ : FSTCK q -> Nat
  
.cur_ : ({rec:0} : FSTCK q) -> IBuffer (bufSize_ {rec:0})
  
.err : FSTCK q -> Ref q (Maybe (BBErr Void))
  
.fastacounter : FSTCK q -> Ref q Nat
  
.fastalines : FSTCK q -> Ref q (SnocList FASTALine)
  
.fastavalues : FSTCK q -> Ref q (SnocList FASTAValue)
  
.from_ : ({rec:0} : FSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  
.line : FSTCK q -> Ref q Nat
  
.positions_ : FSTCK q -> Ref q (SnocList BytePos)
  
.prevOffset_ : FSTCK q -> Nat
  
.prev_ : FSTCK q -> ByteString
  
.strs : FSTCK q -> Ref q (SnocList String)
  
.till_ : ({rec:0} : FSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))

  Hints:
  
HasBBErr FSTCK Void
  
HasBytes FSTCK
  
HasStack FSTCK (SnocList FASTALine)
  
HasStringLits FSTCK
.bufSize_ : FSTCK q -> Nat
  Totality: total
  Visibility: public export
bufSize_ : FSTCK q -> Nat
  Totality: total
  Visibility: public export
.prev_ : FSTCK q -> ByteString
  Totality: total
  Visibility: public export
prev_ : FSTCK q -> ByteString
  Totality: total
  Visibility: public export
.cur_ : ({rec:0} : FSTCK q) -> IBuffer (bufSize_ {rec:0})
  Totality: total
  Visibility: public export
cur_ : ({rec:0} : FSTCK q) -> IBuffer (bufSize_ {rec:0})
  Totality: total
  Visibility: public export
.prevOffset_ : FSTCK q -> Nat
  Totality: total
  Visibility: public export
prevOffset_ : FSTCK q -> Nat
  Totality: total
  Visibility: public export
.curOffset_ : FSTCK q -> Nat
  Totality: total
  Visibility: public export
curOffset_ : FSTCK q -> Nat
  Totality: total
  Visibility: public export
.from_ : ({rec:0} : FSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
from_ : ({rec:0} : FSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
.till_ : ({rec:0} : FSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
till_ : ({rec:0} : FSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
.positions_ : FSTCK q -> Ref q (SnocList BytePos)
  Totality: total
  Visibility: public export
positions_ : FSTCK q -> Ref q (SnocList BytePos)
  Totality: total
  Visibility: public export
.strs : FSTCK q -> Ref q (SnocList String)
  Totality: total
  Visibility: public export
strs : FSTCK q -> Ref q (SnocList String)
  Totality: total
  Visibility: public export
.err : FSTCK q -> Ref q (Maybe (BBErr Void))
  Totality: total
  Visibility: public export
err : FSTCK q -> Ref q (Maybe (BBErr Void))
  Totality: total
  Visibility: public export
.fastavalues : FSTCK q -> Ref q (SnocList FASTAValue)
  Totality: total
  Visibility: public export
fastavalues : FSTCK q -> Ref q (SnocList FASTAValue)
  Totality: total
  Visibility: public export
.fastalines : FSTCK q -> Ref q (SnocList FASTALine)
  Totality: total
  Visibility: public export
fastalines : FSTCK q -> Ref q (SnocList FASTALine)
  Totality: total
  Visibility: public export
.fastacounter : FSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
fastacounter : FSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
.line : FSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
line : FSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
fastainit : CoordinateSystem -> (n : Nat) -> IBuffer n -> F1 q (FSTCK q)
  Totality: total
  Visibility: export
fasta : CoordinateSystem -> P1 q (BBErr Void) FASTA
  Totality: total
  Visibility: public export
parseFASTA : CoordinateSystem -> Origin -> String -> Either (ParseError Void) FASTA
  Totality: total
  Visibility: export