{-# 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
$cshowsPrec :: forall a. Show a => Int -> Elim' a -> ShowS
showsPrec :: Int -> Elim' a -> ShowS
$cshow :: forall a. Show a => Elim' a -> String
show :: Elim' a -> String
$cshowList :: forall a. Show a => [Elim' a] -> ShowS
showList :: [Elim' a] -> ShowS
Show)
type Elim = Elim' Term
type Elims = [Elim]

argsToElims :: Args -> Elims
argsToElims :: Args -> Elims
argsToElims = (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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
$cshowsPrec :: forall a. Show a => Int -> Abs a -> ShowS
showsPrec :: Int -> Abs a -> ShowS
$cshow :: forall a. Show a => Abs a -> String
show :: Abs a -> String
$cshowList :: forall a. Show a => [Abs a] -> ShowS
showList :: [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
$cshowsPrec :: Int -> Term -> ShowS
showsPrec :: Int -> Term -> ShowS
$cshow :: Term -> String
show :: Term -> String
$cshowList :: [Term] -> ShowS
showList :: [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
$cshowsPrec :: Int -> Sort -> ShowS
showsPrec :: Int -> Sort -> ShowS
$cshow :: Sort -> String
show :: Sort -> String
$cshowList :: [Sort] -> ShowS
showList :: [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
$cshowsPrec :: Int -> Pattern -> ShowS
showsPrec :: Int -> Pattern -> ShowS
$cshow :: Pattern -> String
show :: Pattern -> String
$cshowList :: [Pattern] -> ShowS
showList :: [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
$cshowsPrec :: Int -> Clause -> ShowS
showsPrec :: Int -> Clause -> ShowS
$cshow :: Clause -> String
show :: Clause -> String
$cshowList :: [Clause] -> ShowS
showList :: [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
$cshowsPrec :: Int -> Definition -> ShowS
showsPrec :: Int -> Definition -> ShowS
$cshow :: Definition -> String
show :: Definition -> String
$cshowList :: [Definition] -> ShowS
showList :: [Definition] -> ShowS
Show)