regexp.synthesis.clash.constraint

Generating Haskell constraints

Haskell type classes and more generally elements of Constraint Kinds are handled here. In the coq world, the constraint is just ignored where as in the extracted code they are appropriately generated. It is advised to use the notation to build complicated constraints.

Definition typ (k t : Type) := t.
Definition andC k1 k2 := (k1 × k2)%type.
Notation "[ x => t ]" := (constraint.typ x t) : synthesis_scope.
Notation "[ x , .. , y , z => t ]" := (constraint.typ (andC x .. (andC y z) ..) t) : synthesis_scope.

The KnownNat constraint from the Haskell world

Axiom knownNat : Type → Type.
Axiom isSucc : Type → Type.

Extract Constant typ "k" "t" ⇒ "k => t".
Extract Constant andC "c1" "c2" ⇒ "(c1 :: Clash.Prelude.Constraint, c2 :: Clash.Prelude.Constraint)".
Extract Constant knownNat "n" ⇒ "Clash.Prelude.KnownNat n".
Extract Constant isSucc "m" ⇒ "(m ~ ((m Clash.Prelude.- 1) Clash.Prelude.+ 1))".