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

module Agda.TypeChecking.Serialise.Instances.Internal where

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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}.
EmbPrj a =>
Node -> ExceptT TypeError (StateT St IO) (Tele a)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele a)))
valu []     = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_      = 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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => Node -> R (Elim' a)
valu where
    valu :: Node -> R (Elim' a)
valu [Int32
a]       = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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 Node
_         = forall a. R a
malformed

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

  value :: Int32 -> R DataOrRecord
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
    []   -> forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN DataOrRecord
IsData
    [Int32
pm] -> forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternOrCopattern -> DataOrRecord
IsRecord Int32
pm
    Node
_    -> 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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => Node -> R (Abs a)
valu where
    valu :: Node -> R (Abs a)
valu [Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_         = forall a. R a
malformed

instance EmbPrj I.Term where
  icod_ :: Term -> S Int32
icod_ (Var     Int
a []) = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R Term
valu where
    valu :: Node -> R Term
valu [Int32
a]       = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_         = 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), Currying (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), Currying (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 I.Sort where
  icod_ :: Sort -> S Int32
icod_ (Type  Level
a  ) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall t. Level' t -> Sort' t
Type Level
a
  icod_ (Prop  Level
a  ) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall t. Level' t -> Sort' t
Prop Level
a
  icod_ Sort
SizeUniv    = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall t. Sort' t
SizeUniv
  icod_ (Inf IsFibrant
f Integer
a)   = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
a
  icod_ (PiSort Dom' Term Term
a Sort
b Abs Sort
c) = forall t.
(ICODE t (IsBase t), Currying (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
  icod_ (FunSort Sort
a Sort
b) = forall t.
(ICODE t (IsBase t), Currying (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
  icod_ (UnivSort Sort
a) = forall t.
(ICODE t (IsBase t), Currying (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
  icod_ (DefS QName
a Elims
b)   = forall t.
(ICODE t (IsBase t), Currying (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
  icod_ (SSet  Level
a  ) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
8 forall t. Level' t -> Sort' t
SSet Level
a
  icod_ Sort
LockUniv    = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
9 forall t. Sort' t
LockUniv
  icod_ Sort
IntervalUniv = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
10 forall t. Sort' t
IntervalUniv
  icod_ (MetaS MetaId
a Elims
b)  = forall t.
(ICODE t (IsBase t), Currying (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
  icod_ (DummyS ArgName
s)   = forall t.
(ICODE t (IsBase t), Currying (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

  value :: Int32 -> R Sort
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {t}.
(EmbPrj t, EmbPrj (Dom' t t), EmbPrj (Level' t),
 EmbPrj (Sort' t)) =>
Node -> R (Sort' t)
valu where
    valu :: Node -> R (Sort' t)
valu [Int32
0, Int32
a]    = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Level' t -> Sort' t
Type  Int32
a
    valu [Int32
1, Int32
a]    = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Level' t -> Sort' t
Prop  Int32
a
    valu [Int32
2]       = forall t.
(VALU t (IsBase t),
 Currying (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
f, Int32
a] = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. IsFibrant -> Integer -> Sort' t
Inf Int32
f Int32
a
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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
8, Int32
a]    = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Level' t -> Sort' t
SSet Int32
a
    valu [Int32
9]       = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_         = 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), Currying (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), Currying (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj DisplayTerm where
  icod_ :: DisplayTerm -> S Int32
icod_ (DTerm    Term
a  )   = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Term -> DisplayTerm
DTerm Term
a
  icod_ (DDot     Term
a  )   = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Term -> DisplayTerm
DDot Term
a
  icod_ (DCon     ConHead
a ConInfo
b [Arg DisplayTerm]
c) = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R DisplayTerm
valu where
    valu :: Node -> R DisplayTerm
valu [Int32
a]          = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> DisplayTerm
DTerm Int32
a
    valu [Int32
1, Int32
a]       = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> DisplayTerm
DDot Int32
a
    valu [Int32
2, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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 Node
_            = 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {t}.
EmbPrj t =>
Node -> ExceptT TypeError (StateT St IO) (NotBlocked' t)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
valu []     = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_      = forall a. R a
malformed

instance EmbPrj Blocked_ where
  icod_ :: Blocked_ -> S Int32
icod_ (NotBlocked NotBlocked
a ()
b) = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R NLPat
valu where
    valu :: Node -> R NLPat
valu [Int32
0, Int32
a, Int32
b]    = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_            = 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), Currying (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), Currying (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), Currying (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 IsFibrant
f Integer
a)  = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 IsFibrant -> Integer -> NLPSort
PInf IsFibrant
f Integer
a
  icod_ NLPSort
PSizeUniv   = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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), Currying (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), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 NLPat -> NLPSort
PSSet NLPat
a

  value :: Int32 -> R NLPSort
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NLPSort
valu where
    valu :: Node -> R NLPSort
valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsFibrant -> Integer -> NLPSort
PInf Int32
f Int32
a
    valu [Int32
3]    = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_      = 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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R NumGeneralizableArgs
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains NumGeneralizableArgs))
     (R (CoDomain NumGeneralizableArgs))
valu []  = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_   = 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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R EtaEquality
valu where
    valu :: Node -> R EtaEquality
valu [Int32
0,Int32
a] = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_     = forall a. R a
malformed

instance EmbPrj ProjectionLikenessMissing

instance EmbPrj Defn where
  icod_ :: Defn -> S Int32
icod_ (Axiom       Bool
a)                                 = forall t.
(ICODE t (IsBase t), Currying (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 Delayed
f Either ProjectionLikenessMissing Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l)     = forall t.
(ICODE t (IsBase t), Currying (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
-> Delayed
-> Either ProjectionLikenessMissing Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> 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 Delayed
f Either ProjectionLikenessMissing Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l
  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), Currying (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), Currying (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 Induction
f CompKit
g Maybe [QName]
h [IsForced]
i Maybe [Bool]
j)               = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e Induction
f CompKit
g Maybe [QName]
h [IsForced]
i Maybe [Bool]
j
  icod_ (Primitive   IsAbstract
a ArgName
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e)                         = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 IsAbstract
-> ArgName
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive IsAbstract
a ArgName
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e
  icod_ (PrimitiveSort ArgName
a Sort
b)                             = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 ArgName -> Sort -> Defn
PrimitiveSort ArgName
a Sort
b
  icod_ AbstractDefn{}                                  = forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ Defn
GeneralizableVar                                = forall t.
(ICODE t (IsBase t), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R Defn
valu where
    valu :: Node -> R Defn
valu [Int32
0, Int32
a]                                        = forall t.
(VALU t (IsBase t),
 Currying (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] = forall t.
(VALU t (IsBase t),
 Currying (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
-> Delayed
-> Either ProjectionLikenessMissing Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> 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
    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),
 Currying (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),
 Currying (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]             = forall t.
(VALU t (IsBase t),
 Currying (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
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j
    valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e]                            = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
-> ArgName
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive   Int32
a Int32
b Int32
c Int32
d Int32
e
    valu [Int32
6, Int32
a, Int32
b]                                     = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgName -> Sort -> Defn
PrimitiveSort Int32
a Int32
b
    valu [Int32
7]                                           = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Defn
GeneralizableVar
    valu Node
_                                             = forall a. R a
malformed

instance EmbPrj LazySplit where
  icod_ :: LazySplit -> S Int32
icod_ LazySplit
StrictSplit = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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 => (Node -> 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),
 Currying (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),
 Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R SplitTag
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains SplitTag)) (R (CoDomain SplitTag))
valu []     = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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 Node
_      = 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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => Node -> R (SplitTree' a)
valu where
    valu :: Node -> R (SplitTree' a)
valu [Int32
a]          = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_            = forall a. R a
malformed

instance EmbPrj FunctionFlag where
  icod_ :: FunctionFlag -> S Int32
icod_ FunctionFlag
FunStatic       = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 FunctionFlag
FunStatic
  icod_ FunctionFlag
FunInline       = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 FunctionFlag
FunInline
  icod_ FunctionFlag
FunMacro        = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 FunctionFlag
FunMacro

  value :: Int32 -> R FunctionFlag
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R FunctionFlag
valu where
    valu :: [a]
-> Arrows
     (Constant Int32 (Domains FunctionFlag)) (R (CoDomain FunctionFlag))
valu [a
0] = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FunctionFlag
FunStatic
    valu [a
1] = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FunctionFlag
FunInline
    valu [a
2] = forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FunctionFlag
FunMacro
    valu [a]
_   = 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), Currying (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), Currying (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

instance EmbPrj CompiledClauses where
  icod_ :: CompiledClauses -> S Int32
icod_ (Fail [Arg ArgName]
a)   = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}.
(EmbPrj a, EmbPrj (CompiledClauses' a)) =>
Node -> R (CompiledClauses' a)
valu where
    valu :: Node -> R (CompiledClauses' a)
valu [Int32
a]       = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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 Node
_         = 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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {c}.
EmbPrj [c] =>
Node -> ExceptT TypeError (StateT St IO) (FunctionInverse' c)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (FunctionInverse' c)))
     (R (CoDomain (FunctionInverse' c)))
valu []  = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_   = forall a. R a
malformed

instance EmbPrj TermHead where
  icod_ :: TermHead -> S Int32
icod_ TermHead
SortHead     = forall t.
(ICODE t (IsBase t), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R TermHead
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
valu []     = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
UnknownHead
    valu Node
_      = 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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase Node -> R PatOrigin
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
valu []     = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOAbsurd
    valu Node
_      = 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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {x}. EmbPrj x => Node -> R (Pattern' x)
valu where
    valu :: Node -> R (Pattern' x)
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_         = 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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {pf}. EmbPrj pf => Node -> R (Builtin pf)
valu where
    valu :: Node -> R (Builtin pf)
valu [Int32
a]    = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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 Node
_      = 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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}.
EmbPrj a =>
Node -> ExceptT TypeError (StateT St IO) (Substitution' a)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (Substitution' a)))
     (R (CoDomain (Substitution' a)))
valu []           = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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),
 Currying (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 Node
_            = 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), Currying (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), Currying (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), Currying (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 => (Node -> 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),
 Currying (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),
 Currying (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), Currying (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), Currying (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 => (Node -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => Node -> R (Judgement a)
valu
    where
    valu :: Node -> R (Judgement a)
valu [Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
 Currying (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),
 Currying (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 Node
_         = 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), Currying (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