core.bend checks

raw source on the hub · import 0x64aa7934c3659ee6a818595494b38921/core.bend as Core

Fast CSV parser with proofs

1 import

import Base

Types

type Ans source · line 13 · raw

Data

Parsed
```
@rows:List<&2, List<&2, String>> -> Ans
```
Rejected
```
Ans
```

type CK source · line 18 · raw

Data

character class: all nullary, so a class is a shared constant, never allocated

CLf
```
CK
```
CCr
```
CK
```
CSep
```
CK
```
CQuote
```
CK
```
CText
```
CK
```

type FM source · line 30 · raw

Data

mode: S = at field start, B = in bare field, E = in escaped field, Q = just after a quote in an escaped field; SC/BC/QC = the same with one CR held back (it is content only if the next char continues the record). MBad is never built by this file: the walk rejects a bad pair at once. It is the rejected state that PROOF.bend reasons about.

MS
```
FM
```
MB
```
FM
```
ME
```
FM
```
MQ
```
FM
```
MSC
```
FM
```
MBC
```
FM
```
MQC
```
FM
```
MBad
```
FM
```

Definitions

def cls_go source · line 40 · raw

@+lf:Bool -> @+cr:Bool -> @+sep:Bool -> @+quote:Bool -> CK

def cls_u source · line 59 · raw

@+sep:U32 -> @+u:U32 -> CK

def cls source · line 62 · raw

@+sep:U32 -> @+c:Char -> CK

def close_empty source · line 65 · raw

@+flds:List<&2, String> -> @+rows:List<&2, List<&2, String>> -> List<&2, List<&2, String>>

def row source · line 72 · raw

@+txt:String -> @+flds:List<&2, String> -> @+rows:List<&2, List<&2, String>> -> List<&2, List<&2, String>>

def one source · line 75 · raw

@+c:Char -> String

def fin source · line 78 · raw

@+m:FM -> @+txt:String -> @+flds:List<&2, String> -> @+rows:List<&2, List<&2, String>> -> Ans

def cls_of source · line 98 · raw

@+sep:U32 -> @+s:String -> CK

class of the first character of a string (CText for the empty string: unused)

def go source · line 108 · raw

@+s:String -> @+m:FM -> @+k:CK -> @+sep:U32 -> @+txt:String -> @+flds:List<&2, String> -> @+rows:List<&2, List<&2, String>> -> Ans

the one walk: input first (it shrinks), then mode, then the class of the head character (computed once, by the caller), then everything else. ONE match on (input, mode, class) per character; a rejecting pair returns at once.

def parse_sep source · line 177 · raw

@+sep:U32 -> @+s:String -> Ans

def parse source · line 180 · raw

@+s:String -> Ans