{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
--{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}


-- | Allows you to embed Int, (), Bool etc in trees
-- Note that this normally should not be needed because comptrans takes primitives to primitives
-- However, for things like (Maybe Int), because we just have a single hand-written translation of Maybe,
-- we will need to be able to treat the contents of the Maybe uniformly

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