{-# 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), Currying (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), Currying (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)