{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
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 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 ()