{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances.Internal where
import qualified Data.HashSet as HashSet
import Control.Monad
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 ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f
value :: Int32 -> R (Dom a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom
instance EmbPrj Signature where
icod_ :: Signature -> S Int32
icod_ (Sig Sections
a Definitions
b RewriteRuleMap
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Sections -> Definitions -> RewriteRuleMap -> Signature
Sig Sections
a Definitions
b RewriteRuleMap
c
value :: Int32 -> R Signature
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Sections -> Definitions -> RewriteRuleMap -> Signature
Sig
instance EmbPrj Section where
icod_ :: Section -> S Int32
icod_ (Section Telescope
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Telescope -> Section
Section Telescope
a
value :: Int32 -> R Section
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Telescope -> Section
Section
instance EmbPrj a => EmbPrj (Tele a) where
icod_ :: Tele a -> S Int32
icod_ Tele a
EmptyTel = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Tele a
EmptyTel
icod_ (ExtendTel a
a Abs (Tele a)
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a Abs (Tele a)
b
value :: Int32 -> R (Tele a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> StateT St IO (Tele a)
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele a)))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Tele a
EmptyTel
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj Permutation where
icod_ :: Permutation -> S Int32
icod_ (Perm Int
a [Int]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> [Int] -> Permutation
Perm Int
a [Int]
b
value :: Int32 -> R Permutation
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> [Int] -> Permutation
Perm
instance EmbPrj a => EmbPrj (Drop a) where
icod_ :: Drop a -> S Int32
icod_ (Drop Int
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Int -> a -> Drop a
Drop Int
a a
b
value :: Int32 -> R (Drop a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Int -> a -> Drop a
Drop
instance EmbPrj a => EmbPrj (Elim' a) where
icod_ :: Elim' a -> S Int32
icod_ (Apply Arg a
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Arg a -> Elim' a
Apply Arg a
a
icod_ (IApply a
x a
y a
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. a -> a -> a -> Elim' a
IApply a
x a
y a
a
icod_ (Proj ProjOrigin
a QName
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
a QName
b
value :: Int32 -> R (Elim' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (Elim' a)
valu where
valu :: [Int32] -> R (Elim' a)
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Arg a -> Elim' a
Apply Int32
a
valu [Int32
0,Int32
x,Int32
y,Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> a -> a -> Elim' a
IApply Int32
x Int32
y Int32
a
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. ProjOrigin -> QName -> Elim' a
Proj Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj I.DataOrRecord where
icod_ :: DataOrRecord -> S Int32
icod_ = \case
DataOrRecord
IsData -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall p. DataOrRecord' p
IsData
IsRecord PatternOrCopattern
pm -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
pm
value :: Int32 -> R DataOrRecord
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[] -> forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall p. DataOrRecord' p
IsData
[Int32
pm] -> forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall p. p -> DataOrRecord' p
IsRecord Int32
pm
[Int32]
_ -> forall a. R a
malformed
instance EmbPrj I.ConHead where
icod_ :: ConHead -> S Int32
icod_ (ConHead QName
a DataOrRecord
b Induction
c [Arg QName]
d) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
a DataOrRecord
b Induction
c [Arg QName]
d
value :: Int32 -> R ConHead
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead
instance (EmbPrj a) => EmbPrj (I.Type' a) where
icod_ :: Type' a -> S Int32
icod_ (El Sort
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t a. Sort' t -> a -> Type'' t a
El Sort
a a
b
value :: Int32 -> R (Type' a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t a. Sort' t -> a -> Type'' t a
El
instance EmbPrj a => EmbPrj (I.Abs a) where
icod_ :: Abs a -> S Int32
icod_ (NoAbs ArgName
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. ArgName -> a -> Abs a
NoAbs ArgName
a a
b
icod_ (Abs ArgName
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. ArgName -> a -> Abs a
Abs ArgName
a a
b
value :: Int32 -> R (Abs a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (Abs a)
valu where
valu :: [Int32] -> R (Abs a)
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. ArgName -> a -> Abs a
Abs Int32
a Int32
b
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. ArgName -> a -> Abs a
NoAbs Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj I.Term where
icod_ :: Term -> S Int32
icod_ (Var Int
a []) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ Int
a -> Int -> Elims -> Term
Var Int
a []) Int
a
icod_ (Var Int
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Int -> Elims -> Term
Var Int
a Elims
b
icod_ (Lam ArgInfo
a Abs Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 ArgInfo -> Abs Term -> Term
Lam ArgInfo
a Abs Term
b
icod_ (Lit Literal
a ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Literal -> Term
Lit Literal
a
icod_ (Def QName
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 QName -> Elims -> Term
Def QName
a Elims
b
icod_ (Con ConHead
a ConInfo
b Elims
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 ConHead -> ConInfo -> Elims -> Term
Con ConHead
a ConInfo
b Elims
c
icod_ (Pi Dom' Term Type
a Abs Type
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 Dom' Term Type -> Abs Type -> Term
Pi Dom' Term Type
a Abs Type
b
icod_ (MetaV MetaId
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 MetaId -> Elims -> Term
MetaV MetaId
a Elims
b
icod_ (Sort Sort
a ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 Sort -> Term
Sort Sort
a
icod_ (DontCare Term
a ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
8 Term -> Term
DontCare Term
a
icod_ (Level Level
a ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
9 Level -> Term
Level Level
a
icod_ (Dummy ArgName
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
10 ArgName -> Elims -> Term
Dummy ArgName
a Elims
b
value :: Int32 -> R Term
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R Term
valu where
valu :: [Int32] -> R Term
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Term
var Int32
a
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Elims -> Term
Var Int32
a Int32
b
valu [Int32
1, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgInfo -> Abs Term -> Term
Lam Int32
a Int32
b
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Literal -> Term
Lit Int32
a
valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> Elims -> Term
Def Int32
a Int32
b
valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConInfo -> Elims -> Term
Con Int32
a Int32
b Int32
c
valu [Int32
5, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom' Term Type -> Abs Type -> Term
Pi Int32
a Int32
b
valu [Int32
6, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN MetaId -> Elims -> Term
MetaV Int32
a Int32
b
valu [Int32
7, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort -> Term
Sort Int32
a
valu [Int32
8, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Term
DontCare Int32
a
valu [Int32
9, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Level -> Term
Level Int32
a
valu [Int32
10, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgName -> Elims -> Term
Dummy Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj Level where
icod_ :: Level -> S Int32
icod_ (Max Integer
a [PlusLevel]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
a [PlusLevel]
b
value :: Int32 -> R Level
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t. Integer -> [PlusLevel' t] -> Level' t
Max
instance EmbPrj PlusLevel where
icod_ :: PlusLevel -> S Int32
icod_ (Plus Integer
a Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t. Integer -> t -> PlusLevel' t
Plus Integer
a Term
b
value :: Int32 -> R PlusLevel
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t. Integer -> t -> PlusLevel' t
Plus
instance EmbPrj IsFibrant where
icod_ :: IsFibrant -> S Int32
icod_ IsFibrant
IsFibrant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ IsFibrant
IsStrict = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
value :: Int32 -> R IsFibrant
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return IsFibrant
IsFibrant
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return IsFibrant
IsStrict
value Int32
_ = forall a. R a
malformed
instance EmbPrj Univ where
instance EmbPrj I.Sort where
icod_ :: Sort -> S Int32
icod_ = \case
Univ Univ
a Level
b -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall t. Univ -> Level' t -> Sort' t
Univ Univ
a Level
b
Sort
SizeUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall t. Sort' t
SizeUniv
Inf Univ
a Integer
b -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 forall t. Univ -> Integer -> Sort' t
Inf Univ
a Integer
b
PiSort Dom' Term Term
a Sort
b Abs Sort
c -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort
b Abs Sort
c
FunSort Sort
a Sort
b -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
a Sort
b
UnivSort Sort
a -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 forall t. Sort' t -> Sort' t
UnivSort Sort
a
DefS QName
a Elims
b -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 forall t. QName -> [Elim' t] -> Sort' t
DefS QName
a Elims
b
Sort
LockUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
9 forall t. Sort' t
LockUniv
Sort
IntervalUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
10 forall t. Sort' t
IntervalUniv
MetaS MetaId
a Elims
b -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
11 forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
a Elims
b
DummyS ArgName
s -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
12 forall t. ArgName -> Sort' t
DummyS ArgName
s
Sort
LevelUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
13 forall t. Sort' t
LevelUniv
value :: Int32 -> R Sort
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {t}.
(EmbPrj t, EmbPrj (Dom' t t), EmbPrj (Level' t),
EmbPrj (Sort' t)) =>
[Int32] -> R (Sort' t)
valu where
valu :: [Int32] -> R (Sort' t)
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Univ -> Level' t -> Sort' t
Univ Int32
a Int32
b
valu [Int32
2] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
SizeUniv
valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Univ -> Integer -> Sort' t
Inf Int32
a Int32
b
valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Int32
a Int32
b Int32
c
valu [Int32
5, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t -> Sort' t -> Sort' t
FunSort Int32
a Int32
b
valu [Int32
6, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t -> Sort' t
UnivSort Int32
a
valu [Int32
7, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. QName -> [Elim' t] -> Sort' t
DefS Int32
a Int32
b
valu [Int32
9] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
LockUniv
valu [Int32
10] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
IntervalUniv
valu [Int32
11, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. MetaId -> [Elim' t] -> Sort' t
MetaS Int32
a Int32
b
valu [Int32
12, Int32
s] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. ArgName -> Sort' t
DummyS Int32
s
valu [Int32
13] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Sort' t
LevelUniv
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj DisplayForm where
icod_ :: DisplayForm -> S Int32
icod_ (Display Int
a Elims
b DisplayTerm
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
a Elims
b DisplayTerm
c
value :: Int32 -> R DisplayForm
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> Elims -> DisplayTerm -> DisplayForm
Display
instance EmbPrj a => EmbPrj (Open a) where
icod_ :: Open a -> S Int32
icod_ (OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d
value :: Int32 -> R (Open a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing
instance EmbPrj CheckpointId where
icod_ :: CheckpointId -> S Int32
icod_ (CheckpointId Int
a) = forall a. EmbPrj a => a -> S Int32
icode Int
a
value :: Int32 -> R CheckpointId
value Int32
n = Int -> CheckpointId
CheckpointId forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> forall a. EmbPrj a => Int32 -> R a
value Int32
n
instance EmbPrj DisplayTerm where
icod_ :: DisplayTerm -> S Int32
icod_ (DTerm' Term
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Term -> Elims -> DisplayTerm
DTerm' Term
a Elims
b
icod_ (DDot' Term
a Elims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Term -> Elims -> DisplayTerm
DDot' Term
a Elims
b
icod_ (DCon ConHead
a ConInfo
b [Arg DisplayTerm]
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
a ConInfo
b [Arg DisplayTerm]
c
icod_ (DDef QName
a [Elim' DisplayTerm]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
a [Elim' DisplayTerm]
b
icod_ (DWithApp DisplayTerm
a [DisplayTerm]
b Elims
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
a [DisplayTerm]
b Elims
c
value :: Int32 -> R DisplayTerm
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R DisplayTerm
valu where
valu :: [Int32] -> R DisplayTerm
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Elims -> DisplayTerm
DTerm' Int32
a Int32
b
valu [Int32
1, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Elims -> DisplayTerm
DDot' Int32
a Int32
b
valu [Int32
2, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon Int32
a Int32
b Int32
c
valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef Int32
a Int32
b
valu [Int32
4, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (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 [Int32]
_ = forall a. R a
malformed
instance EmbPrj MutualId where
icod_ :: MutualId -> S Int32
icod_ (MutId Int32
a) = forall a. EmbPrj a => a -> S Int32
icode Int32
a
value :: Int32 -> R MutualId
value Int32
n = Int32 -> MutualId
MutId forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> forall a. EmbPrj a => Int32 -> R a
value Int32
n
instance EmbPrj CompKit where
icod_ :: CompKit -> S Int32
icod_ (CompKit Maybe QName
a Maybe QName
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe QName -> Maybe QName -> CompKit
CompKit Maybe QName
a Maybe QName
b
value :: Int32 -> R CompKit
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe QName -> Maybe QName -> CompKit
CompKit
instance EmbPrj Definition where
icod_ :: Definition -> S Int32
icod_ (Defn ArgInfo
a QName
b Type
c [Polarity]
d [Occurrence]
e NumGeneralizableArgs
f [Maybe Name]
g [LocalDisplayForm]
h MutualId
i CompiledRepresentation
j Maybe QName
k Bool
l Set QName
m Bool
n Bool
o Bool
p Blocked_
q Language
r Defn
s) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn ArgInfo
a QName
b (forall a. KillRange a => KillRangeT a
P.killRange Type
c) [Polarity]
d [Occurrence]
e NumGeneralizableArgs
f [Maybe Name]
g [LocalDisplayForm]
h MutualId
i CompiledRepresentation
j Maybe QName
k Bool
l Set QName
m Bool
n Bool
o Bool
p Blocked_
q Language
r Defn
s
value :: Int32 -> R Definition
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn
instance EmbPrj NotBlocked where
icod_ :: NotBlocked -> S Int32
icod_ NotBlocked
ReallyNotBlocked = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t. NotBlocked' t
ReallyNotBlocked
icod_ (StuckOn Elim' Term
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall t. Elim' t -> NotBlocked' t
StuckOn Elim' Term
a
icod_ NotBlocked
Underapplied = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall t. NotBlocked' t
Underapplied
icod_ NotBlocked
AbsurdMatch = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall t. NotBlocked' t
AbsurdMatch
icod_ (MissingClauses QName
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 forall t. QName -> NotBlocked' t
MissingClauses QName
a
value :: Int32 -> R NotBlocked
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {t}. EmbPrj t => [Int32] -> StateT St IO (NotBlocked' t)
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains (NotBlocked' t)))
(R (CoDomain (NotBlocked' t)))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. NotBlocked' t
ReallyNotBlocked
valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. Elim' t -> NotBlocked' t
StuckOn Int32
a
valu [Int32
1] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. NotBlocked' t
Underapplied
valu [Int32
2] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. NotBlocked' t
AbsurdMatch
valu [Int32
3, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall t. QName -> NotBlocked' t
MissingClauses Int32
a
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj Blocked_ where
icod_ :: Blocked_ -> S Int32
icod_ (NotBlocked NotBlocked
a ()
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
a ()
b
icod_ Blocked{} = forall a. HasCallStack => a
__IMPOSSIBLE__
value :: Int32 -> R Blocked_
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked
instance EmbPrj NLPat where
icod_ :: NLPat -> S Int32
icod_ (PVar Int
a [Arg Int]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Int -> [Arg Int] -> NLPat
PVar Int
a [Arg Int]
b
icod_ (PDef QName
a PElims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 QName -> PElims -> NLPat
PDef QName
a PElims
b
icod_ (PLam ArgInfo
a Abs NLPat
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
a Abs NLPat
b
icod_ (PPi Dom NLPType
a Abs NLPType
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
a Abs NLPType
b
icod_ (PSort NLPSort
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 NLPSort -> NLPat
PSort NLPSort
a
icod_ (PBoundVar Int
a PElims
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 Int -> PElims -> NLPat
PBoundVar Int
a PElims
b
icod_ (PTerm Term
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 Term -> NLPat
PTerm Term
a
value :: Int32 -> R NLPat
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NLPat
valu where
valu :: [Int32] -> R NLPat
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> [Arg Int] -> NLPat
PVar Int32
a Int32
b
valu [Int32
1, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> PElims -> NLPat
PDef Int32
a Int32
b
valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgInfo -> Abs NLPat -> NLPat
PLam Int32
a Int32
b
valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom NLPType -> Abs NLPType -> NLPat
PPi Int32
a Int32
b
valu [Int32
4, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort -> NLPat
PSort Int32
a
valu [Int32
5, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> PElims -> NLPat
PBoundVar Int32
a Int32
b
valu [Int32
6, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (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 [Int32]
_ = forall a. R a
malformed
instance EmbPrj NLPType where
icod_ :: NLPType -> S Int32
icod_ (NLPType NLPSort
a NLPat
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NLPSort -> NLPat -> NLPType
NLPType NLPSort
a NLPat
b
value :: Int32 -> R NLPType
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN NLPSort -> NLPat -> NLPType
NLPType
instance EmbPrj NLPSort where
icod_ :: NLPSort -> S Int32
icod_ (PType NLPat
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 NLPat -> NLPSort
PType NLPat
a
icod_ (PProp NLPat
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 NLPat -> NLPSort
PProp NLPat
a
icod_ (PInf Univ
f Integer
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Univ -> Integer -> NLPSort
PInf Univ
f Integer
a
icod_ NLPSort
PSizeUniv = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 NLPSort
PSizeUniv
icod_ NLPSort
PLockUniv = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 NLPSort
PLockUniv
icod_ NLPSort
PIntervalUniv = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 NLPSort
PIntervalUniv
icod_ (PSSet NLPat
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 NLPat -> NLPSort
PSSet NLPat
a
icod_ NLPSort
PLevelUniv = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 NLPSort
PLevelUniv
value :: Int32 -> R NLPSort
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NLPSort
valu where
valu :: [Int32] -> R NLPSort
valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PType Int32
a
valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PProp Int32
a
valu [Int32
2, Int32
f, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Univ -> Integer -> NLPSort
PInf Int32
f Int32
a
valu [Int32
3] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PSizeUniv
valu [Int32
4] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PLockUniv
valu [Int32
5] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PIntervalUniv
valu [Int32
6, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPat -> NLPSort
PSSet Int32
a
valu [Int32
7] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NLPSort
PLevelUniv
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj RewriteRule where
icod_ :: RewriteRule -> S Int32
icod_ (RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f Bool
g) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f Bool
g
value :: Int32 -> R RewriteRule
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule
instance EmbPrj Projection where
icod_ :: Projection -> S Int32
icod_ (Projection Maybe QName
a QName
b Arg QName
c Int
d ProjLams
e) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection Maybe QName
a QName
b Arg QName
c Int
d ProjLams
e
value :: Int32 -> R Projection
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection
instance EmbPrj ProjLams where
icod_ :: ProjLams -> S Int32
icod_ (ProjLams [Arg ArgName]
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> ProjLams
ProjLams [Arg ArgName]
a
value :: Int32 -> R ProjLams
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN [Arg ArgName] -> ProjLams
ProjLams
instance EmbPrj System where
icod_ :: System -> S Int32
icod_ (System Telescope
a [(Face, Term)]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Telescope -> [(Face, Term)] -> System
System Telescope
a [(Face, Term)]
b
value :: Int32 -> R System
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Telescope -> [(Face, Term)] -> System
System
instance EmbPrj ExtLamInfo where
icod_ :: ExtLamInfo -> S Int32
icod_ (ExtLamInfo ModuleName
a Bool
b Maybe System
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
a Bool
b Maybe System
c
value :: Int32 -> R ExtLamInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo
instance EmbPrj Polarity where
icod_ :: Polarity -> S Int32
icod_ Polarity
Covariant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Polarity
Contravariant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ Polarity
Invariant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
icod_ Polarity
Nonvariant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
value :: Int32 -> R Polarity
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Covariant
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Contravariant
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Invariant
value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return Polarity
Nonvariant
value Int32
_ = forall a. R a
malformed
instance EmbPrj IsForced where
icod_ :: IsForced -> S Int32
icod_ IsForced
Forced = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ IsForced
NotForced = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
value :: Int32 -> R IsForced
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return IsForced
Forced
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return IsForced
NotForced
value Int32
_ = forall a. R a
malformed
instance EmbPrj NumGeneralizableArgs where
icod_ :: NumGeneralizableArgs -> S Int32
icod_ NumGeneralizableArgs
NoGeneralizableArgs = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NumGeneralizableArgs
NoGeneralizableArgs
icod_ (SomeGeneralizableArgs Int
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> NumGeneralizableArgs
SomeGeneralizableArgs Int
a
value :: Int32 -> R NumGeneralizableArgs
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NumGeneralizableArgs
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains NumGeneralizableArgs))
(R (CoDomain NumGeneralizableArgs))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NumGeneralizableArgs
NoGeneralizableArgs
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (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 [Int32]
_ = forall a. R a
malformed
instance EmbPrj DoGeneralize where
icod_ :: DoGeneralize -> S Int32
icod_ DoGeneralize
YesGeneralizeVar = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ DoGeneralize
YesGeneralizeMeta = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ DoGeneralize
NoGeneralize = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R DoGeneralize
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
YesGeneralizeVar
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
YesGeneralizeMeta
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return DoGeneralize
NoGeneralize
value Int32
_ = forall a. R a
malformed
instance EmbPrj Occurrence where
icod_ :: Occurrence -> S Int32
icod_ Occurrence
StrictPos = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Occurrence
Mixed = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ Occurrence
Unused = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
icod_ Occurrence
GuardPos = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
icod_ Occurrence
JustPos = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
4
icod_ Occurrence
JustNeg = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
5
value :: Int32 -> R Occurrence
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
StrictPos
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Mixed
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
Unused
value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
GuardPos
value Int32
4 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
JustPos
value Int32
5 = forall (m :: * -> *) a. Monad m => a -> m a
return Occurrence
JustNeg
value Int32
_ = forall a. R a
malformed
instance EmbPrj EtaEquality where
icod_ :: EtaEquality -> S Int32
icod_ (Specified HasEta
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 HasEta -> EtaEquality
Specified HasEta
a
icod_ (Inferred HasEta
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 HasEta -> EtaEquality
Inferred HasEta
a
value :: Int32 -> R EtaEquality
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R EtaEquality
valu where
valu :: [Int32] -> R EtaEquality
valu [Int32
0,Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN HasEta -> EtaEquality
Specified Int32
a
valu [Int32
1,Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (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 [Int32]
_ = forall a. R a
malformed
instance EmbPrj ProjectionLikenessMissing
instance EmbPrj BuiltinSort where
icod_ :: BuiltinSort -> S Int32
icod_ = \case
SortUniv Univ
a -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Univ -> BuiltinSort
SortUniv Univ
a
SortOmega Univ
a -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Univ -> BuiltinSort
SortOmega Univ
a
BuiltinSort
SortIntervalUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 BuiltinSort
SortIntervalUniv
BuiltinSort
SortLevelUniv -> forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 BuiltinSort
SortLevelUniv
value :: Int32 -> R BuiltinSort
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase \case
[Int32
0, Int32
a] -> forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Univ -> BuiltinSort
SortUniv Int32
a
[Int32
1, Int32
a] -> forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Univ -> BuiltinSort
SortOmega Int32
a
[Int32
2] -> forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN BuiltinSort
SortIntervalUniv
[Int32
3] -> forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN BuiltinSort
SortLevelUniv
[Int32]
_ -> forall a. R a
malformed
instance EmbPrj Defn where
icod_ :: Defn -> S Int32
icod_ (Axiom Bool
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Bool -> Defn
Axiom Bool
a
icod_ (Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t [Clause]
u FunctionInverse
c Maybe [QName]
d IsAbstract
e Either ProjectionLikenessMissing Projection
f Bool
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l IsOpaque
m) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 (\ [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Either ProjectionLikenessMissing Projection
-> Bool
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> IsOpaque
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s Maybe Compiled
t) [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s [Clause]
u FunctionInverse
c Maybe [QName]
d IsAbstract
e Either ProjectionLikenessMissing Projection
f Bool
g Set FunctionFlag
h Maybe Bool
i Maybe ExtLamInfo
j Maybe QName
k Maybe QName
l IsOpaque
m
icod_ (Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j
icod_ (Record Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> Maybe Bool
-> IsAbstract
-> CompKit
-> Defn
Record Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m
icod_ (Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e CompKit
f Maybe [QName]
g [IsForced]
h Maybe [Bool]
i Bool
j Bool
k) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Bool
-> Bool
-> Defn
Constructor Int
a Int
b ConHead
c QName
d IsAbstract
e CompKit
f Maybe [QName]
g [IsForced]
h Maybe [Bool]
i Bool
j Bool
k
icod_ (Primitive IsAbstract
a PrimitiveId
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e IsOpaque
f) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 IsAbstract
-> PrimitiveId
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> IsOpaque
-> Defn
Primitive IsAbstract
a PrimitiveId
b [Clause]
c FunctionInverse
d Maybe CompiledClauses
e IsOpaque
f
icod_ (PrimitiveSort BuiltinSort
a Sort
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 BuiltinSort -> Sort -> Defn
PrimitiveSort BuiltinSort
a Sort
b
icod_ AbstractDefn{} = forall a. HasCallStack => a
__IMPOSSIBLE__
icod_ Defn
GeneralizableVar = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 Defn
GeneralizableVar
icod_ DataOrRecSig{} = forall a. HasCallStack => a
__IMPOSSIBLE__
value :: Int32 -> R Defn
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R Defn
valu where
valu :: [Int32] -> R Defn
valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Bool -> Defn
Axiom Int32
a
valu [Int32
1, Int32
a, Int32
b, Int32
s, Int32
u, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l, Int32
m]
= forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN (\ [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s -> [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Either ProjectionLikenessMissing Projection
-> Bool
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Maybe QName
-> IsOpaque
-> Defn
Function [Clause]
a Maybe CompiledClauses
b Maybe SplitTree
s forall a. Maybe a
Nothing) Int32
a Int32
b Int32
s Int32
u Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l Int32
m
valu [Int32
2, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j
valu [Int32
3, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l, Int32
m] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> Maybe Bool
-> IsAbstract
-> CompKit
-> Defn
Record Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l Int32
m
valu [Int32
4, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k] = forall t.
(VALU t (IsBase t),
StrictCurrying (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
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Bool
-> Bool
-> Defn
Constructor Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k
valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
-> PrimitiveId
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> IsOpaque
-> Defn
Primitive Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f
valu [Int32
6, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN BuiltinSort -> Sort -> Defn
PrimitiveSort Int32
a Int32
b
valu [Int32
7] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Defn
GeneralizableVar
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj LazySplit where
icod_ :: LazySplit -> S Int32
icod_ LazySplit
StrictSplit = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' LazySplit
StrictSplit
icod_ LazySplit
LazySplit = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 LazySplit
LazySplit
value :: Int32 -> R LazySplit
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R LazySplit
valu where
valu :: [a]
-> Arrows
(Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN LazySplit
StrictSplit
valu [a
0] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN LazySplit
LazySplit
valu [a]
_ = forall a. R a
malformed
instance EmbPrj SplitTag where
icod_ :: SplitTag -> S Int32
icod_ (SplitCon QName
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 QName -> SplitTag
SplitCon QName
c
icod_ (SplitLit Literal
l) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Literal -> SplitTag
SplitLit Literal
l
icod_ SplitTag
SplitCatchall = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' SplitTag
SplitCatchall
value :: Int32 -> R SplitTag
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R SplitTag
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains SplitTag)) (R (CoDomain SplitTag))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN SplitTag
SplitCatchall
valu [Int32
0, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> SplitTag
SplitCon Int32
c
valu [Int32
1, Int32
l] = forall t.
(VALU t (IsBase t),
StrictCurrying (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 [Int32]
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (SplitTree' a) where
icod_ :: SplitTree' a -> S Int32
icod_ (SplittingDone Int
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Int -> SplitTree' a
SplittingDone Int
a
icod_ (SplitAt Arg Int
a LazySplit
b SplitTrees' a
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
a LazySplit
b SplitTrees' a
c
value :: Int32 -> R (SplitTree' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (SplitTree' a)
valu where
valu :: [Int32] -> R (SplitTree' a)
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Int -> SplitTree' a
SplittingDone Int32
a
valu [Int32
0, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Int32
a Int32
b Int32
c
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj FunctionFlag where
icod_ :: FunctionFlag -> S Int32
icod_ FunctionFlag
FunStatic = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
0
icod_ FunctionFlag
FunInline = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
1
icod_ FunctionFlag
FunMacro = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
2
value :: Int32 -> R FunctionFlag
value = \case
Int32
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunStatic
Int32
1 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunInline
Int32
2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunMacro
Int32
_ -> forall a. R a
malformed
instance EmbPrj a => EmbPrj (WithArity a) where
icod_ :: WithArity a -> S Int32
icod_ (WithArity Int
a a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c. Int -> c -> WithArity c
WithArity Int
a a
b
value :: Int32 -> R (WithArity a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall c. Int -> c -> WithArity c
WithArity
instance EmbPrj a => EmbPrj (Case a) where
icod_ :: Case a -> S Int32
icod_ (Branches Bool
a Map QName (WithArity a)
b Maybe (ConHead, WithArity a)
c Map Literal a
d Maybe a
e Maybe Bool
f Bool
g) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
a Map QName (WithArity a)
b Maybe (ConHead, WithArity a)
c Map Literal a
d Maybe a
e Maybe Bool
f Bool
g
value :: Int32 -> R (Case a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches
instance EmbPrj OpaqueBlock where
icod_ :: OpaqueBlock -> S Int32
icod_ (OpaqueBlock OpaqueId
id HashSet QName
uf HashSet QName
_ Maybe OpaqueId
_ Range
r) =
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\OpaqueId
id [QName]
uf ->
let !unfolding :: HashSet QName
unfolding = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList [QName]
uf
in OpaqueId
-> HashSet QName
-> HashSet QName
-> Maybe OpaqueId
-> Range
-> OpaqueBlock
OpaqueBlock OpaqueId
id HashSet QName
unfolding forall a. Monoid a => a
mempty forall a. Maybe a
Nothing)
OpaqueId
id (forall a. HashSet a -> [a]
HashSet.toList HashSet QName
uf) Range
r
value :: Int32 -> R OpaqueBlock
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (\OpaqueId
id [QName]
uf -> let !unfolding :: HashSet QName
unfolding = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList [QName]
uf
in OpaqueId
-> HashSet QName
-> HashSet QName
-> Maybe OpaqueId
-> Range
-> OpaqueBlock
OpaqueBlock OpaqueId
id HashSet QName
unfolding forall a. Monoid a => a
mempty forall a. Maybe a
Nothing)
instance EmbPrj CompiledClauses where
icod_ :: CompiledClauses -> S Int32
icod_ (Fail [Arg ArgName]
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. [Arg ArgName] -> CompiledClauses' a
Fail [Arg ArgName]
a
icod_ (Done [Arg ArgName]
a Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [Arg ArgName]
a (forall a. KillRange a => KillRangeT a
P.killRange Term
b)
icod_ (Case Arg Int
a Case CompiledClauses
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
a Case CompiledClauses
b
value :: Int32 -> R CompiledClauses
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}.
(EmbPrj a, EmbPrj (CompiledClauses' a)) =>
[Int32] -> R (CompiledClauses' a)
valu where
valu :: [Int32] -> R (CompiledClauses' a)
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. [Arg ArgName] -> CompiledClauses' a
Fail Int32
a
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done Int32
a Int32
b
valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (FunctionInverse' a) where
icod_ :: FunctionInverse' a -> S Int32
icod_ FunctionInverse' a
NotInjective = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c. FunctionInverse' c
NotInjective
icod_ (Inverse InversionMap a
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall c. InversionMap c -> FunctionInverse' c
Inverse InversionMap a
a
value :: Int32 -> R (FunctionInverse' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {c}.
EmbPrj [c] =>
[Int32] -> StateT St IO (FunctionInverse' c)
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains (FunctionInverse' c)))
(R (CoDomain (FunctionInverse' c)))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall c. FunctionInverse' c
NotInjective
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall c. InversionMap c -> FunctionInverse' c
Inverse Int32
a
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj TermHead where
icod_ :: TermHead -> S Int32
icod_ TermHead
SortHead = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' TermHead
SortHead
icod_ TermHead
PiHead = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 TermHead
PiHead
icod_ (ConsHead QName
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 QName -> TermHead
ConsHead QName
a
icod_ (VarHead Int
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Int -> TermHead
VarHead Int
a
icod_ TermHead
UnknownHead = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 TermHead
UnknownHead
value :: Int32 -> R TermHead
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R TermHead
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
SortHead
valu [Int32
1] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
PiHead
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> TermHead
ConsHead Int32
a
valu [Int32
3, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> TermHead
VarHead Int32
a
valu [Int32
4] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TermHead
UnknownHead
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj I.Clause where
icod_ :: Clause -> S Int32
icod_ (Clause Range
a Range
b Telescope
c NAPs
d Maybe Term
e Maybe (Arg Type)
f Bool
g Maybe Bool
h Maybe Bool
i Maybe Bool
j ExpandedEllipsis
k Maybe ModuleName
l) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
a Range
b Telescope
c NAPs
d Maybe Term
e Maybe (Arg Type)
f Bool
g Maybe Bool
h Maybe Bool
i Maybe Bool
j ExpandedEllipsis
k Maybe ModuleName
l
value :: Int32 -> R Clause
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause
instance EmbPrj I.ConPatternInfo where
icod_ :: ConPatternInfo -> S Int32
icod_ (ConPatternInfo PatternInfo
a Bool
b Bool
c Maybe (Arg Type)
d Bool
e) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
a Bool
b Bool
c Maybe (Arg Type)
d Bool
e
value :: Int32 -> R ConPatternInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo
instance EmbPrj I.DBPatVar where
icod_ :: DBPatVar -> S Int32
icod_ (DBPatVar ArgName
a Int
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgName -> Int -> DBPatVar
DBPatVar ArgName
a Int
b
value :: Int32 -> R DBPatVar
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ArgName -> Int -> DBPatVar
DBPatVar
instance EmbPrj I.PatternInfo where
icod_ :: PatternInfo -> S Int32
icod_ (PatternInfo PatOrigin
a [Name]
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
a [Name]
b
value :: Int32 -> R PatternInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN PatOrigin -> [Name] -> PatternInfo
PatternInfo
instance EmbPrj I.PatOrigin where
icod_ :: PatOrigin -> S Int32
icod_ PatOrigin
PatOSystem = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatOrigin
PatOSystem
icod_ PatOrigin
PatOSplit = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 PatOrigin
PatOSplit
icod_ (PatOVar Name
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Name -> PatOrigin
PatOVar Name
a
icod_ PatOrigin
PatODot = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 PatOrigin
PatODot
icod_ PatOrigin
PatOWild = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 PatOrigin
PatOWild
icod_ PatOrigin
PatOCon = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 PatOrigin
PatOCon
icod_ PatOrigin
PatORec = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 PatOrigin
PatORec
icod_ PatOrigin
PatOLit = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 PatOrigin
PatOLit
icod_ PatOrigin
PatOAbsurd = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
8 PatOrigin
PatOAbsurd
value :: Int32 -> R PatOrigin
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R PatOrigin
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOSystem
valu [Int32
1] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOSplit
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Name -> PatOrigin
PatOVar Int32
a
valu [Int32
3] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatODot
valu [Int32
4] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOWild
valu [Int32
5] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOCon
valu [Int32
6] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatORec
valu [Int32
7] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOLit
valu [Int32
8] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatOrigin
PatOAbsurd
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (I.Pattern' a) where
icod_ :: Pattern' a -> S Int32
icod_ (VarP PatternInfo
a a
b ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
a a
b
icod_ (ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c
icod_ (LitP PatternInfo
a Literal
b ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
a Literal
b
icod_ (DotP PatternInfo
a Term
b ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
a Term
b
icod_ (ProjP ProjOrigin
a QName
b ) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
a QName
b
icod_ (IApplyP PatternInfo
a Term
b Term
c a
d) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
a Term
b Term
c a
d
icod_ (DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c
value :: Int32 -> R (Pattern' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {x}. EmbPrj x => [Int32] -> R (Pattern' x)
valu where
valu :: [Int32] -> R (Pattern' x)
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> x -> Pattern' x
VarP Int32
a Int32
b
valu [Int32
1, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP Int32
a Int32
b Int32
c
valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> Literal -> Pattern' x
LitP Int32
a Int32
b
valu [Int32
3, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> Term -> Pattern' x
DotP Int32
a Int32
b
valu [Int32
4, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. ProjOrigin -> QName -> Pattern' x
ProjP Int32
a Int32
b
valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP Int32
a Int32
b Int32
c Int32
d
valu [Int32
6, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP Int32
a Int32
b Int32
c
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (Builtin a) where
icod_ :: Builtin a -> S Int32
icod_ (Prim a
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall pf. pf -> Builtin pf
Prim a
a
icod_ (Builtin Term
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall pf. Term -> Builtin pf
Builtin Term
a
icod_ (BuiltinRewriteRelations Set QName
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
a
value :: Int32 -> R (Builtin a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {pf}. EmbPrj pf => [Int32] -> R (Builtin pf)
valu where
valu :: [Int32] -> R (Builtin pf)
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall pf. pf -> Builtin pf
Prim Int32
a
valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall pf. Term -> Builtin pf
Builtin Int32
a
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Int32
a
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (Substitution' a) where
icod_ :: Substitution' a -> S Int32
icod_ Substitution' a
IdS = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Substitution' a
IdS
icod_ (EmptyS Impossible
a) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Impossible -> Substitution' a
EmptyS Impossible
a
icod_ (a
a :# Substitution' a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Substitution' a -> Substitution' a
(:#) a
a Substitution' a
b
icod_ (Strengthen Impossible
a Int
b Substitution' a
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
a Int
b Substitution' a
c
icod_ (Wk Int
a Substitution' a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall a. Int -> Substitution' a -> Substitution' a
Wk Int
a Substitution' a
b
icod_ (Lift Int
a Substitution' a
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall a. Int -> Substitution' a -> Substitution' a
Lift Int
a Substitution' a
b
value :: Int32 -> R (Substitution' a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> StateT St IO (Substitution' a)
valu where
valu :: [Int32]
-> Arrows
(Constant Int32 (Domains (Substitution' a)))
(R (CoDomain (Substitution' a)))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Substitution' a
IdS
valu [Int32
a] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Impossible -> Substitution' a
EmptyS Int32
a
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Substitution' a -> Substitution' a
(:#) Int32
a Int32
b
valu [Int32
0, Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Int32
a Int32
b Int32
c
valu [Int32
1, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Int -> Substitution' a -> Substitution' a
Wk Int32
a Int32
b
valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Int -> Substitution' a -> Substitution' a
Lift Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj Instantiation where
icod_ :: Instantiation -> S Int32
icod_ (Instantiation [Arg ArgName]
a Term
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> Term -> Instantiation
Instantiation [Arg ArgName]
a Term
b
value :: Int32 -> R Instantiation
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN [Arg ArgName] -> Term -> Instantiation
Instantiation
instance EmbPrj Comparison where
icod_ :: Comparison -> S Int32
icod_ Comparison
CmpEq = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Comparison
CmpEq
icod_ Comparison
CmpLeq = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Comparison
CmpLeq
value :: Int32 -> R Comparison
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R Comparison
valu
where
valu :: [a]
-> Arrows
(Constant Int32 (Domains Comparison)) (R (CoDomain Comparison))
valu [] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Comparison
CmpEq
valu [a
0] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Comparison
CmpLeq
valu [a]
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (Judgement a) where
icod_ :: Judgement a -> S Int32
icod_ (HasType a
a Comparison
b Type
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Comparison -> Type -> Judgement a
HasType a
a Comparison
b Type
c
icod_ (IsSort a
a Type
b) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Type -> Judgement a
IsSort a
a Type
b
value :: Int32 -> R (Judgement a)
value = forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase forall {a}. EmbPrj a => [Int32] -> R (Judgement a)
valu
where
valu :: [Int32] -> R (Judgement a)
valu [Int32
a, Int32
b, Int32
c] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Comparison -> Type -> Judgement a
HasType Int32
a Int32
b Int32
c
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Type -> Judgement a
IsSort Int32
a Int32
b
valu [Int32]
_ = forall a. R a
malformed
instance EmbPrj RemoteMetaVariable where
icod_ :: RemoteMetaVariable -> S Int32
icod_ (RemoteMetaVariable Instantiation
a Modality
b Judgement MetaId
c) = forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
RemoteMetaVariable Instantiation
a Modality
b Judgement MetaId
c
value :: Int32 -> R RemoteMetaVariable
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
RemoteMetaVariable