module Strongweak.Example where

import Strongweak
import Strongweak.Generic

import GHC.Generics ( Generic )

import Data.Word ( Word8 )

import Refined hiding ( Weaken(..) )
import Numeric.Natural

data Ex1D (s :: Strength) = Ex1C
  { forall (s :: Strength). Ex1D s -> SW s Word8
ex1f1 :: SW s Word8
  , forall (s :: Strength).
Ex1D s -> SW s (Refined (LessThan 100) Natural)
ex1f2 :: SW s (Refined (LessThan 100) Natural)
  } deriving stock (forall x. Ex1D s -> Rep (Ex1D s) x)
-> (forall x. Rep (Ex1D s) x -> Ex1D s) -> Generic (Ex1D s)
forall x. Rep (Ex1D s) x -> Ex1D s
forall x. Ex1D s -> Rep (Ex1D s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: Strength) x. Rep (Ex1D s) x -> Ex1D s
forall (s :: Strength) x. Ex1D s -> Rep (Ex1D s) x
$cto :: forall (s :: Strength) x. Rep (Ex1D s) x -> Ex1D s
$cfrom :: forall (s :: Strength) x. Ex1D s -> Rep (Ex1D s) x
Generic
deriving stock instance Show (Ex1D 'Strong)
deriving stock instance Show (Ex1D 'Weak)
instance Weaken     (Ex1D 'Strong) (Ex1D 'Weak)   where weaken :: Ex1D 'Strong -> Ex1D 'Weak
weaken     = Ex1D 'Strong -> Ex1D 'Weak
forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric
instance Strengthen (Ex1D 'Weak)   (Ex1D 'Strong) where strengthen :: Ex1D 'Weak -> Validation (NonEmpty StrengthenError) (Ex1D 'Strong)
strengthen = Ex1D 'Weak -> Validation (NonEmpty StrengthenError) (Ex1D 'Strong)
forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Validation (NonEmpty StrengthenError) s
strengthenGeneric

data Ex2D (s :: Strength) = Ex2C
  { forall (s :: Strength). Ex2D s -> Ex1D s
ex2f1 :: Ex1D s
  , forall (s :: Strength). Ex2D s -> SW s Word8
ex2f2 :: SW s Word8
  } deriving stock (forall x. Ex2D s -> Rep (Ex2D s) x)
-> (forall x. Rep (Ex2D s) x -> Ex2D s) -> Generic (Ex2D s)
forall x. Rep (Ex2D s) x -> Ex2D s
forall x. Ex2D s -> Rep (Ex2D s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: Strength) x. Rep (Ex2D s) x -> Ex2D s
forall (s :: Strength) x. Ex2D s -> Rep (Ex2D s) x
$cto :: forall (s :: Strength) x. Rep (Ex2D s) x -> Ex2D s
$cfrom :: forall (s :: Strength) x. Ex2D s -> Rep (Ex2D s) x
Generic
deriving stock instance Show (Ex2D 'Strong)
deriving stock instance Show (Ex2D 'Weak)
instance Weaken     (Ex2D 'Strong) (Ex2D 'Weak)   where weaken :: Ex2D 'Strong -> Ex2D 'Weak
weaken     = Ex2D 'Strong -> Ex2D 'Weak
forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric
instance Strengthen (Ex2D 'Weak)   (Ex2D 'Strong) where strengthen :: Ex2D 'Weak -> Validation (NonEmpty StrengthenError) (Ex2D 'Strong)
strengthen = Ex2D 'Weak -> Validation (NonEmpty StrengthenError) (Ex2D 'Strong)
forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Validation (NonEmpty StrengthenError) s
strengthenGeneric

ex1w :: Ex1D 'Weak
ex1w :: Ex1D 'Weak
ex1w = SW 'Weak Word8
-> SW 'Weak (Refined (LessThan 100) Natural) -> Ex1D 'Weak
forall (s :: Strength).
SW s Word8 -> SW s (Refined (LessThan 100) Natural) -> Ex1D s
Ex1C Natural
SW 'Weak Word8
256 Natural
SW 'Weak (Refined (LessThan 100) Natural)
210

ex2w :: Ex2D 'Weak
ex2w :: Ex2D 'Weak
ex2w = Ex1D 'Weak -> SW 'Weak Word8 -> Ex2D 'Weak
forall (s :: Strength). Ex1D s -> SW s Word8 -> Ex2D s
Ex2C Ex1D 'Weak
ex1w Natural
SW 'Weak Word8
256

data ExVoid (s :: Strength) deriving stock (forall x. ExVoid s -> Rep (ExVoid s) x)
-> (forall x. Rep (ExVoid s) x -> ExVoid s) -> Generic (ExVoid s)
forall x. Rep (ExVoid s) x -> ExVoid s
forall x. ExVoid s -> Rep (ExVoid s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: Strength) x. Rep (ExVoid s) x -> ExVoid s
forall (s :: Strength) x. ExVoid s -> Rep (ExVoid s) x
$cto :: forall (s :: Strength) x. Rep (ExVoid s) x -> ExVoid s
$cfrom :: forall (s :: Strength) x. ExVoid s -> Rep (ExVoid s) x
Generic
instance Weaken     (ExVoid 'Strong) (ExVoid 'Weak)   where weaken :: ExVoid 'Strong -> ExVoid 'Weak
weaken     = ExVoid 'Strong -> ExVoid 'Weak
forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric
instance Strengthen (ExVoid 'Weak)   (ExVoid 'Strong) where strengthen :: ExVoid 'Weak
-> Validation (NonEmpty StrengthenError) (ExVoid 'Strong)
strengthen = ExVoid 'Weak
-> Validation (NonEmpty StrengthenError) (ExVoid 'Strong)
forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Validation (NonEmpty StrengthenError) s
strengthenGeneric

data ExUnit (s :: Strength) = ExUnit deriving stock (forall x. ExUnit s -> Rep (ExUnit s) x)
-> (forall x. Rep (ExUnit s) x -> ExUnit s) -> Generic (ExUnit s)
forall x. Rep (ExUnit s) x -> ExUnit s
forall x. ExUnit s -> Rep (ExUnit s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: Strength) x. Rep (ExUnit s) x -> ExUnit s
forall (s :: Strength) x. ExUnit s -> Rep (ExUnit s) x
$cto :: forall (s :: Strength) x. Rep (ExUnit s) x -> ExUnit s
$cfrom :: forall (s :: Strength) x. ExUnit s -> Rep (ExUnit s) x
Generic
instance Weaken     (ExUnit 'Strong) (ExUnit 'Weak)   where weaken :: ExUnit 'Strong -> ExUnit 'Weak
weaken     = ExUnit 'Strong -> ExUnit 'Weak
forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric
instance Strengthen (ExUnit 'Weak)   (ExUnit 'Strong) where strengthen :: ExUnit 'Weak
-> Validation (NonEmpty StrengthenError) (ExUnit 'Strong)
strengthen = ExUnit 'Weak
-> Validation (NonEmpty StrengthenError) (ExUnit 'Strong)
forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Validation (NonEmpty StrengthenError) s
strengthenGeneric