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