1  /-
 2    Cornell - Verified Parsing at Three Power Levels
 3    
 4    Named after Joseph Cornell's shadow boxes from Count Zero.
 5    
 6    ## Parser Power Hierarchy
 7    
 8    ```
 9    Box < Scanner < Parser
10    ```
11    
12    - **Box** (LL(0) + dep): Bidirectional codecs for binary formats
13      - Roundtrip proof: `parse (serialize a) = a`
14      - Consumption proof: `parse (serialize a ++ extra) = (a, extra)`
15      - Use for: Git pack, protobuf, Nix wire, binary formats
16    
17    - **Scanner** (LL(0) + delimiters): One-way parsing for text protocols
18      - Delimiter-based: scan until `\r\n`, `:`, etc.
19      - Uniqueness proof: at most one parse result
20      - Use for: HTTP/1.1, PEM, CSV, line protocols
21    
22    - **Parser** (LL(k)): Grammar-based parsing for structured text
23      - Explicit lookahead, ordered choice
24      - Unambiguity proof, FIRST/FOLLOW analysis
25      - Use for: JSON, YAML, config files, DSLs
26    
27    ## Embedding
28    
29    Each level can embed the one below:
30    - `Scanner.fromBox`: Use a Box within a Scanner
31    - `Parser.fromScanner`: Use a Lexer (Scanner) to produce tokens
32    
33    ## Modules
34    
35    - `Cornell.Basic`: Box primitives and combinators
36    - `Cornell.Scanner`: Delimiter-based text scanning
37    - `Cornell.Parser`: LL(k) grammar parsing
38    - `Cornell.Nix`: Nix daemon wire format
39    - `Cornell.Protobuf`: Protobuf/gRPC wire format
40    - `Cornell.StateMachine`: Verified protocol state machines
41  -/
42  
43  import Cornell.Basic
44  import Cornell.Scanner
45  import Cornell.Parser
46  import Cornell.Nix
47  import Cornell.Protobuf
48  import Cornell.StateMachine
49  
50  namespace Cornell
51  
52  -- Re-export key types from each power level
53  
54  -- Box (LL(0) + dep, bidirectional, binary)
55  export Cornell (
56    Bytes
57    ParseResult
58    Box
59    unit u8 u16le u32le u64le bool64
60    seq isoMap dep
61    listN arrayN
62    parseList serializeList
63  )
64  
65  -- Scanner (LL(0) + delimiters, one-way, text)
66  export Cornell.Scanner (
67    ScanResult
68    Scanner
69    scanLine scanCRLFLine
70    scanUntilByte scanUntilBytes
71    scanWhile scanUntil
72    scanDigits scanAlphaNum skipWhitespace
73    exact exactByte
74    fromBox boxThen
75  )
76  
77  -- Parser (LL(k), grammar-based)
78  export Cornell.Parser (
79    Token TokenStream
80    PResult
81    Parser Parser1 Parser2
82    token satisfy anyToken eof
83    lookAhead notFollowedBy
84    optional many many1
85    sepBy sepBy1 between
86    Lexer mkLexer fromScanner
87  )
88  
89  end Cornell