{-# OPTIONS_HADDOCK hide #-}
--{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}

{-# LANGUAGE CPP                     #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE TemplateHaskell         #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}

-- This is a separate file due to GHC's phase restriction.

#ifdef ONLY_ONE_LANGUAGE
module Cubix.Language.C.Parametric.Full.Trans () where
#else
module Cubix.Language.C.Parametric.Full.Trans (
    translate
  , translateNodeInfo
  , untranslate
  ) where

import Data.Proxy
import Data.Typeable ( Typeable )

import qualified Language.C as C
import qualified Language.Haskell.TH as TH

import Data.Comp.Multi ( caseCxt, Sum, All )
import Data.Comp.Trans ( runCompTrans, withSubstitutions, deriveTrans, deriveUntrans )

import Cubix.Language.C.Parametric.Full.Names
import Cubix.Language.C.Parametric.Full.Types
import Cubix.Language.Parametric.Syntax.Base
import Cubix.Language.Parametric.Syntax.Functor


do substs <- makeSubsts
   runCompTrans $ withSubstitutions substs $ deriveTrans origASTTypes (TH.ConT ''CTerm)

translate :: C.CTranslationUnit () -> CTerm CTranslationUnitL
translate :: CTranslationUnit () -> CTerm CTranslationUnitL
translate = CTranslationUnit () -> CTerm CTranslationUnitL
forall a i. Trans a i => a -> CTerm i
trans

translateNodeInfo :: C.NodeInfo -> CTerm NodeInfoL
translateNodeInfo :: NodeInfo -> CTerm NodeInfoL
translateNodeInfo = NodeInfo -> CTerm NodeInfoL
forall a i. Trans a i => a -> CTerm i
trans

instance (Trans c l, Typeable l) => Trans [c] [l] where
  trans :: [c] -> CTerm [l]
trans [] = CTerm [l]
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(ListF :<: f, Typeable l) =>
Cxt h f a [l]
riNilF
  trans (x :: c
x:xs :: [c]
xs) = (c -> CTerm l
forall a i. Trans a i => a -> CTerm i
trans c
x :: CTerm l) CTerm l -> CTerm [l] -> CTerm [l]
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
(ListF :-<: fs, InjF fs [l] l', Typeable l) =>
CxtS h fs a l -> CxtS h fs a [l] -> CxtS h fs a l'
`iConsF` ([c] -> CTerm [l]
forall a i. Trans a i => a -> CTerm i
trans [c]
xs)

instance (Trans c l, Typeable l) => Trans (Maybe c) (Maybe l) where
  trans :: Maybe c -> CTerm (Maybe l)
trans Nothing  = CTerm (Maybe l)
forall h (f :: (* -> *) -> * -> *) (a :: * -> *) l.
(MaybeF :<: f, Typeable l) =>
Cxt h f a (Maybe l)
riNothingF
  trans (Just x :: c
x) = CxtS NoHole CSig (K ()) l -> CTerm (Maybe l)
forall (fs :: [(* -> *) -> * -> *]) l l' h (a :: * -> *).
(MaybeF :-<: fs, InjF fs (Maybe l) l', Typeable l) =>
CxtS h fs a l -> CxtS h fs a l'
iJustF (CxtS NoHole CSig (K ()) l -> CTerm (Maybe l))
-> CxtS NoHole CSig (K ()) l -> CTerm (Maybe l)
forall a b. (a -> b) -> a -> b
$ (c -> CxtS NoHole CSig (K ()) l
forall a i. Trans a i => a -> CTerm i
trans c
x :: CTerm l)

instance (Trans c l, Trans d l', Typeable l, Typeable l') => Trans (c, d) (l, l')  where
  trans :: (c, d) -> CTerm (l, l')
trans (x :: c
x, y :: d
y) = Cxt NoHole (Sum CSig) (K ()) l
-> Cxt NoHole (Sum CSig) (K ()) l' -> CTerm (l, l')
forall (f :: (* -> *) -> * -> *) i j h (a :: * -> *).
(PairF :<: f, Typeable i, Typeable j) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a (i, j)
riPairF (c -> Cxt NoHole (Sum CSig) (K ()) l
forall a i. Trans a i => a -> CTerm i
trans c
x) (d -> Cxt NoHole (Sum CSig) (K ()) l'
forall a i. Trans a i => a -> CTerm i
trans d
y)

instance (Trans c l, Trans d l', Trans e l'', Typeable l, Typeable l', Typeable l'') => Trans (c, d, e) (l, l', l'') where
  trans :: (c, d, e) -> CTerm (l, l', l'')
trans (x :: c
x, y :: d
y, z :: e
z) = Cxt NoHole (Sum CSig) (K ()) l
-> Cxt NoHole (Sum CSig) (K ()) l'
-> Cxt NoHole (Sum CSig) (K ()) l''
-> CTerm (l, l', l'')
forall (f :: (* -> *) -> * -> *) i j k h (a :: * -> *).
(TripleF :<: f, Typeable i, Typeable j, Typeable k) =>
Cxt h f a i -> Cxt h f a j -> Cxt h f a k -> Cxt h f a (i, j, k)
riTripleF (c -> Cxt NoHole (Sum CSig) (K ()) l
forall a i. Trans a i => a -> CTerm i
trans c
x) (d -> Cxt NoHole (Sum CSig) (K ()) l'
forall a i. Trans a i => a -> CTerm i
trans d
y) (e -> Cxt NoHole (Sum CSig) (K ()) l''
forall a i. Trans a i => a -> CTerm i
trans e
z)

instance (Trans c l, Trans d l', Typeable l, Typeable l') => Trans (Either c d) (Either l l') where
  trans :: Either c d -> CTerm (Either l l')
trans (Left x :: c
x)  = Cxt NoHole (Sum CSig) (K ()) l -> CTerm (Either l l')
forall (f :: (* -> *) -> * -> *) i j h (a :: * -> *).
(EitherF :<: f, Typeable i, Typeable j) =>
Cxt h f a i -> Cxt h f a (Either i j)
riLeftF (c -> Cxt NoHole (Sum CSig) (K ()) l
forall a i. Trans a i => a -> CTerm i
trans c
x)
  trans (Right x :: d
x) = Cxt NoHole (Sum CSig) (K ()) l' -> CTerm (Either l l')
forall (f :: (* -> *) -> * -> *) i j h (a :: * -> *).
(EitherF :<: f, Typeable i, Typeable j) =>
Cxt h f a j -> Cxt h f a (Either i j)
riRightF (d -> Cxt NoHole (Sum CSig) (K ()) l'
forall a i. Trans a i => a -> CTerm i
trans d
x)

instance Trans Bool BoolL where
  trans :: Bool -> CTerm BoolL
trans x :: Bool
x = Bool -> CTerm BoolL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(BoolF :-<: fs, InjF fs BoolL j) =>
Bool -> CxtS h fs a j
iBoolF Bool
x

instance Trans Int IntL where
  trans :: Int -> CTerm IntL
trans x :: Int
x = Int -> CTerm IntL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(IntF :-<: fs, InjF fs IntL j) =>
Int -> CxtS h fs a j
iIntF Int
x

instance Trans Integer IntegerL where
  trans :: Integer -> CTerm IntegerL
trans x :: Integer
x = Integer -> CTerm IntegerL
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(IntegerF :-<: fs, InjF fs IntegerL j) =>
Integer -> CxtS h fs a j
iIntegerF Integer
x

instance Trans () () where
  trans :: () -> CTerm ()
trans _ = CTerm ()
forall h (fs :: [(* -> *) -> * -> *]) (a :: * -> *) j.
(UnitF :-<: fs, InjF fs () j) =>
CxtS h fs a j
iUnitF


do substs <- makeSubsts
   runCompTrans $ withSubstitutions substs $ deriveUntrans origASTTypes (TH.ConT ''CTerm)

type instance Targ [l] = [Targ l]
instance Untrans ListF where
  untrans :: ListF T i -> T i
untrans NilF = Targ i -> T i
forall i. Targ i -> T i
T []
  untrans (ConsF a :: T l
a b :: T [l]
b) = Targ i -> T i
forall i. Targ i -> T i
T ((T l -> Targ l
forall i. T i -> Targ i
t T l
a) Targ l -> [Targ l] -> [Targ l]
forall a. a -> [a] -> [a]
: (T [l] -> Targ [l]
forall i. T i -> Targ i
t T [l]
b))

type instance Targ (Maybe l) = Maybe (Targ l)
instance Untrans MaybeF where
  untrans :: MaybeF T i -> T i
untrans NothingF = Targ i -> T i
forall i. Targ i -> T i
T Targ i
forall a. Maybe a
Nothing
  untrans (JustF x :: T l
x) = Targ i -> T i
forall i. Targ i -> T i
T (Targ l -> Maybe (Targ l)
forall a. a -> Maybe a
Just (T l -> Targ l
forall i. T i -> Targ i
t T l
x))

type instance Targ (l, l') = (Targ l, Targ l')
instance Untrans PairF where
  untrans :: PairF T i -> T i
untrans (PairF x :: T i
x y :: T j
y) = Targ i -> T i
forall i. Targ i -> T i
T (T i -> Targ i
forall i. T i -> Targ i
t T i
x, T j -> Targ j
forall i. T i -> Targ i
t T j
y)

type instance Targ (l, l', l'') = (Targ l, Targ l', Targ l'')
instance Untrans TripleF where
  untrans :: TripleF T i -> T i
untrans (TripleF x :: T i
x y :: T j
y z :: T k
z) = Targ i -> T i
forall i. Targ i -> T i
T (T i -> Targ i
forall i. T i -> Targ i
t T i
x, T j -> Targ j
forall i. T i -> Targ i
t T j
y, T k -> Targ k
forall i. T i -> Targ i
t T k
z)
  
type instance Targ (Either l l') = Either (Targ l) (Targ l')
instance Untrans EitherF where
  untrans :: EitherF T i -> T i
untrans (LeftF x :: T i
x)  = Targ i -> T i
forall i. Targ i -> T i
T (Targ i -> Either (Targ i) (Targ j)
forall a b. a -> Either a b
Left (T i -> Targ i
forall i. T i -> Targ i
t T i
x))
  untrans (RightF x :: T j
x) = Targ i -> T i
forall i. Targ i -> T i
T (Targ j -> Either (Targ i) (Targ j)
forall a b. b -> Either a b
Right (T j -> Targ j
forall i. T i -> Targ i
t T j
x))

type instance Targ BoolL = Bool
instance Untrans BoolF where
  untrans :: BoolF T i -> T i
untrans (BoolF x :: Bool
x) = Targ i -> T i
forall i. Targ i -> T i
T Bool
Targ i
x

type instance Targ IntL = Int
instance Untrans IntF where
  untrans :: IntF T i -> T i
untrans (IntF x :: Int
x) = Targ i -> T i
forall i. Targ i -> T i
T Int
Targ i
x

type instance Targ IntegerL = Integer
instance Untrans IntegerF where
  untrans :: IntegerF T i -> T i
untrans (IntegerF x :: Integer
x) = Targ i -> T i
forall i. Targ i -> T i
T Integer
Targ i
x

type instance Targ () = ()
instance Untrans UnitF where
  untrans :: UnitF T i -> T i
untrans UnitF = Targ i -> T i
forall i. Targ i -> T i
T ()

instance (All Untrans fs) => Untrans (Sum fs) where
  untrans :: Sum fs T i -> T i
untrans = Proxy Untrans
-> (forall (f :: (* -> *) -> * -> *). Untrans f => f T i -> T i)
-> Sum fs T i
-> T i
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
       (fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy Untrans
forall k (t :: k). Proxy t
Proxy @Untrans) forall (f :: (* -> *) -> * -> *). Untrans f => f T i -> T i
forall (f :: (* -> *) -> * -> *). Untrans f => Alg f T
untrans

type instance Targ IntL = Int
type instance Targ BoolL = Bool
type instance Targ () = ()
#endif