regexp.synthesis.clash.function

To get synthesisable circuits out of the automata that we constructed, we need extraction of finite universes as well as sets, functions and relations on them to be extracted to synthesisable clash. Elements of sort type now needs to be converted into type level nats in clash

Axiom t : Type → Type → Type.
Notation "s ~> A" := (t A s) (at level 99, right associativity) : synthesis_scope.

Axiom singleton : ∀ {A : Type}, A → t A Unit.
Axiom concat : ∀ {A M N: Type}, t A M → t A N → t A (M ∐ N)%syn.
Axiom constant : ∀ {A N : Type}, [knownNat N ⇒ A → t A N ]%syn.
Axiom fold : ∀ {A M : Type}, [isSucc M ⇒ (A → A → A ) → t A M → A ]%syn.
Axiom map : ∀ {A B N : Type}, (A → B ) → t A N → t B N.
Axiom zipWith : ∀ {A B C N : Type}, (A → B → C ) → t A N → t B N → t C N.

Extract Constant t "a" "n" ⇒ "(Clash.Sized.Vector.Vec n a)".
Extract Constant singleton ⇒ "Clash.Sized.Vector.singleton".
Extract Constant constant ⇒ "Clash.Sized.Vector.repeat".
Extract Constant concat ⇒ "(Clash.Sized.Vector.++)".
Extract Constant fold ⇒ "Clash.Sized.Vector.fold".
Extract Constant map ⇒ "Clash.Sized.Vector.map".
Extract Constant zipWith ⇒ "Clash.Sized.Vector.zipWith".

Synthesis

Synthesis of concrete functions to clash.

Require Import regexp.concrete.universe.
Require regexp.concrete.function.

Fixpoint syn {s : universe.sort}{A}(u : concrete.function.t A s) : (⟨ s ⟩ ~> A)%syn:=
  match u with
  | concrete.function.const x ⇒ singleton x
  | concrete.function.concat _ _ u1 u2 ⇒ concat (syn u1) (syn u2)
  end.