{-# 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 Control.DeepSeq

import Data.Word

import GHC.Generics (Generic)

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

data Compiled = Compiled
  { Compiled -> TTerm
cTreeless :: TTerm
  , Compiled -> Maybe [ArgUsage]
cArgUsage :: Maybe [ArgUsage]
      -- ^ 'Nothing' if treeless usage analysis has not run yet.
  }
  deriving (Int -> Compiled -> ShowS
[Compiled] -> ShowS
Compiled -> String
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
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
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
Ord, forall x. Rep Compiled x -> Compiled
forall x. Compiled -> Rep Compiled x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Compiled x -> Compiled
$cfrom :: forall x. Compiled -> Rep Compiled x
Generic)

-- | Usage status of function arguments in treeless code.
data ArgUsage
  = ArgUsed
  | ArgUnused
  deriving (Int -> ArgUsage -> ShowS
[ArgUsage] -> ShowS
ArgUsage -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ArgUsage] -> ShowS
$cshowList :: [ArgUsage] -> ShowS
show :: ArgUsage -> String
$cshow :: ArgUsage -> String
showsPrec :: Int -> ArgUsage -> ShowS
$cshowsPrec :: Int -> ArgUsage -> ShowS
Show, ArgUsage -> ArgUsage -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ArgUsage -> ArgUsage -> Bool
$c/= :: ArgUsage -> ArgUsage -> Bool
== :: ArgUsage -> ArgUsage -> Bool
$c== :: ArgUsage -> ArgUsage -> Bool
Eq, Eq ArgUsage
ArgUsage -> ArgUsage -> Bool
ArgUsage -> ArgUsage -> Ordering
ArgUsage -> ArgUsage -> ArgUsage
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 :: ArgUsage -> ArgUsage -> ArgUsage
$cmin :: ArgUsage -> ArgUsage -> ArgUsage
max :: ArgUsage -> ArgUsage -> ArgUsage
$cmax :: ArgUsage -> ArgUsage -> ArgUsage
>= :: ArgUsage -> ArgUsage -> Bool
$c>= :: ArgUsage -> ArgUsage -> Bool
> :: ArgUsage -> ArgUsage -> Bool
$c> :: ArgUsage -> ArgUsage -> Bool
<= :: ArgUsage -> ArgUsage -> Bool
$c<= :: ArgUsage -> ArgUsage -> Bool
< :: ArgUsage -> ArgUsage -> Bool
$c< :: ArgUsage -> ArgUsage -> Bool
compare :: ArgUsage -> ArgUsage -> Ordering
$ccompare :: ArgUsage -> ArgUsage -> Ordering
Ord, forall x. Rep ArgUsage x -> ArgUsage
forall x. ArgUsage -> Rep ArgUsage x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ArgUsage x -> ArgUsage
$cfrom :: forall x. ArgUsage -> Rep ArgUsage x
Generic)

-- | 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
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
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 (Int -> TTerm -> ShowS
Args -> ShowS
TTerm -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: Args -> ShowS
$cshowList :: Args -> ShowS
show :: TTerm -> String
$cshow :: TTerm -> String
showsPrec :: Int -> TTerm -> ShowS
$cshowsPrec :: Int -> TTerm -> ShowS
Show, TTerm -> TTerm -> Bool
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
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
Ord, forall x. Rep TTerm x -> TTerm
forall x. TTerm -> Rep TTerm x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TTerm x -> TTerm
$cfrom :: forall x. TTerm -> Rep TTerm x
Generic)

-- | 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 (Int -> TPrim -> ShowS
[TPrim] -> ShowS
TPrim -> String
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
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
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
Ord, forall x. Rep TPrim x -> TPrim
forall x. TPrim -> Rep TPrim x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TPrim x -> TPrim
$cfrom :: forall x. TPrim -> Rep TPrim x
Generic)

isPrimEq :: TPrim -> Bool
isPrimEq :: TPrim -> Bool
isPrimEq TPrim
p = TPrim
p 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,) forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd 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 -> Args -> TTerm
mkTApp TTerm
x           [] = TTerm
x
mkTApp (TApp TTerm
x Args
as) Args
bs = TTerm -> Args -> TTerm
TApp TTerm
x (Args
as forall a. [a] -> [a] -> [a]
++ Args
bs)
mkTApp TTerm
x           Args
as = TTerm -> Args -> TTerm
TApp TTerm
x Args
as

tAppView :: TTerm -> (TTerm, [TTerm])
tAppView :: TTerm -> (TTerm, Args)
tAppView = \case
  TApp TTerm
a Args
bs -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall a. [a] -> [a] -> [a]
++ Args
bs) forall a b. (a -> b) -> a -> b
$ TTerm -> (TTerm, Args)
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), Args)
coerceAppView = \case
  TCoerce TTerm
t -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Bool
True,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ TTerm -> ((Bool, TTerm), Args)
coerceAppView TTerm
t
  TApp TTerm
a Args
bs -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall a. [a] -> [a] -> [a]
++ Args
bs) forall a b. (a -> b) -> a -> b
$ TTerm -> ((Bool, TTerm), Args)
coerceAppView TTerm
a
  TTerm
t         -> ((Bool
False, TTerm
t), [])

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

tLamView :: TTerm -> (Int, TTerm)
tLamView :: TTerm -> (Int, TTerm)
tLamView = 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 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
($) TTerm
b forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
LitNat

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

word64View :: TTerm -> Maybe Word64
word64View :: TTerm -> Maybe Word64
word64View (TLit (LitWord64 Word64
x)) = forall a. a -> Maybe a
Just Word64
x
word64View TTerm
_ = 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 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 = 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 = forall a. a -> Maybe a
Just (-Integer
k, TTerm
n)
plusKView 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 = forall a. a -> Maybe a
Just (-Integer
k, TTerm
n)
negPlusKView 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) -> ((# #) -> 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) -> ((# #) -> 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 -> Args -> TTerm
TApp (TPrim -> TTerm
TPrim TPrim
PIf) [TTerm
c, TTerm
i, TTerm
e]

data CaseType
  = CTData Quantity QName
    -- Case on datatype. The 'Quantity' is zero for matches on erased
    -- arguments.
  | CTNat
  | CTInt
  | CTChar
  | CTString
  | CTFloat
  | CTQName
  deriving (Int -> CaseType -> ShowS
[CaseType] -> ShowS
CaseType -> String
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
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
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
Ord, forall x. Rep CaseType x -> CaseType
forall x. CaseType -> Rep CaseType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CaseType x -> CaseType
$cfrom :: forall x. CaseType -> Rep CaseType x
Generic)

data CaseInfo = CaseInfo
  { CaseInfo -> Bool
caseLazy :: Bool
  , CaseInfo -> CaseType
caseType :: CaseType }
  deriving (Int -> CaseInfo -> ShowS
[CaseInfo] -> ShowS
CaseInfo -> String
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
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
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
Ord, forall x. Rep CaseInfo x -> CaseInfo
forall x. CaseInfo -> Rep CaseInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CaseInfo x -> CaseInfo
$cfrom :: forall x. CaseInfo -> Rep CaseInfo x
Generic)

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 (Int -> TAlt -> ShowS
[TAlt] -> ShowS
TAlt -> String
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
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
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
Ord, forall x. Rep TAlt x -> TAlt
forall x. TAlt -> Rep TAlt x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TAlt x -> TAlt
$cfrom :: forall x. TAlt -> Rep TAlt x
Generic)

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.
  | TMeta String
  -- ^ Code which could not be obtained because of a hole in the program.
  -- This should throw a runtime error.
  -- The string gives some information about the meta variable that got compiled.
  deriving (Int -> TError -> ShowS
[TError] -> ShowS
TError -> String
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
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
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
Ord, forall x. Rep TError x -> TError
forall x. TError -> Rep TError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TError x -> TError
$cfrom :: forall x. TError -> Rep TError x
Generic)


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

instance Unreachable TAlt where
  isUnreachable :: TAlt -> Bool
isUnreachable = forall a. Unreachable a => a -> Bool
isUnreachable 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) = 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


-- * Utilities for ArgUsage
---------------------------------------------------------------------------

-- | @filterUsed used args@ drops those @args@ which are labelled
-- @ArgUnused@ in list @used@.
--
-- Specification:
--
-- @
--   filterUsed used args = [ a | (a, ArgUsed) <- zip args $ used ++ repeat ArgUsed ]
-- @
--
-- Examples:
--
-- @
--   filterUsed []                 == id
--   filterUsed (repeat ArgUsed)   == id
--   filterUsed (repeat ArgUnused) == const []
-- @
filterUsed :: [ArgUsage] -> [a] -> [a]
filterUsed :: forall a. [ArgUsage] -> [a] -> [a]
filterUsed = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
  ([], [a]
args) -> [a]
args
  ([ArgUsage]
_ , [])   -> []
  (ArgUsage
ArgUsed   : [ArgUsage]
used, a
a : [a]
args) -> a
a forall a. a -> [a] -> [a]
: forall a. [ArgUsage] -> [a] -> [a]
filterUsed [ArgUsage]
used [a]
args
  (ArgUsage
ArgUnused : [ArgUsage]
used, a
a : [a]
args) ->     forall a. [ArgUsage] -> [a] -> [a]
filterUsed [ArgUsage]
used [a]
args

-- NFData instances
---------------------------------------------------------------------------

instance NFData Compiled
instance NFData ArgUsage
instance NFData TTerm
instance NFData TPrim
instance NFData CaseType
instance NFData CaseInfo
instance NFData TAlt
instance NFData TError