
   0 | module FASTA.Parser
   1 | 
   2 | import Data.Bits
   3 | import Data.Buffer
   4 | import Data.ByteString
   5 | import Data.Linear.Ref1
   6 | import Derive.Prelude
   7 | import FS.Posix
   8 | import IO.Async.Loop.Epoll
   9 | import IO.Async.Loop.Posix
  10 | import Syntax.T1
  11 | import Text.ILex.Derive
  12 | import Text.ILex.FS
  13 | 
  14 | import public Text.ILex
  15 | 
  16 | %default total
  17 | %language ElabReflection
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | --          Coordinate System
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | public export
  24 | data CoordinateSystem = ZeroBased
  25 |                       | OneBased
  26 | 
  27 | %runElab derive "CoordinateSystem" [Show,Eq]
  28 | 
  29 | --------------------------------------------------------------------------------
  30 | --          FASTAValue
  31 | --------------------------------------------------------------------------------
  32 | 
  33 | public export
  34 | data FASTAValue : Type where
  35 |   NL          : ByteString -> FASTAValue
  36 |   HeaderStart : FASTAValue
  37 |   HeaderValue : String -> FASTAValue
  38 |   Adenine     : Nat -> FASTAValue
  39 |   Thymine     : Nat -> FASTAValue
  40 |   Guanine     : Nat -> FASTAValue
  41 |   Cytosine    : Nat -> FASTAValue
  42 | 
  43 | %runElab derive "FASTAValue" [Show,Eq]
  44 | 
  45 | isHeader : FASTAValue -> Bool
  46 | isHeader HeaderStart     = True
  47 | isHeader (HeaderValue _) = True
  48 | isHeader _               = False
  49 | 
  50 | isData : FASTAValue -> Bool
  51 | isData (Adenine _)  = True
  52 | isData (Thymine _)  = True
  53 | isData (Guanine _)  = True
  54 | isData (Cytosine _) = True
  55 | isData _            = False
  56 | 
  57 | --------------------------------------------------------------------------------
  58 | --          FASTALine
  59 | --------------------------------------------------------------------------------
  60 | 
  61 | public export
  62 | record FASTALine where
  63 |   constructor MkFASTALine
  64 |   nr     : Nat
  65 |   values : List FASTAValue
  66 | 
  67 | %runElab derive "FASTALine" [Show,Eq]
  68 | 
  69 | Interpolation FASTALine where interpolate = show
  70 | 
  71 | --------------------------------------------------------------------------------
  72 | --          FASTA
  73 | --------------------------------------------------------------------------------
  74 | 
  75 | public export
  76 | 0 FASTA : Type
  77 | FASTA = List FASTALine
  78 | 
  79 | --------------------------------------------------------------------------------
  80 | --          RExp
  81 | --------------------------------------------------------------------------------
  82 | 
  83 | linebreak : RExp True
  84 | linebreak = '\n' <|> '\r' <|> "\r\n"
  85 | 
  86 | nucleotide : RExp True
  87 | nucleotide = 'A' <|> 'T' <|> 'G' <|> 'C'
  88 | 
  89 | adenine : RExp True
  90 | adenine = 'A'
  91 | 
  92 | thymine : RExp True
  93 | thymine = 'T'
  94 | 
  95 | guanine : RExp True
  96 | guanine = 'G'
  97 | 
  98 | cytosine : RExp True
  99 | cytosine = 'C'
 100 | 
 101 | --------------------------------------------------------------------------------
 102 | --          Parser State
 103 | --------------------------------------------------------------------------------
 104 | 
 105 | public export
 106 | record FSTCK (q : Type) where
 107 |   constructor F
 108 |   bufSize_     : Nat
 109 |   prev_        : ByteString
 110 |   cur_         : IBuffer bufSize_
 111 |   prevOffset_  : Nat
 112 |   curOffset_   : Nat
 113 |   from_        : Ref q (LTENat bufSize_)
 114 |   till_        : Ref q (LTENat bufSize_)
 115 |   positions_   : Ref q (SnocList BytePos)
 116 |   strs         : Ref q (SnocList String)
 117 |   err          : Ref q (Maybe $ BBErr Void)
 118 |   fastavalues  : Ref q (SnocList FASTAValue)
 119 |   fastalines   : Ref q (SnocList FASTALine)
 120 |   fastacounter : Ref q Nat
 121 |   line         : Ref q Nat
 122 | 
 123 | export %inline
 124 | HasBBErr FSTCK Void where
 125 |   error = err
 126 | 
 127 | export %inline
 128 | HasStringLits FSTCK where
 129 |   strings = strs
 130 | 
 131 | export %inline
 132 | HasStack FSTCK (SnocList FASTALine) where
 133 |   stack = fastalines
 134 | 
 135 | export %inline
 136 | HasBytes FSTCK where
 137 |   bufSize    = bufSize_
 138 |   prev       = prev_
 139 |   cur        = cur_
 140 |   prevOffset = prevOffset_
 141 |   curOffset  = curOffset_
 142 |   from       = from_
 143 |   till       = till_
 144 |   positions  = positions_
 145 |   copy s o bs buf rf rt sk =
 146 |     { bufSize_    := s
 147 |     , cur_        := buf
 148 |     , prev_       := bs
 149 |     , prevOffset_ := o
 150 |     , curOffset_  := o + bs.size
 151 |     , from_       := rf
 152 |     , till_       := rt
 153 |     } sk
 154 | 
 155 | export
 156 | fastainit : CoordinateSystem -> (n : Nat) -> IBuffer n -> F1 q (FSTCK q)
 157 | fastainit coordsys n buf = T1.do
 158 |   rf <- ref1 (first n)
 159 |   rt <- ref1 (first n)
 160 |   ps <- ref1 [<]
 161 |   ss <- ref1 [<]
 162 |   er <- ref1 Nothing
 163 |   fvs <- ref1 [<]
 164 |   fls <- ref1 [<]
 165 |   ln  <- ref1 Z
 166 |   fc <- case coordsys of
 167 |           ZeroBased => ref1 Z
 168 |           OneBased => ref1 (S Z)
 169 |   by <- ref1 ""
 170 |   pure (F n empty buf 0 0 rf rt ps ss er fvs fls fc ln)
 171 | 
 172 | --------------------------------------------------------------------------------
 173 | --          Parser State
 174 | --------------------------------------------------------------------------------
 175 | 
 176 | %runElab deriveParserState "FSz" "FST"
 177 |   ["FIni", "FBroken", "FHdr", "FHdrToNLR", "FHdrToNLS", "FHdrDone", "FD", "FDNL", "FEmpty", "FComplete"]
 178 | 
 179 | --------------------------------------------------------------------------------
 180 | --          Errors
 181 | --------------------------------------------------------------------------------
 182 | 
 183 | fastaErr : Arr32 FSz (FSTCK q -> F1 q (BBErr Void))
 184 | fastaErr =
 185 |   arr32 FSz (unexpected [])
 186 |     [ E FBroken $ unexpected ["character other than '>'"]
 187 |     , E FEmpty $ unexpected ["sequence data"]
 188 |     , E FHdr $ unexpected ["sequence line"]
 189 |     ]
 190 | 
 191 | --------------------------------------------------------------------------------
 192 | --          State Transitions
 193 | --------------------------------------------------------------------------------
 194 | 
 195 | onFASTAValueHdrS : (x : FSTCK q) => FASTAValue -> F1 q FST
 196 | onFASTAValueHdrS v = push1 x.fastavalues v >> pure FHdrToNLS
 197 | 
 198 | onFASTAValueHdrR : (x : FSTCK q) => FASTAValue -> F1 q FST
 199 | onFASTAValueHdrR v = push1 x.fastavalues v >> pure FHdrToNLR
 200 | 
 201 | onFASTAValueAdenine : (x : FSTCK q) => F1 q FST
 202 | onFASTAValueAdenine = T1.do
 203 |   fc <- read1 x.fastacounter
 204 |   push1 x.fastavalues (Adenine fc) >> write1 x.fastacounter (S fc) >> pure FD
 205 | 
 206 | onFASTAValueThymine : (x : FSTCK q) => F1 q FST
 207 | onFASTAValueThymine = T1.do
 208 |   fc <- read1 x.fastacounter
 209 |   push1 x.fastavalues (Thymine fc) >> write1 x.fastacounter (S fc) >> pure FD
 210 | 
 211 | onFASTAValueGuanine : (x : FSTCK q) => F1 q FST
 212 | onFASTAValueGuanine = T1.do
 213 |   fc <- read1 x.fastacounter
 214 |   push1 x.fastavalues (Guanine fc) >> write1 x.fastacounter (S fc) >> pure FD
 215 | 
 216 | onFASTAValueCytosine : (x : FSTCK q) => F1 q FST
 217 | onFASTAValueCytosine = T1.do
 218 |   fc <- read1 x.fastacounter
 219 |   push1 x.fastavalues (Cytosine fc) >> write1 x.fastacounter (S fc) >> pure FD
 220 | 
 221 | onNLFHdr : (x : FSTCK q) => ByteString -> F1 q FST
 222 | onNLFHdr v = T1.do
 223 |   mod1 x.line S
 224 |   push1 x.fastavalues (NL v)
 225 |   fvs@(_::_) <- getList x.fastavalues | [] => pure FEmpty
 226 |   case Prelude.any isHeader fvs && Prelude.any isData fvs of
 227 |     True  => pure FBroken
 228 |     False => T1.do
 229 |       ln <- read1 x.line
 230 |       push1 x.fastalines (MkFASTALine ln fvs)
 231 |       pure FHdrDone
 232 | 
 233 | onNLFD : (x : FSTCK q) => ByteString -> F1 q FST
 234 | onNLFD v = T1.do
 235 |   mod1 x.line S
 236 |   push1 x.fastavalues (NL v)
 237 |   fvs@(_::_) <- getList x.fastavalues | [] => pure FEmpty
 238 |   case Prelude.any isHeader fvs && Prelude.any isData fvs of
 239 |     True  => pure FBroken
 240 |     False => T1.do
 241 |       ln <- read1 x.line
 242 |       push1 x.fastalines (MkFASTALine ln fvs)
 243 |       pure FDNL
 244 | 
 245 | onEOI : (x : FSTCK q) => F1 q (Either (BBErr Void) FST)
 246 | onEOI = T1.do
 247 |   mod1 x.line S
 248 |   fvs@(_::_) <- getList x.fastavalues
 249 |     | [] => arrFail FSTCK fastaErr FEmpty x
 250 |   ln <- read1 x.line
 251 |   push1 x.fastalines (MkFASTALine ln fvs)
 252 |   pure (Right FComplete)
 253 | 
 254 | fastaInit : DFA q FSz FSTCK
 255 | fastaInit =
 256 |   dfa
 257 |     [ string '>' (\_ => onFASTAValueHdrS HeaderStart)
 258 |     ]
 259 | 
 260 | fastaHdrStrStart : DFA q FSz FSTCK
 261 | fastaHdrStrStart =
 262 |   dfa
 263 |     [ string dot (onFASTAValueHdrR . HeaderValue)
 264 |     ]
 265 | 
 266 | fastaHdrStrRest : DFA q FSz FSTCK
 267 | fastaHdrStrRest =
 268 |   dfa
 269 |     [ string dot (onFASTAValueHdrR . HeaderValue)
 270 |     , bytes linebreak (\bs => onNLFHdr bs)
 271 |     ]
 272 | 
 273 | fastaFDInit : DFA q FSz FSTCK
 274 | fastaFDInit =
 275 |   dfa
 276 |     [ step adenine onFASTAValueAdenine
 277 |     , step thymine onFASTAValueThymine
 278 |     , step guanine onFASTAValueGuanine
 279 |     , step cytosine onFASTAValueCytosine
 280 |     ]
 281 | 
 282 | fastaFD : DFA q FSz FSTCK
 283 | fastaFD =
 284 |   dfa
 285 |     [ bytes linebreak onNLFD
 286 |     , step adenine onFASTAValueAdenine
 287 |     , step thymine onFASTAValueThymine
 288 |     , step guanine onFASTAValueGuanine
 289 |     , step cytosine onFASTAValueCytosine
 290 |     ]
 291 | 
 292 | fastaSteps : Lex1 q FSz FSTCK
 293 | fastaSteps =
 294 |   lex1
 295 |     [ E FIni fastaInit
 296 |     , E FHdrToNLS fastaHdrStrStart
 297 |     , E FHdrToNLR fastaHdrStrRest
 298 |     , E FHdrDone fastaFDInit
 299 |     , E FDNL fastaFDInit
 300 |     , E FD fastaFD
 301 |     ]
 302 | 
 303 | fastaEOI : FST -> FSTCK q -> F1 q (Either (BBErr Void) FASTA)
 304 | fastaEOI st x =
 305 |   case st == FIni || st == FHdr || st == FEmpty || st == FBroken of
 306 |     True  => arrFail FSTCK fastaErr st x
 307 |     False => T1.do
 308 |       _ <- onEOI
 309 |       fasta <- getList x.fastalines
 310 |       pure (Right fasta)
 311 | 
 312 | --------------------------------------------------------------------------------
 313 | --          Parser
 314 | --------------------------------------------------------------------------------
 315 | 
 316 | public export
 317 | fasta : CoordinateSystem -> P1 q (BBErr Void) FASTA
 318 | fasta coordsys = P FIni (fastainit coordsys) fastaSteps snocChunk fastaErr fastaEOI
 319 | 
 320 | export %inline
 321 | parseFASTA : CoordinateSystem -> Origin -> String -> Either (ParseError Void) FASTA
 322 | parseFASTA coordsys origin str = parseString (fasta coordsys) origin str
 323 | 
 324 | --------------------------------------------------------------------------------
 325 | --          Streaming
 326 | --------------------------------------------------------------------------------
 327 | 
 328 | streamFASTA :  CoordinateSystem
 329 |             -> String
 330 |             -> AsyncPull Poll Void [BBErr Void, Errno] ()
 331 | streamFASTA coordsys pth =
 332 |      readBytes pth
 333 |   |> streamParse (fasta coordsys)
 334 |   |> C.count
 335 |   |> printLnTo Stdout
 336 | 
 337 | streamFASTAFiles :  CoordinateSystem
 338 |                  -> AsyncPull Poll String [BBErr Void, Errno] ()
 339 |                  -> AsyncPull Poll Void [BBErr Void, Errno] ()
 340 | streamFASTAFiles coordsys pths =
 341 |      flatMap pths (\p => readBytes p |> streamParse (fasta coordsys))
 342 |   |> C.count
 343 |   |> printLnTo Stdout
 344 |