module Data.Yoko.SmartPreciseCase (precise_case0, Default(..)) where
import Data.YokoRaw hiding (precise_case0)
import qualified Data.YokoRaw as Raw
class Error_precise_case_requires_at_least_1_special_case a
data AdHoc dcs dt r = AdHoc dt (forall p1 p0. dcs p1 p0 -> r)
newtype Default a r = Default (forall p1 p0. a p1 p0 -> r)
class Builder adhoc bldr where
precise_case_ :: adhoc -> bldr
instance Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a final -> b) where
precise_case_ = error "precise_case_ requires at least 1 special case"
newtype Start dt = Start dt
instance (dt ~ Codomain dc,
Builder (AdHoc (N dc) (Codomain dc) r) bldr) =>
Builder (Start dt) ((dc -> r) -> bldr) where
precise_case_ (Start dt) f = precise_case_ $ AdHoc dt $ one f
instance (dt ~ Codomain dc, dt ~ Codomain0 dcs, r ~ r',
Builder (AdHoc (dcs :+: N dc) dt r) bldr) =>
Builder (AdHoc dcs dt r) ((dc -> r') -> bldr) where
precise_case_ (AdHoc dt adhoc) f = precise_case_ $ AdHoc dt $ adhoc ||. f
instance (DT dt, dt ~ Codomain0 dcs, dt ~ Codomain0 (DCs dt),
Partition (DCs dt) dcs (DCs dt :-: dcs),
x ~ (DCs dt :-: dcs),
final ~ r, final' ~ r) =>
Builder (AdHoc dcs dt r) (Default x final -> final') where
precise_case_ (AdHoc dt adhoc) (Default dflt) = Raw.precise_case0 dflt dt adhoc
precise_case0 :: Builder (Start dt) bldr => dt -> bldr
precise_case0 = precise_case_ . Start