{-# 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), StrictCurrying (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), StrictCurrying (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) -> StateT St IO [ForeignCode] -> R ForeignCodeStack forall a b. (a -> b) -> StateT St IO a -> StateT St IO b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap [ForeignCode] -> ForeignCodeStack ForeignCodeStack (StateT St IO [ForeignCode] -> R ForeignCodeStack) -> (Int32 -> StateT St IO [ForeignCode]) -> Int32 -> R ForeignCodeStack forall b c a. (b -> c) -> (a -> b) -> a -> c . Int32 -> StateT St IO [ForeignCode] forall a. EmbPrj a => Int32 -> R a value