content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  
  -- Only instances exported
  module Agda.TypeChecking.Serialise.Instances () where
  
  import Agda.Syntax.Position
  import Agda.Syntax.TopLevelModuleName
  import Agda.TypeChecking.Monad.Base
  import Agda.TypeChecking.Serialise.Base
  import Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..))
  import Agda.TypeChecking.Serialise.Instances.Errors ()
  import Agda.TypeChecking.Serialise.Instances.General ()
  import Agda.TypeChecking.Serialise.Instances.Highlighting ()
  import Agda.Utils.Hash
  
  type RangedImportedModules =
    [(SerialisedRange, TopLevelModuleName, Hash)]
  
  fromImportedModules ::
    [(TopLevelModuleName, Hash)] -> RangedImportedModules
  fromImportedModules ms = [(SerialisedRange $ getRange x, x, hash) | (x, hash) <- ms]
  
  toImportedModules ::
    RangedImportedModules -> [(TopLevelModuleName, Hash)]
  toImportedModules ms = [(setRange (underlyingRange r) x, hash) | (r, x, hash) <- ms]
  
  instance EmbPrj Interface where
    icod_ (Interface a b c d e f g h i j k l m n o p q r s t u v w x) =
        icodeN' interface a b c (fromImportedModules d) e f g h i j k l m n o p q r s t u v w x
      where interface a b c = Interface a b c . toImportedModules
  
    value = valueN interface
      where interface a b c = Interface a b c . toImportedModules
  