{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
-- | Defines the structure of the training data, as well as how to translate
-- internal Agda definition to this format.
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)

-- * Types

-- | Name identifiers.
type Name = String
-- | DeBruijn indices.
type DB   = Int
-- | A head of a λ-application can either be a defined name in the global scope,
-- or a DeBruijn index into the local context.
type Head = Either Name DB

-- * Generic constructions

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}
-- | Bundle a thing with its "pretty" version.
--
-- NB: In JSON format, we follow a /shallow/ encoding with "pretty" being
-- an additional field and "thing" just inlined in the top-level record.
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))

-- | Bundle a term with (several of) its normalised forms.
--
-- We do not repeat identical elements in subsequent evaluations
-- (in the order simp/red/norm) and some fields may not be populated due to
-- the evaluation taking to long and leading to a timeout (currently 2 seconds).
--
-- NB: Like 'Named', encoded in a /shallow/ JSON.
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}

-- | Bundle a thing with its name.
--
-- NB: Like 'Named' and 'Reduced', encoded in a /shallow/ JSON.
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))

-- * Concrete types (~ JSON schema)

-- | Data for a file include the filename and its training data.
type FileData = Named TrainData
-- | The training data for a module, divided into three parts.
data TrainData = TrainData
  { TrainData -> [ScopeEntry]
scopeGlobal  :: [ScopeEntry]
  -- ^ The /global/ scope, giving the types and definitions of all @import@ statements.
  --
  -- NB: does not contain any /holes/ for subterms.
  , TrainData -> [ScopeEntry]
scopeLocal   :: [ScopeEntry]
  -- ^ The /local/ scope, containing the types, definitions, and training data
  -- for each of this module's definitions.
  , TrainData -> Maybe [ScopeEntry]
scopePrivate :: Maybe [ScopeEntry]
  -- ^ The /private/ scope, containing private definitions not exported to the public,
  -- as well as system-generated definitions stemming from @where@ or @with@.
  } 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

-- | Every 'ScopeEntry'' is /named/.
type ScopeEntry = Named ScopeEntry'
-- | An entry in the scope: type, definitions, and holes.
data ScopeEntry' = ScopeEntry
  { ScopeEntry' -> Pretty (Reduced Type)
_type      :: Pretty (Reduced Type)
  -- ^ The entry's type.
  , ScopeEntry' -> Maybe (Pretty Definition)
definition :: Maybe (Pretty Definition)
  -- ^ The actual body of this entry's definition.
  , ScopeEntry' -> Maybe [Sample]
holes      :: Maybe [Sample]
  -- ^ Training data for each of the subterms in this entry's 'definition'.
  } 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

-- | The training sample for each sub-hole.
data Sample = Sample
  { Sample -> Pretty Telescope
ctx      :: Pretty Telescope
  -- ^ The current context, as a /binding telescope/.
  , Sample -> Pretty (Reduced Type)
goal     :: Pretty (Reduced Type)
  -- ^ The current goal, i.e. type of the sub-term.
  --
  -- NB: DeBruijn indices here refer to the 'ctx'.
  , Sample -> Pretty (Reduced Type)
term     :: Pretty (Reduced Term)
  -- ^ The term that successfully fills the current 'goal'.
  , Sample -> [String]
premises :: [Name]
  -- ^ Definitions used in this "proof", intended to be used for /premise selection/.
  } 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)


-- | Agda definitions: datatypes, records, functions, postulates and primitives.
data Definition
  = ADT {Definition -> [Type]
variants :: [Type]}
  -- ^ e.g.
  -- data ℕ : Set where
  --   zero : ℕ
  --   suc  : ℕ → ℕ
  | Constructor {Definition -> String
reference :: Name, Definition -> Integer
variant :: Integer}
  -- ^ e.g. `(ℕ, 0) ~ zero` or `(ℕ, 1) ~ suc`
  | Record {Definition -> Telescope
telescope :: Telescope, Definition -> [Type]
fields :: [Type]}
  -- ^ e.g.
  -- record X : Set where
  --   field x : ℕ
  --         y : ℕ
  | Function {Definition -> [Clause]
clauses :: [Clause]}
  -- ^ e.g.
  -- f []       = []
  -- f (x ∷ xs) = x ∷ x ∷ xs
  | Postulate {}
  -- ^ e.g. `postulate pred : ℕ → ℕ`
  | Primitive {}
  -- ^ e.g. `primitive primShowNat : ℕ → String`
  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)

-- | Function clauses.
data Clause = Clause
  { Clause -> Telescope
_telescope :: Telescope
  -- ^ the telescope induced by the clause's context and patterns
  , Clause -> [Type]
patterns  :: [Pattern]
  -- ^ the actual patterns of this function clause
  , Clause -> Maybe Type
body      :: Maybe Term
  -- ^ the right hand side of the clause (@Nothing@ for absurd clauses)
  } 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

-- | A telescope is a sequence of (named) types, a.k.a. bindings.
type Telescope = [Named (Pretty Type)]
-- | We under-approximate patterns as terms,
-- e.g. losing information about forced patterns.
type Pattern   = Term
-- | Types are the same as terms.
type Type      = Term

-- | The AST of Agda terms.
data Term
  = Pi Bool (Named Term) Term -- ^ e.g. @∀ {A : Set}. A → A@
  | Lam (Named Term)          -- ^ e.g. @λ x. x@
  | App Head [Term]           -- ^ e.g. @f x (x + x)@ or @@0 (λ x. x)@
  | Lit String   -- ^ e.g. @42@ or @"something"@
  | Sort String  -- ^ e.g. @Set@
  | Level String -- ^ e.g. @0ℓ@
  | UnsolvedMeta -- ^ i.e. @{!!}@
  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 -- T0D0: remove if "(nothing) (or _)?"
      , 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

-- * Conversion from Agda's internal syntax

-- | Converting between two types @a@ and @b@ under Agda's typechecking monad.
--
-- NB: 'go' is only used internally to de-clutter the recursive calls.
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
      -- NB: handle funWith and funExtLam
      [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
      -- NB: what is a dataClause???
      [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
      -- NB: incorporate conHead/namedCon in the future for accuracy
      --     + to solve the issue with private (non-public) fields
      (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)
           -- ^ drop visibility and name information
           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
    -- ** abstractions
    (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')
    -- ** applications
    (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)
    -- ** other constants
    (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
    -- ** there are some occurrences of `DontCare` in the standard library
    (A.DontCare Term
t) -> Term -> TCMT IO Type
forall a b. (a ~> b) => a -> TCM b
go Term
t
    -- ** crash on the rest (should never be encountered)
    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

-- * Utilities

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

-- | Configure JSON to omit empty (optional) fields and switch
-- from camelCase to kebab-case.
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>"