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

module Agda.TypeChecking.Serialise.Instances.Internal where

import qualified Data.HashSet as HashSet
import Control.Monad
import Control.Monad.IO.Class

import Agda.Syntax.Internal as I
import Agda.Syntax.Position as P

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Coverage.SplitTree

import Agda.Utils.Permutation

import Agda.Utils.Impossible

instance EmbPrj a => EmbPrj (Dom a) where
  icod_ :: Dom a -> S Int32
icod_ (Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f

  value :: Int32 -> R (Dom a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom

instance EmbPrj Signature where
  icod_ :: Signature -> S Int32
icod_ (Sig Sections
a Definitions
b RewriteRuleMap
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Sections -> Definitions -> RewriteRuleMap -> Signature
Sig Sections
a Definitions
b RewriteRuleMap
c

  value :: Int32 -> R Signature
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Sections -> Definitions -> RewriteRuleMap -> Signature
Sig

instance EmbPrj Section where
  icod_ :: Section -> S Int32
icod_ (Section Telescope
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Telescope -> Section
Section Telescope
a

  value :: Int32 -> R Section
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Telescope -> Section
Section

instance EmbPrj a => EmbPrj (Tele a) where
  icod_ :: Tele a -> S Int32
icod_ Tele a
EmptyTel        = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Tele a
EmptyTel
  icod_ (ExtendTel a
a Abs (Tele a)
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a Abs (Tele a)
b

  value :: Int32 -> R (Tele a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> StateT St IO (Tele a)
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele a)))
valu []     = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Tele a
EmptyTel
    valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Int32
a Int32
b
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj Permutation where
  icod_ :: Permutation -> S Int32
icod_ (Perm Int
a [Int]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> [Int] -> Permutation
Perm Int
a [Int]
b

  value :: Int32 -> R Permutation
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> [Int] -> Permutation
Perm

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

  value :: Int32 -> R (Drop a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Int -> a -> Drop a
Drop

instance EmbPrj a => EmbPrj (Elim' a) where
  icod_ :: Elim' a -> S Int32
icod_ (Apply Arg a
a)      = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Arg a -> Elim' a
Apply Arg a
a
  icod_ (IApply a
x a
y a
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. a -> a -> a -> Elim' a
IApply a
x a
y a
a
  icod_ (Proj ProjOrigin
a QName
b)     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
a QName
b

  value :: Int32 -> R (Elim' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (Elim' a)
valu where
    valu :: [Int32] -> R (Elim' a)
valu [Int32
a]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Arg a -> Elim' a
Apply Int32
a
    valu [Int32
0,Int32
x,Int32
y,Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> a -> a -> Elim' a
IApply Int32
x Int32
y Int32
a
    valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. ProjOrigin -> QName -> Elim' a
Proj Int32
a Int32
b
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj I.DataOrRecord where
  icod_ :: DataOrRecord -> S Int32
icod_ = \case
    DataOrRecord
IsData      -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall p. DataOrRecord' p
IsData
    IsRecord PatternOrCopattern
pm -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
pm

  value :: Int32 -> R DataOrRecord
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
    []   -> forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall p. DataOrRecord' p
IsData
    [Int32
pm] -> forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall p. p -> DataOrRecord' p
IsRecord Int32
pm
    [Int32]
_    -> forall a. R a
malformed

instance EmbPrj I.ConHead where
  icod_ :: ConHead -> S Int32
icod_ (ConHead QName
a DataOrRecord
b Induction
c [Arg QName]
d) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
a DataOrRecord
b Induction
c [Arg QName]
d

  value :: Int32 -> R ConHead
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead

instance (EmbPrj a) => EmbPrj (I.Type' a) where
  icod_ :: Type' a -> S Int32
icod_ (El Sort
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t a. Sort' t -> a -> Type'' t a
El Sort
a a
b

  value :: Int32 -> R (Type' a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t a. Sort' t -> a -> Type'' t a
El

instance EmbPrj a => EmbPrj (I.Abs a) where
  icod_ :: Abs a -> S Int32
icod_ (NoAbs ArgName
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. ArgName -> a -> Abs a
NoAbs ArgName
a a
b
  icod_ (Abs ArgName
a a
b)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. ArgName -> a -> Abs a
Abs ArgName
a a
b

  value :: Int32 -> R (Abs a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (Abs a)
valu where
    valu :: [Int32] -> R (Abs a)
valu [Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. ArgName -> a -> Abs a
Abs Int32
a Int32
b
    valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. ArgName -> a -> Abs a
NoAbs Int32
a Int32
b
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj I.Term where
  icod_ :: Term -> S Int32
icod_ (Var     Int
a []) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ Int
a -> Int -> Elims -> Term
Var Int
a []) Int
a
  icod_ (Var      Int
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Int -> Elims -> Term
Var Int
a Elims
b
  icod_ (Lam      ArgInfo
a Abs Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 ArgInfo -> Abs Term -> Term
Lam ArgInfo
a Abs Term
b
  icod_ (Lit      Literal
a  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Literal -> Term
Lit Literal
a
  icod_ (Def      QName
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 QName -> Elims -> Term
Def QName
a Elims
b
  icod_ (Con    ConHead
a ConInfo
b Elims
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 ConHead -> ConInfo -> Elims -> Term
Con ConHead
a ConInfo
b Elims
c
  icod_ (Pi       Dom' Term Type
a Abs Type
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 Dom' Term Type -> Abs Type -> Term
Pi Dom' Term Type
a Abs Type
b
  icod_ (MetaV    MetaId
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 MetaId -> Elims -> Term
MetaV MetaId
a Elims
b
  icod_ (Sort     Sort
a  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 Sort -> Term
Sort Sort
a
  icod_ (DontCare Term
a  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
8 Term -> Term
DontCare Term
a
  icod_ (Level    Level
a  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
9 Level -> Term
Level Level
a
  icod_ (Dummy    ArgName
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
10 ArgName -> Elims -> Term
Dummy ArgName
a Elims
b

  value :: Int32 -> R Term
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R Term
valu where
    valu :: [Int32] -> R Term
valu [Int32
a]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Term
var   Int32
a
    valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Elims -> Term
Var   Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgInfo -> Abs Term -> Term
Lam   Int32
a Int32
b
    valu [Int32
2, Int32
a]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Literal -> Term
Lit   Int32
a
    valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> Elims -> Term
Def   Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConInfo -> Elims -> Term
Con Int32
a Int32
b Int32
c
    valu [Int32
5, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom' Term Type -> Abs Type -> Term
Pi    Int32
a Int32
b
    valu [Int32
6, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN MetaId -> Elims -> Term
MetaV Int32
a Int32
b
    valu [Int32
7, Int32
a]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort -> Term
Sort  Int32
a
    valu [Int32
8, Int32
a]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Term
DontCare Int32
a
    valu [Int32
9, Int32
a]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Level -> Term
Level Int32
a
    valu [Int32
10, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgName -> Elims -> Term
Dummy Int32
a Int32
b
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj Level where
  icod_ :: Level -> S Int32
icod_ (Max Integer
a [PlusLevel]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
a [PlusLevel]
b

  value :: Int32 -> R Level
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t. Integer -> [PlusLevel' t] -> Level' t
Max

instance EmbPrj PlusLevel where
  icod_ :: PlusLevel -> S Int32
icod_ (Plus Integer
a Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t. Integer -> t -> PlusLevel' t
Plus Integer
a Term
b

  value :: Int32 -> R PlusLevel
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t. Integer -> t -> PlusLevel' t
Plus

instance EmbPrj IsFibrant where
  icod_ :: IsFibrant -> S Int32
icod_ IsFibrant
IsFibrant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ IsFibrant
IsStrict  = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1

  value :: Int32 -> R IsFibrant
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return IsFibrant
IsFibrant
  value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return IsFibrant
IsStrict
  value Int32
_ = forall a. R a
malformed

instance EmbPrj Univ where

instance EmbPrj I.Sort where
  icod_ :: Sort -> S Int32
icod_ = \case
    Univ Univ
a Level
b     -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0  forall t. Univ -> Level' t -> Sort' t
Univ Univ
a Level
b
    Sort
SizeUniv     -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2  forall t. Sort' t
SizeUniv
    Inf Univ
a Integer
b      -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3  forall t. Univ -> Integer -> Sort' t
Inf Univ
a Integer
b
    PiSort Dom' Term Term
a Sort
b Abs Sort
c -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4  forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
b Abs Sort
c
    FunSort Sort
a Sort
b  -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5  forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
a Sort
b
    UnivSort Sort
a   -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6  forall t. Sort' t -> Sort' t
UnivSort Sort
a
    DefS QName
a Elims
b     -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7  forall t. QName -> [Elim' t] -> Sort' t
DefS QName
a Elims
b
    Sort
LockUniv     -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
9  forall t. Sort' t
LockUniv
    Sort
IntervalUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
10 forall t. Sort' t
IntervalUniv
    MetaS MetaId
a Elims
b    -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
11 forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
a Elims
b
    DummyS ArgName
s     -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
12 forall t. ArgName -> Sort' t
DummyS ArgName
s
    Sort
LevelUniv    -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
13 forall t. Sort' t
LevelUniv

  value :: Int32 -> R Sort
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {t}.
(EmbPrj t, EmbPrj (Dom' t t), EmbPrj (Level' t),
 EmbPrj (Sort' t)) =>
[Int32] -> R (Sort' t)
valu where
    valu :: [Int32] -> R (Sort' t)
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Univ -> Level' t -> Sort' t
Univ Int32
a Int32
b
    valu [Int32
2]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
SizeUniv
    valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Univ -> Integer -> Sort' t
Inf Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Int32
a Int32
b Int32
c
    valu [Int32
5, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t -> Sort' t -> Sort' t
FunSort Int32
a Int32
b
    valu [Int32
6, Int32
a]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t -> Sort' t
UnivSort Int32
a
    valu [Int32
7, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. QName -> [Elim' t] -> Sort' t
DefS Int32
a Int32
b
    valu [Int32
9]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
LockUniv
    valu [Int32
10]      = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
IntervalUniv
    valu [Int32
11, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. MetaId -> [Elim' t] -> Sort' t
MetaS Int32
a Int32
b
    valu [Int32
12, Int32
s]   = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. ArgName -> Sort' t
DummyS Int32
s
    valu [Int32
13]      = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
LevelUniv
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj DisplayForm where
  icod_ :: DisplayForm -> S Int32
icod_ (Display Int
a Elims
b DisplayTerm
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
a Elims
b DisplayTerm
c

  value :: Int32 -> R DisplayForm
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> Elims -> DisplayTerm -> DisplayForm
Display

instance EmbPrj a => EmbPrj (Open a) where
  icod_ :: Open a -> S Int32
icod_ (OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d

  value :: Int32 -> R (Open a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing

instance EmbPrj CheckpointId where
  icod_ :: CheckpointId -> S Int32
icod_ (CheckpointId Int
a) = forall a. EmbPrj a => a -> S Int32
icode Int
a
  value :: Int32 -> R CheckpointId
value Int32
n                = Int -> CheckpointId
CheckpointId forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj DisplayTerm where
  icod_ :: DisplayTerm -> S Int32
icod_ (DTerm'   Term
a Elims
b)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Term -> Elims -> DisplayTerm
DTerm' Term
a Elims
b
  icod_ (DDot'    Term
a Elims
b)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Term -> Elims -> DisplayTerm
DDot' Term
a Elims
b
  icod_ (DCon     ConHead
a ConInfo
b [Arg DisplayTerm]
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
a ConInfo
b [Arg DisplayTerm]
c
  icod_ (DDef     QName
a [Elim' DisplayTerm]
b)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
a [Elim' DisplayTerm]
b
  icod_ (DWithApp DisplayTerm
a [DisplayTerm]
b Elims
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
a [DisplayTerm]
b Elims
c

  value :: Int32 -> R DisplayTerm
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R DisplayTerm
valu where
    valu :: [Int32] -> R DisplayTerm
valu [Int32
a, Int32
b]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Elims -> DisplayTerm
DTerm' Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Elims -> DisplayTerm
DDot' Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon Int32
a Int32
b Int32
c
    valu [Int32
3, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp Int32
a Int32
b Int32
c
    valu [Int32]
_            = forall a. R a
malformed

instance EmbPrj MutualId where
  icod_ :: MutualId -> S Int32
icod_ (MutId Int32
a) = forall a. EmbPrj a => a -> S Int32
icode Int32
a
  value :: Int32 -> R MutualId
value Int32
n         = Int32 -> MutualId
MutId forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj CompKit where
  icod_ :: CompKit -> S Int32
icod_ (CompKit Maybe QName
a Maybe QName
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe QName -> Maybe QName -> CompKit
CompKit Maybe QName
a Maybe QName
b
  value :: Int32 -> R CompKit
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe QName -> Maybe QName -> CompKit
CompKit

instance EmbPrj Definition where
  icod_ :: Definition -> S Int32
icod_ (Defn ArgInfo
a QName
b Type
c [Polarity]
d [Occurrence]
e NumGeneralizableArgs
f [Maybe Name]
g [LocalDisplayForm]
h MutualId
i CompiledRepresentation
j Maybe QName
k Bool
l Set QName
m Bool
n Bool
o Bool
p Blocked_
q Language
r Defn
s) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn ArgInfo
a QName
b (forall a. KillRange a => KillRangeT a
P.killRange Type
c) [Polarity]
d [Occurrence]
e NumGeneralizableArgs
f [Maybe Name]
g [LocalDisplayForm]
h MutualId
i CompiledRepresentation
j Maybe QName
k Bool
l Set QName
m Bool
n Bool
o Bool
p Blocked_
q Language
r Defn
s

  value :: Int32 -> R Definition
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn

instance EmbPrj NotBlocked where
  icod_ :: NotBlocked -> S Int32
icod_ NotBlocked
ReallyNotBlocked = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t. NotBlocked' t
ReallyNotBlocked
  icod_ (StuckOn Elim' Term
a)      = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall t. Elim' t -> NotBlocked' t
StuckOn Elim' Term
a
  icod_ NotBlocked
Underapplied     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall t. NotBlocked' t
Underapplied
  icod_ NotBlocked
AbsurdMatch      = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall t. NotBlocked' t
AbsurdMatch
  icod_ (MissingClauses QName
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 forall t. QName -> NotBlocked' t
MissingClauses QName
a

  value :: Int32 -> R NotBlocked
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {t}. EmbPrj t => [Int32] -> StateT St IO (NotBlocked' t)
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
valu []     = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. NotBlocked' t
ReallyNotBlocked
    valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Elim' t -> NotBlocked' t
StuckOn Int32
a
    valu [Int32
1]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. NotBlocked' t
Underapplied
    valu [Int32
2]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. NotBlocked' t
AbsurdMatch
    valu [Int32
3, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. QName -> NotBlocked' t
MissingClauses Int32
a
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj Blocked_ where
  icod_ :: Blocked_ -> S Int32
icod_ (NotBlocked NotBlocked
a ()
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
a ()
b
  icod_ Blocked{} = forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R Blocked_
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked

instance EmbPrj NLPat where
  icod_ :: NLPat -> S Int32
icod_ (PVar Int
a [Arg Int]
b)      = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Int -> [Arg Int] -> NLPat
PVar Int
a [Arg Int]
b
  icod_ (PDef QName
a PElims
b)      = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 QName -> PElims -> NLPat
PDef QName
a PElims
b
  icod_ (PLam ArgInfo
a Abs NLPat
b)      = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
a Abs NLPat
b
  icod_ (PPi Dom NLPType
a Abs NLPType
b)       = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
a Abs NLPType
b
  icod_ (PSort NLPSort
a)       = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 NLPSort -> NLPat
PSort NLPSort
a
  icod_ (PBoundVar Int
a PElims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 Int -> PElims -> NLPat
PBoundVar Int
a PElims
b
  icod_ (PTerm Term
a)       = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 Term -> NLPat
PTerm Term
a

  value :: Int32 -> R NLPat
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NLPat
valu where
    valu :: [Int32] -> R NLPat
valu [Int32
0, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> [Arg Int] -> NLPat
PVar Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> PElims -> NLPat
PDef Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgInfo -> Abs NLPat -> NLPat
PLam Int32
a Int32
b
    valu [Int32
3, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom NLPType -> Abs NLPType -> NLPat
PPi Int32
a Int32
b
    valu [Int32
4, Int32
a]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort -> NLPat
PSort Int32
a
    valu [Int32
5, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> PElims -> NLPat
PBoundVar Int32
a Int32
b
    valu [Int32
6, Int32
a]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> NLPat
PTerm Int32
a
    valu [Int32]
_            = forall a. R a
malformed

instance EmbPrj NLPType where
  icod_ :: NLPType -> S Int32
icod_ (NLPType NLPSort
a NLPat
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NLPSort -> NLPat -> NLPType
NLPType NLPSort
a NLPat
b

  value :: Int32 -> R NLPType
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN NLPSort -> NLPat -> NLPType
NLPType

instance EmbPrj NLPSort where
  icod_ :: NLPSort -> S Int32
icod_ (PType NLPat
a)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 NLPat -> NLPSort
PType NLPat
a
  icod_ (PProp NLPat
a)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 NLPat -> NLPSort
PProp NLPat
a
  icod_ (PInf Univ
f Integer
a)  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Univ -> Integer -> NLPSort
PInf Univ
f Integer
a
  icod_ NLPSort
PSizeUniv   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 NLPSort
PSizeUniv
  icod_ NLPSort
PLockUniv   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 NLPSort
PLockUniv
  icod_ NLPSort
PIntervalUniv = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 NLPSort
PIntervalUniv
  icod_ (PSSet NLPat
a)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 NLPat -> NLPSort
PSSet NLPat
a
  icod_ NLPSort
PLevelUniv = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 NLPSort
PLevelUniv

  value :: Int32 -> R NLPSort
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NLPSort
valu where
    valu :: [Int32] -> R NLPSort
valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PType Int32
a
    valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PProp Int32
a
    valu [Int32
2, Int32
f, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Univ -> Integer -> NLPSort
PInf Int32
f Int32
a
    valu [Int32
3]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PSizeUniv
    valu [Int32
4]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PLockUniv
    valu [Int32
5]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PIntervalUniv
    valu [Int32
6, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PSSet Int32
a
    valu [Int32
7]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PLevelUniv
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj RewriteRule where
  icod_ :: RewriteRule -> S Int32
icod_ (RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f Bool
g) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f Bool
g

  value :: Int32 -> R RewriteRule
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule

instance EmbPrj Projection where
  icod_ :: Projection -> S Int32
icod_ (Projection Maybe QName
a QName
b Arg QName
c Int
d ProjLams
e) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection Maybe QName
a QName
b Arg QName
c Int
d ProjLams
e

  value :: Int32 -> R Projection
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection

instance EmbPrj ProjLams where
  icod_ :: ProjLams -> S Int32
icod_ (ProjLams [Arg ArgName]
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> ProjLams
ProjLams [Arg ArgName]
a

  value :: Int32 -> R ProjLams
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN [Arg ArgName] -> ProjLams
ProjLams

instance EmbPrj System where
  icod_ :: System -> S Int32
icod_ (System Telescope
a [(Face, Term)]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Telescope -> [(Face, Term)] -> System
System Telescope
a [(Face, Term)]
b

  value :: Int32 -> R System
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Telescope -> [(Face, Term)] -> System
System

instance EmbPrj ExtLamInfo where
  icod_ :: ExtLamInfo -> S Int32
icod_ (ExtLamInfo ModuleName
a Bool
b Maybe System
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
a Bool
b Maybe System
c

  value :: Int32 -> R ExtLamInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo

instance EmbPrj Polarity where
  icod_ :: Polarity -> S Int32
icod_ Polarity
Covariant     = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ Polarity
Contravariant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
  icod_ Polarity
Invariant     = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
  icod_ Polarity
Nonvariant    = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3

  value :: Int32 -> R Polarity
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Covariant
  value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Contravariant
  value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant
  value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Nonvariant
  value Int32
_ = forall a. R a
malformed

instance EmbPrj IsForced where
  icod_ :: IsForced -> S Int32
icod_ IsForced
Forced    = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ IsForced
NotForced = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1

  value :: Int32 -> R IsForced
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return IsForced
Forced
  value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return IsForced
NotForced
  value Int32
_ = forall a. R a
malformed

instance EmbPrj NumGeneralizableArgs where
  icod_ :: NumGeneralizableArgs -> S Int32
icod_ NumGeneralizableArgs
NoGeneralizableArgs       = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NumGeneralizableArgs
NoGeneralizableArgs
  icod_ (SomeGeneralizableArgs Int
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> NumGeneralizableArgs
SomeGeneralizableArgs Int
a

  value :: Int32 -> R NumGeneralizableArgs
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NumGeneralizableArgs
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains NumGeneralizableArgs))
     (R (CoDomain NumGeneralizableArgs))
valu []  = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NumGeneralizableArgs
NoGeneralizableArgs
    valu [Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> NumGeneralizableArgs
SomeGeneralizableArgs Int32
a
    valu [Int32]
_   = forall a. R a
malformed

instance EmbPrj DoGeneralize where
  icod_ :: DoGeneralize -> S Int32
icod_ DoGeneralize
YesGeneralizeVar  = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ DoGeneralize
YesGeneralizeMeta = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
  icod_ DoGeneralize
NoGeneralize      = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2

  value :: Int32 -> R DoGeneralize
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
YesGeneralizeVar
  value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
YesGeneralizeMeta
  value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
NoGeneralize
  value Int32
_ = forall a. R a
malformed

instance EmbPrj Occurrence where
  icod_ :: Occurrence -> S Int32
icod_ Occurrence
StrictPos = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ Occurrence
Mixed     = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
  icod_ Occurrence
Unused    = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
  icod_ Occurrence
GuardPos  = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
  icod_ Occurrence
JustPos   = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
4
  icod_ Occurrence
JustNeg   = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
5

  value :: Int32 -> R Occurrence
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
StrictPos
  value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Mixed
  value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Unused
  value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
GuardPos
  value Int32
4 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
JustPos
  value Int32
5 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
JustNeg
  value Int32
_ = forall a. R a
malformed

instance EmbPrj EtaEquality where
  icod_ :: EtaEquality -> S Int32
icod_ (Specified HasEta
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 HasEta -> EtaEquality
Specified HasEta
a
  icod_ (Inferred HasEta
a)  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 HasEta -> EtaEquality
Inferred HasEta
a

  value :: Int32 -> R EtaEquality
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R EtaEquality
valu where
    valu :: [Int32] -> R EtaEquality
valu [Int32
0,Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN HasEta -> EtaEquality
Specified Int32
a
    valu [Int32
1,Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN HasEta -> EtaEquality
Inferred Int32
a
    valu [Int32]
_     = forall a. R a
malformed

instance EmbPrj ProjectionLikenessMissing

instance EmbPrj BuiltinSort where
  icod_ :: BuiltinSort -> S Int32
icod_ = \case
    SortUniv  Univ
a      -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Univ -> BuiltinSort
SortUniv  Univ
a
    SortOmega Univ
a      -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Univ -> BuiltinSort
SortOmega Univ
a
    BuiltinSort
SortIntervalUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 BuiltinSort
SortIntervalUniv
    BuiltinSort
SortLevelUniv    -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 BuiltinSort
SortLevelUniv

  value :: Int32 -> R BuiltinSort
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase \case
    [Int32
0, Int32
a] -> forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Univ -> BuiltinSort
SortUniv  Int32
a
    [Int32
1, Int32
a] -> forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Univ -> BuiltinSort
SortOmega Int32
a
    [Int32
2]    -> forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN BuiltinSort
SortIntervalUniv
    [Int32
3]    -> forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN BuiltinSort
SortLevelUniv
    [Int32]
_ -> forall a. R a
malformed

instance EmbPrj Defn where
  icod_ :: Defn -> S Int32
icod_ (Axiom       Bool
a)                                 = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Bool -> Defn
Axiom Bool
a
  icod_ (Function    [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t [Clause]
u FunctionInverse
c Maybe [QName]
d IsAbstract
e Either ProjectionLikenessMissing Projection
f Bool
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l IsOpaque
m)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 (\ [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Either ProjectionLikenessMissing Projection
-> Bool
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> IsOpaque
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t) [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s [Clause]
u FunctionInverse
c Maybe [QName]
d IsAbstract
e Either ProjectionLikenessMissing Projection
f Bool
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l IsOpaque
m
  icod_ (Datatype    Int
a Int
b Maybe Clause
c [QName]
d Sort
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j)               = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j
  icod_ (Record      Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m)         = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> Maybe Bool
-> IsAbstract
-> CompKit
-> Defn
Record Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m
  icod_ (Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e CompKit
f Maybe [QName]
g [IsForced]
h Maybe [Bool]
i Bool
j Bool
k)             = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Bool
-> Bool
-> Defn
Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e CompKit
f Maybe [QName]
g [IsForced]
h Maybe [Bool]
i Bool
j Bool
k
  icod_ (Primitive   IsAbstract
a PrimitiveId
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e IsOpaque
f)                       = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 IsAbstract
-> PrimitiveId
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> IsOpaque
-> Defn
Primitive IsAbstract
a PrimitiveId
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e IsOpaque
f
  icod_ (PrimitiveSort BuiltinSort
a Sort
b)                             = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 BuiltinSort -> Sort -> Defn
PrimitiveSort BuiltinSort
a Sort
b
  icod_ AbstractDefn{}                                  = forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ Defn
GeneralizableVar                                = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 Defn
GeneralizableVar
  icod_ DataOrRecSig{}                                  = forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R Defn
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R Defn
valu where
    valu :: [Int32] -> R Defn
valu [Int32
0, Int32
a]                                        = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Bool -> Defn
Axiom Int32
a
    valu [Int32
1, Int32
a, Int32
b, Int32
s, Int32
u, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l, Int32
m]
                                                       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN (\ [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Either ProjectionLikenessMissing Projection
-> Bool
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> IsOpaque
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s forall a. Maybe a
Nothing) Int32
a Int32
b Int32
s Int32
u Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l Int32
m
    valu [Int32
2, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j]             = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j
    valu [Int32
3, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l, Int32
m]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> Maybe Bool
-> IsAbstract
-> CompKit
-> Defn
Record   Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l Int32
m
    valu [Int32
4, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k]          = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Bool
-> Bool
-> Defn
Constructor Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k
    valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f]                         = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
-> PrimitiveId
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> IsOpaque
-> Defn
Primitive   Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f
    valu [Int32
6, Int32
a, Int32
b]                                     = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN BuiltinSort -> Sort -> Defn
PrimitiveSort Int32
a Int32
b
    valu [Int32
7]                                           = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Defn
GeneralizableVar
    valu [Int32]
_                                             = forall a. R a
malformed

instance EmbPrj LazySplit where
  icod_ :: LazySplit -> S Int32
icod_ LazySplit
StrictSplit = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' LazySplit
StrictSplit
  icod_ LazySplit
LazySplit   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 LazySplit
LazySplit

  value :: Int32 -> R LazySplit
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R LazySplit
valu where
    valu :: [a]
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
valu []  = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN LazySplit
StrictSplit
    valu [a
0] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN LazySplit
LazySplit
    valu [a]
_   = forall a. R a
malformed

instance EmbPrj SplitTag where
  icod_ :: SplitTag -> S Int32
icod_ (SplitCon QName
c)  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 QName -> SplitTag
SplitCon QName
c
  icod_ (SplitLit Literal
l)  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Literal -> SplitTag
SplitLit Literal
l
  icod_ SplitTag
SplitCatchall = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' SplitTag
SplitCatchall

  value :: Int32 -> R SplitTag
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R SplitTag
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains SplitTag)) (R (CoDomain SplitTag))
valu []     = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN SplitTag
SplitCatchall
    valu [Int32
0, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> SplitTag
SplitCon Int32
c
    valu [Int32
1, Int32
l] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Literal -> SplitTag
SplitLit Int32
l
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj a => EmbPrj (SplitTree' a) where
  icod_ :: SplitTree' a -> S Int32
icod_ (SplittingDone Int
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Int -> SplitTree' a
SplittingDone Int
a
  icod_ (SplitAt Arg Int
a LazySplit
b SplitTrees' a
c)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
a LazySplit
b SplitTrees' a
c

  value :: Int32 -> R (SplitTree' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (SplitTree' a)
valu where
    valu :: [Int32] -> R (SplitTree' a)
valu [Int32
a]          = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Int -> SplitTree' a
SplittingDone Int32
a
    valu [Int32
0, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Int32
a Int32
b Int32
c
    valu [Int32]
_            = forall a. R a
malformed

instance EmbPrj FunctionFlag where
  icod_ :: FunctionFlag -> S Int32
icod_ FunctionFlag
FunStatic       = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
0
  icod_ FunctionFlag
FunInline       = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
1
  icod_ FunctionFlag
FunMacro        = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
2

  value :: Int32 -> R FunctionFlag
value = \case
    Int32
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunStatic
    Int32
1 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunInline
    Int32
2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunMacro
    Int32
_ -> forall a. R a
malformed

instance EmbPrj a => EmbPrj (WithArity a) where
  icod_ :: WithArity a -> S Int32
icod_ (WithArity Int
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c. Int -> c -> WithArity c
WithArity Int
a a
b

  value :: Int32 -> R (WithArity a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall c. Int -> c -> WithArity c
WithArity

instance EmbPrj a => EmbPrj (Case a) where
  icod_ :: Case a -> S Int32
icod_ (Branches Bool
a Map QName (WithArity a)
b Maybe (ConHead, WithArity a)
c Map Literal a
d Maybe a
e Maybe Bool
f Bool
g) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
a Map QName (WithArity a)
b Maybe (ConHead, WithArity a)
c Map Literal a
d Maybe a
e Maybe Bool
f Bool
g

  value :: Int32 -> R (Case a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches

-- Opaque blocks are serialised in an abbreviated manner: We only need
-- the enclosed definitions (3rd argument) and parent (4th argument) to
-- compute the transitive closure during scope checking, never
-- afterwards.
instance EmbPrj OpaqueBlock where
  icod_ :: OpaqueBlock -> S Int32
icod_ (OpaqueBlock OpaqueId
id HashSet QName
uf HashSet QName
_ Maybe OpaqueId
_ Range
r) =
    forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\OpaqueId
id [QName]
uf ->
      let !unfolding :: HashSet QName
unfolding = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList [QName]
uf
      in OpaqueId
-> HashSet QName
-> HashSet QName
-> Maybe OpaqueId
-> Range
-> OpaqueBlock
OpaqueBlock OpaqueId
id HashSet QName
unfolding forall a. Monoid a => a
mempty forall a. Maybe a
Nothing)
    OpaqueId
id (forall a. HashSet a -> [a]
HashSet.toList HashSet QName
uf) Range
r

  value :: Int32 -> R OpaqueBlock
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (\OpaqueId
id [QName]
uf -> let !unfolding :: HashSet QName
unfolding = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList [QName]
uf
                            in OpaqueId
-> HashSet QName
-> HashSet QName
-> Maybe OpaqueId
-> Range
-> OpaqueBlock
OpaqueBlock OpaqueId
id HashSet QName
unfolding forall a. Monoid a => a
mempty forall a. Maybe a
Nothing)

instance EmbPrj CompiledClauses where
  icod_ :: CompiledClauses -> S Int32
icod_ (Fail [Arg ArgName]
a)   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. [Arg ArgName] -> CompiledClauses' a
Fail [Arg ArgName]
a
  icod_ (Done [Arg ArgName]
a Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [Arg ArgName]
a (forall a. KillRange a => KillRangeT a
P.killRange Term
b)
  icod_ (Case Arg Int
a Case CompiledClauses
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
a Case CompiledClauses
b

  value :: Int32 -> R CompiledClauses
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}.
(EmbPrj a, EmbPrj (CompiledClauses' a)) =>
[Int32] -> R (CompiledClauses' a)
valu where
    valu :: [Int32] -> R (CompiledClauses' a)
valu [Int32
a]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. [Arg ArgName] -> CompiledClauses' a
Fail Int32
a
    valu [Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Int32
a Int32
b
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj a => EmbPrj (FunctionInverse' a) where
  icod_ :: FunctionInverse' a -> S Int32
icod_ FunctionInverse' a
NotInjective = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c. FunctionInverse' c
NotInjective
  icod_ (Inverse InversionMap a
a)  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c. InversionMap c -> FunctionInverse' c
Inverse InversionMap a
a

  value :: Int32 -> R (FunctionInverse' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {c}.
EmbPrj [c] =>
[Int32] -> StateT St IO (FunctionInverse' c)
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains (FunctionInverse' c)))
     (R (CoDomain (FunctionInverse' c)))
valu []  = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall c. FunctionInverse' c
NotInjective
    valu [Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall c. InversionMap c -> FunctionInverse' c
Inverse Int32
a
    valu [Int32]
_   = forall a. R a
malformed

instance EmbPrj TermHead where
  icod_ :: TermHead -> S Int32
icod_ TermHead
SortHead     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' TermHead
SortHead
  icod_ TermHead
PiHead       = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 TermHead
PiHead
  icod_ (ConsHead QName
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 QName -> TermHead
ConsHead QName
a
  icod_ (VarHead Int
a)  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Int -> TermHead
VarHead Int
a
  icod_ TermHead
UnknownHead  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 TermHead
UnknownHead

  value :: Int32 -> R TermHead
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R TermHead
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
valu []     = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
SortHead
    valu [Int32
1]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
PiHead
    valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> TermHead
ConsHead Int32
a
    valu [Int32
3, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> TermHead
VarHead Int32
a
    valu [Int32
4]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
UnknownHead
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj I.Clause where
  icod_ :: Clause -> S Int32
icod_ (Clause Range
a Range
b Telescope
c NAPs
d Maybe Term
e Maybe (Arg Type)
f Bool
g Maybe Bool
h Maybe Bool
i Maybe Bool
j ExpandedEllipsis
k Maybe ModuleName
l) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
a Range
b Telescope
c NAPs
d Maybe Term
e Maybe (Arg Type)
f Bool
g Maybe Bool
h Maybe Bool
i Maybe Bool
j ExpandedEllipsis
k Maybe ModuleName
l

  value :: Int32 -> R Clause
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause

instance EmbPrj I.ConPatternInfo where
  icod_ :: ConPatternInfo -> S Int32
icod_ (ConPatternInfo PatternInfo
a Bool
b Bool
c Maybe (Arg Type)
d Bool
e) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
a Bool
b Bool
c Maybe (Arg Type)
d Bool
e

  value :: Int32 -> R ConPatternInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo

instance EmbPrj I.DBPatVar where
  icod_ :: DBPatVar -> S Int32
icod_ (DBPatVar ArgName
a Int
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgName -> Int -> DBPatVar
DBPatVar ArgName
a Int
b

  value :: Int32 -> R DBPatVar
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ArgName -> Int -> DBPatVar
DBPatVar

instance EmbPrj I.PatternInfo where
  icod_ :: PatternInfo -> S Int32
icod_ (PatternInfo PatOrigin
a [Name]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
a [Name]
b

  value :: Int32 -> R PatternInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN PatOrigin -> [Name] -> PatternInfo
PatternInfo

instance EmbPrj I.PatOrigin where
  icod_ :: PatOrigin -> S Int32
icod_ PatOrigin
PatOSystem  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatOrigin
PatOSystem
  icod_ PatOrigin
PatOSplit   = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 PatOrigin
PatOSplit
  icod_ (PatOVar Name
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Name -> PatOrigin
PatOVar Name
a
  icod_ PatOrigin
PatODot     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 PatOrigin
PatODot
  icod_ PatOrigin
PatOWild    = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 PatOrigin
PatOWild
  icod_ PatOrigin
PatOCon     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 PatOrigin
PatOCon
  icod_ PatOrigin
PatORec     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 PatOrigin
PatORec
  icod_ PatOrigin
PatOLit     = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 PatOrigin
PatOLit
  icod_ PatOrigin
PatOAbsurd  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
8 PatOrigin
PatOAbsurd

  value :: Int32 -> R PatOrigin
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R PatOrigin
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
valu []     = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOSystem
    valu [Int32
1]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOSplit
    valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Name -> PatOrigin
PatOVar Int32
a
    valu [Int32
3]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatODot
    valu [Int32
4]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOWild
    valu [Int32
5]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOCon
    valu [Int32
6]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatORec
    valu [Int32
7]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOLit
    valu [Int32
8]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOAbsurd
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj a => EmbPrj (I.Pattern' a) where
  icod_ :: Pattern' a -> S Int32
icod_ (VarP PatternInfo
a a
b  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
a a
b
  icod_ (ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c
  icod_ (LitP PatternInfo
a Literal
b  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
a Literal
b
  icod_ (DotP PatternInfo
a Term
b  ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
a Term
b
  icod_ (ProjP ProjOrigin
a QName
b ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
a QName
b
  icod_ (IApplyP PatternInfo
a Term
b Term
c a
d) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
a Term
b Term
c a
d
  icod_ (DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c

  value :: Int32 -> R (Pattern' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {x}. EmbPrj x => [Int32] -> R (Pattern' x)
valu where
    valu :: [Int32] -> R (Pattern' x)
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> x -> Pattern' x
VarP Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP Int32
a Int32
b Int32
c
    valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> Literal -> Pattern' x
LitP Int32
a Int32
b
    valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> Term -> Pattern' x
DotP Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. ProjOrigin -> QName -> Pattern' x
ProjP Int32
a Int32
b
    valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP Int32
a Int32
b Int32
c Int32
d
    valu [Int32
6, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP Int32
a Int32
b Int32
c
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj a => EmbPrj (Builtin a) where
  icod_ :: Builtin a -> S Int32
icod_ (Prim    a
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall pf. pf -> Builtin pf
Prim a
a
  icod_ (Builtin Term
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall pf. Term -> Builtin pf
Builtin Term
a
  icod_ (BuiltinRewriteRelations Set QName
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
a

  value :: Int32 -> R (Builtin a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {pf}. EmbPrj pf => [Int32] -> R (Builtin pf)
valu where
    valu :: [Int32] -> R (Builtin pf)
valu [Int32
a]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall pf. pf -> Builtin pf
Prim    Int32
a
    valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall pf. Term -> Builtin pf
Builtin Int32
a
    valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Int32
a
    valu [Int32]
_      = forall a. R a
malformed

instance EmbPrj a => EmbPrj (Substitution' a) where
  icod_ :: Substitution' a -> S Int32
icod_ Substitution' a
IdS                = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Substitution' a
IdS
  icod_ (EmptyS Impossible
a)         = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Impossible -> Substitution' a
EmptyS Impossible
a
  icod_ (a
a :# Substitution' a
b)           = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Substitution' a -> Substitution' a
(:#) a
a Substitution' a
b
  icod_ (Strengthen Impossible
a Int
b Substitution' a
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
a Int
b Substitution' a
c
  icod_ (Wk Int
a Substitution' a
b)           = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall a. Int -> Substitution' a -> Substitution' a
Wk Int
a Substitution' a
b
  icod_ (Lift Int
a Substitution' a
b)         = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall a. Int -> Substitution' a -> Substitution' a
Lift Int
a Substitution' a
b

  value :: Int32 -> R (Substitution' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> StateT St IO (Substitution' a)
valu where
    valu :: [Int32]
-> Arrows
     (Constant Int32 (Domains (Substitution' a)))
     (R (CoDomain (Substitution' a)))
valu []           = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Substitution' a
IdS
    valu [Int32
a]          = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Impossible -> Substitution' a
EmptyS Int32
a
    valu [Int32
a, Int32
b]       = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Substitution' a -> Substitution' a
(:#) Int32
a Int32
b
    valu [Int32
0, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Int32
a Int32
b Int32
c
    valu [Int32
1, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Int -> Substitution' a -> Substitution' a
Wk Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Int -> Substitution' a -> Substitution' a
Lift Int32
a Int32
b
    valu [Int32]
_            = forall a. R a
malformed

instance EmbPrj Instantiation where
  icod_ :: Instantiation -> S Int32
icod_ (Instantiation [Arg ArgName]
a Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> Term -> Instantiation
Instantiation [Arg ArgName]
a Term
b
  value :: Int32 -> R Instantiation
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN [Arg ArgName] -> Term -> Instantiation
Instantiation

instance EmbPrj Comparison where
  icod_ :: Comparison -> S Int32
icod_ Comparison
CmpEq  = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Comparison
CmpEq
  icod_ Comparison
CmpLeq = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Comparison
CmpLeq

  value :: Int32 -> R Comparison
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R Comparison
valu
    where
    valu :: [a]
-> Arrows
     (Constant Int32 (Domains Comparison)) (R (CoDomain Comparison))
valu []  = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Comparison
CmpEq
    valu [a
0] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Comparison
CmpLeq
    valu [a]
_   = forall a. R a
malformed

instance EmbPrj a => EmbPrj (Judgement a) where
  icod_ :: Judgement a -> S Int32
icod_ (HasType a
a Comparison
b Type
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Comparison -> Type -> Judgement a
HasType a
a Comparison
b Type
c
  icod_ (IsSort a
a Type
b)    = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Type -> Judgement a
IsSort a
a Type
b

  value :: Int32 -> R (Judgement a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (Judgement a)
valu
    where
    valu :: [Int32] -> R (Judgement a)
valu [Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Comparison -> Type -> Judgement a
HasType Int32
a Int32
b Int32
c
    valu [Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Type -> Judgement a
IsSort Int32
a Int32
b
    valu [Int32]
_         = forall a. R a
malformed

instance EmbPrj RemoteMetaVariable where
  icod_ :: RemoteMetaVariable -> S Int32
icod_ (RemoteMetaVariable Instantiation
a Modality
b Judgement MetaId
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
RemoteMetaVariable Instantiation
a Modality
b Judgement MetaId
c
  value :: Int32 -> R RemoteMetaVariable
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
RemoteMetaVariable