{-# OPTIONS_HADDOCK hide #-}

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

{-# 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.

module Cubix.Language.Lua.Parametric.Full.Trans (
    translate
  , untranslate
  , Targ
  ) where

import Prelude hiding ( EQ, GT, LT )

import Data.Maybe ( isJust )
import Data.Proxy
import Data.Typeable ( Typeable )

import Data.Comp.Multi ( inject', caseCxt'', Sum, All, (:&:)(..), injectOpt, DistAnn, stripA )

import qualified Language.Lua.Annotated as Lua

import Data.Comp.Trans ( runCompTrans, deriveTrans, deriveUntrans, withSubstitutions, withAnnotationProp, defaultUnpropAnn, withExcludedNames )

import Cubix.Language.Info
import Cubix.Language.Lua.Parametric.Full.Exclusions
import Cubix.Language.Lua.Parametric.Full.Names
import Cubix.Language.Lua.Parametric.Full.Types
import Cubix.Language.Parametric.Syntax.Base
import Cubix.Language.Parametric.Syntax.Functor

do substs <- makeSubsts
   runCompTrans $ withAnnotationProp annType isAnn propAnn defaultUnpropAnn
                $ withSubstitutions substs
                $ withExcludedNames excludedNamesSet
                $ deriveTrans origASTTypes annotatedTargType

translate :: Lua.Block (Maybe SourceSpan) -> LuaTerm {-OptAnn SourceSpan-} BlockL
translate :: Block (Maybe SourceSpan) -> LuaTerm BlockL
translate = AnnTerm (Maybe SourceSpan) LuaSig BlockL -> LuaTerm BlockL
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(RemA g f, HFunctor g) =>
CxtFun g f
stripA (AnnTerm (Maybe SourceSpan) LuaSig BlockL -> LuaTerm BlockL)
-> (Block (Maybe SourceSpan)
    -> AnnTerm (Maybe SourceSpan) LuaSig BlockL)
-> Block (Maybe SourceSpan)
-> LuaTerm BlockL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block (Maybe SourceSpan)
-> AnnTerm (Maybe SourceSpan) LuaSig BlockL
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans

instance Trans (Lua.FunBody (Maybe SourceSpan)) FunBodyL where
  trans :: FunBody (Maybe SourceSpan)
-> AnnTerm (Maybe SourceSpan) LuaSig FunBodyL
trans (Lua.FunBody a :: Maybe SourceSpan
a args :: [Name (Maybe SourceSpan)]
args varArg :: Maybe (Maybe SourceSpan)
varArg blk :: Block (Maybe SourceSpan)
blk) = (:&:)
  FunBody
  (Maybe SourceSpan)
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
  FunBodyL
-> AnnTerm (Maybe SourceSpan) LuaSig FunBodyL
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p h
       (a :: * -> *).
(f :<: g) =>
(:&:) f p (Cxt h (g :&: p) a) :-> Cxt h (g :&: p) a
inject' ((:&:)
   FunBody
   (Maybe SourceSpan)
   (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
   FunBodyL
 -> AnnTerm (Maybe SourceSpan) LuaSig FunBodyL)
-> (:&:)
     FunBody
     (Maybe SourceSpan)
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
     FunBodyL
-> AnnTerm (Maybe SourceSpan) LuaSig FunBodyL
forall a b. (a -> b) -> a -> b
$ (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) [NameL]
-> Bool
-> AnnTerm (Maybe SourceSpan) LuaSig BlockL
-> FunBody
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) FunBodyL
forall (e :: * -> *).
e [NameL] -> Bool -> e BlockL -> FunBody e FunBodyL
FunBody ([Name (Maybe SourceSpan)]
-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) [NameL]
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans [Name (Maybe SourceSpan)]
args) (Maybe (Maybe SourceSpan) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Maybe SourceSpan)
varArg) (Block (Maybe SourceSpan)
-> AnnTerm (Maybe SourceSpan) LuaSig BlockL
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans Block (Maybe SourceSpan)
blk)) FunBody
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) FunBodyL
-> Maybe SourceSpan
-> (:&:)
     FunBody
     (Maybe SourceSpan)
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
     FunBodyL
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: Maybe SourceSpan
a

instance (Trans c l, Typeable l) => Trans [c] [l] where
  trans :: [c] -> AnnTerm (Maybe SourceSpan) LuaSig [l]
trans [] = ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
-> AnnTerm (Maybe SourceSpan) LuaSig [l]
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p l.
(f :<: g) =>
f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
injectOpt ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
forall l (e :: * -> *). Typeable l => ListF e [l]
NilF
  trans (x :: c
x:xs :: [c]
xs) = ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
-> AnnTerm (Maybe SourceSpan) LuaSig [l]
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p l.
(f :<: g) =>
f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
injectOpt (ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
 -> AnnTerm (Maybe SourceSpan) LuaSig [l])
-> ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
-> AnnTerm (Maybe SourceSpan) LuaSig [l]
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
-> AnnTerm (Maybe SourceSpan) LuaSig [l]
-> ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
forall l (e :: * -> *). Typeable l => e l -> e [l] -> ListF e [l]
ConsF (c -> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans c
x) ([c] -> AnnTerm (Maybe SourceSpan) LuaSig [l]
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans [c]
xs)

instance (Trans c l, Typeable l) => Trans (Maybe c) (Maybe l) where
  trans :: Maybe c -> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l)
trans Nothing  = MaybeF
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
-> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p l.
(f :<: g) =>
f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
injectOpt MaybeF
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
forall l (e :: * -> *). Typeable l => MaybeF e (Maybe l)
NothingF
  trans (Just x :: c
x) = MaybeF
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
-> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l)
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p l.
(f :<: g) =>
f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
injectOpt (MaybeF
   (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
 -> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l))
-> MaybeF
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
-> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l)
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
-> MaybeF
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
forall l (e :: * -> *). Typeable l => e l -> MaybeF e (Maybe l)
JustF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
 -> MaybeF
      (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l))
-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
-> MaybeF
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
forall a b. (a -> b) -> a -> b
$ c -> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans c
x

instance (Trans c l, Trans d l', Typeable l, Typeable l') => Trans (c, d) (l, l')  where
  trans :: (c, d) -> AnnTerm (Maybe SourceSpan) LuaSig (l, l')
trans (x :: c
x, y :: d
y) = PairF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (l, l')
-> AnnTerm (Maybe SourceSpan) LuaSig (l, l')
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p l.
(f :<: g) =>
f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
injectOpt (PairF
   (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (l, l')
 -> AnnTerm (Maybe SourceSpan) LuaSig (l, l'))
-> PairF
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (l, l')
-> AnnTerm (Maybe SourceSpan) LuaSig (l, l')
forall a b. (a -> b) -> a -> b
$ Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l'
-> PairF
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (l, l')
forall i j (e :: * -> *).
(Typeable i, Typeable j) =>
e i -> e j -> PairF e (i, j)
PairF (c -> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans c
x) (d -> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) l'
forall a i. Trans a i => a -> AnnTerm (Maybe SourceSpan) LuaSig i
trans d
y)

instance Trans () () where
  trans :: () -> AnnTerm (Maybe SourceSpan) LuaSig ()
trans _ = UnitF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) ()
-> AnnTerm (Maybe SourceSpan) LuaSig ()
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) p l.
(f :<: g) =>
f (AnnHFix (Maybe p) g) l -> AnnHFix (Maybe p) g l
injectOpt UnitF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) ()
forall (e :: * -> *). UnitF e ()
UnitF

do substs <- makeSubsts
   runCompTrans $ withAnnotationProp annType isAnn propAnn defaultUnpropAnn
                $ withExcludedNames excludedNamesSet
                $ withSubstitutions substs
                $ deriveUntrans origASTTypes annotatedTargType

type instance Targ FunBodyL = Lua.FunBody (Maybe SourceSpan)
instance Untrans (FunBody :&: (Maybe SourceSpan)) where
  untrans :: (:&:) FunBody (Maybe SourceSpan) T i -> T i
untrans (FunBody args :: T [NameL]
args varArg :: Bool
varArg blk :: T BlockL
blk :&: a :: Maybe SourceSpan
a) = Targ i -> T i
forall i. Targ i -> T i
T (Targ i -> T i) -> Targ i -> T i
forall a b. (a -> b) -> a -> b
$ Maybe SourceSpan
-> [Name (Maybe SourceSpan)]
-> Maybe (Maybe SourceSpan)
-> Block (Maybe SourceSpan)
-> FunBody (Maybe SourceSpan)
forall a. a -> [Name a] -> Maybe a -> Block a -> FunBody a
Lua.FunBody Maybe SourceSpan
a (T [NameL] -> Targ [NameL]
forall i. T i -> Targ i
t T [NameL]
args) Maybe (Maybe SourceSpan)
varArg' (T BlockL -> Targ BlockL
forall i. T i -> Targ i
t T BlockL
blk)
    where
      varArg' :: Maybe (Maybe SourceSpan)
varArg' = if Bool
varArg then Maybe SourceSpan -> Maybe (Maybe SourceSpan)
forall a. a -> Maybe a
Just Maybe SourceSpan
forall a. Maybe a
Nothing else Maybe (Maybe SourceSpan)
forall a. Maybe a
Nothing

type instance Targ [l] = [Targ l]
instance Untrans (ListF :&: a) where
  untrans :: (:&:) ListF a 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 :&: a) where
  untrans :: (:&:) MaybeF a 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 :&: a) where
  untrans :: (:&:) PairF a 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)

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

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