{-# 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
(Int -> CaseDef -> ShowS)
-> (CaseDef -> String) -> ([CaseDef] -> ShowS) -> Show CaseDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CaseDef -> ShowS
showsPrec :: Int -> CaseDef -> ShowS
$cshow :: CaseDef -> String
show :: CaseDef -> String
$cshowList :: [CaseDef] -> ShowS
showList :: [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
(SC' t -> SC' t -> Bool) -> (SC' t -> SC' t -> Bool) -> Eq (SC' t)
forall t. Eq t => SC' t -> SC' t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: SC' t -> SC' t -> Bool
Eq, Eq (SC' t)
Eq (SC' t) =>
(SC' t -> SC' t -> Ordering)
-> (SC' t -> SC' t -> Bool)
-> (SC' t -> SC' t -> Bool)
-> (SC' t -> SC' t -> Bool)
-> (SC' t -> SC' t -> Bool)
-> (SC' t -> SC' t -> SC' t)
-> (SC' t -> SC' t -> SC' t)
-> Ord (SC' t)
SC' t -> SC' t -> Bool
SC' t -> SC' t -> Ordering
SC' t -> SC' t -> SC' t
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
$ccompare :: forall t. Ord t => SC' t -> SC' t -> Ordering
compare :: SC' t -> SC' t -> Ordering
$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
>= :: SC' t -> SC' t -> Bool
$cmax :: forall t. Ord t => SC' t -> SC' t -> SC' t
max :: SC' t -> SC' t -> SC' t
$cmin :: forall t. Ord t => SC' t -> SC' t -> SC' t
min :: SC' t -> SC' t -> SC' t
Ord, (forall a b. (a -> b) -> SC' a -> SC' b)
-> (forall a b. a -> SC' b -> SC' a) -> Functor SC'
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
$cfmap :: forall a b. (a -> b) -> SC' a -> SC' b
fmap :: forall a b. (a -> b) -> SC' a -> SC' b
$c<$ :: forall a b. a -> SC' b -> SC' a
<$ :: forall a b. a -> SC' b -> SC' a
Functor, (forall x. SC' t -> Rep (SC' t) x)
-> (forall x. Rep (SC' t) x -> SC' t) -> Generic (SC' t)
forall x. Rep (SC' t) x -> SC' t
forall x. SC' t -> Rep (SC' t) x
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
$cfrom :: forall t x. SC' t -> Rep (SC' t) x
from :: forall x. SC' t -> Rep (SC' t) x
$cto :: forall t x. Rep (SC' t) x -> SC' t
to :: forall x. Rep (SC' t) x -> SC' t
Generic)
data CaseType = Updatable | Shared
deriving (CaseType -> CaseType -> Bool
(CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool) -> Eq CaseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CaseType -> CaseType -> Bool
== :: CaseType -> CaseType -> Bool
$c/= :: CaseType -> CaseType -> Bool
/= :: CaseType -> CaseType -> Bool
Eq, Eq CaseType
Eq CaseType =>
(CaseType -> CaseType -> Ordering)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> CaseType)
-> (CaseType -> CaseType -> CaseType)
-> Ord CaseType
CaseType -> CaseType -> Bool
CaseType -> CaseType -> Ordering
CaseType -> CaseType -> CaseType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CaseType -> CaseType -> Ordering
compare :: CaseType -> CaseType -> Ordering
$c< :: CaseType -> CaseType -> Bool
< :: CaseType -> CaseType -> Bool
$c<= :: CaseType -> CaseType -> Bool
<= :: CaseType -> CaseType -> Bool
$c> :: CaseType -> CaseType -> Bool
> :: CaseType -> CaseType -> Bool
$c>= :: CaseType -> CaseType -> Bool
>= :: CaseType -> CaseType -> Bool
$cmax :: CaseType -> CaseType -> CaseType
max :: CaseType -> CaseType -> CaseType
$cmin :: CaseType -> CaseType -> CaseType
min :: CaseType -> CaseType -> CaseType
Ord, Int -> CaseType -> ShowS
[CaseType] -> ShowS
CaseType -> String
(Int -> CaseType -> ShowS)
-> (CaseType -> String) -> ([CaseType] -> ShowS) -> Show CaseType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CaseType -> ShowS
showsPrec :: Int -> CaseType -> ShowS
$cshow :: CaseType -> String
show :: CaseType -> String
$cshowList :: [CaseType] -> ShowS
showList :: [CaseType] -> ShowS
Show, (forall x. CaseType -> Rep CaseType x)
-> (forall x. Rep CaseType x -> CaseType) -> Generic CaseType
forall x. Rep CaseType x -> CaseType
forall x. CaseType -> Rep CaseType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseType -> Rep CaseType x
from :: forall x. CaseType -> Rep CaseType x
$cto :: forall x. Rep CaseType x -> CaseType
to :: forall x. Rep CaseType x -> CaseType
Generic)
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
[CaseAlt' t] -> ShowS
CaseAlt' t -> String
(Int -> CaseAlt' t -> ShowS)
-> (CaseAlt' t -> String)
-> ([CaseAlt' t] -> ShowS)
-> Show (CaseAlt' t)
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
$cshowsPrec :: forall t. Show t => Int -> CaseAlt' t -> ShowS
showsPrec :: Int -> CaseAlt' t -> ShowS
$cshow :: forall t. Show t => CaseAlt' t -> String
show :: CaseAlt' t -> String
$cshowList :: forall t. Show t => [CaseAlt' t] -> ShowS
showList :: [CaseAlt' t] -> ShowS
Show, CaseAlt' t -> CaseAlt' t -> Bool
(CaseAlt' t -> CaseAlt' t -> Bool)
-> (CaseAlt' t -> CaseAlt' t -> Bool) -> Eq (CaseAlt' t)
forall t. Eq t => CaseAlt' t -> CaseAlt' t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: CaseAlt' t -> CaseAlt' t -> Bool
Eq, Eq (CaseAlt' t)
Eq (CaseAlt' t) =>
(CaseAlt' t -> CaseAlt' t -> Ordering)
-> (CaseAlt' t -> CaseAlt' t -> Bool)
-> (CaseAlt' t -> CaseAlt' t -> Bool)
-> (CaseAlt' t -> CaseAlt' t -> Bool)
-> (CaseAlt' t -> CaseAlt' t -> Bool)
-> (CaseAlt' t -> CaseAlt' t -> CaseAlt' t)
-> (CaseAlt' t -> CaseAlt' t -> CaseAlt' t)
-> Ord (CaseAlt' t)
CaseAlt' t -> CaseAlt' t -> Bool
CaseAlt' t -> CaseAlt' t -> Ordering
CaseAlt' t -> CaseAlt' t -> CaseAlt' t
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
$ccompare :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Ordering
compare :: CaseAlt' t -> CaseAlt' t -> Ordering
$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
>= :: CaseAlt' t -> CaseAlt' t -> Bool
$cmax :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
max :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t
$cmin :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
min :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t
Ord, (forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b)
-> (forall a b. a -> CaseAlt' b -> CaseAlt' a) -> Functor CaseAlt'
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
$cfmap :: forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b
fmap :: forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b
$c<$ :: forall a b. a -> CaseAlt' b -> CaseAlt' a
<$ :: forall a b. a -> CaseAlt' b -> CaseAlt' a
Functor, (forall x. CaseAlt' t -> Rep (CaseAlt' t) x)
-> (forall x. Rep (CaseAlt' t) x -> CaseAlt' t)
-> Generic (CaseAlt' t)
forall x. Rep (CaseAlt' t) x -> CaseAlt' t
forall x. CaseAlt' t -> Rep (CaseAlt' t) x
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
$cfrom :: forall t x. CaseAlt' t -> Rep (CaseAlt' t) x
from :: forall x. CaseAlt' t -> Rep (CaseAlt' t) x
$cto :: forall t x. Rep (CaseAlt' t) x -> CaseAlt' t
to :: forall x. Rep (CaseAlt' t) x -> CaseAlt' t
Generic)
type CaseAlt = CaseAlt' Term
instance Show t => Show (SC' t) where
show :: SC' t -> String
show SC' t
sc = Int -> SC' t -> String
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" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
u String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
indent Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep (String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
indent Int
i) ((CaseAlt' a -> String) -> [CaseAlt' a] -> [String]
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
tm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" of " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep (String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
indent Int
i) ((CaseAlt' a -> String) -> [CaseAlt' a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> CaseAlt' a -> String
showA Int
i) [CaseAlt' a]
alts)
show' Int
i (STerm a
tm) = a -> String
forall a. Show a => a -> String
show a
tm
show' Int
i (UnmatchedCase String
str) = String
"error " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
str
show' Int
i SC' a
ImpossibleCase = String
"impossible"
indent :: Int -> String
indent Int
i = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
i (String -> [String]
forall a. a -> [a]
repeat String
" ")
showA :: Int -> CaseAlt' a -> String
showA Int
i (ConCase Name
n Int
t [Name]
args SC' a
sc)
= Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep (String
", ") ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
forall a. Show a => a -> String
show [Name]
args) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") => "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SC' a
sc
showA Int
i (FnCase Name
n [Name]
args SC' a
sc)
= String
"FN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep (String
", ") ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
forall a. Show a => a -> String
show [Name]
args) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") => "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SC' a
sc
showA Int
i (ConstCase Const
t SC' a
sc)
= Const -> String
forall a. Show a => a -> String
show Const
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SC' a
sc
showA Int
i (SucCase Name
n SC' a
sc)
= Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"+1 => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) SC' a
sc
showA Int
i (DefaultCase SC' a
sc)
= String
"_ => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall 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) = Name -> [CaseAlt' Term] -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n [CaseAlt' Term]
as
termsize Name
n (ProjCase Term
n' [CaseAlt' Term]
as) = Name -> [CaseAlt' Term] -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n [CaseAlt' Term]
as
termsize Name
n (STerm Term
t) = Name -> Term -> Int
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) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize Name
n (FnCase Name
_ [Name]
_ SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize Name
n (ConstCase Const
_ SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize Name
n (SucCase Name
_ SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize Name
n (DefaultCase SC
s) = Name -> SC -> Int
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 = SC -> [Name] -> [Name]
forall {t :: * -> *}. Foldable t => SC -> t Name -> [Name]
findAllUsedArgs SC
t [Name]
args in
[Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub [Name]
as) Bool -> Bool -> Bool
&&
Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
20
namesUsed :: SC -> [Name]
namesUsed :: SC -> [Name]
namesUsed SC
sc = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
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) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ((CaseAlt' Term -> [Name]) -> [CaseAlt' Term] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Name] -> CaseAlt' Term -> [Name]
nua [Name]
ps) [CaseAlt' Term]
alts) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n]
nu' [Name]
ps (ProjCase Term
t [CaseAlt' Term]
alts) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> [Name]
forall {a}. Eq a => [a] -> TT a -> [a]
nut [Name]
ps Term
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (CaseAlt' Term -> [Name]) -> [CaseAlt' Term] -> [Name]
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) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> [Name]
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) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> SC -> [Name]
nu' ([Name]
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
args
nua [Name]
ps (FnCase Name
n [Name]
args SC
sc) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> SC -> [Name]
nu' ([Name]
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc) [Name] -> [Name] -> [Name]
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 a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 [a] -> [a] -> [a]
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 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a] -> TT a -> [a]
nut (a
na -> [a] -> [a]
forall 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
na -> [a] -> [a]
forall 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 = Set (Name, [[Name]]) -> [(Name, [[Name]])]
forall a. Set a -> [a]
S.toList (Set (Name, [[Name]]) -> [(Name, [[Name]])])
-> Set (Name, [[Name]]) -> [(Name, [[Name]])]
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) = [Set (Name, [[Name]])] -> Set (Name, [[Name]])
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (Name, [[Name]])] -> Set (Name, [[Name]]))
-> [Set (Name, [[Name]])] -> Set (Name, [[Name]])
forall a b. (a -> b) -> a -> b
$ (CaseAlt' Term -> Set (Name, [[Name]]))
-> [CaseAlt' Term] -> [Set (Name, [[Name]])]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> CaseAlt' Term -> Set (Name, [[Name]])
nua (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
ps)) [CaseAlt' Term]
alts
nu' [Name]
ps (ProjCase Term
t [CaseAlt' Term]
alts) = [Set (Name, [[Name]])] -> Set (Name, [[Name]])
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (Name, [[Name]])] -> Set (Name, [[Name]]))
-> [Set (Name, [[Name]])] -> Set (Name, [[Name]])
forall a b. (a -> b) -> a -> b
$ [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
t Set (Name, [[Name]])
-> [Set (Name, [[Name]])] -> [Set (Name, [[Name]])]
forall a. a -> [a] -> [a]
: (CaseAlt' Term -> Set (Name, [[Name]]))
-> [CaseAlt' Term] -> [Set (Name, [[Name]])]
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
_ = Set (Name, [[Name]])
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 [Name] -> [Name] -> [Name]
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 [Name] -> [Name] -> [Name]
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ps = Set (Name, [[Name]])
forall a. Set a
S.empty
| Bool
otherwise = (Name, [[Name]]) -> Set (Name, [[Name]])
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn
= if Bool
ignoreasserts Bool -> Bool -> Bool
&& Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"assert_total"
then Set (Name, [[Name]])
forall a. Set a
S.empty
else if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ps
then Set (Name, [[Name]])
-> Set (Name, [[Name]]) -> Set (Name, [[Name]])
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 (Name, [[Name]]) -> Set (Name, [[Name]]) -> Set (Name, [[Name]])
forall a. Ord a => a -> Set a -> Set a
S.insert (Name
n, (Term -> [Name]) -> [Term] -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map Term -> [Name]
argNames [Term]
args)
([Set (Name, [[Name]])] -> Set (Name, [[Name]])
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (Name, [[Name]])] -> Set (Name, [[Name]]))
-> [Set (Name, [[Name]])] -> Set (Name, [[Name]])
forall a b. (a -> b) -> a -> b
$ (Term -> Set (Name, [[Name]])) -> [Term] -> [Set (Name, [[Name]])]
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]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn = Set (Name, [[Name]])
forall a. Set a
S.empty
| Bool
otherwise = Set (Name, [[Name]])
-> Set (Name, [[Name]]) -> Set (Name, [[Name]])
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) = Set (Name, [[Name]])
-> Set (Name, [[Name]]) -> Set (Name, [[Name]])
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
nName -> [Name] -> [Name]
forall 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
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ps) Term
sc
nut [Name]
ps Term
_ = Set (Name, [[Name]])
forall a. Set a
S.empty
argNames :: Term -> [Name]
argNames Term
tm = let ns :: [Name]
ns = Term -> [Name]
directUse Term
tm in
(Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
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) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
v [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Term -> [Name]
directUse Term
sc [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n])
[Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
t
directUse (Bind Name
n Binder Term
b Term
sc) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Term -> [Name]
directUse Term
sc [Name] -> [Name] -> [Name]
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]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn,
Text
pfk Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"prim_fork"
= Term -> [Name]
directUse Term
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
w
| (P NameType
Ref (UN Text
fce) Term
_, [Term
_, Term
_, Term
a]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn,
Text
fce Text -> Text -> Bool
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn = []
| (P (TCon Int
_ Int
_) Name
n Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn = []
| Bool
otherwise = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
a
directUse (Proj Term
x Int
i) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
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 = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (SC -> [Name] -> [Name]
forall {t :: * -> *}. Foldable t => SC -> t Name -> [Name]
findAllUsedArgs SC
sc [Name]
topargs)
findAllUsedArgs :: SC -> t Name -> [Name]
findAllUsedArgs SC
sc t Name
topargs = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
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 Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: (CaseAlt' Term -> [Name]) -> [CaseAlt' Term] -> [Name]
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (CaseAlt' Term -> [Name]) -> [CaseAlt' Term] -> [Name]
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
|| (CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> 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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
t Bool -> Bool -> Bool
|| (CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> 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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Term -> [Name]
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 = State CS a -> CS -> (a, CS)
forall s a. State s a -> s -> (a, s)
runState (State CS a -> CS -> (a, CS)) -> State CS a -> CS -> (a, CS)
forall a b. (a -> b) -> a -> b
$ CaseBuilder a -> ErasureInfo -> State CS a
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
(Int -> Phase -> ShowS)
-> (Phase -> String) -> ([Phase] -> ShowS) -> Show Phase
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Phase -> ShowS
showsPrec :: Int -> Phase -> ShowS
$cshow :: Phase -> String
show :: Phase -> String
$cshowList :: [Phase] -> ShowS
showList :: [Phase] -> ShowS
Show, Phase -> Phase -> Bool
(Phase -> Phase -> Bool) -> (Phase -> Phase -> Bool) -> Eq Phase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Phase -> Phase -> Bool
== :: Phase -> Phase -> Bool
$c/= :: Phase -> Phase -> Bool
/= :: 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
= Bool -> SC -> Phase -> FC -> [([Name], Term, Term)] -> TC CaseDef
forall {t :: * -> *}.
Foldable t =>
Bool -> SC -> Phase -> FC -> [(t Name, Term, Term)] -> TC CaseDef
sc' Bool
tc SC
defcase Phase
phase FC
fc ((([Name], Term, Term) -> Bool)
-> [([Name], Term, Term)] -> [([Name], Term, Term)]
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 []
= CaseDef -> TC CaseDef
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseDef -> TC CaseDef) -> CaseDef -> TC CaseDef
forall a b. (a -> b) -> a -> b
$ [Name] -> SC -> [Term] -> CaseDef
CaseDef [] (String -> SC
forall t. String -> SC' t
UnmatchedCase (FC -> String
forall a. Show a => a -> String
show FC
fc String -> ShowS
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 Phase -> Phase -> Bool
forall a. Eq a => a -> a -> Bool
== Phase
RunTime
pats :: [(t Name, [Pat], (Term, Term))]
pats = ((t Name, Term, Term) -> (t Name, [Pat], (Term, Term)))
-> [(t Name, Term, Term)] -> [(t Name, [Pat], (Term, Term))]
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 = ((t Name, [Pat], (Term, Term)) -> TC Clause)
-> [(t Name, [Pat], (Term, Term))] -> TC [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (t Name, [Pat], (Term, Term)) -> TC Clause
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 = [Pat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Clause -> [Pat]
forall a b. (a, b) -> a
fst ([Clause] -> Clause
forall a. HasCallStack => [a] -> a
head [Clause]
pats))
ns :: [Name]
ns = Int -> [Name] -> [Name]
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 Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
inacc) | (Int
i,Name
n) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Name]
ns] [Clause]
pats (((Term, Bool) -> Bool) -> [(Term, Bool)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Term, Bool)]
argtys)
(SC
tree, CS
st) = ErasureInfo -> CaseBuilder SC -> CS -> (SC, CS)
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 (CS -> [Term]
forall {a} {b} {c}. (a, b, c) -> a
fstT CS
st) in
if Bool
proj then CaseDef -> TC CaseDef
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseDef -> CaseDef
stripLambdas CaseDef
t)
else CaseDef -> TC CaseDef
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return CaseDef
t
Error Err
err -> Err -> TC CaseDef
forall a. Err -> TC a
Error (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc Err
err)
where args :: [Name]
args = (Int -> Name) -> [Int] -> [Name]
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 Phase -> Phase -> Bool
forall a. Eq a => a -> a -> Bool
/= Phase
CompileTime Bool -> Bool -> Bool
|| Bool
reflect = ([Pat], b) -> TC ([Pat], b)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)
| Bool
otherwise = do (Name -> TC ()) -> t Name -> TC ()
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
([Pat], b) -> TC ([Pat], b)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)
acc :: [Pat] -> Name -> TC ()
acc [] Name
n = Err -> TC ()
forall a. Err -> TC a
Error (Name -> Err
forall t. Name -> Err' t
Inaccessible Name
n)
acc (PV Name
x Term
t : [Pat]
xs) Name
n | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = () -> TC ()
forall a. a -> TC a
OK ()
acc (PCon Bool
_ Name
_ Int
_ [Pat]
ps : [Pat]
xs) Name
n = [Pat] -> Name -> TC ()
acc ([Pat]
ps [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ [Pat]
xs) Name
n
acc (PSuc Pat
p : [Pat]
xs) Name
n = [Pat] -> Name -> TC ()
acc (Pat
p Pat -> [Pat] -> [Pat]
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
(Int -> Pat -> ShowS)
-> (Pat -> String) -> ([Pat] -> ShowS) -> Show Pat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Pat -> ShowS
showsPrec :: Int -> Pat -> ShowS
$cshow :: Pat -> String
show :: Pat -> String
$cshowList :: [Pat] -> ShowS
showList :: [Pat] -> ShowS
Show
toPats :: Bool -> Bool -> Term -> [Pat]
toPats :: Bool -> Bool -> Term -> [Pat]
toPats Bool
reflect Bool
tc Term
f = [Pat] -> [Pat]
forall a. [a] -> [a]
reverse (Bool -> Bool -> [Term] -> [Pat]
toPat Bool
reflect Bool
tc (Term -> [Term]
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 TT n -> [TT n] -> [TT n]
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 = (Term -> Pat) -> [Term] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Pat) -> [Term] -> [Pat])
-> (Term -> Pat) -> [Term] -> [Pat]
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 Text -> Text -> Bool
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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Read" Bool -> Bool -> Bool
&& Text
own Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Ownership"
= Bool -> Name -> Int -> [Pat] -> Pat
PCon Bool
False Name
nm Int
t ((Pat -> Pat) -> [Pat] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
shareCons ((Term -> Pat) -> [Term] -> [Pat]
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 ((Pat -> Pat) -> [Pat] -> [Pat]
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 ([Pat] -> Pat) -> [Pat] -> Pat
forall a b. (a -> b) -> a -> b
$ (Term -> Pat) -> [Term] -> [Pat]
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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"prim__addBigInt"
= Pat -> Pat
PSuc (Pat -> Pat) -> Pat -> Pat
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 Term -> [Term] -> [Term]
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
&& Name -> Term -> 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 ([Pat] -> Pat) -> [Pat] -> Pat
forall a b. (a -> b) -> a -> b
$ (Term -> Pat) -> [Term] -> [Pat]
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
(Int -> Partition -> ShowS)
-> (Partition -> String)
-> ([Partition] -> ShowS)
-> Show Partition
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Partition -> ShowS
showsPrec :: Int -> Partition -> ShowS
$cshow :: Partition -> String
show :: Partition -> String
$cshowList :: [Partition] -> ShowS
showList :: [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]
_)
| Clause -> Bool
forall {b}. ([Pat], b) -> Bool
isVarPat Clause
m = let ([Clause]
vars, [Clause]
rest) = (Clause -> Bool) -> [Clause] -> ([Clause], [Clause])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Clause -> Bool
forall {b}. ([Pat], b) -> Bool
isVarPat [Clause]
ms in
[Clause] -> Partition
Vars [Clause]
vars Partition -> [Partition] -> [Partition]
forall a. a -> [a] -> [a]
: [Clause] -> [Partition]
partition [Clause]
rest
| Clause -> Bool
forall {b}. ([Pat], b) -> Bool
isConPat Clause
m = let ([Clause]
cons, [Clause]
rest) = (Clause -> Bool) -> [Clause] -> ([Clause], [Clause])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Clause -> Bool
forall {b}. ([Pat], b) -> Bool
isConPat [Clause]
ms in
[Clause] -> Partition
Cons [Clause]
cons Partition -> [Partition] -> [Partition]
forall a. a -> [a] -> [a]
: [Clause] -> [Partition]
partition [Clause]
rest
partition [Clause]
xs = String -> [Partition]
forall a. HasCallStack => String -> a
error (String -> [Partition]) -> String -> [Partition]
forall a b. (a -> b) -> a -> b
$ String
"Partition " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Clause] -> String
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 = (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
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 = Int -> [Name] -> [Name] -> [Name]
forall {a}. Int -> [a] -> [a] -> [a]
pick Int
0 [] (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
ns')
cs_out :: [Clause]
cs_out = (Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Clause
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) = (Int -> [a] -> [a] -> [a]
forall {a}. Int -> [a] -> [a] -> [a]
pick Int
0 [] [a]
pats, b
def)
pick :: Int -> [a] -> [a] -> [a]
pick Int
i [a]
skipped [] = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
skipped
pick Int
i [a]
skipped (a
x : [a]
xs)
| Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
pos = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a] -> [a]
pick (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [a]
skipped [a]
xs
| Bool
otherwise = Int -> [a] -> [a] -> [a]
pick (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (a
x a -> [a] -> [a]
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 = [[((Name, Bool), (Bool, Pat))]] -> [[((Name, Bool), (Bool, Pat))]]
forall a. [[a]] -> [[a]]
transpose (([(Bool, Pat)] -> [((Name, Bool), (Bool, Pat))])
-> [[(Bool, Pat)]] -> [[((Name, Bool), (Bool, Pat))]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Bool)] -> [(Bool, Pat)] -> [((Name, Bool), (Bool, Pat))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Name, Bool)]
ns') (([Pat] -> [(Bool, Pat)]) -> [[Pat]] -> [[(Bool, Pat)]]
forall a b. (a -> b) -> [a] -> [b]
map ([Bool] -> [Pat] -> [(Bool, Pat)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
cans) ((Clause -> [Pat]) -> [Clause] -> [[Pat]]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> [Pat]
forall a b. (a, b) -> a
fst [Clause]
cs)))
([[((Name, Bool), (Bool, Pat))]]
patnames_ord, [[((Name, Bool), (Bool, Pat))]]
patnames_rest)
= ([((Name, Bool), (Bool, Pat))] -> Bool)
-> [[((Name, Bool), (Bool, Pat))]]
-> ([[((Name, Bool), (Bool, Pat))]],
[[((Name, Bool), (Bool, Pat))]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
Data.List.partition ([(Bool, Pat)] -> Bool
noClash ([(Bool, Pat)] -> Bool)
-> ([((Name, Bool), (Bool, Pat))] -> [(Bool, Pat)])
-> [((Name, Bool), (Bool, Pat))]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Name, Bool), (Bool, Pat)) -> (Bool, Pat))
-> [((Name, Bool), (Bool, Pat))] -> [(Bool, Pat)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Bool), (Bool, Pat)) -> (Bool, Pat)
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 -> [[((Name, Bool), (Bool, Pat))]] -> [[((Name, Bool), (Bool, Pat))]]
forall a. [a] -> [a]
reverse [[((Name, Bool), (Bool, Pat))]]
patnames_ord
pats' :: [[((Name, Bool), (Bool, Pat))]]
pats' = [[((Name, Bool), (Bool, Pat))]] -> [[((Name, Bool), (Bool, Pat))]]
forall a. [[a]] -> [[a]]
transpose (([((Name, Bool), (Bool, Pat))]
-> [((Name, Bool), (Bool, Pat))] -> Ordering)
-> [[((Name, Bool), (Bool, Pat))]]
-> [[((Name, Bool), (Bool, Pat))]]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy [((Name, Bool), (Bool, Pat))]
-> [((Name, Bool), (Bool, Pat))] -> Ordering
forall {a} {a} {a} {a} {a}.
Ord a =>
[((a, a), (a, Pat))] -> [((a, a), (a, Pat))] -> Ordering
moreDistinct [[((Name, Bool), (Bool, Pat))]]
patnames_ord'
[[((Name, Bool), (Bool, Pat))]]
-> [[((Name, Bool), (Bool, Pat))]]
-> [[((Name, Bool), (Bool, Pat))]]
forall a. [a] -> [a] -> [a]
++ [[((Name, Bool), (Bool, Pat))]]
patnames_rest) in
([[((Name, Bool), (Bool, Pat))]] -> [Name]
forall {b} {b} {b}. [[((b, b), b)]] -> [b]
getNOrder [[((Name, Bool), (Bool, Pat))]]
pats', ([((Name, Bool), (Bool, Pat))] -> Clause -> Clause)
-> [[((Name, Bool), (Bool, Pat))]] -> [Clause] -> [Clause]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [((Name, Bool), (Bool, Pat))] -> Clause -> Clause
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 [] = String -> [b]
forall a. HasCallStack => String -> a
error (String -> [b]) -> String -> [b]
forall a b. (a -> b) -> a -> b
$ String
"Failed order on " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Name], [Clause]) -> String
forall a. Show a => a -> String
show (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
ns', [Clause]
cs)
getNOrder ([((b, b), b)]
c : [[((b, b), b)]]
_) = (((b, b), b) -> b) -> [((b, b), b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((b, b) -> b
forall a b. (a, b) -> a
fst ((b, b) -> b) -> (((b, b), b) -> (b, b)) -> ((b, b), b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b), b) -> (b, b)
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 = (((a, (a, b)) -> b) -> [(a, (a, b))] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((a, b) -> b
forall a b. (a, b) -> b
snd ((a, b) -> b) -> ((a, (a, b)) -> (a, b)) -> (a, (a, b)) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, (a, b)) -> (a, b)
forall a b. (a, b) -> b
snd) [(a, (a, b))]
patnames, (a, b) -> b
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 ((Pat -> Bool) -> [Pat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Pat -> Pat -> Bool
clashPat Pat
p) (((Bool, Pat) -> Pat) -> [(Bool, Pat)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, Pat) -> Pat
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' = Name
n Name -> Name -> Bool
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
= (a, Int) -> (a, Int) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((a, a) -> a
forall a b. (a, b) -> b
snd ((a, a) -> a)
-> ([((a, a), (a, Pat))] -> (a, a)) -> [((a, a), (a, Pat))] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, a), (a, Pat)) -> (a, a)
forall a b. (a, b) -> a
fst (((a, a), (a, Pat)) -> (a, a))
-> ([((a, a), (a, Pat))] -> ((a, a), (a, Pat)))
-> [((a, a), (a, Pat))]
-> (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((a, a), (a, Pat))] -> ((a, a), (a, Pat))
forall a. HasCallStack => [a] -> a
head ([((a, a), (a, Pat))] -> a) -> [((a, a), (a, Pat))] -> a
forall a b. (a -> b) -> a -> b
$ [((a, a), (a, Pat))]
xs, [Either Name Const] -> [(a, Pat)] -> Int
forall {a}. [Either Name Const] -> [(a, Pat)] -> Int
numNames [] ((((a, a), (a, Pat)) -> (a, Pat))
-> [((a, a), (a, Pat))] -> [(a, Pat)]
forall a b. (a -> b) -> [a] -> [b]
map ((a, a), (a, Pat)) -> (a, Pat)
forall a b. (a, b) -> b
snd [((a, a), (a, Pat))]
ys))
((a, a) -> a
forall a b. (a, b) -> b
snd ((a, a) -> a)
-> ([((a, a), (a, Pat))] -> (a, a)) -> [((a, a), (a, Pat))] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, a), (a, Pat)) -> (a, a)
forall a b. (a, b) -> a
fst (((a, a), (a, Pat)) -> (a, a))
-> ([((a, a), (a, Pat))] -> ((a, a), (a, Pat)))
-> [((a, a), (a, Pat))]
-> (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((a, a), (a, Pat))] -> ((a, a), (a, Pat))
forall a. HasCallStack => [a] -> a
head ([((a, a), (a, Pat))] -> a) -> [((a, a), (a, Pat))] -> a
forall a b. (a -> b) -> a -> b
$ [((a, a), (a, Pat))]
ys, [Either Name Const] -> [(a, Pat)] -> Int
forall {a}. [Either Name Const] -> [(a, Pat)] -> Int
numNames [] ((((a, a), (a, Pat)) -> (a, Pat))
-> [((a, a), (a, Pat))] -> [(a, Pat)]
forall a b. (a -> b) -> [a] -> [b]
map ((a, a), (a, Pat)) -> (a, Pat)
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 (Name -> Either Name Const
forall a b. a -> Either a b
Left Name
n Either Name Const -> [Either Name Const] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Either Name Const]
xs) = [Either Name Const] -> [(a, Pat)] -> Int
numNames (Name -> Either Name Const
forall a b. a -> Either a b
Left Name
n Either Name Const -> [Either Name Const] -> [Either Name Const]
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 (Const -> Either Name Const
forall a b. b -> Either a b
Right Const
c Either Name Const -> [Either Name Const] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Either Name Const]
xs) = [Either Name Const] -> [(a, Pat)] -> Int
numNames (Const -> Either Name Const
forall a b. b -> Either a b
Right Const
c Either Name Const -> [Either Name Const] -> [Either Name Const]
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 [] = [Either Name Const] -> Int
forall a. [a] -> Int
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 = [Clause] -> [Int]
forall {a} {b}. (Num a, Eq a) => [([Pat], b)] -> [a]
getInf [Clause]
cs in
([Int] -> [Name] -> [Name]
forall a. [Int] -> [a] -> [a]
selectInf [Int]
alwaysInf [Name]
vs,
(Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Clause
forall {b}. ([Pat], b) -> ([Pat], b)
deInf ((Clause -> Clause) -> [Clause] -> [Clause]
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)] = a -> [Pat] -> [a]
forall {t}. Num t => t -> [Pat] -> [t]
infPos a
0 [Pat]
pats
getInf (([Pat]
pats, b
def) : [([Pat], b)]
cs) = a -> [Pat] -> [a]
forall {t}. Num t => t -> [Pat] -> [t]
infPos a
0 [Pat]
pats [a] -> [a] -> [a]
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) = Int -> [Int] -> [Pat] -> [Pat] -> [Pat] -> ([Pat], [Pat])
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 [Pat] -> [Pat] -> [Pat]
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) = Int -> [Int] -> [a] -> [a] -> [a] -> ([a], [a])
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 [a] -> [a] -> [a]
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 [] = ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
notInf, [a] -> [a]
forall a. [a] -> [a]
reverse [a]
inf)
splitPats t
i t t
infpos [a]
notInf [a]
inf (a
p : [a]
ps)
| t
i t -> t t -> Bool
forall a. Eq a => a -> t a -> Bool
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 t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) t t
infpos [a]
notInf (a
p a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
inf) [a]
ps
| Bool
otherwise = t -> t t -> [a] -> [a] -> [a] -> ([a], [a])
splitPats (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) t t
infpos (a
p a -> [a] -> [a]
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 t -> [t] -> [t]
forall a. a -> [a] -> [a]
: t -> [Pat] -> [t]
infPos (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [Pat]
ps
infPos t
i (Pat
_ : [Pat]
ps) = t -> [Pat] -> [t]
infPos (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [Pat]
ps
deInf :: ([Pat], b) -> ([Pat], b)
deInf ([Pat]
pats, b
def) = ((Pat -> Pat) -> [Pat] -> [Pat]
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) <- ReaderT ErasureInfo (State CS) CS
forall s (m :: * -> *). MonadState s m => m s
get
CS -> ReaderT ErasureInfo (State CS) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
ts [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ ((Clause -> Term) -> [Clause] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, Term) -> Term
forall a b. (a, b) -> a
fst((Term, Term) -> Term)
-> (Clause -> (Term, Term)) -> Clause -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Clause -> (Term, Term)
forall a b. (a, b) -> b
snd) [Clause]
xs), Int
v, [(Name, Term)]
ntys)
case (Term, Term) -> Term
forall a b. (a, b) -> b
snd (Term, Term)
ret of
Term
Impossible -> SC -> CaseBuilder SC
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return SC
forall t. SC' t
ImpossibleCase
Term
tm -> SC -> CaseBuilder SC
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SC -> CaseBuilder SC) -> SC -> CaseBuilder SC
forall a b. (a -> b) -> a -> b
$ Term -> SC
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 = SC -> CaseBuilder SC
forall a. a -> ReaderT ErasureInfo (State CS) a
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 <- ReaderT ErasureInfo (State CS) ErasureInfo
forall r (m :: * -> *). MonadReader r m => m r
ask
[Int] -> CaseBuilder [Int]
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Int] -> CaseBuilder [Int]) -> [Int] -> CaseBuilder [Int]
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
(Int -> ConType -> ShowS)
-> (ConType -> String) -> ([ConType] -> ShowS) -> Show ConType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConType -> ShowS
showsPrec :: Int -> ConType -> ShowS
$cshow :: ConType -> String
show :: ConType -> String
$cshowList :: [ConType] -> ShowS
showList :: [ConType] -> ShowS
Show, ConType -> ConType -> Bool
(ConType -> ConType -> Bool)
-> (ConType -> ConType -> Bool) -> Eq ConType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConType -> ConType -> Bool
== :: ConType -> ConType -> Bool
$c/= :: ConType -> ConType -> Bool
/= :: ConType -> ConType -> Bool
Eq)
data Group = ConGroup Bool
ConType
[([Pat], Clause)]
deriving Int -> Group -> ShowS
[Group] -> ShowS
Group -> String
(Int -> Group -> ShowS)
-> (Group -> String) -> ([Group] -> ShowS) -> Show Group
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Group -> ShowS
showsPrec :: Int -> Group -> ShowS
$cshow :: Group -> String
show :: Group -> String
$cshowList :: [Group] -> ShowS
showList :: [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
vName -> [Name] -> [Name]
forall 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
SC -> CaseBuilder SC
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SC -> CaseBuilder SC) -> SC -> CaseBuilder SC
forall a b. (a -> b) -> a -> b
$ CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case ([Group] -> CaseType
getShared [Group]
gs) Name
v ([CaseAlt' Term] -> [CaseAlt' Term]
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 [] = [CaseAlt' Term] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return [SC -> CaseAlt' Term
forall t. SC' t -> CaseAlt' t
DefaultCase SC
err]
altGroups (ConGroup Bool
_ (CName Name
n Int
i) [([Pat], Clause)]
args : [Group]
cs)
= (:) (CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
-> ReaderT
ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
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 ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
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)
= (:) (CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
-> ReaderT
ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
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 ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
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)
= (:) (CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
-> ReaderT
ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Pat], Clause)] -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altSucGroup [([Pat], Clause)]
args ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
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)
= (:) (CaseAlt' Term -> [CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
-> ReaderT
ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
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 ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
vs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
inaccVars) [Clause]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term))
-> CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a b. (a -> b) -> a -> b
$ Name -> Int -> [Name] -> SC -> CaseAlt' Term
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
vs) [Clause]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term))
-> CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> SC -> CaseAlt' Term
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
newVarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
vs) [Clause]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term))
-> CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a b. (a -> b) -> a -> b
$ Name -> SC -> CaseAlt' Term
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
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term))
-> CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
forall a b. (a -> b) -> a -> b
$ Const -> SC -> CaseAlt' Term
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]
_ [] = ([Name], [Name], [Name], [Clause])
-> CaseBuilder ([Name], [Name], [Name], [Clause])
forall a. a -> ReaderT ErasureInfo (State CS) a
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) = [Name] -> ([Name], [Name])
forall {a}. [a] -> ([a], [a])
partitionAcc [Name]
newVars
([Name], [Name], [Name], [Clause])
-> CaseBuilder ([Name], [Name], [Name], [Clause])
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
newVars, [Name]
accVars, [Name]
inaccVars, [([Pat], Clause)] -> [Clause]
forall {a} {b}. [([a], ([a], b))] -> [([a], b)]
addRs [([Pat], Clause)]
rs)
where
getNewVars :: [Pat] -> CaseBuilder [Name]
getNewVars :: [Pat] -> CaseBuilder [Name]
getNewVars [] = [Name] -> CaseBuilder [Name]
forall a. a -> ReaderT ErasureInfo (State CS) a
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) <- ReaderT ErasureInfo (State CS) CS
forall s (m :: * -> *). MonadState s m => m s
get
CS -> ReaderT ErasureInfo (State CS) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
cs, Int
i, (Name
v, Term
t) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
ntys)
[Name] -> CaseBuilder [Name]
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
v Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
nsv)
getNewVars (Pat
PAny : [Pat]
ns) = (:) (Name -> [Name] -> [Name])
-> CaseBuilder Name
-> ReaderT ErasureInfo (State CS) ([Name] -> [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> CaseBuilder Name
getVar String
"i" ReaderT ErasureInfo (State CS) ([Name] -> [Name])
-> CaseBuilder [Name] -> CaseBuilder [Name]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
getNewVars (Pat
PTyPat : [Pat]
ns) = (:) (Name -> [Name] -> [Name])
-> CaseBuilder Name
-> ReaderT ErasureInfo (State CS) ([Name] -> [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> CaseBuilder Name
getVar String
"t" ReaderT ErasureInfo (State CS) ([Name] -> [Name])
-> CaseBuilder [Name] -> CaseBuilder [Name]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
getNewVars (Pat
_ : [Pat]
ns) = (:) (Name -> [Name] -> [Name])
-> CaseBuilder Name
-> ReaderT ErasureInfo (State CS) ([Name] -> [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> CaseBuilder Name
getVar String
"e" ReaderT ErasureInfo (State CS) ([Name] -> [Name])
-> CaseBuilder [Name] -> CaseBuilder [Name]
forall a b.
ReaderT ErasureInfo (State CS) (a -> b)
-> ReaderT ErasureInfo (State CS) a
-> ReaderT ErasureInfo (State CS) b
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) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [a]
xs, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
inacc]
, [a
x | (Int
i,a
x) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [a]
xs, Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
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]
acc[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
ps[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
inacc, b
res) ([a], b) -> [([a], b)] -> [([a], b)]
forall a. a -> [a] -> [a]
: [([a], ([a], b))] -> [([a], b)]
addRs [([a], ([a], b))]
rs)
where
([a]
acc, [a]
inacc) = [a] -> ([a], [a])
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) <- ReaderT ErasureInfo (State CS) CS
forall s (m :: * -> *). MonadState s m => m s
get; CS -> ReaderT ErasureInfo (State CS) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
t, Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, [(Name, Term)]
ntys); Name -> CaseBuilder Name
forall a. a -> ReaderT ErasureInfo (State CS) a
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 = [Group] -> [Clause] -> CaseBuilder [Group]
forall {m :: * -> *}. Monad m => [Group] -> [Clause] -> m [Group]
gc [] [Clause]
cs
where
gc :: [Group] -> [Clause] -> m [Group]
gc [Group]
acc [] = [Group] -> m [Group]
forall a. a -> m a
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' <- Pat -> [Pat] -> (Term, Term) -> [Group] -> m [Group]
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 -> [Group] -> m [Group]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Group] -> m [Group]) -> [Group] -> m [Group]
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 -> [Group] -> m [Group]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Group] -> m [Group]) -> [Group] -> m [Group]
forall a b. (a -> b) -> a -> b
$ Const -> Clause -> [Group] -> [Group]
addConG Const
cval ([Pat]
ps, (Term, Term)
res) [Group]
acc
PSuc Pat
n -> [Group] -> m [Group]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Group] -> m [Group]) -> [Group] -> m [Group]
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 -> [Group] -> m [Group]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Group] -> m [Group]) -> [Group] -> m [Group]
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 -> String -> m [Group]
forall a. HasCallStack => String -> a
error (String -> m [Group]) -> String -> m [Group]
forall a b. (a -> b) -> a -> b
$ Pat -> String
forall a. Show a => a -> String
show Pat
pat String -> ShowS
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 ConType -> ConType -> Bool
forall a. Eq a => a -> a -> Bool
== ConType
c' = Bool -> ConType -> [([Pat], Clause)] -> Group
ConGroup Bool
uniq ConType
c ([([Pat], Clause)]
cs [([Pat], Clause)] -> [([Pat], Clause)] -> [([Pat], Clause)]
forall a. [a] -> [a] -> [a]
++ [([Pat]
conargs, Clause
res)]) Group -> [Group] -> [Group]
forall a. a -> [a] -> [a]
: [Group]
gs
| Bool
otherwise = Group
g Group -> [Group] -> [Group]
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 Const -> Const -> Bool
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 [([Pat], Clause)] -> [([Pat], Clause)] -> [([Pat], Clause)]
forall a. [a] -> [a] -> [a]
++ [([], Clause
res)]) Group -> [Group] -> [Group]
forall a. a -> [a] -> [a]
: [Group]
gs
addConG Const
con Clause
res (Group
g : [Group]
gs) = Group
g Group -> [Group] -> [Group]
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' <- (Clause -> ReaderT ErasureInfo (State CS) Clause)
-> [Clause] -> ReaderT ErasureInfo (State CS) [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name -> Clause -> ReaderT ErasureInfo (State CS) Clause
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) <- m (a, b, [(Name, Term)])
forall s (m :: * -> *). MonadState s m => m s
get
(a, b, [(Name, Term)]) -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (a
cs, b
i, (Name
v, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
ntys)
([Pat], (a, Term)) -> m ([Pat], (a, Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a
lhs, Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
p (NameType -> Name -> Term -> Term
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) = ([Pat], (a, Term)) -> m ([Pat], (a, Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a, Term)
res)
repVar Name
v (Pat
PTyPat : [Pat]
ps , (a, Term)
res) = ([Pat], (a, Term)) -> m ([Pat], (a, Term))
forall a. a -> m a
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) = Term -> SC
forall t. t -> SC' t
STerm ([(Name, (Name, [Name]))] -> Term -> Term
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) = CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x ((CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
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)
= Name -> Int -> [Name] -> SC -> CaseAlt' Term
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)) (Name, (Name, [Name]))
-> [(Name, (Name, [Name]))] -> [(Name, (Name, [Name]))]
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)
= Name -> [Name] -> SC -> CaseAlt' Term
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)) (Name, (Name, [Name]))
-> [(Name, (Name, [Name]))] -> [(Name, (Name, [Name]))]
forall a. a -> [a] -> [a]
: [(Name, (Name, [Name]))]
ms) SC
sc)
dpa [(Name, (Name, [Name]))]
ms Name
x (ConstCase Const
c SC
sc) = Const -> SC -> CaseAlt' Term
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) = Name -> SC -> CaseAlt' Term
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) = SC -> CaseAlt' Term
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) <- TT t -> (TT t, [TT t])
forall n. TT n -> (TT n, [TT n])
unApply TT t
f
= let args' :: [TT t]
args' = (TT t -> TT t) -> [TT t] -> [TT t]
forall a b. (a -> b) -> [a] -> [b]
map ([(t, (t, [t]))] -> TT t -> TT t
applyMaps [(t, (t, [t]))]
ms) [TT t]
args in
[(t, (t, [t]))] -> NameType -> t -> TT t -> [TT t] -> TT t
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' = TT t -> [TT t] -> TT t
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> t -> TT t -> TT t
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'
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (([t] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TT t] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT t]
args') Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:
(t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
cn) Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (t -> TT t -> Bool) -> [t] -> [TT t] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith t -> TT t -> Bool
forall n. Eq n => n -> TT n -> Bool
same [t]
args [TT t]
args') = NameType -> t -> TT t -> TT t
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref t
x TT t
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 a -> a -> Bool
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) = AppStatus t -> TT t -> TT t -> TT t
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
[] -> SC
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 (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SC -> Name -> Bool
isUsed SC
sc') [Name]
args
then CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [Name -> Int -> [Name] -> SC -> CaseAlt' Term
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) (SC -> SC) -> SC -> SC
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]
-> CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [Const -> SC -> CaseAlt' Term
forall t. Const -> SC' t -> CaseAlt' t
ConstCase (Integer -> Const
BI Integer
0) SC
dc, CaseAlt' Term
s]
[CaseAlt' Term]
as -> CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [CaseAlt' Term]
as
where
alts' :: [CaseAlt' Term]
alts' = (CaseAlt' Term -> Bool) -> [CaseAlt' Term] -> [CaseAlt' Term]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CaseAlt' Term -> Bool) -> CaseAlt' Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CaseAlt' Term -> Bool
forall {n}. CaseAlt' (TT n) -> Bool
erased) ([CaseAlt' Term] -> [CaseAlt' Term])
-> [CaseAlt' Term] -> [CaseAlt' Term]
forall a b. (a -> b) -> a -> b
$ (CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
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) = Name -> Int -> [Name] -> SC -> CaseAlt' Term
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) = Name -> [Name] -> SC -> CaseAlt' Term
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) = Const -> SC -> CaseAlt' Term
forall t. Const -> SC' t -> CaseAlt' t
ConstCase Const
c (Bool -> SC -> SC
prune Bool
proj SC
sc)
pruneAlt (SucCase Name
n SC
sc) = Name -> SC -> CaseAlt' Term
forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n (Bool -> SC -> SC
prune Bool
proj SC
sc)
pruneAlt (DefaultCase SC
sc) = SC -> CaseAlt' Term
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
arg
= Term -> [CaseAlt' Term] -> SC
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase (Term -> Int -> Term
forall n. TT n -> Int -> TT n
Proj (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
forall n. TT n
Erased) Int
i) ([CaseAlt' Term] -> SC) -> [CaseAlt' Term] -> SC
forall a b. (a -> b) -> a -> b
$ (CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
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)
= CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x ((CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
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)
= Term -> [CaseAlt' Term] -> SC
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase (Name -> Name -> Int -> Term -> Term
forall {n}. Eq n => n -> n -> Int -> TT n -> TT n
projRepTm Name
arg Name
n Int
i Term
t) ([CaseAlt' Term] -> SC) -> [CaseAlt' Term] -> SC
forall a b. (a -> b) -> a -> b
$ (CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
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) = Term -> SC
forall t. t -> SC' t
STerm (Name -> Name -> Int -> Term -> Term
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)
= Name -> Int -> [Name] -> SC -> CaseAlt' Term
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)
= Name -> [Name] -> SC -> CaseAlt' Term
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)
= Const -> SC -> CaseAlt' Term
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)
= Name -> SC -> CaseAlt' Term
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)
= SC -> CaseAlt' Term
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 = n -> TT n -> TT n -> TT n
forall n. Eq n => n -> TT n -> TT n -> TT n
subst n
arg (TT n -> Int -> TT n
forall n. TT n -> Int -> TT n
Proj (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT 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' = (CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Int)] -> Name -> CaseAlt' Term -> CaseAlt' Term
ruAlt [(Name, Int)]
checked Name
n) (Maybe Int -> [CaseAlt' Term] -> [CaseAlt' Term]
forall {t}. Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
checked) [CaseAlt' Term]
alts) in
CaseType -> Name -> [CaseAlt' Term] -> SC
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tag = [Name -> Int -> [Name] -> SC' t -> CaseAlt' t
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 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
t) [CaseAlt' t]
rest
dropImpossible (Just Int
t) (CaseAlt' t
c : [CaseAlt' t]
rest)
= CaseAlt' t
c CaseAlt' t -> [CaseAlt' t] -> [CaseAlt' t]
forall a. a -> [a] -> [a]
: Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (Int -> Maybe Int
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
Name -> Int -> [Name] -> SC -> CaseAlt' Term
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
Name -> [Name] -> SC -> CaseAlt' Term
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
Const -> SC -> CaseAlt' Term
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
Name -> SC -> CaseAlt' Term
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
SC -> CaseAlt' Term
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) (Name, Int) -> [(Name, Int)] -> [(Name, Int)]
forall a. a -> [a] -> [a]
: ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, Int)
x -> (Name, Int) -> Name
forall a b. (a, b) -> a
fst (Name, Int)
x Name -> Name -> Bool
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 = ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, Int)
x -> (Name, Int) -> Name
forall a b. (a, b) -> a
fst (Name, Int)
x Name -> [Name] -> Bool
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
x]) (Term -> SC
forall t. t -> SC' t
STerm (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
repl ((CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' Term -> CaseAlt' Term
substAlt Name
n Name
repl) [CaseAlt' Term]
alts)
| Bool
otherwise = CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n' ((CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
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) = Term -> SC
forall t. t -> SC' t
STerm (Term -> SC) -> Term -> SC
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
repl Term
forall n. TT n
Erased) Term
t
substSC Name
n Name
repl (UnmatchedCase String
errmsg) = String -> SC
forall t. String -> SC' t
UnmatchedCase String
errmsg
substSC Name
n Name
repl SC
ImpossibleCase = SC
forall t. SC' t
ImpossibleCase
substSC Name
n Name
repl SC
sc = String -> SC
forall a. HasCallStack => String -> a
error (String -> SC) -> String -> SC
forall a b. (a -> b) -> a -> b
$ String
"unsupported in substSC: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
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) = Name -> Int -> [Name] -> SC -> CaseAlt' Term
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) = Name -> [Name] -> SC -> CaseAlt' Term
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) = Const -> SC -> CaseAlt' Term
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Name -> SC -> CaseAlt' Term
forall t. Name -> SC' t -> CaseAlt' t
SucCase Name
n (Name -> Name -> SC -> SC
substSC Name
n Name
repl SC
sc)
| Bool
otherwise = Name -> SC -> CaseAlt' Term
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) = SC -> CaseAlt' Term
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 = Name -> Name -> SC -> SC
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
arg
= CaseType -> Name -> [CaseAlt' t] -> SC' t
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n ([CaseAlt' t] -> SC' t) -> [CaseAlt' t] -> SC' t
forall a b. (a -> b) -> a -> b
$ (CaseAlt' t -> CaseAlt' t) -> [CaseAlt' t] -> [CaseAlt' t]
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)
= CaseType -> Name -> [CaseAlt' t] -> SC' t
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x ((CaseAlt' t -> CaseAlt' t) -> [CaseAlt' t] -> [CaseAlt' t]
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)
= t -> [CaseAlt' t] -> SC' t
forall t. t -> [CaseAlt' t] -> SC' t
ProjCase t
t ([CaseAlt' t] -> SC' t) -> [CaseAlt' t] -> SC' t
forall a b. (a -> b) -> a -> b
$ (CaseAlt' t -> CaseAlt' t) -> [CaseAlt' t] -> [CaseAlt' t]
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)
= Name -> Int -> [Name] -> SC' t -> CaseAlt' t
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)
= Name -> [Name] -> SC' t -> CaseAlt' t
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)
= Const -> SC' t -> CaseAlt' t
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)
= Name -> SC' t -> CaseAlt' t
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)
= SC' t -> CaseAlt' t
forall t. SC' t -> CaseAlt' t
DefaultCase (Name -> Name -> SC' t -> SC' t
mkForceSC Name
n Name
arg SC' t
rhs)