{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PatternSynonyms #-}

-- | The treeless syntax is intended to be used as input for the compiler backends.
-- It is more low-level than Internal syntax and is not used for type checking.
--
-- Some of the features of treeless syntax are:
-- - case expressions instead of case trees
-- - no instantiated datatypes / constructors
module Agda.Syntax.Treeless
    ( module Agda.Syntax.Abstract.Name
    , module Agda.Syntax.Treeless
    ) where

import Control.Arrow (first, second)

import Data.Data (Data)
import Data.Word

import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name

data Compiled = Compiled
  { Compiled -> TTerm
cTreeless :: TTerm
  , Compiled -> [Bool]
cArgUsage :: [Bool] }
  deriving (Typeable Compiled
DataType
Constr
Typeable Compiled
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Compiled -> c Compiled)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Compiled)
-> (Compiled -> Constr)
-> (Compiled -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Compiled))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled))
-> ((forall b. Data b => b -> b) -> Compiled -> Compiled)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Compiled -> r)
-> (forall u. (forall d. Data d => d -> u) -> Compiled -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Compiled -> m Compiled)
-> Data Compiled
Compiled -> DataType
Compiled -> Constr
(forall b. Data b => b -> b) -> Compiled -> Compiled
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Compiled -> c Compiled
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Compiled
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u
forall u. (forall d. Data d => d -> u) -> Compiled -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Compiled -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Compiled -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Compiled -> m Compiled
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Compiled -> m Compiled
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Compiled
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Compiled -> c Compiled
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Compiled)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled)
$cCompiled :: Constr
$tCompiled :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Compiled -> m Compiled
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Compiled -> m Compiled
gmapMp :: (forall d. Data d => d -> m d) -> Compiled -> m Compiled
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Compiled -> m Compiled
gmapM :: (forall d. Data d => d -> m d) -> Compiled -> m Compiled
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Compiled -> m Compiled
gmapQi :: Int -> (forall d. Data d => d -> u) -> Compiled -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Compiled -> u
gmapQ :: (forall d. Data d => d -> u) -> Compiled -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Compiled -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Compiled -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Compiled -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Compiled -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Compiled -> r
gmapT :: (forall b. Data b => b -> b) -> Compiled -> Compiled
$cgmapT :: (forall b. Data b => b -> b) -> Compiled -> Compiled
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Compiled)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Compiled)
dataTypeOf :: Compiled -> DataType
$cdataTypeOf :: Compiled -> DataType
toConstr :: Compiled -> Constr
$ctoConstr :: Compiled -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Compiled
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Compiled
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Compiled -> c Compiled
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Compiled -> c Compiled
$cp1Data :: Typeable Compiled
Data, Int -> Compiled -> ShowS
[Compiled] -> ShowS
Compiled -> String
(Int -> Compiled -> ShowS)
-> (Compiled -> String) -> ([Compiled] -> ShowS) -> Show Compiled
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Compiled] -> ShowS
$cshowList :: [Compiled] -> ShowS
show :: Compiled -> String
$cshow :: Compiled -> String
showsPrec :: Int -> Compiled -> ShowS
$cshowsPrec :: Int -> Compiled -> ShowS
Show, Compiled -> Compiled -> Bool
(Compiled -> Compiled -> Bool)
-> (Compiled -> Compiled -> Bool) -> Eq Compiled
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Compiled -> Compiled -> Bool
$c/= :: Compiled -> Compiled -> Bool
== :: Compiled -> Compiled -> Bool
$c== :: Compiled -> Compiled -> Bool
Eq, Eq Compiled
Eq Compiled
-> (Compiled -> Compiled -> Ordering)
-> (Compiled -> Compiled -> Bool)
-> (Compiled -> Compiled -> Bool)
-> (Compiled -> Compiled -> Bool)
-> (Compiled -> Compiled -> Bool)
-> (Compiled -> Compiled -> Compiled)
-> (Compiled -> Compiled -> Compiled)
-> Ord Compiled
Compiled -> Compiled -> Bool
Compiled -> Compiled -> Ordering
Compiled -> Compiled -> Compiled
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Compiled -> Compiled -> Compiled
$cmin :: Compiled -> Compiled -> Compiled
max :: Compiled -> Compiled -> Compiled
$cmax :: Compiled -> Compiled -> Compiled
>= :: Compiled -> Compiled -> Bool
$c>= :: Compiled -> Compiled -> Bool
> :: Compiled -> Compiled -> Bool
$c> :: Compiled -> Compiled -> Bool
<= :: Compiled -> Compiled -> Bool
$c<= :: Compiled -> Compiled -> Bool
< :: Compiled -> Compiled -> Bool
$c< :: Compiled -> Compiled -> Bool
compare :: Compiled -> Compiled -> Ordering
$ccompare :: Compiled -> Compiled -> Ordering
$cp1Ord :: Eq Compiled
Ord)

-- | The treeless compiler can behave differently depending on the target
--   language evaluation strategy. For instance, more aggressive erasure for
--   lazy targets.
data EvaluationStrategy = LazyEvaluation | EagerEvaluation
  deriving (EvaluationStrategy -> EvaluationStrategy -> Bool
(EvaluationStrategy -> EvaluationStrategy -> Bool)
-> (EvaluationStrategy -> EvaluationStrategy -> Bool)
-> Eq EvaluationStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EvaluationStrategy -> EvaluationStrategy -> Bool
$c/= :: EvaluationStrategy -> EvaluationStrategy -> Bool
== :: EvaluationStrategy -> EvaluationStrategy -> Bool
$c== :: EvaluationStrategy -> EvaluationStrategy -> Bool
Eq, Int -> EvaluationStrategy -> ShowS
[EvaluationStrategy] -> ShowS
EvaluationStrategy -> String
(Int -> EvaluationStrategy -> ShowS)
-> (EvaluationStrategy -> String)
-> ([EvaluationStrategy] -> ShowS)
-> Show EvaluationStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EvaluationStrategy] -> ShowS
$cshowList :: [EvaluationStrategy] -> ShowS
show :: EvaluationStrategy -> String
$cshow :: EvaluationStrategy -> String
showsPrec :: Int -> EvaluationStrategy -> ShowS
$cshowsPrec :: Int -> EvaluationStrategy -> ShowS
Show)

type Args = [TTerm]

-- this currently assumes that TApp is translated in a lazy/cbn fashion.
-- The AST should also support strict translation.
--
-- All local variables are using de Bruijn indices.
data TTerm = TVar Int
           | TPrim TPrim
           | TDef QName
           | TApp TTerm Args
           | TLam TTerm
           | TLit Literal
           | TCon QName
           | TLet TTerm TTerm
           -- ^ introduces a new local binding. The bound term
           -- MUST only be evaluated if it is used inside the body.
           -- Sharing may happen, but is optional.
           -- It is also perfectly valid to just inline the bound term in the body.
           | TCase Int CaseInfo TTerm [TAlt]
           -- ^ Case scrutinee (always variable), case type, default value, alternatives
           -- First, all TACon alternatives are tried; then all TAGuard alternatives
           -- in top to bottom order.
           -- TACon alternatives must not overlap.
           | TUnit -- used for levels right now
           | TSort
           | TErased
           | TCoerce TTerm  -- ^ Used by the GHC backend
           | TError TError
           -- ^ A runtime error, something bad has happened.
  deriving (Typeable TTerm
DataType
Constr
Typeable TTerm
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TTerm -> c TTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TTerm)
-> (TTerm -> Constr)
-> (TTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm))
-> ((forall b. Data b => b -> b) -> TTerm -> TTerm)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> TTerm -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TTerm -> m TTerm)
-> Data TTerm
TTerm -> DataType
TTerm -> Constr
(forall b. Data b => b -> b) -> TTerm -> TTerm
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TTerm -> c TTerm
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TTerm
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u
forall u. (forall d. Data d => d -> u) -> TTerm -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TTerm -> m TTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TTerm -> m TTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TTerm -> c TTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm)
$cTError :: Constr
$cTCoerce :: Constr
$cTErased :: Constr
$cTSort :: Constr
$cTUnit :: Constr
$cTCase :: Constr
$cTLet :: Constr
$cTCon :: Constr
$cTLit :: Constr
$cTLam :: Constr
$cTApp :: Constr
$cTDef :: Constr
$cTPrim :: Constr
$cTVar :: Constr
$tTTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TTerm -> m TTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TTerm -> m TTerm
gmapMp :: (forall d. Data d => d -> m d) -> TTerm -> m TTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TTerm -> m TTerm
gmapM :: (forall d. Data d => d -> m d) -> TTerm -> m TTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TTerm -> m TTerm
gmapQi :: Int -> (forall d. Data d => d -> u) -> TTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TTerm -> u
gmapQ :: (forall d. Data d => d -> u) -> TTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TTerm -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r
gmapT :: (forall b. Data b => b -> b) -> TTerm -> TTerm
$cgmapT :: (forall b. Data b => b -> b) -> TTerm -> TTerm
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TTerm)
dataTypeOf :: TTerm -> DataType
$cdataTypeOf :: TTerm -> DataType
toConstr :: TTerm -> Constr
$ctoConstr :: TTerm -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TTerm
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TTerm -> c TTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TTerm -> c TTerm
$cp1Data :: Typeable TTerm
Data, Int -> TTerm -> ShowS
[TTerm] -> ShowS
TTerm -> String
(Int -> TTerm -> ShowS)
-> (TTerm -> String) -> ([TTerm] -> ShowS) -> Show TTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TTerm] -> ShowS
$cshowList :: [TTerm] -> ShowS
show :: TTerm -> String
$cshow :: TTerm -> String
showsPrec :: Int -> TTerm -> ShowS
$cshowsPrec :: Int -> TTerm -> ShowS
Show, TTerm -> TTerm -> Bool
(TTerm -> TTerm -> Bool) -> (TTerm -> TTerm -> Bool) -> Eq TTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TTerm -> TTerm -> Bool
$c/= :: TTerm -> TTerm -> Bool
== :: TTerm -> TTerm -> Bool
$c== :: TTerm -> TTerm -> Bool
Eq, Eq TTerm
Eq TTerm
-> (TTerm -> TTerm -> Ordering)
-> (TTerm -> TTerm -> Bool)
-> (TTerm -> TTerm -> Bool)
-> (TTerm -> TTerm -> Bool)
-> (TTerm -> TTerm -> Bool)
-> (TTerm -> TTerm -> TTerm)
-> (TTerm -> TTerm -> TTerm)
-> Ord TTerm
TTerm -> TTerm -> Bool
TTerm -> TTerm -> Ordering
TTerm -> TTerm -> TTerm
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TTerm -> TTerm -> TTerm
$cmin :: TTerm -> TTerm -> TTerm
max :: TTerm -> TTerm -> TTerm
$cmax :: TTerm -> TTerm -> TTerm
>= :: TTerm -> TTerm -> Bool
$c>= :: TTerm -> TTerm -> Bool
> :: TTerm -> TTerm -> Bool
$c> :: TTerm -> TTerm -> Bool
<= :: TTerm -> TTerm -> Bool
$c<= :: TTerm -> TTerm -> Bool
< :: TTerm -> TTerm -> Bool
$c< :: TTerm -> TTerm -> Bool
compare :: TTerm -> TTerm -> Ordering
$ccompare :: TTerm -> TTerm -> Ordering
$cp1Ord :: Eq TTerm
Ord)

-- | Compiler-related primitives. This are NOT the same thing as primitives
-- in Agda's surface or internal syntax!
-- Some of the primitives have a suffix indicating which type of arguments they take,
-- using the following naming convention:
-- Char | Type
-- C    | Character
-- F    | Float
-- I    | Integer
-- Q    | QName
-- S    | String
data TPrim
  = PAdd | PAdd64
  | PSub | PSub64
  | PMul | PMul64
  | PQuot | PQuot64
  | PRem  | PRem64
  | PGeq
  | PLt   | PLt64
  | PEqI  | PEq64
  | PEqF
  | PEqS
  | PEqC
  | PEqQ
  | PIf
  | PSeq
  | PITo64 | P64ToI
  deriving (Typeable TPrim
DataType
Constr
Typeable TPrim
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TPrim -> c TPrim)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TPrim)
-> (TPrim -> Constr)
-> (TPrim -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TPrim))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim))
-> ((forall b. Data b => b -> b) -> TPrim -> TPrim)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r)
-> (forall u. (forall d. Data d => d -> u) -> TPrim -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TPrim -> m TPrim)
-> Data TPrim
TPrim -> DataType
TPrim -> Constr
(forall b. Data b => b -> b) -> TPrim -> TPrim
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TPrim -> c TPrim
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TPrim
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u
forall u. (forall d. Data d => d -> u) -> TPrim -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TPrim -> m TPrim
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TPrim -> m TPrim
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TPrim
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TPrim -> c TPrim
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TPrim)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim)
$cP64ToI :: Constr
$cPITo64 :: Constr
$cPSeq :: Constr
$cPIf :: Constr
$cPEqQ :: Constr
$cPEqC :: Constr
$cPEqS :: Constr
$cPEqF :: Constr
$cPEq64 :: Constr
$cPEqI :: Constr
$cPLt64 :: Constr
$cPLt :: Constr
$cPGeq :: Constr
$cPRem64 :: Constr
$cPRem :: Constr
$cPQuot64 :: Constr
$cPQuot :: Constr
$cPMul64 :: Constr
$cPMul :: Constr
$cPSub64 :: Constr
$cPSub :: Constr
$cPAdd64 :: Constr
$cPAdd :: Constr
$tTPrim :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TPrim -> m TPrim
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TPrim -> m TPrim
gmapMp :: (forall d. Data d => d -> m d) -> TPrim -> m TPrim
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TPrim -> m TPrim
gmapM :: (forall d. Data d => d -> m d) -> TPrim -> m TPrim
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TPrim -> m TPrim
gmapQi :: Int -> (forall d. Data d => d -> u) -> TPrim -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TPrim -> u
gmapQ :: (forall d. Data d => d -> u) -> TPrim -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TPrim -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r
gmapT :: (forall b. Data b => b -> b) -> TPrim -> TPrim
$cgmapT :: (forall b. Data b => b -> b) -> TPrim -> TPrim
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TPrim)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TPrim)
dataTypeOf :: TPrim -> DataType
$cdataTypeOf :: TPrim -> DataType
toConstr :: TPrim -> Constr
$ctoConstr :: TPrim -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TPrim
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TPrim
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TPrim -> c TPrim
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TPrim -> c TPrim
$cp1Data :: Typeable TPrim
Data, Int -> TPrim -> ShowS
[TPrim] -> ShowS
TPrim -> String
(Int -> TPrim -> ShowS)
-> (TPrim -> String) -> ([TPrim] -> ShowS) -> Show TPrim
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TPrim] -> ShowS
$cshowList :: [TPrim] -> ShowS
show :: TPrim -> String
$cshow :: TPrim -> String
showsPrec :: Int -> TPrim -> ShowS
$cshowsPrec :: Int -> TPrim -> ShowS
Show, TPrim -> TPrim -> Bool
(TPrim -> TPrim -> Bool) -> (TPrim -> TPrim -> Bool) -> Eq TPrim
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TPrim -> TPrim -> Bool
$c/= :: TPrim -> TPrim -> Bool
== :: TPrim -> TPrim -> Bool
$c== :: TPrim -> TPrim -> Bool
Eq, Eq TPrim
Eq TPrim
-> (TPrim -> TPrim -> Ordering)
-> (TPrim -> TPrim -> Bool)
-> (TPrim -> TPrim -> Bool)
-> (TPrim -> TPrim -> Bool)
-> (TPrim -> TPrim -> Bool)
-> (TPrim -> TPrim -> TPrim)
-> (TPrim -> TPrim -> TPrim)
-> Ord TPrim
TPrim -> TPrim -> Bool
TPrim -> TPrim -> Ordering
TPrim -> TPrim -> TPrim
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TPrim -> TPrim -> TPrim
$cmin :: TPrim -> TPrim -> TPrim
max :: TPrim -> TPrim -> TPrim
$cmax :: TPrim -> TPrim -> TPrim
>= :: TPrim -> TPrim -> Bool
$c>= :: TPrim -> TPrim -> Bool
> :: TPrim -> TPrim -> Bool
$c> :: TPrim -> TPrim -> Bool
<= :: TPrim -> TPrim -> Bool
$c<= :: TPrim -> TPrim -> Bool
< :: TPrim -> TPrim -> Bool
$c< :: TPrim -> TPrim -> Bool
compare :: TPrim -> TPrim -> Ordering
$ccompare :: TPrim -> TPrim -> Ordering
$cp1Ord :: Eq TPrim
Ord)

isPrimEq :: TPrim -> Bool
isPrimEq :: TPrim -> Bool
isPrimEq TPrim
p = TPrim
p TPrim -> [TPrim] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PEqI, TPrim
PEqF, TPrim
PEqS, TPrim
PEqC, TPrim
PEqQ, TPrim
PEq64]

-- | Strip leading coercions and indicate whether there were some.
coerceView :: TTerm -> (Bool, TTerm)
coerceView :: TTerm -> (Bool, TTerm)
coerceView = \case
  TCoerce TTerm
t -> (Bool
True,) (TTerm -> (Bool, TTerm)) -> TTerm -> (Bool, TTerm)
forall a b. (a -> b) -> a -> b
$ (Bool, TTerm) -> TTerm
forall a b. (a, b) -> b
snd ((Bool, TTerm) -> TTerm) -> (Bool, TTerm) -> TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> (Bool, TTerm)
coerceView TTerm
t
  TTerm
t         -> (Bool
False, TTerm
t)

mkTApp :: TTerm -> Args -> TTerm
mkTApp :: TTerm -> [TTerm] -> TTerm
mkTApp TTerm
x           [] = TTerm
x
mkTApp (TApp TTerm
x [TTerm]
as) [TTerm]
bs = TTerm -> [TTerm] -> TTerm
TApp TTerm
x ([TTerm]
as [TTerm] -> [TTerm] -> [TTerm]
forall a. [a] -> [a] -> [a]
++ [TTerm]
bs)
mkTApp TTerm
x           [TTerm]
as = TTerm -> [TTerm] -> TTerm
TApp TTerm
x [TTerm]
as

tAppView :: TTerm -> (TTerm, [TTerm])
tAppView :: TTerm -> (TTerm, [TTerm])
tAppView = \case
  TApp TTerm
a [TTerm]
bs -> ([TTerm] -> [TTerm]) -> (TTerm, [TTerm]) -> (TTerm, [TTerm])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([TTerm] -> [TTerm] -> [TTerm]
forall a. [a] -> [a] -> [a]
++ [TTerm]
bs) ((TTerm, [TTerm]) -> (TTerm, [TTerm]))
-> (TTerm, [TTerm]) -> (TTerm, [TTerm])
forall a b. (a -> b) -> a -> b
$ TTerm -> (TTerm, [TTerm])
tAppView TTerm
a
  TTerm
t         -> (TTerm
t, [])

-- | Expose the format @coerce f args@.
--
--   We fuse coercions, even if interleaving with applications.
--   We assume that coercion is powerful enough to satisfy
--   @
--      coerce (coerce f a) b = coerce f a b
--   @
coerceAppView :: TTerm -> ((Bool, TTerm), [TTerm])
coerceAppView :: TTerm -> ((Bool, TTerm), [TTerm])
coerceAppView = \case
  TCoerce TTerm
t -> ((Bool, TTerm) -> (Bool, TTerm))
-> ((Bool, TTerm), [TTerm]) -> ((Bool, TTerm), [TTerm])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Bool
True,) (TTerm -> (Bool, TTerm))
-> ((Bool, TTerm) -> TTerm) -> (Bool, TTerm) -> (Bool, TTerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, TTerm) -> TTerm
forall a b. (a, b) -> b
snd) (((Bool, TTerm), [TTerm]) -> ((Bool, TTerm), [TTerm]))
-> ((Bool, TTerm), [TTerm]) -> ((Bool, TTerm), [TTerm])
forall a b. (a -> b) -> a -> b
$ TTerm -> ((Bool, TTerm), [TTerm])
coerceAppView TTerm
t
  TApp TTerm
a [TTerm]
bs -> ([TTerm] -> [TTerm])
-> ((Bool, TTerm), [TTerm]) -> ((Bool, TTerm), [TTerm])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([TTerm] -> [TTerm] -> [TTerm]
forall a. [a] -> [a] -> [a]
++ [TTerm]
bs) (((Bool, TTerm), [TTerm]) -> ((Bool, TTerm), [TTerm]))
-> ((Bool, TTerm), [TTerm]) -> ((Bool, TTerm), [TTerm])
forall a b. (a -> b) -> a -> b
$ TTerm -> ((Bool, TTerm), [TTerm])
coerceAppView TTerm
a
  TTerm
t         -> ((Bool
False, TTerm
t), [])

tLetView :: TTerm -> ([TTerm], TTerm)
tLetView :: TTerm -> ([TTerm], TTerm)
tLetView (TLet TTerm
e TTerm
b) = ([TTerm] -> [TTerm]) -> ([TTerm], TTerm) -> ([TTerm], TTerm)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TTerm
e TTerm -> [TTerm] -> [TTerm]
forall a. a -> [a] -> [a]
:) (([TTerm], TTerm) -> ([TTerm], TTerm))
-> ([TTerm], TTerm) -> ([TTerm], TTerm)
forall a b. (a -> b) -> a -> b
$ TTerm -> ([TTerm], TTerm)
tLetView TTerm
b
tLetView TTerm
e          = ([], TTerm
e)

tLamView :: TTerm -> (Int, TTerm)
tLamView :: TTerm -> (Int, TTerm)
tLamView = Int -> TTerm -> (Int, TTerm)
forall a. Num a => a -> TTerm -> (a, TTerm)
go Int
0
  where go :: a -> TTerm -> (a, TTerm)
go a
n (TLam TTerm
b) = a -> TTerm -> (a, TTerm)
go (a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) TTerm
b
        go a
n TTerm
t        = (a
n, TTerm
t)

mkTLam :: Int -> TTerm -> TTerm
mkTLam :: Int -> TTerm -> TTerm
mkTLam Int
n TTerm
b = ((TTerm -> TTerm) -> TTerm -> TTerm)
-> TTerm -> [TTerm -> TTerm] -> TTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
($) TTerm
b ([TTerm -> TTerm] -> TTerm) -> [TTerm -> TTerm] -> TTerm
forall a b. (a -> b) -> a -> b
$ Int -> (TTerm -> TTerm) -> [TTerm -> TTerm]
forall a. Int -> a -> [a]
replicate Int
n TTerm -> TTerm
TLam

-- | Introduces a new binding
mkLet :: TTerm -> TTerm -> TTerm
mkLet :: TTerm -> TTerm -> TTerm
mkLet TTerm
x TTerm
body = TTerm -> TTerm -> TTerm
TLet TTerm
x TTerm
body

tInt :: Integer -> TTerm
tInt :: Integer -> TTerm
tInt = Literal -> TTerm
TLit (Literal -> TTerm) -> (Integer -> Literal) -> Integer -> TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Integer -> Literal
LitNat Range
forall a. Range' a
noRange

intView :: TTerm -> Maybe Integer
intView :: TTerm -> Maybe Integer
intView (TLit (LitNat Range
_ Integer
x)) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
x
intView TTerm
_ = Maybe Integer
forall a. Maybe a
Nothing

word64View :: TTerm -> Maybe Word64
word64View :: TTerm -> Maybe Word64
word64View (TLit (LitWord64 Range
_ Word64
x)) = Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
x
word64View TTerm
_ = Maybe Word64
forall a. Maybe a
Nothing

tPlusK :: Integer -> TTerm -> TTerm
tPlusK :: Integer -> TTerm -> TTerm
tPlusK Integer
0 TTerm
n = TTerm
n
tPlusK Integer
k TTerm
n | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub TTerm
n (Integer -> TTerm
tInt (-Integer
k))
tPlusK Integer
k TTerm
n = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PAdd (Integer -> TTerm
tInt Integer
k) TTerm
n

-- -(k + n)
tNegPlusK :: Integer -> TTerm -> TTerm
tNegPlusK :: Integer -> TTerm -> TTerm
tNegPlusK Integer
k TTerm
n = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub (Integer -> TTerm
tInt (-Integer
k)) TTerm
n

plusKView :: TTerm -> Maybe (Integer, TTerm)
plusKView :: TTerm -> Maybe (Integer, TTerm)
plusKView (TApp (TPrim TPrim
PAdd) [TTerm
k, TTerm
n]) | Just Integer
k <- TTerm -> Maybe Integer
intView TTerm
k = (Integer, TTerm) -> Maybe (Integer, TTerm)
forall a. a -> Maybe a
Just (Integer
k, TTerm
n)
plusKView (TApp (TPrim TPrim
PSub) [TTerm
n, TTerm
k]) | Just Integer
k <- TTerm -> Maybe Integer
intView TTerm
k = (Integer, TTerm) -> Maybe (Integer, TTerm)
forall a. a -> Maybe a
Just (-Integer
k, TTerm
n)
plusKView TTerm
_ = Maybe (Integer, TTerm)
forall a. Maybe a
Nothing

negPlusKView :: TTerm -> Maybe (Integer, TTerm)
negPlusKView :: TTerm -> Maybe (Integer, TTerm)
negPlusKView (TApp (TPrim TPrim
PSub) [TTerm
k, TTerm
n]) | Just Integer
k <- TTerm -> Maybe Integer
intView TTerm
k = (Integer, TTerm) -> Maybe (Integer, TTerm)
forall a. a -> Maybe a
Just (-Integer
k, TTerm
n)
negPlusKView TTerm
_ = Maybe (Integer, TTerm)
forall a. Maybe a
Nothing

tOp :: TPrim -> TTerm -> TTerm -> TTerm
tOp :: TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
op TTerm
a TTerm
b = TPrim -> TTerm -> TTerm -> TTerm
TPOp TPrim
op TTerm
a TTerm
b

pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm
pattern $bTPOp :: TPrim -> TTerm -> TTerm -> TTerm
$mTPOp :: forall r.
TTerm -> (TPrim -> TTerm -> TTerm -> r) -> (Void# -> r) -> r
TPOp op a b = TApp (TPrim op) [a, b]

pattern TPFn :: TPrim -> TTerm -> TTerm
pattern $bTPFn :: TPrim -> TTerm -> TTerm
$mTPFn :: forall r. TTerm -> (TPrim -> TTerm -> r) -> (Void# -> r) -> r
TPFn op a = TApp (TPrim op) [a]

tUnreachable :: TTerm
tUnreachable :: TTerm
tUnreachable = TError -> TTerm
TError TError
TUnreachable

tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm
tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm
tIfThenElse TTerm
c TTerm
i TTerm
e = TTerm -> [TTerm] -> TTerm
TApp (TPrim -> TTerm
TPrim TPrim
PIf) [TTerm
c, TTerm
i, TTerm
e]

data CaseType
  = CTData QName -- case on datatype
  | CTNat
  | CTInt
  | CTChar
  | CTString
  | CTFloat
  | CTQName
  deriving (Typeable CaseType
DataType
Constr
Typeable CaseType
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseType -> c CaseType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseType)
-> (CaseType -> Constr)
-> (CaseType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType))
-> ((forall b. Data b => b -> b) -> CaseType -> CaseType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseType -> r)
-> (forall u. (forall d. Data d => d -> u) -> CaseType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseType -> m CaseType)
-> Data CaseType
CaseType -> DataType
CaseType -> Constr
(forall b. Data b => b -> b) -> CaseType -> CaseType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseType -> c CaseType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseType
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u
forall u. (forall d. Data d => d -> u) -> CaseType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CaseType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CaseType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CaseType -> m CaseType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CaseType -> m CaseType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseType -> c CaseType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CaseType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)
$cCTQName :: Constr
$cCTFloat :: Constr
$cCTString :: Constr
$cCTChar :: Constr
$cCTInt :: Constr
$cCTNat :: Constr
$cCTData :: Constr
$tCaseType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CaseType -> m CaseType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CaseType -> m CaseType
gmapMp :: (forall d. Data d => d -> m d) -> CaseType -> m CaseType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CaseType -> m CaseType
gmapM :: (forall d. Data d => d -> m d) -> CaseType -> m CaseType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CaseType -> m CaseType
gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CaseType -> u
gmapQ :: (forall d. Data d => d -> u) -> CaseType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CaseType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CaseType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CaseType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CaseType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CaseType -> r
gmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType
$cgmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CaseType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CaseType)
dataTypeOf :: CaseType -> DataType
$cdataTypeOf :: CaseType -> DataType
toConstr :: CaseType -> Constr
$ctoConstr :: CaseType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseType -> c CaseType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseType -> c CaseType
$cp1Data :: Typeable CaseType
Data, Int -> CaseType -> ShowS
[CaseType] -> ShowS
CaseType -> String
(Int -> CaseType -> ShowS)
-> (CaseType -> String) -> ([CaseType] -> ShowS) -> Show CaseType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CaseType] -> ShowS
$cshowList :: [CaseType] -> ShowS
show :: CaseType -> String
$cshow :: CaseType -> String
showsPrec :: Int -> CaseType -> ShowS
$cshowsPrec :: Int -> CaseType -> ShowS
Show, CaseType -> CaseType -> Bool
(CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool) -> Eq CaseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CaseType -> CaseType -> Bool
$c/= :: CaseType -> CaseType -> Bool
== :: CaseType -> CaseType -> Bool
$c== :: CaseType -> CaseType -> Bool
Eq, Eq CaseType
Eq CaseType
-> (CaseType -> CaseType -> Ordering)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> CaseType)
-> (CaseType -> CaseType -> CaseType)
-> Ord CaseType
CaseType -> CaseType -> Bool
CaseType -> CaseType -> Ordering
CaseType -> CaseType -> CaseType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CaseType -> CaseType -> CaseType
$cmin :: CaseType -> CaseType -> CaseType
max :: CaseType -> CaseType -> CaseType
$cmax :: CaseType -> CaseType -> CaseType
>= :: CaseType -> CaseType -> Bool
$c>= :: CaseType -> CaseType -> Bool
> :: CaseType -> CaseType -> Bool
$c> :: CaseType -> CaseType -> Bool
<= :: CaseType -> CaseType -> Bool
$c<= :: CaseType -> CaseType -> Bool
< :: CaseType -> CaseType -> Bool
$c< :: CaseType -> CaseType -> Bool
compare :: CaseType -> CaseType -> Ordering
$ccompare :: CaseType -> CaseType -> Ordering
$cp1Ord :: Eq CaseType
Ord)

data CaseInfo = CaseInfo
  { CaseInfo -> Bool
caseLazy :: Bool
  , CaseInfo -> CaseType
caseType :: CaseType }
  deriving (Typeable CaseInfo
DataType
Constr
Typeable CaseInfo
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CaseInfo -> c CaseInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CaseInfo)
-> (CaseInfo -> Constr)
-> (CaseInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CaseInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo))
-> ((forall b. Data b => b -> b) -> CaseInfo -> CaseInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo)
-> Data CaseInfo
CaseInfo -> DataType
CaseInfo -> Constr
(forall b. Data b => b -> b) -> CaseInfo -> CaseInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u
forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CaseInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo)
$cCaseInfo :: Constr
$tCaseInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
gmapMp :: (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
gmapM :: (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CaseInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> CaseInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CaseInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CaseInfo -> r
gmapT :: (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo
$cgmapT :: (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CaseInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CaseInfo)
dataTypeOf :: CaseInfo -> DataType
$cdataTypeOf :: CaseInfo -> DataType
toConstr :: CaseInfo -> Constr
$ctoConstr :: CaseInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CaseInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CaseInfo -> c CaseInfo
$cp1Data :: Typeable CaseInfo
Data, Int -> CaseInfo -> ShowS
[CaseInfo] -> ShowS
CaseInfo -> String
(Int -> CaseInfo -> ShowS)
-> (CaseInfo -> String) -> ([CaseInfo] -> ShowS) -> Show CaseInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CaseInfo] -> ShowS
$cshowList :: [CaseInfo] -> ShowS
show :: CaseInfo -> String
$cshow :: CaseInfo -> String
showsPrec :: Int -> CaseInfo -> ShowS
$cshowsPrec :: Int -> CaseInfo -> ShowS
Show, CaseInfo -> CaseInfo -> Bool
(CaseInfo -> CaseInfo -> Bool)
-> (CaseInfo -> CaseInfo -> Bool) -> Eq CaseInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CaseInfo -> CaseInfo -> Bool
$c/= :: CaseInfo -> CaseInfo -> Bool
== :: CaseInfo -> CaseInfo -> Bool
$c== :: CaseInfo -> CaseInfo -> Bool
Eq, Eq CaseInfo
Eq CaseInfo
-> (CaseInfo -> CaseInfo -> Ordering)
-> (CaseInfo -> CaseInfo -> Bool)
-> (CaseInfo -> CaseInfo -> Bool)
-> (CaseInfo -> CaseInfo -> Bool)
-> (CaseInfo -> CaseInfo -> Bool)
-> (CaseInfo -> CaseInfo -> CaseInfo)
-> (CaseInfo -> CaseInfo -> CaseInfo)
-> Ord CaseInfo
CaseInfo -> CaseInfo -> Bool
CaseInfo -> CaseInfo -> Ordering
CaseInfo -> CaseInfo -> CaseInfo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CaseInfo -> CaseInfo -> CaseInfo
$cmin :: CaseInfo -> CaseInfo -> CaseInfo
max :: CaseInfo -> CaseInfo -> CaseInfo
$cmax :: CaseInfo -> CaseInfo -> CaseInfo
>= :: CaseInfo -> CaseInfo -> Bool
$c>= :: CaseInfo -> CaseInfo -> Bool
> :: CaseInfo -> CaseInfo -> Bool
$c> :: CaseInfo -> CaseInfo -> Bool
<= :: CaseInfo -> CaseInfo -> Bool
$c<= :: CaseInfo -> CaseInfo -> Bool
< :: CaseInfo -> CaseInfo -> Bool
$c< :: CaseInfo -> CaseInfo -> Bool
compare :: CaseInfo -> CaseInfo -> Ordering
$ccompare :: CaseInfo -> CaseInfo -> Ordering
$cp1Ord :: Eq CaseInfo
Ord)

data TAlt
  = TACon    { TAlt -> QName
aCon  :: QName, TAlt -> Int
aArity :: Int, TAlt -> TTerm
aBody :: TTerm }
  -- ^ Matches on the given constructor. If the match succeeds,
  -- the pattern variables are prepended to the current environment
  -- (pushes all existing variables aArity steps further away)
  | TAGuard  { TAlt -> TTerm
aGuard :: TTerm, aBody :: TTerm }
  -- ^ Binds no variables
  | TALit    { TAlt -> Literal
aLit :: Literal,   aBody:: TTerm }
  deriving (Typeable TAlt
DataType
Constr
Typeable TAlt
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TAlt -> c TAlt)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TAlt)
-> (TAlt -> Constr)
-> (TAlt -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TAlt))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt))
-> ((forall b. Data b => b -> b) -> TAlt -> TAlt)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r)
-> (forall u. (forall d. Data d => d -> u) -> TAlt -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TAlt -> m TAlt)
-> Data TAlt
TAlt -> DataType
TAlt -> Constr
(forall b. Data b => b -> b) -> TAlt -> TAlt
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TAlt -> c TAlt
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TAlt
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u
forall u. (forall d. Data d => d -> u) -> TAlt -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TAlt -> m TAlt
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TAlt -> m TAlt
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TAlt
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TAlt -> c TAlt
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TAlt)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt)
$cTALit :: Constr
$cTAGuard :: Constr
$cTACon :: Constr
$tTAlt :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TAlt -> m TAlt
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TAlt -> m TAlt
gmapMp :: (forall d. Data d => d -> m d) -> TAlt -> m TAlt
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TAlt -> m TAlt
gmapM :: (forall d. Data d => d -> m d) -> TAlt -> m TAlt
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TAlt -> m TAlt
gmapQi :: Int -> (forall d. Data d => d -> u) -> TAlt -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TAlt -> u
gmapQ :: (forall d. Data d => d -> u) -> TAlt -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TAlt -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r
gmapT :: (forall b. Data b => b -> b) -> TAlt -> TAlt
$cgmapT :: (forall b. Data b => b -> b) -> TAlt -> TAlt
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TAlt)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TAlt)
dataTypeOf :: TAlt -> DataType
$cdataTypeOf :: TAlt -> DataType
toConstr :: TAlt -> Constr
$ctoConstr :: TAlt -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TAlt
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TAlt
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TAlt -> c TAlt
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TAlt -> c TAlt
$cp1Data :: Typeable TAlt
Data, Int -> TAlt -> ShowS
[TAlt] -> ShowS
TAlt -> String
(Int -> TAlt -> ShowS)
-> (TAlt -> String) -> ([TAlt] -> ShowS) -> Show TAlt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TAlt] -> ShowS
$cshowList :: [TAlt] -> ShowS
show :: TAlt -> String
$cshow :: TAlt -> String
showsPrec :: Int -> TAlt -> ShowS
$cshowsPrec :: Int -> TAlt -> ShowS
Show, TAlt -> TAlt -> Bool
(TAlt -> TAlt -> Bool) -> (TAlt -> TAlt -> Bool) -> Eq TAlt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TAlt -> TAlt -> Bool
$c/= :: TAlt -> TAlt -> Bool
== :: TAlt -> TAlt -> Bool
$c== :: TAlt -> TAlt -> Bool
Eq, Eq TAlt
Eq TAlt
-> (TAlt -> TAlt -> Ordering)
-> (TAlt -> TAlt -> Bool)
-> (TAlt -> TAlt -> Bool)
-> (TAlt -> TAlt -> Bool)
-> (TAlt -> TAlt -> Bool)
-> (TAlt -> TAlt -> TAlt)
-> (TAlt -> TAlt -> TAlt)
-> Ord TAlt
TAlt -> TAlt -> Bool
TAlt -> TAlt -> Ordering
TAlt -> TAlt -> TAlt
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TAlt -> TAlt -> TAlt
$cmin :: TAlt -> TAlt -> TAlt
max :: TAlt -> TAlt -> TAlt
$cmax :: TAlt -> TAlt -> TAlt
>= :: TAlt -> TAlt -> Bool
$c>= :: TAlt -> TAlt -> Bool
> :: TAlt -> TAlt -> Bool
$c> :: TAlt -> TAlt -> Bool
<= :: TAlt -> TAlt -> Bool
$c<= :: TAlt -> TAlt -> Bool
< :: TAlt -> TAlt -> Bool
$c< :: TAlt -> TAlt -> Bool
compare :: TAlt -> TAlt -> Ordering
$ccompare :: TAlt -> TAlt -> Ordering
$cp1Ord :: Eq TAlt
Ord)

data TError
  = TUnreachable
  -- ^ Code which is unreachable. E.g. absurd branches or missing case defaults.
  -- Runtime behaviour of unreachable code is undefined, but preferably
  -- the program will exit with an error message. The compiler is free
  -- to assume that this code is unreachable and to remove it.
  deriving (Typeable TError
DataType
Constr
Typeable TError
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TError -> c TError)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TError)
-> (TError -> Constr)
-> (TError -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TError))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError))
-> ((forall b. Data b => b -> b) -> TError -> TError)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TError -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TError -> r)
-> (forall u. (forall d. Data d => d -> u) -> TError -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TError -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TError -> m TError)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TError -> m TError)
-> Data TError
TError -> DataType
TError -> Constr
(forall b. Data b => b -> b) -> TError -> TError
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TError -> c TError
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TError
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TError -> u
forall u. (forall d. Data d => d -> u) -> TError -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TError -> m TError
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TError -> m TError
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TError
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TError -> c TError
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TError)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError)
$cTUnreachable :: Constr
$tTError :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TError -> m TError
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TError -> m TError
gmapMp :: (forall d. Data d => d -> m d) -> TError -> m TError
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TError -> m TError
gmapM :: (forall d. Data d => d -> m d) -> TError -> m TError
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TError -> m TError
gmapQi :: Int -> (forall d. Data d => d -> u) -> TError -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TError -> u
gmapQ :: (forall d. Data d => d -> u) -> TError -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TError -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r
gmapT :: (forall b. Data b => b -> b) -> TError -> TError
$cgmapT :: (forall b. Data b => b -> b) -> TError -> TError
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TError)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TError)
dataTypeOf :: TError -> DataType
$cdataTypeOf :: TError -> DataType
toConstr :: TError -> Constr
$ctoConstr :: TError -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TError
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TError
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TError -> c TError
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TError -> c TError
$cp1Data :: Typeable TError
Data, Int -> TError -> ShowS
[TError] -> ShowS
TError -> String
(Int -> TError -> ShowS)
-> (TError -> String) -> ([TError] -> ShowS) -> Show TError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TError] -> ShowS
$cshowList :: [TError] -> ShowS
show :: TError -> String
$cshow :: TError -> String
showsPrec :: Int -> TError -> ShowS
$cshowsPrec :: Int -> TError -> ShowS
Show, TError -> TError -> Bool
(TError -> TError -> Bool)
-> (TError -> TError -> Bool) -> Eq TError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TError -> TError -> Bool
$c/= :: TError -> TError -> Bool
== :: TError -> TError -> Bool
$c== :: TError -> TError -> Bool
Eq, Eq TError
Eq TError
-> (TError -> TError -> Ordering)
-> (TError -> TError -> Bool)
-> (TError -> TError -> Bool)
-> (TError -> TError -> Bool)
-> (TError -> TError -> Bool)
-> (TError -> TError -> TError)
-> (TError -> TError -> TError)
-> Ord TError
TError -> TError -> Bool
TError -> TError -> Ordering
TError -> TError -> TError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TError -> TError -> TError
$cmin :: TError -> TError -> TError
max :: TError -> TError -> TError
$cmax :: TError -> TError -> TError
>= :: TError -> TError -> Bool
$c>= :: TError -> TError -> Bool
> :: TError -> TError -> Bool
$c> :: TError -> TError -> Bool
<= :: TError -> TError -> Bool
$c<= :: TError -> TError -> Bool
< :: TError -> TError -> Bool
$c< :: TError -> TError -> Bool
compare :: TError -> TError -> Ordering
$ccompare :: TError -> TError -> Ordering
$cp1Ord :: Eq TError
Ord)


class Unreachable a where
  -- | Checks if the given expression is unreachable or not.
  isUnreachable :: a -> Bool

instance Unreachable TAlt where
  isUnreachable :: TAlt -> Bool
isUnreachable = TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable (TTerm -> Bool) -> (TAlt -> TTerm) -> TAlt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TAlt -> TTerm
aBody

instance Unreachable TTerm where
  isUnreachable :: TTerm -> Bool
isUnreachable (TError TUnreachable{}) = Bool
True
  isUnreachable (TLet TTerm
_ TTerm
b) = TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable TTerm
b
  isUnreachable TTerm
_ = Bool
False

instance KillRange Compiled where
  killRange :: Compiled -> Compiled
killRange Compiled
c = Compiled
c -- bogus, but not used anyway