{-# 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) =
    forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (Range -> String -> CompilerPragma
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 = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (Range -> String -> CompilerPragma
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) =
    forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (Range -> String -> ForeignCode
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 = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (Range -> String -> ForeignCode
ForeignCode forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange)

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