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

module Agda.TypeChecking.Serialise.Instances.Internal where

import Control.Monad.IO.Class

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

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

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

import Agda.Utils.Permutation

import Agda.Utils.Impossible

instance EmbPrj a => EmbPrj (Dom a) where
  icod_ :: Dom a -> S Int32
icod_ (Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f) = (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
-> Arrows
     (Domains
        (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom 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 -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f

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

instance EmbPrj Signature where
  icod_ :: Signature -> S Int32
icod_ (Sig Sections
a Definitions
b RewriteRuleMap
c) = (Sections -> Definitions -> RewriteRuleMap -> Signature)
-> Arrows
     (Domains (Sections -> Definitions -> RewriteRuleMap -> Signature))
     (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)
-> Arrows (Domains (Telescope -> Section)) (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)
-> Arrows (Domains (a -> Abs (Tele a) -> 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 -> ExceptT TypeError (StateT St IO) (Tele a)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (Tele a))) (R (CoDomain (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)
-> Arrows
     (Constant Int32 (Domains (a -> Abs (Tele a) -> Tele a)))
     (R (CoDomain (a -> Abs (Tele a) -> 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
_      = ExceptT TypeError (StateT St IO) (Tele a)
Arrows (Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele a)))
forall a. R a
malformed

instance EmbPrj Permutation where
  icod_ :: Permutation -> S Int32
icod_ (Perm Int
a [Int]
b) = (Int -> [Int] -> Permutation)
-> Arrows (Domains (Int -> [Int] -> Permutation)) (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)
-> Arrows (Domains (Int -> a -> Drop 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) -> Arrows (Domains (Arg a -> Elim' 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)
-> Arrows (Domains (a -> a -> a -> Elim' 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)
-> Arrows (Domains (ProjOrigin -> QName -> Elim' 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
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)
-> Arrows
     (Constant Int32 (Domains (Arg a -> Elim' a)))
     (R (CoDomain (Arg a -> 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)
-> Arrows
     (Constant Int32 (Domains (a -> a -> a -> Elim' a)))
     (R (CoDomain (a -> a -> a -> 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)
-> Arrows
     (Constant Int32 (Domains (ProjOrigin -> QName -> Elim' a)))
     (R (CoDomain (ProjOrigin -> QName -> 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)
-> Arrows (Domains (PatternOrCopattern -> 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' 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)
-> Arrows
     (Constant Int32 (Domains (PatternOrCopattern -> DataOrRecord)))
     (R (CoDomain (PatternOrCopattern -> 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)
-> Arrows
     (Domains
        (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead))
     (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)
-> Arrows (Domains (Sort' Term -> a -> Type' 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)
-> Arrows (Domains (ArgName -> a -> Abs 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)
-> Arrows (Domains (ArgName -> a -> Abs 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)
-> Arrows
     (Constant Int32 (Domains (ArgName -> a -> Abs a)))
     (R (CoDomain (ArgName -> a -> 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)
-> Arrows
     (Constant Int32 (Domains (ArgName -> a -> Abs a)))
     (R (CoDomain (ArgName -> a -> 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) -> Arrows (Domains (Int -> 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' (\ Int
a -> Int -> Elims -> Term
Var Int
a []) Int
a
  icod_ (Var      Int
a Elims
b) = Int32
-> (Int -> Elims -> Term)
-> Arrows (Domains (Int -> Elims -> 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
0 Int -> Elims -> Term
Var Int
a Elims
b
  icod_ (Lam      ArgInfo
a Abs Term
b) = Int32
-> (ArgInfo -> Abs Term -> Term)
-> Arrows (Domains (ArgInfo -> Abs 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
1 ArgInfo -> Abs Term -> Term
Lam ArgInfo
a Abs Term
b
  icod_ (Lit      Literal
a  ) = Int32
-> (Literal -> Term)
-> Arrows (Domains (Literal -> 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
2 Literal -> Term
Lit Literal
a
  icod_ (Def      QName
a Elims
b) = Int32
-> (QName -> Elims -> Term)
-> Arrows (Domains (QName -> Elims -> 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 QName -> Elims -> Term
Def QName
a Elims
b
  icod_ (Con    ConHead
a ConInfo
b Elims
c) = Int32
-> (ConHead -> ConInfo -> Elims -> Term)
-> Arrows (Domains (ConHead -> ConInfo -> Elims -> 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 ConHead -> ConInfo -> Elims -> Term
Con ConHead
a ConInfo
b Elims
c
  icod_ (Pi       Dom' Term Type
a Abs Type
b) = Int32
-> (Dom' Term Type -> Abs Type -> Term)
-> Arrows (Domains (Dom' Term Type -> Abs Type -> 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 Dom' Term Type -> Abs Type -> Term
Pi Dom' Term Type
a Abs Type
b
  icod_ (MetaV    MetaId
a Elims
b) = Int32
-> (MetaId -> Elims -> Term)
-> Arrows (Domains (MetaId -> Elims -> 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 MetaId -> Elims -> Term
MetaV MetaId
a Elims
b
  icod_ (Sort     Sort' Term
a  ) = Int32
-> (Sort' Term -> Term)
-> Arrows (Domains (Sort' 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
7 Sort' Term -> Term
Sort Sort' Term
a
  icod_ (DontCare Term
a  ) = Int32
-> (Term -> Term) -> Arrows (Domains (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) -> Arrows (Domains (Level -> 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
9 Level -> Term
Level Level
a
  icod_ (Dummy    ArgName
a Elims
b) = Int32
-> (ArgName -> Elims -> Term)
-> Arrows (Domains (ArgName -> Elims -> 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
10 ArgName -> Elims -> Term
Dummy ArgName
a Elims
b

  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)
-> Arrows
     (Constant Int32 (Domains (Int -> Term)))
     (R (CoDomain (Int -> 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 -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (Int -> Elims -> Term)))
     (R (CoDomain (Int -> Elims -> 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 -> Elims -> Term
Var   Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b] = (ArgInfo -> Abs Term -> Term)
-> Arrows
     (Constant Int32 (Domains (ArgInfo -> Abs Term -> Term)))
     (R (CoDomain (ArgInfo -> Abs Term -> 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)
-> Arrows
     (Constant Int32 (Domains (Literal -> Term)))
     (R (CoDomain (Literal -> 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 -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (QName -> Elims -> Term)))
     (R (CoDomain (QName -> Elims -> 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 -> Elims -> Term
Def   Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = (ConHead -> ConInfo -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (ConHead -> ConInfo -> Elims -> Term)))
     (R (CoDomain (ConHead -> ConInfo -> Elims -> 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 -> Elims -> Term
Con Int32
a Int32
b Int32
c
    valu [Int32
5, Int32
a, Int32
b] = (Dom' Term Type -> Abs Type -> Term)
-> Arrows
     (Constant Int32 (Domains (Dom' Term Type -> Abs Type -> Term)))
     (R (CoDomain (Dom' Term Type -> Abs Type -> 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' Term Type -> Abs Type -> Term
Pi    Int32
a Int32
b
    valu [Int32
6, Int32
a, Int32
b] = (MetaId -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (MetaId -> Elims -> Term)))
     (R (CoDomain (MetaId -> Elims -> 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 MetaId -> Elims -> Term
MetaV Int32
a Int32
b
    valu [Int32
7, Int32
a]    = (Sort' Term -> Term)
-> Arrows
     (Constant Int32 (Domains (Sort' Term -> Term)))
     (R (CoDomain (Sort' Term -> 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)
-> Arrows
     (Constant Int32 (Domains (Term -> Term)))
     (R (CoDomain (Term -> 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)
-> Arrows
     (Constant Int32 (Domains (Level -> Term)))
     (R (CoDomain (Level -> 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 [Int32
10, Int32
a, Int32
b] = (ArgName -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (ArgName -> Elims -> Term)))
     (R (CoDomain (ArgName -> Elims -> 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 ArgName -> Elims -> Term
Dummy Int32
a Int32
b
    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)
-> Arrows
     (Domains (Integer -> [PlusLevel' Term] -> Level)) (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)
-> Arrows (Domains (Integer -> Term -> 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 -> 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 a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ IsFibrant
IsStrict  = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1

  value :: Int32 -> R IsFibrant
value Int32
0 = IsFibrant -> R IsFibrant
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IsFibrant
IsFibrant
  value Int32
1 = IsFibrant -> R IsFibrant
forall a. a -> ExceptT TypeError (StateT St IO) a
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)
-> Arrows (Domains (Level -> 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
0 Level -> Sort' Term
forall t. Level' t -> Sort' t
Type Level
a
  icod_ (Prop  Level
a  ) = Int32
-> (Level -> Sort' Term)
-> Arrows (Domains (Level -> 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
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)
-> Arrows (Domains (IsFibrant -> Integer -> 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
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)
-> Arrows
     (Domains
        (Dom' Term Term -> Sort' Term -> Abs (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
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)
-> Arrows
     (Domains (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)
-> Arrows (Domains (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_ (DefS QName
a Elims
b)   = Int32
-> (QName -> Elims -> Sort' Term)
-> Arrows (Domains (QName -> Elims -> 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 QName -> Elims -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
a Elims
b
  icod_ (SSet  Level
a  ) = Int32
-> (Level -> Sort' Term)
-> Arrows (Domains (Level -> 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
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_ Sort' Term
IntervalUniv = 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
10 Sort' Any
forall t. Sort' t
IntervalUniv
  icod_ (MetaS MetaId
a Elims
b)  = Int32
-> (MetaId -> Elims -> Sort' Term)
-> Arrows (Domains (MetaId -> Elims -> 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
11 MetaId -> Elims -> Sort' Term
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
a Elims
b
  icod_ (DummyS ArgName
s)   = Int32
-> (ArgName -> Sort' Any)
-> Arrows (Domains (ArgName -> 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
12 ArgName -> Sort' Any
forall t. ArgName -> Sort' t
DummyS ArgName
s

  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)
-> Arrows
     (Constant Int32 (Domains (Level' t -> Sort' t)))
     (R (CoDomain (Level' t -> 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)
-> Arrows
     (Constant Int32 (Domains (Level' t -> Sort' t)))
     (R (CoDomain (Level' t -> 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)
-> Arrows
     (Constant Int32 (Domains (IsFibrant -> Integer -> Sort' t)))
     (R (CoDomain (IsFibrant -> Integer -> 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)
-> Arrows
     (Constant
        Int32 (Domains (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)))
     (R (CoDomain (Dom' t t -> Sort' t -> Abs (Sort' t) -> 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)
-> Arrows
     (Constant Int32 (Domains (Sort' t -> Sort' t -> Sort' t)))
     (R (CoDomain (Sort' t -> Sort' t -> 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)
-> Arrows
     (Constant Int32 (Domains (Sort' t -> Sort' t)))
     (R (CoDomain (Sort' t -> 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)
-> Arrows
     (Constant Int32 (Domains (QName -> [Elim' t] -> Sort' t)))
     (R (CoDomain (QName -> [Elim' t] -> 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)
-> Arrows
     (Constant Int32 (Domains (Level' t -> Sort' t)))
     (R (CoDomain (Level' t -> 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 [Int32
10]      = 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
IntervalUniv
    valu [Int32
11, Int32
a, Int32
b] = (MetaId -> [Elim' t] -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (MetaId -> [Elim' t] -> Sort' t)))
     (R (CoDomain (MetaId -> [Elim' t] -> 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 MetaId -> [Elim' t] -> Sort' t
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS Int32
a Int32
b
    valu [Int32
12, Int32
s]   = (ArgName -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (ArgName -> Sort' t)))
     (R (CoDomain (ArgName -> 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 ArgName -> Sort' t
forall t. ArgName -> Sort' t
DummyS Int32
s
    valu Node
_         = R (Sort' t)
forall a. R a
malformed

instance EmbPrj DisplayForm where
  icod_ :: DisplayForm -> S Int32
icod_ (Display Int
a Elims
b DisplayTerm
c) = (Int -> Elims -> DisplayTerm -> DisplayForm)
-> Arrows
     (Domains (Int -> Elims -> DisplayTerm -> DisplayForm)) (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 -> Elims -> DisplayTerm -> DisplayForm
Display Int
a Elims
b DisplayTerm
c

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

instance EmbPrj a => EmbPrj (Open a) where
  icod_ :: Open a -> S Int32
icod_ (OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d) = (CheckpointId
 -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a)
-> Arrows
     (Domains
        (CheckpointId
         -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open 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 a b.
(a -> b)
-> ExceptT TypeError (StateT St IO) a
-> ExceptT TypeError (StateT St IO) b
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)
-> Arrows (Domains (Term -> 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' Term -> DisplayTerm
DTerm Term
a
  icod_ (DDot     Term
a  )   = Int32
-> (Term -> DisplayTerm)
-> Arrows (Domains (Term -> 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
1 Term -> DisplayTerm
DDot Term
a
  icod_ (DCon     ConHead
a ConInfo
b [Arg DisplayTerm]
c) = Int32
-> (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> Arrows
     (Domains (ConHead -> ConInfo -> [Arg DisplayTerm] -> 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)
-> Arrows
     (Domains (QName -> [Elim' DisplayTerm] -> 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 Elims
c) = Int32
-> (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> Arrows
     (Domains (DisplayTerm -> [DisplayTerm] -> Elims -> 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
4 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
a [DisplayTerm]
b Elims
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)
-> Arrows
     (Constant Int32 (Domains (Term -> DisplayTerm)))
     (R (CoDomain (Term -> 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)
-> Arrows
     (Constant Int32 (Domains (Term -> DisplayTerm)))
     (R (CoDomain (Term -> 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)
-> Arrows
     (Constant
        Int32
        (Domains (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)))
     (R (CoDomain
           (ConHead -> ConInfo -> [Arg DisplayTerm] -> 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)
-> Arrows
     (Constant
        Int32 (Domains (QName -> [Elim' DisplayTerm] -> DisplayTerm)))
     (R (CoDomain (QName -> [Elim' DisplayTerm] -> 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] -> Elims -> DisplayTerm)
-> Arrows
     (Constant
        Int32
        (Domains (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)))
     (R (CoDomain
           (DisplayTerm -> [DisplayTerm] -> Elims -> 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] -> Elims -> 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 a b.
(a -> b)
-> ExceptT TypeError (StateT St IO) a
-> ExceptT TypeError (StateT St IO) b
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)
-> Arrows
     (Domains (Maybe QName -> Maybe QName -> CompKit)) (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)
-> Arrows
     (Domains
        (ArgInfo
         -> QName
         -> Type
         -> [Polarity]
         -> [Occurrence]
         -> NumGeneralizableArgs
         -> [Maybe Name]
         -> [LocalDisplayForm]
         -> MutualId
         -> CompiledRepresentation
         -> Maybe QName
         -> Bool
         -> Set QName
         -> Bool
         -> Bool
         -> Bool
         -> Blocked_
         -> Language
         -> Defn
         -> Definition))
     (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' Term
a)      = Int32
-> (Elim' Term -> NotBlocked)
-> Arrows (Domains (Elim' Term -> NotBlocked)) (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' Term -> NotBlocked
forall t. Elim' t -> NotBlocked' t
StuckOn Elim' Term
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_ (MissingClauses QName
a) = Int32
-> (QName -> NotBlocked' Any)
-> Arrows (Domains (QName -> 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 QName -> NotBlocked' Any
forall t. QName -> NotBlocked' t
MissingClauses QName
a

  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 -> ExceptT TypeError (StateT St IO) (NotBlocked' t)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (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)
-> Arrows
     (Constant Int32 (Domains (Elim' t -> NotBlocked' t)))
     (R (CoDomain (Elim' t -> 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, Int32
a] = (QName -> NotBlocked' t)
-> Arrows
     (Constant Int32 (Domains (QName -> NotBlocked' t)))
     (R (CoDomain (QName -> 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 QName -> NotBlocked' t
forall t. QName -> NotBlocked' t
MissingClauses Int32
a
    valu Node
_      = ExceptT TypeError (StateT St IO) (NotBlocked' t)
Arrows
  (Constant Int32 (Domains (NotBlocked' t)))
  (R (CoDomain (NotBlocked' t)))
forall a. R a
malformed

instance EmbPrj Blocked_ where
  icod_ :: Blocked_ -> S Int32
icod_ (NotBlocked NotBlocked
a ()
b) = (NotBlocked -> () -> Blocked_)
-> Arrows (Domains (NotBlocked -> () -> Blocked_)) (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)
-> Arrows (Domains (Int -> [Arg Int] -> 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 Int -> [Arg Int] -> NLPat
PVar Int
a [Arg Int]
b
  icod_ (PDef QName
a PElims
b)      = Int32
-> (QName -> PElims -> NLPat)
-> Arrows (Domains (QName -> PElims -> 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 QName -> PElims -> NLPat
PDef QName
a PElims
b
  icod_ (PLam ArgInfo
a Abs NLPat
b)      = Int32
-> (ArgInfo -> Abs NLPat -> NLPat)
-> Arrows (Domains (ArgInfo -> Abs NLPat -> 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)
-> Arrows (Domains (Dom NLPType -> Abs NLPType -> 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
3 Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
a Abs NLPType
b
  icod_ (PSort NLPSort
a)       = Int32
-> (NLPSort -> NLPat)
-> Arrows (Domains (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
4 NLPSort -> NLPat
PSort NLPSort
a
  icod_ (PBoundVar Int
a PElims
b) = Int32
-> (Int -> PElims -> NLPat)
-> Arrows (Domains (Int -> PElims -> 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
5 Int -> PElims -> NLPat
PBoundVar Int
a PElims
b
  icod_ (PTerm Term
a)       = Int32
-> (Term -> NLPat) -> Arrows (Domains (Term -> 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
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)
-> Arrows
     (Constant Int32 (Domains (Int -> [Arg Int] -> NLPat)))
     (R (CoDomain (Int -> [Arg Int] -> 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)
-> Arrows
     (Constant Int32 (Domains (QName -> PElims -> NLPat)))
     (R (CoDomain (QName -> PElims -> 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)
-> Arrows
     (Constant Int32 (Domains (ArgInfo -> Abs NLPat -> NLPat)))
     (R (CoDomain (ArgInfo -> Abs NLPat -> 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)
-> Arrows
     (Constant Int32 (Domains (Dom NLPType -> Abs NLPType -> NLPat)))
     (R (CoDomain (Dom NLPType -> Abs NLPType -> 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)
-> Arrows
     (Constant Int32 (Domains (NLPSort -> NLPat)))
     (R (CoDomain (NLPSort -> 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)
-> Arrows
     (Constant Int32 (Domains (Int -> PElims -> NLPat)))
     (R (CoDomain (Int -> PElims -> 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)
-> Arrows
     (Constant Int32 (Domains (Term -> NLPat)))
     (R (CoDomain (Term -> 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)
-> Arrows (Domains (NLPSort -> NLPat -> NLPType)) (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)
-> Arrows (Domains (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
0 NLPat -> NLPSort
PType NLPat
a
  icod_ (PProp NLPat
a)   = Int32
-> (NLPat -> NLPSort)
-> Arrows (Domains (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
1 NLPat -> NLPSort
PProp NLPat
a
  icod_ (PInf IsFibrant
f Integer
a)  = Int32
-> (IsFibrant -> Integer -> NLPSort)
-> Arrows (Domains (IsFibrant -> Integer -> 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
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
PLockUniv
  icod_ NLPSort
PIntervalUniv = 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
5 NLPSort
PIntervalUniv
  icod_ (PSSet NLPat
a)   = Int32
-> (NLPat -> NLPSort)
-> Arrows (Domains (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
6 NLPat -> NLPSort
PSSet NLPat
a

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

  value :: Int32 -> R Polarity
value Int32
0 = Polarity -> R Polarity
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Covariant
  value Int32
1 = Polarity -> R Polarity
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Contravariant
  value Int32
2 = Polarity -> R Polarity
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant
  value Int32
3 = Polarity -> R Polarity
forall a. a -> ExceptT TypeError (StateT St IO) a
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 a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ IsForced
NotForced = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1

  value :: Int32 -> R IsForced
value Int32
0 = IsForced -> R IsForced
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return IsForced
Forced
  value Int32
1 = IsForced -> R IsForced
forall a. a -> ExceptT TypeError (StateT St IO) a
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)
-> Arrows (Domains (Int -> 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' 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
-> Arrows
     (Constant Int32 (Domains NumGeneralizableArgs))
     (R (CoDomain 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)
-> Arrows
     (Constant Int32 (Domains (Int -> NumGeneralizableArgs)))
     (R (CoDomain (Int -> 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
Arrows
  (Constant Int32 (Domains NumGeneralizableArgs))
  (R (CoDomain NumGeneralizableArgs))
forall a. R a
malformed

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

  value :: Int32 -> R DoGeneralize
value Int32
0 = DoGeneralize -> R DoGeneralize
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
YesGeneralizeVar
  value Int32
1 = DoGeneralize -> R DoGeneralize
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
YesGeneralizeMeta
  value Int32
2 = DoGeneralize -> R DoGeneralize
forall a. a -> ExceptT TypeError (StateT St IO) a
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 a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
  icod_ Occurrence
Mixed     = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
  icod_ Occurrence
Unused    = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
  icod_ Occurrence
GuardPos  = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
  icod_ Occurrence
JustPos   = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
4
  icod_ Occurrence
JustNeg   = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
5

  value :: Int32 -> R Occurrence
value Int32
0 = Occurrence -> R Occurrence
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
StrictPos
  value Int32
1 = Occurrence -> R Occurrence
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Mixed
  value Int32
2 = Occurrence -> R Occurrence
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Unused
  value Int32
3 = Occurrence -> R Occurrence
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
GuardPos
  value Int32
4 = Occurrence -> R Occurrence
forall a. a -> ExceptT TypeError (StateT St IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
JustPos
  value Int32
5 = Occurrence -> R Occurrence
forall a. a -> ExceptT TypeError (StateT St IO) a
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)
-> Arrows (Domains (HasEta -> EtaEquality)) (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)
-> Arrows (Domains (HasEta -> EtaEquality)) (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)
-> Arrows
     (Constant Int32 (Domains (HasEta -> EtaEquality)))
     (R (CoDomain (HasEta -> 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)
-> Arrows
     (Constant Int32 (Domains (HasEta -> EtaEquality)))
     (R (CoDomain (HasEta -> 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 ProjectionLikenessMissing

instance EmbPrj Defn where
  icod_ :: Defn -> S Int32
icod_ (Axiom       Bool
a)                                 = Int32
-> (Bool -> Defn) -> Arrows (Domains (Bool -> 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
0 Bool -> Defn
Axiom Bool
a
  icod_ (Function    [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t [Clause]
u FunctionInverse
c Maybe [QName]
d IsAbstract
e Delayed
f Either ProjectionLikenessMissing Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l)     = Int32
-> ([Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> [Clause]
    -> FunctionInverse
    -> Maybe [QName]
    -> IsAbstract
    -> Delayed
    -> Either ProjectionLikenessMissing Projection
    -> Set FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Maybe QName
    -> Defn)
-> Arrows
     (Domains
        ([Clause]
         -> Maybe CompiledClauses
         -> Maybe SplitTree
         -> [Clause]
         -> FunctionInverse
         -> Maybe [QName]
         -> IsAbstract
         -> Delayed
         -> Either ProjectionLikenessMissing Projection
         -> Set FunctionFlag
         -> Maybe Bool
         -> Maybe ExtLamInfo
         -> Maybe QName
         -> Maybe QName
         -> 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
1 (\ [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Delayed
-> Either ProjectionLikenessMissing Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t) [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s [Clause]
u FunctionInverse
c Maybe [QName]
d IsAbstract
e Delayed
f Either ProjectionLikenessMissing Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l
  icod_ (Datatype    Int
a Int
b Maybe Clause
c [QName]
d Sort' Term
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j)               = Int32
-> (Int
    -> Int
    -> Maybe Clause
    -> [QName]
    -> Sort' Term
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Maybe QName
    -> Maybe QName
    -> Defn)
-> Arrows
     (Domains
        (Int
         -> Int
         -> Maybe Clause
         -> [QName]
         -> Sort' Term
         -> Maybe [QName]
         -> IsAbstract
         -> [QName]
         -> Maybe QName
         -> Maybe QName
         -> 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
2 Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort' Term
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j
  icod_ (Record      Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m)         = Int32
-> (Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> Maybe Bool
    -> IsAbstract
    -> CompKit
    -> Defn)
-> Arrows
     (Domains
        (Int
         -> Maybe Clause
         -> ConHead
         -> Bool
         -> [Dom QName]
         -> Telescope
         -> Maybe [QName]
         -> EtaEquality
         -> PatternOrCopattern
         -> Maybe Induction
         -> Maybe Bool
         -> IsAbstract
         -> CompKit
         -> 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
3 Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> Maybe Bool
-> IsAbstract
-> CompKit
-> Defn
Record Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m
  icod_ (Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e Induction
f CompKit
g Maybe [QName]
h [IsForced]
i Maybe [Bool]
j)               = Int32
-> (Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn)
-> Arrows
     (Domains
        (Int
         -> Int
         -> ConHead
         -> QName
         -> IsAbstract
         -> Induction
         -> CompKit
         -> Maybe [QName]
         -> [IsForced]
         -> Maybe [Bool]
         -> 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
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)
-> Arrows
     (Domains
        (IsAbstract
         -> ArgName
         -> [Clause]
         -> FunctionInverse
         -> Maybe CompiledClauses
         -> 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
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)
-> Arrows (Domains (ArgName -> Sort' Term -> 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
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)
-> Arrows
     (Constant Int32 (Domains (Bool -> Defn)))
     (R (CoDomain (Bool -> 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
u, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l] = ([Clause]
 -> Maybe CompiledClauses
 -> Maybe SplitTree
 -> [Clause]
 -> FunctionInverse
 -> Maybe [QName]
 -> IsAbstract
 -> Delayed
 -> Either ProjectionLikenessMissing Projection
 -> Set FunctionFlag
 -> Maybe Bool
 -> Maybe ExtLamInfo
 -> Maybe QName
 -> Maybe QName
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           ([Clause]
            -> Maybe CompiledClauses
            -> Maybe SplitTree
            -> [Clause]
            -> FunctionInverse
            -> Maybe [QName]
            -> IsAbstract
            -> Delayed
            -> Either ProjectionLikenessMissing Projection
            -> Set FunctionFlag
            -> Maybe Bool
            -> Maybe ExtLamInfo
            -> Maybe QName
            -> Maybe QName
            -> Defn)))
     (R (CoDomain
           ([Clause]
            -> Maybe CompiledClauses
            -> Maybe SplitTree
            -> [Clause]
            -> FunctionInverse
            -> Maybe [QName]
            -> IsAbstract
            -> Delayed
            -> Either ProjectionLikenessMissing Projection
            -> Set FunctionFlag
            -> Maybe Bool
            -> Maybe ExtLamInfo
            -> Maybe QName
            -> Maybe QName
            -> 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
-> Either ProjectionLikenessMissing Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
forall a. Maybe a
Nothing) Int32
a Int32
b Int32
s Int32
u Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l
    valu [Int32
2, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j]             = (Int
 -> Int
 -> Maybe Clause
 -> [QName]
 -> Sort' Term
 -> Maybe [QName]
 -> IsAbstract
 -> [QName]
 -> Maybe QName
 -> Maybe QName
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (Int
            -> Int
            -> Maybe Clause
            -> [QName]
            -> Sort' Term
            -> Maybe [QName]
            -> IsAbstract
            -> [QName]
            -> Maybe QName
            -> Maybe QName
            -> Defn)))
     (R (CoDomain
           (Int
            -> Int
            -> Maybe Clause
            -> [QName]
            -> Sort' Term
            -> Maybe [QName]
            -> IsAbstract
            -> [QName]
            -> Maybe QName
            -> Maybe QName
            -> 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]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j
    valu [Int32
3, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l, Int32
m]    = (Int
 -> Maybe Clause
 -> ConHead
 -> Bool
 -> [Dom QName]
 -> Telescope
 -> Maybe [QName]
 -> EtaEquality
 -> PatternOrCopattern
 -> Maybe Induction
 -> Maybe Bool
 -> IsAbstract
 -> CompKit
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (Int
            -> Maybe Clause
            -> ConHead
            -> Bool
            -> [Dom QName]
            -> Telescope
            -> Maybe [QName]
            -> EtaEquality
            -> PatternOrCopattern
            -> Maybe Induction
            -> Maybe Bool
            -> IsAbstract
            -> CompKit
            -> Defn)))
     (R (CoDomain
           (Int
            -> Maybe Clause
            -> ConHead
            -> Bool
            -> [Dom QName]
            -> Telescope
            -> Maybe [QName]
            -> EtaEquality
            -> PatternOrCopattern
            -> Maybe Induction
            -> Maybe Bool
            -> IsAbstract
            -> CompKit
            -> 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
-> Maybe Bool
-> IsAbstract
-> CompKit
-> Defn
Record   Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l Int32
m
    valu [Int32
4, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j]             = (Int
 -> Int
 -> ConHead
 -> QName
 -> IsAbstract
 -> Induction
 -> CompKit
 -> Maybe [QName]
 -> [IsForced]
 -> Maybe [Bool]
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (Int
            -> Int
            -> ConHead
            -> QName
            -> IsAbstract
            -> Induction
            -> CompKit
            -> Maybe [QName]
            -> [IsForced]
            -> Maybe [Bool]
            -> Defn)))
     (R (CoDomain
           (Int
            -> Int
            -> ConHead
            -> QName
            -> IsAbstract
            -> Induction
            -> CompKit
            -> Maybe [QName]
            -> [IsForced]
            -> Maybe [Bool]
            -> 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)
-> Arrows
     (Constant
        Int32
        (Domains
           (IsAbstract
            -> ArgName
            -> [Clause]
            -> FunctionInverse
            -> Maybe CompiledClauses
            -> Defn)))
     (R (CoDomain
           (IsAbstract
            -> ArgName
            -> [Clause]
            -> FunctionInverse
            -> Maybe CompiledClauses
            -> 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)
-> Arrows
     (Constant Int32 (Domains (ArgName -> Sort' Term -> Defn)))
     (R (CoDomain (ArgName -> Sort' Term -> 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]
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain 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
Arrows
  (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
forall a. R a
malformed

instance EmbPrj SplitTag where
  icod_ :: SplitTag -> S Int32
icod_ (SplitCon QName
c)  = Int32
-> (QName -> SplitTag)
-> Arrows (Domains (QName -> SplitTag)) (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)
-> Arrows (Domains (Literal -> SplitTag)) (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
-> Arrows
     (Constant Int32 (Domains SplitTag)) (R (CoDomain 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)
-> Arrows
     (Constant Int32 (Domains (QName -> SplitTag)))
     (R (CoDomain (QName -> 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)
-> Arrows
     (Constant Int32 (Domains (Literal -> SplitTag)))
     (R (CoDomain (Literal -> 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
Arrows (Constant Int32 (Domains SplitTag)) (R (CoDomain 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)
-> Arrows (Domains (Int -> SplitTree' 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' 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)
-> Arrows
     (Domains (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' 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)
-> Arrows
     (Constant Int32 (Domains (Int -> SplitTree' a)))
     (R (CoDomain (Int -> 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)
-> Arrows
     (Constant
        Int32
        (Domains (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)))
     (R (CoDomain
           (Arg Int -> LazySplit -> SplitTrees' a -> 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]
-> Arrows
     (Constant Int32 (Domains FunctionFlag)) (R (CoDomain 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
Arrows
  (Constant Int32 (Domains FunctionFlag)) (R (CoDomain 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)
-> Arrows (Domains (Int -> a -> WithArity 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)
-> Arrows
     (Domains
        (Bool
         -> Map QName (WithArity a)
         -> Maybe (ConHead, WithArity a)
         -> Map Literal a
         -> Maybe a
         -> Maybe Bool
         -> Bool
         -> Case 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' 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)
-> Arrows
     (Domains ([Arg ArgName] -> CompiledClauses' 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' [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)
-> Arrows
     (Domains ([Arg ArgName] -> Term -> CompiledClauses)) (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)
-> Arrows
     (Domains (Arg Int -> Case CompiledClauses -> 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)
-> Arrows
     (Constant Int32 (Domains ([Arg ArgName] -> CompiledClauses' a)))
     (R (CoDomain ([Arg ArgName] -> 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)
-> Arrows
     (Constant
        Int32 (Domains ([Arg ArgName] -> a -> CompiledClauses' a)))
     (R (CoDomain ([Arg ArgName] -> a -> 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)
-> Arrows
     (Constant
        Int32
        (Domains
           (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)))
     (R (CoDomain
           (Arg Int -> Case (CompiledClauses' a) -> 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)
-> Arrows
     (Domains (InversionMap a -> FunctionInverse' 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], Typeable c) =>
Node -> ExceptT TypeError (StateT St IO) (FunctionInverse' c)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (FunctionInverse' c)))
     (R (CoDomain (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)
-> Arrows
     (Constant Int32 (Domains (InversionMap c -> FunctionInverse' c)))
     (R (CoDomain (InversionMap c -> 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
_   = ExceptT TypeError (StateT St IO) (FunctionInverse' c)
Arrows
  (Constant Int32 (Domains (FunctionInverse' c)))
  (R (CoDomain (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)
-> Arrows (Domains (QName -> 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
2 QName -> TermHead
ConsHead QName
a
  icod_ (VarHead Int
a)  = Int32
-> (Int -> TermHead)
-> Arrows (Domains (Int -> 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
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
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain 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)
-> Arrows
     (Constant Int32 (Domains (QName -> TermHead)))
     (R (CoDomain (QName -> 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)
-> Arrows
     (Constant Int32 (Domains (Int -> TermHead)))
     (R (CoDomain (Int -> 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
Arrows (Constant Int32 (Domains TermHead)) (R (CoDomain 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 Maybe ModuleName
l) = (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Bool
 -> Maybe Bool
 -> Maybe Bool
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Maybe ModuleName
 -> Clause)
-> Arrows
     (Domains
        (Range
         -> Range
         -> Telescope
         -> NAPs
         -> Maybe Term
         -> Maybe (Arg Type)
         -> Bool
         -> Maybe Bool
         -> Maybe Bool
         -> Maybe Bool
         -> ExpandedEllipsis
         -> Maybe ModuleName
         -> Clause))
     (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
-> Maybe ModuleName
-> Clause
Clause Range
a Range
b Telescope
c NAPs
d Maybe Term
e Maybe (Arg Type)
f Bool
g Maybe Bool
h Maybe Bool
i Maybe Bool
j ExpandedEllipsis
k Maybe ModuleName
l

  value :: Int32 -> R Clause
value = (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Bool
 -> Maybe Bool
 -> Maybe Bool
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Maybe ModuleName
 -> Clause)
-> Int32
-> R (CoDomain
        (Range
         -> Range
         -> Telescope
         -> NAPs
         -> Maybe Term
         -> Maybe (Arg Type)
         -> Bool
         -> Maybe Bool
         -> Maybe Bool
         -> Maybe Bool
         -> ExpandedEllipsis
         -> Maybe ModuleName
         -> 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
-> Maybe ModuleName
-> Clause
Clause

instance EmbPrj I.ConPatternInfo where
  icod_ :: ConPatternInfo -> S Int32
icod_ (ConPatternInfo PatternInfo
a Bool
b Bool
c Maybe (Arg Type)
d Bool
e) = (PatternInfo
 -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> Arrows
     (Domains
        (PatternInfo
         -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo))
     (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)
-> Arrows (Domains (ArgName -> Int -> DBPatVar)) (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)
-> Arrows (Domains (PatOrigin -> [Name] -> PatternInfo)) (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)
-> Arrows (Domains (Name -> 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
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
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain 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)
-> Arrows
     (Constant Int32 (Domains (Name -> PatOrigin)))
     (R (CoDomain (Name -> 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
Arrows
  (Constant Int32 (Domains PatOrigin)) (R (CoDomain 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)
-> Arrows (Domains (PatternInfo -> a -> 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
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)
-> Arrows
     (Domains
        (ConHead
         -> ConPatternInfo -> [NamedArg (Pattern' a)] -> 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)
-> Arrows
     (Domains (PatternInfo -> Literal -> Pattern' 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 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)
-> Arrows (Domains (PatternInfo -> Term -> Pattern' 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 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)
-> Arrows (Domains (ProjOrigin -> QName -> Pattern' 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
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)
-> Arrows
     (Domains (PatternInfo -> Term -> Term -> a -> 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
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)
-> Arrows
     (Domains
        (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> 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)
-> Arrows
     (Constant Int32 (Domains (PatternInfo -> x -> Pattern' x)))
     (R (CoDomain (PatternInfo -> x -> 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)
-> Arrows
     (Constant
        Int32
        (Domains
           (ConHead
            -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)))
     (R (CoDomain
           (ConHead
            -> ConPatternInfo -> [NamedArg (Pattern' x)] -> 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)
-> Arrows
     (Constant Int32 (Domains (PatternInfo -> Literal -> Pattern' x)))
     (R (CoDomain (PatternInfo -> Literal -> 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)
-> Arrows
     (Constant Int32 (Domains (PatternInfo -> Term -> Pattern' x)))
     (R (CoDomain (PatternInfo -> Term -> 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)
-> Arrows
     (Constant Int32 (Domains (ProjOrigin -> QName -> Pattern' x)))
     (R (CoDomain (ProjOrigin -> QName -> 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)
-> Arrows
     (Constant
        Int32 (Domains (PatternInfo -> Term -> Term -> x -> Pattern' x)))
     (R (CoDomain (PatternInfo -> Term -> Term -> x -> 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)
-> Arrows
     (Constant
        Int32
        (Domains
           (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)))
     (R (CoDomain
           (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> 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) -> Arrows (Domains (a -> Builtin 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)
-> Arrows (Domains (Term -> Builtin 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 Term -> Builtin Any
forall pf. Term -> Builtin pf
Builtin Term
a
  icod_ (BuiltinRewriteRelations Set QName
a) = Int32
-> (Set QName -> Builtin Any)
-> Arrows (Domains (Set QName -> Builtin 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 Set QName -> Builtin Any
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
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)
-> Arrows
     (Constant Int32 (Domains (pf -> Builtin pf)))
     (R (CoDomain (pf -> 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)
-> Arrows
     (Constant Int32 (Domains (Term -> Builtin pf)))
     (R (CoDomain (Term -> 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 [Int32
2, Int32
a] = (Set QName -> Builtin pf)
-> Arrows
     (Constant Int32 (Domains (Set QName -> Builtin pf)))
     (R (CoDomain (Set QName -> 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 Set QName -> Builtin pf
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations 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)         = (Impossible -> Substitution' Any)
-> Arrows (Domains (Impossible -> 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' Impossible -> Substitution' Any
forall a. Impossible -> Substitution' a
EmptyS Impossible
a
  icod_ (a
a :# Substitution' a
b)           = (a -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (a -> Substitution' a -> Substitution' 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 -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) a
a Substitution' a
b
  icod_ (Strengthen Impossible
a Int
b Substitution' a
c) = Int32
-> (Impossible -> Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (Impossible -> Int -> Substitution' 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
0 Impossible -> Int -> Substitution' a -> Substitution' a
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
a Int
b Substitution' a
c
  icod_ (Wk Int
a Substitution' a
b)           = Int32
-> (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (Int -> Substitution' 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
1 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)
-> Arrows
     (Domains (Int -> Substitution' 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 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 -> ExceptT TypeError (StateT St IO) (Substitution' a)
valu where
    valu :: Node
-> Arrows
     (Constant Int32 (Domains (Substitution' a)))
     (R (CoDomain (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
a]          = (Impossible -> Substitution' a)
-> Arrows
     (Constant Int32 (Domains (Impossible -> Substitution' a)))
     (R (CoDomain (Impossible -> 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
a, Int32
b]       = (a -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32 (Domains (a -> Substitution' a -> Substitution' a)))
     (R (CoDomain (a -> Substitution' a -> 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
0, Int32
a, Int32
b, Int32
c] = (Impossible -> Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32
        (Domains
           (Impossible -> Int -> Substitution' a -> Substitution' a)))
     (R (CoDomain
           (Impossible -> Int -> Substitution' a -> 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 -> Int -> Substitution' a -> Substitution' a
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Int32
a Int32
b Int32
c
    valu [Int32
1, Int32
a, Int32
b]    = (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32 (Domains (Int -> Substitution' a -> Substitution' a)))
     (R (CoDomain (Int -> Substitution' a -> 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
2, Int32
a, Int32
b]    = (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32 (Domains (Int -> Substitution' a -> Substitution' a)))
     (R (CoDomain (Int -> Substitution' a -> 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
_            = ExceptT TypeError (StateT St IO) (Substitution' a)
Arrows
  (Constant Int32 (Domains (Substitution' a)))
  (R (CoDomain (Substitution' a)))
forall a. R a
malformed

instance EmbPrj Instantiation where
  icod_ :: Instantiation -> S Int32
icod_ (Instantiation [Arg ArgName]
a Term
b) = ([Arg ArgName] -> Term -> Instantiation)
-> Arrows
     (Domains ([Arg ArgName] -> Term -> Instantiation)) (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 -> Instantiation
Instantiation [Arg ArgName]
a Term
b
  value :: Int32 -> R Instantiation
value = ([Arg ArgName] -> Term -> Instantiation)
-> Int32 -> R (CoDomain ([Arg ArgName] -> Term -> Instantiation))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN [Arg ArgName] -> Term -> Instantiation
Instantiation

instance EmbPrj Comparison where
  icod_ :: Comparison -> S Int32
icod_ Comparison
CmpEq  = Comparison -> Arrows (Domains Comparison) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Comparison
CmpEq
  icod_ Comparison
CmpLeq = Int32 -> Comparison -> Arrows (Domains Comparison) (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 Comparison
CmpLeq

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

instance EmbPrj a => EmbPrj (Judgement a) where
  icod_ :: Judgement a -> S Int32
icod_ (HasType a
a Comparison
b Type
c) = (a -> Comparison -> Type -> Judgement a)
-> Arrows
     (Domains (a -> Comparison -> Type -> Judgement 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 -> Comparison -> Type -> Judgement a
forall a. a -> Comparison -> Type -> Judgement a
HasType a
a Comparison
b Type
c
  icod_ (IsSort a
a Type
b)    = (a -> Type -> Judgement a)
-> Arrows (Domains (a -> Type -> Judgement 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 -> Type -> Judgement a
forall a. a -> Type -> Judgement a
IsSort a
a Type
b

  value :: Int32 -> R (Judgement a)
value = (Node -> R (Judgement a)) -> Int32 -> R (Judgement a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Judgement a)
forall {a}. EmbPrj a => Node -> R (Judgement a)
valu
    where
    valu :: Node -> R (Judgement a)
valu [Int32
a, Int32
b, Int32
c] = (a -> Comparison -> Type -> Judgement a)
-> Arrows
     (Constant Int32 (Domains (a -> Comparison -> Type -> Judgement a)))
     (R (CoDomain (a -> Comparison -> Type -> Judgement 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 -> Comparison -> Type -> Judgement a
forall a. a -> Comparison -> Type -> Judgement a
HasType Int32
a Int32
b Int32
c
    valu [Int32
a, Int32
b]    = (a -> Type -> Judgement a)
-> Arrows
     (Constant Int32 (Domains (a -> Type -> Judgement a)))
     (R (CoDomain (a -> Type -> Judgement 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 -> Type -> Judgement a
forall a. a -> Type -> Judgement a
IsSort Int32
a Int32
b
    valu Node
_         = R (Judgement a)
forall a. R a
malformed

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