    {-# LANGUAGE OverlappingInstances,
                 TypeSynonymInstances,
                 IncoherentInstances,
                 ExistentialQuantification,
                 ScopedTypeVariables,
                 CPP
                 #-}
    {-# OPTIONS_GHC -O2 #-}

    -- | Structure-sharing serialisation of Agda interface files.

    -- -!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-
    -- NOTE: Every time the interface format is changed the interface
    -- version number should be bumped _in the same patch_.
    -- -!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-!-

    module Agda.TypeChecking.Serialise
      ( encode
      , encodeFile
      , decode
      , decodeFile
      , EmbPrj
      )
      where

    import qualified Control.Exception as E
    import Control.Monad
    import Control.Monad.Reader
    import Control.Monad.State.Strict
    import Control.Monad.Error
    import Data.Array.IArray
    import Data.Bits (shiftR)
    import Data.Word
    import Data.ByteString.Lazy as L
    import Data.Char (ord, chr)
    import Data.HashTable (HashTable)
    import qualified Data.HashTable as H
    import Data.Int (Int32, Int64)
    import Data.IORef
    import Data.Map (Map)
    import qualified Data.Map as M
    import Data.Set (Set)
    import qualified Data.Set as S
    import qualified Data.Binary as B
    import qualified Data.Binary.Get as B
    import qualified Data.List as List
    import Data.Function
    import Data.Generics
    import Data.Typeable
    import qualified Codec.Compression.GZip as G

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Name as C
    import Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Position (Position(..), Range)
    import qualified Agda.Syntax.Position as P
    import Agda.Syntax.Common
    import Agda.Syntax.Fixity
    import Agda.Syntax.Literal
    import qualified Agda.Interaction.Highlighting.Range   as HR
    import qualified Agda.Interaction.Highlighting.Precise as HP
    import Agda.Interaction.FindFile

    import Agda.TypeChecking.Monad
    import Agda.Utils.FileName
    import Agda.Utils.Monad
    import Agda.Utils.Tuple
    import Agda.Utils.Permutation

    #include "../undefined.h"
    import Agda.Utils.Impossible

    -- Note that the Binary instance for Int writes 64 bits, but throws
    -- away the 32 high bits when reading (at the time of writing, on
    -- 32-bit machines). Word64 does not have these problems.

    currentInterfaceVersion :: Word64
    currentInterfaceVersion = 20091123 * 10 + 0

    type Node = [Int] -- constructor tag (maybe omitted) and arg indices

    data Dict = Dict{ nodeD     :: !(HashTable Node    Int)
                    , stringD   :: !(HashTable String  Int)
                    , integerD  :: !(HashTable Integer Int)
                    , doubleD   :: !(HashTable Double  Int)
                    , nodeC     :: !(IORef Int)  -- counters for fresh indexes
                    , stringC   :: !(IORef Int)
                    , integerC  :: !(IORef Int)
                    , doubleC   :: !(IORef Int)
                    , fileMod   :: !SourceToModule
                    }

    data U    = forall a . Data a => U !a
    type Memo = HashTable (Int, Int) U    -- (node index, type rep key)

    data St = St
      { nodeE     :: !(Array Int Node)
      , stringE   :: !(Array Int String)
      , integerE  :: !(Array Int Integer)
      , doubleE   :: !(Array Int Double)
      , nodeMemo  :: !Memo
      , modFile   :: !ModuleToSource
        -- ^ Maps module names to file names. This is the only component
        -- of the state which is updated by the decoder.
      , includes  :: [AbsolutePath]
        -- ^ The include directories.
      }

    -- | Monad used by the encoder.

    type S a = ReaderT Dict IO a

    -- | Monad used by the decoder.
    --
    -- 'TCM' is not used because the associated overheads would make
    -- decoding slower.

    type R a = ErrorT TypeError (StateT St IO) a

    -- | Throws an error which is suitable when the data stream is
    -- malformed.

    malformed :: R a
    malformed = throwError $ GenericError "Malformed input."

    class Data a => EmbPrj a where
      icode :: a -> S Int
      value :: Int -> R a

    -- | Encodes something. To ensure relocatability file paths in
    -- positions are replaced with module names.

    encode :: EmbPrj a => a -> TCM ByteString
    encode a = do
        fileMod <- sourceToModule
        liftIO $ do
          newD@(Dict nD sD iD dD _ _ _ _ _) <- emptyDict fileMod
          root <- runReaderT (icode a) newD
          nL <- l nD; sL <- l sD; iL <- l iD; dL <- l dD
          return $ B.encode currentInterfaceVersion `L.append`
                   G.compress (B.encode (root, nL, sL, iL, dL))
      where l = fmap (List.map fst . List.sortBy (compare `on` snd)) . H.toList

    -- | Decodes something. The result depends on the include path.
    --
    -- Returns 'Nothing' if the input does not start with the right magic
    -- number or some other decoding error is encountered.

    decode :: EmbPrj a => ByteString -> TCM (Maybe a)
    decode s = do
      mf   <- stModuleToSource <$> get
      incs <- getIncludeDirs

      -- Note that B.runGetState and G.decompress can raise errors if the
      -- input is malformed. The decoder is (intended to be) strict enough
      -- to ensure that all such errors can be caught by the handler here.

      (mf, x) <- liftIO $ E.handle (\(E.ErrorCall {}) -> noResult) $ do

        (ver, s, _) <- return $ B.runGetState B.get s 0
        if ver /= currentInterfaceVersion
         then noResult
         else do

          ((r, nL, sL, iL, dL), s, _) <-
            return $ B.runGetState B.get (G.decompress s) 0
          if s /= L.empty
             -- G.decompress seems to throw away garbage at the end, so
             -- the then branch is possibly dead code.
           then noResult
           else do

            st <- St (ar nL) (ar sL) (ar iL) (ar dL)
                    <$> liftIO (H.new (==) hashInt2)
                    <*> return mf <*> return incs
            (r, st) <- runStateT (runErrorT (value r)) st
            return (Just (modFile st), case r of
              Left  _ -> Nothing
              Right x -> Just x)

      case mf of
        Nothing -> return ()
        Just mf -> modify $ \s -> s { stModuleToSource = mf }

      return x

      where
      ar l = listArray (0, List.length l - 1) l

      noResult = return (Nothing, Nothing)

    -- | Encodes something. To ensure relocatability file paths in
    -- positions are replaced with module names.

    encodeFile :: EmbPrj a
               => FilePath
                  -- ^ The encoded data is written to this file.
               -> a
                  -- ^ Something.
               -> TCM ()
    encodeFile f x = liftIO . L.writeFile f =<< encode x

    -- | Decodes something. The result depends on the include path.
    --
    -- Returns 'Nothing' if the file does not start with the right magic
    -- number or some other decoding error is encountered.

    decodeFile :: EmbPrj a => FilePath -> TCM (Maybe a)
    decodeFile f = decode =<< liftIO (L.readFile f)

    instance EmbPrj String where
      icode   = icodeX stringD stringC
      value i = (! i) `fmap` gets stringE

    instance EmbPrj Integer where
      icode   = icodeX integerD integerC
      value i = (! i) `fmap` gets integerE

    instance EmbPrj Int where
      icode i = return i
      value i = return i

    instance EmbPrj Char where
      icode c = return (ord c)
      value i = return (chr i)

    instance EmbPrj Double where
      icode   = icodeX doubleD doubleC
      value i = (! i) `fmap` gets doubleE

    instance (EmbPrj a, EmbPrj b) => EmbPrj (a, b) where
      icode (a, b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 (,) a b
                               valu _      = malformed

    instance (EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) where
      icode (a, b, c) = icode3' a b c
      value = vcase valu where valu [a, b, c] = valu3 (,,) a b c
                               valu _         = malformed

    instance EmbPrj a => EmbPrj (Maybe a) where
      icode Nothing  = icode0'
      icode (Just x) = icode1' x
      value = vcase valu where valu []  = valu0 Nothing
                               valu [x] = valu1 Just x
                               valu _   = malformed

    instance EmbPrj Bool where
      icode True  = icode0 0
      icode False = icode0 1
      value = vcase valu where valu [0] = valu0 True
                               valu [1] = valu0 False
                               valu _   = malformed

    instance EmbPrj AbsolutePath where
      icode file = do
        mm <- M.lookup file . fileMod <$> ask
        case mm of
          Just m  -> icode m
          Nothing -> __IMPOSSIBLE__
      value m = do
        m       <- value m
        mf      <- modFile  <$> get
        incs    <- includes <$> get
        (r, mf) <- liftIO $ findFile'' incs m mf
        modify $ \s -> s { modFile = mf }
        case r of
          Left err -> throwError $ findErrorToTypeError m err
          Right f  -> return f

    instance EmbPrj Position where
      icode (P.Pn file pos line col) = icode4' file pos line col
      value = vcase valu
        where
        valu [f, p, l, c] = valu4 P.Pn f p l c
        valu _            = malformed

    instance EmbPrj TopLevelModuleName where
      icode (TopLevelModuleName a) = icode1' a
      value = vcase valu where valu [a] = valu1 TopLevelModuleName a
                               valu _   = malformed

    instance EmbPrj a => EmbPrj [a] where
      icode xs = icodeN =<< mapM icode xs
      value = vcase $ mapM value
    --   icode []       = icode0'
    --   icode (x : xs) = icode2' x xs
    --   value = vcase valu where valu []      = valu0 []
    --                            valu [x, xs] = valu2 (:) x xs
    --                            valu _       = malformed

    instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) where
      icode m = icode (M.toList m)
      value m = M.fromList `fmap` value m

    instance (Ord a, EmbPrj a) => EmbPrj (Set a) where
      icode s = icode (S.toList s)
      value s = S.fromList `fmap` value s

    instance EmbPrj P.Interval where
      icode (P.Interval p q) = icode2' p q
      value = vcase valu where valu [p, q] = valu2 P.Interval p q
                               valu _      = malformed

    instance EmbPrj Range where
      icode (P.Range is) = icode1' is
      value = vcase valu where valu [is] = valu1 P.Range is
                               valu _    = malformed

    instance EmbPrj HR.Range where
      icode (HR.Range a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 HR.Range a b
                               valu _      = malformed

    instance EmbPrj C.Name where
      icode (C.NoName a b) = icode2 0 a b
      icode (C.Name r xs)  = icode2 1 r xs
      value = vcase valu where valu [0, a, b]  = valu2 C.NoName a b
                               valu [1, r, xs] = valu2 C.Name   r xs
                               valu _          = malformed

    instance EmbPrj NamePart where
      icode Hole   = icode0'
      icode (Id a) = icode1' a
      value = vcase valu where valu []  = valu0 Hole
                               valu [a] = valu1 Id a
                               valu _   = malformed

    instance EmbPrj C.QName where
      icode (Qual    a b) = icode2' a b
      icode (C.QName a  ) = icode1' a
      value = vcase valu where valu [a, b] = valu2 Qual    a b
                               valu [a]    = valu1 C.QName a
                               valu _      = malformed

    instance EmbPrj Scope where
      icode (Scope a b c d e f) = icode6' a b c d e f
      value = vcase valu where valu [a, b, c, d, e, f] = valu6 Scope a b c d e f
                               valu _                  = malformed

    instance EmbPrj Access where
      icode PrivateAccess = icode0 0
      icode PublicAccess  = icode0 1
      value = vcase valu where valu [0] = valu0 PrivateAccess
                               valu [1] = valu0 PublicAccess
                               valu _   = malformed

    instance EmbPrj NameSpace where
      icode (NameSpace a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 NameSpace a b
                               valu _      = malformed

    instance EmbPrj AbstractName where
      icode (AbsName a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 AbsName a b
                               valu _      = malformed

    instance EmbPrj AbstractModule where
      icode (AbsModule a) = icode a
      value n = AbsModule `fmap` value n

    instance EmbPrj KindOfName where
      icode DefName = icode0 0
      icode ConName = icode0 1
      value = vcase valu where valu [0] = valu0 DefName
                               valu [1] = valu0 ConName
                               valu _   = malformed

    instance EmbPrj Agda.Syntax.Fixity.Fixity where
      icode (LeftAssoc  a b) = icode2 0 a b
      icode (RightAssoc a b) = icode2 1 a b
      icode (NonAssoc   a b) = icode2 2 a b
      value = vcase valu where valu [0, a, b] = valu2 LeftAssoc  a b
                               valu [1, a, b] = valu2 RightAssoc a b
                               valu [2, a, b] = valu2 NonAssoc   a b
                               valu _         = malformed

    instance EmbPrj A.QName where
      icode (A.QName a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 A.QName a b
                               valu _      = malformed

    instance EmbPrj A.ModuleName where
      icode (A.MName a) = icode a
      value n = A.MName `fmap` value n

    instance EmbPrj A.Name where
      icode (A.Name a b c d) = icode4' a b c d
      value = vcase valu where valu [a, b, c, d] = valu4 A.Name a b c d
                               valu _            = malformed

    instance EmbPrj NameId where
      icode (NameId a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 NameId a b
                               valu _      = malformed

    instance EmbPrj Signature where
      icode (Sig a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 Sig a b
                               valu _      = malformed

    instance EmbPrj Section where
      icode (Section a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 Section a b
                               valu _      = malformed

    instance EmbPrj Telescope where
      icode EmptyTel        = icode0'
      icode (ExtendTel a b) = icode2' a b
      value = vcase valu where valu []     = valu0 EmptyTel
                               valu [a, b] = valu2 ExtendTel a b
                               valu _      = malformed

    instance EmbPrj Permutation where
      icode (Perm a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 Perm a b
                               valu _      = malformed

    instance (EmbPrj a) => EmbPrj (Agda.Syntax.Common.Arg a) where
      icode (Arg a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 Arg a b
                               valu _      = malformed

    instance EmbPrj Agda.Syntax.Common.Induction where
      icode Inductive   = icode0 0
      icode CoInductive = icode0 1
      value = vcase valu where valu [0] = valu0 Inductive
                               valu [1] = valu0 CoInductive
                               valu _   = malformed

    instance EmbPrj Agda.Syntax.Common.Hiding where
      icode Hidden    = icode0 0
      icode NotHidden = icode0 1
      value = vcase valu where valu [0] = valu0 Hidden
                               valu [1] = valu0 NotHidden
                               valu _   = malformed

    instance EmbPrj I.Type where
      icode (El a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 El a b
                               valu _      = malformed

    instance EmbPrj I.MetaId where
      icode (MetaId a) = icode a
      value n = MetaId `fmap` value n

    instance (EmbPrj a) => EmbPrj (I.Abs a) where
      icode (Abs a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 Abs a b
                               valu _      = malformed

    instance EmbPrj I.Term where
      icode (Var      a b) = icode2 0 a b
      icode (Lam      a b) = icode2 1 a b
      icode (Lit      a  ) = icode1 2 a
      icode (Def      a b) = icode2 3 a b
      icode (Con      a b) = icode2 4 a b
      icode (Pi       a b) = icode2 5 a b
      icode (Fun      a b) = icode2 6 a b
      icode (Sort     a  ) = icode1 7 a
      icode (MetaV    a b) = icode2 8 a b
      value = vcase valu where valu [0, a, b] = valu2 Var   a b
                               valu [1, a, b] = valu2 Lam   a b
                               valu [2, a]    = valu1 Lit   a
                               valu [3, a, b] = valu2 Def   a b
                               valu [4, a, b] = valu2 Con   a b
                               valu [5, a, b] = valu2 Pi    a b
                               valu [6, a, b] = valu2 Fun   a b
                               valu [7, a]    = valu1 Sort  a
                               valu [8, a, b] = valu2 MetaV a b
                               valu _         = malformed

    instance EmbPrj I.Sort where
      icode (Type  a  ) = icode1 0 a
      icode Prop        = icode0 1
      icode (Lub   a b) = icode2 2 a b
      icode (Suc   a  ) = icode1 3 a
      icode (MetaS a b) = icode2 4 a b
      icode Inf         = icode0 5
      icode (DLub a b)  = icode2 6 a b
      value = vcase valu where valu [0, a]    = valu1 Type  a
                               valu [1]       = valu0 Prop
                               valu [2, a, b] = valu2 Lub   a b
                               valu [3, a]    = valu1 Suc   a
                               valu [4, a, b] = valu2 MetaS a b
                               valu [5]       = valu0 Inf
                               valu [6, a, b] = valu2 DLub a b
                               valu _         = malformed

    instance EmbPrj Agda.Syntax.Literal.Literal where
      icode (LitInt    a b) = icode2 0 a b
      icode (LitFloat  a b) = icode2 1 a b
      icode (LitString a b) = icode2 2 a b
      icode (LitChar   a b) = icode2 3 a b
      icode (LitLevel  a b) = icode2 4 a b
      value = vcase valu where valu [0, a, b] = valu2 LitInt    a b
                               valu [1, a, b] = valu2 LitFloat  a b
                               valu [2, a, b] = valu2 LitString a b
                               valu [3, a, b] = valu2 LitChar   a b
                               valu [4, a, b] = valu2 LitLevel  a b
                               valu _         = malformed

    instance EmbPrj DisplayForm where
      icode (Display a b c) = icode3' a b c
      value = vcase valu where valu [a, b, c] = valu3 Display a b c
                               valu _         = malformed

    instance EmbPrj a => EmbPrj (Open a) where
      icode (OpenThing a b) = icode2' a b
      value = vcase valu where valu [a, b] = valu2 OpenThing a b
                               valu _      = malformed

    instance EmbPrj CtxId where
      icode (CtxId a) = icode a
      value n = CtxId `fmap` value n

    instance EmbPrj DisplayTerm where
      icode (DTerm    a  ) = icode1' a
      icode (DWithApp a b) = icode2' a b
      value = vcase valu where valu [a]    = valu1 DTerm a
                               valu [a, b] = valu2 DWithApp a b
                               valu _      = malformed

    instance EmbPrj MutualId where
      icode (MutId a) = icode a
      value n = MutId `fmap` value n

    instance EmbPrj Definition where
      icode (Defn a b c d e) = icode5' a b c d e
      value = vcase valu where valu [a, b, c, d, e] = valu5 Defn a b c d e
                               valu _               = malformed

    instance EmbPrj HaskellRepresentation where
      icode (HsType a)   = icode1 0 a
      icode (HsDefn a b) = icode2 1 a b

      value = vcase valu where
        valu [0, a]    = valu1 HsType a
        valu [1, a, b] = valu2 HsDefn a b
        valu _         = malformed

    instance EmbPrj Polarity where
      icode Covariant     = icode0 0
      icode Contravariant = icode0 1
      icode Invariant     = icode0 2

      value = vcase valu where
        valu [0] = valu0 Covariant
        valu [1] = valu0 Contravariant
        valu [2] = valu0 Invariant
        valu _   = malformed

    instance EmbPrj Occurrence where
      icode Positive = icode0 0
      icode Negative = icode0 1
      icode Unused   = icode0 2

      value = vcase valu where
        valu [0] = valu0 Positive
        valu [1] = valu0 Negative
        valu [2] = valu0 Unused
        valu _   = malformed

    instance EmbPrj Defn where
      icode (Axiom       a)                   = icode1 0 a
      icode (Function    a b c d e f)         = icode6 1 a b c d e f
      icode (Datatype    a b c d e f g h i j) = icode10 2 a b c d e f g h i j
      icode (Record      a b c d e f g h i)   = icode9 3 a b c d e f g h i
      icode (Constructor a b c d e f)         = icode6 4 a b c d e f
      icode (Primitive   a b c)               = icode3 5 a b c
      value = vcase valu where
        valu [0, a]                            = valu1 Axiom       a
        valu [1, a, b, c, d, e, f]             = valu6 Function    a b c d e f
        valu [2, a, b, c, d, e, f, g, h, i, j] = valu10 Datatype    a b c d e f g h i j
        valu [3, a, b, c, d, e, f, g, h, i]    = valu9 Record      a b c d e f g h i
        valu [4, a, b, c, d, e, f]             = valu6 Constructor a b c d e f
        valu [5, a, b, c]                      = valu3 Primitive   a b c
        valu _                                 = malformed

    instance EmbPrj FunctionInverse where
      icode NotInjective = icode0'
      icode (Inverse a)  = icode1' a
      value = vcase valu where valu []  = valu0 NotInjective
                               valu [a] = valu1 Inverse a
                               valu _   = malformed

    instance EmbPrj TermHead where
      icode SortHead    = icode0 0
      icode PiHead      = icode0 1
      icode (ConHead a) = icode1 2 a
      value = vcase valu where valu [0]    = return SortHead
                               valu [1]    = return PiHead
                               valu [2, a] = valu1 ConHead a
                               valu _      = malformed

    instance EmbPrj Agda.Syntax.Common.IsAbstract where
      icode AbstractDef = icode0 0
      icode ConcreteDef = icode0 1
      value = vcase valu where valu [0] = valu0 AbstractDef
                               valu [1] = valu0 ConcreteDef
                               valu _   = malformed

    instance EmbPrj I.Clause where
      icode (Clause a b c d e) = icode5' a b c d e
      value = vcase valu where valu [a, b, c, d, e] = valu5 Clause a b c d e
                               valu _               = malformed

    instance EmbPrj I.ClauseBody where
      icode (Body   a) = icode1 0 a
      icode (Bind   a) = icode1 1 a
      icode (NoBind a) = icode1 2 a
      icode NoBody     = icode0'
      value = vcase valu where valu [0, a] = valu1 Body   a
                               valu [1, a] = valu1 Bind   a
                               valu [2, a] = valu1 NoBind a
                               valu []     = valu0 NoBody
                               valu _      = malformed

    instance EmbPrj Delayed where
      icode Delayed    = icode0 0
      icode NotDelayed = icode0 1
      value = vcase valu where valu [0] = valu0 Delayed
                               valu [1] = valu0 NotDelayed
                               valu _   = malformed

    instance EmbPrj I.Pattern where
      icode (VarP a  ) = icode1 0 a
      icode (ConP a b) = icode2 1 a b
      icode (LitP a  ) = icode1 2 a
      icode (DotP a  ) = icode1 3 a
      value = vcase valu where valu [0, a]    = valu1 VarP a
                               valu [1, a, b] = valu2 ConP a b
                               valu [2, a]    = valu1 LitP a
                               valu [3, a]    = valu1 DotP a
                               valu _         = malformed

    instance EmbPrj a => EmbPrj (Builtin a) where
      icode (Prim    a) = icode1 0 a
      icode (Builtin a) = icode1 1 a
      value = vcase valu where valu [0, a] = valu1 Prim    a
                               valu [1, a] = valu1 Builtin a
                               valu _      = malformed

    instance EmbPrj HP.NameKind where
      icode HP.Bound           = icode0 0
      icode (HP.Constructor a) = icode1 1 a
      icode HP.Datatype        = icode0 2
      icode HP.Field           = icode0 3
      icode HP.Function        = icode0 4
      icode HP.Module          = icode0 5
      icode HP.Postulate       = icode0 6
      icode HP.Primitive       = icode0 7
      icode HP.Record          = icode0 8

      value = vcase valu where
        valu [0]     = valu0 HP.Bound
        valu [1 , a] = valu1 HP.Constructor a
        valu [2]     = valu0 HP.Datatype
        valu [3]     = valu0 HP.Field
        valu [4]     = valu0 HP.Function
        valu [5]     = valu0 HP.Module
        valu [6]     = valu0 HP.Postulate
        valu [7]     = valu0 HP.Primitive
        valu [8]     = valu0 HP.Record
        valu _       = malformed

    instance EmbPrj HP.Aspect where
      icode HP.Comment       = icode0 0
      icode HP.Keyword       = icode0 1
      icode HP.String        = icode0 2
      icode HP.Number        = icode0 3
      icode HP.Symbol        = icode0 4
      icode HP.PrimitiveType = icode0 5
      icode (HP.Name mk b)   = icode2 6 mk b

      value = vcase valu where
        valu [0]        = valu0 HP.Comment
        valu [1]        = valu0 HP.Keyword
        valu [2]        = valu0 HP.String
        valu [3]        = valu0 HP.Number
        valu [4]        = valu0 HP.Symbol
        valu [5]        = valu0 HP.PrimitiveType
        valu [6, mk, b] = valu2 HP.Name mk b
        valu _          = malformed

    instance EmbPrj HP.OtherAspect where
      icode HP.Error              = icode0 0
      icode HP.DottedPattern      = icode0 1
      icode HP.UnsolvedMeta       = icode0 2
      icode HP.TerminationProblem = icode0 3
      icode HP.IncompletePattern  = icode0 4

      value = vcase valu where
        valu [0] = valu0 HP.Error
        valu [1] = valu0 HP.DottedPattern
        valu [2] = valu0 HP.UnsolvedMeta
        valu [3] = valu0 HP.TerminationProblem
        valu [4] = valu0 HP.IncompletePattern
        valu _   = malformed

    instance EmbPrj HP.MetaInfo where
      icode (HP.MetaInfo a b c d) = icode4' a b c d

      value = vcase valu where
        valu [a, b, c, d] = valu4 HP.MetaInfo a b c d
        valu _            = malformed

    instance EmbPrj Precedence where
      icode TopCtx                 = icode0 0
      icode FunctionSpaceDomainCtx = icode0 1
      icode (LeftOperandCtx a)     = icode1 2 a
      icode (RightOperandCtx a)    = icode1 3 a
      icode FunctionCtx            = icode0 4
      icode ArgumentCtx            = icode0 5
      icode InsideOperandCtx       = icode0 6
      icode WithFunCtx             = icode0 7
      icode WithArgCtx             = icode0 8
      icode DotPatternCtx          = icode0 9
      value = vcase valu
        where
        valu [0]    = valu0 TopCtx
        valu [1]    = valu0 FunctionSpaceDomainCtx
        valu [2, a] = valu1 LeftOperandCtx a
        valu [3, a] = valu1 RightOperandCtx a
        valu [4]    = valu0 FunctionCtx
        valu [5]    = valu0 ArgumentCtx
        valu [6]    = valu0 InsideOperandCtx
        valu [7]    = valu0 WithFunCtx
        valu [8]    = valu0 WithArgCtx
        valu [9]    = valu0 DotPatternCtx
        valu _      = malformed

    instance EmbPrj ScopeInfo where
      icode (ScopeInfo a b c d) = icode4' a b c d
      value = vcase valu where valu [a, b, c, d] = valu4 ScopeInfo a b c d
                               valu _            = malformed

    instance EmbPrj Interface where
      icode (Interface a b c d e f g h) = icode8' a b c d e f g h
      value = vcase valu where valu [a, b, c, d, e, f, g, h] = valu8 Interface a b c d e f g h
                               valu _                        = malformed

    icodeX :: (Dict -> HashTable k Int) -> (Dict -> IORef Int) ->
              k -> S Int
    icodeX dict counter key = do
      d     <- asks dict
      c     <- asks counter
      fresh <- lift $ readIORef c
      mi    <- lift $ H.lookup d key
      case mi of
        Just i  -> return i
        Nothing -> do lift $ H.insert d key fresh
                      lift $ writeIORef c (fresh + 1)
                      return fresh

    icodeN = icodeX nodeD nodeC

    vcase :: forall a . EmbPrj a => ([Int] -> R a) -> Int -> R a
    vcase valu ix = do
        memo <- gets nodeMemo
        (aTyp, maybeU) <- liftIO $ do
          aTyp   <- typeRepKey $ typeOf (undefined :: a)
          maybeU <- H.lookup memo (ix, aTyp)
          return (aTyp, maybeU)
        case maybeU of
          Just (U u) -> maybe malformed return (cast u)
          Nothing    -> do
              v <- valu . (! ix) =<< gets nodeE
              liftIO $ H.insert memo (ix, aTyp) (U v)
              return v

    icode0  tag                     = icodeN [tag]
    icode1  tag a                   = icodeN . (tag :) =<< sequence [icode a]
    icode2  tag a b                 = icodeN . (tag :) =<< sequence [icode a, icode b]
    icode3  tag a b c               = icodeN . (tag :) =<< sequence [icode a, icode b, icode c]
    icode4  tag a b c d             = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d]
    icode5  tag a b c d e           = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e]
    icode6  tag a b c d e f         = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f]
    icode7  tag a b c d e f g       = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g]
    icode8  tag a b c d e f g h     = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h]
    icode9  tag a b c d e f g h i   = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i]
    icode10 tag a b c d e f g h i j = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j]

    icode0'                      = icodeN []
    icode1'  a                   = icodeN =<< sequence [icode a]
    icode2'  a b                 = icodeN =<< sequence [icode a, icode b]
    icode3'  a b c               = icodeN =<< sequence [icode a, icode b, icode c]
    icode4'  a b c d             = icodeN =<< sequence [icode a, icode b, icode c, icode d]
    icode5'  a b c d e           = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e]
    icode6'  a b c d e f         = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f]
    icode7'  a b c d e f g       = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g]
    icode8'  a b c d e f g h     = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h]
    icode9'  a b c d e f g h i   = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i]
    icode10' a b c d e f g h i j = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j]

    valu0  z                     = return z
    valu1  z a                   = valu0 z                   `ap` value a
    valu2  z a b                 = valu1 z a                 `ap` value b
    valu3  z a b c               = valu2 z a b               `ap` value c
    valu4  z a b c d             = valu3 z a b c             `ap` value d
    valu5  z a b c d e           = valu4 z a b c d           `ap` value e
    valu6  z a b c d e f         = valu5 z a b c d e         `ap` value f
    valu7  z a b c d e f g       = valu6 z a b c d e f       `ap` value g
    valu8  z a b c d e f g h     = valu7 z a b c d e f g     `ap` value h
    valu9  z a b c d e f g h i   = valu8 z a b c d e f g h   `ap` value i
    valu10 z a b c d e f g h i j = valu9 z a b c d e f g h i `ap` value j

    -- | Creates an empty dictionary.

    emptyDict :: SourceToModule
                 -- ^ Maps file names to the corresponding module names.
                 -- Must contain a mapping for every file name that is
                 -- later encountered.
              -> IO Dict
    emptyDict fileMod = Dict
      <$> H.new (==) hashNode
      <*> H.new (==) H.hashString
      <*> H.new (==) (H.hashInt . fromIntegral)
      <*> H.new (==) (H.hashInt . floor)
      <*> newIORef 0
      <*> newIORef 0
      <*> newIORef 0
      <*> newIORef 0
      <*> return fileMod

    hashNode :: [ Int ] -> Int32
    hashNode is = List.foldl' f golden is
       where f m c = fromIntegral c * magic + hashInt32 m
             magic  = 0xdeadbeef
             golden :: Int32
             golden = 1013904242
             hashInt32 x = mulHi x golden + x
             mulHi :: Int32 -> Int32 -> Int32
             mulHi a b = fromIntegral (r `shiftR` 32)
                 where r :: Int64
                       r = fromIntegral a * fromIntegral b

    hashInt2 :: (Int, Int) -> Int32
    hashInt2 (ix, rep) = hashNode [ix , rep]