{-# 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 Bool
b Maybe NamedName
c Maybe Term
d a
e) = (ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
-> ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Bool -> Maybe NamedName -> Maybe t -> e -> Dom' t e
Dom ArgInfo
a Bool
b Maybe NamedName
c Maybe Term
d a
e

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

instance EmbPrj Signature where
  icod_ :: Signature -> S Int32
icod_ (Sig Sections
a Definitions
b RewriteRuleMap
c) = (Sections -> Definitions -> RewriteRuleMap -> Signature)
-> Sections -> Definitions -> RewriteRuleMap -> S Int32
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 = (Sections -> Definitions -> RewriteRuleMap -> Signature)
-> Int32
-> R (CoDomain
        (Sections -> Definitions -> RewriteRuleMap -> Signature))
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) = (Telescope -> Section) -> Telescope -> S Int32
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 = (Telescope -> Section)
-> Int32 -> R (CoDomain (Telescope -> Section))
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        = Tele Any -> Arrows (Domains (Tele Any)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Tele Any
forall a. Tele a
EmptyTel
  icod_ (ExtendTel a
a Abs (Tele a)
b) = (a -> Abs (Tele a) -> Tele a) -> a -> Abs (Tele a) -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a Abs (Tele a)
b

  value :: Int32 -> R (Tele a)
value = (Node -> R (Tele a)) -> Int32 -> R (Tele a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Tele a)
forall a. EmbPrj a => Node -> R (Tele a)
valu where
    valu :: Node -> R (Tele a)
valu []     = Tele a
-> Arrows
     (Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele 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 Tele a
forall a. Tele a
EmptyTel
    valu [Int32
a, Int32
b] = (a -> Abs (Tele a) -> Tele a) -> Int32 -> Int32 -> R (Tele 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 a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Int32
a Int32
b
    valu Node
_      = R (Tele a)
forall a. R a
malformed

instance EmbPrj Permutation where
  icod_ :: Permutation -> S Int32
icod_ (Perm Int
a [Int]
b) = (Int -> [Int] -> Permutation) -> Int -> [Int] -> S Int32
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 = (Int -> [Int] -> Permutation)
-> Int32 -> R (CoDomain (Int -> [Int] -> Permutation))
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) = (Int -> a -> Drop a) -> Int -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> a -> Drop a
forall a. Int -> a -> Drop a
Drop Int
a a
b

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

instance EmbPrj a => EmbPrj (Elim' a) where
  icod_ :: Elim' a -> S Int32
icod_ (Apply Arg a
a)      = (Arg a -> Elim' a) -> Arg a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Arg a
a
  icod_ (IApply a
x a
y a
a) = Int32 -> (a -> a -> a -> Elim' a) -> a -> a -> a -> S Int32
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 a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
x a
y a
a
  icod_ (Proj ProjOrigin
a QName
b)     = Int32
-> (ProjOrigin -> QName -> Elim' Any)
-> ProjOrigin
-> QName
-> S Int32
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 ProjOrigin -> QName -> Elim' Any
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
a QName
b

  value :: Int32 -> R (Elim' a)
value = (Node -> R (Elim' a)) -> Int32 -> R (Elim' a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Elim' a)
forall a. EmbPrj a => Node -> R (Elim' a)
valu where
    valu :: Node -> R (Elim' a)
valu [Int32
a]       = (Arg a -> Elim' a) -> Int32 -> R (Elim' 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 Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Int32
a
    valu [Int32
0,Int32
x,Int32
y,Int32
a] = (a -> a -> a -> Elim' a) -> Int32 -> Int32 -> Int32 -> R (Elim' 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 a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply Int32
x Int32
y Int32
a
    valu [Int32
0, Int32
a, Int32
b] = (ProjOrigin -> QName -> Elim' a) -> Int32 -> Int32 -> R (Elim' 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 ProjOrigin -> QName -> Elim' a
forall a. ProjOrigin -> QName -> Elim' a
Proj Int32
a Int32
b
    valu Node
_         = R (Elim' a)
forall a. R a
malformed

instance EmbPrj I.DataOrRecord where
  icod_ :: DataOrRecord -> S Int32
icod_ = \case
    DataOrRecord
IsData      -> DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
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 -> (PatternOrCopattern -> DataOrRecord)
-> PatternOrCopattern -> S Int32
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 = (Node -> R DataOrRecord) -> Int32 -> R DataOrRecord
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Node -> R DataOrRecord) -> Int32 -> R DataOrRecord)
-> (Node -> R DataOrRecord) -> Int32 -> R DataOrRecord
forall a b. (a -> b) -> a -> b
$ \case
    []   -> DataOrRecord
-> Arrows
     (Constant Int32 (Domains DataOrRecord)) (R (CoDomain DataOrRecord))
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] -> (PatternOrCopattern -> DataOrRecord) -> Int32 -> R DataOrRecord
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
_    -> R DataOrRecord
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) = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
-> QName -> DataOrRecord -> Induction -> [Arg QName] -> S Int32
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 = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
-> Int32
-> R (CoDomain
        (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead))
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' Term
a a
b) = (Sort' Term -> a -> Type' a) -> Sort' Term -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Sort' Term -> a -> Type' a
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
a a
b

  value :: Int32 -> R (Type' a)
value = (Sort' Term -> a -> Type' a)
-> Int32 -> R (CoDomain (Sort' Term -> a -> Type' a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Sort' Term -> a -> Type' a
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) = Int32 -> (ArgName -> a -> Abs a) -> ArgName -> a -> S Int32
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 ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
a a
b
  icod_ (Abs ArgName
a a
b)   = (ArgName -> a -> Abs a) -> ArgName -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
a a
b

  value :: Int32 -> R (Abs a)
value = (Node -> R (Abs a)) -> Int32 -> R (Abs a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Abs a)
forall a. EmbPrj a => Node -> R (Abs a)
valu where
    valu :: Node -> R (Abs a)
valu [Int32
a, Int32
b]    = (ArgName -> a -> Abs a) -> Int32 -> Int32 -> R (Abs 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 ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs Int32
a Int32
b
    valu [Int32
0, Int32
a, Int32
b] = (ArgName -> a -> Abs a) -> Int32 -> Int32 -> R (Abs 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 ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs Int32
a Int32
b
    valu Node
_         = R (Abs a)
forall a. R a
malformed

instance EmbPrj I.Term where
  icod_ :: Term -> S Int32
icod_ (Var     Int
a []) = (Int -> Term) -> Int -> S Int32
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 -> [Elim] -> Term
Var Int
a []) Int
a
  icod_ (Var      Int
a [Elim]
b) = Int32 -> (Int -> [Elim] -> Term) -> Int -> [Elim] -> S Int32
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 -> [Elim] -> Term
Var Int
a [Elim]
b
  icod_ (Lam      ArgInfo
a Abs Term
b) = Int32
-> (ArgInfo -> Abs Term -> Term) -> ArgInfo -> Abs Term -> S Int32
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  ) = Int32 -> (Literal -> Term) -> Literal -> S Int32
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 [Elim]
b) = Int32 -> (QName -> [Elim] -> Term) -> QName -> [Elim] -> S Int32
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] -> Term
Def QName
a [Elim]
b
  icod_ (Con    ConHead
a ConInfo
b [Elim]
c) = Int32
-> (ConHead -> ConInfo -> [Elim] -> Term)
-> ConHead
-> ConInfo
-> [Elim]
-> S Int32
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 -> [Elim] -> Term
Con ConHead
a ConInfo
b [Elim]
c
  icod_ (Pi       Dom Type
a Abs Type
b) = Int32
-> (Dom Type -> Abs Type -> Term)
-> Dom Type
-> Abs Type
-> S Int32
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 Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b
  icod_ (Sort     Sort' Term
a  ) = Int32 -> (Sort' Term -> Term) -> Sort' Term -> S Int32
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 -> Term
Sort Sort' Term
a
  icod_ (MetaV    MetaId
a [Elim]
b) = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (DontCare Term
a  ) = Int32 -> (Term -> Term) -> Term -> S Int32
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  ) = Int32 -> (Level -> Term) -> Level -> S Int32
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
s [Elim]
_)    = do
    IO () -> ReaderT Dict IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Dict IO ()) -> IO () -> ReaderT Dict IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> IO ()
putStrLn (ArgName -> IO ()) -> ArgName -> IO ()
forall a b. (a -> b) -> a -> b
$ ArgName
"Dummy term in serialization: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s
    S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R Term
value = (Node -> R Term) -> Int32 -> R Term
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Term
valu where
    valu :: Node -> R Term
valu [Int32
a]       = (Int -> Term) -> Int32 -> R Term
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] = (Int -> [Elim] -> Term) -> Int32 -> Int32 -> R Term
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 -> [Elim] -> Term
Var   Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b] = (ArgInfo -> Abs Term -> Term) -> Int32 -> Int32 -> R Term
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]    = (Literal -> Term) -> Int32 -> R Term
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] = (QName -> [Elim] -> Term) -> Int32 -> Int32 -> R Term
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] -> Term
Def   Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = (ConHead -> ConInfo -> [Elim] -> Term)
-> Int32 -> Int32 -> Int32 -> R Term
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 -> [Elim] -> Term
Con Int32
a Int32
b Int32
c
    valu [Int32
5, Int32
a, Int32
b] = (Dom Type -> Abs Type -> Term) -> Int32 -> Int32 -> R Term
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 Type -> Abs Type -> Term
Pi    Int32
a Int32
b
    valu [Int32
7, Int32
a]    = (Sort' Term -> Term) -> Int32 -> R Term
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 -> Term
Sort  Int32
a
    valu [Int32
8, Int32
a]    = (Term -> Term) -> Int32 -> R Term
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]    = (Level -> Term) -> Int32 -> R Term
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 Node
_         = R Term
forall a. R a
malformed

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

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

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

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

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

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

instance EmbPrj I.Sort where
  icod_ :: Sort' Term -> S Int32
icod_ (Type  Level
a  ) = Int32 -> (Level -> Sort' Term) -> Level -> S Int32
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 Level -> Sort' Term
forall t. Level' t -> Sort' t
Type Level
a
  icod_ (Prop  Level
a  ) = Int32 -> (Level -> Sort' Term) -> Level -> S Int32
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 Level -> Sort' Term
forall t. Level' t -> Sort' t
Prop Level
a
  icod_ Sort' Term
SizeUniv    = Int32 -> Sort' Any -> Arrows (Domains (Sort' Any)) (S Int32)
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 Sort' Any
forall t. Sort' t
SizeUniv
  icod_ (Inf IsFibrant
f Integer
a)   = Int32
-> (IsFibrant -> Integer -> Sort' Any)
-> IsFibrant
-> Integer
-> S Int32
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 IsFibrant -> Integer -> Sort' Any
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
a
  icod_ (PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c) = Int32
-> (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term)
-> Dom' Term Term
-> Sort' Term
-> Abs (Sort' Term)
-> S Int32
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 Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c
  icod_ (FunSort Sort' Term
a Sort' Term
b) = Int32
-> (Sort' Term -> Sort' Term -> Sort' Term)
-> Sort' Term
-> Sort' Term
-> S Int32
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 Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' Term
a Sort' Term
b
  icod_ (UnivSort Sort' Term
a) = Int32 -> (Sort' Term -> Sort' Term) -> Sort' Term -> S Int32
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 Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort Sort' Term
a
  icod_ (MetaS MetaId
a [Elim]
b)  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (DefS QName
a [Elim]
b)   = Int32
-> (QName -> [Elim] -> Sort' Term) -> QName -> [Elim] -> S Int32
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 QName -> [Elim] -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
a [Elim]
b
  icod_ (SSet  Level
a  ) = Int32 -> (Level -> Sort' Term) -> Level -> S Int32
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 Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet Level
a
  icod_ Sort' Term
LockUniv    = Int32 -> Sort' Any -> Arrows (Domains (Sort' Any)) (S Int32)
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 Sort' Any
forall t. Sort' t
LockUniv
  icod_ (DummyS ArgName
s)   = do
    IO () -> ReaderT Dict IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Dict IO ()) -> IO () -> ReaderT Dict IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> IO ()
putStrLn (ArgName -> IO ()) -> ArgName -> IO ()
forall a b. (a -> b) -> a -> b
$ ArgName
"Dummy sort in serialization: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s
    S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R (Sort' Term)
value = (Node -> R (Sort' Term)) -> Int32 -> R (Sort' Term)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Sort' Term)
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]    = (Level' t -> Sort' t) -> Int32 -> R (Sort' t)
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' t -> Sort' t
forall t. Level' t -> Sort' t
Type  Int32
a
    valu [Int32
1, Int32
a]    = (Level' t -> Sort' t) -> Int32 -> R (Sort' t)
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' t -> Sort' t
forall t. Level' t -> Sort' t
Prop  Int32
a
    valu [Int32
2]       = Sort' t
-> Arrows
     (Constant Int32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
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' t
forall t. Sort' t
SizeUniv
    valu [Int32
3, Int32
f, Int32
a] = (IsFibrant -> Integer -> Sort' t) -> Int32 -> Int32 -> R (Sort' t)
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 -> Sort' t
forall t. IsFibrant -> Integer -> Sort' t
Inf Int32
f Int32
a
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)
-> Int32 -> Int32 -> Int32 -> R (Sort' t)
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' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
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] = (Sort' t -> Sort' t -> Sort' t) -> Int32 -> Int32 -> R (Sort' t)
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' t -> Sort' t -> Sort' t
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Int32
a Int32
b
    valu [Int32
6, Int32
a]    = (Sort' t -> Sort' t) -> Int32 -> R (Sort' t)
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' t -> Sort' t
forall t. Sort' t -> Sort' t
UnivSort Int32
a
    valu [Int32
7, Int32
a, Int32
b] = (QName -> [Elim' t] -> Sort' t) -> Int32 -> Int32 -> R (Sort' t)
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' t] -> Sort' t
forall t. QName -> [Elim' t] -> Sort' t
DefS Int32
a Int32
b
    valu [Int32
8, Int32
a]    = (Level' t -> Sort' t) -> Int32 -> R (Sort' t)
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' t -> Sort' t
forall t. Level' t -> Sort' t
SSet Int32
a
    valu [Int32
9]       = Sort' t
-> Arrows
     (Constant Int32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
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' t
forall t. Sort' t
LockUniv
    valu Node
_         = R (Sort' t)
forall a. R a
malformed

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

  value :: Int32 -> R DisplayForm
value = (Int -> [Elim] -> DisplayTerm -> DisplayForm)
-> Int32
-> R (CoDomain (Int -> [Elim] -> DisplayTerm -> DisplayForm))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> [Elim] -> 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) = (CheckpointId
 -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a)
-> CheckpointId
-> Map CheckpointId Substitution
-> ModuleNameHash
-> a
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
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 = (CheckpointId
 -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a)
-> Int32
-> R (CoDomain
        (CheckpointId
         -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing

instance EmbPrj CheckpointId where
  icod_ :: CheckpointId -> S Int32
icod_ (CheckpointId Int
a) = Int -> S Int32
forall a. EmbPrj a => a -> S Int32
icode Int
a
  value :: Int32 -> R CheckpointId
value Int32
n                = Int -> CheckpointId
CheckpointId (Int -> CheckpointId)
-> ExceptT TypeError (StateT St IO) Int -> R CheckpointId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) Int
forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj DisplayTerm where
  icod_ :: DisplayTerm -> S Int32
icod_ (DTerm    Term
a  )   = (Term -> DisplayTerm) -> Term -> S Int32
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  )   = Int32 -> (Term -> DisplayTerm) -> Term -> S Int32
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) = Int32
-> (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> ConHead
-> ConInfo
-> [Arg DisplayTerm]
-> S Int32
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)   = Int32
-> (QName -> [Elim' DisplayTerm] -> DisplayTerm)
-> QName
-> [Elim' DisplayTerm]
-> S Int32
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 [Elim]
c) = Int32
-> (DisplayTerm -> [DisplayTerm] -> [Elim] -> DisplayTerm)
-> DisplayTerm
-> [DisplayTerm]
-> [Elim]
-> S Int32
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] -> [Elim] -> DisplayTerm
DWithApp DisplayTerm
a [DisplayTerm]
b [Elim]
c

  value :: Int32 -> R DisplayTerm
value = (Node -> R DisplayTerm) -> Int32 -> R DisplayTerm
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R DisplayTerm
valu where
    valu :: Node -> R DisplayTerm
valu [Int32
a]          = (Term -> DisplayTerm) -> Int32 -> R DisplayTerm
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]       = (Term -> DisplayTerm) -> Int32 -> R DisplayTerm
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] = (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> Int32 -> Int32 -> Int32 -> R DisplayTerm
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]    = (QName -> [Elim' DisplayTerm] -> DisplayTerm)
-> Int32 -> Int32 -> R DisplayTerm
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] = (DisplayTerm -> [DisplayTerm] -> [Elim] -> DisplayTerm)
-> Int32 -> Int32 -> Int32 -> R DisplayTerm
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] -> [Elim] -> DisplayTerm
DWithApp Int32
a Int32
b Int32
c
    valu Node
_            = R DisplayTerm
forall a. R a
malformed

instance EmbPrj MutualId where
  icod_ :: MutualId -> S Int32
icod_ (MutId Int32
a) = Int32 -> S Int32
forall a. EmbPrj a => a -> S Int32
icode Int32
a
  value :: Int32 -> R MutualId
value Int32
n         = Int32 -> MutualId
MutId (Int32 -> MutualId)
-> ExceptT TypeError (StateT St IO) Int32 -> R MutualId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) Int32
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) = (Maybe QName -> Maybe QName -> CompKit)
-> Maybe QName -> Maybe QName -> S Int32
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 = (Maybe QName -> Maybe QName -> CompKit)
-> Int32 -> R (CoDomain (Maybe QName -> Maybe QName -> CompKit))
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) = (ArgInfo
 -> QName
 -> Type
 -> [Polarity]
 -> [Occurrence]
 -> NumGeneralizableArgs
 -> [Maybe Name]
 -> [LocalDisplayForm]
 -> MutualId
 -> CompiledRepresentation
 -> Maybe QName
 -> Bool
 -> Set QName
 -> Bool
 -> Bool
 -> Bool
 -> Blocked_
 -> Language
 -> Defn
 -> Definition)
-> ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> S Int32
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 (KillRangeT Type
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 = (ArgInfo
 -> QName
 -> Type
 -> [Polarity]
 -> [Occurrence]
 -> NumGeneralizableArgs
 -> [Maybe Name]
 -> [LocalDisplayForm]
 -> MutualId
 -> CompiledRepresentation
 -> Maybe QName
 -> Bool
 -> Set QName
 -> Bool
 -> Bool
 -> Bool
 -> Blocked_
 -> Language
 -> Defn
 -> Definition)
-> Int32
-> R (CoDomain
        (ArgInfo
         -> QName
         -> Type
         -> [Polarity]
         -> [Occurrence]
         -> NumGeneralizableArgs
         -> [Maybe Name]
         -> [LocalDisplayForm]
         -> MutualId
         -> CompiledRepresentation
         -> Maybe QName
         -> Bool
         -> Set QName
         -> Bool
         -> Bool
         -> Bool
         -> Blocked_
         -> Language
         -> Defn
         -> Definition))
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 = NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NotBlocked' Any
forall t. NotBlocked' t
ReallyNotBlocked
  icod_ (StuckOn Elim
a)      = Int32 -> (Elim -> NotBlocked) -> Elim -> S Int32
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 Elim -> NotBlocked
forall t. Elim' t -> NotBlocked' t
StuckOn Elim
a
  icod_ NotBlocked
Underapplied     = Int32
-> NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
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 NotBlocked' Any
forall t. NotBlocked' t
Underapplied
  icod_ NotBlocked
AbsurdMatch      = Int32
-> NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
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 NotBlocked' Any
forall t. NotBlocked' t
AbsurdMatch
  icod_ NotBlocked
MissingClauses   = Int32
-> NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
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 NotBlocked' Any
forall t. NotBlocked' t
MissingClauses

  value :: Int32 -> R NotBlocked
value = (Node -> R NotBlocked) -> Int32 -> R NotBlocked
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NotBlocked
forall t. EmbPrj t => Node -> R (NotBlocked' t)
valu where
    valu :: Node -> R (NotBlocked' t)
valu []     = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
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 NotBlocked' t
forall t. NotBlocked' t
ReallyNotBlocked
    valu [Int32
0, Int32
a] = (Elim' t -> NotBlocked' t) -> Int32 -> R (NotBlocked' t)
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 Elim' t -> NotBlocked' t
forall t. Elim' t -> NotBlocked' t
StuckOn Int32
a
    valu [Int32
1]    = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
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 NotBlocked' t
forall t. NotBlocked' t
Underapplied
    valu [Int32
2]    = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
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 NotBlocked' t
forall t. NotBlocked' t
AbsurdMatch
    valu [Int32
3]    = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
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 NotBlocked' t
forall t. NotBlocked' t
MissingClauses
    valu Node
_      = R (NotBlocked' t)
forall a. R a
malformed

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

  value :: Int32 -> R Blocked_
value = (NotBlocked -> () -> Blocked_)
-> Int32 -> R (CoDomain (NotBlocked -> () -> Blocked_))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN NotBlocked -> () -> Blocked_
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)      = Int32 -> (Int -> [Arg Int] -> NLPat) -> Int -> [Arg Int] -> S Int32
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)      = Int32 -> (QName -> PElims -> NLPat) -> QName -> PElims -> S Int32
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)      = Int32
-> (ArgInfo -> Abs NLPat -> NLPat)
-> ArgInfo
-> Abs NLPat
-> S Int32
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)       = Int32
-> (Dom NLPType -> Abs NLPType -> NLPat)
-> Dom NLPType
-> Abs NLPType
-> S Int32
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)       = Int32 -> (NLPSort -> NLPat) -> NLPSort -> S Int32
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) = Int32 -> (Int -> PElims -> NLPat) -> Int -> PElims -> S Int32
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)       = Int32 -> (Term -> NLPat) -> Term -> S Int32
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 = (Node -> R NLPat) -> Int32 -> R NLPat
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]    = (Int -> [Arg Int] -> NLPat) -> Int32 -> Int32 -> R NLPat
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]    = (QName -> PElims -> NLPat) -> Int32 -> Int32 -> R NLPat
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]    = (ArgInfo -> Abs NLPat -> NLPat) -> Int32 -> Int32 -> R NLPat
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]    = (Dom NLPType -> Abs NLPType -> NLPat) -> Int32 -> Int32 -> R NLPat
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]       = (NLPSort -> NLPat) -> Int32 -> R NLPat
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]    = (Int -> PElims -> NLPat) -> Int32 -> Int32 -> R NLPat
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]       = (Term -> NLPat) -> Int32 -> R NLPat
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
_            = R NLPat
forall a. R a
malformed

instance EmbPrj NLPType where
  icod_ :: NLPType -> S Int32
icod_ (NLPType NLPSort
a NLPat
b) = (NLPSort -> NLPat -> NLPType) -> NLPSort -> NLPat -> S Int32
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 = (NLPSort -> NLPat -> NLPType)
-> Int32 -> R (CoDomain (NLPSort -> NLPat -> NLPType))
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)   = Int32 -> (NLPat -> NLPSort) -> NLPat -> S Int32
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)   = Int32 -> (NLPat -> NLPSort) -> NLPat -> S Int32
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)  = Int32
-> (IsFibrant -> Integer -> NLPSort)
-> IsFibrant
-> Integer
-> S Int32
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   = Int32 -> NLPSort -> Arrows (Domains NLPSort) (S Int32)
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   = Int32 -> NLPSort -> Arrows (Domains NLPSort) (S Int32)
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
PSizeUniv

  value :: Int32 -> R NLPSort
value = (Node -> R NLPSort) -> Int32 -> R NLPSort
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] = (NLPat -> NLPSort) -> Int32 -> R NLPSort
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] = (NLPat -> NLPSort) -> Int32 -> R NLPSort
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] = (IsFibrant -> Integer -> NLPSort) -> Int32 -> Int32 -> R NLPSort
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]    = NLPSort
-> Arrows (Constant Int32 (Domains NLPSort)) (R (CoDomain NLPSort))
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]    = NLPSort
-> Arrows (Constant Int32 (Domains NLPSort)) (R (CoDomain NLPSort))
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 Node
_      = R NLPSort
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) = (QName
 -> Telescope
 -> QName
 -> PElims
 -> Term
 -> Type
 -> Bool
 -> RewriteRule)
-> QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> S Int32
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 = (QName
 -> Telescope
 -> QName
 -> PElims
 -> Term
 -> Type
 -> Bool
 -> RewriteRule)
-> Int32
-> R (CoDomain
        (QName
         -> Telescope
         -> QName
         -> PElims
         -> Term
         -> Type
         -> Bool
         -> RewriteRule))
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) = (Maybe QName
 -> QName -> Arg QName -> Int -> ProjLams -> Projection)
-> Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> S Int32
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 = (Maybe QName
 -> QName -> Arg QName -> Int -> ProjLams -> Projection)
-> Int32
-> R (CoDomain
        (Maybe QName
         -> QName -> Arg QName -> Int -> ProjLams -> Projection))
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) = ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> S Int32
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 = ([Arg ArgName] -> ProjLams)
-> Int32 -> R (CoDomain ([Arg ArgName] -> ProjLams))
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) = (Telescope -> [(Face, Term)] -> System)
-> Telescope -> [(Face, Term)] -> S Int32
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 = (Telescope -> [(Face, Term)] -> System)
-> Int32 -> R (CoDomain (Telescope -> [(Face, Term)] -> System))
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) = (ModuleName -> Bool -> Maybe System -> ExtLamInfo)
-> ModuleName -> Bool -> Maybe System -> S Int32
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 = (ModuleName -> Bool -> Maybe System -> ExtLamInfo)
-> Int32
-> R (CoDomain (ModuleName -> Bool -> Maybe System -> ExtLamInfo))
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     = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ Polarity
Contravariant = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
  icod_ Polarity
Invariant     = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
  icod_ Polarity
Nonvariant    = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3

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

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

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

instance EmbPrj NumGeneralizableArgs where
  icod_ :: NumGeneralizableArgs -> S Int32
icod_ NumGeneralizableArgs
NoGeneralizableArgs       = NumGeneralizableArgs
-> Arrows (Domains NumGeneralizableArgs) (S Int32)
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) = (Int -> NumGeneralizableArgs) -> Int -> S Int32
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 = (Node -> R NumGeneralizableArgs) -> Int32 -> R NumGeneralizableArgs
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NumGeneralizableArgs
valu where
    valu :: Node -> R NumGeneralizableArgs
valu []  = NumGeneralizableArgs
-> Arrows
     (Constant Int32 (Domains NumGeneralizableArgs))
     (R (CoDomain NumGeneralizableArgs))
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] = (Int -> NumGeneralizableArgs) -> Int32 -> R NumGeneralizableArgs
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
_   = R NumGeneralizableArgs
forall a. R a
malformed

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

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

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

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

instance EmbPrj EtaEquality where
  icod_ :: EtaEquality -> S Int32
icod_ (Specified HasEta
a) = Int32 -> (HasEta -> EtaEquality) -> HasEta -> S Int32
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)  = Int32 -> (HasEta -> EtaEquality) -> HasEta -> S Int32
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 = (Node -> R EtaEquality) -> Int32 -> R EtaEquality
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] = (HasEta -> EtaEquality) -> Int32 -> R EtaEquality
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] = (HasEta -> EtaEquality) -> Int32 -> R EtaEquality
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
_     = R EtaEquality
forall a. R a
malformed

instance EmbPrj Defn where
  icod_ :: Defn -> S Int32
icod_ (Axiom       Bool
a)                                 = Int32 -> (Bool -> Defn) -> Bool -> S Int32
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
_:[Clause]
_) FunctionInverse
c Maybe [QName]
d IsAbstract
e Delayed
f Maybe Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k)   = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (Function    [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t []    FunctionInverse
c Maybe [QName]
d IsAbstract
e Delayed
f Maybe Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k)   =
    Int32
-> ([Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> FunctionInverse
    -> Maybe [QName]
    -> IsAbstract
    -> Delayed
    -> Maybe Projection
    -> Set FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Defn)
-> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Delayed
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> S Int32
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
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t []) [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s FunctionInverse
c Maybe [QName]
d IsAbstract
e Delayed
f Maybe Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k
  icod_ (Datatype    Int
a Int
b Maybe Clause
c [QName]
d Sort' Term
e Maybe [QName]
f IsAbstract
g [QName]
h)                   = Int32
-> (Int
    -> Int
    -> Maybe Clause
    -> [QName]
    -> Sort' Term
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Defn)
-> Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> S Int32
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' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Defn
Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort' Term
e Maybe [QName]
f IsAbstract
g [QName]
h
  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 IsAbstract
k CompKit
l)           = Int32
-> (Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> IsAbstract
    -> CompKit
    -> Defn)
-> Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> IsAbstract
-> CompKit
-> S Int32
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
-> 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 IsAbstract
k CompKit
l
  icod_ (Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e Induction
f CompKit
g Maybe [QName]
h [IsForced]
i Maybe [Bool]
j)               = Int32
-> (Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn)
-> Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> S Int32
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)                         = Int32
-> (IsAbstract
    -> ArgName
    -> [Clause]
    -> FunctionInverse
    -> Maybe CompiledClauses
    -> Defn)
-> IsAbstract
-> ArgName
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> S Int32
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' Term
b)                             = Int32
-> (ArgName -> Sort' Term -> Defn)
-> ArgName
-> Sort' Term
-> S Int32
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' Term -> Defn
PrimitiveSort ArgName
a Sort' Term
b
  icod_ AbstractDefn{}                                  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ Defn
GeneralizableVar                                = Int32 -> Defn -> Arrows (Domains Defn) (S Int32)
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{}                                  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R Defn
value = (Node -> R Defn) -> Int32 -> R Defn
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]                                     = (Bool -> Defn) -> Int32 -> R Defn
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
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k]    = ([Clause]
 -> Maybe CompiledClauses
 -> Maybe SplitTree
 -> FunctionInverse
 -> Maybe [QName]
 -> IsAbstract
 -> Delayed
 -> Maybe Projection
 -> Set FunctionFlag
 -> Maybe Bool
 -> Maybe ExtLamInfo
 -> Maybe QName
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
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
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
forall a. Maybe a
Nothing []) Int32
a Int32
b Int32
s Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k
    valu [Int32
2, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h]                = (Int
 -> Int
 -> Maybe Clause
 -> [QName]
 -> Sort' Term
 -> Maybe [QName]
 -> IsAbstract
 -> [QName]
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
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' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Defn
Datatype Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h
    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]    = (Int
 -> Maybe Clause
 -> ConHead
 -> Bool
 -> [Dom QName]
 -> Telescope
 -> Maybe [QName]
 -> EtaEquality
 -> PatternOrCopattern
 -> Maybe Induction
 -> IsAbstract
 -> CompKit
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
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
-> 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
    valu [Int32
4, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j]          = (Int
 -> Int
 -> ConHead
 -> QName
 -> IsAbstract
 -> Induction
 -> CompKit
 -> Maybe [QName]
 -> [IsForced]
 -> Maybe [Bool]
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
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]                         = (IsAbstract
 -> ArgName
 -> [Clause]
 -> FunctionInverse
 -> Maybe CompiledClauses
 -> Defn)
-> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R Defn
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]                                  = (ArgName -> Sort' Term -> Defn) -> Int32 -> Int32 -> R Defn
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' Term -> Defn
PrimitiveSort Int32
a Int32
b
    valu [Int32
7]                                        = Defn -> Arrows (Constant Int32 (Domains Defn)) (R (CoDomain Defn))
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
_                                          = R Defn
forall a. R a
malformed

instance EmbPrj LazySplit where
  icod_ :: LazySplit -> S Int32
icod_ LazySplit
StrictSplit = LazySplit -> Arrows (Domains LazySplit) (S Int32)
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   = Int32 -> LazySplit -> Arrows (Domains LazySplit) (S Int32)
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 = (Node -> R LazySplit) -> Int32 -> R LazySplit
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R LazySplit
forall a. (Eq a, Num a) => [a] -> R LazySplit
valu where
    valu :: [a] -> R LazySplit
valu []  = LazySplit
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
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] = LazySplit
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
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]
_   = R LazySplit
forall a. R a
malformed

instance EmbPrj SplitTag where
  icod_ :: SplitTag -> S Int32
icod_ (SplitCon QName
c)  = Int32 -> (QName -> SplitTag) -> QName -> S Int32
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)  = Int32 -> (Literal -> SplitTag) -> Literal -> S Int32
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 = SplitTag -> Arrows (Domains SplitTag) (S Int32)
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 = (Node -> R SplitTag) -> Int32 -> R SplitTag
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R SplitTag
valu where
    valu :: Node -> R SplitTag
valu []     = SplitTag
-> Arrows
     (Constant Int32 (Domains SplitTag)) (R (CoDomain SplitTag))
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] = (QName -> SplitTag) -> Int32 -> R SplitTag
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] = (Literal -> SplitTag) -> Int32 -> R SplitTag
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
_      = R SplitTag
forall a. R a
malformed

instance EmbPrj a => EmbPrj (SplitTree' a) where
  icod_ :: SplitTree' a -> S Int32
icod_ (SplittingDone Int
a) = (Int -> SplitTree' Any) -> Int -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> SplitTree' Any
forall a. Int -> SplitTree' a
SplittingDone Int
a
  icod_ (SplitAt Arg Int
a LazySplit
b SplitTrees' a
c)   = Int32
-> (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
-> Arg Int
-> LazySplit
-> SplitTrees' a
-> S Int32
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 Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
a LazySplit
b SplitTrees' a
c

  value :: Int32 -> R (SplitTree' a)
value = (Node -> R (SplitTree' a)) -> Int32 -> R (SplitTree' a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (SplitTree' a)
forall a. EmbPrj a => Node -> R (SplitTree' a)
valu where
    valu :: Node -> R (SplitTree' a)
valu [Int32
a]          = (Int -> SplitTree' a) -> Int32 -> R (SplitTree' 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 -> SplitTree' a
forall a. Int -> SplitTree' a
SplittingDone Int32
a
    valu [Int32
0, Int32
a, Int32
b, Int32
c] = (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
-> Int32 -> Int32 -> Int32 -> R (SplitTree' 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 Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Int32
a Int32
b Int32
c
    valu Node
_            = R (SplitTree' a)
forall a. R a
malformed

instance EmbPrj FunctionFlag where
  icod_ :: FunctionFlag -> S Int32
icod_ FunctionFlag
FunStatic       = Int32 -> FunctionFlag -> Arrows (Domains FunctionFlag) (S Int32)
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       = Int32 -> FunctionFlag -> Arrows (Domains FunctionFlag) (S Int32)
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        = Int32 -> FunctionFlag -> Arrows (Domains FunctionFlag) (S Int32)
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 = (Node -> R FunctionFlag) -> Int32 -> R FunctionFlag
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R FunctionFlag
forall a. (Eq a, Num a) => [a] -> R FunctionFlag
valu where
    valu :: [a] -> R FunctionFlag
valu [a
0] = FunctionFlag
-> Arrows
     (Constant Int32 (Domains FunctionFlag)) (R (CoDomain FunctionFlag))
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] = FunctionFlag
-> Arrows
     (Constant Int32 (Domains FunctionFlag)) (R (CoDomain FunctionFlag))
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] = FunctionFlag
-> Arrows
     (Constant Int32 (Domains FunctionFlag)) (R (CoDomain FunctionFlag))
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]
_   = R FunctionFlag
forall a. R a
malformed

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

  value :: Int32 -> R (WithArity a)
value = (Int -> a -> WithArity a)
-> Int32 -> R (CoDomain (Int -> a -> WithArity a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> a -> WithArity a
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) = (Bool
 -> Map QName (WithArity a)
 -> Maybe (ConHead, WithArity a)
 -> Map Literal a
 -> Maybe a
 -> Maybe Bool
 -> Bool
 -> Case a)
-> Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
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 = (Bool
 -> Map QName (WithArity a)
 -> Maybe (ConHead, WithArity a)
 -> Map Literal a
 -> Maybe a
 -> Maybe Bool
 -> Bool
 -> Case a)
-> Int32
-> R (CoDomain
        (Bool
         -> Map QName (WithArity a)
         -> Maybe (ConHead, WithArity a)
         -> Map Literal a
         -> Maybe a
         -> Maybe Bool
         -> Bool
         -> Case a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
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)   = ([Arg ArgName] -> CompiledClauses' Any) -> [Arg ArgName] -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> CompiledClauses' Any
forall a. [Arg ArgName] -> CompiledClauses' a
Fail [Arg ArgName]
a
  icod_ (Done [Arg ArgName]
a Term
b) = ([Arg ArgName] -> Term -> CompiledClauses)
-> [Arg ArgName] -> Term -> S Int32
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 -> CompiledClauses
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [Arg ArgName]
a (Term -> Term
forall a. KillRange a => KillRangeT a
P.killRange Term
b)
  icod_ (Case Arg Int
a Case CompiledClauses
b) = Int32
-> (Arg Int -> Case CompiledClauses -> CompiledClauses)
-> Arg Int
-> Case CompiledClauses
-> S Int32
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 Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
a Case CompiledClauses
b

  value :: Int32 -> R CompiledClauses
value = (Node -> R CompiledClauses) -> Int32 -> R CompiledClauses
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R CompiledClauses
forall a.
(EmbPrj a, EmbPrj (CompiledClauses' a)) =>
Node -> R (CompiledClauses' a)
valu where
    valu :: Node -> R (CompiledClauses' a)
valu [Int32
a]       = ([Arg ArgName] -> CompiledClauses' a)
-> Int32 -> R (CompiledClauses' 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 [Arg ArgName] -> CompiledClauses' a
forall a. [Arg ArgName] -> CompiledClauses' a
Fail Int32
a
    valu [Int32
a, Int32
b]    = ([Arg ArgName] -> a -> CompiledClauses' a)
-> Int32 -> Int32 -> R (CompiledClauses' 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 [Arg ArgName] -> a -> CompiledClauses' a
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b] = (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)
-> Int32 -> Int32 -> R (CompiledClauses' 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 Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Int32
a Int32
b
    valu Node
_         = R (CompiledClauses' a)
forall a. R a
malformed

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

  value :: Int32 -> R (FunctionInverse' a)
value = (Node -> R (FunctionInverse' a)) -> Int32 -> R (FunctionInverse' a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (FunctionInverse' a)
forall c. EmbPrj [c] => Node -> R (FunctionInverse' c)
valu where
    valu :: Node -> R (FunctionInverse' c)
valu []  = FunctionInverse' c
-> Arrows
     (Constant Int32 (Domains (FunctionInverse' c)))
     (R (CoDomain (FunctionInverse' 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 FunctionInverse' c
forall c. FunctionInverse' c
NotInjective
    valu [Int32
a] = (InversionMap c -> FunctionInverse' c)
-> Int32 -> R (FunctionInverse' 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 InversionMap c -> FunctionInverse' c
forall c. InversionMap c -> FunctionInverse' c
Inverse Int32
a
    valu Node
_   = R (FunctionInverse' c)
forall a. R a
malformed

instance EmbPrj TermHead where
  icod_ :: TermHead -> S Int32
icod_ TermHead
SortHead     = TermHead -> Arrows (Domains TermHead) (S Int32)
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       = Int32 -> TermHead -> Arrows (Domains TermHead) (S Int32)
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) = Int32 -> (QName -> TermHead) -> QName -> S Int32
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)  = Int32 -> (Int -> TermHead) -> Int -> S Int32
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  = Int32 -> TermHead -> Arrows (Domains TermHead) (S Int32)
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 = (Node -> R TermHead) -> Int32 -> R TermHead
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R TermHead
valu where
    valu :: Node -> R TermHead
valu []     = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
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]    = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
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] = (QName -> TermHead) -> Int32 -> R TermHead
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] = (Int -> TermHead) -> Int32 -> R TermHead
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]    = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
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
_      = R TermHead
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) = (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Bool
 -> Maybe Bool
 -> Maybe Bool
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Clause)
-> Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> S Int32
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
-> 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

  value :: Int32 -> R Clause
value = (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Bool
 -> Maybe Bool
 -> Maybe Bool
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Clause)
-> Int32
-> R (CoDomain
        (Range
         -> Range
         -> Telescope
         -> NAPs
         -> Maybe Term
         -> Maybe (Arg Type)
         -> Bool
         -> Maybe Bool
         -> Maybe Bool
         -> Maybe Bool
         -> ExpandedEllipsis
         -> Clause))
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
-> 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) = (PatternInfo
 -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> PatternInfo
-> Bool
-> Bool
-> Maybe (Arg Type)
-> Bool
-> S Int32
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 = (PatternInfo
 -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> Int32
-> R (CoDomain
        (PatternInfo
         -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo))
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) = (ArgName -> Int -> DBPatVar) -> ArgName -> Int -> S Int32
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 = (ArgName -> Int -> DBPatVar)
-> Int32 -> R (CoDomain (ArgName -> Int -> DBPatVar))
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) = (PatOrigin -> [Name] -> PatternInfo)
-> PatOrigin -> [Name] -> S Int32
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 = (PatOrigin -> [Name] -> PatternInfo)
-> Int32 -> R (CoDomain (PatOrigin -> [Name] -> PatternInfo))
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  = PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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   = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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) = Int32 -> (Name -> PatOrigin) -> Name -> S Int32
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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    = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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  = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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 = (Node -> R PatOrigin) -> Int32 -> R PatOrigin
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R PatOrigin
valu where
    valu :: Node -> R PatOrigin
valu []     = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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] = (Name -> PatOrigin) -> Int32 -> R PatOrigin
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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
_      = R PatOrigin
forall a. R a
malformed

instance EmbPrj a => EmbPrj (I.Pattern' a) where
  icod_ :: Pattern' a -> S Int32
icod_ (VarP PatternInfo
a a
b  ) = Int32
-> (PatternInfo -> a -> Pattern' a) -> PatternInfo -> a -> S Int32
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 PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
a a
b
  icod_ (ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c) = Int32
-> (ConHead
    -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
-> ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' a)]
-> S Int32
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 ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c
  icod_ (LitP PatternInfo
a Literal
b  ) = Int32
-> (PatternInfo -> Literal -> Pattern' Any)
-> PatternInfo
-> Literal
-> S Int32
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 PatternInfo -> Literal -> Pattern' Any
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
a Literal
b
  icod_ (DotP PatternInfo
a Term
b  ) = Int32
-> (PatternInfo -> Term -> Pattern' Any)
-> PatternInfo
-> Term
-> S Int32
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 PatternInfo -> Term -> Pattern' Any
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
a Term
b
  icod_ (ProjP ProjOrigin
a QName
b ) = Int32
-> (ProjOrigin -> QName -> Pattern' Any)
-> ProjOrigin
-> QName
-> S Int32
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 ProjOrigin -> QName -> Pattern' Any
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
a QName
b
  icod_ (IApplyP PatternInfo
a Term
b Term
c a
d) = Int32
-> (PatternInfo -> Term -> Term -> a -> Pattern' a)
-> PatternInfo
-> Term
-> Term
-> a
-> S Int32
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 PatternInfo -> Term -> Term -> a -> Pattern' a
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) = Int32
-> (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a)
-> PatternInfo
-> QName
-> [NamedArg (Pattern' a)]
-> S Int32
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 PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c

  value :: Int32 -> R (Pattern' a)
value = (Node -> R (Pattern' a)) -> Int32 -> R (Pattern' a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Pattern' a)
forall x. EmbPrj x => Node -> R (Pattern' x)
valu where
    valu :: Node -> R (Pattern' x)
valu [Int32
0, Int32
a, Int32
b] = (PatternInfo -> x -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
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 PatternInfo -> x -> Pattern' x
forall x. PatternInfo -> x -> Pattern' x
VarP Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b, Int32
c] = (ConHead
 -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)
-> Int32 -> Int32 -> Int32 -> R (Pattern' x)
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 -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP Int32
a Int32
b Int32
c
    valu [Int32
2, Int32
a, Int32
b] = (PatternInfo -> Literal -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
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 PatternInfo -> Literal -> Pattern' x
forall x. PatternInfo -> Literal -> Pattern' x
LitP Int32
a Int32
b
    valu [Int32
3, Int32
a, Int32
b] = (PatternInfo -> Term -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
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 PatternInfo -> Term -> Pattern' x
forall x. PatternInfo -> Term -> Pattern' x
DotP Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b] = (ProjOrigin -> QName -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
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 ProjOrigin -> QName -> Pattern' x
forall x. ProjOrigin -> QName -> Pattern' x
ProjP Int32
a Int32
b
    valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d] = (PatternInfo -> Term -> Term -> x -> Pattern' x)
-> Int32 -> Int32 -> Int32 -> Int32 -> R (Pattern' x)
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 PatternInfo -> Term -> Term -> x -> Pattern' x
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] = (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)
-> Int32 -> Int32 -> Int32 -> R (Pattern' x)
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 PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP Int32
a Int32
b Int32
c
    valu Node
_         = R (Pattern' x)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Builtin a) where
  icod_ :: Builtin a -> S Int32
icod_ (Prim    a
a) = (a -> Builtin a) -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Builtin a
forall pf. pf -> Builtin pf
Prim a
a
  icod_ (Builtin Term
a) = Int32 -> (Term -> Builtin Any) -> Term -> S Int32
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 -> Builtin Any
forall pf. Term -> Builtin pf
Builtin Term
a

  value :: Int32 -> R (Builtin a)
value = (Node -> R (Builtin a)) -> Int32 -> R (Builtin a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Builtin a)
forall pf. EmbPrj pf => Node -> R (Builtin pf)
valu where
    valu :: Node -> R (Builtin pf)
valu [Int32
a]    = (pf -> Builtin pf) -> Int32 -> R (Builtin pf)
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 pf -> Builtin pf
forall pf. pf -> Builtin pf
Prim    Int32
a
    valu [Int32
1, Int32
a] = (Term -> Builtin pf) -> Int32 -> R (Builtin pf)
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 -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Int32
a
    valu Node
_      = R (Builtin pf)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Substitution' a) where
  icod_ :: Substitution' a -> S Int32
icod_ Substitution' a
IdS              = Substitution' Any -> Arrows (Domains (Substitution' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Substitution' Any
forall a. Substitution' a
IdS
  icod_ (EmptyS Impossible
a)       = Int32 -> (Impossible -> Substitution' Any) -> Impossible -> S Int32
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 Impossible -> Substitution' Any
forall a. Impossible -> Substitution' a
EmptyS Impossible
a
  icod_ (a
a :# Substitution' a
b)         = Int32
-> (a -> Substitution' a -> Substitution' a)
-> a
-> Substitution' a
-> S Int32
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 a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) a
a Substitution' a
b
  icod_ (Strengthen Impossible
a Substitution' a
b) = Int32
-> (Impossible -> Substitution' a -> Substitution' a)
-> Impossible
-> Substitution' a
-> S Int32
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 Impossible -> Substitution' a -> Substitution' a
forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Impossible
a Substitution' a
b
  icod_ (Wk Int
a Substitution' a
b)         = Int32
-> (Int -> Substitution' a -> Substitution' a)
-> Int
-> Substitution' a
-> S Int32
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 -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Wk Int
a Substitution' a
b
  icod_ (Lift Int
a Substitution' a
b)       = Int32
-> (Int -> Substitution' a -> Substitution' a)
-> Int
-> Substitution' a
-> S Int32
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 -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Lift Int
a Substitution' a
b

  value :: Int32 -> R (Substitution' a)
value = (Node -> R (Substitution' a)) -> Int32 -> R (Substitution' a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Substitution' a)
forall a. EmbPrj a => Node -> R (Substitution' a)
valu where
    valu :: Node -> R (Substitution' a)
valu []        = Substitution' a
-> Arrows
     (Constant Int32 (Domains (Substitution' a)))
     (R (CoDomain (Substitution' 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 Substitution' a
forall a. Substitution' a
IdS
    valu [Int32
1, Int32
a]    = (Impossible -> Substitution' a) -> Int32 -> R (Substitution' 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 Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Int32
a
    valu [Int32
2, Int32
a, Int32
b] = (a -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' 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 a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) Int32
a Int32
b
    valu [Int32
3, Int32
a, Int32
b]    = (Impossible -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' 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 Impossible -> Substitution' a -> Substitution' a
forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b] = (Int -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' 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 -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Wk Int32
a Int32
b
    valu [Int32
5, Int32
a, Int32
b] = (Int -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' 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 -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Lift Int32
a Int32
b
    valu Node
_         = R (Substitution' a)
forall a. R a
malformed