{-# OPTIONS_HADDOCK hide #-}

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

{-# LANGUAGE TemplateHaskell        #-}
{-# 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.Typeable ( Typeable )

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

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


------------------------------------------------------------------------------------
-------------- Forward translation: 3rd-party syntax to modularized  ---------------
------------------------------------------------------------------------------------

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

translate :: Lua.Block (Maybe SourceSpan) -> LuaTermOptAnn SourceSpan BlockL
translate :: Block (Maybe SourceSpan)
-> AnnTerm (Maybe SourceSpan) LuaSig BlockL
translate = 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)
-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) FunBodyL
trans (Lua.FunBody Maybe SourceSpan
a [Name (Maybe SourceSpan)]
args Maybe (Maybe SourceSpan)
varArg Block (Maybe SourceSpan)
blk) = (:&:)
  FunBody
  (Maybe SourceSpan)
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
  FunBodyL
-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) FunBodyL
(:&:)
  FunBody
  (Maybe SourceSpan)
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (f :: Fragment) (g :: Fragment) 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
 -> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) FunBodyL)
-> (:&:)
     FunBody
     (Maybe SourceSpan)
     (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
     FunBodyL
-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()) FunBodyL
forall a b. (a -> b) -> a -> b
$ (AnnTerm (Maybe SourceSpan) LuaSig [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)]
-> AnnTerm (Maybe SourceSpan) LuaSig [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 (f :: Fragment) a (g :: * -> *) e.
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]
ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
forall l1 (e :: * -> *). Typeable l1 => ListF e [l1]
NilF
  trans (c
x:[c]
xs) = ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) [l]
-> AnnTerm (Maybe SourceSpan) LuaSig [l]
ListF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (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 l1 (e :: * -> *).
Typeable l1 =>
e l1 -> e [l1] -> ListF e [l1]
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 Maybe c
Nothing  = MaybeF
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
-> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l)
MaybeF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject MaybeF
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
forall l1 (e :: * -> *). Typeable l1 => MaybeF e (Maybe l1)
NothingF
  trans (Just c
x) = MaybeF
  (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (Maybe l)
-> AnnTerm (Maybe SourceSpan) LuaSig (Maybe l)
MaybeF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (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 l1 (e :: * -> *). Typeable l1 => e l1 -> MaybeF e (Maybe l1)
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 (c
x, d
y) = PairF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) (l, l')
-> AnnTerm (Maybe SourceSpan) LuaSig (l, l')
PairF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject (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 ()
UnitF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ()))
:-> Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())
forall (g :: Fragment) (f :: Fragment) h (a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject UnitF (Cxt NoHole (Sum LuaSig :&: Maybe SourceSpan) (K ())) ()
forall (a :: * -> *). UnitF a ()
UnitF

------------------------------------------------------------------------------------
------------ Backward translation: Modularized syntax to 3rd-party  ----------------
------------------------------------------------------------------------------------

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 :: Alg (FunBody :&: Maybe SourceSpan) T
untrans (FunBody T [NameL]
args Bool
varArg T BlockL
blk :&: 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 :: Alg (ListF :&: a) T
untrans (ListF T i
NilF :&: a
_) = Targ i -> T i
forall i. Targ i -> T i
T []
  untrans (ConsF T l1
a T [l1]
b :&: a
_) = Targ i -> T i
forall i. Targ i -> T i
T ((T l1 -> Targ l1
forall i. T i -> Targ i
t T l1
a) Targ l1 -> [Targ l1] -> [Targ l1]
forall a. a -> [a] -> [a]
: (T [l1] -> Targ [l1]
forall i. T i -> Targ i
t T [l1]
b))

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

type instance Targ (l, l') = (Targ l, Targ l')
instance Untrans (PairF :&: a) where
  untrans :: Alg (PairF :&: a) T
untrans (PairF T i
x T j
y :&: a
_) = 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 :: Alg (Sum fs :&: a) T
untrans = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment]) a
       (e :: * -> *) l t.
All cxt (DistAnn fs a) =>
(forall (f :: Fragment). cxt (f :&: a) => (:&:) f a e l -> t)
-> (:&:) (Sum fs) a e l -> t
caseCxt'' @Untrans (:&:) f a T i -> T i
Alg (f :&: a) T
forall (f :: Fragment). Untrans f => Alg f T
forall (f :: Fragment). Untrans (f :&: a) => (:&:) f a T i -> T i
untrans

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