{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE NondecreasingIndentation   #-}
{-# LANGUAGE MonoLocalBinds             #-}

{-| 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 Data.Maybe
import Data.Word

import qualified Agda.Interaction.Options.Lenses as Lens

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

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

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

import Agda.Utils.Float
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.String ( Str(Str), unStr )

import Agda.Utils.Impossible

-- Haskell type to Agda type

newtype Nat = Nat { Nat -> Integer
unNat :: Integer }
            deriving (Nat -> Nat -> Bool
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c== :: Nat -> Nat -> Bool
Eq, Eq Nat
Eq Nat
-> (Nat -> Nat -> Ordering)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> Ord Nat
Nat -> Nat -> Bool
Nat -> Nat -> Ordering
Nat -> Nat -> Nat
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmax :: Nat -> Nat -> Nat
>= :: Nat -> Nat -> Bool
$c>= :: Nat -> Nat -> Bool
> :: Nat -> Nat -> Bool
$c> :: Nat -> Nat -> Bool
<= :: Nat -> Nat -> Bool
$c<= :: Nat -> Nat -> Bool
< :: Nat -> Nat -> Bool
$c< :: Nat -> Nat -> Bool
compare :: Nat -> Nat -> Ordering
$ccompare :: Nat -> Nat -> Ordering
$cp1Ord :: Eq Nat
Ord, Integer -> Nat
Nat -> Nat
Nat -> Nat -> Nat
(Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat)
-> (Nat -> Nat)
-> (Nat -> Nat)
-> (Integer -> Nat)
-> Num Nat
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
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, Int -> Nat
Nat -> Int
Nat -> [Nat]
Nat -> Nat
Nat -> Nat -> [Nat]
Nat -> Nat -> Nat -> [Nat]
(Nat -> Nat)
-> (Nat -> Nat)
-> (Int -> Nat)
-> (Nat -> Int)
-> (Nat -> [Nat])
-> (Nat -> Nat -> [Nat])
-> (Nat -> Nat -> [Nat])
-> (Nat -> Nat -> Nat -> [Nat])
-> Enum Nat
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
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 -> Int
$cfromEnum :: Nat -> Int
toEnum :: Int -> Nat
$ctoEnum :: Int -> Nat
pred :: Nat -> Nat
$cpred :: Nat -> Nat
succ :: Nat -> Nat
$csucc :: Nat -> Nat
Enum, Num Nat
Ord Nat
Num Nat -> Ord Nat -> (Nat -> Rational) -> Real Nat
Nat -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Nat -> Rational
$ctoRational :: Nat -> Rational
$cp2Real :: Ord Nat
$cp1Real :: Num Nat
Real)

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

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

instance Show Nat where
  show :: Nat -> String
show = Integer -> String
forall a. Show a => a -> String
show (Integer -> String) -> (Nat -> Integer) -> Nat -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger

newtype Lvl = Lvl { Lvl -> Integer
unLvl :: Integer }
  deriving (Lvl -> Lvl -> Bool
(Lvl -> Lvl -> Bool) -> (Lvl -> Lvl -> Bool) -> Eq Lvl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lvl -> Lvl -> Bool
$c/= :: Lvl -> Lvl -> Bool
== :: Lvl -> Lvl -> Bool
$c== :: Lvl -> Lvl -> Bool
Eq, Eq Lvl
Eq Lvl
-> (Lvl -> Lvl -> Ordering)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Bool)
-> (Lvl -> Lvl -> Lvl)
-> (Lvl -> Lvl -> Lvl)
-> Ord Lvl
Lvl -> Lvl -> Bool
Lvl -> Lvl -> Ordering
Lvl -> Lvl -> 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 :: Lvl -> Lvl -> Lvl
$cmin :: Lvl -> Lvl -> Lvl
max :: Lvl -> Lvl -> Lvl
$cmax :: Lvl -> Lvl -> 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
$cp1Ord :: Eq Lvl
Ord)

instance Show Lvl where
  show :: Lvl -> String
show = Integer -> String
forall a. Show a => a -> String
show (Integer -> String) -> (Lvl -> Integer) -> Lvl -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lvl -> Integer
unLvl

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

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

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

instance PrimTerm a => PrimType a where
  primType :: a -> TCMT IO (Type'' Term Term)
primType a
_ = TCM Term -> TCMT IO (Type'' Term Term)
forall (tcm :: * -> *).
Functor tcm =>
tcm Term -> tcm (Type'' Term Term)
el (TCM Term -> TCMT IO (Type'' Term Term))
-> TCM Term -> TCMT IO (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ a -> TCM Term
forall a. PrimTerm a => a -> TCM Term
primTerm (a
forall a. HasCallStack => a
undefined :: a)

class    PrimTerm a       where primTerm :: a -> TCM Term
instance PrimTerm Integer where primTerm :: Integer -> TCM Term
primTerm Integer
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger
instance PrimTerm Word64  where primTerm :: Word64 -> TCM Term
primTerm Word64
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64
instance PrimTerm Bool    where primTerm :: Bool -> TCM Term
primTerm Bool
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool
instance PrimTerm Char    where primTerm :: Char -> TCM Term
primTerm Char
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar
instance PrimTerm Double  where primTerm :: Double -> TCM Term
primTerm Double
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat
instance PrimTerm Str     where primTerm :: Str -> TCM Term
primTerm Str
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
instance PrimTerm Nat     where primTerm :: Nat -> TCM Term
primTerm Nat
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat
instance PrimTerm Lvl     where primTerm :: Lvl -> TCM Term
primTerm Lvl
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel
instance PrimTerm QName   where primTerm :: QName -> TCM Term
primTerm QName
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
instance PrimTerm MetaId  where primTerm :: MetaId -> TCM Term
primTerm MetaId
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
instance PrimTerm Type    where primTerm :: Type'' Term Term -> TCM Term
primTerm Type'' Term Term
_ = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm

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

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

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

-- From Agda term to Haskell value

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

primQNameToWord64sInjective :: TCM PrimitiveImpl
primQNameToWord64sInjective :: TCM PrimitiveImpl
primQNameToWord64sInjective = do
  Type'' Term Term
name    <- QName -> TCMT IO (Type'' Term Term)
forall a. PrimType a => a -> TCMT IO (Type'' Term Term)
primType (QName
forall a. HasCallStack => a
undefined :: QName)
  Type'' Term Term
words   <- (Word64, Word64) -> TCMT IO (Type'' Term Term)
forall a. PrimType a => a -> TCMT IO (Type'' Term Term)
primType ((Word64, Word64)
forall a. HasCallStack => a
undefined :: (Word64, Word64))
  QName
toWords <- PrimFun -> QName
primFunName (PrimFun -> QName) -> TCMT IO PrimFun -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO PrimFun
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m PrimFun
getPrimitive String
"primQNameToWord64s"
  Type'' Term Term -> Type'' Term Term -> QName -> TCM PrimitiveImpl
mkPrimInjective Type'' Term Term
name Type'' Term Term
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 []) <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
  Maybe ArgInfo
minfo <- (ArgInfo -> ArgInfo) -> Maybe ArgInfo -> Maybe ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) (Maybe ArgInfo -> Maybe ArgInfo)
-> TCMT IO (Maybe ArgInfo) -> TCMT IO (Maybe ArgInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead -> TCMT IO (Maybe ArgInfo)
getReflArgInfo ConHead
rf
  (Arg Term -> Term) -> TCM (Arg Term -> Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Arg Term -> Term) -> TCM (Arg Term -> Term))
-> (Arg Term -> Term) -> TCM (Arg Term -> Term)
forall a b. (a -> b) -> a -> b
$ case Maybe ArgInfo
minfo of
    Just ArgInfo
ai -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
rf ConInfo
ci (Elims -> Term) -> (Arg Term -> Elims) -> Arg Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:[]) (Elim' Term -> Elims)
-> (Arg Term -> Elim' Term) -> Arg Term -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term)
-> (Arg Term -> Arg Term) -> Arg Term -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Arg Term -> Arg Term
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
ai
    Maybe ArgInfo
Nothing -> Term -> Arg Term -> Term
forall a b. a -> b -> a
const Term
con

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

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

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

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

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

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


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

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

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

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

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

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

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

mkPrimFun1TCM :: (FromTerm a, ToTerm b, TermLike b) =>
                 TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
mkPrimFun1TCM :: TCMT IO (Type'' Term Term) -> (a -> ReduceM b) -> TCM PrimitiveImpl
mkPrimFun1TCM TCMT IO (Type'' Term Term)
mt a -> ReduceM b
f = do
    FromTermFunction a
toA   <- TCM (FromTermFunction a)
forall a. FromTerm a => TCM (FromTermFunction a)
fromTerm
    b -> ReduceM Term
fromB <- TCM (b -> ReduceM Term)
forall a. ToTerm a => TCM (a -> ReduceM Term)
toTermR
    Type'' Term Term
t     <- TCMT IO (Type'' Term Term)
mt
    PrimitiveImpl -> TCM PrimitiveImpl
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimitiveImpl -> TCM PrimitiveImpl)
-> PrimitiveImpl -> TCM PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> PrimFun -> PrimitiveImpl
PrimImpl Type'' Term Term
t (PrimFun -> PrimitiveImpl) -> PrimFun -> PrimitiveImpl
forall a b. (a -> b) -> a -> b
$ QName
-> Int
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun QName
forall a. HasCallStack => a
__IMPOSSIBLE__ Int
1 ((Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun)
-> (Args -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
      case Args
ts of
        [Arg Term
v] ->
          ReduceM (Reduced (MaybeReduced (Arg Term)) a)
-> (MaybeReduced (Arg Term) -> MaybeReducedArgs)
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a a' b b'.
ReduceM (Reduced a a')
-> (a -> b)
-> (a' -> ReduceM (Reduced b b'))
-> ReduceM (Reduced b b')
redBind (FromTermFunction a
toA Arg Term
v) MaybeReduced (Arg Term) -> MaybeReducedArgs
forall el coll. Singleton el coll => el -> coll
singleton ((a -> ReduceM (Reduced MaybeReducedArgs Term))
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> (a -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ \ a
x -> do
            b
b <- a -> ReduceM b
f a
x
            case b -> Maybe MetaId
forall a. TermLike a => a -> Maybe MetaId
firstMeta b
b of
              Just MetaId
m  -> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduced MaybeReducedArgs Term
 -> ReduceM (Reduced MaybeReducedArgs Term))
-> Reduced MaybeReducedArgs Term
-> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
forall no yes. no -> Reduced no yes
NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced (MetaId -> Arg Term -> Blocked (Arg Term)
forall t. MetaId -> t -> Blocked t
Blocked MetaId
m Arg Term
v)]
              Maybe MetaId
Nothing -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall a a'. a -> ReduceM (Reduced a' a)
redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
-> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< b -> ReduceM Term
fromB b
b
        Args
_ -> ReduceM (Reduced MaybeReducedArgs Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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


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

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

primitiveFunctions :: Map String (TCM PrimitiveImpl)
primitiveFunctions :: Map String (TCM PrimitiveImpl)
primitiveFunctions = (TCM PrimitiveImpl -> TCM PrimitiveImpl)
-> Map String (TCM PrimitiveImpl) -> Map String (TCM PrimitiveImpl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TCM PrimitiveImpl -> TCM PrimitiveImpl
forall a. TCM a -> TCM a
localTCStateSavingWarnings (Map String (TCM PrimitiveImpl) -> Map String (TCM PrimitiveImpl))
-> Map String (TCM PrimitiveImpl) -> Map String (TCM PrimitiveImpl)
forall a b. (a -> b) -> a -> b
$ [(String, TCM PrimitiveImpl)] -> Map String (TCM PrimitiveImpl)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  -- 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)
  [ String
"primShowInteger"     String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Integer -> Str) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> Str
Str (String -> Str) -> (Integer -> String) -> Integer -> Str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show :: Integer -> Str)

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

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

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

  -- Sorts
  , String
"primSetOmega"        String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
mkPrimSetOmega

  -- Floating point functions
  , String
"primNatToFloat"      String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Nat -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral    :: Nat -> Double)
  , String
"primFloatPlus"       String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Double
forall a. Num a => a -> a -> a
(+)             :: Op Double)
  , String
"primFloatMinus"      String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 ((-)             :: Op Double)
  , String
"primFloatTimes"      String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Double
forall a. Num a => a -> a -> a
(*)             :: Op Double)
  , String
"primFloatNegate"     String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Num a => a -> a
negate          :: Fun Double)
  , String
"primFloatDiv"        String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Double
forall a. Fractional a => a -> a -> a
(/)             :: Op Double)
  -- ASR (2016-09-29). We use bitwise equality for comparing Double
  -- because Haskell's Eq, which equates 0.0 and -0.0, allows to prove
  -- a contradiction (see Issue #2169).
  , String
"primFloatEquality"   String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Bool
floatEq         :: Rel Double)
  , String
"primFloatLess"       String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Bool
floatLt         :: Rel Double)
  , String
"primFloatNumericalEquality" String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
(==)     :: Rel Double)
  , String
"primFloatNumericalLess"     String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
(<)      :: Rel Double)
  , String
"primFloatSqrt"       String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
sqrt            :: Double -> Double)
  , String
"primRound"           String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Integer) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
round   (Double -> Integer) -> (Double -> Double) -> Double -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
normaliseNaN :: Double -> Integer)
  , String
"primFloor"           String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Integer) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor   (Double -> Integer) -> (Double -> Double) -> Double -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
normaliseNaN :: Double -> Integer)
  , String
"primCeiling"         String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Integer) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Double -> Integer) -> (Double -> Double) -> Double -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double
normaliseNaN :: Double -> Integer)
  , String
"primExp"             String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
exp             :: Fun Double)
  , String
"primLog"             String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
log             :: Fun Double)
  , String
"primSin"             String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
sin             :: Fun Double)
  , String
"primCos"             String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
cos             :: Fun Double)
  , String
"primTan"             String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
tan             :: Fun Double)
  , String
"primASin"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
asin            :: Fun Double)
  , String
"primACos"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
acos            :: Fun Double)
  , String
"primATan"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Double -> Double
forall a. Floating a => a -> a
atan            :: Fun Double)
  , String
"primATan2"           String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Double -> Double) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Double -> Double -> Double
forall a. RealFloat a => a -> a -> a
atan2           :: Op Double)
  , String
"primShowFloat"       String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Str) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> Str
Str (String -> Str) -> (Double -> String) -> Double -> Str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> String
forall a. Show a => a -> String
show      :: Double -> Str)
  , String
"primFloatToWord64"   String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Double -> Word64) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Double -> Word64
doubleToWord64
  , String
"primFloatToWord64Injective" String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primFloatToWord64Injective

  -- Character functions
  , String
"primCharEquality"       String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Char -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel Char)
  , String
"primIsLower"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isLower
  , String
"primIsDigit"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isDigit
  , String
"primIsAlpha"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isAlpha
  , String
"primIsSpace"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isSpace
  , String
"primIsAscii"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isAscii
  , String
"primIsLatin1"           String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isLatin1
  , String
"primIsPrint"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isPrint
  , String
"primIsHexDigit"         String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Bool) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Bool
isHexDigit
  , String
"primToUpper"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Char) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Char
toUpper
  , String
"primToLower"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Char) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Char -> Char
toLower
  , String
"primCharToNat"          String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Nat) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Nat) -> (Char -> Int) -> Char -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
forall a. Enum a => a -> Int
fromEnum :: Char -> Nat)
  , String
"primCharToNatInjective" String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primCharToNatInjective
  , String
"primNatToChar"          String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Nat -> Char) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Nat -> Int) -> Nat -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> (Nat -> Nat) -> Nat -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`mod` Nat
0x110000)  :: Nat -> Char)
  , String
"primShowChar"           String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Char -> Str) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> Str
Str (String -> Str) -> (Char -> String) -> Char -> Str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> String
forall a. Pretty a => a -> String
prettyShow (Literal -> String) -> (Char -> Literal) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Char -> Literal
LitChar Range
forall a. Range' a
noRange)

  -- String functions
  , String
"primStringToList"          String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Str -> String) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 Str -> String
unStr
  , String
"primStringToListInjective" String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> TCM PrimitiveImpl
primStringToListInjective
  , String
"primStringFromList"        String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (String -> Str) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 String -> Str
Str
  , String
"primStringAppend"          String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Str -> Str -> Str) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (\Str
s1 Str
s2 -> String -> Str
Str (String -> Str) -> String -> Str
forall a b. (a -> b) -> a -> b
$ Str -> String
unStr Str
s1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ Str -> String
unStr Str
s2)
  , String
"primStringEquality"        String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Str -> Str -> Bool) -> TCM PrimitiveImpl
forall a b c.
(PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b,
 PrimType c, ToTerm c) =>
(a -> b -> c) -> TCM PrimitiveImpl
mkPrimFun2 (Str -> Str -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Rel Str)
  , String
"primShowString"            String -> TCM PrimitiveImpl -> (String, TCM PrimitiveImpl)
forall a b. a -> b -> (a, b)
|-> (Str -> Str) -> TCM PrimitiveImpl
forall a b.
(PrimType a, FromTerm a, PrimType b, ToTerm b) =>
(a -> b) -> TCM PrimitiveImpl
mkPrimFun1 (String -> Str
Str (String -> Str) -> (Str -> String) -> Str -> Str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> String
forall a. Pretty a => a -> String
prettyShow (Literal -> String) -> (Str -> Literal) -> Str -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> String -> Literal
LitString Range
forall a. Range' a
noRange (String -> Literal) -> (Str -> String) -> Str -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Str -> String
unStr)

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