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

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

import Agda.Utils.Functor
import Agda.Utils.Permutation

import Agda.Utils.Impossible

instance EmbPrj a => EmbPrj (Dom a) where
  icod_ :: Dom a -> S Int32
icod_ (Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f) = (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
-> Arrows
     (Domains
        (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom ArgInfo
a Maybe NamedName
c Bool
d Maybe Term
e a
f

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

instance EmbPrj Signature where
  icod_ :: Signature -> S Int32
icod_ (Sig Sections
a Definitions
b RewriteRuleMap
c) = (Sections -> Definitions -> RewriteRuleMap -> Signature)
-> Arrows
     (Domains (Sections -> Definitions -> RewriteRuleMap -> Signature))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Sections -> Definitions -> RewriteRuleMap -> Signature)
-> Int32
-> R (CoDomain
        (Sections -> Definitions -> RewriteRuleMap -> Signature))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Sections -> Definitions -> RewriteRuleMap -> Signature
Sig

instance EmbPrj Section where
  icod_ :: Section -> S Int32
icod_ (Section Telescope
a) = (Telescope -> Section)
-> Arrows (Domains (Telescope -> Section)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Telescope -> Section)
-> Int32 -> R (CoDomain (Telescope -> Section))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Telescope -> Section
Section

instance EmbPrj a => EmbPrj (Tele a) where
  icod_ :: Tele a -> S Int32
icod_ Tele a
EmptyTel        = Tele Any -> Arrows (Domains (Tele Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Tele Any
forall a. Tele a
EmptyTel
  icod_ (ExtendTel a
a Abs (Tele a)
b) = (a -> Abs (Tele a) -> Tele a)
-> Arrows (Domains (a -> Abs (Tele a) -> Tele a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a Abs (Tele a)
b

  value :: Int32 -> R (Tele a)
value = ([Int32] -> R (Tele a)) -> Int32 -> R (Tele a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Tele a)
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 []     = Tele a
-> Arrows
     (Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele 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 Tele a
forall a. Tele a
EmptyTel
    valu [Int32
a, Int32
b] = (a -> Abs (Tele a) -> Tele a)
-> Arrows
     (Constant Int32 (Domains (a -> Abs (Tele a) -> Tele a)))
     (R (CoDomain (a -> Abs (Tele a) -> Tele a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Int32
a Int32
b
    valu [Int32]
_      = StateT St IO (Tele a)
Arrows (Constant Int32 (Domains (Tele a))) (R (CoDomain (Tele a)))
forall a. R a
malformed

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

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

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

instance EmbPrj a => EmbPrj (Elim' a) where
  icod_ :: Elim' a -> S Int32
icod_ (Apply Arg a
a)      = (Arg a -> Elim' a) -> Arrows (Domains (Arg a -> Elim' a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Arg a
a
  icod_ (IApply a
x a
y a
a) = Int32
-> (a -> a -> a -> Elim' a)
-> Arrows (Domains (a -> a -> a -> Elim' a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
x a
y a
a
  icod_ (Proj ProjOrigin
a QName
b)     = Int32
-> (ProjOrigin -> QName -> Elim' Any)
-> Arrows (Domains (ProjOrigin -> QName -> Elim' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 ProjOrigin -> QName -> Elim' Any
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
a QName
b

  value :: Int32 -> R (Elim' a)
value = ([Int32] -> R (Elim' a)) -> Int32 -> R (Elim' a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Elim' a)
forall {a}. EmbPrj a => [Int32] -> R (Elim' a)
valu where
    valu :: [Int32] -> R (Elim' a)
valu [Int32
a]       = (Arg a -> Elim' a)
-> Arrows
     (Constant Int32 (Domains (Arg a -> Elim' a)))
     (R (CoDomain (Arg a -> Elim' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Int32
a
    valu [Int32
0,Int32
x,Int32
y,Int32
a] = (a -> a -> a -> Elim' a)
-> Arrows
     (Constant Int32 (Domains (a -> a -> a -> Elim' a)))
     (R (CoDomain (a -> a -> a -> Elim' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply Int32
x Int32
y Int32
a
    valu [Int32
0, Int32
a, Int32
b] = (ProjOrigin -> QName -> Elim' a)
-> Arrows
     (Constant Int32 (Domains (ProjOrigin -> QName -> Elim' a)))
     (R (CoDomain (ProjOrigin -> QName -> Elim' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ProjOrigin -> QName -> Elim' a
forall a. ProjOrigin -> QName -> Elim' a
Proj Int32
a Int32
b
    valu [Int32]
_         = R (Elim' a)
forall a. R a
malformed

instance EmbPrj I.DataOrRecord where
  icod_ :: DataOrRecord -> S Int32
icod_ = \case
    DataOrRecord
IsData      -> DataOrRecord' Any -> Arrows (Domains (DataOrRecord' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' DataOrRecord' Any
forall p. DataOrRecord' p
IsData
    IsRecord PatternOrCopattern
pm -> (PatternOrCopattern -> DataOrRecord)
-> Arrows (Domains (PatternOrCopattern -> DataOrRecord)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
pm

  value :: Int32 -> R DataOrRecord
value = ([Int32] -> R DataOrRecord) -> Int32 -> R DataOrRecord
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase (([Int32] -> R DataOrRecord) -> Int32 -> R DataOrRecord)
-> ([Int32] -> R DataOrRecord) -> Int32 -> R DataOrRecord
forall a b. (a -> b) -> a -> b
$ \case
    []   -> DataOrRecord
-> Arrows
     (Constant Int32 (Domains DataOrRecord)) (R (CoDomain DataOrRecord))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN DataOrRecord
forall p. DataOrRecord' p
IsData
    [Int32
pm] -> (PatternOrCopattern -> DataOrRecord)
-> Arrows
     (Constant Int32 (Domains (PatternOrCopattern -> DataOrRecord)))
     (R (CoDomain (PatternOrCopattern -> DataOrRecord)))
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 PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord Int32
pm
    [Int32]
_    -> R DataOrRecord
forall a. R a
malformed

instance EmbPrj I.ConHead where
  icod_ :: ConHead -> S Int32
icod_ (ConHead QName
a DataOrRecord
b Induction
c [Arg QName]
d) = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
-> Arrows
     (Domains
        (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead)
-> Int32
-> R (CoDomain
        (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead

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

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

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

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

instance EmbPrj I.Term where
  icod_ :: Term -> S Int32
icod_ (Var     Int
a []) = (Int -> Term) -> Arrows (Domains (Int -> Term)) (S Int32)
forall t.
(ICODE t (IsBase t), 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) = Int32
-> (Int -> Elims -> Term)
-> Arrows (Domains (Int -> Elims -> Term)) (S Int32)
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) = Int32
-> (ArgInfo -> Abs Term -> Term)
-> Arrows (Domains (ArgInfo -> Abs Term -> Term)) (S Int32)
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  ) = Int32
-> (Literal -> Term)
-> Arrows (Domains (Literal -> Term)) (S Int32)
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) = Int32
-> (QName -> Elims -> Term)
-> Arrows (Domains (QName -> Elims -> Term)) (S Int32)
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) = Int32
-> (ConHead -> ConInfo -> Elims -> Term)
-> Arrows (Domains (ConHead -> ConInfo -> Elims -> Term)) (S Int32)
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) = Int32
-> (Dom' Term Type -> Abs Type -> Term)
-> Arrows (Domains (Dom' Term Type -> Abs Type -> Term)) (S Int32)
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) = Int32
-> (MetaId -> Elims -> Term)
-> Arrows (Domains (MetaId -> Elims -> Term)) (S Int32)
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' Term
a  ) = Int32
-> (Sort' Term -> Term)
-> Arrows (Domains (Sort' Term -> Term)) (S Int32)
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 -> Term
Sort Sort' Term
a
  icod_ (DontCare Term
a  ) = Int32
-> (Term -> Term) -> Arrows (Domains (Term -> Term)) (S Int32)
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  ) = Int32
-> (Level -> Term) -> Arrows (Domains (Level -> Term)) (S Int32)
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) = Int32
-> (ArgName -> Elims -> Term)
-> Arrows (Domains (ArgName -> Elims -> Term)) (S Int32)
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 = ([Int32] -> R Term) -> Int32 -> R Term
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R Term
valu where
    valu :: [Int32] -> R Term
valu [Int32
a]       = (Int -> Term)
-> Arrows
     (Constant Int32 (Domains (Int -> Term)))
     (R (CoDomain (Int -> Term)))
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] = (Int -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (Int -> Elims -> Term)))
     (R (CoDomain (Int -> Elims -> Term)))
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] = (ArgInfo -> Abs Term -> Term)
-> Arrows
     (Constant Int32 (Domains (ArgInfo -> Abs Term -> Term)))
     (R (CoDomain (ArgInfo -> Abs Term -> Term)))
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]    = (Literal -> Term)
-> Arrows
     (Constant Int32 (Domains (Literal -> Term)))
     (R (CoDomain (Literal -> Term)))
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] = (QName -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (QName -> Elims -> Term)))
     (R (CoDomain (QName -> Elims -> Term)))
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] = (ConHead -> ConInfo -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (ConHead -> ConInfo -> Elims -> Term)))
     (R (CoDomain (ConHead -> ConInfo -> Elims -> Term)))
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] = (Dom' Term Type -> Abs Type -> Term)
-> Arrows
     (Constant Int32 (Domains (Dom' Term Type -> Abs Type -> Term)))
     (R (CoDomain (Dom' Term Type -> Abs Type -> Term)))
forall t.
(VALU t (IsBase t),
 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] = (MetaId -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (MetaId -> Elims -> Term)))
     (R (CoDomain (MetaId -> Elims -> Term)))
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]    = (Sort' Term -> Term)
-> Arrows
     (Constant Int32 (Domains (Sort' Term -> Term)))
     (R (CoDomain (Sort' Term -> Term)))
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 -> Term
Sort  Int32
a
    valu [Int32
8, Int32
a]    = (Term -> Term)
-> Arrows
     (Constant Int32 (Domains (Term -> Term)))
     (R (CoDomain (Term -> Term)))
forall t.
(VALU t (IsBase t),
 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]    = (Level -> Term)
-> Arrows
     (Constant Int32 (Domains (Level -> Term)))
     (R (CoDomain (Level -> Term)))
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] = (ArgName -> Elims -> Term)
-> Arrows
     (Constant Int32 (Domains (ArgName -> Elims -> Term)))
     (R (CoDomain (ArgName -> Elims -> Term)))
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]
_         = R Term
forall a. R a
malformed

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

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

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

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

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

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

instance EmbPrj Univ where

instance EmbPrj I.Sort where
  icod_ :: Sort' Term -> S Int32
icod_ = \case
    Univ Univ
a Level
b     -> Int32
-> (Univ -> Level -> Sort' Term)
-> Arrows (Domains (Univ -> Level -> Sort' Term)) (S Int32)
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 -> Level -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
a Level
b
    Sort' Term
SizeUniv     -> Int32 -> Sort' Any -> Arrows (Domains (Sort' Any)) (S Int32)
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  Sort' Any
forall t. Sort' t
SizeUniv
    Inf Univ
a Integer
b      -> Int32
-> (Univ -> Integer -> Sort' Any)
-> Arrows (Domains (Univ -> Integer -> Sort' Any)) (S Int32)
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  Univ -> Integer -> Sort' Any
forall t. Univ -> Integer -> Sort' t
Inf Univ
a Integer
b
    PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c -> Int32
-> (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term)
-> Arrows
     (Domains
        (Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4  Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c
    FunSort Sort' Term
a Sort' Term
b  -> Int32
-> (Sort' Term -> Sort' Term -> Sort' Term)
-> Arrows
     (Domains (Sort' Term -> Sort' Term -> Sort' Term)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5  Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort' Term
a Sort' Term
b
    UnivSort Sort' Term
a   -> Int32
-> (Sort' Term -> Sort' Term)
-> Arrows (Domains (Sort' Term -> Sort' Term)) (S Int32)
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  Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort Sort' Term
a
    DefS QName
a Elims
b     -> Int32
-> (QName -> Elims -> Sort' Term)
-> Arrows (Domains (QName -> Elims -> Sort' Term)) (S Int32)
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  QName -> Elims -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
a Elims
b
    Sort' Term
LockUniv     -> Int32 -> Sort' Any -> Arrows (Domains (Sort' Any)) (S Int32)
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  Sort' Any
forall t. Sort' t
LockUniv
    Sort' Term
IntervalUniv -> Int32 -> Sort' Any -> Arrows (Domains (Sort' Any)) (S Int32)
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 Sort' Any
forall t. Sort' t
IntervalUniv
    MetaS MetaId
a Elims
b    -> Int32
-> (MetaId -> Elims -> Sort' Term)
-> Arrows (Domains (MetaId -> Elims -> Sort' Term)) (S Int32)
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 MetaId -> Elims -> Sort' Term
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
a Elims
b
    DummyS ArgName
s     -> Int32
-> (ArgName -> Sort' Any)
-> Arrows (Domains (ArgName -> Sort' Any)) (S Int32)
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 ArgName -> Sort' Any
forall t. ArgName -> Sort' t
DummyS ArgName
s
    Sort' Term
LevelUniv    -> Int32 -> Sort' Any -> Arrows (Domains (Sort' Any)) (S Int32)
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 Sort' Any
forall t. Sort' t
LevelUniv

  value :: Int32 -> R (Sort' Term)
value = ([Int32] -> R (Sort' Term)) -> Int32 -> R (Sort' Term)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Sort' Term)
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] = (Univ -> Level' t -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (Univ -> Level' t -> Sort' t)))
     (R (CoDomain (Univ -> Level' t -> Sort' t)))
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 -> Level' t -> Sort' t
forall t. Univ -> Level' t -> Sort' t
Univ Int32
a Int32
b
    valu [Int32
2]       = Sort' t
-> Arrows
     (Constant Int32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
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' t
forall t. Sort' t
SizeUniv
    valu [Int32
3, Int32
a, Int32
b] = (Univ -> Integer -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (Univ -> Integer -> Sort' t)))
     (R (CoDomain (Univ -> Integer -> Sort' t)))
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 -> Sort' t
forall t. Univ -> Integer -> Sort' t
Inf Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b, Int32
c] = (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)
-> Arrows
     (Constant
        Int32 (Domains (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)))
     (R (CoDomain (Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Int32
a Int32
b Int32
c
    valu [Int32
5, Int32
a, Int32
b] = (Sort' t -> Sort' t -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (Sort' t -> Sort' t -> Sort' t)))
     (R (CoDomain (Sort' t -> Sort' t -> Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort' t -> Sort' t -> Sort' t
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Int32
a Int32
b
    valu [Int32
6, Int32
a]    = (Sort' t -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (Sort' t -> Sort' t)))
     (R (CoDomain (Sort' t -> Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort' t -> Sort' t
forall t. Sort' t -> Sort' t
UnivSort Int32
a
    valu [Int32
7, Int32
a, Int32
b] = (QName -> [Elim' t] -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (QName -> [Elim' t] -> Sort' t)))
     (R (CoDomain (QName -> [Elim' t] -> Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> [Elim' t] -> Sort' t
forall t. QName -> [Elim' t] -> Sort' t
DefS Int32
a Int32
b
    valu [Int32
9]       = Sort' t
-> Arrows
     (Constant Int32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
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' t
forall t. Sort' t
LockUniv
    valu [Int32
10]      = Sort' t
-> Arrows
     (Constant Int32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Sort' t
forall t. Sort' t
IntervalUniv
    valu [Int32
11, Int32
a, Int32
b] = (MetaId -> [Elim' t] -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (MetaId -> [Elim' t] -> Sort' t)))
     (R (CoDomain (MetaId -> [Elim' t] -> Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN MetaId -> [Elim' t] -> Sort' t
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS Int32
a Int32
b
    valu [Int32
12, Int32
s]   = (ArgName -> Sort' t)
-> Arrows
     (Constant Int32 (Domains (ArgName -> Sort' t)))
     (R (CoDomain (ArgName -> Sort' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ArgName -> Sort' t
forall t. ArgName -> Sort' t
DummyS Int32
s
    valu [Int32
13]      = Sort' t
-> Arrows
     (Constant Int32 (Domains (Sort' t))) (R (CoDomain (Sort' t)))
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' t
forall t. Sort' t
LevelUniv
    valu [Int32]
_         = R (Sort' t)
forall a. R a
malformed

instance EmbPrj DisplayForm where
  icod_ :: DisplayForm -> S Int32
icod_ (Display Int
a Elims
b DisplayTerm
c) = (Int -> Elims -> DisplayTerm -> DisplayForm)
-> Arrows
     (Domains (Int -> Elims -> DisplayTerm -> DisplayForm)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Int -> Elims -> DisplayTerm -> DisplayForm)
-> Int32
-> R (CoDomain (Int -> Elims -> DisplayTerm -> DisplayForm))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> Elims -> DisplayTerm -> DisplayForm
Display

instance EmbPrj a => EmbPrj (Open a) where
  icod_ :: Open a -> S Int32
icod_ (OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d) = (CheckpointId
 -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a)
-> Arrows
     (Domains
        (CheckpointId
         -> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing CheckpointId
a Map CheckpointId Substitution
b ModuleNameHash
c a
d

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

instance EmbPrj CheckpointId where
  icod_ :: CheckpointId -> S Int32
icod_ (CheckpointId Int
a) = Int -> S Int32
forall a. EmbPrj a => a -> S Int32
icode Int
a
  value :: Int32 -> R CheckpointId
value Int32
n                = Int -> CheckpointId
CheckpointId (Int -> CheckpointId) -> StateT St IO Int -> R CheckpointId
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Int32 -> StateT St IO Int
forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj DisplayTerm where
  icod_ :: DisplayTerm -> S Int32
icod_ (DTerm'   Term
a Elims
b)   = (Term -> Elims -> DisplayTerm)
-> Arrows (Domains (Term -> Elims -> DisplayTerm)) (S Int32)
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)   = Int32
-> (Term -> Elims -> DisplayTerm)
-> Arrows (Domains (Term -> Elims -> DisplayTerm)) (S Int32)
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) = Int32
-> (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> Arrows
     (Domains (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm))
     (S Int32)
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)   = Int32
-> (QName -> [Elim' DisplayTerm] -> DisplayTerm)
-> Arrows
     (Domains (QName -> [Elim' DisplayTerm] -> DisplayTerm)) (S Int32)
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) = Int32
-> (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> Arrows
     (Domains (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm))
     (S Int32)
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 = ([Int32] -> R DisplayTerm) -> Int32 -> R DisplayTerm
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]       = (Term -> Elims -> DisplayTerm)
-> Arrows
     (Constant Int32 (Domains (Term -> Elims -> DisplayTerm)))
     (R (CoDomain (Term -> Elims -> DisplayTerm)))
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]    = (Term -> Elims -> DisplayTerm)
-> Arrows
     (Constant Int32 (Domains (Term -> Elims -> DisplayTerm)))
     (R (CoDomain (Term -> Elims -> DisplayTerm)))
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] = (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)
-> Arrows
     (Constant
        Int32
        (Domains (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)))
     (R (CoDomain
           (ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm)))
forall t.
(VALU t (IsBase t),
 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]    = (QName -> [Elim' DisplayTerm] -> DisplayTerm)
-> Arrows
     (Constant
        Int32 (Domains (QName -> [Elim' DisplayTerm] -> DisplayTerm)))
     (R (CoDomain (QName -> [Elim' DisplayTerm] -> DisplayTerm)))
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] = (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> Arrows
     (Constant
        Int32
        (Domains (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)))
     (R (CoDomain
           (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)))
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]
_            = R DisplayTerm
forall a. R a
malformed

instance EmbPrj MutualId where
  icod_ :: MutualId -> S Int32
icod_ (MutId Int32
a) = Int32 -> S Int32
forall a. EmbPrj a => a -> S Int32
icode Int32
a
  value :: Int32 -> R MutualId
value Int32
n         = Int32 -> MutualId
MutId (Int32 -> MutualId) -> StateT St IO Int32 -> R MutualId
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Int32 -> StateT St IO Int32
forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj CompKit where
  icod_ :: CompKit -> S Int32
icod_ (CompKit Maybe QName
a Maybe QName
b) = (Maybe QName -> Maybe QName -> CompKit)
-> Arrows
     (Domains (Maybe QName -> Maybe QName -> CompKit)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Maybe QName -> Maybe QName -> CompKit)
-> Int32 -> R (CoDomain (Maybe QName -> Maybe QName -> CompKit))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe QName -> Maybe QName -> CompKit
CompKit

instance EmbPrj Definition where
  icod_ :: Definition -> S Int32
icod_ (Defn ArgInfo
a QName
b Type
c [Polarity]
d [Occurrence]
e NumGeneralizableArgs
f [Maybe Name]
g [LocalDisplayForm]
h MutualId
i CompiledRepresentation
j Maybe QName
k Bool
l Set QName
m Bool
n Bool
o Bool
p Blocked_
blocked Language
r Defn
s) =
    (ArgInfo
 -> QName
 -> Type
 -> [Polarity]
 -> [Occurrence]
 -> NumGeneralizableArgs
 -> [Maybe Name]
 -> [LocalDisplayForm]
 -> MutualId
 -> CompiledRepresentation
 -> Maybe QName
 -> Bool
 -> Set QName
 -> Bool
 -> Bool
 -> Bool
 -> Blocked_
 -> Language
 -> Defn
 -> Definition)
-> Arrows
     (Domains
        (ArgInfo
         -> QName
         -> Type
         -> [Polarity]
         -> [Occurrence]
         -> NumGeneralizableArgs
         -> [Maybe Name]
         -> [LocalDisplayForm]
         -> MutualId
         -> CompiledRepresentation
         -> Maybe QName
         -> Bool
         -> Set QName
         -> Bool
         -> Bool
         -> Bool
         -> Blocked_
         -> Language
         -> Defn
         -> Definition))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 (KillRangeT Type
forall a. KillRange a => KillRangeT a
P.killRange Type
c) [Polarity]
d [Occurrence]
e NumGeneralizableArgs
f [Maybe Name]
g [LocalDisplayForm]
h MutualId
i CompiledRepresentation
j Maybe QName
k Bool
l Set QName
m Bool
n Bool
o Bool
p (Blocked_ -> Blocked_
ossify Blocked_
blocked) Language
r Defn
s
    where
      -- Andreas, 2024-01-02, issue #7044:
      -- After serialization, a definition can never be unblocked,
      -- since all metas are ossified.
      -- Thus, we turn any blocker into 'neverUnblock'.
      ossify :: Blocked_ -> Blocked_
      ossify :: Blocked_ -> Blocked_
ossify = \case
        b :: Blocked_
b@NotBlocked{} -> Blocked_
b
        Blocked Blocker
b () -> Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
neverUnblock ()
  value :: Int32 -> R Definition
value = (ArgInfo
 -> QName
 -> Type
 -> [Polarity]
 -> [Occurrence]
 -> NumGeneralizableArgs
 -> [Maybe Name]
 -> [LocalDisplayForm]
 -> MutualId
 -> CompiledRepresentation
 -> Maybe QName
 -> Bool
 -> Set QName
 -> Bool
 -> Bool
 -> Bool
 -> Blocked_
 -> Language
 -> Defn
 -> Definition)
-> Int32
-> R (CoDomain
        (ArgInfo
         -> QName
         -> Type
         -> [Polarity]
         -> [Occurrence]
         -> NumGeneralizableArgs
         -> [Maybe Name]
         -> [LocalDisplayForm]
         -> MutualId
         -> CompiledRepresentation
         -> Maybe QName
         -> Bool
         -> Set QName
         -> Bool
         -> Bool
         -> Bool
         -> Blocked_
         -> Language
         -> Defn
         -> Definition))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn

instance EmbPrj NotBlocked where
  icod_ :: NotBlocked -> S Int32
icod_ NotBlocked
ReallyNotBlocked = NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NotBlocked' Any
forall t. NotBlocked' t
ReallyNotBlocked
  icod_ (StuckOn Elim' Term
a)      = Int32
-> (Elim' Term -> NotBlocked)
-> Arrows (Domains (Elim' Term -> NotBlocked)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Elim' Term -> NotBlocked
forall t. Elim' t -> NotBlocked' t
StuckOn Elim' Term
a
  icod_ NotBlocked
Underapplied     = Int32
-> NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 NotBlocked' Any
forall t. NotBlocked' t
Underapplied
  icod_ NotBlocked
AbsurdMatch      = Int32
-> NotBlocked' Any -> Arrows (Domains (NotBlocked' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 NotBlocked' Any
forall t. NotBlocked' t
AbsurdMatch
  icod_ (MissingClauses QName
a) = Int32
-> (QName -> NotBlocked' Any)
-> Arrows (Domains (QName -> NotBlocked' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 QName -> NotBlocked' Any
forall t. QName -> NotBlocked' t
MissingClauses QName
a

  value :: Int32 -> R NotBlocked
value = ([Int32] -> R NotBlocked) -> Int32 -> R NotBlocked
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R NotBlocked
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 []     = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
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 NotBlocked' t
forall t. NotBlocked' t
ReallyNotBlocked
    valu [Int32
0, Int32
a] = (Elim' t -> NotBlocked' t)
-> Arrows
     (Constant Int32 (Domains (Elim' t -> NotBlocked' t)))
     (R (CoDomain (Elim' t -> NotBlocked' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Elim' t -> NotBlocked' t
forall t. Elim' t -> NotBlocked' t
StuckOn Int32
a
    valu [Int32
1]    = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NotBlocked' t
forall t. NotBlocked' t
Underapplied
    valu [Int32
2]    = NotBlocked' t
-> Arrows
     (Constant Int32 (Domains (NotBlocked' t)))
     (R (CoDomain (NotBlocked' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NotBlocked' t
forall t. NotBlocked' t
AbsurdMatch
    valu [Int32
3, Int32
a] = (QName -> NotBlocked' t)
-> Arrows
     (Constant Int32 (Domains (QName -> NotBlocked' t)))
     (R (CoDomain (QName -> NotBlocked' t)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> NotBlocked' t
forall t. QName -> NotBlocked' t
MissingClauses Int32
a
    valu [Int32]
_      = StateT St IO (NotBlocked' t)
Arrows
  (Constant Int32 (Domains (NotBlocked' t)))
  (R (CoDomain (NotBlocked' t)))
forall a. R a
malformed

-- Andreas, 2024-01-02, issue #7044.
-- We only serialize 'neverUnblock';
-- other than that, there should not be any blockers left at serialization time.
blockedToMaybe :: Blocked_ -> Maybe NotBlocked
blockedToMaybe :: Blocked_ -> Maybe NotBlocked
blockedToMaybe = \case
  NotBlocked NotBlocked
a ()       -> NotBlocked -> Maybe NotBlocked
forall a. a -> Maybe a
Just NotBlocked
a
  Blocked Blocker
a ()
    | Blocker
a Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> Maybe NotBlocked
forall a. Maybe a
Nothing
    | Bool
otherwise         -> Maybe NotBlocked
forall a. HasCallStack => a
__IMPOSSIBLE__

blockedFromMaybe :: Maybe NotBlocked -> Blocked_
blockedFromMaybe :: Maybe NotBlocked -> Blocked_
blockedFromMaybe = Blocked_
-> (NotBlocked -> Blocked_) -> Maybe NotBlocked -> Blocked_
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
neverUnblock ()) (NotBlocked -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
`NotBlocked` ())

instance EmbPrj Blocked_ where
  icod_ :: Blocked_ -> S Int32
icod_ = Maybe NotBlocked -> S Int32
forall a. EmbPrj a => a -> S Int32
icod_ (Maybe NotBlocked -> S Int32)
-> (Blocked_ -> Maybe NotBlocked) -> Blocked_ -> S Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked_ -> Maybe NotBlocked
blockedToMaybe
  value :: Int32 -> R Blocked_
value = Maybe NotBlocked -> Blocked_
blockedFromMaybe (Maybe NotBlocked -> Blocked_)
-> (Int32 -> StateT St IO (Maybe NotBlocked))
-> Int32
-> R Blocked_
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Int32 -> StateT St IO (Maybe NotBlocked)
forall a. EmbPrj a => Int32 -> R a
value

instance EmbPrj NLPat where
  icod_ :: NLPat -> S Int32
icod_ (PVar Int
a [Arg Int]
b)      = Int32
-> (Int -> [Arg Int] -> NLPat)
-> Arrows (Domains (Int -> [Arg Int] -> NLPat)) (S Int32)
forall t.
(ICODE t (IsBase t), 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)      = Int32
-> (QName -> PElims -> NLPat)
-> Arrows (Domains (QName -> PElims -> NLPat)) (S Int32)
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)      = Int32
-> (ArgInfo -> Abs NLPat -> NLPat)
-> Arrows (Domains (ArgInfo -> Abs NLPat -> NLPat)) (S Int32)
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)       = Int32
-> (Dom NLPType -> Abs NLPType -> NLPat)
-> Arrows (Domains (Dom NLPType -> Abs NLPType -> NLPat)) (S Int32)
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)       = Int32
-> (NLPSort -> NLPat)
-> Arrows (Domains (NLPSort -> NLPat)) (S Int32)
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) = Int32
-> (Int -> PElims -> NLPat)
-> Arrows (Domains (Int -> PElims -> NLPat)) (S Int32)
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)       = Int32
-> (Term -> NLPat) -> Arrows (Domains (Term -> NLPat)) (S Int32)
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 = ([Int32] -> R NLPat) -> Int32 -> R NLPat
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]    = (Int -> [Arg Int] -> NLPat)
-> Arrows
     (Constant Int32 (Domains (Int -> [Arg Int] -> NLPat)))
     (R (CoDomain (Int -> [Arg Int] -> NLPat)))
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]    = (QName -> PElims -> NLPat)
-> Arrows
     (Constant Int32 (Domains (QName -> PElims -> NLPat)))
     (R (CoDomain (QName -> PElims -> NLPat)))
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]    = (ArgInfo -> Abs NLPat -> NLPat)
-> Arrows
     (Constant Int32 (Domains (ArgInfo -> Abs NLPat -> NLPat)))
     (R (CoDomain (ArgInfo -> Abs NLPat -> NLPat)))
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]    = (Dom NLPType -> Abs NLPType -> NLPat)
-> Arrows
     (Constant Int32 (Domains (Dom NLPType -> Abs NLPType -> NLPat)))
     (R (CoDomain (Dom NLPType -> Abs NLPType -> NLPat)))
forall t.
(VALU t (IsBase t),
 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]       = (NLPSort -> NLPat)
-> Arrows
     (Constant Int32 (Domains (NLPSort -> NLPat)))
     (R (CoDomain (NLPSort -> NLPat)))
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]    = (Int -> PElims -> NLPat)
-> Arrows
     (Constant Int32 (Domains (Int -> PElims -> NLPat)))
     (R (CoDomain (Int -> PElims -> NLPat)))
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]       = (Term -> NLPat)
-> Arrows
     (Constant Int32 (Domains (Term -> NLPat)))
     (R (CoDomain (Term -> NLPat)))
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]
_            = R NLPat
forall a. R a
malformed

instance EmbPrj NLPType where
  icod_ :: NLPType -> S Int32
icod_ (NLPType NLPSort
a NLPat
b) = (NLPSort -> NLPat -> NLPType)
-> Arrows (Domains (NLPSort -> NLPat -> NLPType)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (NLPSort -> NLPat -> NLPType)
-> Int32 -> R (CoDomain (NLPSort -> NLPat -> NLPType))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN NLPSort -> NLPat -> NLPType
NLPType

instance EmbPrj NLPSort where
  icod_ :: NLPSort -> S Int32
icod_ (PType NLPat
a)   = Int32
-> (NLPat -> NLPSort)
-> Arrows (Domains (NLPat -> NLPSort)) (S Int32)
forall t.
(ICODE t (IsBase t), 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)   = Int32
-> (NLPat -> NLPSort)
-> Arrows (Domains (NLPat -> NLPSort)) (S Int32)
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)  = Int32
-> (Univ -> Integer -> NLPSort)
-> Arrows (Domains (Univ -> Integer -> NLPSort)) (S Int32)
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   = Int32 -> NLPSort -> Arrows (Domains NLPSort) (S Int32)
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   = Int32 -> NLPSort -> Arrows (Domains NLPSort) (S Int32)
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 = Int32 -> NLPSort -> Arrows (Domains NLPSort) (S Int32)
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)   = Int32
-> (NLPat -> NLPSort)
-> Arrows (Domains (NLPat -> NLPSort)) (S Int32)
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 = Int32 -> NLPSort -> Arrows (Domains NLPSort) (S Int32)
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 = ([Int32] -> R NLPSort) -> Int32 -> R NLPSort
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] = (NLPat -> NLPSort)
-> Arrows
     (Constant Int32 (Domains (NLPat -> NLPSort)))
     (R (CoDomain (NLPat -> NLPSort)))
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] = (NLPat -> NLPSort)
-> Arrows
     (Constant Int32 (Domains (NLPat -> NLPSort)))
     (R (CoDomain (NLPat -> NLPSort)))
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] = (Univ -> Integer -> NLPSort)
-> Arrows
     (Constant Int32 (Domains (Univ -> Integer -> NLPSort)))
     (R (CoDomain (Univ -> Integer -> NLPSort)))
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]    = NLPSort
-> Arrows (Constant Int32 (Domains NLPSort)) (R (CoDomain NLPSort))
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]    = NLPSort
-> Arrows (Constant Int32 (Domains NLPSort)) (R (CoDomain NLPSort))
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]    = NLPSort
-> Arrows (Constant Int32 (Domains NLPSort)) (R (CoDomain NLPSort))
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] = (NLPat -> NLPSort)
-> Arrows
     (Constant Int32 (Domains (NLPat -> NLPSort)))
     (R (CoDomain (NLPat -> NLPSort)))
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]    = NLPSort
-> Arrows (Constant Int32 (Domains NLPSort)) (R (CoDomain NLPSort))
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]
_      = R NLPSort
forall a. R a
malformed

instance EmbPrj RewriteRule where
  icod_ :: RewriteRule -> S Int32
icod_ (RewriteRule QName
a Telescope
b QName
c PElims
d Term
e Type
f Bool
g) = (QName
 -> Telescope
 -> QName
 -> PElims
 -> Term
 -> Type
 -> Bool
 -> RewriteRule)
-> Arrows
     (Domains
        (QName
         -> Telescope
         -> QName
         -> PElims
         -> Term
         -> Type
         -> Bool
         -> RewriteRule))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (QName
 -> Telescope
 -> QName
 -> PElims
 -> Term
 -> Type
 -> Bool
 -> RewriteRule)
-> Int32
-> R (CoDomain
        (QName
         -> Telescope
         -> QName
         -> PElims
         -> Term
         -> Type
         -> Bool
         -> RewriteRule))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule

instance EmbPrj Projection where
  icod_ :: Projection -> S Int32
icod_ (Projection Maybe QName
a QName
b Arg QName
c Int
d ProjLams
e) = (Maybe QName
 -> QName -> Arg QName -> Int -> ProjLams -> Projection)
-> Arrows
     (Domains
        (Maybe QName
         -> QName -> Arg QName -> Int -> ProjLams -> Projection))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Maybe QName
 -> QName -> Arg QName -> Int -> ProjLams -> Projection)
-> Int32
-> R (CoDomain
        (Maybe QName
         -> QName -> Arg QName -> Int -> ProjLams -> Projection))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection

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

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

instance EmbPrj ExtLamInfo where
  icod_ :: ExtLamInfo -> S Int32
icod_ (ExtLamInfo ModuleName
a Bool
b Maybe System
c) = (ModuleName -> Bool -> Maybe System -> ExtLamInfo)
-> Arrows
     (Domains (ModuleName -> Bool -> Maybe System -> ExtLamInfo))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (ModuleName -> Bool -> Maybe System -> ExtLamInfo)
-> Int32
-> R (CoDomain (ModuleName -> Bool -> Maybe System -> ExtLamInfo))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo

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

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

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

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

instance EmbPrj NumGeneralizableArgs where
  icod_ :: NumGeneralizableArgs -> S Int32
icod_ NumGeneralizableArgs
NoGeneralizableArgs       = NumGeneralizableArgs
-> Arrows (Domains NumGeneralizableArgs) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NumGeneralizableArgs
NoGeneralizableArgs
  icod_ (SomeGeneralizableArgs Int
a) = (Int -> NumGeneralizableArgs)
-> Arrows (Domains (Int -> NumGeneralizableArgs)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = ([Int32] -> R NumGeneralizableArgs)
-> Int32 -> R NumGeneralizableArgs
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 []  = NumGeneralizableArgs
-> Arrows
     (Constant Int32 (Domains NumGeneralizableArgs))
     (R (CoDomain NumGeneralizableArgs))
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] = (Int -> NumGeneralizableArgs)
-> Arrows
     (Constant Int32 (Domains (Int -> NumGeneralizableArgs)))
     (R (CoDomain (Int -> NumGeneralizableArgs)))
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]
_   = R NumGeneralizableArgs
Arrows
  (Constant Int32 (Domains NumGeneralizableArgs))
  (R (CoDomain NumGeneralizableArgs))
forall a. R a
malformed

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

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

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

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

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

instance EmbPrj ProjectionLikenessMissing

instance EmbPrj BuiltinSort where
  icod_ :: BuiltinSort -> S Int32
icod_ = \case
    SortUniv  Univ
a      -> Int32
-> (Univ -> BuiltinSort)
-> Arrows (Domains (Univ -> BuiltinSort)) (S Int32)
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      -> Int32
-> (Univ -> BuiltinSort)
-> Arrows (Domains (Univ -> BuiltinSort)) (S Int32)
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 -> Int32 -> BuiltinSort -> Arrows (Domains BuiltinSort) (S Int32)
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    -> Int32 -> BuiltinSort -> Arrows (Domains BuiltinSort) (S Int32)
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 = ([Int32] -> R BuiltinSort) -> Int32 -> R BuiltinSort
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase \case
    [Int32
0, Int32
a] -> (Univ -> BuiltinSort)
-> Arrows
     (Constant Int32 (Domains (Univ -> BuiltinSort)))
     (R (CoDomain (Univ -> BuiltinSort)))
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] -> (Univ -> BuiltinSort)
-> Arrows
     (Constant Int32 (Domains (Univ -> BuiltinSort)))
     (R (CoDomain (Univ -> BuiltinSort)))
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]    -> BuiltinSort
-> Arrows
     (Constant Int32 (Domains BuiltinSort)) (R (CoDomain BuiltinSort))
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]    -> BuiltinSort
-> Arrows
     (Constant Int32 (Domains BuiltinSort)) (R (CoDomain BuiltinSort))
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]
_ -> R BuiltinSort
forall a. R a
malformed

instance EmbPrj Defn where
  icod_ :: Defn -> S Int32
icod_ (Axiom       Bool
a)                                 = Int32
-> (Bool -> Defn) -> Arrows (Domains (Bool -> Defn)) (S Int32)
forall t.
(ICODE t (IsBase t), 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)   = Int32
-> ([Clause]
    -> Maybe CompiledClauses
    -> Maybe SplitTree
    -> [Clause]
    -> FunctionInverse
    -> Maybe [QName]
    -> IsAbstract
    -> Either ProjectionLikenessMissing Projection
    -> Bool
    -> Set FunctionFlag
    -> Maybe Bool
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> Maybe QName
    -> IsOpaque
    -> Defn)
-> Arrows
     (Domains
        ([Clause]
         -> Maybe CompiledClauses
         -> Maybe SplitTree
         -> [Clause]
         -> FunctionInverse
         -> Maybe [QName]
         -> IsAbstract
         -> Either ProjectionLikenessMissing Projection
         -> Bool
         -> Set FunctionFlag
         -> Maybe Bool
         -> Maybe ExtLamInfo
         -> Maybe QName
         -> Maybe QName
         -> IsOpaque
         -> Defn))
     (S Int32)
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' Term
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j)               = Int32
-> (Int
    -> Int
    -> Maybe Clause
    -> [QName]
    -> Sort' Term
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Maybe QName
    -> Maybe QName
    -> Defn)
-> Arrows
     (Domains
        (Int
         -> Int
         -> Maybe Clause
         -> [QName]
         -> Sort' Term
         -> Maybe [QName]
         -> IsAbstract
         -> [QName]
         -> Maybe QName
         -> Maybe QName
         -> Defn))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int
a Int
b Maybe Clause
c [QName]
d Sort' Term
e Maybe [QName]
f IsAbstract
g [QName]
h Maybe QName
i Maybe QName
j
  icod_ (Record      Int
a Maybe Clause
b ConHead
c Bool
d [Dom QName]
e Telescope
f Maybe [QName]
g EtaEquality
h PatternOrCopattern
i Maybe Induction
j Maybe Bool
k IsAbstract
l CompKit
m)         = Int32
-> (Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> Maybe Bool
    -> IsAbstract
    -> CompKit
    -> Defn)
-> Arrows
     (Domains
        (Int
         -> Maybe Clause
         -> ConHead
         -> Bool
         -> [Dom QName]
         -> Telescope
         -> Maybe [QName]
         -> EtaEquality
         -> PatternOrCopattern
         -> Maybe Induction
         -> Maybe Bool
         -> IsAbstract
         -> CompKit
         -> Defn))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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)             = Int32
-> (Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Bool
    -> Bool
    -> Defn)
-> Arrows
     (Domains
        (Int
         -> Int
         -> ConHead
         -> QName
         -> IsAbstract
         -> CompKit
         -> Maybe [QName]
         -> [IsForced]
         -> Maybe [Bool]
         -> Bool
         -> Bool
         -> Defn))
     (S Int32)
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)                       = Int32
-> (IsAbstract
    -> PrimitiveId
    -> [Clause]
    -> FunctionInverse
    -> Maybe CompiledClauses
    -> IsOpaque
    -> Defn)
-> Arrows
     (Domains
        (IsAbstract
         -> PrimitiveId
         -> [Clause]
         -> FunctionInverse
         -> Maybe CompiledClauses
         -> IsOpaque
         -> Defn))
     (S Int32)
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' Term
b)                             = Int32
-> (BuiltinSort -> Sort' Term -> Defn)
-> Arrows (Domains (BuiltinSort -> Sort' Term -> Defn)) (S Int32)
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' Term -> Defn
PrimitiveSort BuiltinSort
a Sort' Term
b
  icod_ AbstractDefn{}                                  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ Defn
GeneralizableVar                                = Int32 -> Defn -> Arrows (Domains Defn) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 Defn
GeneralizableVar
  icod_ DataOrRecSig{}                                  = S Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R Defn
value = ([Int32] -> R Defn) -> Int32 -> R Defn
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]                                        = (Bool -> Defn)
-> Arrows
     (Constant Int32 (Domains (Bool -> Defn)))
     (R (CoDomain (Bool -> Defn)))
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]
                                                       = ([Clause]
 -> Maybe CompiledClauses
 -> Maybe SplitTree
 -> [Clause]
 -> FunctionInverse
 -> Maybe [QName]
 -> IsAbstract
 -> Either ProjectionLikenessMissing Projection
 -> Bool
 -> Set FunctionFlag
 -> Maybe Bool
 -> Maybe ExtLamInfo
 -> Maybe QName
 -> Maybe QName
 -> IsOpaque
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           ([Clause]
            -> Maybe CompiledClauses
            -> Maybe SplitTree
            -> [Clause]
            -> FunctionInverse
            -> Maybe [QName]
            -> IsAbstract
            -> Either ProjectionLikenessMissing Projection
            -> Bool
            -> Set FunctionFlag
            -> Maybe Bool
            -> Maybe ExtLamInfo
            -> Maybe QName
            -> Maybe QName
            -> IsOpaque
            -> Defn)))
     (R (CoDomain
           ([Clause]
            -> Maybe CompiledClauses
            -> Maybe SplitTree
            -> [Clause]
            -> FunctionInverse
            -> Maybe [QName]
            -> IsAbstract
            -> Either ProjectionLikenessMissing Projection
            -> Bool
            -> Set FunctionFlag
            -> Maybe Bool
            -> Maybe ExtLamInfo
            -> Maybe QName
            -> Maybe QName
            -> IsOpaque
            -> Defn)))
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 Maybe Compiled
forall a. Maybe a
Nothing) Int32
a Int32
b Int32
s Int32
u Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l 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]             = (Int
 -> Int
 -> Maybe Clause
 -> [QName]
 -> Sort' Term
 -> Maybe [QName]
 -> IsAbstract
 -> [QName]
 -> Maybe QName
 -> Maybe QName
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (Int
            -> Int
            -> Maybe Clause
            -> [QName]
            -> Sort' Term
            -> Maybe [QName]
            -> IsAbstract
            -> [QName]
            -> Maybe QName
            -> Maybe QName
            -> Defn)))
     (R (CoDomain
           (Int
            -> Int
            -> Maybe Clause
            -> [QName]
            -> Sort' Term
            -> Maybe [QName]
            -> IsAbstract
            -> [QName]
            -> Maybe QName
            -> Maybe QName
            -> Defn)))
forall t.
(VALU t (IsBase t),
 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' Term
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Maybe QName
-> Maybe QName
-> Defn
Datatype Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j
    valu [Int32
3, Int32
a, Int32
b, Int32
c, Int32
d, Int32
e, Int32
f, Int32
g, Int32
h, Int32
i, Int32
j, Int32
k, Int32
l, Int32
m]    = (Int
 -> Maybe Clause
 -> ConHead
 -> Bool
 -> [Dom QName]
 -> Telescope
 -> Maybe [QName]
 -> EtaEquality
 -> PatternOrCopattern
 -> Maybe Induction
 -> Maybe Bool
 -> IsAbstract
 -> CompKit
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (Int
            -> Maybe Clause
            -> ConHead
            -> Bool
            -> [Dom QName]
            -> Telescope
            -> Maybe [QName]
            -> EtaEquality
            -> PatternOrCopattern
            -> Maybe Induction
            -> Maybe Bool
            -> IsAbstract
            -> CompKit
            -> Defn)))
     (R (CoDomain
           (Int
            -> Maybe Clause
            -> ConHead
            -> Bool
            -> [Dom QName]
            -> Telescope
            -> Maybe [QName]
            -> EtaEquality
            -> PatternOrCopattern
            -> Maybe Induction
            -> Maybe Bool
            -> IsAbstract
            -> CompKit
            -> Defn)))
forall t.
(VALU t (IsBase t),
 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]          = (Int
 -> Int
 -> ConHead
 -> QName
 -> IsAbstract
 -> CompKit
 -> Maybe [QName]
 -> [IsForced]
 -> Maybe [Bool]
 -> Bool
 -> Bool
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (Int
            -> Int
            -> ConHead
            -> QName
            -> IsAbstract
            -> CompKit
            -> Maybe [QName]
            -> [IsForced]
            -> Maybe [Bool]
            -> Bool
            -> Bool
            -> Defn)))
     (R (CoDomain
           (Int
            -> Int
            -> ConHead
            -> QName
            -> IsAbstract
            -> CompKit
            -> Maybe [QName]
            -> [IsForced]
            -> Maybe [Bool]
            -> Bool
            -> Bool
            -> Defn)))
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]                         = (IsAbstract
 -> PrimitiveId
 -> [Clause]
 -> FunctionInverse
 -> Maybe CompiledClauses
 -> IsOpaque
 -> Defn)
-> Arrows
     (Constant
        Int32
        (Domains
           (IsAbstract
            -> PrimitiveId
            -> [Clause]
            -> FunctionInverse
            -> Maybe CompiledClauses
            -> IsOpaque
            -> Defn)))
     (R (CoDomain
           (IsAbstract
            -> PrimitiveId
            -> [Clause]
            -> FunctionInverse
            -> Maybe CompiledClauses
            -> IsOpaque
            -> Defn)))
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]                                     = (BuiltinSort -> Sort' Term -> Defn)
-> Arrows
     (Constant Int32 (Domains (BuiltinSort -> Sort' Term -> Defn)))
     (R (CoDomain (BuiltinSort -> Sort' Term -> Defn)))
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' Term -> Defn
PrimitiveSort Int32
a Int32
b
    valu [Int32
7]                                           = Defn -> Arrows (Constant Int32 (Domains Defn)) (R (CoDomain Defn))
forall t.
(VALU t (IsBase t),
 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]
_                                             = R Defn
forall a. R a
malformed

instance EmbPrj LazySplit where
  icod_ :: LazySplit -> S Int32
icod_ LazySplit
StrictSplit = LazySplit -> Arrows (Domains LazySplit) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' LazySplit
StrictSplit
  icod_ LazySplit
LazySplit   = Int32 -> LazySplit -> Arrows (Domains LazySplit) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = ([Int32] -> R LazySplit) -> Int32 -> R LazySplit
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R LazySplit
forall {a}. (Eq a, Num a) => [a] -> R LazySplit
valu where
    valu :: [a]
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
valu []  = LazySplit
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
forall t.
(VALU t (IsBase t),
 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] = LazySplit
-> Arrows
     (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
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]
_   = R LazySplit
Arrows
  (Constant Int32 (Domains LazySplit)) (R (CoDomain LazySplit))
forall a. R a
malformed

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

instance EmbPrj a => EmbPrj (SplitTree' a) where
  icod_ :: SplitTree' a -> S Int32
icod_ (SplittingDone Int
a) = (Int -> SplitTree' Any)
-> Arrows (Domains (Int -> SplitTree' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> SplitTree' Any
forall a. Int -> SplitTree' a
SplittingDone Int
a
  icod_ (SplitAt Arg Int
a LazySplit
b SplitTrees' a
c)   = Int32
-> (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
-> Arrows
     (Domains (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
a LazySplit
b SplitTrees' a
c

  value :: Int32 -> R (SplitTree' a)
value = ([Int32] -> R (SplitTree' a)) -> Int32 -> R (SplitTree' a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (SplitTree' a)
forall {a}. EmbPrj a => [Int32] -> R (SplitTree' a)
valu where
    valu :: [Int32] -> R (SplitTree' a)
valu [Int32
a]          = (Int -> SplitTree' a)
-> Arrows
     (Constant Int32 (Domains (Int -> SplitTree' a)))
     (R (CoDomain (Int -> SplitTree' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> SplitTree' a
forall a. Int -> SplitTree' a
SplittingDone Int32
a
    valu [Int32
0, Int32
a, Int32
b, Int32
c] = (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)
-> Arrows
     (Constant
        Int32
        (Domains (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)))
     (R (CoDomain
           (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Int32
a Int32
b Int32
c
    valu [Int32]
_            = R (SplitTree' a)
forall a. R a
malformed

instance EmbPrj FunctionFlag where
  icod_ :: FunctionFlag -> S Int32
icod_ FunctionFlag
FunStatic       = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
0
  icod_ FunctionFlag
FunInline       = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
1
  icod_ FunctionFlag
FunMacro        = Int32 -> S Int32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int32
2

  value :: Int32 -> R FunctionFlag
value = \case
    Int32
0 -> FunctionFlag -> R FunctionFlag
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunStatic
    Int32
1 -> FunctionFlag -> R FunctionFlag
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunInline
    Int32
2 -> FunctionFlag -> R FunctionFlag
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionFlag
FunMacro
    Int32
_ -> R FunctionFlag
forall a. R a
malformed

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

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

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

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

-- Opaque blocks are serialised in an abbreviated manner: We only need
-- the enclosed definitions (3rd argument) and parent (4th argument) to
-- compute the transitive closure during scope checking, never
-- afterwards.
instance EmbPrj OpaqueBlock where
  icod_ :: OpaqueBlock -> S Int32
icod_ (OpaqueBlock OpaqueId
id HashSet QName
uf HashSet QName
_ Maybe OpaqueId
_ Range
r) =
    (OpaqueId -> [QName] -> Range -> OpaqueBlock)
-> Arrows
     (Domains (OpaqueId -> [QName] -> Range -> OpaqueBlock)) (S Int32)
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 = [QName] -> HashSet QName
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 HashSet QName
forall a. Monoid a => a
mempty Maybe OpaqueId
forall a. Maybe a
Nothing)
    OpaqueId
id (HashSet QName -> [QName]
forall a. HashSet a -> [a]
HashSet.toList HashSet QName
uf) Range
r

  value :: Int32 -> R OpaqueBlock
value = (OpaqueId -> [QName] -> Range -> OpaqueBlock)
-> Int32
-> R (CoDomain (OpaqueId -> [QName] -> Range -> OpaqueBlock))
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 = [QName] -> HashSet QName
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 HashSet QName
forall a. Monoid a => a
mempty Maybe OpaqueId
forall a. Maybe a
Nothing)

instance EmbPrj CompiledClauses where
  icod_ :: CompiledClauses -> S Int32
icod_ (Fail [Arg ArgName]
a)   = ([Arg ArgName] -> CompiledClauses' Any)
-> Arrows
     (Domains ([Arg ArgName] -> CompiledClauses' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> CompiledClauses' Any
forall a. [Arg ArgName] -> CompiledClauses' a
Fail [Arg ArgName]
a
  icod_ (Done [Arg ArgName]
a Term
b) = ([Arg ArgName] -> Term -> CompiledClauses)
-> Arrows
     (Domains ([Arg ArgName] -> Term -> CompiledClauses)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' [Arg ArgName] -> Term -> CompiledClauses
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [Arg ArgName]
a (Term -> Term
forall a. KillRange a => KillRangeT a
P.killRange Term
b)
  icod_ (Case Arg Int
a Case CompiledClauses
b) = Int32
-> (Arg Int -> Case CompiledClauses -> CompiledClauses)
-> Arrows
     (Domains (Arg Int -> Case CompiledClauses -> CompiledClauses))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
a Case CompiledClauses
b

  value :: Int32 -> R CompiledClauses
value = ([Int32] -> R CompiledClauses) -> Int32 -> R CompiledClauses
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R CompiledClauses
forall {a}.
(EmbPrj a, EmbPrj (CompiledClauses' a)) =>
[Int32] -> R (CompiledClauses' a)
valu where
    valu :: [Int32] -> R (CompiledClauses' a)
valu [Int32
a]       = ([Arg ArgName] -> CompiledClauses' a)
-> Arrows
     (Constant Int32 (Domains ([Arg ArgName] -> CompiledClauses' a)))
     (R (CoDomain ([Arg ArgName] -> CompiledClauses' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN [Arg ArgName] -> CompiledClauses' a
forall a. [Arg ArgName] -> CompiledClauses' a
Fail Int32
a
    valu [Int32
a, Int32
b]    = ([Arg ArgName] -> a -> CompiledClauses' a)
-> Arrows
     (Constant
        Int32 (Domains ([Arg ArgName] -> a -> CompiledClauses' a)))
     (R (CoDomain ([Arg ArgName] -> a -> CompiledClauses' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN [Arg ArgName] -> a -> CompiledClauses' a
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b] = (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)
-> Arrows
     (Constant
        Int32
        (Domains
           (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)))
     (R (CoDomain
           (Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Int32
a Int32
b
    valu [Int32]
_         = R (CompiledClauses' a)
forall a. R a
malformed

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

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

instance EmbPrj TermHead where
  icod_ :: TermHead -> S Int32
icod_ TermHead
SortHead     = TermHead -> Arrows (Domains TermHead) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' TermHead
SortHead
  icod_ TermHead
PiHead       = Int32 -> TermHead -> Arrows (Domains TermHead) (S Int32)
forall t.
(ICODE t (IsBase t), 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) = Int32
-> (QName -> TermHead)
-> Arrows (Domains (QName -> TermHead)) (S Int32)
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)  = Int32
-> (Int -> TermHead)
-> Arrows (Domains (Int -> TermHead)) (S Int32)
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  = Int32 -> TermHead -> Arrows (Domains TermHead) (S Int32)
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 = ([Int32] -> R TermHead) -> Int32 -> R TermHead
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 []     = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
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]    = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
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] = (QName -> TermHead)
-> Arrows
     (Constant Int32 (Domains (QName -> TermHead)))
     (R (CoDomain (QName -> TermHead)))
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] = (Int -> TermHead)
-> Arrows
     (Constant Int32 (Domains (Int -> TermHead)))
     (R (CoDomain (Int -> TermHead)))
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]    = TermHead
-> Arrows
     (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
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]
_      = R TermHead
Arrows (Constant Int32 (Domains TermHead)) (R (CoDomain TermHead))
forall a. R a
malformed

instance EmbPrj I.Clause where
  icod_ :: Clause -> S Int32
icod_ (Clause Range
a Range
b Telescope
c NAPs
d Maybe Term
e Maybe (Arg Type)
f Bool
g Maybe Bool
h Maybe Bool
i Maybe Bool
j ExpandedEllipsis
k Maybe ModuleName
l) = (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Bool
 -> Maybe Bool
 -> Maybe Bool
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Maybe ModuleName
 -> Clause)
-> Arrows
     (Domains
        (Range
         -> Range
         -> Telescope
         -> NAPs
         -> Maybe Term
         -> Maybe (Arg Type)
         -> Bool
         -> Maybe Bool
         -> Maybe Bool
         -> Maybe Bool
         -> ExpandedEllipsis
         -> Maybe ModuleName
         -> Clause))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Bool
 -> Maybe Bool
 -> Maybe Bool
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Maybe ModuleName
 -> Clause)
-> Int32
-> R (CoDomain
        (Range
         -> Range
         -> Telescope
         -> NAPs
         -> Maybe Term
         -> Maybe (Arg Type)
         -> Bool
         -> Maybe Bool
         -> Maybe Bool
         -> Maybe Bool
         -> ExpandedEllipsis
         -> Maybe ModuleName
         -> Clause))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause

instance EmbPrj I.ConPatternInfo where
  icod_ :: ConPatternInfo -> S Int32
icod_ (ConPatternInfo PatternInfo
a Bool
b Bool
c Maybe (Arg Type)
d Bool
e) = (PatternInfo
 -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> Arrows
     (Domains
        (PatternInfo
         -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (PatternInfo
 -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo)
-> Int32
-> R (CoDomain
        (PatternInfo
         -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo

instance EmbPrj I.DBPatVar where
  icod_ :: DBPatVar -> S Int32
icod_ (DBPatVar ArgName
a Int
b) = (ArgName -> Int -> DBPatVar)
-> Arrows (Domains (ArgName -> Int -> DBPatVar)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (ArgName -> Int -> DBPatVar)
-> Int32 -> R (CoDomain (ArgName -> Int -> DBPatVar))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ArgName -> Int -> DBPatVar
DBPatVar

instance EmbPrj I.PatternInfo where
  icod_ :: PatternInfo -> S Int32
icod_ (PatternInfo PatOrigin
a [Name]
b) = (PatOrigin -> [Name] -> PatternInfo)
-> Arrows (Domains (PatOrigin -> [Name] -> PatternInfo)) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (PatOrigin -> [Name] -> PatternInfo)
-> Int32 -> R (CoDomain (PatOrigin -> [Name] -> PatternInfo))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN PatOrigin -> [Name] -> PatternInfo
PatternInfo

instance EmbPrj I.PatOrigin where
  icod_ :: PatOrigin -> S Int32
icod_ PatOrigin
PatOSystem  = PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' PatOrigin
PatOSystem
  icod_ PatOrigin
PatOSplit   = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
forall t.
(ICODE t (IsBase t), 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) = Int32
-> (Name -> PatOrigin)
-> Arrows (Domains (Name -> PatOrigin)) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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    = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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     = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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  = Int32 -> PatOrigin -> Arrows (Domains PatOrigin) (S Int32)
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 = ([Int32] -> R PatOrigin) -> Int32 -> R PatOrigin
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 []     = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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] = (Name -> PatOrigin)
-> Arrows
     (Constant Int32 (Domains (Name -> PatOrigin)))
     (R (CoDomain (Name -> PatOrigin)))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]    = PatOrigin
-> Arrows
     (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
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]
_      = R PatOrigin
Arrows
  (Constant Int32 (Domains PatOrigin)) (R (CoDomain PatOrigin))
forall a. R a
malformed

instance EmbPrj a => EmbPrj (I.Pattern' a) where
  icod_ :: Pattern' a -> S Int32
icod_ (VarP PatternInfo
a a
b  ) = Int32
-> (PatternInfo -> a -> Pattern' a)
-> Arrows (Domains (PatternInfo -> a -> Pattern' a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
a a
b
  icod_ (ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c) = Int32
-> (ConHead
    -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a)
-> Arrows
     (Domains
        (ConHead
         -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
a ConPatternInfo
b [NamedArg (Pattern' a)]
c
  icod_ (LitP PatternInfo
a Literal
b  ) = Int32
-> (PatternInfo -> Literal -> Pattern' Any)
-> Arrows
     (Domains (PatternInfo -> Literal -> Pattern' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 PatternInfo -> Literal -> Pattern' Any
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
a Literal
b
  icod_ (DotP PatternInfo
a Term
b  ) = Int32
-> (PatternInfo -> Term -> Pattern' Any)
-> Arrows (Domains (PatternInfo -> Term -> Pattern' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 PatternInfo -> Term -> Pattern' Any
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
a Term
b
  icod_ (ProjP ProjOrigin
a QName
b ) = Int32
-> (ProjOrigin -> QName -> Pattern' Any)
-> Arrows (Domains (ProjOrigin -> QName -> Pattern' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
4 ProjOrigin -> QName -> Pattern' Any
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
a QName
b
  icod_ (IApplyP PatternInfo
a Term
b Term
c a
d) = Int32
-> (PatternInfo -> Term -> Term -> a -> Pattern' a)
-> Arrows
     (Domains (PatternInfo -> Term -> Term -> a -> Pattern' a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 PatternInfo -> Term -> Term -> a -> Pattern' a
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
a Term
b Term
c a
d
  icod_ (DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c) = Int32
-> (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a)
-> Arrows
     (Domains
        (PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
a QName
b [NamedArg (Pattern' a)]
c

  value :: Int32 -> R (Pattern' a)
value = ([Int32] -> R (Pattern' a)) -> Int32 -> R (Pattern' a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Pattern' a)
forall {x}. EmbPrj x => [Int32] -> R (Pattern' x)
valu where
    valu :: [Int32] -> R (Pattern' x)
valu [Int32
0, Int32
a, Int32
b] = (PatternInfo -> x -> Pattern' x)
-> Arrows
     (Constant Int32 (Domains (PatternInfo -> x -> Pattern' x)))
     (R (CoDomain (PatternInfo -> x -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> x -> Pattern' x
forall x. PatternInfo -> x -> Pattern' x
VarP Int32
a Int32
b
    valu [Int32
1, Int32
a, Int32
b, Int32
c] = (ConHead
 -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)
-> Arrows
     (Constant
        Int32
        (Domains
           (ConHead
            -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)))
     (R (CoDomain
           (ConHead
            -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP Int32
a Int32
b Int32
c
    valu [Int32
2, Int32
a, Int32
b] = (PatternInfo -> Literal -> Pattern' x)
-> Arrows
     (Constant Int32 (Domains (PatternInfo -> Literal -> Pattern' x)))
     (R (CoDomain (PatternInfo -> Literal -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> Literal -> Pattern' x
forall x. PatternInfo -> Literal -> Pattern' x
LitP Int32
a Int32
b
    valu [Int32
3, Int32
a, Int32
b] = (PatternInfo -> Term -> Pattern' x)
-> Arrows
     (Constant Int32 (Domains (PatternInfo -> Term -> Pattern' x)))
     (R (CoDomain (PatternInfo -> Term -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> Term -> Pattern' x
forall x. PatternInfo -> Term -> Pattern' x
DotP Int32
a Int32
b
    valu [Int32
4, Int32
a, Int32
b] = (ProjOrigin -> QName -> Pattern' x)
-> Arrows
     (Constant Int32 (Domains (ProjOrigin -> QName -> Pattern' x)))
     (R (CoDomain (ProjOrigin -> QName -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ProjOrigin -> QName -> Pattern' x
forall x. ProjOrigin -> QName -> Pattern' x
ProjP Int32
a Int32
b
    valu [Int32
5, Int32
a, Int32
b, Int32
c, Int32
d] = (PatternInfo -> Term -> Term -> x -> Pattern' x)
-> Arrows
     (Constant
        Int32 (Domains (PatternInfo -> Term -> Term -> x -> Pattern' x)))
     (R (CoDomain (PatternInfo -> Term -> Term -> x -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> Term -> Term -> x -> Pattern' x
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP Int32
a Int32
b Int32
c Int32
d
    valu [Int32
6, Int32
a, Int32
b, Int32
c] = (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)
-> Arrows
     (Constant
        Int32
        (Domains
           (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)))
     (R (CoDomain
           (PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP Int32
a Int32
b Int32
c
    valu [Int32]
_         = R (Pattern' x)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Builtin a) where
  icod_ :: Builtin a -> S Int32
icod_ (Prim    a
a) = (a -> Builtin a) -> Arrows (Domains (a -> Builtin a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Builtin a
forall pf. pf -> Builtin pf
Prim a
a
  icod_ (Builtin Term
a) = Int32
-> (Term -> Builtin Any)
-> Arrows (Domains (Term -> Builtin Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Term -> Builtin Any
forall pf. Term -> Builtin pf
Builtin Term
a
  icod_ (BuiltinRewriteRelations Set QName
a) = Int32
-> (Set QName -> Builtin Any)
-> Arrows (Domains (Set QName -> Builtin Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Set QName -> Builtin Any
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Set QName
a

  value :: Int32 -> R (Builtin a)
value = ([Int32] -> R (Builtin a)) -> Int32 -> R (Builtin a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Builtin a)
forall {pf}. EmbPrj pf => [Int32] -> R (Builtin pf)
valu where
    valu :: [Int32] -> R (Builtin pf)
valu [Int32
a]    = (pf -> Builtin pf)
-> Arrows
     (Constant Int32 (Domains (pf -> Builtin pf)))
     (R (CoDomain (pf -> Builtin pf)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN pf -> Builtin pf
forall pf. pf -> Builtin pf
Prim    Int32
a
    valu [Int32
1, Int32
a] = (Term -> Builtin pf)
-> Arrows
     (Constant Int32 (Domains (Term -> Builtin pf)))
     (R (CoDomain (Term -> Builtin pf)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Term -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Int32
a
    valu [Int32
2, Int32
a] = (Set QName -> Builtin pf)
-> Arrows
     (Constant Int32 (Domains (Set QName -> Builtin pf)))
     (R (CoDomain (Set QName -> Builtin pf)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Set QName -> Builtin pf
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations Int32
a
    valu [Int32]
_      = R (Builtin pf)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Substitution' a) where
  icod_ :: Substitution' a -> S Int32
icod_ Substitution' a
IdS                = Substitution' Any -> Arrows (Domains (Substitution' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Substitution' Any
forall a. Substitution' a
IdS
  icod_ (EmptyS Impossible
a)         = (Impossible -> Substitution' Any)
-> Arrows (Domains (Impossible -> Substitution' Any)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Impossible -> Substitution' Any
forall a. Impossible -> Substitution' a
EmptyS Impossible
a
  icod_ (a
a :# Substitution' a
b)           = (a -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (a -> Substitution' a -> Substitution' a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) a
a Substitution' a
b
  icod_ (Strengthen Impossible
a Int
b Substitution' a
c) = Int32
-> (Impossible -> Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (Impossible -> Int -> Substitution' a -> Substitution' a))
     (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Impossible -> Int -> Substitution' a -> Substitution' a
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Impossible
a Int
b Substitution' a
c
  icod_ (Wk Int
a Substitution' a
b)           = Int32
-> (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (Int -> Substitution' a -> Substitution' a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Wk Int
a Substitution' a
b
  icod_ (Lift Int
a Substitution' a
b)         = Int32
-> (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Domains (Int -> Substitution' a -> Substitution' a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Lift Int
a Substitution' a
b

  value :: Int32 -> R (Substitution' a)
value = ([Int32] -> R (Substitution' a)) -> Int32 -> R (Substitution' a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Substitution' a)
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 []           = Substitution' a
-> Arrows
     (Constant Int32 (Domains (Substitution' a)))
     (R (CoDomain (Substitution' 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 Substitution' a
forall a. Substitution' a
IdS
    valu [Int32
a]          = (Impossible -> Substitution' a)
-> Arrows
     (Constant Int32 (Domains (Impossible -> Substitution' a)))
     (R (CoDomain (Impossible -> Substitution' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Int32
a
    valu [Int32
a, Int32
b]       = (a -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32 (Domains (a -> Substitution' a -> Substitution' a)))
     (R (CoDomain (a -> Substitution' a -> Substitution' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
(:#) Int32
a Int32
b
    valu [Int32
0, Int32
a, Int32
b, Int32
c] = (Impossible -> Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32
        (Domains
           (Impossible -> Int -> Substitution' a -> Substitution' a)))
     (R (CoDomain
           (Impossible -> Int -> Substitution' a -> Substitution' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Impossible -> Int -> Substitution' a -> Substitution' a
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
Strengthen Int32
a Int32
b Int32
c
    valu [Int32
1, Int32
a, Int32
b]    = (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32 (Domains (Int -> Substitution' a -> Substitution' a)))
     (R (CoDomain (Int -> Substitution' a -> Substitution' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Wk Int32
a Int32
b
    valu [Int32
2, Int32
a, Int32
b]    = (Int -> Substitution' a -> Substitution' a)
-> Arrows
     (Constant
        Int32 (Domains (Int -> Substitution' a -> Substitution' a)))
     (R (CoDomain (Int -> Substitution' a -> Substitution' a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
Lift Int32
a Int32
b
    valu [Int32]
_            = StateT St IO (Substitution' a)
Arrows
  (Constant Int32 (Domains (Substitution' a)))
  (R (CoDomain (Substitution' a)))
forall a. R a
malformed

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

instance EmbPrj Comparison where
  icod_ :: Comparison -> S Int32
icod_ Comparison
CmpEq  = Comparison -> Arrows (Domains Comparison) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Comparison
CmpEq
  icod_ Comparison
CmpLeq = Int32 -> Comparison -> Arrows (Domains Comparison) (S Int32)
forall t.
(ICODE t (IsBase t), 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 = ([Int32] -> R Comparison) -> Int32 -> R Comparison
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R Comparison
forall {a}. (Eq a, Num a) => [a] -> R Comparison
valu
    where
    valu :: [a]
-> Arrows
     (Constant Int32 (Domains Comparison)) (R (CoDomain Comparison))
valu []  = Comparison
-> Arrows
     (Constant Int32 (Domains Comparison)) (R (CoDomain Comparison))
forall t.
(VALU t (IsBase t),
 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] = Comparison
-> Arrows
     (Constant Int32 (Domains Comparison)) (R (CoDomain Comparison))
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]
_   = R Comparison
Arrows
  (Constant Int32 (Domains Comparison)) (R (CoDomain Comparison))
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Judgement a) where
  icod_ :: Judgement a -> S Int32
icod_ (HasType a
a Comparison
b Type
c) = (a -> Comparison -> Type -> Judgement a)
-> Arrows
     (Domains (a -> Comparison -> Type -> Judgement a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Comparison -> Type -> Judgement a
forall a. a -> Comparison -> Type -> Judgement a
HasType a
a Comparison
b Type
c
  icod_ (IsSort a
a Type
b)    = (a -> Type -> Judgement a)
-> Arrows (Domains (a -> Type -> Judgement a)) (S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Type -> Judgement a
forall a. a -> Type -> Judgement a
IsSort a
a Type
b

  value :: Int32 -> R (Judgement a)
value = ([Int32] -> R (Judgement a)) -> Int32 -> R (Judgement a)
forall a. EmbPrj a => ([Int32] -> R a) -> Int32 -> R a
vcase [Int32] -> R (Judgement a)
forall {a}. EmbPrj a => [Int32] -> R (Judgement a)
valu
    where
    valu :: [Int32] -> R (Judgement a)
valu [Int32
a, Int32
b, Int32
c] = (a -> Comparison -> Type -> Judgement a)
-> Arrows
     (Constant Int32 (Domains (a -> Comparison -> Type -> Judgement a)))
     (R (CoDomain (a -> Comparison -> Type -> Judgement a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> Comparison -> Type -> Judgement a
forall a. a -> Comparison -> Type -> Judgement a
HasType Int32
a Int32
b Int32
c
    valu [Int32
a, Int32
b]    = (a -> Type -> Judgement a)
-> Arrows
     (Constant Int32 (Domains (a -> Type -> Judgement a)))
     (R (CoDomain (a -> Type -> Judgement a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Int32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN a -> Type -> Judgement a
forall a. a -> Type -> Judgement a
IsSort Int32
a Int32
b
    valu [Int32]
_         = R (Judgement a)
forall a. R a
malformed

instance EmbPrj RemoteMetaVariable where
  icod_ :: RemoteMetaVariable -> S Int32
icod_ (RemoteMetaVariable Instantiation
a Modality
b Judgement MetaId
c) = (Instantiation
 -> Modality -> Judgement MetaId -> RemoteMetaVariable)
-> Arrows
     (Domains
        (Instantiation
         -> Modality -> Judgement MetaId -> RemoteMetaVariable))
     (S Int32)
forall t.
(ICODE t (IsBase t), 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 = (Instantiation
 -> Modality -> Judgement MetaId -> RemoteMetaVariable)
-> Int32
-> R (CoDomain
        (Instantiation
         -> Modality -> Judgement MetaId -> RemoteMetaVariable))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Instantiation -> Modality -> Judgement MetaId -> RemoteMetaVariable
RemoteMetaVariable