{-# 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]
| ProjCase t [CaseAlt' t]
| STerm !t
| UnmatchedCase String
| ImpossibleCase
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)
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)
| 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)
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
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
_ = []
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
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
| (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
| (P NameType
Ref Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn = []
| (P (TCon Int
_ Int
_) Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
fn = []
| 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
_ = []
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
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]
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]
| 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)
simpleCase :: Bool -> SC -> Bool ->
Phase -> FC ->
[Int] ->
[(Type, Bool)] ->
[([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
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
| PReflected Name [Pat]
| PAny
| PTyPat
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
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
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
order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
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)
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)))
([[((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
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
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
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
-> 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
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
inaccessibleArgs :: Name -> CaseBuilder [Int]
inaccessibleArgs :: Name -> CaseBuilder [Int]
inaccessibleArgs Name
n = do
ErasureInfo
getInaccessiblePositions <- forall r (m :: * -> *). MonadReader r m => m r
ask
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
| CFn Name
| CSuc
| CConst Const
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
ConType
[([Pat], Clause)]
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
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
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
([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
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
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)
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
prune :: Bool
-> 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
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
[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
removeUnreachable :: SC -> SC
removeUnreachable :: SC -> SC
removeUnreachable SC
sc = [(Name, Int)] -> SC -> SC
ru [] SC
sc
where
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]
| Bool
otherwise = Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (forall a. a -> Maybe a
Just Int
t) [CaseAlt' t]
rest
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 :: 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)