    {-# OPTIONS_GHC -fwarn-missing-signatures #-}

    module Agda.Syntax.Reflected where

    import Data.Text (Text)

    import Agda.Syntax.Common
    import Agda.Syntax.Literal
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Internal (Dom)

    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1

    type Args       = [Arg Term]

    data Elim' a = Apply (Arg a) -- no record projections for now
      deriving (Int -> Elim' a -> ShowS
    [Elim' a] -> ShowS
    Elim' a -> String
    (Int -> Elim' a -> ShowS)
    -> (Elim' a -> String) -> ([Elim' a] -> ShowS) -> Show (Elim' a)
    forall a. Show a => Int -> Elim' a -> ShowS
    forall a. Show a => [Elim' a] -> ShowS
    forall a. Show a => Elim' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Elim' a] -> ShowS
    $cshowList :: forall a. Show a => [Elim' a] -> ShowS
    show :: Elim' a -> String
    $cshow :: forall a. Show a => Elim' a -> String
    showsPrec :: Int -> Elim' a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Elim' a -> ShowS
    Show)
    type Elim = Elim' Term
    type Elims = [Elim]

    argsToElims :: Args -> Elims
    argsToElims :: Args -> Elims
    argsToElims = (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply

    data Abs a = Abs String a
      deriving (Int -> Abs a -> ShowS
    [Abs a] -> ShowS
    Abs a -> String
    (Int -> Abs a -> ShowS)
    -> (Abs a -> String) -> ([Abs a] -> ShowS) -> Show (Abs a)
    forall a. Show a => Int -> Abs a -> ShowS
    forall a. Show a => [Abs a] -> ShowS
    forall a. Show a => Abs a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Abs a] -> ShowS
    $cshowList :: forall a. Show a => [Abs a] -> ShowS
    show :: Abs a -> String
    $cshow :: forall a. Show a => Abs a -> String
    showsPrec :: Int -> Abs a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Abs a -> ShowS
    Show)

    data Term = Var Int Elims
              | Con QName Elims
              | Def QName Elims
              | Meta MetaId Elims
              | Lam Hiding (Abs Term)
              | ExtLam (List1 Clause) Elims
              | Pi (Dom Type) (Abs Type)
              | Sort Sort
              | Lit Literal
              | Unknown
      deriving (Int -> Term -> ShowS
    [Term] -> ShowS
    Term -> String
    (Int -> Term -> ShowS)
    -> (Term -> String) -> ([Term] -> ShowS) -> Show Term
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Term] -> ShowS
    $cshowList :: [Term] -> ShowS
    show :: Term -> String
    $cshow :: Term -> String
    showsPrec :: Int -> Term -> ShowS
    $cshowsPrec :: Int -> Term -> ShowS
    Show)

    type Type = Term

    data Sort = SetS Term
              | LitS Integer
              | PropS Term
              | PropLitS Integer
              | InfS Integer
              | UnknownS
      deriving (Int -> Sort -> ShowS
    [Sort] -> ShowS
    Sort -> String
    (Int -> Sort -> ShowS)
    -> (Sort -> String) -> ([Sort] -> ShowS) -> Show Sort
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Sort] -> ShowS
    $cshowList :: [Sort] -> ShowS
    show :: Sort -> String
    $cshow :: Sort -> String
    showsPrec :: Int -> Sort -> ShowS
    $cshowsPrec :: Int -> Sort -> ShowS
    Show)

    data Pattern = ConP QName [Arg Pattern]
                 | DotP Term
                 | VarP Int
                 | LitP Literal
                 | AbsurdP Int
                 | ProjP QName
      deriving (Int -> Pattern -> ShowS
    [Pattern] -> ShowS
    Pattern -> String
    (Int -> Pattern -> ShowS)
    -> (Pattern -> String) -> ([Pattern] -> ShowS) -> Show Pattern
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Pattern] -> ShowS
    $cshowList :: [Pattern] -> ShowS
    show :: Pattern -> String
    $cshow :: Pattern -> String
    showsPrec :: Int -> Pattern -> ShowS
    $cshowsPrec :: Int -> Pattern -> ShowS
    Show)

    data Clause
      = Clause
        { Clause -> [(Text, Arg Term)]
    clauseTel  :: [(Text, Arg Type)]
        , Clause -> [Arg Pattern]
    clausePats :: [Arg Pattern]
        , Clause -> Term
    clauseRHS  :: Term
        }
      | AbsurdClause
        { clauseTel  :: [(Text, Arg Type)]
        , clausePats :: [Arg Pattern]
        }
      deriving (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
    showList :: [Clause] -> ShowS
    $cshowList :: [Clause] -> ShowS
    show :: Clause -> String
    $cshow :: Clause -> String
    showsPrec :: Int -> Clause -> ShowS
    $cshowsPrec :: Int -> Clause -> ShowS
    Show)

    data Definition = FunDef Type [Clause]
                    | DataDef   -- nothing for now
                    | RecordDef -- nothing for now
                    | DataConstructor
                    | Axiom
                    | Primitive
      deriving (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
    showList :: [Definition] -> ShowS
    $cshowList :: [Definition] -> ShowS
    show :: Definition -> String
    $cshow :: Definition -> String
    showsPrec :: Int -> Definition -> ShowS
    $cshowsPrec :: Int -> Definition -> ShowS
    Show)