{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
module Output where
import Control.Arrow ( second )
import Control.Applicative ( (<|>) )
import GHC.Generics ( Generic )
import Data.List ( notElem, elemIndex )
import Data.String ( fromString )
import Data.Aeson
import qualified Data.Aeson as JSON
import qualified Data.Aeson.KeyMap as KM
import Agda.Syntax.Common ( unArg )
import qualified Agda.Syntax.Common as A
import qualified Agda.Syntax.Internal as A
import qualified Agda.Syntax.Literal as A
import Agda.Syntax.Internal
( QName, absName, qnameName, qnameModule, unAbs, unEl, unDom
, nameId, conName, dbPatVarIndex, pDom, telToList, telFromList )
import Agda.Syntax.Translation.InternalToAbstract ( NamedClause(..) )
import qualified Agda.TypeChecking.Monad as A
import Agda.TypeChecking.Monad
( TCM, MonadTCM, liftTCM, typeOfConst, theDef, defName, getConstInfo
, reportSDoc, VerboseLevel )
import qualified Agda.Utils.Pretty as P
import Agda.TypeChecking.Pretty
( PrettyTCM(..), MonadPretty, fsep, punctuate, braces, parens, Doc )
import qualified Agda.TypeChecking.Pretty as P
hiding (text)
type Name = String
type DB = Int
type Head = Either Name DB
infixr 4 :>; pattern x $m:> :: forall {r} {a}. Pretty a -> (String -> a -> r) -> ((# #) -> r) -> r
$b:> :: forall {a}. String -> a -> Pretty a
:> y = Pretty {pretty = x, thing = y}
data Pretty a = Pretty
{ forall a. Pretty a -> String
pretty :: String
, forall a. Pretty a -> a
thing :: a
} deriving (forall x. Pretty a -> Rep (Pretty a) x)
-> (forall x. Rep (Pretty a) x -> Pretty a) -> Generic (Pretty a)
forall x. Rep (Pretty a) x -> Pretty a
forall x. Pretty a -> Rep (Pretty a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Pretty a) x -> Pretty a
forall a x. Pretty a -> Rep (Pretty a) x
$cfrom :: forall a x. Pretty a -> Rep (Pretty a) x
from :: forall x. Pretty a -> Rep (Pretty a) x
$cto :: forall a x. Rep (Pretty a) x -> Pretty a
to :: forall x. Rep (Pretty a) x -> Pretty a
Generic
deriving instance Show a => Show (Pretty a)
instance ToJSON a => ToJSON (Pretty a) where
toJSON :: Pretty a -> Value
toJSON (Pretty{a
String
pretty :: forall a. Pretty a -> String
thing :: forall a. Pretty a -> a
pretty :: String
thing :: a
..}) = let pretty' :: Value
pretty' = String -> Value
forall a. ToJSON a => a -> Value
toJSON String
pretty in
case a -> Value
forall a. ToJSON a => a -> Value
toJSON a
thing of
(Object Object
fs) -> [Pair] -> Value
object (Key
"pretty" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
pretty' Pair -> [Pair] -> [Pair]
forall a. a -> [a] -> [a]
: Object -> [Pair]
forall v. KeyMap v -> [(Key, v)]
KM.toList Object
fs)
t :: Value
t@(Array Array
xs) -> [Pair] -> Value
object [Key
"pretty" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
pretty', Key
"telescope" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
t]
Value
t -> [Pair] -> Value
object [Key
"pretty" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
pretty', Key
"thing" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value -> Value
forall a. ToJSON a => a -> Value
toJSON Value
t]
instance FromJSON a => FromJSON (Pretty a) where
parseJSON :: Value -> Parser (Pretty a)
parseJSON = String
-> (Object -> Parser (Pretty a)) -> Value -> Parser (Pretty a)
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"Pretty" ((Object -> Parser (Pretty a)) -> Value -> Parser (Pretty a))
-> (Object -> Parser (Pretty a)) -> Value -> Parser (Pretty a)
forall a b. (a -> b) -> a -> b
$ \Object
v -> String -> a -> Pretty a
forall {a}. String -> a -> Pretty a
Pretty
(String -> a -> Pretty a)
-> Parser String -> Parser (a -> Pretty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Key -> Parser String
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"pretty"
Parser (a -> Pretty a) -> Parser a -> Parser (Pretty a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
v Object -> Key -> Parser a
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"thing" Parser a -> Parser a -> Parser a
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON (Object -> Value
Object Object
v))
data Reduced a = Reduced
{ forall a. Reduced a -> a
original :: a
, forall a. Reduced a -> Maybe a
simplified :: Maybe a
, forall a. Reduced a -> Maybe a
reduced :: Maybe a
, forall a. Reduced a -> Maybe a
normalised :: Maybe a
} deriving ((forall x. Reduced a -> Rep (Reduced a) x)
-> (forall x. Rep (Reduced a) x -> Reduced a)
-> Generic (Reduced a)
forall x. Rep (Reduced a) x -> Reduced a
forall x. Reduced a -> Rep (Reduced a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Reduced a) x -> Reduced a
forall a x. Reduced a -> Rep (Reduced a) x
$cfrom :: forall a x. Reduced a -> Rep (Reduced a) x
from :: forall x. Reduced a -> Rep (Reduced a) x
$cto :: forall a x. Rep (Reduced a) x -> Reduced a
to :: forall x. Rep (Reduced a) x -> Reduced a
Generic, (forall a b. (a -> b) -> Reduced a -> Reduced b)
-> (forall a b. a -> Reduced b -> Reduced a) -> Functor Reduced
forall a b. a -> Reduced b -> Reduced a
forall a b. (a -> b) -> Reduced a -> Reduced b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Reduced a -> Reduced b
fmap :: forall a b. (a -> b) -> Reduced a -> Reduced b
$c<$ :: forall a b. a -> Reduced b -> Reduced a
<$ :: forall a b. a -> Reduced b -> Reduced a
Functor, (forall m. Monoid m => Reduced m -> m)
-> (forall m a. Monoid m => (a -> m) -> Reduced a -> m)
-> (forall m a. Monoid m => (a -> m) -> Reduced a -> m)
-> (forall a b. (a -> b -> b) -> b -> Reduced a -> b)
-> (forall a b. (a -> b -> b) -> b -> Reduced a -> b)
-> (forall b a. (b -> a -> b) -> b -> Reduced a -> b)
-> (forall b a. (b -> a -> b) -> b -> Reduced a -> b)
-> (forall a. (a -> a -> a) -> Reduced a -> a)
-> (forall a. (a -> a -> a) -> Reduced a -> a)
-> (forall a. Reduced a -> [a])
-> (forall a. Reduced a -> Bool)
-> (forall a. Reduced a -> Int)
-> (forall a. Eq a => a -> Reduced a -> Bool)
-> (forall a. Ord a => Reduced a -> a)
-> (forall a. Ord a => Reduced a -> a)
-> (forall a. Num a => Reduced a -> a)
-> (forall a. Num a => Reduced a -> a)
-> Foldable Reduced
forall a. Eq a => a -> Reduced a -> Bool
forall a. Num a => Reduced a -> a
forall a. Ord a => Reduced a -> a
forall m. Monoid m => Reduced m -> m
forall a. Reduced a -> Bool
forall a. Reduced a -> Int
forall a. Reduced a -> [a]
forall a. (a -> a -> a) -> Reduced a -> a
forall m a. Monoid m => (a -> m) -> Reduced a -> m
forall b a. (b -> a -> b) -> b -> Reduced a -> b
forall a b. (a -> b -> b) -> b -> Reduced a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Reduced m -> m
fold :: forall m. Monoid m => Reduced m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Reduced a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Reduced a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Reduced a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Reduced a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Reduced a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Reduced a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Reduced a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Reduced a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Reduced a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Reduced a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Reduced a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Reduced a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Reduced a -> a
foldr1 :: forall a. (a -> a -> a) -> Reduced a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Reduced a -> a
foldl1 :: forall a. (a -> a -> a) -> Reduced a -> a
$ctoList :: forall a. Reduced a -> [a]
toList :: forall a. Reduced a -> [a]
$cnull :: forall a. Reduced a -> Bool
null :: forall a. Reduced a -> Bool
$clength :: forall a. Reduced a -> Int
length :: forall a. Reduced a -> Int
$celem :: forall a. Eq a => a -> Reduced a -> Bool
elem :: forall a. Eq a => a -> Reduced a -> Bool
$cmaximum :: forall a. Ord a => Reduced a -> a
maximum :: forall a. Ord a => Reduced a -> a
$cminimum :: forall a. Ord a => Reduced a -> a
minimum :: forall a. Ord a => Reduced a -> a
$csum :: forall a. Num a => Reduced a -> a
sum :: forall a. Num a => Reduced a -> a
$cproduct :: forall a. Num a => Reduced a -> a
product :: forall a. Num a => Reduced a -> a
Foldable, Functor Reduced
Foldable Reduced
Functor Reduced
-> Foldable Reduced
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Reduced a -> f (Reduced b))
-> (forall (f :: * -> *) a.
Applicative f =>
Reduced (f a) -> f (Reduced a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Reduced a -> m (Reduced b))
-> (forall (m :: * -> *) a.
Monad m =>
Reduced (m a) -> m (Reduced a))
-> Traversable Reduced
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Reduced (m a) -> m (Reduced a)
forall (f :: * -> *) a.
Applicative f =>
Reduced (f a) -> f (Reduced a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Reduced a -> m (Reduced b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Reduced a -> f (Reduced b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Reduced a -> f (Reduced b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Reduced a -> f (Reduced b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Reduced (f a) -> f (Reduced a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Reduced (f a) -> f (Reduced a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Reduced a -> m (Reduced b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Reduced a -> m (Reduced b)
$csequence :: forall (m :: * -> *) a. Monad m => Reduced (m a) -> m (Reduced a)
sequence :: forall (m :: * -> *) a. Monad m => Reduced (m a) -> m (Reduced a)
Traversable)
deriving instance Show a => Show (Reduced a)
instance ToJSON a => ToJSON (Reduced a) where
toJSON :: Reduced a -> Value
toJSON r :: Reduced a
r@(Reduced{a
Maybe a
original :: forall a. Reduced a -> a
simplified :: forall a. Reduced a -> Maybe a
reduced :: forall a. Reduced a -> Maybe a
normalised :: forall a. Reduced a -> Maybe a
original :: a
simplified :: Maybe a
reduced :: Maybe a
normalised :: Maybe a
..})
| Maybe a
Nothing <- Maybe a
simplified Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
reduced Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
normalised
= a -> Value
forall a. ToJSON a => a -> Value
toJSON a
original
| Bool
otherwise
= Options -> Reduced a -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
jsonOpts Reduced a
r
instance FromJSON a => FromJSON (Reduced a) where
parseJSON :: Value -> Parser (Reduced a)
parseJSON = String
-> (Object -> Parser (Reduced a)) -> Value -> Parser (Reduced a)
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"Object" ((Object -> Parser (Reduced a)) -> Value -> Parser (Reduced a))
-> (Object -> Parser (Reduced a)) -> Value -> Parser (Reduced a)
forall a b. (a -> b) -> a -> b
$ \Object
v -> a -> Maybe a -> Maybe a -> Maybe a -> Reduced a
forall a. a -> Maybe a -> Maybe a -> Maybe a -> Reduced a
Reduced
(a -> Maybe a -> Maybe a -> Maybe a -> Reduced a)
-> Parser a -> Parser (Maybe a -> Maybe a -> Maybe a -> Reduced a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Object
v Object -> Key -> Parser a
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"original" Parser a -> Parser a -> Parser a
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON (Object -> Value
Object Object
v))
Parser (Maybe a -> Maybe a -> Maybe a -> Reduced a)
-> Parser (Maybe a) -> Parser (Maybe a -> Maybe a -> Reduced a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Key -> Parser (Maybe a)
forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"simplified"
Parser (Maybe a -> Maybe a -> Reduced a)
-> Parser (Maybe a) -> Parser (Maybe a -> Reduced a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Key -> Parser (Maybe a)
forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"reduced"
Parser (Maybe a -> Reduced a)
-> Parser (Maybe a) -> Parser (Reduced a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Key -> Parser (Maybe a)
forall a. FromJSON a => Object -> Key -> Parser (Maybe a)
.:? Key
"normalised"
infixr 4 :~; pattern x $m:~ :: forall {r} {a}. Named a -> (String -> a -> r) -> ((# #) -> r) -> r
$b:~ :: forall {a}. String -> a -> Named a
:~ y = Named {name = x, item = y}
data Named a = Named
{ forall a. Named a -> String
name :: Name
, forall a. Named a -> a
item :: a
} deriving ((forall x. Named a -> Rep (Named a) x)
-> (forall x. Rep (Named a) x -> Named a) -> Generic (Named a)
forall x. Rep (Named a) x -> Named a
forall x. Named a -> Rep (Named a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Named a) x -> Named a
forall a x. Named a -> Rep (Named a) x
$cfrom :: forall a x. Named a -> Rep (Named a) x
from :: forall x. Named a -> Rep (Named a) x
$cto :: forall a x. Rep (Named a) x -> Named a
to :: forall x. Rep (Named a) x -> Named a
Generic, Int -> Named a -> ShowS
[Named a] -> ShowS
Named a -> String
(Int -> Named a -> ShowS)
-> (Named a -> String) -> ([Named a] -> ShowS) -> Show (Named a)
forall a. Show a => Int -> Named a -> ShowS
forall a. Show a => [Named a] -> ShowS
forall a. Show a => Named a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Named a -> ShowS
showsPrec :: Int -> Named a -> ShowS
$cshow :: forall a. Show a => Named a -> String
show :: Named a -> String
$cshowList :: forall a. Show a => [Named a] -> ShowS
showList :: [Named a] -> ShowS
Show)
instance ToJSON a => ToJSON (Named a) where
toJSON :: Named a -> Value
toJSON (Named{a
String
name :: forall a. Named a -> String
item :: forall a. Named a -> a
name :: String
item :: a
..}) = let name' :: Value
name' = String -> Value
forall a. ToJSON a => a -> Value
toJSON String
name in
case a -> Value
forall a. ToJSON a => a -> Value
toJSON a
item of
(Object Object
fs) -> [Pair] -> Value
object (Key
"name" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
name' Pair -> [Pair] -> [Pair]
forall a. a -> [a] -> [a]
: Object -> [Pair]
forall v. KeyMap v -> [(Key, v)]
KM.toList Object
fs)
Value
x -> [Pair] -> Value
object [Key
"name" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
name', Key
"item" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value -> Value
forall a. ToJSON a => a -> Value
toJSON Value
x]
instance FromJSON a => FromJSON (Named a) where
parseJSON :: Value -> Parser (Named a)
parseJSON = String -> (Object -> Parser (Named a)) -> Value -> Parser (Named a)
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"Named" ((Object -> Parser (Named a)) -> Value -> Parser (Named a))
-> (Object -> Parser (Named a)) -> Value -> Parser (Named a)
forall a b. (a -> b) -> a -> b
$ \Object
v -> String -> a -> Named a
forall {a}. String -> a -> Named a
Named
(String -> a -> Named a) -> Parser String -> Parser (a -> Named a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Key -> Parser String
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"name"
Parser (a -> Named a) -> Parser a -> Parser (Named a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Object
v Object -> Key -> Parser a
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"item" Parser a -> Parser a -> Parser a
forall a. Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON (Object -> Value
Object Object
v))
type FileData = Named TrainData
data TrainData = TrainData
{ TrainData -> [ScopeEntry]
scopeGlobal :: [ScopeEntry]
, TrainData -> [ScopeEntry]
scopeLocal :: [ScopeEntry]
, TrainData -> Maybe [ScopeEntry]
scopePrivate :: Maybe [ScopeEntry]
} deriving (forall x. TrainData -> Rep TrainData x)
-> (forall x. Rep TrainData x -> TrainData) -> Generic TrainData
forall x. Rep TrainData x -> TrainData
forall x. TrainData -> Rep TrainData x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TrainData -> Rep TrainData x
from :: forall x. TrainData -> Rep TrainData x
$cto :: forall x. Rep TrainData x -> TrainData
to :: forall x. Rep TrainData x -> TrainData
Generic
instance ToJSON TrainData where toJSON :: TrainData -> Value
toJSON = Options -> TrainData -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
jsonOpts
instance FromJSON TrainData where parseJSON :: Value -> Parser TrainData
parseJSON = Options -> Value -> Parser TrainData
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
jsonOpts
type ScopeEntry = Named ScopeEntry'
data ScopeEntry' = ScopeEntry
{ ScopeEntry' -> Pretty (Reduced Type)
_type :: Pretty (Reduced Type)
, ScopeEntry' -> Maybe (Pretty Definition)
definition :: Maybe (Pretty Definition)
, ScopeEntry' -> Maybe [Sample]
holes :: Maybe [Sample]
} deriving ((forall x. ScopeEntry' -> Rep ScopeEntry' x)
-> (forall x. Rep ScopeEntry' x -> ScopeEntry')
-> Generic ScopeEntry'
forall x. Rep ScopeEntry' x -> ScopeEntry'
forall x. ScopeEntry' -> Rep ScopeEntry' x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ScopeEntry' -> Rep ScopeEntry' x
from :: forall x. ScopeEntry' -> Rep ScopeEntry' x
$cto :: forall x. Rep ScopeEntry' x -> ScopeEntry'
to :: forall x. Rep ScopeEntry' x -> ScopeEntry'
Generic, Int -> ScopeEntry' -> ShowS
[ScopeEntry'] -> ShowS
ScopeEntry' -> String
(Int -> ScopeEntry' -> ShowS)
-> (ScopeEntry' -> String)
-> ([ScopeEntry'] -> ShowS)
-> Show ScopeEntry'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeEntry' -> ShowS
showsPrec :: Int -> ScopeEntry' -> ShowS
$cshow :: ScopeEntry' -> String
show :: ScopeEntry' -> String
$cshowList :: [ScopeEntry'] -> ShowS
showList :: [ScopeEntry'] -> ShowS
Show)
instance ToJSON ScopeEntry' where toJSON :: ScopeEntry' -> Value
toJSON = Options -> ScopeEntry' -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
jsonOpts
instance FromJSON ScopeEntry' where parseJSON :: Value -> Parser ScopeEntry'
parseJSON = Options -> Value -> Parser ScopeEntry'
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
jsonOpts
data Sample = Sample
{ Sample -> Pretty Telescope
ctx :: Pretty Telescope
, Sample -> Pretty (Reduced Type)
goal :: Pretty (Reduced Type)
, Sample -> Pretty (Reduced Type)
term :: Pretty (Reduced Term)
, Sample -> [String]
premises :: [Name]
} deriving ((forall x. Sample -> Rep Sample x)
-> (forall x. Rep Sample x -> Sample) -> Generic Sample
forall x. Rep Sample x -> Sample
forall x. Sample -> Rep Sample x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Sample -> Rep Sample x
from :: forall x. Sample -> Rep Sample x
$cto :: forall x. Rep Sample x -> Sample
to :: forall x. Rep Sample x -> Sample
Generic, Int -> Sample -> ShowS
[Sample] -> ShowS
Sample -> String
(Int -> Sample -> ShowS)
-> (Sample -> String) -> ([Sample] -> ShowS) -> Show Sample
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Sample -> ShowS
showsPrec :: Int -> Sample -> ShowS
$cshow :: Sample -> String
show :: Sample -> String
$cshowList :: [Sample] -> ShowS
showList :: [Sample] -> ShowS
Show, [Sample] -> Value
[Sample] -> Encoding
Sample -> Value
Sample -> Encoding
(Sample -> Value)
-> (Sample -> Encoding)
-> ([Sample] -> Value)
-> ([Sample] -> Encoding)
-> ToJSON Sample
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
$ctoJSON :: Sample -> Value
toJSON :: Sample -> Value
$ctoEncoding :: Sample -> Encoding
toEncoding :: Sample -> Encoding
$ctoJSONList :: [Sample] -> Value
toJSONList :: [Sample] -> Value
$ctoEncodingList :: [Sample] -> Encoding
toEncodingList :: [Sample] -> Encoding
ToJSON, Value -> Parser [Sample]
Value -> Parser Sample
(Value -> Parser Sample)
-> (Value -> Parser [Sample]) -> FromJSON Sample
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser Sample
parseJSON :: Value -> Parser Sample
$cparseJSONList :: Value -> Parser [Sample]
parseJSONList :: Value -> Parser [Sample]
FromJSON)
data Definition
= ADT {Definition -> [Type]
variants :: [Type]}
| Constructor {Definition -> String
reference :: Name, Definition -> Integer
variant :: Integer}
| Record {Definition -> Telescope
telescope :: Telescope, Definition -> [Type]
fields :: [Type]}
| Function {Definition -> [Clause]
clauses :: [Clause]}
| Postulate {}
| Primitive {}
deriving ((forall x. Definition -> Rep Definition x)
-> (forall x. Rep Definition x -> Definition) -> Generic Definition
forall x. Rep Definition x -> Definition
forall x. Definition -> Rep Definition x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Definition -> Rep Definition x
from :: forall x. Definition -> Rep Definition x
$cto :: forall x. Rep Definition x -> Definition
to :: forall x. Rep Definition x -> Definition
Generic, Int -> Definition -> ShowS
[Definition] -> ShowS
Definition -> String
(Int -> Definition -> ShowS)
-> (Definition -> String)
-> ([Definition] -> ShowS)
-> Show Definition
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Definition -> ShowS
showsPrec :: Int -> Definition -> ShowS
$cshow :: Definition -> String
show :: Definition -> String
$cshowList :: [Definition] -> ShowS
showList :: [Definition] -> ShowS
Show, [Definition] -> Value
[Definition] -> Encoding
Definition -> Value
Definition -> Encoding
(Definition -> Value)
-> (Definition -> Encoding)
-> ([Definition] -> Value)
-> ([Definition] -> Encoding)
-> ToJSON Definition
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
$ctoJSON :: Definition -> Value
toJSON :: Definition -> Value
$ctoEncoding :: Definition -> Encoding
toEncoding :: Definition -> Encoding
$ctoJSONList :: [Definition] -> Value
toJSONList :: [Definition] -> Value
$ctoEncodingList :: [Definition] -> Encoding
toEncodingList :: [Definition] -> Encoding
ToJSON, Value -> Parser [Definition]
Value -> Parser Definition
(Value -> Parser Definition)
-> (Value -> Parser [Definition]) -> FromJSON Definition
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser Definition
parseJSON :: Value -> Parser Definition
$cparseJSONList :: Value -> Parser [Definition]
parseJSONList :: Value -> Parser [Definition]
FromJSON)
data Clause = Clause
{ Clause -> Telescope
_telescope :: Telescope
, Clause -> [Type]
patterns :: [Pattern]
, Clause -> Maybe Type
body :: Maybe Term
} deriving ((forall x. Clause -> Rep Clause x)
-> (forall x. Rep Clause x -> Clause) -> Generic Clause
forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Clause -> Rep Clause x
from :: forall x. Clause -> Rep Clause x
$cto :: forall x. Rep Clause x -> Clause
to :: forall x. Rep Clause x -> Clause
Generic, Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Clause -> ShowS
showsPrec :: Int -> Clause -> ShowS
$cshow :: Clause -> String
show :: Clause -> String
$cshowList :: [Clause] -> ShowS
showList :: [Clause] -> ShowS
Show)
instance ToJSON Clause where toJSON :: Clause -> Value
toJSON = Options -> Clause -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
jsonOpts
instance FromJSON Clause where parseJSON :: Value -> Parser Clause
parseJSON = Options -> Value -> Parser Clause
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
jsonOpts
type Telescope = [Named (Pretty Type)]
type Pattern = Term
type Type = Term
data Term
= Pi Bool (Named Term) Term
| Lam (Named Term)
| App Head [Term]
| Lit String
| Sort String
| Level String
| UnsolvedMeta
deriving ((forall x. Type -> Rep Type x)
-> (forall x. Rep Type x -> Type) -> Generic Type
forall x. Rep Type x -> Type
forall x. Type -> Rep Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Type -> Rep Type x
from :: forall x. Type -> Rep Type x
$cto :: forall x. Rep Type x -> Type
to :: forall x. Rep Type x -> Type
Generic, Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Type -> ShowS
showsPrec :: Int -> Type -> ShowS
$cshow :: Type -> String
show :: Type -> String
$cshowList :: [Type] -> ShowS
showList :: [Type] -> ShowS
Show, Value -> Parser [Type]
Value -> Parser Type
(Value -> Parser Type) -> (Value -> Parser [Type]) -> FromJSON Type
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser Type
parseJSON :: Value -> Parser Type
$cparseJSONList :: Value -> Parser [Type]
parseJSONList :: Value -> Parser [Type]
FromJSON)
instance ToJSON Term where
toJSON :: Type -> Value
toJSON = \case
(Pi Bool
isDep (String
n :~ Type
dom) Type
codom) -> [Pair] -> Value
object
[ Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"Pi"
, Key
"name" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
n
, Key
"domain" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Type -> Value
forall a. ToJSON a => a -> Value
toJSON Type
dom
, Key
"codomain" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Type -> Value
forall a. ToJSON a => a -> Value
toJSON Type
codom
]
(Lam (String
n :~ Type
f)) -> [Pair] -> Value
object
[ Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"Lambda"
, Key
"abstraction" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
n
, Key
"body" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Type -> Value
forall a. ToJSON a => a -> Value
toJSON Type
f
]
(App Head
f [Type]
xs) ->
if [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
xs then
Value
refHead
else
[Pair] -> Value
object [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"Application", Key
"head" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Value
refHead, Key
"arguments" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= [Type] -> Value
forall a. ToJSON a => a -> Value
toJSON [Type]
xs]
where
refHead :: Value
refHead = [Pair] -> Value
object ([Pair] -> Value) -> [Pair] -> Value
forall a b. (a -> b) -> a -> b
$ case Head
f of
(Left String
n) -> [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"ScopeReference", Key
"name" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
n]
(Right Int
i) -> [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"DeBruijn", Key
"index" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= Int -> Value
forall a. ToJSON a => a -> Value
toJSON Int
i]
(Lit String
s) -> [Pair] -> Value
object [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"Literal", Key
"literal" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
s]
(Sort String
s) -> [Pair] -> Value
object [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"Sort", Key
"sort" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
s]
(Level String
s) -> [Pair] -> Value
object [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"Level", Key
"level" Key -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> Pair
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
s]
Type
UnsolvedMeta -> [Pair] -> Value
object [Text -> Pair
forall {kv}. KeyValue kv => Text -> kv
tag Text
"UnsolvedMetavariable"]
where tag :: Text -> kv
tag Text
s = Key
"tag" Key -> Value -> kv
forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
forall v. ToJSON v => Key -> v -> kv
.= Text -> Value
JSON.String Text
s
class (~>) a b | a -> b where
convert, go :: a -> TCM b
convert = a -> TCM b
forall a b. (a ~> b) => a -> TCM b
go
instance A.Definition ~> Definition where
go :: Definition -> TCM Definition
go = Defn -> TCM Definition
forall a b. (a ~> b) => a -> TCM b
go (Defn -> TCM Definition)
-> (Definition -> Defn) -> Definition -> TCM Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef
instance A.Defn ~> Definition where
go :: Defn -> TCM Definition
go = \case
A.AbstractDefn Defn
defn -> Defn -> TCM Definition
forall a b. (a ~> b) => a -> TCM b
go Defn
defn
A.Function{[Clause]
Maybe Bool
Maybe [QName]
Maybe QName
Maybe Compiled
Maybe SplitTree
Maybe CompiledClauses
Maybe ExtLamInfo
Either ProjectionLikenessMissing Projection
IsAbstract
Delayed
FunctionInverse
Set FunctionFlag
funClauses :: [Clause]
funCompiled :: Maybe CompiledClauses
funSplitTree :: Maybe SplitTree
funTreeless :: Maybe Compiled
funCovering :: [Clause]
funInv :: FunctionInverse
funMutual :: Maybe [QName]
funAbstr :: IsAbstract
funDelayed :: Delayed
funProjection :: Either ProjectionLikenessMissing Projection
funFlags :: Set FunctionFlag
funTerminates :: Maybe Bool
funExtLam :: Maybe ExtLamInfo
funWith :: Maybe QName
funIsKanOp :: Maybe QName
funClauses :: Defn -> [Clause]
funCompiled :: Defn -> Maybe CompiledClauses
funSplitTree :: Defn -> Maybe SplitTree
funTreeless :: Defn -> Maybe Compiled
funCovering :: Defn -> [Clause]
funInv :: Defn -> FunctionInverse
funMutual :: Defn -> Maybe [QName]
funAbstr :: Defn -> IsAbstract
funDelayed :: Defn -> Delayed
funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funFlags :: Defn -> Set FunctionFlag
funTerminates :: Defn -> Maybe Bool
funExtLam :: Defn -> Maybe ExtLamInfo
funWith :: Defn -> Maybe QName
funIsKanOp :: Defn -> Maybe QName
..} -> let cls :: [Clause]
cls = (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Clause -> Bool
isNotCubical [Clause]
funClauses in
[Clause] -> Definition
Function ([Clause] -> Definition) -> TCMT IO [Clause] -> TCM Definition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Clause -> TCMT IO Clause
forall a b. (a ~> b) => a -> TCM b
go [Clause]
cls
A.Datatype{Int
[QName]
Maybe [QName]
Maybe QName
Maybe Clause
IsAbstract
Sort
dataPars :: Int
dataIxs :: Int
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataMutual :: Maybe [QName]
dataAbstr :: IsAbstract
dataPathCons :: [QName]
dataTranspIx :: Maybe QName
dataTransp :: Maybe QName
dataPars :: Defn -> Int
dataIxs :: Defn -> Int
dataClause :: Defn -> Maybe Clause
dataCons :: Defn -> [QName]
dataSort :: Defn -> Sort
dataMutual :: Defn -> Maybe [QName]
dataAbstr :: Defn -> IsAbstract
dataPathCons :: Defn -> [QName]
dataTranspIx :: Defn -> Maybe QName
dataTransp :: Defn -> Maybe QName
..} -> do
[Term]
tys <- (Type'' Term Term -> Term) -> [Type'' Term Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl ([Type'' Term Term] -> [Term])
-> TCMT IO [Type'' Term Term] -> TCMT IO [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO (Type'' Term Term))
-> [QName] -> TCMT IO [Type'' Term Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse QName -> TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Type'' Term Term)
typeOfConst [QName]
dataCons
[Type] -> Definition
ADT ([Type] -> Definition) -> TCMT IO [Type] -> TCM Definition
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> TCMT IO Type) -> [Term] -> TCMT IO [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go [Term]
tys
A.Record{Bool
Int
[Dom QName]
Maybe Bool
Maybe [QName]
Maybe Induction
Maybe Clause
IsAbstract
PatternOrCopattern
Telescope
ConHead
CompKit
EtaEquality
recPars :: Int
recClause :: Maybe Clause
recConHead :: ConHead
recNamedCon :: Bool
recFields :: [Dom QName]
recTel :: Telescope
recMutual :: Maybe [QName]
recEtaEquality' :: EtaEquality
recPatternMatching :: PatternOrCopattern
recInduction :: Maybe Induction
recTerminates :: Maybe Bool
recAbstr :: IsAbstract
recComp :: CompKit
recPars :: Defn -> Int
recClause :: Defn -> Maybe Clause
recConHead :: Defn -> ConHead
recNamedCon :: Defn -> Bool
recFields :: Defn -> [Dom QName]
recTel :: Defn -> Telescope
recMutual :: Defn -> Maybe [QName]
recEtaEquality' :: Defn -> EtaEquality
recPatternMatching :: Defn -> PatternOrCopattern
recInduction :: Defn -> Maybe Induction
recTerminates :: Defn -> Maybe Bool
recAbstr :: Defn -> IsAbstract
recComp :: Defn -> CompKit
..} -> do
(Telescope
tel, Telescope
fs) <- Int -> Telescope -> (Telescope, Telescope)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
recPars (Telescope -> (Telescope, Telescope))
-> TCMT IO Telescope -> TCMT IO (Telescope, Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> TCMT IO Telescope
forall a b. (a ~> b) => a -> TCM b
go Telescope
recTel
Definition -> TCM Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> TCM Definition) -> Definition -> TCM Definition
forall a b. (a -> b) -> a -> b
$ Telescope -> [Type] -> Definition
Record Telescope
tel (Pretty Type -> Type
forall a. Pretty a -> a
thing (Pretty Type -> Type)
-> (Named (Pretty Type) -> Pretty Type)
-> Named (Pretty Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (Pretty Type) -> Pretty Type
forall a. Named a -> a
item (Named (Pretty Type) -> Type) -> Telescope -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
fs)
A.Constructor{Int
[IsForced]
Maybe [Bool]
Maybe [QName]
IsAbstract
Induction
QName
ConHead
CompKit
conPars :: Int
conArity :: Int
conSrcCon :: ConHead
conData :: QName
conAbstr :: IsAbstract
conInd :: Induction
conComp :: CompKit
conProj :: Maybe [QName]
conForced :: [IsForced]
conErased :: Maybe [Bool]
conPars :: Defn -> Int
conArity :: Defn -> Int
conSrcCon :: Defn -> ConHead
conData :: Defn -> QName
conAbstr :: Defn -> IsAbstract
conInd :: Defn -> Induction
conComp :: Defn -> CompKit
conProj :: Defn -> Maybe [QName]
conForced :: Defn -> [IsForced]
conErased :: Defn -> Maybe [Bool]
..} -> do
let cn :: QName
cn = ConHead -> QName
conName ConHead
conSrcCon
Defn
d <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
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
conData
Definition -> TCM Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Definition -> TCM Definition) -> Definition -> TCM Definition
forall a b. (a -> b) -> a -> b
$ case Defn
d of
A.Datatype{Int
[QName]
Maybe [QName]
Maybe QName
Maybe Clause
IsAbstract
Sort
dataPars :: Defn -> Int
dataIxs :: Defn -> Int
dataClause :: Defn -> Maybe Clause
dataCons :: Defn -> [QName]
dataSort :: Defn -> Sort
dataMutual :: Defn -> Maybe [QName]
dataAbstr :: Defn -> IsAbstract
dataPathCons :: Defn -> [QName]
dataTranspIx :: Defn -> Maybe QName
dataTransp :: Defn -> Maybe QName
dataPars :: Int
dataIxs :: Int
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataMutual :: Maybe [QName]
dataAbstr :: IsAbstract
dataPathCons :: [QName]
dataTranspIx :: Maybe QName
dataTransp :: Maybe QName
..} ->
let Just Int
ix = String -> [String] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (QName -> String
unqualify QName
cn) (QName -> String
unqualify (QName -> String) -> [QName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QName]
dataCons)
in String -> Integer -> Definition
Constructor (QName -> String
forall a. Pretty a => a -> String
pp QName
conData) (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
ix)
A.Record{Bool
Int
[Dom QName]
Maybe Bool
Maybe [QName]
Maybe Induction
Maybe Clause
IsAbstract
PatternOrCopattern
Telescope
ConHead
CompKit
EtaEquality
recPars :: Defn -> Int
recClause :: Defn -> Maybe Clause
recConHead :: Defn -> ConHead
recNamedCon :: Defn -> Bool
recFields :: Defn -> [Dom QName]
recTel :: Defn -> Telescope
recMutual :: Defn -> Maybe [QName]
recEtaEquality' :: Defn -> EtaEquality
recPatternMatching :: Defn -> PatternOrCopattern
recInduction :: Defn -> Maybe Induction
recTerminates :: Defn -> Maybe Bool
recAbstr :: Defn -> IsAbstract
recComp :: Defn -> CompKit
recPars :: Int
recClause :: Maybe Clause
recConHead :: ConHead
recNamedCon :: Bool
recFields :: [Dom QName]
recTel :: Telescope
recMutual :: Maybe [QName]
recEtaEquality' :: EtaEquality
recPatternMatching :: PatternOrCopattern
recInduction :: Maybe Induction
recTerminates :: Maybe Bool
recAbstr :: IsAbstract
recComp :: CompKit
..} -> String -> Integer -> Definition
Constructor (QName -> String
forall a. Pretty a => a -> String
pp QName
conData) Integer
0
A.Primitive{String
[Clause]
Maybe CompiledClauses
IsAbstract
FunctionInverse
primAbstr :: IsAbstract
primName :: String
primClauses :: [Clause]
primInv :: FunctionInverse
primCompiled :: Maybe CompiledClauses
primAbstr :: Defn -> IsAbstract
primName :: Defn -> String
primClauses :: Defn -> [Clause]
primInv :: Defn -> FunctionInverse
primCompiled :: Defn -> Maybe CompiledClauses
..} -> Definition -> TCM Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
Primitive
A.PrimitiveSort{String
Sort
primSortName :: String
primSortSort :: Sort
primSortName :: Defn -> String
primSortSort :: Defn -> Sort
..} -> Definition -> TCM Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
Primitive
A.Axiom{Bool
axiomConstTransp :: Bool
axiomConstTransp :: Defn -> Bool
..} -> Definition -> TCM Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
Postulate
d :: Defn
d@A.DataOrRecSig{Int
datarecPars :: Int
datarecPars :: Defn -> Int
..} -> String -> Defn -> TCM Definition
forall a b. (Pretty a, Show a) => String -> a -> b
panic String
"dataOrRecSig" Defn
d
d :: Defn
d@Defn
A.GeneralizableVar -> String -> Defn -> TCM Definition
forall a b. (Pretty a, Show a) => String -> a -> b
panic String
"generalizable variable" Defn
d
instance A.Clause ~> Clause where
go :: Clause -> TCMT IO Clause
go A.Clause{Bool
NAPs
Maybe Bool
Maybe (Arg (Type'' Term Term))
Maybe ModuleName
Maybe Term
Range
ExpandedEllipsis
Telescope
clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
namedClausePats :: NAPs
clauseBody :: Maybe Term
clauseType :: Maybe (Arg (Type'' Term Term))
clauseCatchall :: Bool
clauseExact :: Maybe Bool
clauseRecursive :: Maybe Bool
clauseUnreachable :: Maybe Bool
clauseEllipsis :: ExpandedEllipsis
clauseWhereModule :: Maybe ModuleName
clauseLHSRange :: Clause -> Range
clauseFullRange :: Clause -> Range
clauseTel :: Clause -> Telescope
namedClausePats :: Clause -> NAPs
clauseBody :: Clause -> Maybe Term
clauseType :: Clause -> Maybe (Arg (Type'' Term Term))
clauseCatchall :: Clause -> Bool
clauseExact :: Clause -> Maybe Bool
clauseRecursive :: Clause -> Maybe Bool
clauseUnreachable :: Clause -> Maybe Bool
clauseEllipsis :: Clause -> ExpandedEllipsis
clauseWhereModule :: Clause -> Maybe ModuleName
..} =
Telescope -> [Type] -> Maybe Type -> Clause
Clause (Telescope -> [Type] -> Maybe Type -> Clause)
-> TCMT IO Telescope -> TCMT IO ([Type] -> Maybe Type -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> TCMT IO Telescope
forall a b. (a ~> b) => a -> TCM b
go Telescope
clauseTel
TCMT IO ([Type] -> Maybe Type -> Clause)
-> TCMT IO [Type] -> TCMT IO (Maybe Type -> Clause)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (DeBruijnPattern -> TCMT IO Type)
-> [DeBruijnPattern] -> TCMT IO [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DeBruijnPattern -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
A.namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (Arg (Named NamedName DeBruijnPattern)
-> Named NamedName DeBruijnPattern)
-> Arg (Named NamedName DeBruijnPattern)
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named NamedName DeBruijnPattern)
-> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg (Arg (Named NamedName DeBruijnPattern) -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs
namedClausePats)
TCMT IO (Maybe Type -> Clause)
-> TCMT IO (Maybe Type) -> TCMT IO Clause
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> TCMT IO Type) -> Maybe Term -> TCMT IO (Maybe Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Maybe Term
clauseBody
instance A.DeBruijnPattern ~> Pattern where
go :: DeBruijnPattern -> TCMT IO Type
go = \case
A.VarP PatternInfo
_ DBPatVar
v -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Head -> [Type] -> Type
App (Int -> Head
forall a b. b -> Either a b
Right (Int -> Head) -> Int -> Head
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
v) []
A.DotP PatternInfo
_ Term
t -> Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Term
t
A.ConP ConHead
c ConPatternInfo
_ NAPs
ps -> do
Head -> [Type] -> Type
App (String -> Head
forall a b. a -> Either a b
Left (String -> Head) -> String -> Head
forall a b. (a -> b) -> a -> b
$ ConHead -> String
forall a. Pretty a => a -> String
pp ConHead
c) ([Type] -> Type) -> TCMT IO [Type] -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DeBruijnPattern -> TCMT IO Type)
-> [DeBruijnPattern] -> TCMT IO [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DeBruijnPattern -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
A.namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (Arg (Named NamedName DeBruijnPattern)
-> Named NamedName DeBruijnPattern)
-> Arg (Named NamedName DeBruijnPattern)
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named NamedName DeBruijnPattern)
-> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg (Arg (Named NamedName DeBruijnPattern) -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NAPs
ps)
A.LitP PatternInfo
_ Literal
lit -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ String -> Type
Lit (Literal -> String
forall a. Pretty a => a -> String
pp Literal
lit)
A.ProjP ProjOrigin
_ QName
qn -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Head -> [Type] -> Type
App (String -> Head
forall a b. a -> Either a b
Left (String -> Head) -> String -> Head
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
pp QName
qn) []
p :: DeBruijnPattern
p@(A.IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
_) -> String -> DeBruijnPattern -> TCMT IO Type
forall a b. (Pretty a, Show a) => String -> a -> b
panic String
"pattern (cubical)" DeBruijnPattern
p
p :: DeBruijnPattern
p@(A.DefP PatternInfo
_ QName
_ NAPs
_) -> String -> DeBruijnPattern -> TCMT IO Type
forall a b. (Pretty a, Show a) => String -> a -> b
panic String
"pattern (cubical)" DeBruijnPattern
p
instance A.Telescope ~> Telescope where
go :: Telescope -> TCMT IO Telescope
go = (Dom (String, Type'' Term Term) -> TCMT IO (Named (Pretty Type)))
-> [Dom (String, Type'' Term Term)] -> TCMT IO Telescope
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Dom (String, Type'' Term Term) -> TCMT IO (Named (Pretty Type))
action ([Dom (String, Type'' Term Term)] -> TCMT IO Telescope)
-> (Telescope -> [Dom (String, Type'' Term Term)])
-> Telescope
-> TCMT IO Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Dom (String, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (String, t)]
A.telToList
where
action :: A.Dom (Name, A.Type) -> TCM (Named (Pretty Type))
action :: Dom (String, Type'' Term Term) -> TCMT IO (Named (Pretty Type))
action Dom (String, Type'' Term Term)
dty = do
let (String
n, Type'' Term Term
ty) = Dom (String, Type'' Term Term) -> (String, Type'' Term Term)
forall t e. Dom' t e -> e
unDom Dom (String, Type'' Term Term)
dty
Doc
pty <- Type'' Term Term -> TCMT IO Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Type'' Term Term
ty
Type
ty' <- Type'' Term Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Type'' Term Term
ty
let pdty :: String
pdty = Doc -> String
prender (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Dom (String, Type'' Term Term) -> Doc -> Doc
forall a. LensHiding a => a -> Doc -> Doc
pDom Dom (String, Type'' Term Term)
dty (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" : " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Doc -> String
prender Doc
pty
Named (Pretty Type) -> TCMT IO (Named (Pretty Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Named (Pretty Type) -> TCMT IO (Named (Pretty Type)))
-> Named (Pretty Type) -> TCMT IO (Named (Pretty Type))
forall a b. (a -> b) -> a -> b
$ String
n String -> Pretty Type -> Named (Pretty Type)
forall {a}. String -> a -> Named a
:~ String
pdty String -> Type -> Pretty Type
forall {a}. String -> a -> Pretty a
:> Type
ty'
instance A.Type ~> Type where
go :: Type'' Term Term -> TCMT IO Type
go = Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Term -> TCMT IO Type)
-> (Type'' Term Term -> Term) -> Type'' Term Term -> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> Term
forall t a. Type'' t a -> a
A.unEl
instance A.Term ~> Term where
go :: Term -> TCMT IO Type
go = ((Term -> TCMT IO Type) -> (Term -> Term) -> Term -> TCMT IO Type)
-> (Term -> Term) -> (Term -> TCMT IO Type) -> Term -> TCMT IO Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Term -> TCMT IO Type) -> (Term -> Term) -> Term -> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Term -> Term
A.unSpine ((Term -> TCMT IO Type) -> Term -> TCMT IO Type)
-> (Term -> TCMT IO Type) -> Term -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ \case
(A.Pi Dom (Type'' Term Term)
ty Abs (Type'' Term Term)
ab) -> do
let nameUsed :: Bool
nameUsed = Maybe NamedName -> String
forall a. Pretty a => a -> String
pp (Dom (Type'' Term Term) -> Maybe NamedName
forall t e. Dom' t e -> Maybe NamedName
A.domName Dom (Type'' Term Term)
ty) String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String
"_", String
"(nothing)"]
Type
ty' <- Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term) -> Type'' Term Term -> Term
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom (Type'' Term Term)
ty)
Type
ab' <- Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term) -> Type'' Term Term -> Term
forall a b. (a -> b) -> a -> b
$ Abs (Type'' Term Term) -> Type'' Term Term
forall a. Abs a -> a
unAbs Abs (Type'' Term Term)
ab)
Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Bool -> Named Type -> Type -> Type
Pi Bool
nameUsed (Abs (Type'' Term Term) -> String
forall a. Abs a -> String
absName Abs (Type'' Term Term)
ab String -> Type -> Named Type
forall {a}. String -> a -> Named a
:~ Type
ty') Type
ab'
(A.Lam ArgInfo
_ Abs Term
ab) -> do
Type
ab' <- Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
ab)
Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Named Type -> Type
Lam (ShowS
forall a. Pretty a => a -> String
pp (Abs Term -> String
forall a. Abs a -> String
absName Abs Term
ab) String -> Type -> Named Type
forall {a}. String -> a -> Named a
:~ Type
ab')
(A.Var Int
i Elims
xs) -> Head -> [Type] -> Type
App (Int -> Head
forall a b. b -> Either a b
Right Int
i) ([Type] -> Type) -> TCMT IO [Type] -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Elim -> TCMT IO Type) -> Elims -> TCMT IO [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Elim -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Elims
xs)
(A.Def QName
f Elims
xs) -> Head -> [Type] -> Type
App (String -> Head
forall a b. a -> Either a b
Left (String -> Head) -> String -> Head
forall a b. (a -> b) -> a -> b
$ QName -> String
ppName QName
f) ([Type] -> Type) -> TCMT IO [Type] -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Elim -> TCMT IO Type) -> Elims -> TCMT IO [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Elim -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Elims
xs)
(A.Con ConHead
c ConInfo
_ Elims
xs) -> Head -> [Type] -> Type
App (String -> Head
forall a b. a -> Either a b
Left (String -> Head) -> String -> Head
forall a b. (a -> b) -> a -> b
$ QName -> String
ppName (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) ([Type] -> Type) -> TCMT IO [Type] -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Elim -> TCMT IO Type) -> Elims -> TCMT IO [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Elim -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Elims
xs)
(A.Lit Literal
x) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ String -> Type
Lit (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ Literal -> String
forall a. Pretty a => a -> String
pp Literal
x
(A.Level Level
x) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ String -> Type
Level (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ Level -> String
forall a. Pretty a => a -> String
pp Level
x
(A.Sort Sort
x) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ String -> Type
Sort (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ Sort -> String
forall a. Pretty a => a -> String
pp Sort
x
(A.MetaV MetaId
_ Elims
_) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
UnsolvedMeta
(A.DontCare Term
t) -> Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Term
t
t :: Term
t@(A.Dummy String
_ Elims
_) -> String -> Term -> TCMT IO Type
forall a b. (Pretty a, Show a) => String -> a -> b
panic String
"term" Term
t
instance A.Elim ~> Term where
go :: Elim -> TCMT IO Type
go = \case
(A.Apply Arg Term
x) -> Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x)
(A.Proj ProjOrigin
_ QName
qn) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Head -> [Type] -> Type
App (String -> Head
forall a b. a -> Either a b
Left (String -> Head) -> String -> Head
forall a b. (a -> b) -> a -> b
$ QName -> String
ppName QName
qn) []
(A.IApply Term
_ Term
_ Term
x) -> Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Term
x
pp :: P.Pretty a => a -> String
pp :: forall a. Pretty a => a -> String
pp = a -> String
forall a. Pretty a => a -> String
P.prettyShow
ppm :: (MonadPretty m, P.PrettyTCM a) => a -> m Doc
ppm :: forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
P.prettyTCM
prender :: Doc -> String
prender :: Doc -> String
prender = Style -> Doc -> String
P.renderStyle (Mode -> Int -> Float -> Style
P.Style Mode
P.OneLineMode Int
0 Float
0.0)
pinterleave :: (Applicative m, Semigroup (m Doc)) => m Doc -> [m Doc] -> m Doc
pinterleave :: forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> m Doc
pinterleave m Doc
sep = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([m Doc] -> [m Doc]) -> [m Doc] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
sep
pbindings :: (MonadPretty m, PrettyTCM a) => [(String, a)] -> [m Doc]
pbindings :: forall (m :: * -> *) a.
(MonadPretty m, PrettyTCM a) =>
[(String, a)] -> [m Doc]
pbindings = ((String, a) -> m Doc) -> [(String, a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (((String, a) -> m Doc) -> [(String, a)] -> [m Doc])
-> ((String, a) -> m Doc) -> [(String, a)] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ \(String
n, a
ty) -> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm String
n m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
" : " m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> a -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm a
ty
report :: MonadTCM m => VerboseLevel -> TCM Doc -> m ()
report :: forall (m :: * -> *). MonadTCM m => Int -> TCMT IO Doc -> m ()
report Int
n TCMT IO Doc
x = TCM () -> m ()
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> m ()) -> TCM () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"agda2train" Int
n TCMT IO Doc
x
panic :: (P.Pretty a, Show a) => String -> a -> b
panic :: forall a b. (Pretty a, Show a) => String -> a -> b
panic String
s a
t = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$
String
"[PANIC] unexpected " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
s String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
": " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Pretty a => a -> String
pp a
t String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n show: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
forall a. Pretty a => a -> String
pp (a -> String
forall a. Show a => a -> String
show a
t)
ppName :: A.QName -> String
ppName :: QName -> String
ppName QName
qn = QName -> String
forall a. Pretty a => a -> String
pp QName
qn String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"<" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (NameId -> Int
forall a. Enum a => a -> Int
fromEnum (NameId -> Int) -> NameId -> Int
forall a b. (a -> b) -> a -> b
$ Name -> NameId
nameId (Name -> NameId) -> Name -> NameId
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
qn) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
">"
unqualify :: A.QName -> String
unqualify :: QName -> String
unqualify = Name -> String
forall a. Pretty a => a -> String
pp (Name -> String) -> (QName -> Name) -> QName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName
(\/) :: (a -> Bool) -> (a -> Bool) -> (a -> Bool)
(a -> Bool
f \/ :: forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
\/ a -> Bool
g) a
x = a -> Bool
f a
x Bool -> Bool -> Bool
|| a -> Bool
g a
x
isNotCubical :: A.Clause -> Bool
isNotCubical :: Clause -> Bool
isNotCubical A.Clause{Bool
NAPs
Maybe Bool
Maybe (Arg (Type'' Term Term))
Maybe ModuleName
Maybe Term
Range
ExpandedEllipsis
Telescope
clauseLHSRange :: Clause -> Range
clauseFullRange :: Clause -> Range
clauseTel :: Clause -> Telescope
namedClausePats :: Clause -> NAPs
clauseBody :: Clause -> Maybe Term
clauseType :: Clause -> Maybe (Arg (Type'' Term Term))
clauseCatchall :: Clause -> Bool
clauseExact :: Clause -> Maybe Bool
clauseRecursive :: Clause -> Maybe Bool
clauseUnreachable :: Clause -> Maybe Bool
clauseEllipsis :: Clause -> ExpandedEllipsis
clauseWhereModule :: Clause -> Maybe ModuleName
clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
namedClausePats :: NAPs
clauseBody :: Maybe Term
clauseType :: Maybe (Arg (Type'' Term Term))
clauseCatchall :: Bool
clauseExact :: Maybe Bool
clauseRecursive :: Maybe Bool
clauseUnreachable :: Maybe Bool
clauseEllipsis :: ExpandedEllipsis
clauseWhereModule :: Maybe ModuleName
..}
| Just (A.Def QName
qn Elims
_) <- Maybe Term
clauseBody
= ModuleName -> String
forall a. Pretty a => a -> String
pp (QName -> ModuleName
qnameModule QName
qn) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"Agda.Primitive.Cubical"
| Bool
otherwise
= Bool
True
jsonOpts :: JSON.Options
jsonOpts :: Options
jsonOpts = Options
defaultOptions
{ omitNothingFields :: Bool
omitNothingFields = Bool
True
, fieldLabelModifier :: ShowS
fieldLabelModifier = \case
(Char
'_' : String
s) -> String
s
String
"scopeGlobal" -> String
"scope-global"
String
"scopeLocal" -> String
"scope-local"
String
"scopePrivate" -> String
"scope-private"
String
s -> String
s
}
instance P.PrettyTCM A.Definition where
prettyTCM :: forall (m :: * -> *). MonadPretty m => Definition -> m Doc
prettyTCM Definition
d = Defn -> m Doc
go (Definition -> Defn
theDef Definition
d)
where
go :: Defn -> m Doc
go = \case
A.AbstractDefn Defn
defn -> Defn -> m Doc
go Defn
defn
A.Function{[Clause]
Maybe Bool
Maybe [QName]
Maybe QName
Maybe Compiled
Maybe SplitTree
Maybe CompiledClauses
Maybe ExtLamInfo
Either ProjectionLikenessMissing Projection
IsAbstract
Delayed
FunctionInverse
Set FunctionFlag
funClauses :: Defn -> [Clause]
funCompiled :: Defn -> Maybe CompiledClauses
funSplitTree :: Defn -> Maybe SplitTree
funTreeless :: Defn -> Maybe Compiled
funCovering :: Defn -> [Clause]
funInv :: Defn -> FunctionInverse
funMutual :: Defn -> Maybe [QName]
funAbstr :: Defn -> IsAbstract
funDelayed :: Defn -> Delayed
funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funFlags :: Defn -> Set FunctionFlag
funTerminates :: Defn -> Maybe Bool
funExtLam :: Defn -> Maybe ExtLamInfo
funWith :: Defn -> Maybe QName
funIsKanOp :: Defn -> Maybe QName
funClauses :: [Clause]
funCompiled :: Maybe CompiledClauses
funSplitTree :: Maybe SplitTree
funTreeless :: Maybe Compiled
funCovering :: [Clause]
funInv :: FunctionInverse
funMutual :: Maybe [QName]
funAbstr :: IsAbstract
funDelayed :: Delayed
funProjection :: Either ProjectionLikenessMissing Projection
funFlags :: Set FunctionFlag
funTerminates :: Maybe Bool
funExtLam :: Maybe ExtLamInfo
funWith :: Maybe QName
funIsKanOp :: Maybe QName
..} -> let cls :: [Clause]
cls = (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Clause -> Bool
isNotCubical [Clause]
funClauses in
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" |"
([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ NamedClause -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm (NamedClause -> m Doc)
-> (Clause -> NamedClause) -> Clause -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause (Definition -> QName
defName Definition
d) Bool
True (Clause -> m Doc) -> [Clause] -> [m Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Clause]
cls
A.Datatype{Int
[QName]
Maybe [QName]
Maybe QName
Maybe Clause
IsAbstract
Sort
dataPars :: Defn -> Int
dataIxs :: Defn -> Int
dataClause :: Defn -> Maybe Clause
dataCons :: Defn -> [QName]
dataSort :: Defn -> Sort
dataMutual :: Defn -> Maybe [QName]
dataAbstr :: Defn -> IsAbstract
dataPathCons :: Defn -> [QName]
dataTranspIx :: Defn -> Maybe QName
dataTransp :: Defn -> Maybe QName
dataPars :: Int
dataIxs :: Int
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataMutual :: Maybe [QName]
dataAbstr :: IsAbstract
dataPathCons :: [QName]
dataTranspIx :: Maybe QName
dataTransp :: Maybe QName
..} -> do
[Term]
tys <- (Type'' Term Term -> Term) -> [Type'' Term Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl ([Type'' Term Term] -> [Term]) -> m [Type'' Term Term] -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> m (Type'' Term Term)) -> [QName] -> m [Type'' Term Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse QName -> m (Type'' Term Term)
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Type'' Term Term)
typeOfConst [QName]
dataCons
m Doc -> [m Doc] -> m Doc
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> m Doc
pinterleave m Doc
" |" ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [(String, Term)] -> [m Doc]
forall (m :: * -> *) a.
(MonadPretty m, PrettyTCM a) =>
[(String, a)] -> [m Doc]
pbindings ([(String, Term)] -> [m Doc]) -> [(String, Term)] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [String] -> [Term] -> [(String, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip (QName -> String
unqualify (QName -> String) -> [QName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QName]
dataCons) [Term]
tys
A.Record{Bool
Int
[Dom QName]
Maybe Bool
Maybe [QName]
Maybe Induction
Maybe Clause
IsAbstract
PatternOrCopattern
Telescope
ConHead
CompKit
EtaEquality
recPars :: Defn -> Int
recClause :: Defn -> Maybe Clause
recConHead :: Defn -> ConHead
recNamedCon :: Defn -> Bool
recFields :: Defn -> [Dom QName]
recTel :: Defn -> Telescope
recMutual :: Defn -> Maybe [QName]
recEtaEquality' :: Defn -> EtaEquality
recPatternMatching :: Defn -> PatternOrCopattern
recInduction :: Defn -> Maybe Induction
recTerminates :: Defn -> Maybe Bool
recAbstr :: Defn -> IsAbstract
recComp :: Defn -> CompKit
recPars :: Int
recClause :: Maybe Clause
recConHead :: ConHead
recNamedCon :: Bool
recFields :: [Dom QName]
recTel :: Telescope
recMutual :: Maybe [QName]
recEtaEquality' :: EtaEquality
recPatternMatching :: PatternOrCopattern
recInduction :: Maybe Induction
recTerminates :: Maybe Bool
recAbstr :: IsAbstract
recComp :: CompKit
..} ->
let ([Dom (String, Type'' Term Term)]
tel, [Dom (String, Type'' Term Term)]
fs) = Int
-> [Dom (String, Type'' Term Term)]
-> ([Dom (String, Type'' Term Term)],
[Dom (String, Type'' Term Term)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
recPars ([Dom (String, Type'' Term Term)]
-> ([Dom (String, Type'' Term Term)],
[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
$ Telescope -> [Dom (String, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
recTel in
(if [Dom (String, Type'' Term Term)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Dom (String, Type'' Term Term)]
tel then m Doc
"" else Telescope -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm ([Dom (String, Type'' Term Term)] -> Telescope
telFromList [Dom (String, Type'' Term Term)]
tel) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
" |- ")
m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> (m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
braces (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> m Doc
forall (m :: * -> *).
(Applicative m, Semigroup (m Doc)) =>
m Doc -> [m Doc] -> m Doc
pinterleave m Doc
" ;" ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [(String, Type'' Term Term)] -> [m Doc]
forall (m :: * -> *) a.
(MonadPretty m, PrettyTCM a) =>
[(String, a)] -> [m Doc]
pbindings ([(String, Type'' Term Term)] -> [m Doc])
-> [(String, Type'' Term Term)] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ Dom (String, Type'' Term Term) -> (String, Type'' Term Term)
forall t e. Dom' t e -> e
unDom (Dom (String, Type'' Term Term) -> (String, Type'' Term Term))
-> [Dom (String, Type'' Term Term)] -> [(String, Type'' Term Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom (String, Type'' Term Term)]
fs)
A.Constructor{Int
[IsForced]
Maybe [Bool]
Maybe [QName]
IsAbstract
Induction
QName
ConHead
CompKit
conPars :: Defn -> Int
conArity :: Defn -> Int
conSrcCon :: Defn -> ConHead
conData :: Defn -> QName
conAbstr :: Defn -> IsAbstract
conInd :: Defn -> Induction
conComp :: Defn -> CompKit
conProj :: Defn -> Maybe [QName]
conForced :: Defn -> [IsForced]
conErased :: Defn -> Maybe [Bool]
conPars :: Int
conArity :: Int
conSrcCon :: ConHead
conData :: QName
conAbstr :: IsAbstract
conInd :: Induction
conComp :: CompKit
conProj :: Maybe [QName]
conForced :: [IsForced]
conErased :: Maybe [Bool]
..} -> do
let cn :: QName
cn = ConHead -> QName
conName ConHead
conSrcCon
Defn
d <- 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
conData
case Defn
d of
A.Datatype{Int
[QName]
Maybe [QName]
Maybe QName
Maybe Clause
IsAbstract
Sort
dataPars :: Defn -> Int
dataIxs :: Defn -> Int
dataClause :: Defn -> Maybe Clause
dataCons :: Defn -> [QName]
dataSort :: Defn -> Sort
dataMutual :: Defn -> Maybe [QName]
dataAbstr :: Defn -> IsAbstract
dataPathCons :: Defn -> [QName]
dataTranspIx :: Defn -> Maybe QName
dataTransp :: Defn -> Maybe QName
dataPars :: Int
dataIxs :: Int
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataMutual :: Maybe [QName]
dataAbstr :: IsAbstract
dataPathCons :: [QName]
dataTranspIx :: Maybe QName
dataTransp :: Maybe QName
..} ->
let Just Int
ix = String -> [String] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (QName -> String
unqualify QName
cn) (QName -> String
unqualify (QName -> String) -> [QName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QName]
dataCons)
in QName -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm QName
conData m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"@" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Int -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm Int
ix
A.Record{Bool
Int
[Dom QName]
Maybe Bool
Maybe [QName]
Maybe Induction
Maybe Clause
IsAbstract
PatternOrCopattern
Telescope
ConHead
CompKit
EtaEquality
recPars :: Defn -> Int
recClause :: Defn -> Maybe Clause
recConHead :: Defn -> ConHead
recNamedCon :: Defn -> Bool
recFields :: Defn -> [Dom QName]
recTel :: Defn -> Telescope
recMutual :: Defn -> Maybe [QName]
recEtaEquality' :: Defn -> EtaEquality
recPatternMatching :: Defn -> PatternOrCopattern
recInduction :: Defn -> Maybe Induction
recTerminates :: Defn -> Maybe Bool
recAbstr :: Defn -> IsAbstract
recComp :: Defn -> CompKit
recPars :: Int
recClause :: Maybe Clause
recConHead :: ConHead
recNamedCon :: Bool
recFields :: [Dom QName]
recTel :: Telescope
recMutual :: Maybe [QName]
recEtaEquality' :: EtaEquality
recPatternMatching :: PatternOrCopattern
recInduction :: Maybe Induction
recTerminates :: Maybe Bool
recAbstr :: IsAbstract
recComp :: CompKit
..} -> QName -> m Doc
forall (m :: * -> *) a. (MonadPretty m, PrettyTCM a) => a -> m Doc
ppm QName
conData m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"@0"
A.Primitive{String
[Clause]
Maybe CompiledClauses
IsAbstract
FunctionInverse
primAbstr :: Defn -> IsAbstract
primName :: Defn -> String
primClauses :: Defn -> [Clause]
primInv :: Defn -> FunctionInverse
primCompiled :: Defn -> Maybe CompiledClauses
primAbstr :: IsAbstract
primName :: String
primClauses :: [Clause]
primInv :: FunctionInverse
primCompiled :: Maybe CompiledClauses
..} -> m Doc
"<Primitive>"
A.PrimitiveSort{String
Sort
primSortName :: Defn -> String
primSortSort :: Defn -> Sort
primSortName :: String
primSortSort :: Sort
..} -> m Doc
"<PrimitiveSort>"
A.Axiom{Bool
axiomConstTransp :: Defn -> Bool
axiomConstTransp :: Bool
..} -> m Doc
"<Axiom>"
A.DataOrRecSig{Int
datarecPars :: Defn -> Int
datarecPars :: Int
..} -> m Doc
"<DataOrRecSig>"
Defn
A.GeneralizableVar -> m Doc
"<GeneralizableVar>"