regexp.synthesis.clash.universe

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 Zero : Type.
Axiom Unit : Type.
Axiom CoProd : Type → Type → Type.
Notation "'𝟙'" := Unit : synthesis_scope.
Infix "∐" := CoProd (at level 50, left associativity) : synthesis_scope.

We accordingly design the extraction code for these types.

Extract Inlined Constant Zero ⇒ "0".
Extract Inlined Constant Unit ⇒ "1".
Extract Constant CoProd "m" "n" ⇒ "(m Clash.Prelude.+ n)".

Fixpoint lift (s : sort) : Type :=
  match s with
  | 𝟙%con ⇒ 𝟙%syn
  | (s1 ∐ s2)%con ⇒ (lift s1 ∐ lift s2)%syn
  end.

Fixpoint predlift (s : sort) : Type :=
  match s with
  | 𝟙%con ⇒ Zero
  | (s1 ∐ s2)%con ⇒
      if s1 is 𝟙%con then lift s2
      else if s2 is 𝟙%con then lift s1
           else (predlift s1 ∐ lift s2)%syn
  end.

Notation "⟨ s ⟩" := (lift s).