{-# OPTIONS_GHC -Wunused-imports #-}

{-# OPTIONS_GHC -fno-warn-orphans     #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Agda.TypeChecking.Serialise.Instances.Compilers where

import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common

import Agda.TypeChecking.Monad

instance EmbPrj CompilerPragma where
  icod_ :: CompilerPragma -> S Int32
icod_ (CompilerPragma Range
a String
b) =
    (SerialisedRange -> String -> CompilerPragma)
-> Arrows
     (Domains (SerialisedRange -> String -> CompilerPragma)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (Range -> String -> CompilerPragma
CompilerPragma (Range -> String -> CompilerPragma)
-> (SerialisedRange -> Range)
-> SerialisedRange
-> String
-> CompilerPragma
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange) (Range -> SerialisedRange
SerialisedRange Range
a) String
b

  value :: Int32 -> R CompilerPragma
value = (SerialisedRange -> String -> CompilerPragma)
-> Int32
-> R (CoDomain (SerialisedRange -> String -> CompilerPragma))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (Range -> String -> CompilerPragma
CompilerPragma (Range -> String -> CompilerPragma)
-> (SerialisedRange -> Range)
-> SerialisedRange
-> String
-> CompilerPragma
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange)

instance EmbPrj ForeignCode where
  icod_ :: ForeignCode -> S Int32
icod_ (ForeignCode Range
r String
a) =
    (SerialisedRange -> String -> ForeignCode)
-> Arrows
     (Domains (SerialisedRange -> String -> ForeignCode)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (Range -> String -> ForeignCode
ForeignCode (Range -> String -> ForeignCode)
-> (SerialisedRange -> Range)
-> SerialisedRange
-> String
-> ForeignCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange) (Range -> SerialisedRange
SerialisedRange Range
r) String
a

  value :: Int32 -> R ForeignCode
value = (SerialisedRange -> String -> ForeignCode)
-> Int32 -> R (CoDomain (SerialisedRange -> String -> ForeignCode))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (Range -> String -> ForeignCode
ForeignCode (Range -> String -> ForeignCode)
-> (SerialisedRange -> Range)
-> SerialisedRange
-> String
-> ForeignCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange)

instance EmbPrj ForeignCodeStack where
  icod_ :: ForeignCodeStack -> S Int32
icod_ = [ForeignCode] -> S Int32
forall a. EmbPrj a => a -> S Int32
icod_ ([ForeignCode] -> S Int32)
-> (ForeignCodeStack -> [ForeignCode])
-> ForeignCodeStack
-> S Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ForeignCodeStack -> [ForeignCode]
getForeignCodeStack
  value :: Int32 -> R ForeignCodeStack
value = ([ForeignCode] -> ForeignCodeStack)
-> ExceptT TypeError (StateT St IO) [ForeignCode]
-> R ForeignCodeStack
forall a b.
(a -> b)
-> ExceptT TypeError (StateT St IO) a
-> ExceptT TypeError (StateT St IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [ForeignCode] -> ForeignCodeStack
ForeignCodeStack (ExceptT TypeError (StateT St IO) [ForeignCode]
 -> R ForeignCodeStack)
-> (Int32 -> ExceptT TypeError (StateT St IO) [ForeignCode])
-> Int32
-> R ForeignCodeStack
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> ExceptT TypeError (StateT St IO) [ForeignCode]
forall a. EmbPrj a => Int32 -> R a
value