• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
        • Pdf-example
        • Smtp-example
        • Imap-example
        • Http-example
        • Uri-example
          • *all-uri-grammar-rules*
          • Uri-cst-path-conc?
          • Uri-cst-host-conc?
          • Uri-cst-uri-reference-conc?
          • Uri-cst-list-list-conc-matchp$
          • Uri-cst-list-list-alt-matchp$
          • Uri-cst-reserved-conc?
          • Uri-cst-list-rep-matchp$
          • Uri-cst-list-elem-matchp$
          • Uri-cst-uri-reference-conc2-rep-elem
          • Uri-cst-uri-reference-conc2-rep
          • Uri-cst-uri-reference-conc1-rep-elem
          • Uri-cst-uri-reference-conc1-rep
          • Uri-cst-matchp$
          • Uri-cst-uri-reference-conc2
          • Uri-cst-uri-reference-conc1
          • Uri-cst-reserved-conc2-rep-elem
          • Uri-cst-reserved-conc2-rep
          • Uri-cst-reserved-conc1-rep-elem
          • Uri-cst-reserved-conc1-rep
          • Uri-cst-segment-nz-nc-conc
          • Uri-cst-reserved-conc2
          • Uri-cst-reserved-conc1
          • Uri-cst-relative-ref-conc
          • Uri-cst-path-rootless-conc
          • Uri-cst-path-noscheme-conc
          • Uri-cst-path-conc5-rep-elem
          • Uri-cst-path-conc5-rep
          • Uri-cst-path-conc4-rep-elem
          • Uri-cst-path-conc4-rep
          • Uri-cst-path-conc3-rep-elem
          • Uri-cst-path-conc3-rep
          • Uri-cst-path-conc2-rep-elem
          • Uri-cst-path-conc2-rep
          • Uri-cst-path-conc1-rep-elem
          • Uri-cst-path-conc1-rep
          • Uri-cst-path-absolute-conc
          • Uri-cst-path-abempty-conc
          • Uri-cst-ipv4address-conc
          • Uri-cst-ip-literal-conc
          • Uri-cst-host-conc3-rep-elem
          • Uri-cst-host-conc3-rep
          • Uri-cst-host-conc2-rep-elem
          • Uri-cst-host-conc2-rep
          • Uri-cst-host-conc1-rep-elem
          • Uri-cst-host-conc1-rep
          • Uri-cst-absolute-uri-conc
          • Uri-cst-userinfo-conc
          • Uri-cst-segment-nz-conc
          • Uri-cst-segment-conc
          • Uri-cst-scheme-conc
          • Uri-cst-reg-name-conc
          • Uri-cst-pct-encoded-conc
          • Uri-cst-path-empty-conc
          • Uri-cst-path-conc5
          • Uri-cst-path-conc4
          • Uri-cst-path-conc3
          • Uri-cst-path-conc2
          • Uri-cst-path-conc1
          • Uri-cst-ipvfuture-conc
          • Uri-cst-host-conc3
          • Uri-cst-host-conc2
          • Uri-cst-host-conc1
          • Uri-cst-fragment-conc
          • Uri-cst-digit-conc-rep-elem
          • Uri-cst-digit-conc-rep
          • Uri-cst-authority-conc
          • Uri-cst-uri-conc
          • Uri-cst-query-conc
          • Uri-cst-port-conc
          • Uri-cst-h16-conc
          • Uri-cst-digit-conc
          • *uri-grammar-rules*
          • Uri-cst-%x61-7a-nat
          • Uri-cst-%x41-5a-nat
          • Uri-cst-%x31-39-nat
          • Uri-cst-%x30-39-nat
          • Uri-cst-%x30-35-nat
          • Uri-cst-%x30-34-nat
        • Imf-example
      • Differences-with-paper
      • Constructor-utilities
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Uri-example

*uri-grammar-rules*

The URI grammar rules from RFC 3986.

The file uri.abnf contains the URI grammar rules, copied and pasted from RFC 3986. The ABNF grammar parser and abstractor are used to build an ACL2 representation of the URI grammar rules, excluding the referenced ABNF core rules.

The URI grammar rules are well-formed.

We keep this constant unexpanded in output.

Definitions and Theorems

Function: untranslate-preprocess-*uri-grammar-rules*

(defun untranslate-preprocess-*uri-grammar-rules*
       (acl2::term acl2::wrld)
  (if (equal acl2::term
             (list 'quote *uri-grammar-rules*))
      '*uri-grammar-rules*
    (untranslate-preprocess-*grammar* acl2::term acl2::wrld)))

Theorem: rulelist-wfp-of-*uri-grammar-rules*

(defthm rulelist-wfp-of-*uri-grammar-rules*
  (rulelist-wfp *uri-grammar-rules*))