{-# 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 ()
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
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