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

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

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

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

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

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

instance EmbPrj a => EmbPrj (Tele a) where
  icod_ :: Tele a -> S Int32
icod_ 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
a b :: Abs (Tele a)
b) = (a -> Abs (Tele a) -> Tele a) -> a -> Abs (Tele a) -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a Abs (Tele a)
b

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

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

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

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

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

instance EmbPrj a => EmbPrj (Elim' a) where
  icod_ :: Elim' a -> S Int32
icod_ (Apply a :: Arg a
a)      = (Arg a -> Elim' a) -> Arg a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Arg a
a
  icod_ (IApply x :: a
x y :: a
y a :: a
a) = Int32 -> (a -> a -> a -> Elim' a) -> a -> a -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
x a
y a
a
  icod_ (Proj a :: ProjOrigin
a b :: QName
b)     = Int32
-> (ProjOrigin -> QName -> Elim' Any)
-> ProjOrigin
-> QName
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 [a :: Int32
a]       = (Arg a -> Elim' a) -> Int32 -> R (Elim' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Int32
a
    valu [0,x :: Int32
x,y :: Int32
y,a :: Int32
a] = (a -> a -> a -> Elim' a) -> Int32 -> Int32 -> Int32 -> R (Elim' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply Int32
x Int32
y Int32
a
    valu [0, a :: Int32
a, b :: Int32
b] = (ProjOrigin -> QName -> Elim' a) -> Int32 -> Int32 -> R (Elim' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ProjOrigin -> QName -> Elim' a
forall a. ProjOrigin -> QName -> Elim' a
Proj Int32
a Int32
b
    valu _         = R (Elim' a)
forall a. R a
malformed

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

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

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

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

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

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

instance EmbPrj I.Term where
  icod_ :: Term -> S Int32
icod_ (Var     a :: Int
a []) = (Int -> Term) -> Int -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ a :: Int
a -> Int -> Elims -> Term
Var Int
a []) Int
a
  icod_ (Var      a :: Int
a b :: Elims
b) = Int32 -> (Int -> Elims -> Term) -> Int -> Elims -> 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 0 Int -> Elims -> Term
Var Int
a Elims
b
  icod_ (Lam      a :: ArgInfo
a b :: Abs Term
b) = Int32
-> (ArgInfo -> Abs Term -> Term) -> ArgInfo -> Abs Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 ArgInfo -> Abs Term -> Term
Lam ArgInfo
a Abs Term
b
  icod_ (Lit      a :: Literal
a  ) = Int32 -> (Literal -> Term) -> Literal -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 Literal -> Term
Lit Literal
a
  icod_ (Def      a :: QName
a b :: Elims
b) = Int32 -> (QName -> Elims -> Term) -> QName -> Elims -> 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 3 QName -> Elims -> Term
Def QName
a Elims
b
  icod_ (Con    a :: ConHead
a b :: ConInfo
b c :: Elims
c) = Int32
-> (ConHead -> ConInfo -> Elims -> Term)
-> ConHead
-> ConInfo
-> Elims
-> 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 4 ConHead -> ConInfo -> Elims -> Term
Con ConHead
a ConInfo
b Elims
c
  icod_ (Pi       a :: Dom Type
a b :: Abs Type
b) = Int32
-> (Dom Type -> Abs Type -> Term)
-> Dom Type
-> Abs Type
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 5 Dom Type -> Abs Type -> Term
Pi Dom Type
a Abs Type
b
  icod_ (Sort     a :: Sort' Term
a  ) = Int32 -> (Sort' Term -> Term) -> Sort' Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 7 Sort' Term -> Term
Sort Sort' Term
a
  icod_ (MetaV    a :: MetaId
a b :: Elims
b) = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (DontCare a :: Term
a  ) = Int32 -> (Term -> Term) -> Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 8 Term -> Term
DontCare Term
a
  icod_ (Level    a :: Level
a  ) = Int32 -> (Level -> Term) -> Level -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 9 Level -> Term
Level Level
a
  icod_ (Dummy s :: ArgName
s _)    = do
    IO () -> ReaderT Dict IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Dict IO ()) -> IO () -> ReaderT Dict IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> IO ()
putStrLn (ArgName -> IO ()) -> ArgName -> IO ()
forall a b. (a -> b) -> a -> b
$ "Dummy term in serialization: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s
    S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

instance EmbPrj PlusLevel where
  icod_ :: PlusLevel' Term -> S Int32
icod_ (Plus a :: Integer
a b :: LevelAtom' Term
b) = (Integer -> LevelAtom' Term -> PlusLevel' Term)
-> Integer -> LevelAtom' 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 -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
a LevelAtom' Term
b

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

instance EmbPrj LevelAtom where
  icod_ :: LevelAtom' Term -> S Int32
icod_ (NeutralLevel r :: NotBlocked
r a :: Term
a) = (Term -> LevelAtom' Term) -> 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' (NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
r) Term
a
  icod_ (UnreducedLevel a :: Term
a) = Int32 -> (Term -> LevelAtom' 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 1 Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel Term
a
  icod_ (MetaLevel a :: MetaId
a b :: Elims
b)    = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ BlockedLevel{}     = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R (LevelAtom' Term)
value = (Node -> R (LevelAtom' Term)) -> Int32 -> R (LevelAtom' Term)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (LevelAtom' Term)
forall t. EmbPrj t => Node -> R (LevelAtom' t)
valu where
    valu :: Node -> R (LevelAtom' t)
valu [a :: Int32
a]    = (t -> LevelAtom' t) -> Int32 -> R (LevelAtom' 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 t -> LevelAtom' t
forall t. t -> LevelAtom' t
UnreducedLevel Int32
a -- we forget that we are a NeutralLevel,
                                         -- since we do not want do (de)serialize
                                         -- the reason for neutrality
    valu [1, a :: Int32
a] = (t -> LevelAtom' t) -> Int32 -> R (LevelAtom' 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 t -> LevelAtom' t
forall t. t -> LevelAtom' t
UnreducedLevel Int32
a
    valu _      = R (LevelAtom' t)
forall a. R a
malformed

instance EmbPrj I.Sort where
  icod_ :: Sort' Term -> S Int32
icod_ (Type  a :: Level
a  ) = Int32 -> (Level -> Sort' Term) -> Level -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Level -> Sort' Term
forall t. Level' t -> Sort' t
Type Level
a
  icod_ (Prop  a :: Level
a  ) = Int32 -> (Level -> Sort' Term) -> Level -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Level -> Sort' Term
forall t. Level' t -> Sort' t
Prop Level
a
  icod_ 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 2 Sort' Any
forall t. Sort' t
SizeUniv
  icod_ Inf         = 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 3 Sort' Any
forall t. Sort' t
Inf
  icod_ (PiSort a :: Dom Type
a b :: Abs (Sort' Term)
b) = Int32
-> (Dom Type -> Abs (Sort' Term) -> Sort' Term)
-> Dom Type
-> Abs (Sort' Term)
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 4 Dom Type -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort Dom Type
a Abs (Sort' Term)
b
  icod_ (FunSort a :: Sort' Term
a b :: Sort' Term
b) = Int32
-> (Sort' Term -> Sort' Term -> Sort' Term)
-> Sort' Term
-> Sort' Term
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 5 Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' Term
a Sort' Term
b
  icod_ (UnivSort a :: Sort' Term
a) = Int32 -> (Sort' Term -> Sort' Term) -> Sort' Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 6 Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort Sort' Term
a
  icod_ (MetaS a :: MetaId
a b :: Elims
b)  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (DefS a :: QName
a b :: Elims
b)   = Int32
-> (QName -> Elims -> Sort' Term) -> QName -> Elims -> 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 7 QName -> Elims -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
a Elims
b
  icod_ (DummyS s :: ArgName
s)   = do
    IO () -> ReaderT Dict IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Dict IO ()) -> IO () -> ReaderT Dict IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> IO ()
putStrLn (ArgName -> IO ()) -> ArgName -> IO ()
forall a b. (a -> b) -> a -> b
$ "Dummy sort in serialization: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s
    S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R (Sort' Term)
value = (Node -> R (Sort' Term)) -> Int32 -> R (Sort' Term)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Sort' Term)
forall t.
(EmbPrj t, EmbPrj (Dom' t (Type'' t t)), EmbPrj (Level' t),
 EmbPrj (Sort' t)) =>
Node -> R (Sort' t)
valu where
    valu :: Node -> R (Sort' t)
valu [0, a :: Int32
a]    = (Level' t -> Sort' t) -> Int32 -> R (Sort' t)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Level' t -> Sort' t
forall t. Level' t -> Sort' t
Type  Int32
a
    valu [1, a :: Int32
a]    = (Level' t -> Sort' t) -> Int32 -> R (Sort' t)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Level' t -> Sort' t
forall t. Level' t -> Sort' t
Prop  Int32
a
    valu [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 [3]       = 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
Inf
    valu [4, a :: Int32
a, b :: Int32
b] = (Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t)
-> Int32 -> Int32 -> R (Sort' t)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort Int32
a Int32
b
    valu [5, a :: Int32
a, b :: Int32
b] = (Sort' t -> Sort' t -> Sort' t) -> Int32 -> Int32 -> R (Sort' t)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort' t -> Sort' t -> Sort' t
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Int32
a Int32
b
    valu [6, a :: Int32
a]    = (Sort' t -> Sort' t) -> Int32 -> R (Sort' t)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort' t -> Sort' t
forall t. Sort' t -> Sort' t
UnivSort Int32
a
    valu [7, a :: Int32
a, b :: Int32
b] = (QName -> [Elim' t] -> Sort' t) -> Int32 -> Int32 -> R (Sort' t)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> [Elim' t] -> Sort' t
forall t. QName -> [Elim' t] -> Sort' t
DefS Int32
a Int32
b
    valu _         = R (Sort' t)
forall a. R a
malformed

instance EmbPrj DisplayForm where
  icod_ :: DisplayForm -> S Int32
icod_ (Display a :: Int
a b :: Elims
b c :: DisplayTerm
c) = (Int -> Elims -> DisplayTerm -> DisplayForm)
-> Int -> Elims -> DisplayTerm -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> 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 a :: CheckpointId
a b :: a
b) = (CheckpointId -> a -> Open a) -> CheckpointId -> 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 -> a -> Open a
forall a. CheckpointId -> a -> Open a
OpenThing CheckpointId
a a
b

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

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

instance EmbPrj DisplayTerm where
  icod_ :: DisplayTerm -> S Int32
icod_ (DTerm    a :: Term
a  )   = (Term -> DisplayTerm) -> Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Term -> DisplayTerm
DTerm Term
a
  icod_ (DDot     a :: Term
a  )   = Int32 -> (Term -> DisplayTerm) -> Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Term -> DisplayTerm
DDot Term
a
  icod_ (DCon     a :: ConHead
a b :: ConInfo
b c :: [Arg DisplayTerm]
c) = Int32
-> (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> ConHead
-> ConInfo
-> [Arg DisplayTerm]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
a ConInfo
b [Arg DisplayTerm]
c
  icod_ (DDef     a :: QName
a b :: [Elim' DisplayTerm]
b)   = Int32
-> (QName -> [Elim' DisplayTerm] -> DisplayTerm)
-> QName
-> [Elim' DisplayTerm]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
a [Elim' DisplayTerm]
b
  icod_ (DWithApp a :: DisplayTerm
a b :: [DisplayTerm]
b c :: Elims
c) = Int32
-> (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> DisplayTerm
-> [DisplayTerm]
-> Elims
-> 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 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 [a :: Int32
a]          = (Term -> DisplayTerm) -> Int32 -> R DisplayTerm
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> DisplayTerm
DTerm Int32
a
    valu [1, a :: Int32
a]       = (Term -> DisplayTerm) -> Int32 -> R DisplayTerm
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> DisplayTerm
DDot Int32
a
    valu [2, a :: Int32
a, b :: Int32
b, c :: Int32
c] = (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> Int32 -> Int32 -> Int32 -> R DisplayTerm
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon Int32
a Int32
b Int32
c
    valu [3, a :: Int32
a, b :: Int32
b]    = (QName -> [Elim' DisplayTerm] -> DisplayTerm)
-> Int32 -> Int32 -> R DisplayTerm
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef Int32
a Int32
b
    valu [4, a :: Int32
a, b :: Int32
b, c :: Int32
c] = (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> Int32 -> Int32 -> Int32 -> R DisplayTerm
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp Int32
a Int32
b Int32
c
    valu _            = R DisplayTerm
forall a. R a
malformed

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

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

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

  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_
 -> 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_
         -> 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_
-> Defn
-> Definition
Defn

instance EmbPrj NotBlocked where
  icod_ :: NotBlocked -> S Int32
icod_ ReallyNotBlocked = NotBlocked -> Arrows (Domains NotBlocked) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NotBlocked
ReallyNotBlocked
  icod_ (StuckOn a :: Elim
a)      = Int32 -> (Elim -> NotBlocked) -> Elim -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Elim -> NotBlocked
StuckOn Elim
a
  icod_ Underapplied     = Int32 -> NotBlocked -> Arrows (Domains 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 1 NotBlocked
Underapplied
  icod_ AbsurdMatch      = Int32 -> NotBlocked -> Arrows (Domains 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 2 NotBlocked
AbsurdMatch
  icod_ MissingClauses   = Int32 -> NotBlocked -> Arrows (Domains 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 3 NotBlocked
MissingClauses

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

instance EmbPrj Blocked_ where
  icod_ :: Blocked_ -> S Int32
icod_ (NotBlocked a :: NotBlocked
a b :: ()
b) = (NotBlocked -> () -> Blocked_) -> NotBlocked -> () -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NotBlocked -> () -> Blocked_
forall t. NotBlocked -> t -> Blocked t
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. NotBlocked -> t -> Blocked t
NotBlocked

instance EmbPrj NLPat where
  icod_ :: NLPat -> S Int32
icod_ (PVar a :: Int
a b :: [Arg Int]
b)      = Int32 -> (Int -> [Arg Int] -> NLPat) -> Int -> [Arg Int] -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Int -> [Arg Int] -> NLPat
PVar Int
a [Arg Int]
b
  icod_ (PDef a :: QName
a b :: PElims
b)      = Int32 -> (QName -> PElims -> NLPat) -> QName -> PElims -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 QName -> PElims -> NLPat
PDef QName
a PElims
b
  icod_ (PLam a :: ArgInfo
a b :: Abs NLPat
b)      = Int32
-> (ArgInfo -> Abs NLPat -> NLPat)
-> ArgInfo
-> Abs NLPat
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
a Abs NLPat
b
  icod_ (PPi a :: Dom NLPType
a b :: Abs NLPType
b)       = Int32
-> (Dom NLPType -> Abs NLPType -> NLPat)
-> Dom NLPType
-> Abs NLPType
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
a Abs NLPType
b
  icod_ (PSort a :: NLPSort
a)       = Int32 -> (NLPSort -> NLPat) -> NLPSort -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 4 NLPSort -> NLPat
PSort NLPSort
a
  icod_ (PBoundVar a :: Int
a b :: PElims
b) = Int32 -> (Int -> PElims -> NLPat) -> Int -> PElims -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 5 Int -> PElims -> NLPat
PBoundVar Int
a PElims
b
  icod_ (PTerm a :: Term
a)       = Int32 -> (Term -> NLPat) -> Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 [0, a :: Int32
a, b :: Int32
b]    = (Int -> [Arg Int] -> NLPat) -> Int32 -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> [Arg Int] -> NLPat
PVar Int32
a Int32
b
    valu [1, a :: Int32
a, b :: Int32
b]    = (QName -> PElims -> NLPat) -> Int32 -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> PElims -> NLPat
PDef Int32
a Int32
b
    valu [2, a :: Int32
a, b :: Int32
b]    = (ArgInfo -> Abs NLPat -> NLPat) -> Int32 -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgInfo -> Abs NLPat -> NLPat
PLam Int32
a Int32
b
    valu [3, a :: Int32
a, b :: Int32
b]    = (Dom NLPType -> Abs NLPType -> NLPat) -> Int32 -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom NLPType -> Abs NLPType -> NLPat
PPi Int32
a Int32
b
    valu [4, a :: Int32
a]       = (NLPSort -> NLPat) -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort -> NLPat
PSort Int32
a
    valu [5, a :: Int32
a, b :: Int32
b]    = (Int -> PElims -> NLPat) -> Int32 -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> PElims -> NLPat
PBoundVar Int32
a Int32
b
    valu [6, a :: Int32
a]       = (Term -> NLPat) -> Int32 -> R NLPat
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> NLPat
PTerm Int32
a
    valu _            = R NLPat
forall a. R a
malformed

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

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

instance EmbPrj NLPSort where
  icod_ :: NLPSort -> S Int32
icod_ (PType a :: NLPat
a)   = Int32 -> (NLPat -> NLPSort) -> NLPat -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 NLPat -> NLPSort
PType NLPat
a
  icod_ (PProp a :: NLPat
a)   = Int32 -> (NLPat -> NLPSort) -> NLPat -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 NLPat -> NLPSort
PProp NLPat
a
  icod_ PInf        = 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 2 NLPSort
PInf
  icod_ 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 3 NLPSort
PSizeUniv

  value :: Int32 -> R NLPSort
value = (Node -> R NLPSort) -> Int32 -> R NLPSort
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NLPSort
valu where
    valu :: Node -> R NLPSort
valu [0, a :: Int32
a] = (NLPat -> NLPSort) -> Int32 -> R NLPSort
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PType Int32
a
    valu [1, a :: Int32
a] = (NLPat -> NLPSort) -> Int32 -> R NLPSort
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PProp Int32
a
    valu [2]    = 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
PInf
    valu [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 _      = R NLPSort
forall a. R a
malformed

instance EmbPrj RewriteRule where
  icod_ :: RewriteRule -> S Int32
icod_ (RewriteRule a :: QName
a b :: Telescope
b c :: QName
c d :: PElims
d e :: Term
e f :: Type
f) = (QName
 -> Telescope -> QName -> PElims -> Term -> Type -> RewriteRule)
-> QName -> Telescope -> QName -> PElims -> Term -> Type -> 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 -> RewriteRule
RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f

  value :: Int32 -> R RewriteRule
value = (QName
 -> Telescope -> QName -> PElims -> Term -> Type -> RewriteRule)
-> Int32
-> R (CoDomain
        (QName
         -> Telescope -> QName -> PElims -> Term -> Type -> 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 -> RewriteRule
RewriteRule

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance EmbPrj EtaEquality where
  icod_ :: EtaEquality -> S Int32
icod_ (Specified a :: HasEta
a) = Int32 -> (HasEta -> EtaEquality) -> HasEta -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 HasEta -> EtaEquality
Specified HasEta
a
  icod_ (Inferred a :: HasEta
a)  = Int32 -> (HasEta -> EtaEquality) -> HasEta -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 [0,a :: Int32
a] = (HasEta -> EtaEquality) -> Int32 -> R EtaEquality
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN HasEta -> EtaEquality
Specified Int32
a
    valu [1,a :: Int32
a] = (HasEta -> EtaEquality) -> Int32 -> R EtaEquality
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN HasEta -> EtaEquality
Inferred Int32
a
    valu _     = R EtaEquality
forall a. R a
malformed

instance EmbPrj Defn where
  icod_ :: Defn -> S Int32
icod_ Axiom                                           = 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 0 Defn
Axiom
  icod_ (Function    a :: [Clause]
a b :: Maybe CompiledClauses
b s :: Maybe SplitTree
s t :: Maybe Compiled
t (_:_) c :: FunctionInverse
c d :: Maybe [QName]
d e :: IsAbstract
e f :: Delayed
f g :: Maybe Projection
g h :: Set FunctionFlag
h i :: Maybe Bool
i j :: Maybe ExtLamInfo
j k :: Maybe QName
k)   = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (Function    a :: [Clause]
a b :: Maybe CompiledClauses
b s :: Maybe SplitTree
s t :: Maybe Compiled
t []    c :: FunctionInverse
c d :: Maybe [QName]
d e :: IsAbstract
e f :: Delayed
f g :: Maybe Projection
g h :: Set FunctionFlag
h i :: Maybe Bool
i j :: Maybe ExtLamInfo
j k :: Maybe QName
k)   =
    Int32
-> ([Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> FunctionInverse
    -> Maybe [QName]
    -> IsAbstract
    -> Delayed
    -> Maybe Projection
    -> Set FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Defn)
-> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Delayed
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 (\ a :: [Clause]
a b :: Maybe CompiledClauses
b s :: Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Delayed
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t []) [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s FunctionInverse
c Maybe [QName]
d IsAbstract
e Delayed
f Maybe Projection
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k
  icod_ (Datatype    a :: Int
a b :: Int
b c :: Maybe Clause
c d :: [QName]
d e :: Sort' Term
e f :: Maybe [QName]
f g :: IsAbstract
g h :: [QName]
h)                   = Int32
-> (Int
    -> Int
    -> Maybe Clause
    -> [QName]
    -> Sort' Term
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Defn)
-> Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Defn
Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort' Term
e Maybe [QName]
f IsAbstract
g [QName]
h
  icod_ (Record      a :: Int
a b :: Maybe Clause
b c :: ConHead
c d :: Bool
d e :: [Dom QName]
e f :: Telescope
f g :: Maybe [QName]
g h :: EtaEquality
h i :: Maybe Induction
i j :: IsAbstract
j k :: CompKit
k)             = Int32
-> (Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> Maybe Induction
    -> IsAbstract
    -> CompKit
    -> Defn)
-> Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> Maybe Induction
-> IsAbstract
-> CompKit
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> Maybe Induction
-> IsAbstract
-> CompKit
-> Defn
Record Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h Maybe Induction
i IsAbstract
j CompKit
k
  icod_ (Constructor a :: Int
a b :: Int
b c :: ConHead
c d :: QName
d e :: IsAbstract
e f :: Induction
f g :: CompKit
g h :: Maybe [QName]
h i :: [IsForced]
i j :: Maybe [Bool]
j)               = Int32
-> (Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn)
-> Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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   a :: IsAbstract
a b :: ArgName
b c :: [Clause]
c d :: FunctionInverse
d e :: Maybe CompiledClauses
e)                         = Int32
-> (IsAbstract
    -> ArgName
    -> [Clause]
    -> FunctionInverse
    -> Maybe CompiledClauses
    -> Defn)
-> IsAbstract
-> ArgName
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 5 IsAbstract
-> ArgName
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive IsAbstract
a ArgName
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e
  icod_ AbstractDefn{}                                  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ 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 6 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 [0]                                        = 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
Axiom
    valu [1, a :: Int32
a, b :: Int32
b, s :: Int32
s, c :: Int32
c, d :: Int32
d, e :: Int32
e, f :: Int32
f, g :: Int32
g, h :: Int32
h, i :: Int32
i, j :: Int32
j, k :: Int32
k]    = ([Clause]
 -> Maybe CompiledClauses
 -> Maybe SplitTree
 -> FunctionInverse
 -> Maybe [QName]
 -> IsAbstract
 -> Delayed
 -> Maybe Projection
 -> Set FunctionFlag
 -> Maybe Bool
 -> Maybe ExtLamInfo
 -> Maybe QName
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN (\ a :: [Clause]
a b :: Maybe CompiledClauses
b s :: Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Delayed
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
forall a. Maybe a
Nothing []) Int32
a Int32
b Int32
s Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k
    valu [2, a :: Int32
a, b :: Int32
b, c :: Int32
c, d :: Int32
d, e :: Int32
e, f :: Int32
f, g :: Int32
g, h :: Int32
h]                = (Int
 -> Int
 -> Maybe Clause
 -> [QName]
 -> Sort' Term
 -> Maybe [QName]
 -> IsAbstract
 -> [QName]
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Defn
Datatype Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h
    valu [3, a :: Int32
a, b :: Int32
b, c :: Int32
c, d :: Int32
d, e :: Int32
e, f :: Int32
f, g :: Int32
g, h :: Int32
h, i :: Int32
i, j :: Int32
j, k :: Int32
k]       = (Int
 -> Maybe Clause
 -> ConHead
 -> Bool
 -> [Dom QName]
 -> Telescope
 -> Maybe [QName]
 -> EtaEquality
 -> Maybe Induction
 -> IsAbstract
 -> CompKit
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> Maybe Induction
-> IsAbstract
-> CompKit
-> Defn
Record  Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k
    valu [4, a :: Int32
a, b :: Int32
b, c :: Int32
c, d :: Int32
d, e :: Int32
e, f :: Int32
f, g :: Int32
g, h :: Int32
h, i :: Int32
i, j :: Int32
j]          = (Int
 -> Int
 -> ConHead
 -> QName
 -> IsAbstract
 -> Induction
 -> CompKit
 -> Maybe [QName]
 -> [IsForced]
 -> Maybe [Bool]
 -> Defn)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Defn
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j
    valu [5, a :: Int32
a, b :: Int32
b, c :: Int32
c, d :: Int32
d, e :: Int32
e]                         = (IsAbstract
 -> ArgName
 -> [Clause]
 -> FunctionInverse
 -> Maybe CompiledClauses
 -> Defn)
-> Int32 -> Int32 -> Int32 -> Int32 -> Int32 -> R Defn
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
-> ArgName
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive   Int32
a Int32
b Int32
c Int32
d Int32
e
    valu [6]                                        = 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 _                                          = R Defn
forall a. R a
malformed

instance EmbPrj LazySplit where
  icod_ :: LazySplit -> S Int32
icod_ 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   = 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 0 LazySplit
LazySplit

  value :: Int32 -> R LazySplit
value = (Node -> R LazySplit) -> Int32 -> R LazySplit
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R LazySplit
forall a. (Eq a, Num a) => [a] -> R LazySplit
valu where
    valu :: [a] -> R LazySplit
valu []  = LazySplit
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN LazySplit
StrictSplit
    valu [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 _   = R LazySplit
forall a. R a
malformed

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

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

instance EmbPrj a => EmbPrj (SplitTree' a) where
  icod_ :: SplitTree' a -> S Int32
icod_ (SplittingDone a :: Int
a) = (Int -> SplitTree' Any) -> Int -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> SplitTree' Any
forall a. Int -> SplitTree' a
SplittingDone Int
a
  icod_ (SplitAt a :: Arg Int
a b :: LazySplit
b c :: SplitTrees' a
c)   = Int32
-> (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
-> Arg Int
-> LazySplit
-> SplitTrees' a
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 [a :: Int32
a]          = (Int -> SplitTree' a) -> Int32 -> R (SplitTree' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> SplitTree' a
forall a. Int -> SplitTree' a
SplittingDone Int32
a
    valu [0, a :: Int32
a, b :: Int32
b, c :: Int32
c] = (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
-> Int32 -> Int32 -> Int32 -> R (SplitTree' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Int32
a Int32
b Int32
c
    valu _            = R (SplitTree' a)
forall a. R a
malformed

instance EmbPrj FunctionFlag where
  icod_ :: FunctionFlag -> S Int32
icod_ 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 0 FunctionFlag
FunStatic
  icod_ 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 1 FunctionFlag
FunInline
  icod_ 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 2 FunctionFlag
FunMacro

  value :: Int32 -> R FunctionFlag
value = (Node -> R FunctionFlag) -> Int32 -> R FunctionFlag
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R FunctionFlag
forall a. (Eq a, Num a) => [a] -> R FunctionFlag
valu where
    valu :: [a] -> R FunctionFlag
valu [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 [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 [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 _   = R FunctionFlag
forall a. R a
malformed

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

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

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

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

instance EmbPrj CompiledClauses where
  icod_ :: CompiledClauses -> S Int32
icod_ Fail       = CompiledClauses' Any
-> Arrows (Domains (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' CompiledClauses' Any
forall a. CompiledClauses' a
Fail
  icod_ (Done a :: [Arg ArgName]
a b :: Term
b) = ([Arg ArgName] -> Term -> CompiledClauses)
-> [Arg ArgName] -> Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> Term -> CompiledClauses
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [Arg ArgName]
a (Term -> Term
forall a. KillRange a => KillRangeT a
P.killRange Term
b)
  icod_ (Case a :: Arg Int
a b :: Case CompiledClauses
b) = Int32
-> (Arg Int -> Case CompiledClauses -> CompiledClauses)
-> Arg Int
-> Case CompiledClauses
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 []        = CompiledClauses' a
-> Arrows
     (Constant Int32 (Domains (CompiledClauses' a)))
     (R (CoDomain (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 CompiledClauses' a
forall a. CompiledClauses' a
Fail
    valu [a :: Int32
a, b :: Int32
b]    = ([Arg ArgName] -> a -> CompiledClauses' a)
-> Int32 -> Int32 -> R (CompiledClauses' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN [Arg ArgName] -> a -> CompiledClauses' a
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done Int32
a Int32
b
    valu [2, a :: Int32
a, b :: Int32
b] = (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)
-> Int32 -> Int32 -> R (CompiledClauses' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Int32
a Int32
b
    valu _         = R (CompiledClauses' a)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (FunctionInverse' a) where
  icod_ :: FunctionInverse' a -> S Int32
icod_ 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 a :: InversionMap a
a)  = (InversionMap a -> FunctionInverse' a) -> InversionMap a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' InversionMap a -> FunctionInverse' a
forall c. InversionMap c -> FunctionInverse' c
Inverse InversionMap a
a

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

instance EmbPrj TermHead where
  icod_ :: TermHead -> S Int32
icod_ 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_ 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 1 TermHead
PiHead
  icod_ (ConsHead a :: QName
a) = Int32 -> (QName -> TermHead) -> QName -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 QName -> TermHead
ConsHead QName
a
  icod_ (VarHead a :: Int
a)  = Int32 -> (Int -> TermHead) -> Int -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 Int -> TermHead
VarHead Int
a
  icod_ 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 4 TermHead
UnknownHead

  value :: Int32 -> R TermHead
value = (Node -> R TermHead) -> Int32 -> R TermHead
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R TermHead
valu where
    valu :: Node -> R TermHead
valu []     = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
SortHead
    valu [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 [2, a :: Int32
a] = (QName -> TermHead) -> Int32 -> R TermHead
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> TermHead
ConsHead Int32
a
    valu [3, a :: Int32
a] = (Int -> TermHead) -> Int32 -> R TermHead
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> TermHead
VarHead Int32
a
    valu [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 _      = R TermHead
forall a. R a
malformed

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

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

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

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

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

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

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

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

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

  value :: Int32 -> R PatOrigin
value = (Node -> R PatOrigin) -> Int32 -> R PatOrigin
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R PatOrigin
valu where
    valu :: Node -> R PatOrigin
valu []     = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOSystem
    valu [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 [2, a :: Int32
a] = (Name -> PatOrigin) -> Int32 -> R PatOrigin
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Name -> PatOrigin
PatOVar Int32
a
    valu [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 [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 [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 [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 [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 [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 _      = R PatOrigin
forall a. R a
malformed

instance EmbPrj a => EmbPrj (I.Pattern' a) where
  icod_ :: Pattern' a -> S Int32
icod_ (VarP a :: PatternInfo
a b :: a
b  ) = Int32
-> (PatternInfo -> a -> Pattern' a) -> PatternInfo -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
a a
b
  icod_ (ConP a :: ConHead
a b :: ConPatternInfo
b c :: [NamedArg (Pattern' a)]
c) = Int32
-> (ConHead
    -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
-> ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' a)]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 a :: PatternInfo
a b :: Literal
b  ) = Int32
-> (PatternInfo -> Literal -> Pattern' Any)
-> PatternInfo
-> Literal
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 PatternInfo -> Literal -> Pattern' Any
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
a Literal
b
  icod_ (DotP a :: PatternInfo
a b :: Term
b  ) = Int32
-> (PatternInfo -> Term -> Pattern' Any)
-> PatternInfo
-> Term
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 PatternInfo -> Term -> Pattern' Any
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
a Term
b
  icod_ (ProjP a :: ProjOrigin
a b :: QName
b ) = Int32
-> (ProjOrigin -> QName -> Pattern' Any)
-> ProjOrigin
-> QName
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 4 ProjOrigin -> QName -> Pattern' Any
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
a QName
b
  icod_ (IApplyP a :: PatternInfo
a b :: Term
b c :: Term
c d :: a
d) = Int32
-> (PatternInfo -> Term -> Term -> a -> Pattern' a)
-> PatternInfo
-> Term
-> Term
-> a
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 a :: PatternInfo
a b :: QName
b c :: [NamedArg (Pattern' a)]
c) = Int32
-> (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a)
-> PatternInfo
-> QName
-> [NamedArg (Pattern' a)]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 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 [0, a :: Int32
a, b :: Int32
b] = (PatternInfo -> x -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> x -> Pattern' x
forall x. PatternInfo -> x -> Pattern' x
VarP Int32
a Int32
b
    valu [1, a :: Int32
a, b :: Int32
b, c :: Int32
c] = (ConHead
 -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)
-> Int32 -> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP Int32
a Int32
b Int32
c
    valu [2, a :: Int32
a, b :: Int32
b] = (PatternInfo -> Literal -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> Literal -> Pattern' x
forall x. PatternInfo -> Literal -> Pattern' x
LitP Int32
a Int32
b
    valu [3, a :: Int32
a, b :: Int32
b] = (PatternInfo -> Term -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> Term -> Pattern' x
forall x. PatternInfo -> Term -> Pattern' x
DotP Int32
a Int32
b
    valu [4, a :: Int32
a, b :: Int32
b] = (ProjOrigin -> QName -> Pattern' x)
-> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ProjOrigin -> QName -> Pattern' x
forall x. ProjOrigin -> QName -> Pattern' x
ProjP Int32
a Int32
b
    valu [5, a :: Int32
a, b :: Int32
b, c :: Int32
c, d :: Int32
d] = (PatternInfo -> Term -> Term -> x -> Pattern' x)
-> Int32 -> Int32 -> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> Term -> Term -> x -> Pattern' x
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP Int32
a Int32
b Int32
c Int32
d
    valu [6, a :: Int32
a, b :: Int32
b, c :: Int32
c] = (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)
-> Int32 -> Int32 -> Int32 -> R (Pattern' x)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP Int32
a Int32
b Int32
c
    valu _         = 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) = (a -> Builtin a) -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Builtin a
forall pf. pf -> Builtin pf
Prim a
a
  icod_ (Builtin a :: Term
a) = Int32 -> (Term -> Builtin Any) -> Term -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Term -> Builtin Any
forall pf. Term -> Builtin pf
Builtin Term
a

  value :: Int32 -> R (Builtin a)
value = (Node -> R (Builtin a)) -> Int32 -> R (Builtin a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Builtin a)
forall pf. EmbPrj pf => Node -> R (Builtin pf)
valu where
    valu :: Node -> R (Builtin pf)
valu [a :: Int32
a]    = (pf -> Builtin pf) -> Int32 -> R (Builtin pf)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN pf -> Builtin pf
forall pf. pf -> Builtin pf
Prim    Int32
a
    valu [1, a :: Int32
a] = (Term -> Builtin pf) -> Int32 -> R (Builtin pf)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Int32
a
    valu _      = R (Builtin pf)
forall a. R a
malformed

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

  value :: Int32 -> R (Substitution' a)
value = (Node -> R (Substitution' a)) -> Int32 -> R (Substitution' a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Substitution' a)
forall a. EmbPrj a => Node -> R (Substitution' a)
valu where
    valu :: Node -> R (Substitution' a)
valu []        = Substitution' a
-> Arrows
     (Constant Int32 (Domains (Substitution' a)))
     (R (CoDomain (Substitution' a)))
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Substitution' a
forall a. Substitution' a
IdS
    valu [1, a :: Int32
a]    = (Empty -> Substitution' a) -> Int32 -> R (Substitution' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Int32
a
    valu [2, a :: Int32
a, b :: Int32
b] = (a -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) Int32
a Int32
b
    valu [3, a :: Int32
a, b :: Int32
b]    = (Empty -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Empty -> Substitution' a -> Substitution' a
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Int32
a Int32
b
    valu [4, a :: Int32
a, b :: Int32
b] = (Int -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Wk Int32
a Int32
b
    valu [5, a :: Int32
a, b :: Int32
b] = (Int -> Substitution' a -> Substitution' a)
-> Int32 -> Int32 -> R (Substitution' a)
forall t.
(VALU t (IsBase t),
 Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Lift Int32
a Int32
b
    valu _         = R (Substitution' a)
forall a. R a
malformed