{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.TypeChecking.Serialise.Instances.Highlighting where

import Control.Monad.Reader
import qualified Data.Map.Strict as Map

import Agda.Utils.Monad
import Agda.Utils.Range (Range(..))
import qualified Agda.Interaction.Highlighting.Precise as HP
import Agda.Utils.RangeMap (PairInt(..))
import qualified Agda.Utils.RangeMap as RM

import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common () --instance only

instance EmbPrj Range where
  icod_ :: Range -> S Word32
icod_ (Range Int
a Int
b) = (Int -> Int -> Range)
-> Arrows (Domains (Int -> Int -> Range)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Int -> Int -> Range
Range Int
a Int
b

  value :: Word32 -> R Range
value = (Int -> Int -> Range)
-> Word32 -> R (CoDomain (Int -> Int -> Range))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Int -> Int -> Range
Range

instance EmbPrj HP.NameKind where
  icod_ :: NameKind -> S Word32
icod_ NameKind
HP.Bound           = NameKind -> Arrows (Domains NameKind) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' NameKind
HP.Bound
  icod_ (HP.Constructor Induction
a) = Word32
-> (Induction -> NameKind)
-> Arrows (Domains (Induction -> NameKind)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Induction -> NameKind
HP.Constructor Induction
a
  icod_ NameKind
HP.Datatype        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 ()
  icod_ NameKind
HP.Field           = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
3 ()
  icod_ NameKind
HP.Function        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
4 ()
  icod_ NameKind
HP.Module          = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
5 ()
  icod_ NameKind
HP.Postulate       = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
6 ()
  icod_ NameKind
HP.Primitive       = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
7 ()
  icod_ NameKind
HP.Record          = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
8 ()
  icod_ NameKind
HP.Argument        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
9 ()
  icod_ NameKind
HP.Macro           = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
10 ()
  icod_ NameKind
HP.Generalizable   = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
11 ()

  value :: Word32 -> R NameKind
value = (Node -> R NameKind) -> Word32 -> R NameKind
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R NameKind
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
valu Node
N0       = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Bound
    valu (N2 Word32
1 Word32
a) = (Induction -> NameKind)
-> Arrows
     (Constant Word32 (Domains (Induction -> NameKind)))
     (R (CoDomain (Induction -> NameKind)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Induction -> NameKind
HP.Constructor Word32
a
    valu (N1 Word32
2)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Datatype
    valu (N1 Word32
3)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Field
    valu (N1 Word32
4)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Function
    valu (N1 Word32
5)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Module
    valu (N1 Word32
6)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Postulate
    valu (N1 Word32
7)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Primitive
    valu (N1 Word32
8)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Record
    valu (N1 Word32
9)   = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Argument
    valu (N1 Word32
10)  = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Macro
    valu (N1 Word32
11)  = NameKind
-> Arrows
     (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameKind
HP.Generalizable
    valu Node
_        = R NameKind
Arrows (Constant Word32 (Domains NameKind)) (R (CoDomain NameKind))
forall a. HasCallStack => R a
malformed

instance EmbPrj HP.Aspect where
  icod_ :: Aspect -> S Word32
icod_ Aspect
HP.Comment        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 ()
  icod_ Aspect
HP.Keyword       = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 ()
  icod_ Aspect
HP.String        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 ()
  icod_ Aspect
HP.Number        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
3 ()
  icod_ Aspect
HP.Symbol        = Aspect -> Arrows (Domains Aspect) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Aspect
HP.Symbol
  icod_ Aspect
HP.PrimitiveType = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
4 ()
  icod_ (HP.Name Maybe NameKind
mk Bool
b)   = Word32
-> (Maybe NameKind -> Bool -> Aspect)
-> Arrows (Domains (Maybe NameKind -> Bool -> Aspect)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
5 Maybe NameKind -> Bool -> Aspect
HP.Name Maybe NameKind
mk Bool
b
  icod_ Aspect
HP.Pragma        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
6 ()
  icod_ Aspect
HP.Background    = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
7 ()
  icod_ Aspect
HP.Markup        = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
8 ()
  icod_ Aspect
HP.Hole          = Word32 -> () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
9 ()
  icod_ (HP.URL Text
a)       = Word32
-> (Text -> Aspect) -> Arrows (Domains (Text -> Aspect)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
10 Text -> Aspect
HP.URL Text
a

  value :: Word32 -> R Aspect
value = (Node -> R Aspect) -> Word32 -> R Aspect
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R Aspect
valu where
    valu :: Node
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
valu (N1 Word32
0)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Comment
    valu (N1 Word32
1)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Keyword
    valu (N1 Word32
2)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.String
    valu (N1 Word32
3)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Number
    valu Node
N0          = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Symbol
    valu (N1 Word32
4)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.PrimitiveType
    valu (N3 Word32
5 Word32
mk Word32
b) = (Maybe NameKind -> Bool -> Aspect)
-> Arrows
     (Constant Word32 (Domains (Maybe NameKind -> Bool -> Aspect)))
     (R (CoDomain (Maybe NameKind -> Bool -> Aspect)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Maybe NameKind -> Bool -> Aspect
HP.Name Word32
mk Word32
b
    valu (N1 Word32
6)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Pragma
    valu (N1 Word32
7)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Background
    valu (N1 Word32
8)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Markup
    valu (N1 Word32
9)      = Aspect
-> Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Aspect
HP.Hole
    valu (N2 Word32
10 Word32
a)   = (Text -> Aspect)
-> Arrows
     (Constant Word32 (Domains (Text -> Aspect)))
     (R (CoDomain (Text -> Aspect)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Text -> Aspect
HP.URL Word32
a
    valu Node
_           = R Aspect
Arrows (Constant Word32 (Domains Aspect)) (R (CoDomain Aspect))
forall a. HasCallStack => R a
malformed

instance EmbPrj HP.OtherAspect where
  icod_ :: OtherAspect -> S Word32
icod_ OtherAspect
HP.Error                = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0
  icod_ OtherAspect
HP.ErrorWarning         = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
1
  icod_ OtherAspect
HP.DottedPattern        = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
2
  icod_ OtherAspect
HP.UnsolvedMeta         = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
3
  icod_ OtherAspect
HP.TerminationProblem   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
4
  icod_ OtherAspect
HP.IncompletePattern    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
5
  icod_ OtherAspect
HP.TypeChecks           = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
6
  icod_ OtherAspect
HP.UnsolvedConstraint   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
7
  icod_ OtherAspect
HP.PositivityProblem    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
8
  icod_ OtherAspect
HP.Deadcode             = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
9
  icod_ OtherAspect
HP.CoverageProblem      = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
10
  icod_ OtherAspect
HP.CatchallClause       = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
11
  icod_ OtherAspect
HP.ConfluenceProblem    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
12
  icod_ OtherAspect
HP.MissingDefinition    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
13
  icod_ OtherAspect
HP.ShadowingInTelescope = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
14
  icod_ OtherAspect
HP.CosmeticProblem      = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
15
  icod_ OtherAspect
HP.InstanceProblem      = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
16

  value :: Word32 -> R OtherAspect
value = \case
    Word32
0  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.Error
    Word32
1  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.ErrorWarning
    Word32
2  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.DottedPattern
    Word32
3  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.UnsolvedMeta
    Word32
4  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.TerminationProblem
    Word32
5  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.IncompletePattern
    Word32
6  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.TypeChecks
    Word32
7  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.UnsolvedConstraint
    Word32
8  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.PositivityProblem
    Word32
9  -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.Deadcode
    Word32
10 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.CoverageProblem
    Word32
11 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.CatchallClause
    Word32
12 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.ConfluenceProblem
    Word32
13 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.MissingDefinition
    Word32
14 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.ShadowingInTelescope
    Word32
15 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.CosmeticProblem
    Word32
16 -> OtherAspect -> R OtherAspect
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure OtherAspect
HP.InstanceProblem
    Word32
_  -> R OtherAspect
forall a. HasCallStack => R a
malformed

instance EmbPrj HP.Aspects where
  icod_ :: Aspects -> S Word32
icod_ (HP.Aspects Maybe Aspect
a Set OtherAspect
b String
c Maybe DefinitionSite
d TokenBased
e) = (Maybe Aspect
 -> Set OtherAspect
 -> String
 -> Maybe DefinitionSite
 -> TokenBased
 -> Aspects)
-> Arrows
     (Domains
        (Maybe Aspect
         -> Set OtherAspect
         -> String
         -> Maybe DefinitionSite
         -> TokenBased
         -> Aspects))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Maybe Aspect
-> Set OtherAspect
-> String
-> Maybe DefinitionSite
-> TokenBased
-> Aspects
HP.Aspects Maybe Aspect
a Set OtherAspect
b String
c Maybe DefinitionSite
d TokenBased
e

  value :: Word32 -> R Aspects
value = (Maybe Aspect
 -> Set OtherAspect
 -> String
 -> Maybe DefinitionSite
 -> TokenBased
 -> Aspects)
-> Word32
-> R (CoDomain
        (Maybe Aspect
         -> Set OtherAspect
         -> String
         -> Maybe DefinitionSite
         -> TokenBased
         -> Aspects))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Maybe Aspect
-> Set OtherAspect
-> String
-> Maybe DefinitionSite
-> TokenBased
-> Aspects
HP.Aspects

instance EmbPrj HP.DefinitionSite where
  icod_ :: DefinitionSite -> S Word32
icod_ (HP.DefinitionSite TopLevelModuleName' Range
a Int
b Bool
c Maybe String
d) = (TopLevelModuleName' Range
 -> Int -> Bool -> Maybe String -> DefinitionSite)
-> Arrows
     (Domains
        (TopLevelModuleName' Range
         -> Int -> Bool -> Maybe String -> DefinitionSite))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' TopLevelModuleName' Range
-> Int -> Bool -> Maybe String -> DefinitionSite
HP.DefinitionSite TopLevelModuleName' Range
a Int
b Bool
c Maybe String
d

  value :: Word32 -> R DefinitionSite
value = (TopLevelModuleName' Range
 -> Int -> Bool -> Maybe String -> DefinitionSite)
-> Word32
-> R (CoDomain
        (TopLevelModuleName' Range
         -> Int -> Bool -> Maybe String -> DefinitionSite))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN TopLevelModuleName' Range
-> Int -> Bool -> Maybe String -> DefinitionSite
HP.DefinitionSite

data KVS a = Cons !Int !Int a !(KVS a) | Nil

toAscList' :: RM.RangeMap a -> KVS a
toAscList' :: forall a. RangeMap a -> KVS a
toAscList' (RM.RangeMap Map Int (PairInt a)
x) =
  (Int -> PairInt a -> KVS a -> KVS a)
-> KVS a -> Map Int (PairInt a) -> KVS a
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey'
    (\Int
a (Int
b :!: a
c) !KVS a
acc -> Int -> Int -> a -> KVS a -> KVS a
forall a. Int -> Int -> a -> KVS a -> KVS a
Cons Int
a Int
b a
c KVS a
acc)
    KVS a
forall a. KVS a
Nil Map Int (PairInt a)
x

{-# INLINABLE icodRM #-}
icodRM :: EmbPrj a => KVS a -> S Node
icodRM :: forall a. EmbPrj a => KVS a -> S Node
icodRM KVS a
xs = (Dict -> IO Node) -> S Node
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT \Dict
r -> case KVS a
xs of
  KVS a
Nil ->
    Node -> IO Node
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Node
N0
  Cons Int
a Int
b a
c KVS a
Nil -> (S Node -> Dict -> IO Node) -> Dict -> S Node -> IO Node
forall a b c. (a -> b -> c) -> b -> a -> c
flip S Node -> Dict -> IO Node
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Dict
r (S Node -> IO Node) -> S Node -> IO Node
forall a b. (a -> b) -> a -> b
$
    Word32 -> Word32 -> Word32 -> Node
N3 (Word32 -> Word32 -> Word32 -> Node)
-> S Word32 -> ReaderT Dict IO (Word32 -> Word32 -> Node)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
a ReaderT Dict IO (Word32 -> Word32 -> Node)
-> S Word32 -> ReaderT Dict IO (Word32 -> Node)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
b ReaderT Dict IO (Word32 -> Node) -> S Word32 -> S Node
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode a
c
  Cons Int
a Int
b a
c (Cons Int
d Int
e a
f KVS a
xs) -> (S Node -> Dict -> IO Node) -> Dict -> S Node -> IO Node
forall a b c. (a -> b -> c) -> b -> a -> c
flip S Node -> Dict -> IO Node
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Dict
r (S Node -> IO Node) -> S Node -> IO Node
forall a b. (a -> b) -> a -> b
$
    Word32
-> Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> Node -> Node
N6 (Word32
 -> Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> Node -> Node)
-> S Word32
-> ReaderT
     Dict
     IO
     (Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> Node -> Node)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
a ReaderT
  Dict
  IO
  (Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> Node -> Node)
-> S Word32
-> ReaderT
     Dict IO (Word32 -> Word32 -> Word32 -> Word32 -> Node -> Node)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
b ReaderT
  Dict IO (Word32 -> Word32 -> Word32 -> Word32 -> Node -> Node)
-> S Word32
-> ReaderT Dict IO (Word32 -> Word32 -> Word32 -> Node -> Node)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode a
c
       ReaderT Dict IO (Word32 -> Word32 -> Word32 -> Node -> Node)
-> S Word32 -> ReaderT Dict IO (Word32 -> Word32 -> Node -> Node)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
d ReaderT Dict IO (Word32 -> Word32 -> Node -> Node)
-> S Word32 -> ReaderT Dict IO (Word32 -> Node -> Node)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
e ReaderT Dict IO (Word32 -> Node -> Node)
-> S Word32 -> ReaderT Dict IO (Node -> Node)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode a
f ReaderT Dict IO (Node -> Node) -> S Node -> S Node
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<*!> KVS a -> S Node
forall a. EmbPrj a => KVS a -> S Node
icodRM KVS a
xs

{-# INLINABLE valueRM #-}
valueRM :: EmbPrj a => Node -> R [(Int, PairInt a)]
valueRM :: forall a. EmbPrj a => Node -> R [(Int, PairInt a)]
valueRM Node
as = (Decode -> IO [(Int, PairInt a)])
-> ReaderT Decode IO [(Int, PairInt a)]
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT \Decode
r -> case Node
as of
  Node
N0 ->
    [(Int, PairInt a)] -> IO [(Int, PairInt a)]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  N3 Word32
a Word32
b Word32
c -> (ReaderT Decode IO [(Int, PairInt a)]
 -> Decode -> IO [(Int, PairInt a)])
-> Decode
-> ReaderT Decode IO [(Int, PairInt a)]
-> IO [(Int, PairInt a)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Decode IO [(Int, PairInt a)]
-> Decode -> IO [(Int, PairInt a)]
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Decode
r do
    !a <- Word32 -> R Int
forall a. EmbPrj a => Word32 -> R a
value Word32
a
    !b <- value b
    !c <- value c
    pure [(a, b :!: c)]
  N6 Word32
a Word32
b Word32
c Word32
d Word32
e Word32
f Node
as -> (ReaderT Decode IO [(Int, PairInt a)]
 -> Decode -> IO [(Int, PairInt a)])
-> Decode
-> ReaderT Decode IO [(Int, PairInt a)]
-> IO [(Int, PairInt a)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Decode IO [(Int, PairInt a)]
-> Decode -> IO [(Int, PairInt a)]
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Decode
r do
    !a  <- Word32 -> R Int
forall a. EmbPrj a => Word32 -> R a
value Word32
a
    !b  <- value b
    !c  <- value c
    !d  <- value d
    !e  <- value e
    !f  <- value f
    !as <- valueRM as
    pure ((a, b :!: c):(d, e :!: f):as)
  Node
_ -> IO [(Int, PairInt a)]
forall a. HasCallStack => IO a
malformedIO

-- We serialize as a flat list of triples
instance EmbPrj a => EmbPrj (RM.RangeMap a) where
  {-# INLINE icod_ #-}
  icod_ :: RangeMap a -> S Word32
icod_ RangeMap a
x = Node -> S Word32
icodeNode (Node -> S Word32) -> S Node -> S Word32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< KVS a -> S Node
forall a. EmbPrj a => KVS a -> S Node
icodRM (RangeMap a -> KVS a
forall a. RangeMap a -> KVS a
toAscList' RangeMap a
x) where
  {-# INLINE value #-}
  value :: Word32 -> R (RangeMap a)
value = (Node -> R (RangeMap a)) -> Word32 -> R (RangeMap a)
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase (\Node
n -> Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RM.RangeMap (Map Int (PairInt a) -> RangeMap a)
-> ([(Int, PairInt a)] -> Map Int (PairInt a))
-> [(Int, PairInt a)]
-> RangeMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, PairInt a)] -> Map Int (PairInt a)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(Int, PairInt a)] -> RangeMap a)
-> ReaderT Decode IO [(Int, PairInt a)] -> R (RangeMap a)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Node -> ReaderT Decode IO [(Int, PairInt a)]
forall a. EmbPrj a => Node -> R [(Int, PairInt a)]
valueRM Node
n) where

instance EmbPrj HP.TokenBased where
  icod_ :: TokenBased -> S Word32
icod_ TokenBased
HP.TokenBased        = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0
  icod_ TokenBased
HP.NotOnlyTokenBased = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
1

  value :: Word32 -> R TokenBased
value = \case
    Word32
0 -> TokenBased -> R TokenBased
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TokenBased
HP.TokenBased
    Word32
1 -> TokenBased -> R TokenBased
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TokenBased
HP.NotOnlyTokenBased
    Word32
_ -> R TokenBased
forall a. HasCallStack => R a
malformed