regexp.README: Source Documentation

• Where to start ?
• Preliminaries
• The three layered proof.
  • Automata construction
  • Automata simulation
• Reification of finite type and sets
  • Semantics via the denote family of functions
• Synthesis of finite types and sets
  • Synthesis via syn family of functions.
  • Axioms in the synthesis layers.

regexp.synthesis: Synthesizing the certified hardware

• Overview
  • The state machine
  • Acceptance/rejection
  • The correctness proof
• Proof of correctness

regexp.byte: Functions on bytes with synthesis to clash.

• Overview

regexp.lang: Languages

• Overview
  • Language operations
  • Co-functor structure on lang
• Language equivalence.
  • Contravariant lift of alphabet transformations.

regexp.lang.world: Languages on Worlds and Thickening

• Overview
• Worlds
• Thickening

regexp.expr: Regular expressions

• Overview
  • Matcher variant.
• Regular expression over languages.
• Generalized regexp matcher.

regexp.abstract.automata: Automata in the abstract layer

• Overview
• A nondeterministic automata

regexp.abstract.automata.build: Regexp to NFA construction

• Overview

regexp.abstract.automata.simulation: Simulation of an NFA on an input

• Overview
• Correctness.

regexp.concrete.automata

• Reified form of NFA.
• Semantics

regexp.concrete.automata.build: Regexp to NFA - concrete layer

• Overview

regexp.concrete.automata.simulation: Simulation of an NFA on an input

• Overview
• Proof of correctness.

regexp.synthesis.clash.automata: Automata in Clash

• Overview
  • Simulation
• Synthesizing automata form the concrete layer
• Correctness of the simulation.

regexp.abstract.automata.path

• Paths in a transition system.
  • Accessability relation
• Reachability and cover.
  • Automata on direct sum of states

regexp.abstract.automata.world

regexp.abstract.relation

regexp.abstract.utils

regexp.abstract.automata.epsilon

regexp.abstract.automata.concat

• Automata construction for concatenation
• The alphabet set B.
• The automata macL and macR with state spaces StL and StR
• Right to left paths

regexp.abstract.automata.singleton

regexp.abstract.automata.alt

regexp.abstract.automata.oneOrMore

regexp.abstract.automata.transition

• Overview
• Disjoint union automata

regexp.concrete.universe

regexp.concrete.function: Functions

• Overview
  • Concrete Functions as Vectors.
• Semantics

regexp.concrete.subset

• Overview
• Finite subset types
• Semantics

regexp.concrete.relation

regexp.synthesis.clash.function

• Synthesis

regexp.synthesis.clash.axioms

• The axioms for correctness of synthesis.

regexp.synthesis.clash.subset

• Finite subset types
• Synthesis

regexp.synthesis.clash.universe

regexp.synthesis.clash.prelude

regexp.synthesis.clash.relation

• Synthesis

regexp.synthesis.clash.constraint

• Generating Haskell constraints

regexp.concrete.rule: String matching rules

• Overview
• String matching rules
  • The associated language
• Interpreting the input

regexp.concrete.automata.singleton

regexp.concrete.automata.alt

regexp.concrete.automata.epsilon

regexp.concrete.automata.concat

regexp.concrete.automata.oneOrMore

regexp.prelude

regexp.syn

• PHOAS based syntax for building regexps