{-| Primitive functions, such as addition on builtin integers.
-}
module Agda.TypeChecking.Primitive
       ( module Agda.TypeChecking.Primitive.Base
       , module Agda.TypeChecking.Primitive.Cubical
       , module Agda.TypeChecking.Primitive
       ) where

import Data.Char
import Data.Function (on)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.Text (Text)
import qualified Data.Text as T
import Data.Word

import qualified Agda.Interaction.Options.Lenses as Lens

import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Nat)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic (TermLike(..))
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad as Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Level

import Agda.TypeChecking.Quote (quoteTermWithKit, quoteTypeWithKit, quotingKit)
import Agda.TypeChecking.Primitive.Base
import Agda.TypeChecking.Primitive.Cubical
import Agda.TypeChecking.Warnings

import Agda.Utils.Char
import Agda.Utils.Float
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

-- Haskell type to Agda type

newtype Nat = Nat { Nat -> Integer
unNat :: Integer }
            deriving (Nat -> Nat -> Bool
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c== :: Nat -> Nat -> Bool
Eq, Eq Nat
Eq Nat
-> (Nat -> Nat -> Ordering)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> Ord Nat
Nat -> Nat -> Bool
Nat -> Nat -> Ordering
Nat -> Nat -> Nat
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmax :: Nat -> Nat -> Nat
>= :: Nat -> Nat -> Bool
$c>= :: Nat -> Nat -> Bool
> :: Nat -> Nat -> Bool
$c> :: Nat -> Nat -> Bool
<= :: Nat -> Nat -> Bool
$c<= :: Nat -> Nat -> Bool
< :: Nat -> Nat -> Bool
$c< :: Nat -> Nat -> Bool
compare :: Nat -> Nat -> Ordering
$ccompare :: Nat -> Nat -> Ordering
Ord, Integer -> Nat
Nat -> Nat
Nat -> Nat -> Nat
(Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat)
-> (Nat -> Nat)
-> (Nat -> Nat)
-> (Integer -> Nat)
-> Num Nat
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Nat
$cfromInteger :: Integer -> Nat
signum :: Nat -> Nat
$csignum :: Nat -> Nat
abs :: Nat -> Nat
$cabs :: Nat -> Nat
negate :: Nat -> Nat
$cnegate :: Nat -> Nat
* :: Nat -> Nat -> Nat
$c* :: Nat -> Nat -> Nat
- :: Nat -> Nat -> Nat
$c- :: Nat -> Nat -> Nat
+ :: Nat -> Nat -> Nat
$c+ :: Nat -> Nat -> Nat
Num, Arity -> Nat
Nat -> Arity
Nat -> [Nat]
Nat -> Nat
Nat -> Nat -> [Nat]
Nat -> Nat -> Nat -> [Nat]
(Nat -> Nat)
-> (Nat -> Nat)
-> (Arity -> Nat)
-> (Nat -> Arity)
-> (Nat -> [Nat])
-> (Nat -> Nat -> [Nat])
-> (Nat -> Nat -> [Nat])
-> (Nat -> Nat -> Nat -> [Nat])
-> Enum Nat
forall a.
(a -> a)
-> (a -> a)
-> (Arity -> a)
-> (a -> Arity)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
$cenumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
enumFromTo :: Nat -> Nat -> [Nat]
$cenumFromTo :: Nat -> Nat -> [Nat]
enumFromThen :: Nat -> Nat -> [Nat]
$cenumFromThen :: Nat -> Nat -> [Nat]
enumFrom :: Nat -> [Nat]
$cenumFrom :: Nat -> [Nat]
fromEnum :: Nat -> Arity
$cfromEnum :: Nat -> Arity
toEnum :: Arity -> Nat
$ctoEnum :: Arity -> Nat
pred :: Nat -> Nat
$cpred :: Nat -> Nat
succ :: Nat -> Nat
$csucc :: Nat -> Nat
Enum, Num Nat
Ord Nat
Num Nat -> Ord Nat -> (Nat -> Rational) -> Real Nat
Nat -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Nat -> Rational
$ctoRational :: Nat -> Rational
Real)

-- In GHC > 7.8 deriving Integral causes an unnecessary toInteger
-- warning.
instance Integral Nat where
  toInteger :: Nat -> Integer
toInteger = Nat -> Integer
unNat
  quotRem :: Nat -> Nat -> (Nat, Nat)
quotRem (Nat Integer
a) (Nat Integer
b) = (Integer -> Nat
Nat Integer
q, Integer -> Nat
Nat Integer
r)
    where (Integer
q, Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
a Integer
b

instance TermLike Nat where
  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Nat -> m Nat
traverseTermM Term -> m Term
_ = Nat -> m Nat
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> Nat -> m
foldTerm Term -> m
_      = Nat -> m
forall a. Monoid a => a
mempty

instance Pretty Nat where
  pretty :: Nat -> Doc
pretty = Integer -> Doc
forall a. Pretty a => a -> Doc
pretty (Integer -> Doc) -> (Nat -> Integer) -> Nat -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger

newtype Lvl = Lvl { Lvl -> Integer
unLvl :: Integer }
  deriving (Lvl -> Lvl -> Bool
(Lvl -> Lvl -> Bool) -> (Lvl -> Lvl -> Bool) -> Eq Lvl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lvl -> Lvl -> Bool
$c/= :: Lvl -> Lvl -> Bool
== :: Lvl -> Lvl -> Bool
$c== :: Lvl -> Lvl -> Bool
Eq, Eq Lvl
Eq Lvl
-> (Lvl -> Lvl -> Ordering)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Bool)
-> Op Lvl
-> Op Lvl
-> Ord Lvl
Lvl -> Lvl -> Bool
Lvl -> Lvl -> Ordering
Op Lvl
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Op Lvl
$cmin :: Op Lvl
max :: Op Lvl
$cmax :: Op Lvl
>= :: Lvl -> Lvl -> Bool
$c>= :: Lvl -> Lvl -> Bool
> :: Lvl -> Lvl -> Bool
$c> :: Lvl -> Lvl -> Bool
<= :: Lvl -> Lvl -> Bool
$c<= :: Lvl -> Lvl -> Bool
< :: Lvl -> Lvl -> Bool
$c< :: Lvl -> Lvl -> Bool
compare :: Lvl -> Lvl -> Ordering
$ccompare :: Lvl -> Lvl -> Ordering
Ord)

instance Pretty Lvl where
  pretty :: Lvl -> Doc
pretty = Integer -> Doc
forall a. Pretty a => a -> Doc
pretty (Integer -> Doc) -> (Lvl -> Integer) -> Lvl -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lvl -> Integer
unLvl

class PrimType a where
  primType :: a -> TCM Type

  -- This used to be a catch-all instance `PrimType a => PrimTerm a` which required UndecidableInstances.
  -- Now we declare the instances separately, but enforce the catch-all-ness with a superclass constraint on PrimTerm.
  default primType :: PrimTerm a => a -> TCM Type
  primType a
_ = TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
forall a b. (a -> b) -> a -> b
$ a -> TCMT IO Term
forall a. PrimTerm a => a -> TCMT IO Term
primTerm (a
forall a. HasCallStack => a
undefined :: a)

class PrimType a => PrimTerm a where
  primTerm :: a -> TCM Term

instance (PrimType a, PrimType b) => PrimType (a -> b)
instance (PrimType a, PrimType b) => PrimTerm (a -> b) where
  primTerm :: (a -> b) -> TCMT IO Term
primTerm a -> b
_ = Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> TCM Type -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (a
forall a. HasCallStack => a
undefined :: a) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> b -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (b
forall a. HasCallStack => a
undefined :: b))

instance (PrimType a, PrimType b) => PrimType (a, b)
instance (PrimType a, PrimType b) => PrimTerm (a, b) where
  primTerm :: (a, b) -> TCMT IO Term
primTerm (a, b)
_ = do
    SigmaKit
sigKit <- SigmaKit -> Maybe SigmaKit -> SigmaKit
forall a. a -> Maybe a -> a
fromMaybe SigmaKit
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit)
-> TCMT IO (Maybe SigmaKit) -> TCMT IO SigmaKit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
    let sig :: Term
sig = QName -> Elims -> Term
Def (SigmaKit -> QName
sigmaName SigmaKit
sigKit) []
    Type
a'       <- a -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (a
forall a. HasCallStack => a
undefined :: a)
    Type
b'       <- b -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (b
forall a. HasCallStack => a
undefined :: b)
    Type Level' Term
la  <- Sort' Term -> TCMT IO (Sort' Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort' Term -> TCMT IO (Sort' Term))
-> Sort' Term -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
a'
    Type Level' Term
lb  <- Sort' Term -> TCMT IO (Sort' Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort' Term -> TCMT IO (Sort' Term))
-> Sort' Term -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
b'
    Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
sig TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Level' Term -> Term
Level Level' Term
la)
             TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Level' Term -> Term
Level Level' Term
lb)
             TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a')
             TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Term
nolam (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
b')

instance PrimType Integer
instance PrimTerm Integer where primTerm :: Integer -> TCMT IO Term
primTerm Integer
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger

instance PrimType Word64
instance PrimTerm Word64  where primTerm :: Word64 -> TCMT IO Term
primTerm Word64
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64

instance PrimType Bool
instance PrimTerm Bool    where primTerm :: Bool -> TCMT IO Term
primTerm Bool
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool

instance PrimType Char
instance PrimTerm Char    where primTerm :: Char -> TCMT IO Term
primTerm Char
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar

instance PrimType Double
instance PrimTerm Double  where primTerm :: Double -> TCMT IO Term
primTerm Double
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat

instance PrimType Text
instance PrimTerm Text    where primTerm :: Text -> TCMT IO Term
primTerm Text
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString

instance PrimType Nat
instance PrimTerm Nat     where primTerm :: Nat -> TCMT IO Term
primTerm Nat
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat

instance PrimType Lvl
instance PrimTerm Lvl     where primTerm :: Lvl -> TCMT IO Term
primTerm Lvl
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel

instance PrimType QName
instance PrimTerm QName   where primTerm :: QName -> TCMT IO Term
primTerm QName
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName

instance PrimType MetaId
instance PrimTerm MetaId  where primTerm :: MetaId -> TCMT IO Term
primTerm MetaId
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta

instance PrimType Type
instance PrimTerm Type    where primTerm :: Type -> TCMT IO Term
primTerm Type
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm

instance PrimType Fixity'
instance PrimTerm Fixity' where primTerm :: Fixity' -> TCMT IO Term
primTerm Fixity'
_ = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixity

instance PrimTerm a => PrimType [a]
instance PrimTerm a => PrimTerm [a] where
  primTerm :: [a] -> TCMT IO Term
primTerm [a]
_ = TCMT IO Term -> TCMT IO Term
list (a -> TCMT IO Term
forall a. PrimTerm a => a -> TCMT IO Term
primTerm (a
forall a. HasCallStack => a
undefined :: a))

instance PrimTerm a => PrimType (Maybe a)
instance PrimTerm a => PrimTerm (Maybe a) where
  primTerm :: Maybe a -> TCMT IO Term
primTerm Maybe a
_ = TCMT IO Term -> TCMT IO Term
tMaybe (a -> TCMT IO Term
forall a. PrimTerm a => a -> TCMT IO Term
primTerm (a
forall a. HasCallStack => a
undefined :: a))

instance PrimTerm a => PrimType (IO a)
instance PrimTerm a => PrimTerm (IO a) where
  primTerm :: IO a -> TCMT IO Term
primTerm IO a
_ = TCMT IO Term -> TCMT IO Term
io (a -> TCMT IO Term
forall a. PrimTerm a => a -> TCMT IO Term
primTerm (a
forall a. HasCallStack => a
undefined :: a))

-- From Agda term to Haskell value

class ToTerm a where
  toTerm  :: TCM (a -> Term)
  toTermR :: TCM (a -> ReduceM Term)

  toTermR = (Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (a -> Term) -> a -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((a -> Term) -> a -> ReduceM Term)
-> TCMT IO (a -> Term) -> TCM (a -> ReduceM Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm

instance ToTerm Nat     where toTerm :: TCM (Nat -> Term)
toTerm = (Nat -> Term) -> TCM (Nat -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Nat -> Term) -> TCM (Nat -> Term))
-> (Nat -> Term) -> TCM (Nat -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (Nat -> Literal) -> Nat -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
LitNat (Integer -> Literal) -> (Nat -> Integer) -> Nat -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger
instance ToTerm Word64  where toTerm :: TCM (Word64 -> Term)
toTerm = (Word64 -> Term) -> TCM (Word64 -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Word64 -> Term) -> TCM (Word64 -> Term))
-> (Word64 -> Term) -> TCM (Word64 -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (Word64 -> Literal) -> Word64 -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Literal
LitWord64
instance ToTerm Lvl     where toTerm :: TCM (Lvl -> Term)
toTerm = (Lvl -> Term) -> TCM (Lvl -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Lvl -> Term) -> TCM (Lvl -> Term))
-> (Lvl -> Term) -> TCM (Lvl -> Term)
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level (Level' Term -> Term) -> (Lvl -> Level' Term) -> Lvl -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Level' Term
ClosedLevel (Integer -> Level' Term) -> (Lvl -> Integer) -> Lvl -> Level' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lvl -> Integer
unLvl
instance ToTerm Double  where toTerm :: TCM (Double -> Term)
toTerm = (Double -> Term) -> TCM (Double -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Double -> Term) -> TCM (Double -> Term))
-> (Double -> Term) -> TCM (Double -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (Double -> Literal) -> Double -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Literal
LitFloat
instance ToTerm Char    where toTerm :: TCM (Char -> Term)
toTerm = (Char -> Term) -> TCM (Char -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Char -> Term) -> TCM (Char -> Term))
-> (Char -> Term) -> TCM (Char -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (Char -> Literal) -> Char -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
LitChar
instance ToTerm Text    where toTerm :: TCM (Text -> Term)
toTerm = (Text -> Term) -> TCM (Text -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Text -> Term) -> TCM (Text -> Term))
-> (Text -> Term) -> TCM (Text -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (Text -> Literal) -> Text -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Literal
LitString
instance ToTerm QName   where toTerm :: TCM (QName -> Term)
toTerm = (QName -> Term) -> TCM (QName -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> Term) -> TCM (QName -> Term))
-> (QName -> Term) -> TCM (QName -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (QName -> Literal) -> QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Literal
LitQName
instance ToTerm MetaId  where
  toTerm :: TCM (MetaId -> Term)
toTerm = do
    AbsolutePath
file <- TCMT IO AbsolutePath
forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
getCurrentPath
    (MetaId -> Term) -> TCM (MetaId -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((MetaId -> Term) -> TCM (MetaId -> Term))
-> (MetaId -> Term) -> TCM (MetaId -> Term)
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> (MetaId -> Literal) -> MetaId -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> MetaId -> Literal
LitMeta AbsolutePath
file

instance ToTerm Integer where
  toTerm :: TCM (Integer -> Term)
toTerm = do
    Term
pos     <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos
    Term
negsuc  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerNegSuc
    Nat -> Term
fromNat <- TCM (Nat -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm :: TCM (Nat -> Term)
    let intToTerm :: Integer -> Term
intToTerm = Nat -> Term
fromNat (Nat -> Term) -> (Integer -> Nat) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Integer -> Term
    let fromInt :: Integer -> Term
fromInt Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
pos    [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Integer -> Term
intToTerm Integer
n]
                  | Bool
otherwise = Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
negsuc [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Integer -> Term
intToTerm (-Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)]
    (Integer -> Term) -> TCM (Integer -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Integer -> Term
fromInt

instance ToTerm Bool where
  toTerm :: TCM (Bool -> Term)
toTerm = do
    Term
true  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
    Term
false <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
    (Bool -> Term) -> TCM (Bool -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool -> Term) -> TCM (Bool -> Term))
-> (Bool -> Term) -> TCM (Bool -> Term)
forall a b. (a -> b) -> a -> b
$ \Bool
b -> if Bool
b then Term
true else Term
false

instance ToTerm Term where
  toTerm :: TCM (Term -> Term)
toTerm  = do QuotingKit
kit <- TCM QuotingKit
quotingKit; (Term -> ReduceM Term) -> TCM (Term -> Term)
forall a b. (a -> ReduceM b) -> TCM (a -> b)
runReduceF (QuotingKit -> Term -> ReduceM Term
quoteTermWithKit QuotingKit
kit)
  toTermR :: TCM (Term -> ReduceM Term)
toTermR = do QuotingKit -> Term -> ReduceM Term
quoteTermWithKit (QuotingKit -> Term -> ReduceM Term)
-> TCM QuotingKit -> TCM (Term -> ReduceM Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM QuotingKit
quotingKit;

instance ToTerm Type where
  toTerm :: TCM (Type -> Term)
toTerm  = do QuotingKit
kit <- TCM QuotingKit
quotingKit; (Type -> ReduceM Term) -> TCM (Type -> Term)
forall a b. (a -> ReduceM b) -> TCM (a -> b)
runReduceF (QuotingKit -> Type -> ReduceM Term
quoteTypeWithKit QuotingKit
kit)
  toTermR :: TCM (Type -> ReduceM Term)
toTermR = QuotingKit -> Type -> ReduceM Term
quoteTypeWithKit (QuotingKit -> Type -> ReduceM Term)
-> TCM QuotingKit -> TCM (Type -> ReduceM Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM QuotingKit
quotingKit

instance ToTerm ArgInfo where
  toTerm :: TCM (ArgInfo -> Term)
toTerm = do
    Term
info <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo
    Term
vis  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primVisible
    Term
hid  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHidden
    Term
ins  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInstance
    Term
rel  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevant
    Term
irr  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIrrelevant
    (ArgInfo -> Term) -> TCM (ArgInfo -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ArgInfo -> Term) -> TCM (ArgInfo -> Term))
-> (ArgInfo -> Term) -> TCM (ArgInfo -> Term)
forall a b. (a -> b) -> a -> b
$ \ ArgInfo
i -> Term
info Term -> [Term] -> Term
forall t. Apply t => t -> [Term] -> t
`applys`
      [ case ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i of
          Hiding
NotHidden  -> Term
vis
          Hiding
Hidden     -> Term
hid
          Instance{} -> Term
ins
      , case ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
i of
          Relevance
Relevant   -> Term
rel
          Relevance
Irrelevant -> Term
irr
          Relevance
NonStrict  -> Term
rel
      ]

instance ToTerm Fixity' where
  toTerm :: TCM (Fixity' -> Term)
toTerm = ((Fixity -> Term) -> (Fixity' -> Fixity) -> Fixity' -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fixity' -> Fixity
theFixity) ((Fixity -> Term) -> Fixity' -> Term)
-> TCMT IO (Fixity -> Term) -> TCM (Fixity' -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Fixity -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm

instance ToTerm Fixity where
  toTerm :: TCMT IO (Fixity -> Term)
toTerm = do
    FixityLevel -> Term
lToTm  <- TCM (FixityLevel -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Associativity -> Term
aToTm  <- TCM (Associativity -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Term
fixity <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixityFixity
    (Fixity -> Term) -> TCMT IO (Fixity -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Fixity -> Term) -> TCMT IO (Fixity -> Term))
-> (Fixity -> Term) -> TCMT IO (Fixity -> Term)
forall a b. (a -> b) -> a -> b
$ \ Fixity{fixityAssoc :: Fixity -> Associativity
fixityAssoc = Associativity
a, fixityLevel :: Fixity -> FixityLevel
fixityLevel = FixityLevel
l} ->
      Term
fixity Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Associativity -> Term
aToTm Associativity
a), Term -> Arg Term
forall a. a -> Arg a
defaultArg (FixityLevel -> Term
lToTm FixityLevel
l)]

instance ToTerm Associativity where
  toTerm :: TCM (Associativity -> Term)
toTerm = do
    Term
lassoc <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocLeft
    Term
rassoc <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocRight
    Term
nassoc <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocNon
    (Associativity -> Term) -> TCM (Associativity -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Associativity -> Term) -> TCM (Associativity -> Term))
-> (Associativity -> Term) -> TCM (Associativity -> Term)
forall a b. (a -> b) -> a -> b
$ \ Associativity
a ->
      case Associativity
a of
        Associativity
NonAssoc   -> Term
nassoc
        Associativity
LeftAssoc  -> Term
lassoc
        Associativity
RightAssoc -> Term
rassoc

instance ToTerm FixityLevel where
  toTerm :: TCM (FixityLevel -> Term)
toTerm = do
    (Double -> Term
iToTm :: PrecedenceLevel -> Term) <- TCM (Double -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Term
related   <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecRelated
    Term
unrelated <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecUnrelated
    (FixityLevel -> Term) -> TCM (FixityLevel -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((FixityLevel -> Term) -> TCM (FixityLevel -> Term))
-> (FixityLevel -> Term) -> TCM (FixityLevel -> Term)
forall a b. (a -> b) -> a -> b
$ \ FixityLevel
p ->
      case FixityLevel
p of
        FixityLevel
Unrelated -> Term
unrelated
        Related Double
n -> Term
related Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Double -> Term
iToTm Double
n]

instance (ToTerm a, ToTerm b) => ToTerm (a, b) where
  toTerm :: TCM ((a, b) -> Term)
toTerm = do
    SigmaKit
sigKit <- SigmaKit -> Maybe SigmaKit -> SigmaKit
forall a. a -> Maybe a -> a
fromMaybe SigmaKit
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit)
-> TCMT IO (Maybe SigmaKit) -> TCMT IO SigmaKit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
    let con :: Term
con = ConHead -> ConInfo -> Elims -> Term
Con (SigmaKit -> ConHead
sigmaCon SigmaKit
sigKit) ConInfo
ConOSystem []
    a -> Term
fromA <- TCM (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    b -> Term
fromB <- TCM (b -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    ((a, b) -> Term) -> TCM ((a, b) -> Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((a, b) -> Term) -> TCM ((a, b) -> Term))
-> ((a, b) -> Term) -> TCM ((a, b) -> Term)
forall a b. (a -> b) -> a -> b
$ \ (a
a, b
b) -> Term
con Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (Term -> Arg Term) -> [Term] -> Args
forall a b. (a -> b) -> [a] -> [b]
map Term -> Arg Term
forall a. a -> Arg a
defaultArg [a -> Term
fromA a
a, b -> Term
fromB b
b]

-- | @buildList A ts@ builds a list of type @List A@. Assumes that the terms
--   @ts@ all have type @A@.
buildList :: TCM ([Term] -> Term)
buildList :: TCM ([Term] -> Term)
buildList = do
    Term
nil'  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil
    Term
cons' <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons
    let nil :: Term
nil       = Term
nil'
        cons :: Term -> Term -> Term
cons Term
x Term
xs = Term
cons' Term -> [Term] -> Term
forall t. Apply t => t -> [Term] -> t
`applys` [Term
x, Term
xs]
    ([Term] -> Term) -> TCM ([Term] -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Term] -> Term) -> TCM ([Term] -> Term))
-> ([Term] -> Term) -> TCM ([Term] -> Term)
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Term -> Term -> Term
cons Term
nil

instance ToTerm a => ToTerm [a] where
  toTerm :: TCM ([a] -> Term)
toTerm = do
    [Term] -> Term
mkList <- TCM ([Term] -> Term)
buildList
    a -> Term
fromA  <- TCM (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    ([a] -> Term) -> TCM ([a] -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (([a] -> Term) -> TCM ([a] -> Term))
-> ([a] -> Term) -> TCM ([a] -> Term)
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
mkList ([Term] -> Term) -> ([a] -> [Term]) -> [a] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Term) -> [a] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map a -> Term
fromA

instance ToTerm a => ToTerm (Maybe a) where
  toTerm :: TCM (Maybe a -> Term)
toTerm = do
    Term
nothing <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing
    Term
just    <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust
    a -> Term
fromA   <- TCM (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    (Maybe a -> Term) -> TCM (Maybe a -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe a -> Term) -> TCM (Maybe a -> Term))
-> (Maybe a -> Term) -> TCM (Maybe a -> Term)
forall a b. (a -> b) -> a -> b
$ Term -> (a -> Term) -> Maybe a -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
nothing (Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
just (Term -> Term) -> (a -> Term) -> a -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Term
fromA)

-- From Haskell value to Agda term

type FromTermFunction a = Arg Term ->
                          ReduceM (Reduced (MaybeReduced (Arg Term)) a)

class FromTerm a where
  fromTerm :: TCM (FromTermFunction a)

instance FromTerm Integer where
  fromTerm :: TCM (FromTermFunction Integer)
fromTerm = do
    Con ConHead
pos ConInfo
_    [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos
    Con ConHead
negsuc ConInfo
_ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerNegSuc
    FromTermFunction Nat
toNat         <- TCM (FromTermFunction Nat)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm :: TCM (FromTermFunction Nat)
    FromTermFunction Integer -> TCM (FromTermFunction Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (FromTermFunction Integer -> TCM (FromTermFunction Integer))
-> FromTermFunction Integer -> TCM (FromTermFunction Integer)
forall a b. (a -> b) -> a -> b
$ \ Arg Term
v -> do
      Blocked (Arg Term)
b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
v
      let v' :: Arg Term
v'  = Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b
          arg :: Term -> Arg Term
arg = (Term -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
v')
      case Arg Term -> Term
forall e. Arg e -> e
unArg (Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b) of
        Con ConHead
c ConInfo
ci [Apply Arg Term
u]
          | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
pos    ->
            ReduceM (Reduced (MaybeReduced (Arg Term)) Nat)
-> (MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
-> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction Nat
toNat Arg Term
u)
              (\ MaybeReduced (Arg Term)
u' -> Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced (Arg Term -> MaybeReduced (Arg Term))
-> Arg Term -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
arg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term) -> Arg Term
forall a. MaybeReduced a -> a
ignoreReduced MaybeReduced (Arg Term)
u']) ((Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a b. (a -> b) -> a -> b
$ \ Nat
n ->
            Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a b. (a -> b) -> a -> b
$ Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n
          | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
negsuc ->
            ReduceM (Reduced (MaybeReduced (Arg Term)) Nat)
-> (MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
-> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction Nat
toNat Arg Term
u)
              (\ MaybeReduced (Arg Term)
u' -> Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced (Arg Term -> MaybeReduced (Arg Term))
-> Arg Term -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
arg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term) -> Arg Term
forall a. MaybeReduced a -> a
ignoreReduced MaybeReduced (Arg Term)
u']) ((Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> (Nat -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a b. (a -> b) -> a -> b
$ \ Nat
n ->
            Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> Integer -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a b. (a -> b) -> a -> b
$ Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Integer) -> Nat -> Integer
forall a b. (a -> b) -> a -> b
$ -Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
        Term
_ -> Reduced (MaybeReduced (Arg Term)) Integer
-> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) Integer
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer))
-> Reduced (MaybeReduced (Arg Term)) Integer
-> ReduceM (Reduced (MaybeReduced (Arg Term)) Integer)
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term)
-> Reduced (MaybeReduced (Arg Term)) Integer
forall no yes. no -> Reduced no yes
NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
b)

instance FromTerm Nat where
  fromTerm :: TCM (FromTermFunction Nat)
fromTerm = (Literal -> Maybe Nat) -> TCM (FromTermFunction Nat)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe Nat) -> TCM (FromTermFunction Nat))
-> (Literal -> Maybe Nat) -> TCM (FromTermFunction Nat)
forall a b. (a -> b) -> a -> b
$ \case
    LitNat Integer
n -> Nat -> Maybe Nat
forall a. a -> Maybe a
Just (Nat -> Maybe Nat) -> Nat -> Maybe Nat
forall a b. (a -> b) -> a -> b
$ Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
n
    Literal
_ -> Maybe Nat
forall a. Maybe a
Nothing

instance FromTerm Word64 where
  fromTerm :: TCM (FromTermFunction Word64)
fromTerm = (Literal -> Maybe Word64) -> TCM (FromTermFunction Word64)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe Word64) -> TCM (FromTermFunction Word64))
-> (Literal -> Maybe Word64) -> TCM (FromTermFunction Word64)
forall a b. (a -> b) -> a -> b
$ \ case
    LitWord64 Word64
n -> Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
n
    Literal
_ -> Maybe Word64
forall a. Maybe a
Nothing

instance FromTerm Lvl where
  fromTerm :: TCM (FromTermFunction Lvl)
fromTerm = (Term -> Maybe Lvl) -> TCM (FromTermFunction Lvl)
forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
fromReducedTerm ((Term -> Maybe Lvl) -> TCM (FromTermFunction Lvl))
-> (Term -> Maybe Lvl) -> TCM (FromTermFunction Lvl)
forall a b. (a -> b) -> a -> b
$ \case
    Level (ClosedLevel Integer
n) -> Lvl -> Maybe Lvl
forall a. a -> Maybe a
Just (Lvl -> Maybe Lvl) -> Lvl -> Maybe Lvl
forall a b. (a -> b) -> a -> b
$ Integer -> Lvl
Lvl Integer
n
    Term
_ -> Maybe Lvl
forall a. Maybe a
Nothing

instance FromTerm Double where
  fromTerm :: TCM (FromTermFunction Double)
fromTerm = (Literal -> Maybe Double) -> TCM (FromTermFunction Double)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe Double) -> TCM (FromTermFunction Double))
-> (Literal -> Maybe Double) -> TCM (FromTermFunction Double)
forall a b. (a -> b) -> a -> b
$ \case
    LitFloat Double
x -> Double -> Maybe Double
forall a. a -> Maybe a
Just Double
x
    Literal
_ -> Maybe Double
forall a. Maybe a
Nothing

instance FromTerm Char where
  fromTerm :: TCM (FromTermFunction Char)
fromTerm = (Literal -> Maybe Char) -> TCM (FromTermFunction Char)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe Char) -> TCM (FromTermFunction Char))
-> (Literal -> Maybe Char) -> TCM (FromTermFunction Char)
forall a b. (a -> b) -> a -> b
$ \case
    LitChar Char
c -> Char -> Maybe Char
forall a. a -> Maybe a
Just Char
c
    Literal
_ -> Maybe Char
forall a. Maybe a
Nothing

instance FromTerm Text where
  fromTerm :: TCM (FromTermFunction Text)
fromTerm = (Literal -> Maybe Text) -> TCM (FromTermFunction Text)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe Text) -> TCM (FromTermFunction Text))
-> (Literal -> Maybe Text) -> TCM (FromTermFunction Text)
forall a b. (a -> b) -> a -> b
$ \case
    LitString Text
s -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
s
    Literal
_ -> Maybe Text
forall a. Maybe a
Nothing

instance FromTerm QName where
  fromTerm :: TCM (FromTermFunction QName)
fromTerm = (Literal -> Maybe QName) -> TCM (FromTermFunction QName)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe QName) -> TCM (FromTermFunction QName))
-> (Literal -> Maybe QName) -> TCM (FromTermFunction QName)
forall a b. (a -> b) -> a -> b
$ \case
    LitQName QName
x -> QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x
    Literal
_ -> Maybe QName
forall a. Maybe a
Nothing

instance FromTerm MetaId where
  fromTerm :: TCM (FromTermFunction MetaId)
fromTerm = (Literal -> Maybe MetaId) -> TCM (FromTermFunction MetaId)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe MetaId) -> TCM (FromTermFunction MetaId))
-> (Literal -> Maybe MetaId) -> TCM (FromTermFunction MetaId)
forall a b. (a -> b) -> a -> b
$ \case
    LitMeta AbsolutePath
_ MetaId
x -> MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x
    Literal
_ -> Maybe MetaId
forall a. Maybe a
Nothing

instance FromTerm Bool where
    fromTerm :: TCM (FromTermFunction Bool)
fromTerm = do
        Term
true  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
        Term
false <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
        (Term -> Maybe Bool) -> TCM (FromTermFunction Bool)
forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
fromReducedTerm ((Term -> Maybe Bool) -> TCM (FromTermFunction Bool))
-> (Term -> Maybe Bool) -> TCM (FromTermFunction Bool)
forall a b. (a -> b) -> a -> b
$ \case
            Term
t   | Term
t Term -> Term -> Bool
=?= Term
true  -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                | Term
t Term -> Term -> Bool
=?= Term
false -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                | Bool
otherwise   -> Maybe Bool
forall a. Maybe a
Nothing
        where
            Term
a =?= :: Term -> Term -> Bool
=?= Term
b = Term
a Term -> Term -> Bool
=== Term
b
            Def QName
x [] === :: Term -> Term -> Bool
=== Def QName
y []   = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
            Con ConHead
x ConInfo
_ [] === Con ConHead
y ConInfo
_ [] = ConHead
x ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
y
            Var Arity
n [] === Var Arity
m []   = Arity
n Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
m
            Term
_        === Term
_          = Bool
False

instance (ToTerm a, FromTerm a) => FromTerm [a] where
  fromTerm :: TCM (FromTermFunction [a])
fromTerm = do
    ConHead
nil   <- Term -> ConHead
isCon (Term -> ConHead) -> TCMT IO Term -> TCMT IO ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil
    ConHead
cons  <- Term -> ConHead
isCon (Term -> ConHead) -> TCMT IO Term -> TCMT IO ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons
    FromTermFunction a
toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    ConHead
-> ConHead
-> FromTermFunction a
-> (a -> Term)
-> FromTermFunction [a]
forall {a}.
ConHead
-> ConHead
-> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
-> (a -> Term)
-> Arg Term
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
mkList ConHead
nil ConHead
cons FromTermFunction a
toA ((a -> Term) -> FromTermFunction [a])
-> TCMT IO (a -> Term) -> TCM (FromTermFunction [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    where
      isCon :: Term -> ConHead
isCon (Lam ArgInfo
_ Abs Term
b)   = Term -> ConHead
isCon (Term -> ConHead) -> Term -> ConHead
forall a b. (a -> b) -> a -> b
$ Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
b
      isCon (Con ConHead
c ConInfo
_ Elims
_) = ConHead
c
      isCon Term
v           = ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__

      mkList :: ConHead
-> ConHead
-> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
-> (a -> Term)
-> Arg Term
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
mkList ConHead
nil ConHead
cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
toA a -> Term
fromA Arg Term
t = do
        Blocked (Arg Term)
b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
        let t :: Arg Term
t = Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b
        let arg :: Term -> Arg Term
arg = (Term -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
t)
        case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t of
          Con ConHead
c ConInfo
ci []
            | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
nil  -> Reduced (MaybeReduced (Arg Term)) [a]
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) [a]
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> Reduced (MaybeReduced (Arg Term)) [a]
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a b. (a -> b) -> a -> b
$ Simplification -> [a] -> Reduced (MaybeReduced (Arg Term)) [a]
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
NoSimplification []
          Con ConHead
c ConInfo
ci Elims
es
            | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
cons, Just [Arg Term
x,Arg Term
xs] <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
-> (a -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
toA Arg Term
x)
                  (\MaybeReduced (Arg Term)
x' -> Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced (Arg Term -> MaybeReduced (Arg Term))
-> Arg Term -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
arg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [MaybeReduced (Arg Term) -> Arg Term
forall a. MaybeReduced a -> a
ignoreReduced MaybeReduced (Arg Term)
x',Arg Term
xs])) ((a -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> (a -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a b. (a -> b) -> a -> b
$ \a
y ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
-> (MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
-> ([a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind
                  (ConHead
-> ConHead
-> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
-> (a -> Term)
-> Arg Term
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
mkList ConHead
nil ConHead
cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
toA a -> Term
fromA Arg Term
xs)
                  ((Arg Term -> Arg Term)
-> MaybeReduced (Arg Term) -> MaybeReduced (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg Term -> Arg Term)
 -> MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
-> (Arg Term -> Arg Term)
-> MaybeReduced (Arg Term)
-> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ \Arg Term
xs' -> Term -> Arg Term
arg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ a -> Term
fromA a
y, Arg Term
xs'])) (([a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> ([a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a b. (a -> b) -> a -> b
$ \[a]
ys ->
              [a] -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys)
          Term
_ -> Reduced (MaybeReduced (Arg Term)) [a]
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) [a]
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) [a]))
-> Reduced (MaybeReduced (Arg Term)) [a]
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term) -> Reduced (MaybeReduced (Arg Term)) [a]
forall no yes. no -> Reduced no yes
NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
b)

instance FromTerm a => FromTerm (Maybe a) where
  fromTerm :: TCM (FromTermFunction (Maybe a))
fromTerm = do
    ConHead
nothing <- Term -> ConHead
isCon (Term -> ConHead) -> TCMT IO Term -> TCMT IO ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing
    ConHead
just    <- Term -> ConHead
isCon (Term -> ConHead) -> TCMT IO Term -> TCMT IO ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust
    FromTermFunction a
toA     <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    FromTermFunction (Maybe a) -> TCM (FromTermFunction (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return (FromTermFunction (Maybe a) -> TCM (FromTermFunction (Maybe a)))
-> FromTermFunction (Maybe a) -> TCM (FromTermFunction (Maybe a))
forall a b. (a -> b) -> a -> b
$ \ Arg Term
t -> do
      let arg :: Term -> Arg Term
arg = (Term -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
t)
      Blocked (Arg Term)
b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
      let t :: Arg Term
t = Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b
      case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t of
        Con ConHead
c ConInfo
ci []
          | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
nothing -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
-> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) (Maybe a)
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
-> Reduced (MaybeReduced (Arg Term)) (Maybe a)
-> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall a b. (a -> b) -> a -> b
$ Simplification
-> Maybe a -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
NoSimplification Maybe a
forall a. Maybe a
Nothing
        Con ConHead
c ConInfo
ci Elims
es
          | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
just, Just [Arg Term
x] <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
            ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReduced (Arg Term))
-> (a -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
-> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
x)
              (\ MaybeReduced (Arg Term)
x' -> Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced (Arg Term -> MaybeReduced (Arg Term))
-> Arg Term -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
arg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (MaybeReduced (Arg Term) -> Arg Term
forall a. MaybeReduced a -> a
ignoreReduced MaybeReduced (Arg Term)
x')])
              (Maybe a -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Maybe a -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
-> (a -> Maybe a)
-> a
-> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just)
        Term
_ -> Reduced (MaybeReduced (Arg Term)) (Maybe a)
-> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) (Maybe a)
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a)))
-> Reduced (MaybeReduced (Arg Term)) (Maybe a)
-> ReduceM (Reduced (MaybeReduced (Arg Term)) (Maybe a))
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term)
-> Reduced (MaybeReduced (Arg Term)) (Maybe a)
forall no yes. no -> Reduced no yes
NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
b)

    where
      isCon :: Term -> ConHead
isCon (Lam ArgInfo
_ Abs Term
b)   = Term -> ConHead
isCon (Term -> ConHead) -> Term -> ConHead
forall a b. (a -> b) -> a -> b
$ Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
b
      isCon (Con ConHead
c ConInfo
_ Elims
_) = ConHead
c
      isCon Term
v           = ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__


fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
fromReducedTerm :: forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
fromReducedTerm Term -> Maybe a
f = FromTermFunction a -> TCMT IO (FromTermFunction a)
forall (m :: * -> *) a. Monad m => a -> m a
return (FromTermFunction a -> TCMT IO (FromTermFunction a))
-> FromTermFunction a -> TCMT IO (FromTermFunction a)
forall a b. (a -> b) -> a -> b
$ \Arg Term
t -> do
    Blocked (Arg Term)
b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
    case Term -> Maybe a
f (Term -> Maybe a) -> Term -> Maybe a
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b) of
        Just a
x  -> Reduced (MaybeReduced (Arg Term)) a
-> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) a
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
-> Reduced (MaybeReduced (Arg Term)) a
-> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
forall a b. (a -> b) -> a -> b
$ Simplification -> a -> Reduced (MaybeReduced (Arg Term)) a
forall no yes. Simplification -> yes -> Reduced no yes
YesReduction Simplification
NoSimplification a
x
        Maybe a
Nothing -> Reduced (MaybeReduced (Arg Term)) a
-> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced (MaybeReduced (Arg Term)) a
 -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
-> Reduced (MaybeReduced (Arg Term)) a
-> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term) -> Reduced (MaybeReduced (Arg Term)) a
forall no yes. no -> Reduced no yes
NoReduction (Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
b)

fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral :: forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral Literal -> Maybe a
f = (Term -> Maybe a) -> TCM (FromTermFunction a)
forall a. (Term -> Maybe a) -> TCM (FromTermFunction a)
fromReducedTerm ((Term -> Maybe a) -> TCM (FromTermFunction a))
-> (Term -> Maybe a) -> TCM (FromTermFunction a)
forall a b. (a -> b) -> a -> b
$ \case
    Lit Literal
lit -> Literal -> Maybe a
f Literal
lit
    Term
_       -> Maybe a
forall a. Maybe a
Nothing

-- | @mkPrimInjective@ takes two Set0 @a@ and @b@ and a function @f@ of type
--   @a -> b@ and outputs a primitive internalizing the fact that @f@ is injective.
mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
a Type
b QName
qn = do
  -- Define the type
  QName
eqName <- TCM QName
primEqualityName
  let lvl0 :: Level' Term
lvl0     = Integer -> Level' Term
ClosedLevel Integer
0
  let eq :: Type -> TCMT IO Term -> TCMT IO Term -> TCM Type
eq Type
a TCMT IO Term
t TCMT IO Term
u = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
Type Level' Term
lvl0) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def QName
eqName []) TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Level' Term -> Term
Level Level' Term
lvl0)
                                TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
t TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
u
  let f :: TCMT IO Term
f    = Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def QName
qn [])
  Type
ty <- ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"t" (Type -> TCM Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
a) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"u" (Type -> TCM Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
a) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
              (Type -> TCMT IO Term -> TCMT IO Term -> TCM Type
eq Type
b (TCMT IO Term
f TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
1) (TCMT IO Term
f TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0))
          TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Type -> TCMT IO Term -> TCMT IO Term -> TCM Type
eq Type
a (      Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
1) (      Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0))

    -- Get the constructor corresponding to BUILTIN REFL
  Arg Term -> Term
refl <- TCM (Arg Term -> Term)
getRefl

  -- Implementation: when the equality argument reduces to refl so does the primitive.
  -- If the user want the primitive to reduce whenever the two values are equal (no
  -- matter whether the equality is refl), they can combine it with @eraseEquality@.
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
ty (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
3 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \ Args
ts -> do
    let t :: Arg Term
t  = Arg Term -> Args -> Arg Term
forall a. a -> [a] -> a
headWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ Args
ts
    let eq :: Term
eq = Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Maybe (Arg Term) -> Arg Term
forall a. a -> Maybe a -> a
fromMaybe Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term) -> Maybe (Arg Term) -> Arg Term
forall a b. (a -> b) -> a -> b
$ Args -> Maybe (Arg Term)
forall a. [a] -> Maybe a
lastMaybe Args
ts
    Term -> ReduceM Term
forall t. Reduce t => t -> ReduceM t
reduce' Term
eq ReduceM Term
-> (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Con{} -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
refl Arg Term
t
      Term
_     -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term)) -> Args -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Args
ts

primMetaToNatInjective :: TCM PrimitiveImpl
primMetaToNatInjective :: TCM PrimitiveImpl
primMetaToNatInjective = do
  Type
meta  <- MetaId -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (MetaId
forall a. HasCallStack => a
undefined :: MetaId)
  Type
nat   <- Nat -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Nat
forall a. HasCallStack => a
undefined :: Nat)
  QName
toNat <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primMetaToNat"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
meta Type
nat QName
toNat

primCharToNatInjective :: TCM PrimitiveImpl
primCharToNatInjective :: TCM PrimitiveImpl
primCharToNatInjective = do
  Type
char  <- Char -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Char
forall a. HasCallStack => a
undefined :: Char)
  Type
nat   <- Nat -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Nat
forall a. HasCallStack => a
undefined :: Nat)
  QName
toNat <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primCharToNat"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
char Type
nat QName
toNat

primStringToListInjective :: TCM PrimitiveImpl
primStringToListInjective :: TCM PrimitiveImpl
primStringToListInjective = do
  Type
string <- Text -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Text
forall a. HasCallStack => a
undefined :: Text)
  Type
chars  <- ArgName -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (ArgName
forall a. HasCallStack => a
undefined :: String)
  QName
toList <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primStringToList"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
string Type
chars QName
toList

primStringFromListInjective :: TCM PrimitiveImpl
primStringFromListInjective :: TCM PrimitiveImpl
primStringFromListInjective = do
  Type
chars  <- ArgName -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (ArgName
forall a. HasCallStack => a
undefined :: String)
  Type
string <- Text -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Text
forall a. HasCallStack => a
undefined :: Text)
  QName
fromList <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primStringFromList"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
chars Type
string QName
fromList

primWord64ToNatInjective :: TCM PrimitiveImpl
primWord64ToNatInjective :: TCM PrimitiveImpl
primWord64ToNatInjective =  do
  Type
word  <- Word64 -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Word64
forall a. HasCallStack => a
undefined :: Word64)
  Type
nat   <- Nat -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Nat
forall a. HasCallStack => a
undefined :: Nat)
  QName
toNat <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primWord64ToNat"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
word Type
nat QName
toNat

primFloatToWord64Injective :: TCM PrimitiveImpl
primFloatToWord64Injective :: TCM PrimitiveImpl
primFloatToWord64Injective = do
  Type
float  <- Double -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Double
forall a. HasCallStack => a
undefined :: Double)
  Type
word   <- Word64 -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Word64
forall a. HasCallStack => a
undefined :: Word64)
  QName
toWord <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primFloatToWord64"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
float Type
word QName
toWord

primQNameToWord64sInjective :: TCM PrimitiveImpl
primQNameToWord64sInjective :: TCM PrimitiveImpl
primQNameToWord64sInjective = do
  Type
name    <- QName -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (QName
forall a. HasCallStack => a
undefined :: QName)
  Type
words   <- (Word64, Word64) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType ((Word64, Word64)
forall a. HasCallStack => a
undefined :: (Word64, Word64))
  QName
toWords <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primQNameToWord64s"
  Type -> Type -> QName -> TCM PrimitiveImpl
mkPrimInjective Type
name Type
words QName
toWords

getRefl :: TCM (Arg Term -> Term)
getRefl :: TCM (Arg Term -> Term)
getRefl = do
  -- BUILTIN REFL maybe a constructor with one (the principal) argument or only parameters.
  -- Get the ArgInfo of the principal argument of refl.
  con :: Term
con@(Con ConHead
rf ConInfo
ci []) <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
  Maybe ArgInfo
minfo <- (ArgInfo -> ArgInfo) -> Maybe ArgInfo -> Maybe ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) (Maybe ArgInfo -> Maybe ArgInfo)
-> TCMT IO (Maybe ArgInfo) -> TCMT IO (Maybe ArgInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> TCMT IO (Maybe ArgInfo)
getReflArgInfo ConHead
rf
  (Arg Term -> Term) -> TCM (Arg Term -> Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Arg Term -> Term) -> TCM (Arg Term -> Term))
-> (Arg Term -> Term) -> TCM (Arg Term -> Term)
forall a b. (a -> b) -> a -> b
$ case Maybe ArgInfo
minfo of
    Just ArgInfo
ai -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
rf ConInfo
ci (Elims -> Term) -> (Arg Term -> Elims) -> Arg Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:[]) (Elim' Term -> Elims)
-> (Arg Term -> Elim' Term) -> Arg Term -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term)
-> (Arg Term -> Arg Term) -> Arg Term -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Arg Term -> Arg Term
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
ai
    Maybe ArgInfo
Nothing -> Term -> Arg Term -> Term
forall a b. a -> b -> a
const Term
con

-- | @primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y@
primEraseEquality :: TCM PrimitiveImpl
primEraseEquality :: TCM PrimitiveImpl
primEraseEquality = do
  -- primEraseEquality is incompatible with --without-K
  -- We raise an error warning if --safe is set and a mere warning otherwise
  TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Bool -> TCMT IO () -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (CommandLineOptions -> Bool
forall a. LensSafeMode a => a -> Bool
Lens.getSafeMode (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions)
      {- then -} (Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
SafeFlagWithoutKFlagPrimEraseEquality)
      {- else -} (Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
WithoutKFlagPrimEraseEquality)
  -- Get the name and type of BUILTIN EQUALITY
  QName
eq   <- TCM QName
primEqualityName
  Type
eqTy <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
eq
  -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@.
  TelV Tele (Dom Type)
eqTel Type
eqCore <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
eqTy
  let eqSort :: Sort' Term
eqSort = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
eqCore of
        Sort Sort' Term
s -> Sort' Term
s
        Term
_      -> Sort' Term
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- Construct the type of primEraseEquality, e.g.
  -- @{a : Level} {A : Set a} {x y : A} → eq {a} {A} x y -> eq {a} {A} x y@.
  Type
t <- let xeqy :: TCM Type
xeqy = Type -> TCM Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
eqSort (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
eq (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> Args -> Elims
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
eqTel in
       Tele (Dom Type) -> Type -> Type
telePi_ ((Dom Type -> Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hide Tele (Dom Type)
eqTel) (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCM Type
xeqy TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
xeqy)

  -- Get the constructor corresponding to BUILTIN REFL
  Arg Term -> Term
refl <- TCM (Arg Term -> Term)
getRefl

  -- The implementation of primEraseEquality:
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Arity
1 Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
+ Tele (Dom Type) -> Arity
forall a. Sized a => a -> Arity
size Tele (Dom Type)
eqTel) ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \ Args
ts -> do
    let (Arg Term
u, Arg Term
v) = (Arg Term, Arg Term)
-> Maybe (Arg Term, Arg Term) -> (Arg Term, Arg Term)
forall a. a -> Maybe a -> a
fromMaybe (Arg Term, Arg Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Term, Arg Term) -> (Arg Term, Arg Term))
-> Maybe (Arg Term, Arg Term) -> (Arg Term, Arg Term)
forall a b. (a -> b) -> a -> b
$ Args -> Maybe (Arg Term, Arg Term)
forall a. [a] -> Maybe (a, a)
last2 (Args -> Maybe (Arg Term, Arg Term))
-> Maybe Args -> Maybe (Arg Term, Arg Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Args -> Maybe Args
forall a. [a] -> Maybe [a]
initMaybe Args
ts
    -- Andreas, 2013-07-22.
    -- Note that we cannot call the conversion checker here,
    -- because 'reduce' might be called in a context where
    -- some bound variables do not have a type (just __DUMMY_TYPE__),
    -- and the conversion checker for eliminations does not
    -- like this.
    -- We can only do untyped equality, e.g., by normalisation.
    -- Jesper, 2020-04-04: We reduce rather than normalise for
    -- efficiency reasons. In general this is weaker but it is
    -- equivalent at base types. A stronger version of
    -- primEraseEquality (using type-directed conversion) may be
    -- implemented using --rewriting.
    (Arg Term
u', Arg Term
v') <- (Arg Term, Arg Term) -> ReduceM (Arg Term, Arg Term)
forall t. Reduce t => t -> ReduceM t
reduce' (Arg Term
u, Arg Term
v)
    if Arg Term
u' Arg Term -> Arg Term -> Bool
forall a. Eq a => a -> a -> Bool
== Arg Term
v' then Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
refl Arg Term
u else
      Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term)) -> Args -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Args
ts

-- | Get the 'ArgInfo' of the principal argument of BUILTIN REFL.
--
--   Returns @Nothing@ for e.g.
--   @
--     data Eq {a} {A : Set a} (x : A) : A → Set a where
--       refl : Eq x x
--   @
--
--   Returns @Just ...@ for e.g.
--   @
--     data Eq {a} {A : Set a} : (x y : A) → Set a where
--       refl : ∀ x → Eq x x
--   @

getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
getReflArgInfo :: ConHead -> TCMT IO (Maybe ArgInfo)
getReflArgInfo ConHead
rf = do
  Definition
def <- ConHead -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
rf
  TelV Tele (Dom Type)
reflTel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  Maybe ArgInfo -> TCMT IO (Maybe ArgInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ArgInfo -> TCMT IO (Maybe ArgInfo))
-> Maybe ArgInfo -> TCMT IO (Maybe ArgInfo)
forall a b. (a -> b) -> a -> b
$ (Dom (ArgName, Type) -> ArgInfo)
-> Maybe (Dom (ArgName, Type)) -> Maybe ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom (ArgName, Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (Maybe (Dom (ArgName, Type)) -> Maybe ArgInfo)
-> Maybe (Dom (ArgName, Type)) -> Maybe ArgInfo
forall a b. (a -> b) -> a -> b
$ [Dom (ArgName, Type)] -> Maybe (Dom (ArgName, Type))
forall a. [a] -> Maybe a
listToMaybe ([Dom (ArgName, Type)] -> Maybe (Dom (ArgName, Type)))
-> [Dom (ArgName, Type)] -> Maybe (Dom (ArgName, Type))
forall a b. (a -> b) -> a -> b
$ Arity -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a. Arity -> [a] -> [a]
drop (Defn -> Arity
conPars (Defn -> Arity) -> Defn -> Arity
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
-> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
reflTel


-- | Used for both @primForce@ and @primForceLemma@.
genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
genPrimForce TCM Type
b Term -> Arg Term -> Term
ret = do
  let varEl :: Arity -> f a -> f (Type'' Term a)
varEl Arity
s f a
a = Sort' Term -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Arity -> Sort' Term
varSort Arity
s) (a -> Type'' Term a) -> f a -> f (Type'' Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
      varT :: Arity -> Arity -> f Type
varT Arity
s Arity
a  = Arity -> f Term -> f Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
s (Arity -> f Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
a)
      varS :: Arity -> f Type
varS Arity
s    = Type -> f Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Sort' Term -> Type) -> Sort' Term -> Type
forall a b. (a -> b) -> a -> b
$ Arity -> Sort' Term
varSort Arity
s
  Type
t <- ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
       ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"b" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
       ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> f Type
varS Arity
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
       ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"B" (Arity -> Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
varT Arity
2 Arity
0 TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> f Type
varS Arity
1) TCM Type
b
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
6 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \ Args
ts ->
    case Args
ts of
      [Arg Term
a, Arg Term
b, Arg Term
s, Arg Term
t, Arg Term
u, Arg Term
f] -> do
        Blocked (Arg Term)
u <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
u
        let isWHNF :: Blocked' t (Arg Term) -> m Bool
isWHNF Blocked{} = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            isWHNF (NotBlocked NotBlocked' t
_ Arg Term
u) =
              case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u of
                Lit{}      -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Con{}      -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Lam{}      -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Pi{}       -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Sort{}     -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- sorts and levels are considered whnf
                Level{}    -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                DontCare{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Def QName
q Elims
_    -> do
                  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
                  Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ case Defn
def of
                    Datatype{} -> Bool
True
                    Record{}   -> Bool
True
                    Defn
_          -> Bool
False
                Var{}      -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                MetaV{}    -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                Dummy ArgName
s Elims
_  -> ArgName -> m Bool
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s
        ReduceM Bool
-> ReduceM (Reduced MaybeReducedArgs Term)
-> ReduceM (Reduced MaybeReducedArgs Term)
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Blocked (Arg Term) -> ReduceM Bool
forall {m :: * -> *} {t}.
HasConstInfo m =>
Blocked' t (Arg Term) -> m Bool
isWHNF Blocked (Arg Term)
u)
            (Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term -> Term
ret (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
f) (Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
u))
            (Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
-> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> MaybeReduced (Arg Term)) -> Args -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
a, Arg Term
b, Arg Term
s, Arg Term
t] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
u, Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
f])
      Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

primForce :: TCM PrimitiveImpl
primForce :: TCM PrimitiveImpl
primForce = do
  let varEl :: Arity -> f a -> f (Type'' Term a)
varEl Arity
s f a
a = Sort' Term -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Arity -> Sort' Term
varSort Arity
s) (a -> Type'' Term a) -> f a -> f (Type'' Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
      varT :: Arity -> Arity -> f Type
varT Arity
s Arity
a  = Arity -> f Term -> f Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
s (Arity -> f Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
a)
  TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
genPrimForce (ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"x" (Arity -> Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
varT Arity
3 Arity
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"y" (Arity -> Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
varT Arity
4 Arity
2) (Arity -> TCMT IO Term -> TCM Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
forall a b. (a -> b) -> a -> b
$ Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                Arity -> TCMT IO Term -> TCM Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
3 (Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0)) ((Term -> Arg Term -> Term) -> TCM PrimitiveImpl)
-> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$
    \ Term
f Arg Term
u -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
f [Arg Term
u]

primForceLemma :: TCM PrimitiveImpl
primForceLemma :: TCM PrimitiveImpl
primForceLemma = do
  let varEl :: Arity -> f a -> f (Type'' Term a)
varEl Arity
s f a
a = Sort' Term -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Arity -> Sort' Term
varSort Arity
s) (a -> Type'' Term a) -> f a -> f (Type'' Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
      varT :: Arity -> Arity -> f Type
varT Arity
s Arity
a  = Arity -> f Term -> f Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
s (Arity -> f Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
a)
  Term
refl  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
  QName
force <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
ArgName -> m PrimFun
getPrimitive ArgName
"primForce"
  TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
genPrimForce (ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"x" (Arity -> Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
varT Arity
3 Arity
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"f" (ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
nPi ArgName
"y" (Arity -> Arity -> TCM Type
forall {f :: * -> *}. Applicative f => Arity -> Arity -> f Type
varT Arity
4 Arity
2) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Arity -> TCMT IO Term -> TCM Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
forall a b. (a -> b) -> a -> b
$ Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                Arity -> TCMT IO Term -> TCM Type
forall {f :: * -> *} {a}.
Functor f =>
Arity -> f a -> f (Type'' Term a)
varEl Arity
4 (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquality TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
4 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
1)
                                       TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Term -> TCMT IO Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def QName
force []) TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
5 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
4 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
3 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0)
                                       TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
0 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Arity -> TCMT IO Term
forall (m :: * -> *). Applicative m => Arity -> m Term
varM Arity
1)
               ) ((Term -> Arg Term -> Term) -> TCM PrimitiveImpl)
-> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ \ Term
_ Arg Term
_ -> Term
refl

mkPrimLevelZero :: TCM PrimitiveImpl
mkPrimLevelZero :: TCM PrimitiveImpl
mkPrimLevelZero = do
  Type
t <- Lvl -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Lvl
forall a. HasCallStack => a
undefined :: Lvl)
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
0 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
_ -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level (Level' Term -> Term) -> Level' Term -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel Integer
0

mkPrimLevelSuc :: TCM PrimitiveImpl
mkPrimLevelSuc :: TCM PrimitiveImpl
mkPrimLevelSuc = do
  Type
t <- (Lvl -> Lvl) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Lvl -> Lvl
forall a. a -> a
id :: Lvl -> Lvl)
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \ ~[Arg Term
a] -> do
    Level' Term
l <- Term -> ReduceM (Level' Term)
forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView' (Term -> ReduceM (Level' Term)) -> Term -> ReduceM (Level' Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a
    Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level (Level' Term -> Term) -> Level' Term -> Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Level' Term
levelSuc Level' Term
l

mkPrimLevelMax :: TCM PrimitiveImpl
mkPrimLevelMax :: TCM PrimitiveImpl
mkPrimLevelMax = do
  Type
t <- Op Lvl -> TCM Type
forall a. PrimType a => a -> TCM Type
primType (Op Lvl
forall a. Ord a => a -> a -> a
max :: Op Lvl)
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
2 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \ ~[Arg Term
a, Arg Term
b] -> do
    Level' Term
a' <- Term -> ReduceM (Level' Term)
forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView' (Term -> ReduceM (Level' Term)) -> Term -> ReduceM (Level' Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a
    Level' Term
b' <- Term -> ReduceM (Level' Term)
forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView' (Term -> ReduceM (Level' Term)) -> Term -> ReduceM (Level' Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b
    Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level (Level' Term -> Term) -> Level' Term -> Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Level' Term -> Level' Term
levelLub Level' Term
a' Level' Term
b'

mkPrimSetOmega :: IsFibrant -> TCM PrimitiveImpl
mkPrimSetOmega :: IsFibrant -> TCM PrimitiveImpl
mkPrimSetOmega IsFibrant
f = do
  let t :: Type
t = Sort' Term -> Type
sort (Sort' Term -> Type) -> Sort' Term -> Type
forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
1
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
0 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
_ -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
Sort (Sort' Term -> Term) -> Sort' Term -> Term
forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
0

primLockUniv' :: TCM PrimitiveImpl
primLockUniv' :: TCM PrimitiveImpl
primLockUniv' = do
  let t :: Type
t = Sort' Term -> Type
sort (Sort' Term -> Type) -> Sort' Term -> Type
forall a b. (a -> b) -> a -> b
$ Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Level' Term
levelSuc (Level' Term -> Level' Term) -> Level' Term -> Level' Term
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' Term] -> Level' Term
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 []
  PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
0 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
_ -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
Sort Sort' Term
forall t. Sort' t
LockUniv

-- mkPrimStrictSet :: TCM PrimitiveImpl
-- mkPrimStrictSet = do
--   t <- nPi "ℓ" (el primLevel) (pure $ sort $ SSet $ Max 0 [Plus 1 $ var 0])
--   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[a] -> do
--     l <- levelView' $ unArg a
--     redReturn $ Sort $ SSet l

mkPrimFun1TCM :: (FromTerm a, ToTerm b) =>
                 TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
mkPrimFun1TCM :: forall a b.
(FromTerm a, ToTerm b) =>
TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
mkPrimFun1TCM TCM Type
mt a -> ReduceM b
f = do
    FromTermFunction a
toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    b -> ReduceM Term
fromB <- TCM (b -> ReduceM Term)
forall a. ToTerm a => TCM (a -> ReduceM Term)
toTermR
    Type
t     <- TCM Type
mt
    PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
      case Args
ts of
        [Arg Term
v] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v) MaybeReduced (Arg Term) -> MaybeReducedArgs
forall el coll. Singleton el coll => el -> coll
singleton ((a -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \ a
x -> do
            Term
b <- b -> ReduceM Term
fromB (b -> ReduceM Term) -> ReduceM b -> ReduceM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> ReduceM b
f a
x
            case (MetaId -> Set MetaId) -> Term -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton Term
b of
              Set MetaId
ms | Set MetaId -> Bool
forall a. Set a -> Bool
Set.null Set MetaId
ms -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn Term
b
                 | Bool
otherwise   -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (Blocker -> Arg Term -> Blocked (Arg Term)
forall t a. Blocker -> a -> Blocked' t a
Blocked (Set MetaId -> Blocker
unblockOnAllMetas Set MetaId
ms) Arg Term
v)]
        Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- Tying the knot
mkPrimFun1 :: (PrimType a, FromTerm a, PrimType b, ToTerm b) =>
              (a -> b) -> TCM PrimitiveImpl
mkPrimFun1 :: forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 a -> b
f = do
    FromTermFunction a
toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    b -> Term
fromB <- TCM (b -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Type
t     <- (a -> b) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType a -> b
f
    PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
      case Args
ts of
        [Arg Term
v] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v) MaybeReduced (Arg Term) -> MaybeReducedArgs
forall el coll. Singleton el coll => el -> coll
singleton ((a -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \ a
x ->
          Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ b -> Term
fromB (b -> Term) -> b -> Term
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
        Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

mkPrimFun2 :: ( PrimType a, FromTerm a, ToTerm a
              , PrimType b, FromTerm b
              , PrimType c, ToTerm c ) =>
              (a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 :: forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 a -> b -> c
f = do
    FromTermFunction a
toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    a -> Term
fromA <- TCM (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    FromTermFunction b
toB   <- TCM (FromTermFunction b)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    c -> Term
fromC <- TCM (c -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Type
t     <- (a -> b -> c) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType a -> b -> c
f
    PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
2 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
      case Args
ts of
        [Arg Term
v,Arg Term
w] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v)
              (\MaybeReduced (Arg Term)
v' -> [MaybeReduced (Arg Term)
v', Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
w]) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \a
x ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) b)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction b
toB Arg Term
w)
              (\MaybeReduced (Arg Term)
w' -> [ Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
-> Blocked (Arg Term) -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked (Arg Term -> Blocked (Arg Term)) -> Arg Term -> Blocked (Arg Term)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Arg Term -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg Term
v) (a -> Term
fromA a
x)
                      , MaybeReduced (Arg Term)
w']) ((b -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \b
y ->
          Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ c -> Term
fromC (c -> Term) -> c -> Term
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f a
x b
y
        Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

mkPrimFun3 :: ( PrimType a, FromTerm a, ToTerm a
              , PrimType b, FromTerm b, ToTerm b
              , PrimType c, FromTerm c
              , PrimType d, ToTerm d ) =>
              (a -> b -> c -> d) -> TCM PrimitiveImpl
mkPrimFun3 :: forall a b c d.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 ToTerm b, PrimType c, FromTerm c, PrimType d, ToTerm d) =>
(a -> b -> c -> d) -> TCM PrimitiveImpl
mkPrimFun3 a -> b -> c -> d
f = do
    (FromTermFunction a
toA, a -> Term
fromA) <- (,) (FromTermFunction a
 -> (a -> Term) -> (FromTermFunction a, a -> Term))
-> TCMT IO (FromTermFunction a)
-> TCMT IO ((a -> Term) -> (FromTermFunction a, a -> Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm TCMT IO ((a -> Term) -> (FromTermFunction a, a -> Term))
-> TCMT IO (a -> Term) -> TCMT IO (FromTermFunction a, a -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    (FromTermFunction b
toB, b -> Term
fromB) <- (,) (FromTermFunction b
 -> (b -> Term) -> (FromTermFunction b, b -> Term))
-> TCMT IO (FromTermFunction b)
-> TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (FromTermFunction b)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
-> TCMT IO (b -> Term) -> TCMT IO (FromTermFunction b, b -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (b -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    FromTermFunction c
toC          <- TCM (FromTermFunction c)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    d -> Term
fromD        <- TCM (d -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Type
t <- (a -> b -> c -> d) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType a -> b -> c -> d
f
    PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
3 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
      let argFrom :: (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom t -> Term
fromX Arg e
a t
x =
            Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
-> Blocked (Arg Term) -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked (Arg Term -> Blocked (Arg Term)) -> Arg Term -> Blocked (Arg Term)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Arg e -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg e
a) (t -> Term
fromX t
x)
      in case Args
ts of
        [Arg Term
a,Arg Term
b,Arg Term
c] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
a)
              (\MaybeReduced (Arg Term)
a' -> [MaybeReduced (Arg Term)
a', Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
b, Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
c]) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \a
x ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) b)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction b
toB Arg Term
b)
              (\MaybeReduced (Arg Term)
b' -> [(a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom a -> Term
fromA Arg Term
a a
x, MaybeReduced (Arg Term)
b', Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
c]) ((b -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \b
y ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) c)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (c -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction c
toC Arg Term
c)
              (\MaybeReduced (Arg Term)
c' -> [ (a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom a -> Term
fromA Arg Term
a a
x, (b -> Term) -> Arg Term -> b -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom b -> Term
fromB Arg Term
b b
y, MaybeReduced (Arg Term)
c']) ((c -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (c -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \c
z ->
          Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ d -> Term
fromD (d -> Term) -> d -> Term
forall a b. (a -> b) -> a -> b
$ a -> b -> c -> d
f a
x b
y c
z
        Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

mkPrimFun4 :: ( PrimType a, FromTerm a, ToTerm a
              , PrimType b, FromTerm b, ToTerm b
              , PrimType c, FromTerm c, ToTerm c
              , PrimType d, FromTerm d
              , PrimType e, ToTerm e ) =>
              (a -> b -> c -> d -> e) -> TCM PrimitiveImpl
mkPrimFun4 :: forall a b c d e.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d,
 PrimType e, ToTerm e) =>
(a -> b -> c -> d -> e) -> TCM PrimitiveImpl
mkPrimFun4 a -> b -> c -> d -> e
f = do
    (FromTermFunction a
toA, a -> Term
fromA) <- (,) (FromTermFunction a
 -> (a -> Term) -> (FromTermFunction a, a -> Term))
-> TCMT IO (FromTermFunction a)
-> TCMT IO ((a -> Term) -> (FromTermFunction a, a -> Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm TCMT IO ((a -> Term) -> (FromTermFunction a, a -> Term))
-> TCMT IO (a -> Term) -> TCMT IO (FromTermFunction a, a -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (a -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    (FromTermFunction b
toB, b -> Term
fromB) <- (,) (FromTermFunction b
 -> (b -> Term) -> (FromTermFunction b, b -> Term))
-> TCMT IO (FromTermFunction b)
-> TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (FromTermFunction b)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm TCMT IO ((b -> Term) -> (FromTermFunction b, b -> Term))
-> TCMT IO (b -> Term) -> TCMT IO (FromTermFunction b, b -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (b -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    (FromTermFunction c
toC, c -> Term
fromC) <- (,) (FromTermFunction c
 -> (c -> Term) -> (FromTermFunction c, c -> Term))
-> TCMT IO (FromTermFunction c)
-> TCMT IO ((c -> Term) -> (FromTermFunction c, c -> Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (FromTermFunction c)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm TCMT IO ((c -> Term) -> (FromTermFunction c, c -> Term))
-> TCMT IO (c -> Term) -> TCMT IO (FromTermFunction c, c -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (c -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    FromTermFunction d
toD          <- TCM (FromTermFunction d)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    e -> Term
fromE        <- TCM (e -> Term)
forall a. ToTerm a => TCMT IO (a -> Term)
toTerm
    Type
t <- (a -> b -> c -> d -> e) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType a -> b -> c -> d -> e
f
    PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
4 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
      let argFrom :: (t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom t -> Term
fromX Arg e
a t
x =
            Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
-> Blocked (Arg Term) -> MaybeReduced (Arg Term)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked (Arg Term -> Blocked (Arg Term)) -> Arg Term -> Blocked (Arg Term)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Arg e -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg e
a) (t -> Term
fromX t
x)
      in case Args
ts of
        [Arg Term
a,Arg Term
b,Arg Term
c,Arg Term
d] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
a)
              (\MaybeReduced (Arg Term)
a' -> MaybeReduced (Arg Term)
a' MaybeReduced (Arg Term) -> MaybeReducedArgs -> MaybeReducedArgs
forall a. a -> [a] -> [a]
: (Arg Term -> MaybeReduced (Arg Term)) -> Args -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term
b,Arg Term
c,Arg Term
d]) ((a -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \a
x ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) b)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction b
toB Arg Term
b)
              (\MaybeReduced (Arg Term)
b' -> [(a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom a -> Term
fromA Arg Term
a a
x, MaybeReduced (Arg Term)
b', Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
c, Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
d]) ((b -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \b
y ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) c)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (c -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction c
toC Arg Term
c)
              (\MaybeReduced (Arg Term)
c' -> [ (a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom a -> Term
fromA Arg Term
a a
x
                      , (b -> Term) -> Arg Term -> b -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom b -> Term
fromB Arg Term
b b
y
                      , MaybeReduced (Arg Term)
c', Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
d]) ((c -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (c -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \c
z ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) d)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (d -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction d
toD Arg Term
d)
              (\MaybeReduced (Arg Term)
d' -> [ (a -> Term) -> Arg Term -> a -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom a -> Term
fromA Arg Term
a a
x
                      , (b -> Term) -> Arg Term -> b -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom b -> Term
fromB Arg Term
b b
y
                      , (c -> Term) -> Arg Term -> c -> MaybeReduced (Arg Term)
forall {t} {e}.
(t -> Term) -> Arg e -> t -> MaybeReduced (Arg Term)
argFrom c -> Term
fromC Arg Term
c c
z
                      , MaybeReduced (Arg Term)
d']) ((d -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (d -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \d
w ->

          Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ e -> Term
fromE (e -> Term) -> e -> Term
forall a b. (a -> b) -> a -> b
$ a -> b -> c -> d -> e
f a
x b
y c
z d
w
        Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__


---------------------------------------------------------------------------
-- * The actual primitive functions
---------------------------------------------------------------------------

type Op   a = a -> a -> a
type Fun  a = a -> a
type Rel  a = a -> a -> Bool
type Pred a = a -> Bool

primitiveFunctions :: Map String (TCM PrimitiveImpl)
primitiveFunctions :: Map ArgName (TCM PrimitiveImpl)
primitiveFunctions = TCM PrimitiveImpl -> TCM PrimitiveImpl
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM PrimitiveImpl -> TCM PrimitiveImpl)
-> Map ArgName (TCM PrimitiveImpl)
-> Map ArgName (TCM PrimitiveImpl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCM PrimitiveImpl -> TCM PrimitiveImpl -> TCM PrimitiveImpl)
-> [(ArgName, TCM PrimitiveImpl)]
-> Map ArgName (TCM PrimitiveImpl)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith TCM PrimitiveImpl -> TCM PrimitiveImpl -> TCM PrimitiveImpl
forall a. HasCallStack => a
__IMPOSSIBLE__
  -- Issue #4375          ^^^^^^^^^^^^^^^^^^^^^^^^^^
  --   Without this the next fresh checkpoint id gets changed building the primitive functions. This
  --   is bad for caching since it happens when scope checking import declarations (rebinding
  --   primitives). During type checking, the caching machinery might then load a cached state with
  --   out-of-date checkpoint ids. Make sure to preserve warnings though, since they include things
  --   like using unsafe things primitives with `--safe`.

  -- Ulf, 2015-10-28: Builtin integers now map to a datatype, and since you
  -- can define these functions (reasonably) efficiently using the primitive
  -- functions on natural numbers there's no need for them anymore. Keeping the
  -- show function around for convenience, and as a test case for a primitive
  -- function taking an integer.
  -- -- Integer functions
  -- [ "primIntegerPlus"     |-> mkPrimFun2 ((+)        :: Op Integer)
  -- , "primIntegerMinus"    |-> mkPrimFun2 ((-)        :: Op Integer)
  -- , "primIntegerTimes"    |-> mkPrimFun2 ((*)        :: Op Integer)
  -- , "primIntegerDiv"      |-> mkPrimFun2 (div        :: Op Integer)    -- partial
  -- , "primIntegerMod"      |-> mkPrimFun2 (mod        :: Op Integer)    -- partial
  -- , "primIntegerEquality" |-> mkPrimFun2 ((==)       :: Rel Integer)
  -- , "primIntegerLess"     |-> mkPrimFun2 ((<)        :: Rel Integer)
  -- , "primIntegerAbs"      |-> mkPrimFun1 (Nat . abs  :: Integer -> Nat)
  -- , "primNatToInteger"    |-> mkPrimFun1 (toInteger  :: Nat -> Integer)
  [ ArgName
"primShowInteger"     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Integer -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (Integer -> ArgName) -> Integer -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow :: Integer -> Text)

  -- Natural number functions
  , ArgName
"primNatPlus"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Nat -> Nat) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
(+)                     :: Op Nat)
  , ArgName
"primNatMinus"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Nat -> Nat) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 ((\Nat
x Nat
y -> Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
0 (Nat
x Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
y)) :: Op Nat)
  , ArgName
"primNatTimes"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Nat -> Nat) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
(*)                     :: Op Nat)
  , ArgName
"primNatDivSucAux"    ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Nat -> Nat -> Nat -> Nat) -> TCM PrimitiveImpl
forall a b c d e.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d,
 PrimType e, ToTerm e) =>
(a -> b -> c -> d -> e) -> TCM PrimitiveImpl
mkPrimFun4 ((\Nat
k Nat
m Nat
n Nat
j -> Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
div (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
0 (Nat -> Nat) -> Nat -> Nat
forall a b. (a -> b) -> a -> b
$ Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
j) (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)) :: Nat -> Nat -> Op Nat)
  , ArgName
"primNatModSucAux"    ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|->
      let aux :: Nat -> Nat -> Op Nat
          aux :: Nat -> Nat -> Nat -> Nat -> Nat
aux Nat
k Nat
m Nat
n Nat
j | Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
j     = Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
mod (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
j Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)
                      | Bool
otherwise = Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n
      in (Nat -> Nat -> Nat -> Nat -> Nat) -> TCM PrimitiveImpl
forall a b c d e.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d,
 PrimType e, ToTerm e) =>
(a -> b -> c -> d -> e) -> TCM PrimitiveImpl
mkPrimFun4 Nat -> Nat -> Nat -> Nat -> Nat
aux
  , ArgName
"primNatEquality"     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Nat -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel Nat)
  , ArgName
"primNatLess"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Nat -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
(<)  :: Rel Nat)
  , ArgName
"primShowNat"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (Nat -> ArgName) -> Nat -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow :: Nat -> Text)

  -- Machine words
  , ArgName
"primWord64ToNat"     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Word64 -> Nat) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Word64 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Word64 -> Nat)
  , ArgName
"primWord64FromNat"   ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Word64) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Nat -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Nat -> Word64)
  , ArgName
"primWord64ToNatInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primWord64ToNatInjective

  -- Level functions
  , ArgName
"primLevelZero"       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelZero
  , ArgName
"primLevelSuc"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelSuc
  , ArgName
"primLevelMax"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelMax

  -- Sorts
  , ArgName
"primSetOmega"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> IsFibrant -> TCM PrimitiveImpl
mkPrimSetOmega IsFibrant
IsFibrant
  , ArgName
"primStrictSetOmega"  ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> IsFibrant -> TCM PrimitiveImpl
mkPrimSetOmega IsFibrant
IsStrict

  -- Floating point functions
  --
  -- Wen, 2020-08-26: Primitives which convert from Float into other, more
  -- well-behaved numeric types should check for unrepresentable values, e.g.,
  -- NaN and the infinities, and return `nothing` if those are encountered, to
  -- ensure that the returned numbers are sensible. That means `primFloatRound`,
  -- `primFloatFloor`, `primFloatCeiling`, and `primFloatDecode`. The conversion
  -- `primFloatRatio` represents NaN as (0,0), and the infinities as (±1,0).
  --
  , ArgName
"primFloatEquality"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Bool
doubleEq
  , ArgName
"primFloatInequality"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Bool
doubleLe
  , ArgName
"primFloatLess"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Bool
doubleLt
  , ArgName
"primFloatIsInfinite"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite :: Double -> Bool)
  , ArgName
"primFloatIsNaN"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN :: Double -> Bool)
  , ArgName
"primFloatIsNegativeZero"    ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero :: Double -> Bool)
  , ArgName
"primFloatIsSafeInteger"     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Bool
isSafeInteger
  , ArgName
"primFloatToWord64"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Word64) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Word64
doubleToWord64
  , ArgName
"primFloatToWord64Injective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primFloatToWord64Injective
  , ArgName
"primNatToFloat"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Nat -> Double
forall a. Integral a => a -> Double
intToDouble :: Nat -> Double)
  , ArgName
"primIntToFloat"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Integer -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Integer -> Double
forall a. Integral a => a -> Double
intToDouble :: Integer -> Double)
  , ArgName
"primFloatRound"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Maybe Integer) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Integer
doubleRound
  , ArgName
"primFloatFloor"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Maybe Integer) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Integer
doubleFloor
  , ArgName
"primFloatCeiling"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Maybe Integer) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Integer
doubleCeiling
  , ArgName
"primFloatToRatio"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> (Integer, Integer)) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> (Integer, Integer)
doubleToRatio
  , ArgName
"primRatioToFloat"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Integer -> Integer -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Integer -> Integer -> Double
ratioToDouble
  , ArgName
"primFloatDecode"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Maybe (Integer, Integer)) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe (Integer, Integer)
doubleDecode
  , ArgName
"primFloatEncode"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Integer -> Integer -> Maybe Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Integer -> Integer -> Maybe Double
doubleEncode
  , ArgName
"primShowFloat"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (Double -> ArgName) -> Double -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> ArgName
forall a. Show a => a -> ArgName
show :: Double -> Text)
  , ArgName
"primFloatPlus"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Double
doublePlus
  , ArgName
"primFloatMinus"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Double
doubleMinus
  , ArgName
"primFloatTimes"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Double
doubleTimes
  , ArgName
"primFloatNegate"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleNegate
  , ArgName
"primFloatDiv"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Double
doubleDiv
  , ArgName
"primFloatPow"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Double
doublePow
  , ArgName
"primFloatSqrt"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleSqrt
  , ArgName
"primFloatExp"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleExp
  , ArgName
"primFloatLog"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleLog
  , ArgName
"primFloatSin"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleSin
  , ArgName
"primFloatCos"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleCos
  , ArgName
"primFloatTan"               ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleTan
  , ArgName
"primFloatASin"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleASin
  , ArgName
"primFloatACos"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleACos
  , ArgName
"primFloatATan"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleATan
  , ArgName
"primFloatATan2"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 Double -> Double -> Double
doubleATan2
  , ArgName
"primFloatSinh"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleSinh
  , ArgName
"primFloatCosh"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleCosh
  , ArgName
"primFloatTanh"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleTanh
  , ArgName
"primFloatASinh"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleASinh
  , ArgName
"primFloatACosh"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleCosh
  , ArgName
"primFloatATanh"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleTanh

  -- Character functions
  , ArgName
"primCharEquality"       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Char -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel Char)
  , ArgName
"primIsLower"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isLower
  , ArgName
"primIsDigit"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isDigit
  , ArgName
"primIsAlpha"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isAlpha
  , ArgName
"primIsSpace"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isSpace
  , ArgName
"primIsAscii"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isAscii
  , ArgName
"primIsLatin1"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isLatin1
  , ArgName
"primIsPrint"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isPrint
  , ArgName
"primIsHexDigit"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isHexDigit
  , ArgName
"primToUpper"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Char) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Char
toUpper
  , ArgName
"primToLower"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Char) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Char
toLower
  , ArgName
"primCharToNat"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Nat) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Arity -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Arity -> Nat) -> (Char -> Arity) -> Char -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Arity
forall a. Enum a => a -> Arity
fromEnum :: Char -> Nat)
  , ArgName
"primCharToNatInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primCharToNatInjective
  , ArgName
"primNatToChar"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Char) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Integer -> Char
integerToChar (Integer -> Char) -> (Nat -> Integer) -> Nat -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
unNat)
  , ArgName
"primShowChar"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (Char -> ArgName) -> Char -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Literal -> ArgName) -> (Char -> Literal) -> Char -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
LitChar)

  -- String functions
  , ArgName
"primStringToList"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Text -> ArgName) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Text -> ArgName
T.unpack
  , ArgName
"primStringToListInjective"   ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primStringToListInjective
  , ArgName
"primStringFromList"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (ArgName -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 ArgName -> Text
T.pack
  , ArgName
"primStringFromListInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primStringFromListInjective
  , ArgName
"primStringAppend"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Text -> Text -> Text) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Text -> Text -> Text
T.append :: Text -> Text -> Text)
  , ArgName
"primStringEquality"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Text -> Text -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel Text)
  , ArgName
"primShowString"              ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Text -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (Text -> ArgName) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Literal -> ArgName) -> (Text -> Literal) -> Text -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Literal
LitString)
  , ArgName
"primStringUncons"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Text -> Maybe (Char, Text)) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Text -> Maybe (Char, Text)
T.uncons

  -- Other stuff
  , ArgName
"primEraseEquality"   ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primEraseEquality
    -- This needs to be force : A → ((x : A) → B x) → B x rather than seq because of call-by-name.
  , ArgName
"primForce"           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primForce
  , ArgName
"primForceLemma"      ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primForceLemma
  , ArgName
"primQNameEquality"   ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (QName -> QName -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel QName)
  , ArgName
"primQNameLess"       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (QName -> QName -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (QName -> QName -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: Rel QName)
  , ArgName
"primShowQName"       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (QName -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (QName -> ArgName) -> QName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow :: QName -> Text)
  , ArgName
"primQNameFixity"     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (QName -> Fixity') -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Name -> Fixity'
nameFixity (Name -> Fixity') -> (QName -> Name) -> QName -> Fixity'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName)
  , ArgName
"primQNameToWord64s"  ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (QName -> (Word64, Word64)) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 ((\ (NameId Word64
x (ModuleNameHash Word64
y)) -> (Word64
x, Word64
y)) (NameId -> (Word64, Word64))
-> (QName -> NameId) -> QName -> (Word64, Word64)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> NameId
nameId (Name -> NameId) -> (QName -> Name) -> QName -> NameId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName
                                          :: QName -> (Word64, Word64))
  , ArgName
"primQNameToWord64sInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primQNameToWord64sInjective
  , ArgName
"primMetaEquality"    ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (MetaId -> MetaId -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel MetaId)
  , ArgName
"primMetaLess"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (MetaId -> MetaId -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (MetaId -> MetaId -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: Rel MetaId)
  , ArgName
"primShowMeta"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (MetaId -> Text) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack (ArgName -> Text) -> (MetaId -> ArgName) -> MetaId -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow :: MetaId -> Text)
  , ArgName
"primMetaToNat"       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (MetaId -> Nat) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Arity -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Arity -> Nat) -> (MetaId -> Arity) -> MetaId -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Arity
metaId :: MetaId -> Nat)
  , ArgName
"primMetaToNatInjective" ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primMetaToNatInjective
  , ArgName
"primIMin"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIMin'
  , ArgName
"primIMax"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIMax'
  , ArgName
"primINeg"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primINeg'
  , ArgName
"primPOr"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primPOr
  , ArgName
"primComp"            ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primComp
  , ArgName
builtinTrans          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primTrans'
  , ArgName
builtinHComp          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primHComp'
  , ArgName
"primIdJ"             ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIdJ
  , ArgName
"primPartial"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primPartial'
  , ArgName
"primPartialP"        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primPartialP'
  , ArgName
builtinGlue           ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primGlue'
  , ArgName
builtin_glue          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_glue'
  , ArgName
builtin_unglue        ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_unglue'
  , ArgName
builtinFaceForall     ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primFaceForall'
  , ArgName
"primDepIMin"         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primDepIMin'
  , ArgName
"primIdFace"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIdFace'
  , ArgName
"primIdPath"          ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIdPath'
  , ArgName
builtinIdElim         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIdElim'
  , ArgName
builtinSubOut         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primSubOut'
  , ArgName
builtin_glueU         ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_glueU'
  , ArgName
builtin_unglueU       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_unglueU'
  , ArgName
builtinLockUniv       ArgName -> TCM PrimitiveImpl -> (ArgName, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primLockUniv'
  ]
  where
    |-> :: a -> b -> (a, b)
(|->) = (,)