• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
        • Proof-support
        • Abstract-syntax
        • R1cs-subset
        • Semantics
        • Abstract-syntax-operations
        • Indexed-names
        • Well-formedness
        • Concrete-syntax
          • Lexer
          • Grammar
          • Parser
          • Tokenizer
        • R1cs-bridge
        • Parser-interface
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Pfcs

Concrete-syntax

Concrete syntax of PFCSes.

We define a concrete syntax of PFCSes to ease reading and writing them. We define the syntax via an ABNF grammar, which we plan to complete with a declarative specification of parsing of PFCSes according to the grammar. We define an executable lexer, tokenizer, and parser to CSTs (concrete syntax trees).

Subtopics

Lexer
An executable lexer of PFCS.
Grammar
ABNF grammar for PFCSes.
Parser
An executable parser of PFCS.
Tokenizer
Turn lexemes into tokens.