{-# OPTIONS_GHC -Wunused-imports #-}

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

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

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

import qualified Agda.Interaction.Options.Lenses as Lens

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

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

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

import Agda.Utils.Char
import Agda.Utils.Float
import Agda.Utils.List
import Agda.Utils.Maybe (fromMaybeM)
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.Utils.Impossible

-- Haskell type to Agda type

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

-- In GHC > 7.8 deriving Integral causes an unnecessary toInteger
-- warning.
instance Integral Nat where
  toInteger :: Nat -> Integer
toInteger = Nat -> Integer
unNat
  quotRem :: Nat -> Nat -> (Nat, Nat)
quotRem (Nat Integer
a) (Nat Integer
b) = (Integer -> Nat
Nat Integer
q, Integer -> Nat
Nat Integer
r)
    where (Integer
q, Integer
r) = 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
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> Nat -> m
foldTerm Term -> m
_      = forall a. Monoid a => a
mempty

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

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

instance Pretty Lvl where
  pretty :: Lvl -> Doc
pretty = forall a. Pretty a => a -> Doc
pretty 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
_ = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall a. PrimTerm a => a -> TCM Term
primTerm (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) -> TCM Term
primTerm a -> b
_ = forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. PrimType a => a -> TCM Type
primType (forall a. HasCallStack => a
undefined :: a) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall a. PrimType a => a -> TCM Type
primType (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) -> TCM Term
primTerm (a, b)
_ = do
    SigmaKit
sigKit <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
NoBindingForBuiltin BuiltinId
BuiltinSigma) forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
    let sig :: Term
sig = QName -> Elims -> Term
Def (SigmaKit -> QName
sigmaName SigmaKit
sigKit) []
    Type
a'       <- forall a. PrimType a => a -> TCM Type
primType (forall a. HasCallStack => a
undefined :: a)
    Type
b'       <- forall a. PrimType a => a -> TCM Type
primType (forall a. HasCallStack => a
undefined :: b)
    Type Level' Term
la  <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Type
a'
    Type Level' Term
lb  <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort Type
b'
    forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
sig forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Level' Term -> Term
Level Level' Term
la)
             forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Level' Term -> Term
Level Level' Term
lb)
             forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t a. Type'' t a -> a
unEl Type
a')
             forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Term
nolam forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
b')

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

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

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

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

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

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

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

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

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

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

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

instance PrimType Fixity'
instance PrimTerm Fixity' where primTerm :: Fixity' -> TCM Term
primTerm Fixity'
_ = 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] -> TCM Term
primTerm [a]
_ = TCM Term -> TCM Term
list (forall a. PrimTerm a => a -> TCM Term
primTerm (forall a. HasCallStack => a
undefined :: a))

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

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

-- From Agda term to Haskell value

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

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

instance ToTerm Nat     where toTerm :: TCM (Nat -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
LitNat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
instance ToTerm Word64  where toTerm :: TCM (Word64 -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Literal
LitWord64
instance ToTerm Lvl     where toTerm :: TCM (Lvl -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Level' Term
ClosedLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lvl -> Integer
unLvl
instance ToTerm Double  where toTerm :: TCM (Double -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Literal
LitFloat
instance ToTerm Char    where toTerm :: TCM (Char -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
LitChar
instance ToTerm Text    where toTerm :: TCM (Text -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Literal
LitString
instance ToTerm QName   where toTerm :: TCM (QName -> Term)
toTerm = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Literal
LitQName
instance ToTerm MetaId  where
  toTerm :: TCM (MetaId -> Term)
toTerm = do
    TopLevelModuleName
top <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> MetaId -> Literal
LitMeta TopLevelModuleName
top

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- From Haskell value to Agda term

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

          forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ e -> Term
fromE forall a b. (a -> b) -> a -> b
$ a -> b -> c -> d -> e
f a
x b
y c
z d
w
        Args
_ -> 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 = forall a. TCM a -> TCM a
localTCStateSavingWarnings forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith 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     forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> ArgName
prettyShow :: Integer -> Text)

  -- Natural number functions
  , PrimitiveId
PrimNatPlus           forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Num a => a -> a -> a
(+)                     :: Op Nat)
  , PrimitiveId
PrimNatMinus          forall a b. a -> b -> (a, b)
|-> 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 -> forall a. Ord a => a -> a -> a
max Nat
0 (Nat
x forall a. Num a => a -> a -> a
- Nat
y)) :: Op Nat)
  , PrimitiveId
PrimNatTimes          forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Num a => a -> a -> a
(*)                     :: Op Nat)
  , PrimitiveId
PrimNatDivSucAux      forall a b. a -> b -> (a, b)
|-> 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 forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> a -> a
div (forall a. Ord a => a -> a -> a
max Nat
0 forall a b. (a -> b) -> a -> b
$ Nat
n forall a. Num a => a -> a -> a
+ Nat
m forall a. Num a => a -> a -> a
- Nat
j) (Nat
m forall a. Num a => a -> a -> a
+ Nat
1)) :: Nat -> Nat -> Op Nat)
  , PrimitiveId
PrimNatModSucAux      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 forall a. Ord a => a -> a -> Bool
> Nat
j     = forall a. Integral a => a -> a -> a
mod (Nat
n forall a. Num a => a -> a -> a
- Nat
j forall a. Num a => a -> a -> a
- Nat
1) (Nat
m forall a. Num a => a -> a -> a
+ Nat
1)
                      | Bool
otherwise = Nat
k forall a. Num a => a -> a -> a
+ Nat
n
      in 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       forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Eq a => a -> a -> Bool
(==) :: Rel Nat)
  , PrimitiveId
PrimNatLess           forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Ord a => a -> a -> Bool
(<)  :: Rel Nat)
  , PrimitiveId
PrimShowNat           forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> ArgName
prettyShow :: Nat -> Text)

  -- -- Machine words
  , PrimitiveId
PrimWord64ToNat      forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Word64 -> Nat)
  , PrimitiveId
PrimWord64FromNat    forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Nat -> Word64)
  , PrimitiveId
PrimWord64ToNatInjective forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primWord64ToNatInjective

  -- -- Level functions
  , PrimitiveId
PrimLevelZero         forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelZero
  , PrimitiveId
PrimLevelSuc          forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimLevelSuc
  , PrimitiveId
PrimLevelMax          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            forall a b. a -> b -> (a, b)
|-> 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          forall a b. a -> b -> (a, b)
|-> 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                forall a b. a -> b -> (a, b)
|-> 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          forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a. RealFloat a => a -> Bool
isInfinite :: Double -> Bool)
  , PrimitiveId
PrimFloatIsNaN               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a. RealFloat a => a -> Bool
isNaN :: Double -> Bool)
  , PrimitiveId
PrimFloatIsNegativeZero      forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a. RealFloat a => a -> Bool
isNegativeZero :: Double -> Bool)
  , PrimitiveId
PrimFloatIsSafeInteger       forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Bool
isSafeInteger
  , PrimitiveId
PrimFloatToWord64            forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Word64
doubleToWord64
  , PrimitiveId
PrimFloatToWord64Injective   forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primFloatToWord64Injective
  , PrimitiveId
PrimNatToFloat               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a. Integral a => a -> Double
intToDouble :: Nat -> Double)
  , PrimitiveId
PrimIntToFloat               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a. Integral a => a -> Double
intToDouble :: Integer -> Double)
  , PrimitiveId
PrimFloatRound               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Integer
doubleRound
  , PrimitiveId
PrimFloatFloor               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Integer
doubleFloor
  , PrimitiveId
PrimFloatCeiling             forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe Integer
doubleCeiling
  , PrimitiveId
PrimFloatToRatio             forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> (Integer, Integer)
doubleToRatio
  , PrimitiveId
PrimRatioToFloat             forall a b. a -> b -> (a, b)
|-> 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              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Maybe (Integer, Integer)
doubleDecode
  , PrimitiveId
PrimFloatEncode              forall a b. a -> b -> (a, b)
|-> 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                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show :: Double -> Text)
  , PrimitiveId
PrimFloatPlus                forall a b. a -> b -> (a, b)
|-> 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               forall a b. a -> b -> (a, b)
|-> 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               forall a b. a -> b -> (a, b)
|-> 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              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleNegate
  , PrimitiveId
PrimFloatDiv                 forall a b. a -> b -> (a, b)
|-> 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                 forall a b. a -> b -> (a, b)
|-> 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                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleSqrt
  , PrimitiveId
PrimFloatExp                 forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleExp
  , PrimitiveId
PrimFloatLog                 forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleLog
  , PrimitiveId
PrimFloatSin                 forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleSin
  , PrimitiveId
PrimFloatCos                 forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleCos
  , PrimitiveId
PrimFloatTan                 forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleTan
  , PrimitiveId
PrimFloatASin                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleASin
  , PrimitiveId
PrimFloatACos                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleACos
  , PrimitiveId
PrimFloatATan                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleATan
  , PrimitiveId
PrimFloatATan2               forall a b. a -> b -> (a, b)
|-> 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                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleSinh
  , PrimitiveId
PrimFloatCosh                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleCosh
  , PrimitiveId
PrimFloatTanh                forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleTanh
  , PrimitiveId
PrimFloatASinh               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleASinh
  , PrimitiveId
PrimFloatACosh               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleCosh
  , PrimitiveId
PrimFloatATanh               forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Double
doubleTanh

  -- Character functions
  , PrimitiveId
PrimCharEquality         forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Eq a => a -> a -> Bool
(==) :: Rel Char)
  , PrimitiveId
PrimIsLower              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isLower
  , PrimitiveId
PrimIsDigit              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isDigit
  , PrimitiveId
PrimIsAlpha              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isAlpha
  , PrimitiveId
PrimIsSpace              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isSpace
  , PrimitiveId
PrimIsAscii              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isAscii
  , PrimitiveId
PrimIsLatin1             forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isLatin1
  , PrimitiveId
PrimIsPrint              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isPrint
  , PrimitiveId
PrimIsHexDigit           forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isHexDigit
  , PrimitiveId
PrimToUpper              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Char
toUpper
  , PrimitiveId
PrimToLower              forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Char
toLower
  , PrimitiveId
PrimCharToNat            forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> Arity
fromEnum :: Char -> Nat)
  , PrimitiveId
PrimCharToNatInjective   forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primCharToNatInjective
  , PrimitiveId
PrimNatToChar            forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Integer -> Char
integerToChar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
unNat)
  , PrimitiveId
PrimShowChar             forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> ArgName
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Literal
LitChar)

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

  -- Other stuff
  , PrimitiveId
PrimEraseEquality     forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primEraseEquality
    -- This needs to be force : A → ((x : A) → B x) → B x rather than seq because of call-by-name.
  , PrimitiveId
PrimForce             forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primForce
  , PrimitiveId
PrimForceLemma        forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primForceLemma
  , PrimitiveId
PrimQNameEquality     forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Eq a => a -> a -> Bool
(==) :: Rel QName)
  , PrimitiveId
PrimQNameLess         forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Ord a => a -> a -> Bool
(<) :: Rel QName)
  , PrimitiveId
PrimShowQName         forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> ArgName
prettyShow :: QName -> Text)
  , PrimitiveId
PrimQNameFixity       forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Name -> Fixity'
nameFixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName)
  , PrimitiveId
PrimQNameToWord64s    forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 ((\ (NameId Word64
x (ModuleNameHash Word64
y)) -> (Word64
x, Word64
y)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> NameId
nameId forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName
                                          :: QName -> (Word64, Word64))
  , PrimitiveId
PrimQNameToWord64sInjective   forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primQNameToWord64sInjective
  , PrimitiveId
PrimMetaEquality      forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Eq a => a -> a -> Bool
(==) :: Rel MetaId)
  , PrimitiveId
PrimMetaLess          forall a b. a -> b -> (a, b)
|-> forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (forall a. Ord a => a -> a -> Bool
(<) :: Rel MetaId)
  , PrimitiveId
PrimShowMeta          forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (ArgName -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> ArgName
prettyShow :: MetaId -> Text)
  , PrimitiveId
PrimMetaToNat         forall a b. a -> b -> (a, b)
|-> forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 MetaId -> Nat
metaToNat
  , PrimitiveId
PrimMetaToNatInjective   forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primMetaToNatInjective

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