search

clash-lang / clash-compiler

Haskell to VHDL/Verilog/SystemVerilog compiler
https://clash-lang.org/
Other
1.42k stars 150 forks source link

Use singletons instead of own SNat #1601

Open uzytkownik opened 3 years ago

uzytkownik commented 3 years ago

singletons library is already in dependencies of clash. However clash uses own SNat implementation. That means that code using singletons needs to convert back and forth between them.

gergoerdi commented 3 years ago

Can you extract a KnownNat witness from a singletons-style Nat singleton? I would expect that to be the biggest hurdle.

uzytkownik commented 3 years ago

@gergoerdi Yes. The definitions are almost exactly the same:

Singletons:

data SNat (n :: Nat) = KnownNat n => SNat
type instance Sing = SNat

Clash:

data SNat (n :: Nat) where
  SNat :: KnownNat n => SNat n
christiaanb commented 3 years ago

It doesn’t have a Lift instance though

martijnbastiaan commented 3 years ago

singletons already depends on template-haskell, so perhaps the maintainers would accept a PR?