{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Cubix.Language.Parametric.Syntax.Base (
BoolF(..)
, BoolL
, IntF(..)
, IntL
, IntegerF(..)
, IntegerL
, CharF(..)
, CharL
, UnitF(..)
, pattern BoolF'
, iBoolF
, pattern IntF'
, iIntF
, pattern IntegerF'
, iIntegerF
, pattern CharF'
, iCharF
, pattern UnitF'
, iUnitF
) where
import Data.Comp.Multi ( CxtS, All, HFunctor, (:-<:), project)
import Cubix.Language.Parametric.Derive
data BoolL
data BoolF (e :: * -> *) l where
BoolF :: Bool -> BoolF e BoolL
data IntL
data IntF (e :: * -> *) l where
IntF :: Int -> IntF e IntL
data IntegerL
data IntegerF (e :: * -> *) l where
IntegerF :: Integer -> IntegerF e IntegerL
data CharL
data CharF (e :: * -> *) l where
CharF :: Char -> CharF e CharL
data UnitF (e :: * -> *) l where
UnitF :: UnitF e ()
deriveAll [''BoolF, ''IntF, ''IntegerF, ''CharF, ''UnitF]
pattern BoolF' :: (BoolF :-<: fs, All HFunctor fs) => Bool -> CxtS h fs a BoolL
pattern $bBoolF' :: Bool -> CxtS h fs a BoolL
$mBoolF' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(BoolF :-<: fs, All HFunctor fs) =>
CxtS h fs a BoolL -> (Bool -> r) -> (Void# -> r) -> r
BoolF' b <- (project -> Just (BoolF b)) where
BoolF' b :: Bool
b = Bool -> CxtS h fs a BoolL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(BoolF :-<: fs, InjF fs BoolL j) =>
Bool -> CxtS h fs a j
iBoolF Bool
b
pattern IntF' :: (IntF :-<: fs, All HFunctor fs) => Int -> CxtS h fs a IntL
pattern $bIntF' :: Int -> CxtS h fs a IntL
$mIntF' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(IntF :-<: fs, All HFunctor fs) =>
CxtS h fs a IntL -> (Int -> r) -> (Void# -> r) -> r
IntF' x <- (project -> Just (IntF x)) where
IntF' x :: Int
x = Int -> CxtS h fs a IntL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(IntF :-<: fs, InjF fs IntL j) =>
Int -> CxtS h fs a j
iIntF Int
x
pattern IntegerF' :: (IntegerF :-<: fs, All HFunctor fs) => Integer -> CxtS h fs a IntegerL
pattern $bIntegerF' :: Integer -> CxtS h fs a IntegerL
$mIntegerF' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(IntegerF :-<: fs, All HFunctor fs) =>
CxtS h fs a IntegerL -> (Integer -> r) -> (Void# -> r) -> r
IntegerF' x <- (project -> Just (IntegerF x)) where
IntegerF' x :: Integer
x = Integer -> CxtS h fs a IntegerL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(IntegerF :-<: fs, InjF fs IntegerL j) =>
Integer -> CxtS h fs a j
iIntegerF Integer
x
pattern CharF' :: (CharF :-<: fs, All HFunctor fs) => Char -> CxtS h fs a CharL
pattern $bCharF' :: Char -> CxtS h fs a CharL
$mCharF' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(CharF :-<: fs, All HFunctor fs) =>
CxtS h fs a CharL -> (Char -> r) -> (Void# -> r) -> r
CharF' x <- (project -> Just (CharF x)) where
CharF' x :: Char
x = Char -> CxtS h fs a CharL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(CharF :-<: fs, InjF fs CharL j) =>
Char -> CxtS h fs a j
iCharF Char
x
pattern UnitF' :: (UnitF :-<: fs, All HFunctor fs) => CxtS h fs a ()
pattern $bUnitF' :: CxtS h fs a ()
$mUnitF' :: forall r (fs :: [(* -> *) -> * -> *]) h (a :: * -> *).
(UnitF :-<: fs, All HFunctor fs) =>
CxtS h fs a () -> (Void# -> r) -> (Void# -> r) -> r
UnitF' <- (project -> Just UnitF) where
UnitF' = CxtS h fs a ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF