    {-# 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