{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wunused-imports #-}

{-| Primitive functions, such as addition on builtin integers.
-}

module Mikan.TypeChecking.Primitive
       ( module Mikan.TypeChecking.Primitive.Base
       , module Mikan.TypeChecking.Primitive.Cubical
       , module Mikan.TypeChecking.Primitive
       ) where

import Data.Char
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Maybe
import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

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

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

import Mikan.TypeChecking.Quote (quoteTermWithKit, quoteTypeWithKit, quoteDomWithKit, quotingKit)
import Mikan.TypeChecking.Primitive.Base
import Mikan.TypeChecking.Primitive.Cubical

import Mikan.Utils.Char
import Mikan.Utils.Float
import Mikan.Utils.Functor
import Mikan.Utils.List
import Mikan.Utils.Maybe (fromMaybeM)
import Mikan.Utils.Monad
import Mikan.Syntax.Common.Pretty
import Mikan.Utils.Singleton

import Mikan.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
$c== :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
/= :: 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
$ccompare :: Nat -> Nat -> Ordering
compare :: Nat -> Nat -> Ordering
$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
>= :: Nat -> Nat -> Bool
$cmax :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
min :: Nat -> Nat -> Nat
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
$c+ :: Nat -> Nat -> Nat
+ :: Nat -> Nat -> Nat
$c- :: Nat -> Nat -> Nat
- :: Nat -> Nat -> Nat
$c* :: Nat -> Nat -> Nat
* :: Nat -> Nat -> Nat
$cnegate :: Nat -> Nat
negate :: Nat -> Nat
$cabs :: Nat -> Nat
abs :: Nat -> Nat
$csignum :: Nat -> Nat
signum :: Nat -> Nat
$cfromInteger :: Integer -> Nat
fromInteger :: Integer -> Nat
Num, Int -> Nat
Nat -> Int
Nat -> [Nat]
Nat -> Nat
Nat -> Nat -> [Nat]
Nat -> Nat -> Nat -> [Nat]
(Nat -> Nat)
-> (Nat -> Nat)
-> (Int -> Nat)
-> (Nat -> Int)
-> (Nat -> [Nat])
-> (Nat -> Nat -> [Nat])
-> (Nat -> Nat -> [Nat])
-> (Nat -> Nat -> Nat -> [Nat])
-> Enum Nat
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Nat -> Nat
succ :: Nat -> Nat
$cpred :: Nat -> Nat
pred :: Nat -> Nat
$ctoEnum :: Int -> Nat
toEnum :: Int -> Nat
$cfromEnum :: Nat -> Int
fromEnum :: Nat -> Int
$cenumFrom :: Nat -> [Nat]
enumFrom :: Nat -> [Nat]
$cenumFromThen :: Nat -> Nat -> [Nat]
enumFromThen :: Nat -> Nat -> [Nat]
$cenumFromTo :: Nat -> Nat -> [Nat]
enumFromTo :: Nat -> Nat -> [Nat]
$cenumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
enumFromThenTo :: Nat -> Nat -> 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
$ctoRational :: Nat -> Rational
toRational :: 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 a. a -> m a
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
$c== :: Lvl -> Lvl -> Bool
== :: Lvl -> Lvl -> Bool
$c/= :: Lvl -> Lvl -> Bool
/= :: 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
$ccompare :: Lvl -> Lvl -> Ordering
compare :: Lvl -> Lvl -> Ordering
$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
>= :: Lvl -> Lvl -> Bool
$cmax :: Op Lvl
max :: Op Lvl
$cmin :: Op Lvl
min :: Op Lvl
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 :: * -> *). HasOptions 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
    sigKit <- TCMT IO SigmaKit -> TCMT IO (Maybe SigmaKit) -> TCMT IO SigmaKit
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (TypeError -> TCMT IO SigmaKit
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCMT IO SigmaKit) -> TypeError -> TCMT IO SigmaKit
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
NoBindingForBuiltin BuiltinId
BuiltinSigma) TCMT IO (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
    let sig = QName -> Elims -> Term
Def (SigmaKit -> QName
sigmaName SigmaKit
sigKit) []
    a'       <- primType_ (undefined :: a)
    b'       <- primType_ (undefined :: b)
    Type la  <- pure $ getSort a'
    Type lb  <- pure $ getSort b'
    pure sig <#> pure (Level la)
             <#> pure (Level lb)
             <@> pure (unEl a')
             <@> pure (nolam $ unEl 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 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 ShortText
instance PrimTerm ShortText where
  primTerm :: ShortText -> TCMT IO Term
primTerm ShortText
_ = 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))

-- From Agda term to Haskell value

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

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

instance ToTerm Nat       where toTerm :: TCM (Nat -> ReduceM Term)
toTerm = (Nat -> ReduceM Term) -> TCM (Nat -> ReduceM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Nat -> ReduceM Term) -> TCM (Nat -> ReduceM Term))
-> (Nat -> ReduceM Term) -> TCM (Nat -> ReduceM Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (Nat -> Term) -> Nat -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Lvl       where toTerm :: TCM (Lvl -> ReduceM Term)
toTerm = (Lvl -> ReduceM Term) -> TCM (Lvl -> ReduceM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Lvl -> ReduceM Term) -> TCM (Lvl -> ReduceM Term))
-> (Lvl -> ReduceM Term) -> TCM (Lvl -> ReduceM Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (Lvl -> Term) -> Lvl -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> ReduceM Term)
toTerm = (Double -> ReduceM Term) -> TCM (Double -> ReduceM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Double -> ReduceM Term) -> TCM (Double -> ReduceM Term))
-> (Double -> ReduceM Term) -> TCM (Double -> ReduceM Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term)
-> (Double -> Term) -> Double -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> ReduceM Term)
toTerm = (Char -> ReduceM Term) -> TCM (Char -> ReduceM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Char -> ReduceM Term) -> TCM (Char -> ReduceM Term))
-> (Char -> ReduceM Term) -> TCM (Char -> ReduceM Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (Char -> Term) -> Char -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Term
Lit (Literal -> Term) -> (Char -> Literal) -> Char -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
LitChar
instance ToTerm ShortText where toTerm :: TCM (ShortText -> ReduceM Term)
toTerm = (ShortText -> ReduceM Term) -> TCM (ShortText -> ReduceM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ShortText -> ReduceM Term) -> TCM (ShortText -> ReduceM Term))
-> (ShortText -> ReduceM Term) -> TCM (ShortText -> ReduceM Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term)
-> (ShortText -> Term) -> ShortText -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Term
Lit (Literal -> Term) -> (ShortText -> Literal) -> ShortText -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> Literal
LitString
instance ToTerm QName     where toTerm :: TCM (QName -> ReduceM Term)
toTerm = (QName -> ReduceM Term) -> TCM (QName -> ReduceM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> ReduceM Term) -> TCM (QName -> ReduceM Term))
-> (QName -> ReduceM Term) -> TCM (QName -> ReduceM Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (QName -> Term) -> QName -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> ReduceM Term)
toTerm = do
    top <- TopLevelModuleName
-> Maybe TopLevelModuleName -> TopLevelModuleName
forall a. a -> Maybe a -> a
fromMaybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
-> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe TopLevelModuleName)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
    return $ pure . Lit . LitMeta top

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

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

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

instance ToTerm (Dom Type) where
  toTerm :: TCM (Dom Type -> ReduceM Term)
toTerm = do QuotingKit -> Dom Type -> ReduceM Term
quoteDomWithKit (QuotingKit -> Dom Type -> ReduceM Term)
-> TCMT IO QuotingKit -> TCM (Dom Type -> ReduceM Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO QuotingKit
quotingKit

instance ToTerm Type where
  toTerm :: TCM (Type -> ReduceM Term)
toTerm = QuotingKit -> Type -> ReduceM Term
quoteTypeWithKit (QuotingKit -> Type -> ReduceM Term)
-> TCMT IO QuotingKit -> TCM (Type -> ReduceM Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO QuotingKit
quotingKit

instance ToTerm ArgInfo where
  toTerm :: TCM (ArgInfo -> ReduceM Term)
toTerm = do
    info <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo
    vis  <- primVisible
    hid  <- primHidden
    ins  <- primInstance
    return $ \ ArgInfo
i -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ 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
      ]

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

instance ToTerm Fixity where
  toTerm :: TCMT IO (Fixity -> ReduceM Term)
toTerm = do
    lToTm  <- TCM (FixityLevel -> ReduceM Term)
forall a. ToTerm a => TCM (a -> ReduceM Term)
toTerm
    aToTm  <- toTerm
    fixity <- primFixityFixity
    return $ \ Fixity{fixityAssoc :: Fixity -> Associativity
fixityAssoc = Associativity
a, fixityLevel :: Fixity -> FixityLevel
fixityLevel = FixityLevel
l} ->
      Term -> Term -> Term -> Term
forall t. Apply t => t -> Term -> Term -> t
apply2 Term
fixity (Term -> Term -> Term) -> ReduceM Term -> ReduceM (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Associativity -> ReduceM Term
aToTm Associativity
a ReduceM (Term -> Term) -> ReduceM Term -> ReduceM Term
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FixityLevel -> ReduceM Term
lToTm FixityLevel
l

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

instance ToTerm Blocker where
  toTerm :: TCM (Blocker -> ReduceM Term)
toTerm = do
    all <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlockerAll
    any <- primAgdaBlockerAny
    meta <- primAgdaBlockerMeta
    lists <- buildList
    metaTm <- toTerm
    let go (UnblockOnAny Set Blocker
xs)    = Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
any (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Term
lists ([Term] -> Term) -> ReduceM [Term] -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Blocker -> ReduceM Term) -> [Blocker] -> ReduceM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Blocker -> ReduceM Term
go (Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
xs)
        go (UnblockOnAll Set Blocker
xs)    = Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
all (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Term
lists ([Term] -> Term) -> ReduceM [Term] -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Blocker -> ReduceM Term) -> [Blocker] -> ReduceM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Blocker -> ReduceM Term
go (Set Blocker -> [Blocker]
forall a. Set a -> [a]
Set.toList Set Blocker
xs)
        go (UnblockOnMeta MetaId
m)    = Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
meta (Term -> Term) -> ReduceM Term -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> ReduceM Term
metaTm MetaId
m
        go (UnblockOnDef QName
_)     = ReduceM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
        go (UnblockOnProblem ProblemId
_) = ReduceM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    pure go

instance ToTerm FixityLevel where
  toTerm :: TCM (FixityLevel -> ReduceM Term)
toTerm = do
    iToTm <- TCM (Double -> ReduceM Term)
forall a. ToTerm a => TCM (a -> ReduceM Term)
toTerm
    related   <- primPrecRelated
    unrelated <- primPrecUnrelated
    return $ \ FixityLevel
p ->
      case FixityLevel
p of
        FixityLevel
Unrelated -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unrelated
        Related Double
n -> Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
related (Term -> Term) -> ReduceM Term -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Double -> ReduceM Term
iToTm Double
n

instance (ToTerm a, ToTerm b) => ToTerm (a, b) where
  toTerm :: TCM ((a, b) -> ReduceM Term)
toTerm = do
    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 = ConHead -> ConInfo -> Elims -> Term
Con (SigmaKit -> ConHead
sigmaCon SigmaKit
sigKit) ConInfo
ConOSystem []

    fromA <- toTerm
    fromB <- toTerm
    pure $ \ (a
a, b
b) -> Term -> Term -> Term -> Term
forall t. Apply t => t -> Term -> Term -> t
apply2 Term
con (Term -> Term -> Term) -> ReduceM Term -> ReduceM (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReduceM Term
fromA a
a ReduceM (Term -> Term) -> ReduceM Term -> ReduceM Term
forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReduceM 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
    nil'  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil
    cons' <- primCons
    let nil       = Term
nil'
        cons Term
x Term
xs = Term
cons' Term -> [Term] -> Term
forall t. Apply t => t -> [Term] -> t
`applys` [Term
x, Term
xs]
    return $ foldr cons nil

instance ToTerm a => ToTerm [a] where
  toTerm :: TCM ([a] -> ReduceM Term)
toTerm = do
    mkList <- TCM ([Term] -> Term)
buildList
    fromA  <- toTerm
    return $ mkList <.> mapM fromA

instance ToTerm a => ToTerm (Maybe a) where
  toTerm :: TCM (Maybe a -> ReduceM Term)
toTerm = do
    nothing <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing
    just    <- primJust
    fromA   <- toTerm
    return $ maybe (pure nothing) (apply1 just <.> 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 pos _    [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos
    Con negsuc _ [] <- primIntegerNegSuc
    toNat         <- fromTerm :: TCM (FromTermFunction Nat)
    return $ \ Arg Term
v -> do
      b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
v
      let v'  = Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b
          arg = (Term -> Arg Term -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
v')
      case unArg (ignoreBlocking 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) -> ReduceM (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 -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction Nat
toNat Arg Term
u)
              (\ MaybeReduced (Arg Term)
u' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ 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) -> ReduceM (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 -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction Nat
toNat Arg Term
u)
              (\ MaybeReduced (Arg Term)
u' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ 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 a. a -> ReduceM a
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 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 ShortText where
  fromTerm :: TCM (FromTermFunction ShortText)
fromTerm = (Literal -> Maybe ShortText) -> TCM (FromTermFunction ShortText)
forall a. (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromLiteral ((Literal -> Maybe ShortText) -> TCM (FromTermFunction ShortText))
-> (Literal -> Maybe ShortText) -> TCM (FromTermFunction ShortText)
forall a b. (a -> b) -> a -> b
$ \case
    LitString ShortText
s -> ShortText -> Maybe ShortText
forall a. a -> Maybe a
Just ShortText
s
    Literal
_ -> Maybe ShortText
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 TopLevelModuleName
_ 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
        true  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
        false <- primFalse
        fromReducedTerm $ \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 Int
n [] === Var Int
m []   = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m
            Term
_        === Term
_          = Bool
False

instance (ToTerm a, FromTerm a) => FromTerm [a] where
  fromTerm :: TCM (FromTermFunction [a])
fromTerm = do
    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
    cons  <- isCon <$> primCons
    toA   <- fromTerm
    mkList nil cons toA <$> 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 -> ReduceM Term)
-> Arg Term
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
mkList ConHead
nil ConHead
cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
toA a -> ReduceM Term
fromA Arg Term
t = do
        b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
        let 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
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
t)
        case unArg 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 a. a -> ReduceM 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 [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
              ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM (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 -> ReduceM 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' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ 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) -> [Arg Term] -> 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) -> ReduceM (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 -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind
                  (ConHead
-> ConHead
-> (Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a))
-> (a -> ReduceM Term)
-> Arg Term
-> ReduceM (Reduced (MaybeReduced (Arg Term)) [a])
mkList ConHead
nil ConHead
cons Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
toA a -> ReduceM Term
fromA Arg Term
xs)
                  (\ MaybeReduced (Arg Term)
xsR -> do
                    yTm <- a -> ReduceM Term
fromA a
y
                    pure $ xsR <&> \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) -> [Arg Term] -> 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
yTm, 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 a. a -> ReduceM 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
    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
    just    <- isCon <$> primJust
    toA     <- fromTerm
    return $ \ Arg Term
t -> do
      let arg :: Term -> Arg Term
arg = (Term -> Arg Term -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
t)
      b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
      let t = Blocked (Arg Term) -> Arg Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
b
      case unArg 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 a. a -> ReduceM 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 [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
            ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM (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 -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
x)
              (\ MaybeReduced (Arg Term)
x' -> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ 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 a. a -> ReduceM 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 a. a -> TCMT IO 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
    b <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
    case f $ unArg (ignoreBlocking b) of
        Just a
x  -> Reduced (MaybeReduced (Arg Term)) a
-> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
forall a. a -> ReduceM 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 a. a -> ReduceM 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 Type0 @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
  eqName <- TCM QName
primEqualityName
  let lvl0     = Integer -> Level' Term
ClosedLevel Integer
0
  let 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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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    = Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Elims -> Term
Def QName
qn [])
  ty <- nPi "t" (pure a) $ nPi "u" (pure a) $
              (eq b (f <@> varM 1) (f <@> varM 0))
          --> (eq a (      varM 1) (      varM 0))

    -- Get the constructor corresponding to BUILTIN REFL
  refl <- 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@.
  return $ PrimImpl ty $ primFun __IMPOSSIBLE__ 3 $ \ [Arg Term]
ts -> do
    let t :: Arg Term
t  = Arg Term -> [Arg Term] -> Arg Term
forall a. a -> [a] -> a
headWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
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
$ [Arg Term] -> Maybe (Arg Term)
forall a. [a] -> Maybe a
lastMaybe [Arg Term]
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 a b. ReduceM a -> (a -> ReduceM b) -> ReduceM b
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 a. a -> ReduceM a
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))
-> [Arg Term] -> MaybeReducedArgs
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced [Arg Term]
ts

-- | Converts 'MetaId's to natural numbers.

metaToNat :: MetaId -> Nat
metaToNat :: MetaId -> Nat
metaToNat MetaId
m =
  Word64 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ModuleNameHash -> Word64
moduleNameHash (ModuleNameHash -> Word64) -> ModuleNameHash -> Word64
forall a b. (a -> b) -> a -> b
$ MetaId -> ModuleNameHash
metaModule MetaId
m) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
2 Nat -> Integer -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
64 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+
  Word64 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (MetaId -> Word64
metaId MetaId
m)

primMetaToNatInjective :: TCM PrimitiveImpl
primMetaToNatInjective :: TCM PrimitiveImpl
primMetaToNatInjective = do
  meta  <- MetaId -> TCM Type
forall a. PrimType a => a -> TCM Type
primType_ (MetaId
forall a. HasCallStack => a
undefined :: MetaId)
  nat   <- primType_ (undefined :: Nat)
  toNat <- primFunName <$> getPrimitive PrimMetaToNat
  mkPrimInjective meta nat toNat

primCharToNatInjective :: TCM PrimitiveImpl
primCharToNatInjective :: TCM PrimitiveImpl
primCharToNatInjective = do
  char  <- Char -> TCM Type
forall a. PrimType a => a -> TCM Type
primType_ (Char
forall a. HasCallStack => a
undefined :: Char)
  nat   <- primType_ (undefined :: Nat)
  toNat <- primFunName <$> getPrimitive PrimCharToNat
  mkPrimInjective char nat toNat

primStringToListInjective :: TCM PrimitiveImpl
primStringToListInjective :: TCM PrimitiveImpl
primStringToListInjective = do
  string <- ShortText -> TCM Type
forall a. PrimType a => a -> TCM Type
primType_ (ShortText
forall a. HasCallStack => a
undefined :: ShortText)
  chars  <- primType_ (undefined :: String)
  toList <- primFunName <$> getPrimitive PrimStringToList
  mkPrimInjective string chars toList

primStringFromListInjective :: TCM PrimitiveImpl
primStringFromListInjective :: TCM PrimitiveImpl
primStringFromListInjective = do
  chars  <- String -> TCM Type
forall a. PrimType a => a -> TCM Type
primType_ (String
forall a. HasCallStack => a
undefined :: String)
  string <- primType_ (undefined :: ShortText)
  fromList <- primFunName <$> getPrimitive PrimStringFromList
  mkPrimInjective chars string fromList

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@(Con rf ci []) <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
  minfo <- fmap (setOrigin Inserted) <$> getReflArgInfo rf
  pure $ case 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

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

getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
getReflArgInfo :: ConHead -> TCMT IO (Maybe ArgInfo)
getReflArgInfo ConHead
rf = do
  def <- ConHead -> TCMT IO Definition
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
ConHead -> m Definition
getConInfo ConHead
rf
  TelV reflTel _ <- telView $ defType def
  return $ fmap getArgInfo $ listToMaybe $ drop (conPars $ theDef def) $ telToList 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 :: Int -> f a -> f (Type'' Term a)
varEl Int
s f a
a = Sort' Term -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort' Term
varSort Int
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 :: Int -> Int -> f Type
varT Int
s Int
a  = Int -> f Term -> f Type
forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
varEl Int
s (Int -> f Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
a)
      varS :: Int -> f Type
varS Int
s    = Type -> f Type
forall a. a -> f a
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
$ Int -> Sort' Term
varSort Int
s
  t <- ShortText -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ShortText -> m Type -> m Type -> m Type
hPi ShortText
"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
$
       ShortText -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ShortText -> m Type -> m Type -> m Type
hPi ShortText
"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
$
       ShortText -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ShortText -> m Type -> m Type -> m Type
hPi ShortText
"A" (Int -> TCM Type
forall {f :: * -> *}. Applicative f => Int -> f Type
varS Int
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
       ShortText -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ShortText -> m Type -> m Type -> m Type
hPi ShortText
"B" (Int -> Int -> TCM Type
forall {f :: * -> *}. Applicative f => Int -> Int -> f Type
varT Int
2 Int
0 TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). HasOptions m => m Type -> m Type -> m Type
--> Int -> TCM Type
forall {f :: * -> *}. Applicative f => Int -> f Type
varS Int
1) TCM Type
b
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ [Arg Term]
ts ->
    case [Arg Term]
ts of
      [Arg Term
a, Arg Term
b, Arg Term
s, Arg Term
t, Arg Term
u, Arg Term
f] -> do
        u <- Arg Term -> ReduceM (Blocked (Arg Term))
forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
u
        let isWHNF Blocked{} = Bool -> m Bool
forall a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Con{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Lam{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Pi{}       -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Sort{}     -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- sorts and levels are considered whnf
                Level{}    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                DontCare{} -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                Def QName
q Elims
_    -> do
                  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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q
                  return $ case def of
                    Datatype{} -> Bool
True
                    Record{}   -> Bool
True
                    Defn
_          -> Bool
False
                Var{}      -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                MetaV{}    -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                Dummy DummyTermKind
s Elims
_  -> String -> m Bool
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> String
forall a. Show a => a -> String
show DummyTermKind
s)
        ifM (isWHNF u)
            (redReturn $ ret (unArg f) (ignoreBlocking u))
            (return $ NoReduction $ map notReduced [a, b, s, t] ++ [reduced u, notReduced f])
      [Arg Term]
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

mkPrimLevelZero :: TCM PrimitiveImpl
mkPrimLevelZero :: TCM PrimitiveImpl
mkPrimLevelZero = do
  t <- Lvl -> TCM Type
forall a. PrimType a => a -> TCM Type
primType_ (Lvl
forall a. HasCallStack => a
undefined :: Lvl)
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \[Arg Term]
_ -> 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
  t <- (Lvl -> Lvl) -> TCM Type
forall a. PrimType a => a -> TCM Type
primType_ (Lvl -> Lvl
forall a. a -> a
id :: Lvl -> Lvl)
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[Arg Term
a] -> do
    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
    redReturn $ Level $ levelSuc l

mkPrimLevelMax :: TCM PrimitiveImpl
mkPrimLevelMax :: TCM PrimitiveImpl
mkPrimLevelMax = do
  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)
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ~[Arg Term
a, Arg Term
b] -> do
    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
    b' <- levelView' $ unArg b
    redReturn $ Level $ levelLub a' b'

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
    toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    fromB <- toTerm
    t     <- mt
    return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \[Arg Term]
ts ->
      case [Arg Term]
ts of
        [Arg Term
v] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v) (MaybeReducedArgs -> ReduceM MaybeReducedArgs
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReducedArgs -> ReduceM MaybeReducedArgs)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> MaybeReduced (Arg Term)
-> ReduceM MaybeReducedArgs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
            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 allMetas Set.singleton 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 a. a -> ReduceM a
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)]
        [Arg Term]
_ -> 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
    toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    fromB <- toTerm
    t     <- primType_ f
    return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \[Arg Term]
ts ->
      case [Arg Term]
ts of
        [Arg Term
v] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v) (MaybeReducedArgs -> ReduceM MaybeReducedArgs
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReducedArgs -> ReduceM MaybeReducedArgs)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> MaybeReduced (Arg Term)
-> ReduceM MaybeReducedArgs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< b -> ReduceM Term
fromB (a -> b
f a
x)
        [Arg Term]
_ -> 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
    toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    fromA <- toTerm
    toB   <- fromTerm
    fromC <- toTerm
    t     <- primType_ f
    return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \[Arg Term]
ts ->
      case [Arg Term]
ts of
        [Arg Term
v,Arg Term
w] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v)
              (\MaybeReduced (Arg Term)
v' -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [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) -> ReduceM MaybeReducedArgs)
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction b
toB Arg Term
w)
              (\MaybeReduced (Arg Term)
w' -> do
                xTm <- a -> ReduceM Term
fromA a
x
                pure [reduced $ notBlocked $ Arg (argInfo v) xTm , 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))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< c -> ReduceM Term
fromC (a -> b -> c
f a
x b
y)
        [Arg Term]
_ -> 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
    (toA, fromA) <- (,) (FromTermFunction a
 -> (a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
-> TCMT IO (FromTermFunction a)
-> TCMT
     IO ((a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM 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 -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
-> TCMT IO (a -> ReduceM Term)
-> TCMT IO (FromTermFunction a, a -> ReduceM Term)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (a -> ReduceM Term)
forall a. ToTerm a => TCM (a -> ReduceM Term)
toTerm
    (toB, fromB) <- (,) <$> fromTerm <*> toTerm
    toC          <- fromTerm
    fromD        <- toTerm
    t <- primType_ f
    return $ PrimImpl t $ primFun __IMPOSSIBLE__ 3 $ \[Arg Term]
ts ->
      let argFrom :: (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom t -> f Term
fromX Arg e
a t
x =
            Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
-> (Term -> Blocked (Arg Term)) -> Term -> MaybeReduced (Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked (Arg Term -> Blocked (Arg Term))
-> (Term -> Arg Term) -> Term -> Blocked (Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Arg e -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg e
a) (Term -> MaybeReduced (Arg Term))
-> f Term -> f (MaybeReduced (Arg Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> f Term
fromX t
x
      in case [Arg Term]
ts of
        [Arg Term
a,Arg Term
b,Arg Term
c] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
a)
              (\MaybeReduced (Arg Term)
a' -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [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) -> ReduceM MaybeReducedArgs)
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction b
toB Arg Term
b)
              (\MaybeReduced (Arg Term)
b' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                [ (a -> ReduceM Term)
-> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom a -> ReduceM Term
fromA Arg Term
a a
x
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MaybeReduced (Arg Term)
b'
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> 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) -> ReduceM MaybeReducedArgs)
-> (c -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction c
toC Arg Term
c)
              (\MaybeReduced (Arg Term)
c' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                [ (a -> ReduceM Term)
-> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom a -> ReduceM Term
fromA Arg Term
a a
x
                , (b -> ReduceM Term)
-> Arg Term -> b -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom b -> ReduceM Term
fromB Arg Term
b b
y
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< d -> ReduceM Term
fromD (a -> b -> c -> d
f a
x b
y c
z)
        [Arg Term]
_ -> 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
    (toA, fromA) <- (,) (FromTermFunction a
 -> (a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
-> TCMT IO (FromTermFunction a)
-> TCMT
     IO ((a -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM 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 -> ReduceM Term) -> (FromTermFunction a, a -> ReduceM Term))
-> TCMT IO (a -> ReduceM Term)
-> TCMT IO (FromTermFunction a, a -> ReduceM Term)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCMT IO (a -> ReduceM Term)
forall a. ToTerm a => TCM (a -> ReduceM Term)
toTerm
    (toB, fromB) <- (,) <$> fromTerm <*> toTerm
    (toC, fromC) <- (,) <$> fromTerm <*> toTerm
    toD          <- fromTerm
    fromE        <- toTerm
    t <- primType_ f
    return $ PrimImpl t $ primFun __IMPOSSIBLE__ 4 $ \[Arg Term]
ts ->
      let argFrom :: (t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom t -> f Term
fromX Arg e
a t
x =
            Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (Blocked (Arg Term) -> MaybeReduced (Arg Term))
-> (Term -> Blocked (Arg Term)) -> Term -> MaybeReduced (Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Blocked (Arg Term)
forall a t. a -> Blocked' t a
notBlocked (Arg Term -> Blocked (Arg Term))
-> (Term -> Arg Term) -> Term -> Blocked (Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Arg e -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg e
a) (Term -> MaybeReduced (Arg Term))
-> f Term -> f (MaybeReduced (Arg Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> f Term
fromX t
x
      in case [Arg Term]
ts of
        [Arg Term
a,Arg Term
b,Arg Term
c,Arg Term
d] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> ReduceM MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
a)
              (\MaybeReduced (Arg Term)
a' -> MaybeReducedArgs -> ReduceM MaybeReducedArgs
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReducedArgs -> ReduceM MaybeReducedArgs)
-> MaybeReducedArgs -> ReduceM MaybeReducedArgs
forall a b. (a -> b) -> a -> b
$ MaybeReduced (Arg Term)
a' MaybeReduced (Arg Term) -> MaybeReducedArgs -> MaybeReducedArgs
forall a. a -> [a] -> [a]
: (Arg Term -> MaybeReduced (Arg Term))
-> [Arg Term] -> 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) -> ReduceM MaybeReducedArgs)
-> (b -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction b
toB Arg Term
b)
              (\MaybeReduced (Arg Term)
b' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                [ (a -> ReduceM Term)
-> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom a -> ReduceM Term
fromA Arg Term
a a
x
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MaybeReduced (Arg Term)
b'
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ Arg Term -> MaybeReduced (Arg Term)
forall a. a -> MaybeReduced a
notReduced Arg Term
c
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ 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) -> ReduceM MaybeReducedArgs)
-> (c -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction c
toC Arg Term
c)
              (\MaybeReduced (Arg Term)
c' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                [ (a -> ReduceM Term)
-> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom a -> ReduceM Term
fromA Arg Term
a a
x
                , (b -> ReduceM Term)
-> Arg Term -> b -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom b -> ReduceM Term
fromB Arg Term
b b
y
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MaybeReduced (Arg Term)
c'
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term)))
-> MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a b. (a -> b) -> a -> b
$ 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) -> ReduceM MaybeReducedArgs)
-> (d -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> ReduceM b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction d
toD Arg Term
d)
              (\MaybeReduced (Arg Term)
d' -> [ReduceM (MaybeReduced (Arg Term))] -> ReduceM MaybeReducedArgs
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                [ (a -> ReduceM Term)
-> Arg Term -> a -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom a -> ReduceM Term
fromA Arg Term
a a
x
                , (b -> ReduceM Term)
-> Arg Term -> b -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom b -> ReduceM Term
fromB Arg Term
b b
y
                , (c -> ReduceM Term)
-> Arg Term -> c -> ReduceM (MaybeReduced (Arg Term))
forall {f :: * -> *} {t} {e}.
Functor f =>
(t -> f Term) -> Arg e -> t -> f (MaybeReduced (Arg Term))
argFrom c -> ReduceM Term
fromC Arg Term
c c
z
                , MaybeReduced (Arg Term) -> ReduceM (MaybeReduced (Arg Term))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< e -> ReduceM Term
fromE (a -> b -> c -> d -> e
f a
x b
y c
z d
w)
        [Arg Term]
_ -> 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 PrimitiveId (TCM PrimitiveImpl)
primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl)
primitiveFunctions = TCM PrimitiveImpl -> TCM PrimitiveImpl
forall a. TCM a -> TCM a
localTCStateSavingWarnings (TCM PrimitiveImpl -> TCM PrimitiveImpl)
-> Map PrimitiveId (TCM PrimitiveImpl)
-> Map PrimitiveId (TCM PrimitiveImpl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCM PrimitiveImpl -> TCM PrimitiveImpl -> TCM PrimitiveImpl)
-> [(PrimitiveId, TCM PrimitiveImpl)]
-> Map PrimitiveId (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)
  [ PrimitiveId
PrimShowInteger     PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Integer -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText)
-> (Integer -> String) -> Integer -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Pretty a => a -> String
prettyShow :: Integer -> ShortText)

  -- Natural number functions
  , PrimitiveId
PrimNatPlus           PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimNatMinus          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimNatTimes          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimNatDivSucAux      PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimNatModSucAux      PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimNatEquality       PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimNatLess           PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimShowNat           PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText) -> (Nat -> String) -> Nat -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> String
forall a. Pretty a => a -> String
prettyShow :: Nat -> ShortText)

  -- -- Level functions
  , PrimitiveId
PrimLevelZero         PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelZero
  , PrimitiveId
PrimLevelSuc          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelSuc
  , PrimitiveId
PrimLevelMax          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelMax

  -- 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).
  --
  , PrimitiveId
PrimFloatEquality            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatInequality          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatLess                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatIsInfinite          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimFloatIsNaN               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimFloatIsNegativeZero      PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimFloatIsSafeInteger       PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimNatToFloat               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimIntToFloat               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimFloatRound               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatFloor               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatCeiling             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatToRatio             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimRatioToFloat             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatDecode              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatEncode              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimShowFloat                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText) -> (Double -> String) -> Double -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> String
forall a. Show a => a -> String
show :: Double -> ShortText)
  , PrimitiveId
PrimFloatPlus                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatMinus               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatTimes               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatNegate              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatDiv                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatPow                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatSqrt                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatExp                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatLog                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatSin                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatCos                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatTan                 PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatASin                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatACos                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatATan                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatATan2               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatSinh                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatCosh                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatTanh                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatASinh               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatACosh               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimFloatATanh               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimCharEquality         PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimIsLower              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsDigit              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsAlpha              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsSpace              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsAscii              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsLatin1             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsPrint              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimIsHexDigit           PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimToUpper              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimToLower              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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
  , PrimitiveId
PrimCharToNat            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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 (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Nat) -> (Char -> Int) -> Char -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
forall a. Enum a => a -> Int
fromEnum :: Char -> Nat)
  , PrimitiveId
PrimCharToNatInjective   PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primCharToNatInjective
  , PrimitiveId
PrimNatToChar            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimShowChar             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText) -> (Char -> String) -> Char -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> String
forall a. Pretty a => a -> String
prettyShow (Literal -> String) -> (Char -> Literal) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
LitChar)

  -- String functions
  , PrimitiveId
PrimStringToList              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (ShortText -> String) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 ShortText -> String
TS.unpack
  , PrimitiveId
PrimStringToListInjective     PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primStringToListInjective
  , PrimitiveId
PrimStringFromList            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (String -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 String -> ShortText
TS.pack
  , PrimitiveId
PrimStringFromListInjective   PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primStringFromListInjective
  , PrimitiveId
PrimStringAppend              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (ShortText -> ShortText -> ShortText) -> 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 (ShortText -> ShortText -> ShortText
TS.append :: ShortText -> ShortText -> ShortText)
  , PrimitiveId
PrimStringEquality            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (ShortText -> ShortText -> 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 (ShortText -> ShortText -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel ShortText)
  , PrimitiveId
PrimShowString                PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (ShortText -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText)
-> (ShortText -> String) -> ShortText -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> String
forall a. Pretty a => a -> String
prettyShow (Literal -> String)
-> (ShortText -> Literal) -> ShortText -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> Literal
LitString)
  , PrimitiveId
PrimStringUncons              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (ShortText -> Maybe (Char, ShortText)) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 ShortText -> Maybe (Char, ShortText)
TS.uncons

    -- This needs to be force : A → ((x : A) → B x) → B x rather than seq because of call-by-name.
  , PrimitiveId
PrimForce             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primForce
  , PrimitiveId
PrimForceLemma        PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primForceLemma
  , PrimitiveId
PrimQNameEquality     PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimQNameLess         PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimShowQName         PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (QName -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText) -> (QName -> String) -> QName -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Pretty a => a -> String
prettyShow :: QName -> ShortText)
  , PrimitiveId
PrimQNameFixity       PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimMetaEquality      PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimMetaLess          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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)
  , PrimitiveId
PrimShowMeta          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (MetaId -> ShortText) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> ShortText
TS.pack (String -> ShortText) -> (MetaId -> String) -> MetaId -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> String
forall a. Pretty a => a -> String
prettyShow :: MetaId -> ShortText)
  , PrimitiveId
PrimMetaToNat         PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, 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 MetaId -> Nat
metaToNat
  , PrimitiveId
PrimMetaToNatInjective   PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primMetaToNatInjective

  , PrimitiveId
PrimIMin              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIMin'
  , PrimitiveId
PrimIMax              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primIMax'
  , PrimitiveId
PrimINeg              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primINeg'
  , PrimitiveId
PrimPOr               PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primPOr
  , PrimitiveId
PrimComp              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primComp
  , PrimitiveId
PrimTrans             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primTrans'
  , PrimitiveId
PrimHComp             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primHComp'
  , PrimitiveId
PrimPartial           PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primPartial'
  , PrimitiveId
PrimPartialP          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primPartialP'
  , PrimitiveId
PrimGlue              PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primGlue'
  , PrimitiveId
Prim_glue             PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_glue'
  , PrimitiveId
Prim_unglue           PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_unglue'
  , PrimitiveId
PrimFaceForall        PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primFaceForall'
  , PrimitiveId
PrimSubOut            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primSubOut'
  , PrimitiveId
Prim_glueU            PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_glueU'
  , PrimitiveId
Prim_unglueU          PrimitiveId
-> TCM PrimitiveImpl -> (PrimitiveId, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
prim_unglueU'
  ]
  where
    |-> :: a -> b -> (a, b)
(|->) = (,)