
   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 |   prev_        : Ref q ByteString
 109 |   cur_         : Ref q ByteString
 110 |   offset_      : Ref q Nat
 111 |   relpos_      : Ref q Integer
 112 |   len_         : Ref q Nat
 113 |   positions_   : Ref q (SnocList BytePos)
 114 |   strs         : Ref q (SnocList String)
 115 |   err          : Ref q (Maybe $ BBErr Void)
 116 |   fastavalues  : Ref q (SnocList FASTAValue)
 117 |   fastalines   : Ref q (SnocList FASTALine)
 118 |   fastacounter : Ref q Nat
 119 |   line         : Ref q Nat
 120 | 
 121 | export %inline
 122 | HasBBErr FSTCK Void where
 123 |   error = err
 124 | 
 125 | export %inline
 126 | HasStringLits FSTCK where
 127 |   strings = strs
 128 | 
 129 | export %inline
 130 | HasStack FSTCK (SnocList FASTALine) where
 131 |   stack = fastalines
 132 | 
 133 | export %inline
 134 | HasBytes FSTCK where
 135 |   prev = prev_
 136 |   cur = cur_
 137 |   offset = offset_
 138 |   relpos = relpos_
 139 |   len = len_
 140 |   positions = positions_
 141 | 
 142 | export
 143 | fastainit : CoordinateSystem -> F1 q (FSTCK q)
 144 | fastainit coordsys = T1.do
 145 |   pr <- ref1 empty
 146 |   fl <- ref1 empty
 147 |   ro <- ref1 Z
 148 |   rr <- ref1 0
 149 |   ll <- ref1 Z
 150 |   ps <- ref1 [<]
 151 |   ss <- ref1 [<]
 152 |   er <- ref1 Nothing
 153 |   fvs <- ref1 [<]
 154 |   fls <- ref1 [<]
 155 |   ln  <- ref1 Z
 156 |   fc <- case coordsys of
 157 |           ZeroBased => ref1 Z
 158 |           OneBased => ref1 (S Z)
 159 |   by <- ref1 ""
 160 |   pure (F pr fl ro rr ll ps ss er fvs fls fc ln)
 161 | 
 162 | --------------------------------------------------------------------------------
 163 | --          Parser State
 164 | --------------------------------------------------------------------------------
 165 | 
 166 | %runElab deriveParserState "FSz" "FST"
 167 |   ["FIni", "FBroken", "FHdr", "FHdrToNLR", "FHdrToNLS", "FHdrDone", "FD", "FDNL", "FEmpty", "FComplete"]
 168 | 
 169 | --------------------------------------------------------------------------------
 170 | --          Errors
 171 | --------------------------------------------------------------------------------
 172 | 
 173 | fastaErr : Arr32 FSz (FSTCK q -> F1 q (BBErr Void))
 174 | fastaErr =
 175 |   arr32 FSz (unexpected [])
 176 |     [ E FBroken $ unexpected ["character other than '>'"]
 177 |     , E FEmpty $ unexpected ["sequence data"]
 178 |     , E FHdr $ unexpected ["sequence line"]
 179 |     ]
 180 | 
 181 | --------------------------------------------------------------------------------
 182 | --          State Transitions
 183 | --------------------------------------------------------------------------------
 184 | 
 185 | onFASTAValueHdrS : (x : FSTCK q) => FASTAValue -> F1 q FST
 186 | onFASTAValueHdrS v = push1 x.fastavalues v >> pure FHdrToNLS
 187 | 
 188 | onFASTAValueHdrR : (x : FSTCK q) => FASTAValue -> F1 q FST
 189 | onFASTAValueHdrR v = push1 x.fastavalues v >> pure FHdrToNLR
 190 | 
 191 | onFASTAValueAdenine : (x : FSTCK q) => F1 q FST
 192 | onFASTAValueAdenine = T1.do
 193 |   fc <- read1 x.fastacounter
 194 |   push1 x.fastavalues (Adenine fc) >> write1 x.fastacounter (S fc) >> pure FD
 195 | 
 196 | onFASTAValueThymine : (x : FSTCK q) => F1 q FST
 197 | onFASTAValueThymine = T1.do
 198 |   fc <- read1 x.fastacounter
 199 |   push1 x.fastavalues (Thymine fc) >> write1 x.fastacounter (S fc) >> pure FD
 200 | 
 201 | onFASTAValueGuanine : (x : FSTCK q) => F1 q FST
 202 | onFASTAValueGuanine = T1.do
 203 |   fc <- read1 x.fastacounter
 204 |   push1 x.fastavalues (Guanine fc) >> write1 x.fastacounter (S fc) >> pure FD
 205 | 
 206 | onFASTAValueCytosine : (x : FSTCK q) => F1 q FST
 207 | onFASTAValueCytosine = T1.do
 208 |   fc <- read1 x.fastacounter
 209 |   push1 x.fastavalues (Cytosine fc) >> write1 x.fastacounter (S fc) >> pure FD
 210 | 
 211 | onNLFHdr : (x : FSTCK q) => ByteString -> F1 q FST
 212 | onNLFHdr v = T1.do
 213 |   mod1 x.line S
 214 |   push1 x.fastavalues (NL v)
 215 |   fvs@(_::_) <- getList x.fastavalues | [] => pure FEmpty
 216 |   case Prelude.any isHeader fvs && Prelude.any isData fvs of
 217 |     True  => pure FBroken
 218 |     False => T1.do
 219 |       ln <- read1 x.line
 220 |       push1 x.fastalines (MkFASTALine ln fvs)
 221 |       pure FHdrDone
 222 | 
 223 | onNLFD : (x : FSTCK q) => ByteString -> F1 q FST
 224 | onNLFD v = T1.do
 225 |   mod1 x.line S
 226 |   push1 x.fastavalues (NL v)
 227 |   fvs@(_::_) <- getList x.fastavalues | [] => pure FEmpty
 228 |   case Prelude.any isHeader fvs && Prelude.any isData fvs of
 229 |     True  => pure FBroken
 230 |     False => T1.do
 231 |       ln <- read1 x.line
 232 |       push1 x.fastalines (MkFASTALine ln fvs)
 233 |       pure FDNL
 234 | 
 235 | onEOI : (x : FSTCK q) => F1 q (Either (BBErr Void) FST)
 236 | onEOI = T1.do
 237 |   mod1 x.line S
 238 |   fvs@(_::_) <- getList x.fastavalues
 239 |     | [] => arrFail FSTCK fastaErr FEmpty x
 240 |   ln <- read1 x.line
 241 |   push1 x.fastalines (MkFASTALine ln fvs)
 242 |   pure (Right FComplete)
 243 | 
 244 | fastaInit : DFA q FSz FSTCK
 245 | fastaInit =
 246 |   dfa
 247 |     [ string '>' (\_ => onFASTAValueHdrS HeaderStart)
 248 |     ]
 249 | 
 250 | fastaHdrStrStart : DFA q FSz FSTCK
 251 | fastaHdrStrStart =
 252 |   dfa
 253 |     [ string dot (onFASTAValueHdrR . HeaderValue)
 254 |     ]
 255 | 
 256 | fastaHdrStrRest : DFA q FSz FSTCK
 257 | fastaHdrStrRest =
 258 |   dfa
 259 |     [ string dot (onFASTAValueHdrR . HeaderValue)
 260 |     , bytes linebreak (\bs => onNLFHdr bs)
 261 |     ]
 262 | 
 263 | fastaFDInit : DFA q FSz FSTCK
 264 | fastaFDInit =
 265 |   dfa
 266 |     [ step adenine onFASTAValueAdenine
 267 |     , step thymine onFASTAValueThymine
 268 |     , step guanine onFASTAValueGuanine
 269 |     , step cytosine onFASTAValueCytosine
 270 |     ]
 271 | 
 272 | fastaFD : DFA q FSz FSTCK
 273 | fastaFD =
 274 |   dfa
 275 |     [ bytes linebreak onNLFD
 276 |     , step adenine onFASTAValueAdenine
 277 |     , step thymine onFASTAValueThymine
 278 |     , step guanine onFASTAValueGuanine
 279 |     , step cytosine onFASTAValueCytosine
 280 |     ]
 281 | 
 282 | fastaSteps : Lex1 q FSz FSTCK
 283 | fastaSteps =
 284 |   lex1
 285 |     [ E FIni fastaInit
 286 |     , E FHdrToNLS fastaHdrStrStart
 287 |     , E FHdrToNLR fastaHdrStrRest
 288 |     , E FHdrDone fastaFDInit
 289 |     , E FDNL fastaFDInit
 290 |     , E FD fastaFD
 291 |     ]
 292 | 
 293 | fastaEOI : FST -> FSTCK q -> F1 q (Either (BBErr Void) FASTA)
 294 | fastaEOI st x =
 295 |   case st == FIni || st == FHdr || st == FEmpty || st == FBroken of
 296 |     True  => arrFail FSTCK fastaErr st x
 297 |     False => T1.do
 298 |       _ <- onEOI
 299 |       fasta <- getList x.fastalines
 300 |       pure (Right fasta)
 301 | 
 302 | --------------------------------------------------------------------------------
 303 | --          Parser
 304 | --------------------------------------------------------------------------------
 305 | 
 306 | public export
 307 | fasta : CoordinateSystem -> P1 q (BBErr Void) FASTA
 308 | fasta coordsys = P FIni (fastainit coordsys) fastaSteps snocChunk fastaErr fastaEOI
 309 | 
 310 | export %inline
 311 | parseFASTA : CoordinateSystem -> Origin -> String -> Either (ParseError Void) FASTA
 312 | parseFASTA coordsys origin str = parseString (fasta coordsys) origin str
 313 | 
 314 | --------------------------------------------------------------------------------
 315 | --          Streaming
 316 | --------------------------------------------------------------------------------
 317 | 
 318 | streamFASTA :  CoordinateSystem
 319 |             -> String
 320 |             -> AsyncPull Poll Void [BBErr Void, Errno] ()
 321 | streamFASTA coordsys pth =
 322 |      readBytes pth
 323 |   |> streamParse (fasta coordsys)
 324 |   |> C.count
 325 |   |> printLnTo Stdout
 326 | 
 327 | streamFASTAFiles :  CoordinateSystem
 328 |                  -> AsyncPull Poll String [BBErr Void, Errno] ()
 329 |                  -> AsyncPull Poll Void [BBErr Void, Errno] ()
 330 | streamFASTAFiles coordsys pths =
 331 |      flatMap pths (\p => readBytes p |> streamParse (fasta coordsys))
 332 |   |> C.count
 333 |   |> printLnTo Stdout
 334 |