{-# OPTIONS_GHC -Wunused-imports #-}

{-# 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
(Int -> Compiled -> ShowS)
-> (Compiled -> String) -> ([Compiled] -> ShowS) -> Show Compiled
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Compiled -> ShowS
showsPrec :: Int -> Compiled -> ShowS
$cshow :: Compiled -> String
show :: Compiled -> String
$cshowList :: [Compiled] -> ShowS
showList :: [Compiled] -> ShowS
Show, Compiled -> Compiled -> Bool
(Compiled -> Compiled -> Bool)
-> (Compiled -> Compiled -> Bool) -> Eq Compiled
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Compiled -> Compiled -> Bool
== :: Compiled -> Compiled -> Bool
$c/= :: Compiled -> Compiled -> Bool
/= :: 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
$ccompare :: Compiled -> Compiled -> Ordering
compare :: Compiled -> Compiled -> Ordering
$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
>= :: Compiled -> Compiled -> Bool
$cmax :: Compiled -> Compiled -> Compiled
max :: Compiled -> Compiled -> Compiled
$cmin :: Compiled -> Compiled -> Compiled
min :: Compiled -> Compiled -> Compiled
Ord, (forall x. Compiled -> Rep Compiled x)
-> (forall x. Rep Compiled x -> Compiled) -> Generic Compiled
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
$cfrom :: forall x. Compiled -> Rep Compiled x
from :: forall x. Compiled -> Rep Compiled x
$cto :: forall x. Rep Compiled x -> Compiled
to :: forall x. Rep Compiled x -> Compiled
Generic)

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

isPrimEq :: TPrim -> Bool
isPrimEq :: TPrim -> Bool
isPrimEq TPrim
p = TPrim
p TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> 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 b c d. (b -> c) -> (d, b) -> (d, c)
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 b c d. (b -> c) -> (b, d) -> (c, d)
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 b c d. (b -> c) -> (b, d) -> (c, d)
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 a b. (a -> b -> b) -> b -> [a] -> b
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
. Integer -> Literal
LitNat

intView :: TTerm -> Maybe Integer
intView :: TTerm -> Maybe Integer
intView (TLit (LitNat 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 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 $mTPOp :: forall {r}.
TTerm -> (TPrim -> TTerm -> TTerm -> r) -> ((# #) -> r) -> r
$bTPOp :: TPrim -> TTerm -> TTerm -> TTerm
TPOp op a b = TApp (TPrim op) [a, b]

pattern TPFn :: TPrim -> TTerm -> TTerm
pattern $mTPFn :: forall {r}. TTerm -> (TPrim -> TTerm -> r) -> ((# #) -> r) -> r
$bTPFn :: TPrim -> TTerm -> TTerm
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 (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
$cshowsPrec :: Int -> CaseType -> ShowS
showsPrec :: Int -> CaseType -> ShowS
$cshow :: CaseType -> String
show :: CaseType -> String
$cshowList :: [CaseType] -> ShowS
showList :: [CaseType] -> ShowS
Show, CaseType -> CaseType -> Bool
(CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool) -> Eq CaseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CaseType -> CaseType -> Bool
== :: CaseType -> CaseType -> Bool
$c/= :: CaseType -> CaseType -> Bool
/= :: 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
$ccompare :: CaseType -> CaseType -> Ordering
compare :: CaseType -> CaseType -> Ordering
$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
>= :: CaseType -> CaseType -> Bool
$cmax :: CaseType -> CaseType -> CaseType
max :: CaseType -> CaseType -> CaseType
$cmin :: CaseType -> CaseType -> CaseType
min :: CaseType -> CaseType -> CaseType
Ord, (forall x. CaseType -> Rep CaseType x)
-> (forall x. Rep CaseType x -> CaseType) -> Generic CaseType
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
$cfrom :: forall x. CaseType -> Rep CaseType x
from :: forall x. CaseType -> Rep CaseType x
$cto :: forall x. Rep CaseType x -> CaseType
to :: forall x. Rep CaseType x -> CaseType
Generic)

data CaseInfo = CaseInfo
  { CaseInfo -> Bool
caseLazy :: Bool
  , CaseInfo -> Erased
caseErased :: Erased
    -- ^ Is this a match on an erased argument?
  , CaseInfo -> CaseType
caseType :: CaseType }
  deriving (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
$cshowsPrec :: Int -> CaseInfo -> ShowS
showsPrec :: Int -> CaseInfo -> ShowS
$cshow :: CaseInfo -> String
show :: CaseInfo -> String
$cshowList :: [CaseInfo] -> ShowS
showList :: [CaseInfo] -> ShowS
Show, CaseInfo -> CaseInfo -> Bool
(CaseInfo -> CaseInfo -> Bool)
-> (CaseInfo -> CaseInfo -> Bool) -> Eq CaseInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CaseInfo -> CaseInfo -> Bool
== :: CaseInfo -> CaseInfo -> Bool
$c/= :: CaseInfo -> CaseInfo -> Bool
/= :: 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
$ccompare :: CaseInfo -> CaseInfo -> Ordering
compare :: CaseInfo -> CaseInfo -> Ordering
$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
>= :: CaseInfo -> CaseInfo -> Bool
$cmax :: CaseInfo -> CaseInfo -> CaseInfo
max :: CaseInfo -> CaseInfo -> CaseInfo
$cmin :: CaseInfo -> CaseInfo -> CaseInfo
min :: CaseInfo -> CaseInfo -> CaseInfo
Ord, (forall x. CaseInfo -> Rep CaseInfo x)
-> (forall x. Rep CaseInfo x -> CaseInfo) -> Generic CaseInfo
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
$cfrom :: forall x. CaseInfo -> Rep CaseInfo x
from :: forall x. CaseInfo -> Rep CaseInfo x
$cto :: forall x. Rep CaseInfo x -> CaseInfo
to :: forall x. Rep CaseInfo x -> CaseInfo
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
  --
  -- The guard must only use the variable that the case expression
  -- matches on.
  | TALit    { TAlt -> Literal
aLit :: Literal,   aBody:: TTerm }
  deriving (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
$cshowsPrec :: Int -> TAlt -> ShowS
showsPrec :: Int -> TAlt -> ShowS
$cshow :: TAlt -> String
show :: TAlt -> String
$cshowList :: [TAlt] -> ShowS
showList :: [TAlt] -> ShowS
Show, TAlt -> TAlt -> Bool
(TAlt -> TAlt -> Bool) -> (TAlt -> TAlt -> Bool) -> Eq TAlt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TAlt -> TAlt -> Bool
== :: TAlt -> TAlt -> Bool
$c/= :: TAlt -> TAlt -> Bool
/= :: 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
$ccompare :: TAlt -> TAlt -> Ordering
compare :: TAlt -> TAlt -> Ordering
$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
>= :: TAlt -> TAlt -> Bool
$cmax :: TAlt -> TAlt -> TAlt
max :: TAlt -> TAlt -> TAlt
$cmin :: TAlt -> TAlt -> TAlt
min :: TAlt -> TAlt -> TAlt
Ord, (forall x. TAlt -> Rep TAlt x)
-> (forall x. Rep TAlt x -> TAlt) -> Generic TAlt
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
$cfrom :: forall x. TAlt -> Rep TAlt x
from :: forall x. TAlt -> Rep TAlt x
$cto :: forall x. Rep TAlt x -> TAlt
to :: forall x. Rep TAlt x -> TAlt
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
(Int -> TError -> ShowS)
-> (TError -> String) -> ([TError] -> ShowS) -> Show TError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TError -> ShowS
showsPrec :: Int -> TError -> ShowS
$cshow :: TError -> String
show :: TError -> String
$cshowList :: [TError] -> ShowS
showList :: [TError] -> ShowS
Show, TError -> TError -> Bool
(TError -> TError -> Bool)
-> (TError -> TError -> Bool) -> Eq TError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TError -> TError -> Bool
== :: TError -> TError -> Bool
$c/= :: TError -> TError -> Bool
/= :: 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
$ccompare :: TError -> TError -> Ordering
compare :: TError -> TError -> Ordering
$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
>= :: TError -> TError -> Bool
$cmax :: TError -> TError -> TError
max :: TError -> TError -> TError
$cmin :: TError -> TError -> TError
min :: TError -> TError -> TError
Ord, (forall x. TError -> Rep TError x)
-> (forall x. Rep TError x -> TError) -> Generic TError
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
$cfrom :: forall x. TError -> Rep TError x
from :: forall x. TError -> Rep TError x
$cto :: forall x. Rep TError x -> TError
to :: forall x. Rep TError x -> TError
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 = 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


-- * 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 = (([ArgUsage], [a]) -> [a]) -> [ArgUsage] -> [a] -> [a]
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((([ArgUsage], [a]) -> [a]) -> [ArgUsage] -> [a] -> [a])
-> (([ArgUsage], [a]) -> [a]) -> [ArgUsage] -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ \case
  ([], [a]
args) -> [a]
args
  ([ArgUsage]
_ , [])   -> []
  (ArgUsage
ArgUsed   : [ArgUsage]
used, a
a : [a]
args) -> a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [ArgUsage] -> [a] -> [a]
forall a. [ArgUsage] -> [a] -> [a]
filterUsed [ArgUsage]
used [a]
args
  (ArgUsage
ArgUnused : [ArgUsage]
used, a
a : [a]
args) ->     [ArgUsage] -> [a] -> [a]
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