{-|
Module      : Idris.Core.CaseTree
Description : Module to define and interact with case trees.

License     : BSD3
Maintainer  : The Idris Community.

Note: The case-tree elaborator only produces (Case n alts)-cases;
in other words, it never inspects anything else than variables.

ProjCase is a special powerful case construct that allows inspection
of compound terms. Occurrences of ProjCase arise no earlier than
in the function `prune` as a means of optimisation
of already built case trees.

While the intermediate representation (follows in the pipeline, named LExp)
allows casing on arbitrary terms, here we choose to maintain the distinction
in order to allow for better optimisation opportunities.

-}

{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances,
             PatternGuards, TypeSynonymInstances #-}

module Idris.Core.CaseTree (
    CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
  , Phase(..), CaseTree, CaseType(..)
  , simpleCase, small, namesUsed, findCalls, findCalls', findUsedArgs
  , substSC, substAlt, mkForce
  ) where

import Idris.Core.TT

import Control.Monad.Reader
import Control.Monad.State
import Data.List hiding (partition)
import qualified Data.List (partition)
import qualified Data.Set as S
import GHC.Generics (Generic)

data CaseDef = CaseDef [Name] !SC [Term]
    deriving Int -> CaseDef -> ShowS
[CaseDef] -> ShowS
CaseDef -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CaseDef] -> ShowS
$cshowList :: [CaseDef] -> ShowS
show :: CaseDef -> String
$cshow :: CaseDef -> String
showsPrec :: Int -> CaseDef -> ShowS
$cshowsPrec :: Int -> CaseDef -> ShowS
Show

data SC' t = Case CaseType Name [CaseAlt' t]  -- ^ invariant: lowest tags first
           | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
           | STerm !t
           | UnmatchedCase String -- ^ error message
           | ImpossibleCase -- ^ already checked to be impossible
    deriving (SC' t -> SC' t -> Bool
forall t. Eq t => SC' t -> SC' t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SC' t -> SC' t -> Bool
$c/= :: forall t. Eq t => SC' t -> SC' t -> Bool
== :: SC' t -> SC' t -> Bool
$c== :: forall t. Eq t => SC' t -> SC' t -> Bool
Eq, SC' t -> SC' t -> Ordering
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
forall {t}. Ord t => Eq (SC' t)
forall t. Ord t => SC' t -> SC' t -> Bool
forall t. Ord t => SC' t -> SC' t -> Ordering
forall t. Ord t => SC' t -> SC' t -> SC' t
min :: SC' t -> SC' t -> SC' t
$cmin :: forall t. Ord t => SC' t -> SC' t -> SC' t
max :: SC' t -> SC' t -> SC' t
$cmax :: forall t. Ord t => SC' t -> SC' t -> SC' t
>= :: SC' t -> SC' t -> Bool
$c>= :: forall t. Ord t => SC' t -> SC' t -> Bool
> :: SC' t -> SC' t -> Bool
$c> :: forall t. Ord t => SC' t -> SC' t -> Bool
<= :: SC' t -> SC' t -> Bool
$c<= :: forall t. Ord t => SC' t -> SC' t -> Bool
< :: SC' t -> SC' t -> Bool
$c< :: forall t. Ord t => SC' t -> SC' t -> Bool
compare :: SC' t -> SC' t -> Ordering
$ccompare :: forall t. Ord t => SC' t -> SC' t -> Ordering
Ord, forall a b. a -> SC' b -> SC' a
forall a b. (a -> b) -> SC' a -> SC' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SC' b -> SC' a
$c<$ :: forall a b. a -> SC' b -> SC' a
fmap :: forall a b. (a -> b) -> SC' a -> SC' b
$cfmap :: forall a b. (a -> b) -> SC' a -> SC' b
Functor, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (SC' t) x -> SC' t
forall t x. SC' t -> Rep (SC' t) x
$cto :: forall t x. Rep (SC' t) x -> SC' t
$cfrom :: forall t x. SC' t -> Rep (SC' t) x
Generic)
{-!
deriving instance Binary SC'
!-}

data CaseType = Updatable | Shared
   deriving (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, 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, 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)

type SC = SC' Term

data CaseAlt' t = ConCase Name Int [Name] !(SC' t)
                | FnCase Name [Name]      !(SC' t) -- ^ reflection function
                | ConstCase Const         !(SC' t)
                | SucCase Name            !(SC' t)
                | DefaultCase             !(SC' t)
    deriving (Int -> CaseAlt' t -> ShowS
forall t. Show t => Int -> CaseAlt' t -> ShowS
forall t. Show t => [CaseAlt' t] -> ShowS
forall t. Show t => CaseAlt' t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CaseAlt' t] -> ShowS
$cshowList :: forall t. Show t => [CaseAlt' t] -> ShowS
show :: CaseAlt' t -> String
$cshow :: forall t. Show t => CaseAlt' t -> String
showsPrec :: Int -> CaseAlt' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> CaseAlt' t -> ShowS
Show, CaseAlt' t -> CaseAlt' t -> Bool
forall t. Eq t => CaseAlt' t -> CaseAlt' t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CaseAlt' t -> CaseAlt' t -> Bool
$c/= :: forall t. Eq t => CaseAlt' t -> CaseAlt' t -> Bool
== :: CaseAlt' t -> CaseAlt' t -> Bool
$c== :: forall t. Eq t => CaseAlt' t -> CaseAlt' t -> Bool
Eq, CaseAlt' t -> CaseAlt' t -> Ordering
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
forall {t}. Ord t => Eq (CaseAlt' t)
forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Ordering
forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
min :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t
$cmin :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
max :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t
$cmax :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
>= :: CaseAlt' t -> CaseAlt' t -> Bool
$c>= :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
> :: CaseAlt' t -> CaseAlt' t -> Bool
$c> :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
<= :: CaseAlt' t -> CaseAlt' t -> Bool
$c<= :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
< :: CaseAlt' t -> CaseAlt' t -> Bool
$c< :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
compare :: CaseAlt' t -> CaseAlt' t -> Ordering
$ccompare :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Ordering
Ord, forall a b. a -> CaseAlt' b -> CaseAlt' a
forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> CaseAlt' b -> CaseAlt' a
$c<$ :: forall a b. a -> CaseAlt' b -> CaseAlt' a
fmap :: forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b
$cfmap :: forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b
Functor, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (CaseAlt' t) x -> CaseAlt' t
forall t x. CaseAlt' t -> Rep (CaseAlt' t) x
$cto :: forall t x. Rep (CaseAlt' t) x -> CaseAlt' t
$cfrom :: forall t x. CaseAlt' t -> Rep (CaseAlt' t) x
Generic)
{-!
deriving instance Binary CaseAlt'
!-}

type CaseAlt = CaseAlt' Term

instance Show t => Show (SC' t) where
    show :: SC' t -> String
show SC' t
sc = forall {a}. Show a => Int -> SC' a -> String
show' Int
1 SC' t
sc
      where
        show' :: Int -> SC' a -> String
show' Int
i (Case CaseType
up Name
n [CaseAlt' a]
alts) = String
"case" forall a. [a] -> [a] -> [a]
++ String
u forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" of\n" forall a. [a] -> [a] -> [a]
++ Int -> String
indent Int
i forall a. [a] -> [a] -> [a]
++
                                    String -> [String] -> String
showSep (String
"\n" forall a. [a] -> [a] -> [a]
++ Int -> String
indent Int
i) (forall a b. (a -> b) -> [a] -> [b]
map (Int -> CaseAlt' a -> String
showA Int
i) [CaseAlt' a]
alts)
            where u :: String
u = case CaseType
up of
                           CaseType
Updatable -> String
"! "
                           CaseType
Shared -> String
" "
        show' Int
i (ProjCase a
tm [CaseAlt' a]
alts) = String
"case " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
tm forall a. [a] -> [a] -> [a]
++ String
" of " forall a. [a] -> [a] -> [a]
++
                                      String -> [String] -> String
showSep (String
"\n" forall a. [a] -> [a] -> [a]
++ Int -> String
indent Int
i) (forall a b. (a -> b) -> [a] -> [b]
map (Int -> CaseAlt' a -> String
showA Int
i) [CaseAlt' a]
alts)
        show' Int
i (STerm a
tm) = forall a. Show a => a -> String
show a
tm
        show' Int
i (UnmatchedCase String
str) = String
"error " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
str
        show' Int
i SC' a
ImpossibleCase = String
"impossible"

        indent :: Int -> String
indent Int
i = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
i (forall a. a -> [a]
repeat String
"    ")

        showA :: Int -> CaseAlt' a -> String
showA Int
i (ConCase Name
n Int
t [Name]
args SC' a
sc)
           = forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"(" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep (String
", ") (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Name]
args) forall a. [a] -> [a] -> [a]
++ String
") => "
                forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iforall a. Num a => a -> a -> a
+Int
1) SC' a
sc
        showA Int
i (FnCase Name
n [Name]
args SC' a
sc)
           = String
"FN " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"(" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep (String
", ") (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Name]
args) forall a. [a] -> [a] -> [a]
++ String
") => "
                forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iforall a. Num a => a -> a -> a
+Int
1) SC' a
sc
        showA Int
i (ConstCase Const
t SC' a
sc)
           = forall a. Show a => a -> String
show Const
t forall a. [a] -> [a] -> [a]
++ String
" => " forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iforall a. Num a => a -> a -> a
+Int
1) SC' a
sc
        showA Int
i (SucCase Name
n SC' a
sc)
           = forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"+1 => " forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iforall a. Num a => a -> a -> a
+Int
1) SC' a
sc
        showA Int
i (DefaultCase SC' a
sc)
           = String
"_ => " forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iforall a. Num a => a -> a -> a
+Int
1) SC' a
sc


type CaseTree = SC
type Clause   = ([Pat], (Term, Term))
type CS = ([Term], Int, [(Name, Type)])

instance TermSize SC where
    termsize :: Name -> SC -> Int
termsize Name
n (Case CaseType
_ Name
n' [CaseAlt' Term]
as) = forall a. TermSize a => Name -> a -> Int
termsize Name
n [CaseAlt' Term]
as
    termsize Name
n (ProjCase Term
n' [CaseAlt' Term]
as) = forall a. TermSize a => Name -> a -> Int
termsize Name
n [CaseAlt' Term]
as
    termsize Name
n (STerm Term
t) = forall a. TermSize a => Name -> a -> Int
termsize Name
n Term
t
    termsize Name
n SC
_ = Int
1

instance TermSize CaseAlt where
    termsize :: Name -> CaseAlt' Term -> Int
termsize Name
n (ConCase Name
_ Int
_ [Name]
_ SC
s) = forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
    termsize Name
n (FnCase Name
_ [Name]
_ SC
s) = forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
    termsize Name
n (ConstCase Const
_ SC
s) = forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
    termsize Name
n (SucCase Name
_ SC
s) = forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
    termsize Name
n (DefaultCase SC
s) = forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s

-- simple terms can be inlined trivially - good for primitives in particular
-- To avoid duplicating work, don't inline something which uses one
-- of its arguments in more than one place

small :: Name -> [Name] -> SC -> Bool
small :: Name -> [Name] -> SC -> Bool
small Name
n [Name]
args SC
t = let as :: [Name]
as = forall {t :: * -> *}. Foldable t => SC -> t Name -> [Name]
findAllUsedArgs SC
t [Name]
args in
                     forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => [a] -> [a]
nub [Name]
as) Bool -> Bool -> Bool
&&
                     forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
t forall a. Ord a => a -> a -> Bool
< Int
20

namesUsed :: SC -> [Name]
namesUsed :: SC -> [Name]
namesUsed SC
sc = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [Name] -> SC -> [Name]
nu' [] SC
sc where
    nu' :: [Name] -> SC -> [Name]
nu' [Name]
ps (Case CaseType
_ Name
n [CaseAlt' Term]
alts) = forall a. Eq a => [a] -> [a]
nub (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Name] -> CaseAlt' Term -> [Name]
nua [Name]
ps) [CaseAlt' Term]
alts) forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n]
    nu' [Name]
ps (ProjCase Term
t [CaseAlt' Term]
alts) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall {a}. Eq a => [a] -> TT a -> [a]
nut [Name]
ps Term
t forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Name] -> CaseAlt' Term -> [Name]
nua [Name]
ps) [CaseAlt' Term]
alts
    nu' [Name]
ps (STerm Term
t)     = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall {a}. Eq a => [a] -> TT a -> [a]
nut [Name]
ps Term
t
    nu' [Name]
ps SC
_ = []

    nua :: [Name] -> CaseAlt' Term -> [Name]
nua [Name]
ps (ConCase Name
n Int
i [Name]
args SC
sc) = forall a. Eq a => [a] -> [a]
nub ([Name] -> SC -> [Name]
nu' ([Name]
ps forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc) forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
args
    nua [Name]
ps (FnCase Name
n [Name]
args SC
sc) = forall a. Eq a => [a] -> [a]
nub ([Name] -> SC -> [Name]
nu' ([Name]
ps forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc) forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
args
    nua [Name]
ps (ConstCase Const
_ SC
sc) = [Name] -> SC -> [Name]
nu' [Name]
ps SC
sc
    nua [Name]
ps (SucCase Name
_ SC
sc) = [Name] -> SC -> [Name]
nu' [Name]
ps SC
sc
    nua [Name]
ps (DefaultCase SC
sc) = [Name] -> SC -> [Name]
nu' [Name]
ps SC
sc

    nut :: [a] -> TT a -> [a]
nut [a]
ps (P NameType
_ a
n TT a
_) | a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ps = []
                     | Bool
otherwise = [a
n]
    nut [a]
ps (App AppStatus a
_ TT a
f TT a
a) = [a] -> TT a -> [a]
nut [a]
ps TT a
f forall a. [a] -> [a] -> [a]
++ [a] -> TT a -> [a]
nut [a]
ps TT a
a
    nut [a]
ps (Proj TT a
t Int
_) = [a] -> TT a -> [a]
nut [a]
ps TT a
t
    nut [a]
ps (Bind a
n (Let RigCount
_ TT a
t TT a
v) TT a
sc) = [a] -> TT a -> [a]
nut [a]
ps TT a
v forall a. [a] -> [a] -> [a]
++ [a] -> TT a -> [a]
nut (a
nforall a. a -> [a] -> [a]
:[a]
ps) TT a
sc
    nut [a]
ps (Bind a
n Binder (TT a)
b TT a
sc) = [a] -> TT a -> [a]
nut (a
nforall a. a -> [a] -> [a]
:[a]
ps) TT a
sc
    nut [a]
ps TT a
_ = []

-- | Return all called functions, and which arguments are used
-- in each argument position for the call, in order to help reduce
-- compilation time, and trace all unused arguments
findCalls :: SC -> [Name] -> [(Name, [[Name]])]
findCalls :: SC -> [Name] -> [(Name, [[Name]])]
findCalls = Bool -> SC -> [Name] -> [(Name, [[Name]])]
findCalls' Bool
False

findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
findCalls' Bool
ignoreasserts SC
sc [Name]
topargs = forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
topargs SC
sc where
    nu' :: [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps (Case CaseType
_ Name
n [CaseAlt' Term]
alts) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> CaseAlt' Term -> Set (Name, [[Name]])
nua (Name
n forall a. a -> [a] -> [a]
: [Name]
ps)) [CaseAlt' Term]
alts
    nu' [Name]
ps (ProjCase Term
t [CaseAlt' Term]
alts) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
t forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> CaseAlt' Term -> Set (Name, [[Name]])
nua [Name]
ps) [CaseAlt' Term]
alts
    nu' [Name]
ps (STerm Term
t)     = [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
t
    nu' [Name]
ps SC
_ = forall a. Set a
S.empty

    nua :: [Name] -> CaseAlt' Term -> Set (Name, [[Name]])
nua [Name]
ps (ConCase Name
n Int
i [Name]
args SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' ([Name]
ps forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc
    nua [Name]
ps (FnCase Name
n [Name]
args SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' ([Name]
ps forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc
    nua [Name]
ps (ConstCase Const
_ SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps SC
sc
    nua [Name]
ps (SucCase Name
_ SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps SC
sc
    nua [Name]
ps (DefaultCase SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps SC
sc

    nut :: [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps (P NameType
_ Name
n Term
_) | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ps = forall a. Set a
S.empty
                     | Bool
otherwise = forall a. a -> Set a
S.singleton (Name
n, [])
    nut [Name]
ps fn :: Term
fn@(App AppStatus Name
_ Term
f Term
a)
        | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn
             = if Bool
ignoreasserts Bool -> Bool -> Bool
&& Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"assert_total"
                  then forall a. Set a
S.empty
                  else if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ps
                          then forall a. Ord a => Set a -> Set a -> Set a
S.union ([Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
f) ([Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
a)
                          else forall a. Ord a => a -> Set a -> Set a
S.insert (Name
n, forall a b. (a -> b) -> [a] -> [b]
map Term -> [Name]
argNames [Term]
args)
                                   (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps) [Term]
args)
        | (P (TCon Int
_ Int
_) Name
n Term
_, [Term]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn = forall a. Set a
S.empty
        | Bool
otherwise = forall a. Ord a => Set a -> Set a -> Set a
S.union ([Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
f) ([Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
a)
    nut [Name]
ps (Bind Name
n (Let RigCount
_ Term
t Term
v) Term
sc) = forall a. Ord a => Set a -> Set a -> Set a
S.union ([Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
v) ([Name] -> Term -> Set (Name, [[Name]])
nut (Name
nforall a. a -> [a] -> [a]
:[Name]
ps) Term
sc)
    nut [Name]
ps (Proj Term
t Int
_) = [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
t
    nut [Name]
ps (Bind Name
n Binder Term
b Term
sc) = [Name] -> Term -> Set (Name, [[Name]])
nut (Name
nforall a. a -> [a] -> [a]
:[Name]
ps) Term
sc
    nut [Name]
ps Term
_ = forall a. Set a
S.empty

    argNames :: Term -> [Name]
argNames Term
tm = let ns :: [Name]
ns = Term -> [Name]
directUse Term
tm in
                      forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns) [Name]
topargs

-- Find names which are used directly (i.e. not in a function call) in a term

directUse :: TT Name -> [Name]
directUse :: Term -> [Name]
directUse (P NameType
_ Name
n Term
_) = [Name
n]
directUse (Bind Name
n (Let RigCount
_ Term
t Term
v) Term
sc) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
v forall a. [a] -> [a] -> [a]
++ (Term -> [Name]
directUse Term
sc forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n])
                                        forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
t
directUse (Bind Name
n Binder Term
b Term
sc) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse (forall b. Binder b -> b
binderTy Binder Term
b) forall a. [a] -> [a] -> [a]
++ (Term -> [Name]
directUse Term
sc forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n])
directUse fn :: Term
fn@(App AppStatus Name
_ Term
f Term
a)
    | (P NameType
Ref (UN Text
pfk) Term
_, [App AppStatus Name
_ Term
e Term
w]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn,
         Text
pfk forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"prim_fork"
             = Term -> [Name]
directUse Term
e forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
w -- HACK so that fork works
    | (P NameType
Ref (UN Text
fce) Term
_, [Term
_, Term
_, Term
a]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn,
         Text
fce forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Force"
             = Term -> [Name]
directUse Term
a -- forcing a value counts as a use
    | (P NameType
Ref Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn = [] -- need to know what n does with them
    | (P (TCon Int
_ Int
_) Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn = [] -- type constructors not used at runtime
    | Bool
otherwise = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
f forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
a
directUse (Proj Term
x Int
i) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
x
directUse Term
_ = []

-- Find all directly used arguments (i.e. used but not in function calls)

findUsedArgs :: SC -> [Name] -> [Name]
findUsedArgs :: SC -> [Name] -> [Name]
findUsedArgs SC
sc [Name]
topargs = forall a. Eq a => [a] -> [a]
nub (forall {t :: * -> *}. Foldable t => SC -> t Name -> [Name]
findAllUsedArgs SC
sc [Name]
topargs)

findAllUsedArgs :: SC -> t Name -> [Name]
findAllUsedArgs SC
sc t Name
topargs = forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
topargs) (SC -> [Name]
nu' SC
sc) where
    nu' :: SC -> [Name]
nu' (Case CaseType
_ Name
n [CaseAlt' Term]
alts) = Name
n forall a. a -> [a] -> [a]
: forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CaseAlt' Term -> [Name]
nua [CaseAlt' Term]
alts
    nu' (ProjCase Term
t [CaseAlt' Term]
alts) = Term -> [Name]
directUse Term
t forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CaseAlt' Term -> [Name]
nua [CaseAlt' Term]
alts
    nu' (STerm Term
t)     = Term -> [Name]
directUse Term
t
    nu' SC
_             = []

    nua :: CaseAlt' Term -> [Name]
nua (ConCase Name
n Int
i [Name]
args SC
sc) = SC -> [Name]
nu' SC
sc
    nua (FnCase Name
n  [Name]
args SC
sc)   = SC -> [Name]
nu' SC
sc
    nua (ConstCase Const
_ SC
sc)      = SC -> [Name]
nu' SC
sc
    nua (SucCase Name
_ SC
sc)        = SC -> [Name]
nu' SC
sc
    nua (DefaultCase SC
sc)      = SC -> [Name]
nu' SC
sc

-- Return whether name is used anywhere in a case tree
isUsed :: SC -> Name -> Bool
isUsed :: SC -> Name -> Bool
isUsed SC
sc Name
n = SC -> Bool
used SC
sc where

  used :: SC -> Bool
used (Case CaseType
_ Name
n' [CaseAlt' Term]
alts) = Name
n forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CaseAlt' Term -> Bool
usedA [CaseAlt' Term]
alts
  used (ProjCase Term
t [CaseAlt' Term]
alts) = Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall n. Eq n => TT n -> [n]
freeNames Term
t Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CaseAlt' Term -> Bool
usedA [CaseAlt' Term]
alts
  used (STerm Term
t) = Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall n. Eq n => TT n -> [n]
freeNames Term
t
  used SC
_ = Bool
False

  usedA :: CaseAlt' Term -> Bool
usedA (ConCase Name
_ Int
_ [Name]
args SC
sc) = SC -> Bool
used SC
sc
  usedA (FnCase Name
_ [Name]
args SC
sc) = SC -> Bool
used SC
sc
  usedA (ConstCase Const
_ SC
sc) = SC -> Bool
used SC
sc
  usedA (SucCase Name
_ SC
sc) = SC -> Bool
used SC
sc
  usedA (DefaultCase SC
sc) = SC -> Bool
used SC
sc

type ErasureInfo = Name -> [Int]  -- name to list of inaccessible arguments; empty list if name not found
type CaseBuilder a = ReaderT ErasureInfo (State CS) a

runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
runCaseBuilder :: forall a. ErasureInfo -> CaseBuilder a -> CS -> (a, CS)
runCaseBuilder ErasureInfo
ei CaseBuilder a
bld = forall s a. State s a -> s -> (a, s)
runState forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CaseBuilder a
bld ErasureInfo
ei

data Phase = CoverageCheck [Int] -- list of positions explicitly given
           | CompileTime
           | RunTime
    deriving (Int -> Phase -> ShowS
[Phase] -> ShowS
Phase -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Phase] -> ShowS
$cshowList :: [Phase] -> ShowS
show :: Phase -> String
$cshow :: Phase -> String
showsPrec :: Int -> Phase -> ShowS
$cshowsPrec :: Int -> Phase -> ShowS
Show, Phase -> Phase -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Phase -> Phase -> Bool
$c/= :: Phase -> Phase -> Bool
== :: Phase -> Phase -> Bool
$c== :: Phase -> Phase -> Bool
Eq)

-- Generate a simple case tree
-- Work Right to Left

simpleCase :: Bool -> SC -> Bool ->
              Phase -> FC ->
              -- Following two can be empty lists when Phase = CoverageCheck
              [Int] -> -- Inaccessible argument positions
              [(Type, Bool)] -> -- (Argument type, whether it's canonical)
              [([Name], Term, Term)] ->
              ErasureInfo ->
              TC CaseDef
simpleCase :: Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
tc SC
defcase Bool
reflect Phase
phase FC
fc [Int]
inacc [(Term, Bool)]
argtys [([Name], Term, Term)]
cs ErasureInfo
erInfo
      = forall {t :: * -> *}.
Foldable t =>
Bool -> SC -> Phase -> FC -> [(t Name, Term, Term)] -> TC CaseDef
sc' Bool
tc SC
defcase Phase
phase FC
fc (forall a. (a -> Bool) -> [a] -> [a]
filter (\([Name]
_, Term
_, Term
r) ->
                                          case Term
r of
                                            Term
Impossible -> Bool
False
                                            Term
_ -> Bool
True) [([Name], Term, Term)]
cs)
          where
 sc' :: Bool -> SC -> Phase -> FC -> [(t Name, Term, Term)] -> TC CaseDef
sc' Bool
tc SC
defcase Phase
phase FC
fc []
                 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Name] -> SC -> [Term] -> CaseDef
CaseDef [] (forall t. String -> SC' t
UnmatchedCase (forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
":No pattern clauses")) []
 sc' Bool
tc SC
defcase Phase
phase FC
fc [(t Name, Term, Term)]
cs
      = let proj :: Bool
proj       = Phase
phase forall a. Eq a => a -> a -> Bool
== Phase
RunTime
            pats :: [(t Name, [Pat], (Term, Term))]
pats       = forall a b. (a -> b) -> [a] -> [b]
map (\ (t Name
avs, Term
l, Term
r) ->
                                   (t Name
avs, Bool -> Bool -> Term -> [Pat]
toPats Bool
reflect Bool
tc Term
l, (Term
l, Term
r))) [(t Name, Term, Term)]
cs
            chkPats :: TC [Clause]
chkPats    = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t :: * -> *} {b}.
Foldable t =>
(t Name, [Pat], b) -> TC ([Pat], b)
chkAccessible [(t Name, [Pat], (Term, Term))]
pats in
            case TC [Clause]
chkPats of
                OK [Clause]
pats ->
                    let numargs :: Int
numargs    = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a b. (a, b) -> a
fst (forall a. [a] -> a
head [Clause]
pats))
                        ns :: [Name]
ns         = forall a. Int -> [a] -> [a]
take Int
numargs [Name]
args
                        ([Name]
ns', [Clause]
ps') = Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
order Phase
phase [(Name
n, Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
inacc) | (Int
i,Name
n) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Name]
ns] [Clause]
pats (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Term, Bool)]
argtys)
                        (SC
tree, CS
st) = forall a. ErasureInfo -> CaseBuilder a -> CS -> (a, CS)
runCaseBuilder ErasureInfo
erInfo
                                         ([Name] -> [Clause] -> SC -> CaseBuilder SC
match [Name]
ns' [Clause]
ps' SC
defcase)
                                         ([], Int
numargs, [])
                        sc :: SC
sc         = SC -> SC
removeUnreachable (Bool -> SC -> SC
prune Bool
proj ([Name] -> SC -> SC
depatt [Name]
ns' SC
tree))
                        t :: CaseDef
t          = [Name] -> SC -> [Term] -> CaseDef
CaseDef [Name]
ns SC
sc (forall {a} {b} {c}. (a, b, c) -> a
fstT CS
st) in
                        if Bool
proj then forall (m :: * -> *) a. Monad m => a -> m a
return (CaseDef -> CaseDef
stripLambdas CaseDef
t)
                                else forall (m :: * -> *) a. Monad m => a -> m a
return CaseDef
t
                Error Err
err -> forall a. Err -> TC a
Error (forall t. FC -> Err' t -> Err' t
At FC
fc Err
err)
    where args :: [Name]
args = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> String -> Name
sMN Int
i String
"e") [Int
0..]
          fstT :: (a, b, c) -> a
fstT (a
x, b
_, c
_) = a
x

          -- Check that all pattern variables are reachable by a case split
          -- Otherwise, they won't make sense on the RHS.
          chkAccessible :: (t Name, [Pat], b) -> TC ([Pat], b)
chkAccessible (t Name
avs, [Pat]
l, b
c)
               | Phase
phase forall a. Eq a => a -> a -> Bool
/= Phase
CompileTime Bool -> Bool -> Bool
|| Bool
reflect = forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)
               | Bool
otherwise = do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Pat] -> Name -> TC ()
acc [Pat]
l) t Name
avs
                                forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)

          acc :: [Pat] -> Name -> TC ()
acc [] Name
n = forall a. Err -> TC a
Error (forall t. Name -> Err' t
Inaccessible Name
n)
          acc (PV Name
x Term
t : [Pat]
xs) Name
n | Name
x forall a. Eq a => a -> a -> Bool
== Name
n = forall a. a -> TC a
OK ()
          acc (PCon Bool
_ Name
_ Int
_ [Pat]
ps : [Pat]
xs) Name
n = [Pat] -> Name -> TC ()
acc ([Pat]
ps forall a. [a] -> [a] -> [a]
++ [Pat]
xs) Name
n
          acc (PSuc Pat
p : [Pat]
xs) Name
n = [Pat] -> Name -> TC ()
acc (Pat
p forall a. a -> [a] -> [a]
: [Pat]
xs) Name
n
          acc (Pat
_ : [Pat]
xs) Name
n = [Pat] -> Name -> TC ()
acc [Pat]
xs Name
n

data Pat = PCon Bool Name Int [Pat]
         | PConst Const
         | PInferred Pat
         | PV Name Type
         | PSuc Pat -- special case for n+1 on Integer
         | PReflected Name [Pat]
         | PAny
         | PTyPat -- typecase, not allowed, inspect last
    deriving Int -> Pat -> ShowS
[Pat] -> ShowS
Pat -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Pat] -> ShowS
$cshowList :: [Pat] -> ShowS
show :: Pat -> String
$cshow :: Pat -> String
showsPrec :: Int -> Pat -> ShowS
$cshowsPrec :: Int -> Pat -> ShowS
Show

-- If there are repeated variables, take the *last* one (could be name shadowing
-- in a where clause, so take the most recent).

toPats :: Bool -> Bool -> Term -> [Pat]
toPats :: Bool -> Bool -> Term -> [Pat]
toPats Bool
reflect Bool
tc Term
f = forall a. [a] -> [a]
reverse (Bool -> Bool -> [Term] -> [Pat]
toPat Bool
reflect Bool
tc (forall {n}. TT n -> [TT n]
getArgs Term
f)) where
   getArgs :: TT n -> [TT n]
getArgs (App AppStatus n
_ TT n
f TT n
a) = TT n
a forall a. a -> [a] -> [a]
: TT n -> [TT n]
getArgs TT n
f
   getArgs TT n
_ = []

toPat :: Bool -> Bool -> [Term] -> [Pat]
toPat :: Bool -> Bool -> [Term] -> [Pat]
toPat Bool
reflect Bool
tc = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ [Term] -> Term -> Pat
toPat' []
  where
    toPat' :: [Term] -> Term -> Pat
toPat' [Term
_,Term
_,Term
arg] (P (DCon Int
t Int
a Bool
uniq) nm :: Name
nm@(UN Text
n) Term
_)
        | Text
n forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay"
        = Bool -> Name -> Int -> [Pat] -> Pat
PCon Bool
uniq Name
nm Int
t [Pat
PAny, Pat
PAny, [Term] -> Term -> Pat
toPat' [] Term
arg]

    toPat' [Term]
args (P (DCon Int
t Int
a Bool
uniq) nm :: Name
nm@(NS (UN Text
n) [Text
own]) Term
_)
        | Text
n forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Read" Bool -> Bool -> Bool
&& Text
own forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Ownership"
        = Bool -> Name -> Int -> [Pat] -> Pat
PCon Bool
False Name
nm Int
t (forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
shareCons (forall a b. (a -> b) -> [a] -> [b]
map ([Term] -> Term -> Pat
toPat' []) [Term]
args))
      where shareCons :: Pat -> Pat
shareCons (PCon Bool
_ Name
n Int
i [Pat]
ps) = Bool -> Name -> Int -> [Pat] -> Pat
PCon Bool
False Name
n Int
i (forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
shareCons [Pat]
ps)
            shareCons Pat
p = Pat
p

    toPat' [Term]
args (P (DCon Int
t Int
a Bool
uniq) Name
n Term
_)
        = Bool -> Name -> Int -> [Pat] -> Pat
PCon Bool
uniq Name
n Int
t forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([Term] -> Term -> Pat
toPat' []) [Term]
args

    -- n + 1
    toPat' [Term
p, Constant (BI Integer
1)] (P NameType
_ (UN Text
pabi) Term
_)
        | Text
pabi forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"prim__addBigInt"
        = Pat -> Pat
PSuc forall a b. (a -> b) -> a -> b
$ [Term] -> Term -> Pat
toPat' [] Term
p

    toPat' []   (P NameType
Bound Name
n Term
ty) = Name -> Term -> Pat
PV Name
n Term
ty
    toPat' [Term]
args (App AppStatus Name
_ Term
f Term
a)    = [Term] -> Term -> Pat
toPat' (Term
a forall a. a -> [a] -> [a]
: [Term]
args) Term
f
    toPat' [Term]
args (Inferred Term
tm)  = Pat -> Pat
PInferred ([Term] -> Term -> Pat
toPat' [Term]
args Term
tm)
    toPat' [] (Constant Const
x) | Const -> Bool
isTypeConst Const
x = Pat
PTyPat
                           | Bool
otherwise     = Const -> Pat
PConst Const
x

    toPat' [] (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
t Term
_) Term
sc)
        | Bool
reflect Bool -> Bool -> Bool
&& forall n. Eq n => n -> TT n -> Bool
noOccurrence Name
n Term
sc
        = Name -> [Pat] -> Pat
PReflected (String -> Name
sUN String
"->") [[Term] -> Term -> Pat
toPat' [] Term
t, [Term] -> Term -> Pat
toPat' [] Term
sc]

    toPat' [Term]
args (P NameType
_ Name
n Term
_)
        | Bool
reflect
        = Name -> [Pat] -> Pat
PReflected Name
n forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([Term] -> Term -> Pat
toPat' []) [Term]
args

    toPat' [Term]
_ Term
t = Pat
PAny

data Partition = Cons [Clause]
               | Vars [Clause]
    deriving Int -> Partition -> ShowS
[Partition] -> ShowS
Partition -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Partition] -> ShowS
$cshowList :: [Partition] -> ShowS
show :: Partition -> String
$cshow :: Partition -> String
showsPrec :: Int -> Partition -> ShowS
$cshowsPrec :: Int -> Partition -> ShowS
Show

isVarPat :: ([Pat], b) -> Bool
isVarPat (PV Name
_ Term
_ : [Pat]
ps , b
_) = Bool
True
isVarPat (Pat
PAny   : [Pat]
ps , b
_) = Bool
True
isVarPat (Pat
PTyPat : [Pat]
ps , b
_) = Bool
True
isVarPat ([Pat], b)
_                 = Bool
False

isConPat :: ([Pat], b) -> Bool
isConPat (PCon Bool
_ Name
_ Int
_ [Pat]
_ : [Pat]
ps, b
_) = Bool
True
isConPat (PReflected Name
_ [Pat]
_ : [Pat]
ps, b
_) = Bool
True
isConPat (PSuc Pat
_   : [Pat]
ps, b
_) = Bool
True
isConPat (PConst Const
_   : [Pat]
ps, b
_) = Bool
True
isConPat ([Pat], b)
_                    = Bool
False

partition :: [Clause] -> [Partition]
partition :: [Clause] -> [Partition]
partition [] = []
partition ms :: [Clause]
ms@(Clause
m : [Clause]
_)
    | forall {b}. ([Pat], b) -> Bool
isVarPat Clause
m = let ([Clause]
vars, [Clause]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span forall {b}. ([Pat], b) -> Bool
isVarPat [Clause]
ms in
                       [Clause] -> Partition
Vars [Clause]
vars forall a. a -> [a] -> [a]
: [Clause] -> [Partition]
partition [Clause]
rest
    | forall {b}. ([Pat], b) -> Bool
isConPat Clause
m = let ([Clause]
cons, [Clause]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span forall {b}. ([Pat], b) -> Bool
isConPat [Clause]
ms in
                       [Clause] -> Partition
Cons [Clause]
cons forall a. a -> [a] -> [a]
: [Clause] -> [Partition]
partition [Clause]
rest
partition [Clause]
xs = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Partition " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Clause]
xs

-- reorder the patterns so that the one with most distinct names
-- comes next. Take rightmost first, otherwise (i.e. pick value rather
-- than dependency)
--
-- The first argument means [(Name, IsInaccessible)].

order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
-- do nothing at compile time: FIXME (EB): Put this in after checking
-- implications for Franck's reflection work... see issue 3233
-- order CompileTime ns cs _ = (map fst ns, cs)
order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
order Phase
_ []  [Clause]
cs [Bool]
cans = ([], [Clause]
cs)
order Phase
_ [(Name, Bool)]
ns' [] [Bool]
cans = (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Bool)]
ns', [])
order (CoverageCheck [Int]
pos) [(Name, Bool)]
ns' [Clause]
cs [Bool]
cans
    = let ns_out :: [Name]
ns_out = forall {a}. Int -> [a] -> [a] -> [a]
pick Int
0 [] (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Bool)]
ns')
          cs_out :: [Clause]
cs_out = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b}. ([a], b) -> ([a], b)
pickClause [Clause]
cs in
          ([Name]
ns_out, [Clause]
cs_out)
  where
    pickClause :: ([a], b) -> ([a], b)
pickClause ([a]
pats, b
def) = (forall {a}. Int -> [a] -> [a] -> [a]
pick Int
0 [] [a]
pats, b
def)

    -- Order the list so that things in a position in 'pos' are in the first
    -- part, then all the other things later. Otherwise preserve order.
    pick :: Int -> [a] -> [a] -> [a]
pick Int
i [a]
skipped [] = forall a. [a] -> [a]
reverse [a]
skipped
    pick Int
i [a]
skipped (a
x : [a]
xs)
         | Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
pos = a
x forall a. a -> [a] -> [a]
: Int -> [a] -> [a] -> [a]
pick (Int
i forall a. Num a => a -> a -> a
+ Int
1) [a]
skipped [a]
xs
         | Bool
otherwise    = Int -> [a] -> [a] -> [a]
pick (Int
i forall a. Num a => a -> a -> a
+ Int
1) (a
x forall a. a -> [a] -> [a]
: [a]
skipped) [a]
xs

order Phase
phase [(Name, Bool)]
ns' [Clause]
cs [Bool]
cans
    = let patnames :: [[((Name, Bool), (Bool, Pat))]]
patnames = forall a. [[a]] -> [[a]]
transpose (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. [a] -> [b] -> [(a, b)]
zip [(Name, Bool)]
ns') (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
cans) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [Clause]
cs)))
          -- only sort the arguments where there is no clash in
          -- constructor tags between families, the argument type is canonical,
          -- and no constructor/constant
          -- clash, because otherwise we can't reliable make the
          -- case distinction on evaluation
          ([[((Name, Bool), (Bool, Pat))]]
patnames_ord, [[((Name, Bool), (Bool, Pat))]]
patnames_rest)
                = forall a. (a -> Bool) -> [a] -> ([a], [a])
Data.List.partition ([(Bool, Pat)] -> Bool
noClash forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd) [[((Name, Bool), (Bool, Pat))]]
patnames
          patnames_ord' :: [[((Name, Bool), (Bool, Pat))]]
patnames_ord' = case Phase
phase of
                               Phase
CompileTime -> [[((Name, Bool), (Bool, Pat))]]
patnames_ord
                               -- reversing tends to make better case trees
                               -- and helps erasure
                               Phase
RunTime -> forall a. [a] -> [a]
reverse [[((Name, Bool), (Bool, Pat))]]
patnames_ord
          pats' :: [[((Name, Bool), (Bool, Pat))]]
pats' = forall a. [[a]] -> [[a]]
transpose (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {a} {a} {a} {a} {a}.
Ord a =>
[((a, a), (a, Pat))] -> [((a, a), (a, Pat))] -> Ordering
moreDistinct [[((Name, Bool), (Bool, Pat))]]
patnames_ord'
                                       forall a. [a] -> [a] -> [a]
++ [[((Name, Bool), (Bool, Pat))]]
patnames_rest) in
          (forall {b} {b} {b}. [[((b, b), b)]] -> [b]
getNOrder [[((Name, Bool), (Bool, Pat))]]
pats', forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a} {a} {b} {a} {b}. [(a, (a, b))] -> (a, b) -> ([b], b)
rebuild [[((Name, Bool), (Bool, Pat))]]
pats' [Clause]
cs)
  where
    getNOrder :: [[((b, b), b)]] -> [b]
getNOrder [] = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Failed order on " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Bool)]
ns', [Clause]
cs)
    getNOrder ([((b, b), b)]
c : [[((b, b), b)]]
_) = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [((b, b), b)]
c

    rebuild :: [(a, (a, b))] -> (a, b) -> ([b], b)
rebuild [(a, (a, b))]
patnames (a, b)
clause = (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(a, (a, b))]
patnames, forall a b. (a, b) -> b
snd (a, b)
clause)

    noClash :: [(Bool, Pat)] -> Bool
noClash [] = Bool
True
    noClash ((Bool
can, Pat
p) : [(Bool, Pat)]
ps) = Bool
can Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Pat -> Pat -> Bool
clashPat Pat
p) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Bool, Pat)]
ps))
                                  Bool -> Bool -> Bool
&& [(Bool, Pat)] -> Bool
noClash [(Bool, Pat)]
ps

    clashPat :: Pat -> Pat -> Bool
clashPat (PCon Bool
_ Name
_ Int
_ [Pat]
_) (PConst Const
_) = Bool
True
    clashPat (PConst Const
_) (PCon Bool
_ Name
_ Int
_ [Pat]
_) = Bool
True
    clashPat (PCon Bool
_ Name
_ Int
_ [Pat]
_) (PSuc Pat
_) = Bool
True
    clashPat (PSuc Pat
_) (PCon Bool
_ Name
_ Int
_ [Pat]
_) = Bool
True
    clashPat (PCon Bool
_ Name
n Int
i [Pat]
_) (PCon Bool
_ Name
n' Int
i' [Pat]
_) | Int
i forall a. Eq a => a -> a -> Bool
== Int
i' = Name
n forall a. Eq a => a -> a -> Bool
/= Name
n'
    clashPat Pat
_ Pat
_ = Bool
False

    -- this compares (+isInaccessible, -numberOfCases)
    moreDistinct :: [((a, a), (a, Pat))] -> [((a, a), (a, Pat))] -> Ordering
moreDistinct [((a, a), (a, Pat))]
xs [((a, a), (a, Pat))]
ys
        = forall a. Ord a => a -> a -> Ordering
compare (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [((a, a), (a, Pat))]
xs, forall {a}. [Either Name Const] -> [(a, Pat)] -> Int
numNames [] (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [((a, a), (a, Pat))]
ys))
                  (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [((a, a), (a, Pat))]
ys, forall {a}. [Either Name Const] -> [(a, Pat)] -> Int
numNames [] (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [((a, a), (a, Pat))]
xs))

    numNames :: [Either Name Const] -> [(a, Pat)] -> Int
numNames [Either Name Const]
xs ((a
_, PCon Bool
_ Name
n Int
_ [Pat]
_) : [(a, Pat)]
ps)
        | Bool -> Bool
not (forall a b. a -> Either a b
Left Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Either Name Const]
xs) = [Either Name Const] -> [(a, Pat)] -> Int
numNames (forall a b. a -> Either a b
Left Name
n forall a. a -> [a] -> [a]
: [Either Name Const]
xs) [(a, Pat)]
ps
    numNames [Either Name Const]
xs ((a
_, PConst Const
c) : [(a, Pat)]
ps)
        | Bool -> Bool
not (forall a b. b -> Either a b
Right Const
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Either Name Const]
xs) = [Either Name Const] -> [(a, Pat)] -> Int
numNames (forall a b. b -> Either a b
Right Const
c forall a. a -> [a] -> [a]
: [Either Name Const]
xs) [(a, Pat)]
ps
    numNames [Either Name Const]
xs ((a, Pat)
_ : [(a, Pat)]
ps) = [Either Name Const] -> [(a, Pat)] -> Int
numNames [Either Name Const]
xs [(a, Pat)]
ps
    numNames [Either Name Const]
xs [] = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Name Const]
xs

-- Reorder the patterns in the clause so that the PInferred patterns come
-- last. Also strip 'PInferred' from the top level patterns so that we can
-- go ahead and match.
orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])
orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])
orderByInf [Name]
vs [Clause]
cs = let alwaysInf :: [Int]
alwaysInf = forall {a} {b}. (Num a, Eq a) => [([Pat], b)] -> [a]
getInf [Clause]
cs in
                       (forall a. [Int] -> [a] -> [a]
selectInf [Int]
alwaysInf [Name]
vs,
                        forall a b. (a -> b) -> [a] -> [b]
map forall {b}. ([Pat], b) -> ([Pat], b)
deInf (forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> Clause -> Clause
selectExp [Int]
alwaysInf) [Clause]
cs))
  where
    getInf :: [([Pat], b)] -> [a]
getInf [] = []
    getInf [([Pat]
pats, b
def)] = forall {t}. Num t => t -> [Pat] -> [t]
infPos a
0 [Pat]
pats
    getInf (([Pat]
pats, b
def) : [([Pat], b)]
cs) = forall {t}. Num t => t -> [Pat] -> [t]
infPos a
0 [Pat]
pats forall a. Eq a => [a] -> [a] -> [a]
`intersect` [([Pat], b)] -> [a]
getInf [([Pat], b)]
cs

    selectExp :: [Int] -> Clause -> Clause
    selectExp :: [Int] -> Clause -> Clause
selectExp [Int]
infs ([Pat]
pats, (Term, Term)
def)
         = let ([Pat]
notInf, [Pat]
inf) = forall {t :: * -> *} {t} {a}.
(Foldable t, Eq t, Num t) =>
t -> t t -> [a] -> [a] -> [a] -> ([a], [a])
splitPats Int
0 [Int]
infs [] [] [Pat]
pats in
               ([Pat]
notInf forall a. [a] -> [a] -> [a]
++ [Pat]
inf, (Term, Term)
def)

    selectInf :: [Int] -> [a] -> [a]
    selectInf :: forall a. [Int] -> [a] -> [a]
selectInf [Int]
infs [a]
ns = let ([a]
notInf, [a]
inf) = forall {t :: * -> *} {t} {a}.
(Foldable t, Eq t, Num t) =>
t -> t t -> [a] -> [a] -> [a] -> ([a], [a])
splitPats Int
0 [Int]
infs [] [] [a]
ns in
                            [a]
notInf forall a. [a] -> [a] -> [a]
++ [a]
inf

    splitPats :: t -> t t -> [a] -> [a] -> [a] -> ([a], [a])
splitPats t
i t t
infpos [a]
notInf [a]
inf [] = (forall a. [a] -> [a]
reverse [a]
notInf, forall a. [a] -> [a]
reverse [a]
inf)
    splitPats t
i t t
infpos [a]
notInf [a]
inf (a
p : [a]
ps)
         | t
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t t
infpos = t -> t t -> [a] -> [a] -> [a] -> ([a], [a])
splitPats (t
i forall a. Num a => a -> a -> a
+ t
1) t t
infpos [a]
notInf (a
p forall a. a -> [a] -> [a]
: [a]
inf) [a]
ps
         | Bool
otherwise = t -> t t -> [a] -> [a] -> [a] -> ([a], [a])
splitPats (t
i forall a. Num a => a -> a -> a
+ t
1) t t
infpos (a
p forall a. a -> [a] -> [a]
: [a]
notInf) [a]
inf [a]
ps

    infPos :: t -> [Pat] -> [t]
infPos t
i [] = []
    infPos t
i (PInferred Pat
p : [Pat]
ps) = t
i forall a. a -> [a] -> [a]
: t -> [Pat] -> [t]
infPos (t
i forall a. Num a => a -> a -> a
+ t
1) [Pat]
ps
    infPos t
i (Pat
_ : [Pat]
ps) = t -> [Pat] -> [t]
infPos (t
i forall a. Num a => a -> a -> a
+ t
1) [Pat]
ps

    deInf :: ([Pat], b) -> ([Pat], b)
deInf ([Pat]
pats, b
def) = (forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
deInfPat [Pat]
pats, b
def)

    deInfPat :: Pat -> Pat
deInfPat (PInferred Pat
p) = Pat
p
    deInfPat Pat
p = Pat
p

match :: [Name] -> [Clause] -> SC -- error case
                            -> CaseBuilder SC
match :: [Name] -> [Clause] -> SC -> CaseBuilder SC
match [] (([], (Term, Term)
ret) : [Clause]
xs) SC
err
    = do ([Term]
ts, Int
v, [(Name, Term)]
ntys) <- forall s (m :: * -> *). MonadState s m => m s
get
         forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
ts forall a. [a] -> [a] -> [a]
++ (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fstforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a b. (a, b) -> b
snd) [Clause]
xs), Int
v, [(Name, Term)]
ntys)
         case forall a b. (a, b) -> b
snd (Term, Term)
ret of
            Term
Impossible -> forall (m :: * -> *) a. Monad m => a -> m a
return forall t. SC' t
ImpossibleCase
            Term
tm -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. t -> SC' t
STerm Term
tm -- run out of arguments
match [Name]
vs [Clause]
cs SC
err = do let ([Name]
vs', [Clause]
de_inf) = [Name] -> [Clause] -> ([Name], [Clause])
orderByInf [Name]
vs [Clause]
cs
                         ps :: [Partition]
ps = [Clause] -> [Partition]
partition [Clause]
de_inf
                     [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture [Name]
vs' [Partition]
ps SC
err

mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture [Name]
vs [] SC
err = forall (m :: * -> *) a. Monad m => a -> m a
return SC
err
mixture [Name]
vs (Cons [Clause]
ms : [Partition]
ps) SC
err = do SC
fallthrough <- [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture [Name]
vs [Partition]
ps SC
err
                                   [Name] -> [Clause] -> SC -> CaseBuilder SC
conRule [Name]
vs [Clause]
ms SC
fallthrough
mixture [Name]
vs (Vars [Clause]
ms : [Partition]
ps) SC
err = do SC
fallthrough <- [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture [Name]
vs [Partition]
ps SC
err
                                   [Name] -> [Clause] -> SC -> CaseBuilder SC
varRule [Name]
vs [Clause]
ms SC
fallthrough

-- Return the list of inaccessible arguments of a data constructor.
inaccessibleArgs :: Name -> CaseBuilder [Int]
inaccessibleArgs :: Name -> CaseBuilder [Int]
inaccessibleArgs Name
n = do
    ErasureInfo
getInaccessiblePositions <- forall r (m :: * -> *). MonadReader r m => m r
ask  -- this function is the only thing in the environment
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ErasureInfo
getInaccessiblePositions Name
n

data ConType = CName Name Int -- named constructor
             | CFn Name -- reflected function name
             | CSuc -- n+1
             | CConst Const -- constant, not implemented yet
   deriving (Int -> ConType -> ShowS
[ConType] -> ShowS
ConType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConType] -> ShowS
$cshowList :: [ConType] -> ShowS
show :: ConType -> String
$cshow :: ConType -> String
showsPrec :: Int -> ConType -> ShowS
$cshowsPrec :: Int -> ConType -> ShowS
Show, ConType -> ConType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConType -> ConType -> Bool
$c/= :: ConType -> ConType -> Bool
== :: ConType -> ConType -> Bool
$c== :: ConType -> ConType -> Bool
Eq)

data Group = ConGroup Bool -- Uniqueness flag
                      ConType -- Constructor
                      [([Pat], Clause)] -- arguments and rest of alternative
   deriving Int -> Group -> ShowS
[Group] -> ShowS
Group -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Group] -> ShowS
$cshowList :: [Group] -> ShowS
show :: Group -> String
$cshow :: Group -> String
showsPrec :: Int -> Group -> ShowS
$cshowsPrec :: Int -> Group -> ShowS
Show

conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
conRule (Name
v:[Name]
vs) [Clause]
cs SC
err = do [Group]
groups <- [Clause] -> CaseBuilder [Group]
groupCons [Clause]
cs
                           [Name] -> [Group] -> SC -> CaseBuilder SC
caseGroups (Name
vforall a. a -> [a] -> [a]
:[Name]
vs) [Group]
groups SC
err

caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
caseGroups (Name
v:[Name]
vs) [Group]
gs SC
err = do [CaseAlt' Term]
g <- [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [Group]
gs
                              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case ([Group] -> CaseType
getShared [Group]
gs) Name
v (forall a. Ord a => [a] -> [a]
sort [CaseAlt' Term]
g)
  where
    getShared :: [Group] -> CaseType
getShared (ConGroup Bool
True ConType
_ [([Pat], Clause)]
_ : [Group]
_) = CaseType
Updatable
    getShared [Group]
_ = CaseType
Shared

    altGroups :: [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [] = forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. SC' t -> CaseAlt' t
DefaultCase SC
err]

    altGroups (ConGroup Bool
_ (CName Name
n Int
i) [([Pat], Clause)]
args : [Group]
cs)
        = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> Int
-> [([Pat], Clause)]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altGroup Name
n Int
i [([Pat], Clause)]
args forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [Group]
cs

    altGroups (ConGroup Bool
_ (CFn Name
n) [([Pat], Clause)]
args : [Group]
cs)
        = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> [([Pat], Clause)]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altFnGroup Name
n [([Pat], Clause)]
args forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [Group]
cs

    altGroups (ConGroup Bool
_ ConType
CSuc [([Pat], Clause)]
args : [Group]
cs)
        = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Pat], Clause)] -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altSucGroup [([Pat], Clause)]
args forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [Group]
cs

    altGroups (ConGroup Bool
_ (CConst Const
c) [([Pat], Clause)]
args : [Group]
cs)
        = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Const
-> [([Pat], Clause)]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altConstGroup Const
c [([Pat], Clause)]
args forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [Group]
cs

    altGroup :: Name
-> Int
-> [([Pat], Clause)]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altGroup Name
n Int
i [([Pat], Clause)]
args
         = do [Int]
inacc <- Name -> CaseBuilder [Int]
inaccessibleArgs Name
n
              ~([Name]
newVars, [Name]
accVars, [Name]
inaccVars, [Clause]
nextCs) <- [Int]
-> [([Pat], Clause)]
-> CaseBuilder ([Name], [Name], [Name], [Clause])
argsToAlt [Int]
inacc [([Pat], Clause)]
args
              SC
matchCs <- [Name] -> [Clause] -> SC -> CaseBuilder SC
match ([Name]
accVars forall a. [a] -> [a] -> [a]
++ [Name]
vs forall a. [a] -> [a] -> [a]
++ [Name]
inaccVars) [Clause]
nextCs SC
err
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
i [Name]
newVars SC
matchCs

    altFnGroup :: Name
-> [([Pat], Clause)]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altFnGroup Name
n [([Pat], Clause)]
args = do ~([Name]
newVars, [Name]
_, [], [Clause]
nextCs) <- [Int]
-> [([Pat], Clause)]
-> CaseBuilder ([Name], [Name], [Name], [Clause])
argsToAlt [] [([Pat], Clause)]
args
                           SC
matchCs <- [Name] -> [Clause] -> SC -> CaseBuilder SC
match ([Name]
newVars forall a. [a] -> [a] -> [a]
++ [Name]
vs) [Clause]
nextCs SC
err
                           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
newVars SC
matchCs

    altSucGroup :: [([Pat], Clause)] -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altSucGroup [([Pat], Clause)]
args = do ~([Name
newVar], [Name]
_, [], [Clause]
nextCs) <- [Int]
-> [([Pat], Clause)]
-> CaseBuilder ([Name], [Name], [Name], [Clause])
argsToAlt [] [([Pat], Clause)]
args
                          SC
matchCs <- [Name] -> [Clause] -> SC -> CaseBuilder SC
match (Name
newVarforall a. a -> [a] -> [a]
:[Name]
vs) [Clause]
nextCs SC
err
                          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
newVar SC
matchCs

    altConstGroup :: Const
-> [([Pat], Clause)]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altConstGroup Const
n [([Pat], Clause)]
args = do ~([Name]
_, [Name]
_, [], [Clause]
nextCs) <- [Int]
-> [([Pat], Clause)]
-> CaseBuilder ([Name], [Name], [Name], [Clause])
argsToAlt [] [([Pat], Clause)]
args
                              SC
matchCs <- [Name] -> [Clause] -> SC -> CaseBuilder SC
match [Name]
vs [Clause]
nextCs SC
err
                              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
n SC
matchCs

-- Returns:
--   * names of all variables arising from match
--   * names of accessible variables (subset of all variables)
--   * names of inaccessible variables (subset of all variables)
--   * clauses corresponding to (accVars ++ origVars ++ inaccVars)
argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
argsToAlt :: [Int]
-> [([Pat], Clause)]
-> CaseBuilder ([Name], [Name], [Name], [Clause])
argsToAlt [Int]
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], [], [])
argsToAlt [Int]
inacc rs :: [([Pat], Clause)]
rs@(([Pat]
r, Clause
m) : [([Pat], Clause)]
rest) = do
    [Name]
newVars <- [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
r
    let ([Name]
accVars, [Name]
inaccVars) = forall {a}. [a] -> ([a], [a])
partitionAcc [Name]
newVars
    forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
newVars, [Name]
accVars, [Name]
inaccVars, forall {a} {b}. [([a], ([a], b))] -> [([a], b)]
addRs [([Pat], Clause)]
rs)
  where
    -- Create names for new variables arising from the given patterns.
    getNewVars :: [Pat] -> CaseBuilder [Name]
    getNewVars :: [Pat] -> CaseBuilder [Name]
getNewVars [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    getNewVars ((PV Name
n Term
t) : [Pat]
ns) = do Name
v <- String -> CaseBuilder Name
getVar String
"e"
                                    [Name]
nsv <- [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns

                                    -- Record the type of the variable.
                                    --
                                    -- It seems that the ordering is not important
                                    -- and we can put (v,t) always in front of "ntys"
                                    -- (the varName-type pairs seem to represent a mapping).
                                    --
                                    -- The code that reads this is currently
                                    -- commented out, anyway.
                                    ([Term]
cs, Int
i, [(Name, Term)]
ntys) <- forall s (m :: * -> *). MonadState s m => m s
get
                                    forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
cs, Int
i, (Name
v, Term
t) forall a. a -> [a] -> [a]
: [(Name, Term)]
ntys)

                                    forall (m :: * -> *) a. Monad m => a -> m a
return (Name
v forall a. a -> [a] -> [a]
: [Name]
nsv)

    getNewVars (Pat
PAny   : [Pat]
ns) = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> CaseBuilder Name
getVar String
"i" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
    getNewVars (Pat
PTyPat : [Pat]
ns) = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> CaseBuilder Name
getVar String
"t" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
    getNewVars (Pat
_      : [Pat]
ns) = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> CaseBuilder Name
getVar String
"e" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns

    -- Partition a list of things into (accessible, inaccessible) things,
    -- according to the list of inaccessible indices.
    partitionAcc :: [a] -> ([a], [a])
partitionAcc [a]
xs =
        ( [a
x | (Int
i,a
x) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [a]
xs, Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
inacc]
        , [a
x | (Int
i,a
x) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [a]
xs, Int
i    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
inacc]
        )

    addRs :: [([a], ([a], b))] -> [([a], b)]
addRs [] = []
    addRs (([a]
r, ([a]
ps, b
res)) : [([a], ([a], b))]
rs) = (([a]
accforall a. [a] -> [a] -> [a]
++[a]
psforall a. [a] -> [a] -> [a]
++[a]
inacc, b
res) forall a. a -> [a] -> [a]
: [([a], ([a], b))] -> [([a], b)]
addRs [([a], ([a], b))]
rs)
      where
        ([a]
acc, [a]
inacc) = forall {a}. [a] -> ([a], [a])
partitionAcc [a]
r

getVar :: String -> CaseBuilder Name
getVar :: String -> CaseBuilder Name
getVar String
b = do ([Term]
t, Int
v, [(Name, Term)]
ntys) <- forall s (m :: * -> *). MonadState s m => m s
get; forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
t, Int
vforall a. Num a => a -> a -> a
+Int
1, [(Name, Term)]
ntys); forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> String -> Name
sMN Int
v String
b)

groupCons :: [Clause] -> CaseBuilder [Group]
groupCons :: [Clause] -> CaseBuilder [Group]
groupCons [Clause]
cs = forall {m :: * -> *}. Monad m => [Group] -> [Clause] -> m [Group]
gc [] [Clause]
cs
  where
    gc :: [Group] -> [Clause] -> m [Group]
gc [Group]
acc [] = forall (m :: * -> *) a. Monad m => a -> m a
return [Group]
acc
    gc [Group]
acc ((Pat
p : [Pat]
ps, (Term, Term)
res) : [Clause]
cs) =
        do [Group]
acc' <- forall {m :: * -> *}.
Monad m =>
Pat -> [Pat] -> (Term, Term) -> [Group] -> m [Group]
addGroup Pat
p [Pat]
ps (Term, Term)
res [Group]
acc
           [Group] -> [Clause] -> m [Group]
gc [Group]
acc' [Clause]
cs
    addGroup :: Pat -> [Pat] -> (Term, Term) -> [Group] -> m [Group]
addGroup Pat
p [Pat]
ps (Term, Term)
res [Group]
acc = case Pat
p of
        PCon Bool
uniq Name
con Int
i [Pat]
args -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> ConType -> [Pat] -> Clause -> [Group] -> [Group]
addg Bool
uniq (Name -> Int -> ConType
CName Name
con Int
i) [Pat]
args ([Pat]
ps, (Term, Term)
res) [Group]
acc
        PConst Const
cval -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Const -> Clause -> [Group] -> [Group]
addConG Const
cval ([Pat]
ps, (Term, Term)
res) [Group]
acc
        PSuc Pat
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> ConType -> [Pat] -> Clause -> [Group] -> [Group]
addg Bool
False ConType
CSuc [Pat
n] ([Pat]
ps, (Term, Term)
res) [Group]
acc
        PReflected Name
fn [Pat]
args -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> ConType -> [Pat] -> Clause -> [Group] -> [Group]
addg Bool
False (Name -> ConType
CFn Name
fn) [Pat]
args ([Pat]
ps, (Term, Term)
res) [Group]
acc
        Pat
pat -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Pat
pat forall a. [a] -> [a] -> [a]
++ String
" is not a constructor or constant (can't happen)"

    addg :: Bool -> ConType -> [Pat] -> Clause -> [Group] -> [Group]
addg Bool
uniq ConType
c [Pat]
conargs Clause
res []
           = [Bool -> ConType -> [([Pat], Clause)] -> Group
ConGroup Bool
uniq ConType
c [([Pat]
conargs, Clause
res)]]
    addg Bool
uniq ConType
c [Pat]
conargs Clause
res (g :: Group
g@(ConGroup Bool
_ ConType
c' [([Pat], Clause)]
cs):[Group]
gs)
        | ConType
c forall a. Eq a => a -> a -> Bool
== ConType
c' = Bool -> ConType -> [([Pat], Clause)] -> Group
ConGroup Bool
uniq ConType
c ([([Pat], Clause)]
cs forall a. [a] -> [a] -> [a]
++ [([Pat]
conargs, Clause
res)]) forall a. a -> [a] -> [a]
: [Group]
gs
        | Bool
otherwise = Group
g forall a. a -> [a] -> [a]
: Bool -> ConType -> [Pat] -> Clause -> [Group] -> [Group]
addg Bool
uniq ConType
c [Pat]
conargs Clause
res [Group]
gs

    addConG :: Const -> Clause -> [Group] -> [Group]
addConG Const
con Clause
res [] = [Bool -> ConType -> [([Pat], Clause)] -> Group
ConGroup Bool
False (Const -> ConType
CConst Const
con) [([], Clause
res)]]
    addConG Const
con Clause
res (g :: Group
g@(ConGroup Bool
False (CConst Const
n) [([Pat], Clause)]
cs) : [Group]
gs)
        | Const
con forall a. Eq a => a -> a -> Bool
== Const
n = Bool -> ConType -> [([Pat], Clause)] -> Group
ConGroup Bool
False (Const -> ConType
CConst Const
n) ([([Pat], Clause)]
cs forall a. [a] -> [a] -> [a]
++ [([], Clause
res)]) forall a. a -> [a] -> [a]
: [Group]
gs
--         | otherwise = g : addConG con res gs
    addConG Const
con Clause
res (Group
g : [Group]
gs) = Group
g forall a. a -> [a] -> [a]
: Const -> Clause -> [Group] -> [Group]
addConG Const
con Clause
res [Group]
gs

varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
varRule (Name
v : [Name]
vs) [Clause]
alts SC
err =
    do [Clause]
alts' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *} {a} {b} {a}.
MonadState (a, b, [(Name, Term)]) m =>
Name -> ([Pat], (a, Term)) -> m ([Pat], (a, Term))
repVar Name
v) [Clause]
alts
       [Name] -> [Clause] -> SC -> CaseBuilder SC
match [Name]
vs [Clause]
alts' SC
err
  where
    repVar :: Name -> ([Pat], (a, Term)) -> m ([Pat], (a, Term))
repVar Name
v (PV Name
p Term
ty : [Pat]
ps , (a
lhs, Term
res))
           = do (a
cs, b
i, [(Name, Term)]
ntys) <- forall s (m :: * -> *). MonadState s m => m s
get
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (a
cs, b
i, (Name
v, Term
ty) forall a. a -> [a] -> [a]
: [(Name, Term)]
ntys)
                forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a
lhs, forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
p (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
v Term
ty) Term
res))
    repVar Name
v (Pat
PAny : [Pat]
ps , (a, Term)
res) = forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a, Term)
res)
    repVar Name
v (Pat
PTyPat : [Pat]
ps , (a, Term)
res) = forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a, Term)
res)

-- fix: case e of S k -> f (S k)  ==> case e of S k -> f e

depatt :: [Name] -> SC -> SC
depatt :: [Name] -> SC -> SC
depatt [Name]
ns SC
tm = [(Name, (Name, [Name]))] -> SC -> SC
dp [] SC
tm
  where
    dp :: [(Name, (Name, [Name]))] -> SC -> SC
dp [(Name, (Name, [Name]))]
ms (STerm Term
tm) = forall t. t -> SC' t
STerm (forall {t}. Eq t => [(t, (t, [t]))] -> TT t -> TT t
applyMaps [(Name, (Name, [Name]))]
ms Term
tm)
    dp [(Name, (Name, [Name]))]
ms (Case CaseType
up Name
x [CaseAlt' Term]
alts) = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, (Name, [Name]))] -> Name -> CaseAlt' Term -> CaseAlt' Term
dpa [(Name, (Name, [Name]))]
ms Name
x) [CaseAlt' Term]
alts)
    dp [(Name, (Name, [Name]))]
ms SC
sc = SC
sc

    dpa :: [(Name, (Name, [Name]))] -> Name -> CaseAlt' Term -> CaseAlt' Term
dpa [(Name, (Name, [Name]))]
ms Name
x (ConCase Name
n Int
i [Name]
args SC
sc)
        = forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
n Int
i [Name]
args ([(Name, (Name, [Name]))] -> SC -> SC
dp ((Name
x, (Name
n, [Name]
args)) forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
ms) SC
sc)
    dpa [(Name, (Name, [Name]))]
ms Name
x (FnCase Name
n [Name]
args SC
sc)
        = forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
args ([(Name, (Name, [Name]))] -> SC -> SC
dp ((Name
x, (Name
n, [Name]
args)) forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
ms) SC
sc)
    dpa [(Name, (Name, [Name]))]
ms Name
x (ConstCase Const
c SC
sc) = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c ([(Name, (Name, [Name]))] -> SC -> SC
dp [(Name, (Name, [Name]))]
ms SC
sc)
    dpa [(Name, (Name, [Name]))]
ms Name
x (SucCase Name
n SC
sc) = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n ([(Name, (Name, [Name]))] -> SC -> SC
dp [(Name, (Name, [Name]))]
ms SC
sc)
    dpa [(Name, (Name, [Name]))]
ms Name
x (DefaultCase SC
sc) = forall t. SC' t -> CaseAlt' t
DefaultCase ([(Name, (Name, [Name]))] -> SC -> SC
dp [(Name, (Name, [Name]))]
ms SC
sc)

    applyMaps :: [(t, (t, [t]))] -> TT t -> TT t
applyMaps [(t, (t, [t]))]
ms f :: TT t
f@(App AppStatus t
_ TT t
_ TT t
_)
       | (P NameType
nt t
cn TT t
pty, [TT t]
args) <- forall n. TT n -> (TT n, [TT n])
unApply TT t
f
            = let args' :: [TT t]
args' = forall a b. (a -> b) -> [a] -> [b]
map ([(t, (t, [t]))] -> TT t -> TT t
applyMaps [(t, (t, [t]))]
ms) [TT t]
args in
                  forall {t}.
Eq t =>
[(t, (t, [t]))] -> NameType -> t -> TT t -> [TT t] -> TT t
applyMap [(t, (t, [t]))]
ms NameType
nt t
cn TT t
pty [TT t]
args'
        where
          applyMap :: [(t, (t, [t]))] -> NameType -> t -> TT t -> [TT t] -> TT t
applyMap [] NameType
nt t
cn TT t
pty [TT t]
args' = forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
nt t
cn TT t
pty) [TT t]
args'
          applyMap ((t
x, (t
n, [t]
args)) : [(t, (t, [t]))]
ms) NameType
nt t
cn TT t
pty [TT t]
args'
            | forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
args forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT t]
args') forall a. a -> [a] -> [a]
:
                     (t
n forall a. Eq a => a -> a -> Bool
== t
cn) forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall n. Eq n => n -> TT n -> Bool
same [t]
args [TT t]
args') = forall n. NameType -> n -> TT n -> TT n
P NameType
Ref t
x forall n. TT n
Erased
            | Bool
otherwise = [(t, (t, [t]))] -> NameType -> t -> TT t -> [TT t] -> TT t
applyMap [(t, (t, [t]))]
ms NameType
nt t
cn TT t
pty [TT t]
args'
          same :: a -> TT a -> Bool
same a
n (P NameType
_ a
n' TT a
_) = a
n forall a. Eq a => a -> a -> Bool
== a
n'
          same a
_ TT a
_ = Bool
False

    applyMaps [(t, (t, [t]))]
ms (App AppStatus t
s TT t
f TT t
a) = forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus t
s ([(t, (t, [t]))] -> TT t -> TT t
applyMaps [(t, (t, [t]))]
ms TT t
f) ([(t, (t, [t]))] -> TT t -> TT t
applyMaps [(t, (t, [t]))]
ms TT t
a)
    applyMaps [(t, (t, [t]))]
ms TT t
t = TT t
t

-- FIXME: Do this for SucCase too
-- Issue #1719 on the issue tracker:  https://github.com/idris-lang/Idris-dev/issues/1719
prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)
      -> SC -> SC
prune :: Bool -> SC -> SC
prune Bool
proj (Case CaseType
up Name
n [CaseAlt' Term]
alts) = case [CaseAlt' Term]
alts' of
    [] -> forall t. SC' t
ImpossibleCase

    -- Projection transformations prevent us from seeing some uses of ctor fields
    -- because they delete information about which ctor is being used.
    -- Consider:
    --   f (X x) = ...  x  ...
    -- vs.
    --   f  x    = ... x!0 ...
    --
    -- Hence, we disable this step.
    -- TODO: re-enable this in toIR
    --
    -- as@[ConCase cn i args sc]
    --     | proj -> mkProj n 0 args (prune proj sc)
    -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs

    -- If none of the args are used in the sc, however, we can just replace it
    -- with sc
    as :: [CaseAlt' Term]
as@[ConCase Name
cn Int
i [Name]
args SC
sc]
        | Bool
proj -> let sc' :: SC
sc' = Bool -> SC -> SC
prune Bool
proj SC
sc in
                      if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SC -> Name -> Bool
isUsed SC
sc') [Name]
args
                         then forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
i [Name]
args SC
sc']
                         else SC
sc'

    [SucCase Name
cn SC
sc]
        | Bool
proj
        -> Name -> Name -> Int -> SC -> SC
projRep Name
cn Name
n (-Int
1) forall a b. (a -> b) -> a -> b
$ Bool -> SC -> SC
prune Bool
proj SC
sc

    [ConstCase Const
_ SC
sc]
        -> Bool -> SC -> SC
prune Bool
proj SC
sc

    -- Bit of a hack here! The default case will always be 0, make sure
    -- it gets caught first.
    [s :: CaseAlt' Term
s@(SucCase Name
_ SC
_), DefaultCase SC
dc]
        -> forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [forall t. Const -> SC' t -> CaseAlt' t
ConstCase (Integer -> Const
BI Integer
0) SC
dc, CaseAlt' Term
s]

    [CaseAlt' Term]
as  -> forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [CaseAlt' Term]
as
  where
    alts' :: [CaseAlt' Term]
alts' = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {n}. CaseAlt' (TT n) -> Bool
erased) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map CaseAlt' Term -> CaseAlt' Term
pruneAlt [CaseAlt' Term]
alts

    pruneAlt :: CaseAlt' Term -> CaseAlt' Term
pruneAlt (ConCase Name
cn Int
i [Name]
ns SC
sc) = forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
i [Name]
ns (Bool -> SC -> SC
prune Bool
proj SC
sc)
    pruneAlt (FnCase Name
cn [Name]
ns SC
sc) = forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
cn [Name]
ns (Bool -> SC -> SC
prune Bool
proj SC
sc)
    pruneAlt (ConstCase Const
c SC
sc) = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c (Bool -> SC -> SC
prune Bool
proj SC
sc)
    pruneAlt (SucCase Name
n SC
sc) = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n (Bool -> SC -> SC
prune Bool
proj SC
sc)
    pruneAlt (DefaultCase SC
sc) = forall t. SC' t -> CaseAlt' t
DefaultCase (Bool -> SC -> SC
prune Bool
proj SC
sc)

    erased :: CaseAlt' (TT n) -> Bool
erased (DefaultCase (STerm TT n
Erased)) = Bool
True
    erased (DefaultCase SC' (TT n)
ImpossibleCase) = Bool
True
    erased CaseAlt' (TT n)
_ = Bool
False

    projRep :: Name -> Name -> Int -> SC -> SC
    projRep :: Name -> Name -> Int -> SC -> SC
projRep Name
arg Name
n Int
i (Case CaseType
up Name
x [CaseAlt' Term]
alts) | Name
x forall a. Eq a => a -> a -> Bool
== Name
arg
        = forall t. t -> [CaseAlt' t] -> SC' t
ProjCase (forall n. TT n -> Int -> TT n
Proj (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) Int
i) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> Int -> CaseAlt' Term -> CaseAlt' Term
projRepAlt Name
arg Name
n Int
i) [CaseAlt' Term]
alts
    projRep Name
arg Name
n Int
i (Case CaseType
up Name
x [CaseAlt' Term]
alts)
        = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x (forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> Int -> CaseAlt' Term -> CaseAlt' Term
projRepAlt Name
arg Name
n Int
i) [CaseAlt' Term]
alts)
    projRep Name
arg Name
n Int
i (ProjCase Term
t [CaseAlt' Term]
alts)
        = forall t. t -> [CaseAlt' t] -> SC' t
ProjCase (forall {n}. Eq n => n -> n -> Int -> TT n -> TT n
projRepTm Name
arg Name
n Int
i Term
t) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> Int -> CaseAlt' Term -> CaseAlt' Term
projRepAlt Name
arg Name
n Int
i) [CaseAlt' Term]
alts
    projRep Name
arg Name
n Int
i (STerm Term
t) = forall t. t -> SC' t
STerm (forall {n}. Eq n => n -> n -> Int -> TT n -> TT n
projRepTm Name
arg Name
n Int
i Term
t)
    projRep Name
arg Name
n Int
i SC
c = SC
c

    projRepAlt :: Name -> Name -> Int -> CaseAlt' Term -> CaseAlt' Term
projRepAlt Name
arg Name
n Int
i (ConCase Name
cn Int
t [Name]
args SC
rhs)
        = forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
t [Name]
args (Name -> Name -> Int -> SC -> SC
projRep Name
arg Name
n Int
i SC
rhs)
    projRepAlt Name
arg Name
n Int
i (FnCase Name
cn [Name]
args SC
rhs)
        = forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
cn [Name]
args (Name -> Name -> Int -> SC -> SC
projRep Name
arg Name
n Int
i SC
rhs)
    projRepAlt Name
arg Name
n Int
i (ConstCase Const
t SC
rhs)
        = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
t (Name -> Name -> Int -> SC -> SC
projRep Name
arg Name
n Int
i SC
rhs)
    projRepAlt Name
arg Name
n Int
i (SucCase Name
sn SC
rhs)
        = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
sn (Name -> Name -> Int -> SC -> SC
projRep Name
arg Name
n Int
i SC
rhs)
    projRepAlt Name
arg Name
n Int
i (DefaultCase SC
rhs)
        = forall t. SC' t -> CaseAlt' t
DefaultCase (Name -> Name -> Int -> SC -> SC
projRep Name
arg Name
n Int
i SC
rhs)

    projRepTm :: n -> n -> Int -> TT n -> TT n
projRepTm n
arg n
n Int
i TT n
t = forall n. Eq n => n -> TT n -> TT n -> TT n
subst n
arg (forall n. TT n -> Int -> TT n
Proj (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n forall n. TT n
Erased) Int
i) TT n
t

prune Bool
_ SC
t = SC
t

-- Remove any branches we can't reach because of variables we've already
-- tested
removeUnreachable :: SC -> SC
removeUnreachable :: SC -> SC
removeUnreachable SC
sc = [(Name, Int)] -> SC -> SC
ru [] SC
sc
  where
    -- keep a mapping from variable names, to the constructor tag we've
    -- already checked it as in this branch
    ru :: [(Name, Int)] -> SC -> SC
    ru :: [(Name, Int)] -> SC -> SC
ru [(Name, Int)]
checked (Case CaseType
t Name
n [CaseAlt' Term]
alts)
        = let alts' :: [CaseAlt' Term]
alts' = forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Int)] -> Name -> CaseAlt' Term -> CaseAlt' Term
ruAlt [(Name, Int)]
checked Name
n) (forall {t}. Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
checked) [CaseAlt' Term]
alts) in
              forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
n [CaseAlt' Term]
alts'
    ru [(Name, Int)]
checked SC
t = SC
t

    dropImpossible :: Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible Maybe Int
Nothing [CaseAlt' t]
alts = [CaseAlt' t]
alts
    dropImpossible (Just Int
t) [] = []
    dropImpossible (Just Int
t) (ConCase Name
con Int
tag [Name]
args SC' t
sc : [CaseAlt' t]
rest)
        | Int
t forall a. Eq a => a -> a -> Bool
== Int
tag = [forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
con Int
tag [Name]
args SC' t
sc] -- must be this case
        | Bool
otherwise = Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (forall a. a -> Maybe a
Just Int
t) [CaseAlt' t]
rest -- can't be this case
    dropImpossible (Just Int
t) (CaseAlt' t
c : [CaseAlt' t]
rest)
        = CaseAlt' t
c forall a. a -> [a] -> [a]
: Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (forall a. a -> Maybe a
Just Int
t) [CaseAlt' t]
rest

    ruAlt :: [(Name, Int)] -> Name -> CaseAlt -> CaseAlt
    ruAlt :: [(Name, Int)] -> Name -> CaseAlt' Term -> CaseAlt' Term
ruAlt [(Name, Int)]
checked Name
var (ConCase Name
con Int
tag [Name]
args SC
sc)
        = let checked' :: [(Name, Int)]
checked' = [Name] -> [(Name, Int)] -> [(Name, Int)]
dropChecked [Name]
args (Name -> Int -> [(Name, Int)] -> [(Name, Int)]
updateChecked Name
var Int
tag [(Name, Int)]
checked)
              sc' :: SC
sc' = [(Name, Int)] -> SC -> SC
ru [(Name, Int)]
checked' SC
sc in
              forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
con Int
tag [Name]
args SC
sc'
    ruAlt [(Name, Int)]
checked Name
var (FnCase Name
n [Name]
args SC
sc)
        = let checked' :: [(Name, Int)]
checked' = [Name] -> [(Name, Int)] -> [(Name, Int)]
dropChecked [Name
var] [(Name, Int)]
checked
              sc' :: SC
sc' = [(Name, Int)] -> SC -> SC
ru [(Name, Int)]
checked' SC
sc in
              forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
n [Name]
args SC
sc'
    ruAlt [(Name, Int)]
checked Name
var (ConstCase Const
c SC
sc)
        = let checked' :: [(Name, Int)]
checked' = [Name] -> [(Name, Int)] -> [(Name, Int)]
dropChecked [Name
var] [(Name, Int)]
checked
              sc' :: SC
sc' = [(Name, Int)] -> SC -> SC
ru [(Name, Int)]
checked' SC
sc in
              forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c SC
sc'
    ruAlt [(Name, Int)]
checked Name
var (SucCase Name
n SC
sc)
        = let checked' :: [(Name, Int)]
checked' = [Name] -> [(Name, Int)] -> [(Name, Int)]
dropChecked [Name
var] [(Name, Int)]
checked
              sc' :: SC
sc' = [(Name, Int)] -> SC -> SC
ru [(Name, Int)]
checked' SC
sc in
              forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n SC
sc'
    ruAlt [(Name, Int)]
checked Name
var (DefaultCase SC
sc)
        = let checked' :: [(Name, Int)]
checked' = [Name] -> [(Name, Int)] -> [(Name, Int)]
dropChecked [Name
var] [(Name, Int)]
checked
              sc' :: SC
sc' = [(Name, Int)] -> SC -> SC
ru [(Name, Int)]
checked' SC
sc in
              forall t. SC' t -> CaseAlt' t
DefaultCase SC
sc'

    updateChecked :: Name -> Int -> [(Name, Int)] -> [(Name, Int)]
    updateChecked :: Name -> Int -> [(Name, Int)] -> [(Name, Int)]
updateChecked Name
n Int
i [(Name, Int)]
checked
        = (Name
n, Int
i) forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, Int)
x -> forall a b. (a, b) -> a
fst (Name, Int)
x forall a. Eq a => a -> a -> Bool
/= Name
n) [(Name, Int)]
checked

    dropChecked :: [Name] -> [(Name, Int)] -> [(Name, Int)]
    dropChecked :: [Name] -> [(Name, Int)] -> [(Name, Int)]
dropChecked [Name]
ns [(Name, Int)]
checked = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, Int)
x -> forall a b. (a, b) -> a
fst (Name, Int)
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
ns) [(Name, Int)]
checked

stripLambdas :: CaseDef -> CaseDef
stripLambdas :: CaseDef -> CaseDef
stripLambdas (CaseDef [Name]
ns (STerm (Bind Name
x (Lam RigCount
_ Term
_) Term
sc)) [Term]
tm)
    = CaseDef -> CaseDef
stripLambdas ([Name] -> SC -> [Term] -> CaseDef
CaseDef ([Name]
ns forall a. [a] -> [a] -> [a]
++ [Name
x]) (forall t. t -> SC' t
STerm (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x forall n. TT n
Erased) Term
sc)) [Term]
tm)
stripLambdas CaseDef
x = CaseDef
x

substSC :: Name -> Name -> SC -> SC
substSC :: Name -> Name -> SC -> SC
substSC Name
n Name
repl (Case CaseType
up Name
n' [CaseAlt' Term]
alts)
    | Name
n forall a. Eq a => a -> a -> Bool
== Name
n'   = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
repl (forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' Term -> CaseAlt' Term
substAlt Name
n Name
repl) [CaseAlt' Term]
alts)
    | Bool
otherwise = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n'   (forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' Term -> CaseAlt' Term
substAlt Name
n Name
repl) [CaseAlt' Term]
alts)
substSC Name
n Name
repl (STerm Term
t) = forall t. t -> SC' t
STerm forall a b. (a -> b) -> a -> b
$ forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
repl forall n. TT n
Erased) Term
t
substSC Name
n Name
repl (UnmatchedCase String
errmsg) = forall t. String -> SC' t
UnmatchedCase String
errmsg
substSC Name
n Name
repl  SC
ImpossibleCase = forall t. SC' t
ImpossibleCase
substSC Name
n Name
repl SC
sc = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"unsupported in substSC: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SC
sc

substAlt :: Name -> Name -> CaseAlt -> CaseAlt
substAlt :: Name -> Name -> CaseAlt' Term -> CaseAlt' Term
substAlt Name
n Name
repl (ConCase Name
cn Int
a [Name]
ns SC
sc) = forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
a [Name]
ns (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)
substAlt Name
n Name
repl (FnCase Name
fn [Name]
ns SC
sc)    = forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
fn [Name]
ns (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)
substAlt Name
n Name
repl (ConstCase Const
c SC
sc)     = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)
substAlt Name
n Name
repl (SucCase Name
n' SC
sc)
    | Name
n forall a. Eq a => a -> a -> Bool
== Name
n'   = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n  (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)
    | Bool
otherwise = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n' (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)
substAlt Name
n Name
repl (DefaultCase SC
sc)     = forall t. SC' t -> CaseAlt' t
DefaultCase (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)

-- mkForce n' n t updates the tree t under the assumption that
-- n' = force n (so basically updating n to n')
mkForce :: Name -> Name -> SC -> SC
mkForce :: Name -> Name -> SC -> SC
mkForce = forall {t}. Name -> Name -> SC' t -> SC' t
mkForceSC
  where
    mkForceSC :: Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg (Case CaseType
up Name
x [CaseAlt' t]
alts) | Name
x forall a. Eq a => a -> a -> Bool
== Name
arg
        = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' t -> CaseAlt' t
mkForceAlt Name
n Name
arg) [CaseAlt' t]
alts

    mkForceSC Name
n Name
arg (Case CaseType
up Name
x [CaseAlt' t]
alts)
        = forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x (forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' t -> CaseAlt' t
mkForceAlt Name
n Name
arg) [CaseAlt' t]
alts)

    mkForceSC Name
n Name
arg (ProjCase t
t [CaseAlt' t]
alts)
        = forall t. t -> [CaseAlt' t] -> SC' t
ProjCase t
t forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' t -> CaseAlt' t
mkForceAlt Name
n Name
arg) [CaseAlt' t]
alts

    mkForceSC Name
n Name
arg SC' t
c = SC' t
c

    mkForceAlt :: Name -> Name -> CaseAlt' t -> CaseAlt' t
mkForceAlt Name
n Name
arg (ConCase Name
cn Int
t [Name]
args SC' t
rhs)
        = forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
t [Name]
args (Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg SC' t
rhs)
    mkForceAlt Name
n Name
arg (FnCase Name
cn [Name]
args SC' t
rhs)
        = forall t. Name -> [Name] -> SC' t -> CaseAlt' t
FnCase Name
cn [Name]
args (Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg SC' t
rhs)
    mkForceAlt Name
n Name
arg (ConstCase Const
t SC' t
rhs)
        = forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
t (Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg SC' t
rhs)
    mkForceAlt Name
n Name
arg (SucCase Name
sn SC' t
rhs)
        = forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
sn (Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg SC' t
rhs)
    mkForceAlt Name
n Name
arg (DefaultCase SC' t
rhs)
        = forall t. SC' t -> CaseAlt' t
DefaultCase (Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg SC' t
rhs)