{-# 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
showList :: [CaseDef] -> ShowS
$cshowList :: [CaseDef] -> ShowS
show :: CaseDef -> String
$cshow :: CaseDef -> String
showsPrec :: Int -> CaseDef -> ShowS
$cshowsPrec :: Int -> CaseDef -> ShowS
Show
data SC' t = Case CaseType Name [CaseAlt' t]
| ProjCase t [CaseAlt' t]
| STerm !t
| UnmatchedCase String
| ImpossibleCase
deriving (SC' t -> SC' t -> Bool
(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
/= :: SC' t -> SC' t -> Bool
$c/= :: forall t. Eq t => SC' t -> SC' t -> Bool
== :: SC' t -> SC' t -> Bool
$c== :: forall t. Eq t => SC' t -> SC' t -> Bool
Eq, 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
min :: SC' t -> SC' t -> SC' t
$cmin :: forall t. Ord t => SC' t -> SC' t -> SC' t
max :: SC' t -> SC' t -> SC' t
$cmax :: forall t. Ord t => SC' t -> SC' t -> SC' t
>= :: SC' t -> SC' t -> Bool
$c>= :: forall t. Ord t => SC' t -> SC' t -> Bool
> :: SC' t -> SC' t -> Bool
$c> :: forall t. Ord t => SC' t -> SC' t -> Bool
<= :: SC' t -> SC' t -> Bool
$c<= :: forall t. Ord t => SC' t -> SC' t -> Bool
< :: SC' t -> SC' t -> Bool
$c< :: forall t. Ord t => SC' t -> SC' t -> Bool
compare :: SC' t -> SC' t -> Ordering
$ccompare :: forall t. Ord t => SC' t -> SC' t -> Ordering
$cp1Ord :: forall t. Ord t => Eq (SC' t)
Ord, a -> SC' b -> SC' a
(a -> b) -> SC' a -> SC' b
(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
<$ :: a -> SC' b -> SC' a
$c<$ :: forall a b. a -> SC' b -> SC' a
fmap :: (a -> b) -> SC' a -> SC' b
$cfmap :: forall a b. (a -> b) -> SC' a -> SC' b
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
$cto :: forall t x. Rep (SC' t) x -> SC' t
$cfrom :: forall t x. SC' t -> Rep (SC' t) x
Generic)
data CaseType = Updatable | Shared
deriving (CaseType -> CaseType -> Bool
(CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool) -> Eq CaseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CaseType -> CaseType -> Bool
$c/= :: CaseType -> CaseType -> Bool
== :: CaseType -> CaseType -> Bool
$c== :: CaseType -> CaseType -> Bool
Eq, Eq CaseType
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
min :: CaseType -> CaseType -> CaseType
$cmin :: CaseType -> CaseType -> CaseType
max :: CaseType -> CaseType -> CaseType
$cmax :: CaseType -> CaseType -> CaseType
>= :: CaseType -> CaseType -> Bool
$c>= :: CaseType -> CaseType -> Bool
> :: CaseType -> CaseType -> Bool
$c> :: CaseType -> CaseType -> Bool
<= :: CaseType -> CaseType -> Bool
$c<= :: CaseType -> CaseType -> Bool
< :: CaseType -> CaseType -> Bool
$c< :: CaseType -> CaseType -> Bool
compare :: CaseType -> CaseType -> Ordering
$ccompare :: CaseType -> CaseType -> Ordering
$cp1Ord :: Eq 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
showList :: [CaseType] -> ShowS
$cshowList :: [CaseType] -> ShowS
show :: CaseType -> String
$cshow :: CaseType -> String
showsPrec :: Int -> CaseType -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep CaseType x -> CaseType
$cfrom :: forall x. CaseType -> Rep CaseType x
Generic)
type SC = SC' Term
data CaseAlt' t = ConCase Name Int [Name] !(SC' t)
| FnCase Name [Name] !(SC' t)
| ConstCase Const !(SC' t)
| SucCase Name !(SC' t)
| DefaultCase !(SC' t)
deriving (Int -> CaseAlt' t -> ShowS
[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
showList :: [CaseAlt' t] -> ShowS
$cshowList :: forall t. Show t => [CaseAlt' t] -> ShowS
show :: CaseAlt' t -> String
$cshow :: forall t. Show t => CaseAlt' t -> String
showsPrec :: Int -> CaseAlt' t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> CaseAlt' t -> ShowS
Show, CaseAlt' t -> CaseAlt' t -> Bool
(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
/= :: CaseAlt' t -> CaseAlt' t -> Bool
$c/= :: forall t. Eq t => CaseAlt' t -> CaseAlt' t -> Bool
== :: CaseAlt' t -> CaseAlt' t -> Bool
$c== :: forall t. Eq t => CaseAlt' t -> CaseAlt' t -> Bool
Eq, 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
min :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t
$cmin :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
max :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t
$cmax :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> CaseAlt' t
>= :: CaseAlt' t -> CaseAlt' t -> Bool
$c>= :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
> :: CaseAlt' t -> CaseAlt' t -> Bool
$c> :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
<= :: CaseAlt' t -> CaseAlt' t -> Bool
$c<= :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
< :: CaseAlt' t -> CaseAlt' t -> Bool
$c< :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Bool
compare :: CaseAlt' t -> CaseAlt' t -> Ordering
$ccompare :: forall t. Ord t => CaseAlt' t -> CaseAlt' t -> Ordering
$cp1Ord :: forall t. Ord t => Eq (CaseAlt' t)
Ord, a -> CaseAlt' b -> CaseAlt' a
(a -> b) -> CaseAlt' a -> CaseAlt' b
(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
<$ :: a -> CaseAlt' b -> CaseAlt' a
$c<$ :: forall a b. a -> CaseAlt' b -> CaseAlt' a
fmap :: (a -> b) -> CaseAlt' a -> CaseAlt' b
$cfmap :: forall a b. (a -> b) -> CaseAlt' a -> CaseAlt' b
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
$cto :: forall t x. Rep (CaseAlt' t) x -> CaseAlt' t
$cfrom :: forall t x. CaseAlt' t -> Rep (CaseAlt' t) x
Generic)
type CaseAlt = CaseAlt' Term
instance Show t => Show (SC' t) where
show :: SC' t -> String
show sc :: SC' t
sc = Int -> SC' t -> String
forall a. Show a => Int -> SC' a -> String
show' 1 SC' t
sc
where
show' :: Int -> SC' a -> String
show' i :: Int
i (Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' a]
alts) = "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]
++ " 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 ("\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
Updatable -> "! "
Shared -> " "
show' i :: Int
i (ProjCase tm :: a
tm alts :: [CaseAlt' a]
alts) = "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]
++ " of " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep ("\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' i :: Int
i (STerm tm :: a
tm) = a -> String
forall a. Show a => a -> String
show a
tm
show' i :: Int
i (UnmatchedCase str :: String
str) = "error " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
str
show' i :: Int
i ImpossibleCase = "impossible"
indent :: Int -> String
indent i :: 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 " ")
showA :: Int -> CaseAlt' a -> String
showA i :: Int
i (ConCase n :: Name
n t :: Int
t args :: [Name]
args sc :: SC' a
sc)
= Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep (", ") ((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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) SC' a
sc
showA i :: Int
i (FnCase n :: Name
n args :: [Name]
args sc :: SC' a
sc)
= "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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep (", ") ((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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) SC' a
sc
showA i :: Int
i (ConstCase t :: Const
t sc :: SC' a
sc)
= Const -> String
forall a. Show a => a -> String
show Const
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ " => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) SC' a
sc
showA i :: Int
i (SucCase n :: Name
n sc :: SC' a
sc)
= Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ "+1 => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) SC' a
sc
showA i :: Int
i (DefaultCase sc :: SC' a
sc)
= "_ => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> SC' a -> String
show' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+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 n :: Name
n (Case _ n' :: Name
n' as :: [CaseAlt' Term]
as) = Name -> [CaseAlt' Term] -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n [CaseAlt' Term]
as
termsize n :: Name
n (ProjCase n' :: Term
n' as :: [CaseAlt' Term]
as) = Name -> [CaseAlt' Term] -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n [CaseAlt' Term]
as
termsize n :: Name
n (STerm t :: Term
t) = Name -> Term -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n Term
t
termsize n :: Name
n _ = 1
instance TermSize CaseAlt where
termsize :: Name -> CaseAlt' Term -> Int
termsize n :: Name
n (ConCase _ _ _ s :: SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize n :: Name
n (FnCase _ _ s :: SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize n :: Name
n (ConstCase _ s :: SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize n :: Name
n (SucCase _ s :: SC
s) = Name -> SC -> Int
forall a. TermSize a => Name -> a -> Int
termsize Name
n SC
s
termsize n :: Name
n (DefaultCase s :: 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 n :: Name
n args :: [Name]
args t :: 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 (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> 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
< 20
namesUsed :: SC -> [Name]
namesUsed :: SC -> [Name]
namesUsed sc :: 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' ps :: [Name]
ps (Case _ n :: Name
n alts :: [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' ps :: [Name]
ps (ProjCase t :: Term
t alts :: [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' ps :: [Name]
ps (STerm t :: 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' ps :: [Name]
ps _ = []
nua :: [Name] -> CaseAlt' Term -> [Name]
nua ps :: [Name]
ps (ConCase n :: Name
n i :: Int
i args :: [Name]
args sc :: 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 ps :: [Name]
ps (FnCase n :: Name
n args :: [Name]
args sc :: 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 ps :: [Name]
ps (ConstCase _ sc :: SC
sc) = [Name] -> SC -> [Name]
nu' [Name]
ps SC
sc
nua ps :: [Name]
ps (SucCase _ sc :: SC
sc) = [Name] -> SC -> [Name]
nu' [Name]
ps SC
sc
nua ps :: [Name]
ps (DefaultCase sc :: SC
sc) = [Name] -> SC -> [Name]
nu' [Name]
ps SC
sc
nut :: [a] -> TT a -> [a]
nut ps :: [a]
ps (P _ n :: a
n _) | a
n a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ps = []
| Bool
otherwise = [a
n]
nut ps :: [a]
ps (App _ f :: TT a
f a :: 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 ps :: [a]
ps (Proj t :: TT a
t _) = [a] -> TT a -> [a]
nut [a]
ps TT a
t
nut ps :: [a]
ps (Bind n :: a
n (Let _ t :: TT a
t v :: TT a
v) sc :: 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 ps :: [a]
ps (Bind n :: a
n b :: Binder (TT a)
b sc :: TT a
sc) = [a] -> TT a -> [a]
nut (a
na -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ps) TT a
sc
nut ps :: [a]
ps _ = []
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' ignoreasserts :: Bool
ignoreasserts sc :: SC
sc topargs :: [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' ps :: [Name]
ps (Case _ n :: Name
n alts :: [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' ps :: [Name]
ps (ProjCase t :: Term
t alts :: [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' ps :: [Name]
ps (STerm t :: Term
t) = [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
t
nu' ps :: [Name]
ps _ = Set (Name, [[Name]])
forall a. Set a
S.empty
nua :: [Name] -> CaseAlt' Term -> Set (Name, [[Name]])
nua ps :: [Name]
ps (ConCase n :: Name
n i :: Int
i args :: [Name]
args sc :: SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' ([Name]
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc
nua ps :: [Name]
ps (FnCase n :: Name
n args :: [Name]
args sc :: SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' ([Name]
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
args) SC
sc
nua ps :: [Name]
ps (ConstCase _ sc :: SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps SC
sc
nua ps :: [Name]
ps (SucCase _ sc :: SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps SC
sc
nua ps :: [Name]
ps (DefaultCase sc :: SC
sc) = [Name] -> SC -> Set (Name, [[Name]])
nu' [Name]
ps SC
sc
nut :: [Name] -> Term -> Set (Name, [[Name]])
nut ps :: [Name]
ps (P _ n :: Name
n _) | Name
n Name -> [Name] -> 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 ps :: [Name]
ps fn :: Term
fn@(App _ f :: Term
f a :: Term
a)
| (P _ n :: Name
n _, args :: [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 "assert_total"
then Set (Name, [[Name]])
forall a. Set a
S.empty
else if Name
n Name -> [Name] -> 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 _ _) n :: Name
n _, _) <- 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 ps :: [Name]
ps (Bind n :: Name
n (Let _ t :: Term
t v :: Term
v) sc :: 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 ps :: [Name]
ps (Proj t :: Term
t _) = [Name] -> Term -> Set (Name, [[Name]])
nut [Name]
ps Term
t
nut ps :: [Name]
ps (Bind n :: Name
n b :: Binder Term
b sc :: Term
sc) = [Name] -> Term -> Set (Name, [[Name]])
nut (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ps) Term
sc
nut ps :: [Name]
ps _ = Set (Name, [[Name]])
forall a. Set a
S.empty
argNames :: Term -> [Name]
argNames tm :: Term
tm = let ns :: [Name]
ns = Term -> [Name]
directUse Term
tm in
(Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\x :: Name
x -> Name
x Name -> [Name] -> 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 _ n :: Name
n _) = [Name
n]
directUse (Bind n :: Name
n (Let _ t :: Term
t v :: Term
v) sc :: 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 n :: Name
n b :: Binder Term
b sc :: 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 _ f :: Term
f a :: Term
a)
| (P Ref (UN pfk :: Text
pfk) _, [App _ e :: Term
e w :: 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 "prim_fork"
= Term -> [Name]
directUse Term
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
w
| (P Ref (UN fce :: Text
fce) _, [_, _, a :: 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 "Force"
= Term -> [Name]
directUse Term
a
| (P Ref n :: Name
n _, args :: [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn = []
| (P (TCon _ _) n :: Name
n _, args :: [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 x :: Term
x i :: 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 _ = []
findUsedArgs :: SC -> [Name] -> [Name]
findUsedArgs :: SC -> [Name] -> [Name]
findUsedArgs sc :: SC
sc topargs :: [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
sc topargs :: t Name
topargs = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\x :: Name
x -> Name
x Name -> t Name -> 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 _ n :: Name
n alts :: [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 t :: Term
t alts :: [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 t :: Term
t) = Term -> [Name]
directUse Term
t
nu' _ = []
nua :: CaseAlt' Term -> [Name]
nua (ConCase n :: Name
n i :: Int
i args :: [Name]
args sc :: SC
sc) = SC -> [Name]
nu' SC
sc
nua (FnCase n :: Name
n args :: [Name]
args sc :: SC
sc) = SC -> [Name]
nu' SC
sc
nua (ConstCase _ sc :: SC
sc) = SC -> [Name]
nu' SC
sc
nua (SucCase _ sc :: SC
sc) = SC -> [Name]
nu' SC
sc
nua (DefaultCase sc :: SC
sc) = SC -> [Name]
nu' SC
sc
isUsed :: SC -> Name -> Bool
isUsed :: SC -> Name -> Bool
isUsed sc :: SC
sc n :: Name
n = SC -> Bool
used SC
sc where
used :: SC -> Bool
used (Case _ n' :: Name
n' alts :: [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 t :: Term
t alts :: [CaseAlt' Term]
alts) = Name
n Name -> [Name] -> 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 t :: Term
t) = Name
n Name -> [Name] -> 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 _ = Bool
False
usedA :: CaseAlt' Term -> Bool
usedA (ConCase _ _ args :: [Name]
args sc :: SC
sc) = SC -> Bool
used SC
sc
usedA (FnCase _ args :: [Name]
args sc :: SC
sc) = SC -> Bool
used SC
sc
usedA (ConstCase _ sc :: SC
sc) = SC -> Bool
used SC
sc
usedA (SucCase _ sc :: SC
sc) = SC -> Bool
used SC
sc
usedA (DefaultCase sc :: 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 :: ErasureInfo -> CaseBuilder a -> CS -> (a, CS)
runCaseBuilder ei :: ErasureInfo
ei bld :: 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
showList :: [Phase] -> ShowS
$cshowList :: [Phase] -> ShowS
show :: Phase -> String
$cshow :: Phase -> String
showsPrec :: Int -> Phase -> ShowS
$cshowsPrec :: Int -> Phase -> ShowS
Show, Phase -> Phase -> Bool
(Phase -> Phase -> Bool) -> (Phase -> Phase -> Bool) -> Eq Phase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Phase -> Phase -> Bool
$c/= :: Phase -> Phase -> Bool
== :: Phase -> Phase -> Bool
$c== :: Phase -> Phase -> Bool
Eq)
simpleCase :: Bool -> SC -> Bool ->
Phase -> FC ->
[Int] ->
[(Type, Bool)] ->
[([Name], Term, Term)] ->
ErasureInfo ->
TC CaseDef
simpleCase :: Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> ErasureInfo
-> TC CaseDef
simpleCase tc :: Bool
tc defcase :: SC
defcase reflect :: Bool
reflect phase :: Phase
phase fc :: FC
fc inacc :: [Int]
inacc argtys :: [(Term, Bool)]
argtys cs :: [([Name], Term, Term)]
cs erInfo :: 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 (\(_, _, r :: Term
r) ->
case Term
r of
Impossible -> Bool
False
_ -> Bool
True) [([Name], Term, Term)]
cs)
where
sc' :: Bool -> SC -> Phase -> FC -> [(t Name, Term, Term)] -> TC CaseDef
sc' tc :: Bool
tc defcase :: SC
defcase phase :: Phase
phase fc :: FC
fc []
= CaseDef -> TC CaseDef
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]
++ ":No pattern clauses")) []
sc' tc :: Bool
tc defcase :: SC
defcase phase :: Phase
phase fc :: FC
fc cs :: [(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 (\ (avs :: t Name
avs, l :: Term
l, r :: 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 [([Pat], (Term, Term))]
chkPats = ((t Name, [Pat], (Term, Term)) -> TC ([Pat], (Term, Term)))
-> [(t Name, [Pat], (Term, Term))] -> TC [([Pat], (Term, Term))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (t Name, [Pat], (Term, Term)) -> TC ([Pat], (Term, Term))
forall (t :: * -> *) b.
Foldable t =>
(t Name, [Pat], b) -> TC ([Pat], b)
chkAccessible [(t Name, [Pat], (Term, Term))]
pats in
case TC [([Pat], (Term, Term))]
chkPats of
OK pats :: [([Pat], (Term, Term))]
pats ->
let numargs :: Int
numargs = [Pat] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Pat], (Term, Term)) -> [Pat]
forall a b. (a, b) -> a
fst ([([Pat], (Term, Term))] -> ([Pat], (Term, Term))
forall a. [a] -> a
head [([Pat], (Term, Term))]
pats))
ns :: [Name]
ns = Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
numargs [Name]
args
(ns' :: [Name]
ns', ps' :: [([Pat], (Term, Term))]
ps') = Phase
-> [(Name, Bool)]
-> [([Pat], (Term, Term))]
-> [Bool]
-> ([Name], [([Pat], (Term, Term))])
order Phase
phase [(Name
n, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
inacc) | (i :: Int
i,n :: Name
n) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Name]
ns] [([Pat], (Term, Term))]
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)
(tree :: SC
tree, st :: CS
st) = ErasureInfo -> CaseBuilder SC -> CS -> (SC, CS)
forall a. ErasureInfo -> CaseBuilder a -> CS -> (a, CS)
runCaseBuilder ErasureInfo
erInfo
([Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
match [Name]
ns' [([Pat], (Term, Term))]
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 (m :: * -> *) a. Monad m => a -> m a
return (CaseDef -> CaseDef
stripLambdas CaseDef
t)
else CaseDef -> TC CaseDef
forall (m :: * -> *) a. Monad m => a -> m a
return CaseDef
t
Error err :: 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 (\i :: Int
i -> Int -> String -> Name
sMN Int
i "e") [0..]
fstT :: (a, b, c) -> a
fstT (x :: a
x, _, _) = a
x
chkAccessible :: (t Name, [Pat], b) -> TC ([Pat], b)
chkAccessible (avs :: t Name
avs, l :: [Pat]
l, c :: 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 (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 (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)
acc :: [Pat] -> Name -> TC ()
acc [] n :: Name
n = Err -> TC ()
forall a. Err -> TC a
Error (Name -> Err
forall t. Name -> Err' t
Inaccessible Name
n)
acc (PV x :: Name
x t :: Term
t : xs :: [Pat]
xs) n :: 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 _ _ _ ps :: [Pat]
ps : xs :: [Pat]
xs) n :: Name
n = [Pat] -> Name -> TC ()
acc ([Pat]
ps [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ [Pat]
xs) Name
n
acc (PSuc p :: Pat
p : xs :: [Pat]
xs) n :: Name
n = [Pat] -> Name -> TC ()
acc (Pat
p Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
xs) Name
n
acc (_ : xs :: [Pat]
xs) n :: 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
showList :: [Pat] -> ShowS
$cshowList :: [Pat] -> ShowS
show :: Pat -> String
$cshow :: Pat -> String
showsPrec :: Int -> Pat -> ShowS
$cshowsPrec :: Int -> Pat -> ShowS
Show
toPats :: Bool -> Bool -> Term -> [Pat]
toPats :: Bool -> Bool -> Term -> [Pat]
toPats reflect :: Bool
reflect tc :: Bool
tc f :: 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 _ f :: TT n
f a :: 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 _ = []
toPat :: Bool -> Bool -> [Term] -> [Pat]
toPat :: Bool -> Bool -> [Term] -> [Pat]
toPat reflect :: Bool
reflect tc :: 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' [_,_,arg :: Term
arg] (P (DCon t :: Int
t a :: Int
a uniq :: Bool
uniq) nm :: Name
nm@(UN n :: Text
n) _)
| Text
n Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Delay"
= Bool -> Name -> Int -> [Pat] -> Pat
PCon Bool
uniq Name
nm Int
t [Pat
PAny, Pat
PAny, [Term] -> Term -> Pat
toPat' [] Term
arg]
toPat' args :: [Term]
args (P (DCon t :: Int
t a :: Int
a uniq :: Bool
uniq) nm :: Name
nm@(NS (UN n :: Text
n) [own :: Text
own]) _)
| Text
n Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Read" Bool -> Bool -> Bool
&& Text
own Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "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 _ n :: Name
n i :: Int
i ps :: [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 p :: Pat
p = Pat
p
toPat' args :: [Term]
args (P (DCon t :: Int
t a :: Int
a uniq :: Bool
uniq) n :: Name
n _)
= 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' [p :: Term
p, Constant (BI 1)] (P _ (UN pabi :: Text
pabi) _)
| Text
pabi Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "prim__addBigInt"
= Pat -> Pat
PSuc (Pat -> Pat) -> Pat -> Pat
forall a b. (a -> b) -> a -> b
$ [Term] -> Term -> Pat
toPat' [] Term
p
toPat' [] (P Bound n :: Name
n ty :: Term
ty) = Name -> Term -> Pat
PV Name
n Term
ty
toPat' args :: [Term]
args (App _ f :: Term
f a :: Term
a) = [Term] -> Term -> Pat
toPat' (Term
a Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args) Term
f
toPat' args :: [Term]
args (Inferred tm :: Term
tm) = Pat -> Pat
PInferred ([Term] -> Term -> Pat
toPat' [Term]
args Term
tm)
toPat' [] (Constant x :: Const
x) | Const -> Bool
isTypeConst Const
x = Pat
PTyPat
| Bool
otherwise = Const -> Pat
PConst Const
x
toPat' [] (Bind n :: Name
n (Pi _ _ t :: Term
t _) sc :: 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 "->") [[Term] -> Term -> Pat
toPat' [] Term
t, [Term] -> Term -> Pat
toPat' [] Term
sc]
toPat' args :: [Term]
args (P _ n :: Name
n _)
| 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' _ t :: 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
showList :: [Partition] -> ShowS
$cshowList :: [Partition] -> ShowS
show :: Partition -> String
$cshow :: Partition -> String
showsPrec :: Int -> Partition -> ShowS
$cshowsPrec :: Int -> Partition -> ShowS
Show
isVarPat :: ([Pat], b) -> Bool
isVarPat (PV _ _ : ps :: [Pat]
ps , _) = Bool
True
isVarPat (PAny : ps :: [Pat]
ps , _) = Bool
True
isVarPat (PTyPat : ps :: [Pat]
ps , _) = Bool
True
isVarPat _ = Bool
False
isConPat :: ([Pat], b) -> Bool
isConPat (PCon _ _ _ _ : ps :: [Pat]
ps, _) = Bool
True
isConPat (PReflected _ _ : ps :: [Pat]
ps, _) = Bool
True
isConPat (PSuc _ : ps :: [Pat]
ps, _) = Bool
True
isConPat (PConst _ : ps :: [Pat]
ps, _) = Bool
True
isConPat _ = Bool
False
partition :: [Clause] -> [Partition]
partition :: [([Pat], (Term, Term))] -> [Partition]
partition [] = []
partition ms :: [([Pat], (Term, Term))]
ms@(m :: ([Pat], (Term, Term))
m : _)
| ([Pat], (Term, Term)) -> Bool
forall b. ([Pat], b) -> Bool
isVarPat ([Pat], (Term, Term))
m = let (vars :: [([Pat], (Term, Term))]
vars, rest :: [([Pat], (Term, Term))]
rest) = (([Pat], (Term, Term)) -> Bool)
-> [([Pat], (Term, Term))]
-> ([([Pat], (Term, Term))], [([Pat], (Term, Term))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ([Pat], (Term, Term)) -> Bool
forall b. ([Pat], b) -> Bool
isVarPat [([Pat], (Term, Term))]
ms in
[([Pat], (Term, Term))] -> Partition
Vars [([Pat], (Term, Term))]
vars Partition -> [Partition] -> [Partition]
forall a. a -> [a] -> [a]
: [([Pat], (Term, Term))] -> [Partition]
partition [([Pat], (Term, Term))]
rest
| ([Pat], (Term, Term)) -> Bool
forall b. ([Pat], b) -> Bool
isConPat ([Pat], (Term, Term))
m = let (cons :: [([Pat], (Term, Term))]
cons, rest :: [([Pat], (Term, Term))]
rest) = (([Pat], (Term, Term)) -> Bool)
-> [([Pat], (Term, Term))]
-> ([([Pat], (Term, Term))], [([Pat], (Term, Term))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ([Pat], (Term, Term)) -> Bool
forall b. ([Pat], b) -> Bool
isConPat [([Pat], (Term, Term))]
ms in
[([Pat], (Term, Term))] -> Partition
Cons [([Pat], (Term, Term))]
cons Partition -> [Partition] -> [Partition]
forall a. a -> [a] -> [a]
: [([Pat], (Term, Term))] -> [Partition]
partition [([Pat], (Term, Term))]
rest
partition xs :: [([Pat], (Term, Term))]
xs = String -> [Partition]
forall a. HasCallStack => String -> a
error (String -> [Partition]) -> String -> [Partition]
forall a b. (a -> b) -> a -> b
$ "Partition " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [([Pat], (Term, Term))] -> String
forall a. Show a => a -> String
show [([Pat], (Term, Term))]
xs
order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
order :: Phase
-> [(Name, Bool)]
-> [([Pat], (Term, Term))]
-> [Bool]
-> ([Name], [([Pat], (Term, Term))])
order _ [] cs :: [([Pat], (Term, Term))]
cs cans :: [Bool]
cans = ([], [([Pat], (Term, Term))]
cs)
order _ ns' :: [(Name, Bool)]
ns' [] cans :: [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 pos :: [Int]
pos) ns' :: [(Name, Bool)]
ns' cs :: [([Pat], (Term, Term))]
cs cans :: [Bool]
cans
= let ns_out :: [Name]
ns_out = Int -> [Name] -> [Name] -> [Name]
forall a. Int -> [a] -> [a] -> [a]
pick 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 :: [([Pat], (Term, Term))]
cs_out = (([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))] -> [([Pat], (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
forall a b. ([a], b) -> ([a], b)
pickClause [([Pat], (Term, Term))]
cs in
([Name]
ns_out, [([Pat], (Term, Term))]
cs_out)
where
pickClause :: ([a], b) -> ([a], b)
pickClause (pats :: [a]
pats, def :: b
def) = (Int -> [a] -> [a] -> [a]
forall a. Int -> [a] -> [a] -> [a]
pick 0 [] [a]
pats, b
def)
pick :: Int -> [a] -> [a] -> [a]
pick i :: Int
i skipped :: [a]
skipped [] = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
skipped
pick i :: Int
i skipped :: [a]
skipped (x :: a
x : xs :: [a]
xs)
| Int
i Int -> [Int] -> 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
+ 1) [a]
skipped [a]
xs
| Bool
otherwise = Int -> [a] -> [a] -> [a]
pick (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
skipped) [a]
xs
order phase :: Phase
phase ns' :: [(Name, Bool)]
ns' cs :: [([Pat], (Term, Term))]
cs cans :: [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) ((([Pat], (Term, Term)) -> [Pat])
-> [([Pat], (Term, Term))] -> [[Pat]]
forall a b. (a -> b) -> [a] -> [b]
map ([Pat], (Term, Term)) -> [Pat]
forall a b. (a, b) -> a
fst [([Pat], (Term, Term))]
cs)))
(patnames_ord :: [[((Name, Bool), (Bool, Pat))]]
patnames_ord, patnames_rest :: [[((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
CompileTime -> [[((Name, Bool), (Bool, Pat))]]
patnames_ord
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))]
-> ([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [[((Name, Bool), (Bool, Pat))]]
-> [([Pat], (Term, Term))]
-> [([Pat], (Term, Term))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [((Name, Bool), (Bool, Pat))]
-> ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
forall a a b a b. [(a, (a, b))] -> (a, b) -> ([b], b)
rebuild [[((Name, Bool), (Bool, Pat))]]
pats' [([Pat], (Term, Term))]
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
$ "Failed order on " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Name], [([Pat], (Term, Term))]) -> 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', [([Pat], (Term, Term))]
cs)
getNOrder (c :: [((b, b), b)]
c : _) = (((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 patnames :: [(a, (a, b))]
patnames clause :: (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 ((can :: Bool
can, p :: Pat
p) : ps :: [(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 _ _ _ _) (PConst _) = Bool
True
clashPat (PConst _) (PCon _ _ _ _) = Bool
True
clashPat (PCon _ _ _ _) (PSuc _) = Bool
True
clashPat (PSuc _) (PCon _ _ _ _) = Bool
True
clashPat (PCon _ n :: Name
n i :: Int
i _) (PCon _ n' :: Name
n' i' :: Int
i' _) | 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 _ _ = Bool
False
moreDistinct :: [((a, a), (a, Pat))] -> [((a, a), (a, Pat))] -> Ordering
moreDistinct xs :: [((a, a), (a, Pat))]
xs ys :: [((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. [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. [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 xs :: [Either Name Const]
xs ((_, PCon _ n :: Name
n _ _) : ps :: [(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 (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 xs :: [Either Name Const]
xs ((_, PConst c :: Const
c) : ps :: [(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 (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 xs :: [Either Name Const]
xs (_ : ps :: [(a, Pat)]
ps) = [Either Name Const] -> [(a, Pat)] -> Int
numNames [Either Name Const]
xs [(a, Pat)]
ps
numNames xs :: [Either Name Const]
xs [] = [Either Name Const] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Name Const]
xs
orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])
orderByInf :: [Name]
-> [([Pat], (Term, Term))] -> ([Name], [([Pat], (Term, Term))])
orderByInf vs :: [Name]
vs cs :: [([Pat], (Term, Term))]
cs = let alwaysInf :: [Int]
alwaysInf = [([Pat], (Term, Term))] -> [Int]
forall a b. (Num a, Eq a) => [([Pat], b)] -> [a]
getInf [([Pat], (Term, Term))]
cs in
([Int] -> [Name] -> [Name]
forall a. [Int] -> [a] -> [a]
selectInf [Int]
alwaysInf [Name]
vs,
(([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))] -> [([Pat], (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
forall b. ([Pat], b) -> ([Pat], b)
deInf ((([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))] -> [([Pat], (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
selectExp [Int]
alwaysInf) [([Pat], (Term, Term))]
cs))
where
getInf :: [([Pat], b)] -> [a]
getInf [] = []
getInf [(pats :: [Pat]
pats, def :: b
def)] = a -> [Pat] -> [a]
forall a. Num a => a -> [Pat] -> [a]
infPos 0 [Pat]
pats
getInf ((pats :: [Pat]
pats, def :: b
def) : cs :: [([Pat], b)]
cs) = a -> [Pat] -> [a]
forall a. Num a => a -> [Pat] -> [a]
infPos 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] -> ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
selectExp infs :: [Int]
infs (pats :: [Pat]
pats, def :: (Term, Term)
def)
= let (notInf :: [Pat]
notInf, inf :: [Pat]
inf) = Int -> [Int] -> [Pat] -> [Pat] -> [Pat] -> ([Pat], [Pat])
forall (t :: * -> *) a a.
(Foldable t, Eq a, Num a) =>
a -> t a -> [a] -> [a] -> [a] -> ([a], [a])
splitPats 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 :: [Int] -> [a] -> [a]
selectInf infs :: [Int]
infs ns :: [a]
ns = let (notInf :: [a]
notInf, inf :: [a]
inf) = Int -> [Int] -> [a] -> [a] -> [a] -> ([a], [a])
forall (t :: * -> *) a a.
(Foldable t, Eq a, Num a) =>
a -> t a -> [a] -> [a] -> [a] -> ([a], [a])
splitPats 0 [Int]
infs [] [] [a]
ns in
[a]
notInf [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
inf
splitPats :: a -> t a -> [a] -> [a] -> [a] -> ([a], [a])
splitPats i :: a
i infpos :: t a
infpos notInf :: [a]
notInf inf :: [a]
inf [] = ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
notInf, [a] -> [a]
forall a. [a] -> [a]
reverse [a]
inf)
splitPats i :: a
i infpos :: t a
infpos notInf :: [a]
notInf inf :: [a]
inf (p :: a
p : ps :: [a]
ps)
| a
i a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
infpos = a -> t a -> [a] -> [a] -> [a] -> ([a], [a])
splitPats (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) t a
infpos [a]
notInf (a
p a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
inf) [a]
ps
| Bool
otherwise = a -> t a -> [a] -> [a] -> [a] -> ([a], [a])
splitPats (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) t a
infpos (a
p a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
notInf) [a]
inf [a]
ps
infPos :: a -> [Pat] -> [a]
infPos i :: a
i [] = []
infPos i :: a
i (PInferred p :: Pat
p : ps :: [Pat]
ps) = a
i a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a -> [Pat] -> [a]
infPos (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) [Pat]
ps
infPos i :: a
i (_ : ps :: [Pat]
ps) = a -> [Pat] -> [a]
infPos (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) [Pat]
ps
deInf :: ([Pat], b) -> ([Pat], b)
deInf (pats :: [Pat]
pats, def :: 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 p :: Pat
p) = Pat
p
deInfPat p :: Pat
p = Pat
p
match :: [Name] -> [Clause] -> SC
-> CaseBuilder SC
match :: [Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
match [] (([], ret :: (Term, Term)
ret) : xs :: [([Pat], (Term, Term))]
xs) err :: SC
err
= do (ts :: [Term]
ts, v :: Int
v, ntys :: [(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]
++ ((([Pat], (Term, Term)) -> Term)
-> [([Pat], (Term, Term))] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, Term) -> Term
forall a b. (a, b) -> a
fst((Term, Term) -> Term)
-> (([Pat], (Term, Term)) -> (Term, Term))
-> ([Pat], (Term, Term))
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
.([Pat], (Term, Term)) -> (Term, Term)
forall a b. (a, b) -> b
snd) [([Pat], (Term, Term))]
xs), Int
v, [(Name, Term)]
ntys)
case (Term, Term) -> Term
forall a b. (a, b) -> b
snd (Term, Term)
ret of
Impossible -> SC -> CaseBuilder SC
forall (m :: * -> *) a. Monad m => a -> m a
return SC
forall t. SC' t
ImpossibleCase
tm :: Term
tm -> SC -> CaseBuilder SC
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 vs :: [Name]
vs cs :: [([Pat], (Term, Term))]
cs err :: SC
err = do let (vs' :: [Name]
vs', de_inf :: [([Pat], (Term, Term))]
de_inf) = [Name]
-> [([Pat], (Term, Term))] -> ([Name], [([Pat], (Term, Term))])
orderByInf [Name]
vs [([Pat], (Term, Term))]
cs
ps :: [Partition]
ps = [([Pat], (Term, Term))] -> [Partition]
partition [([Pat], (Term, Term))]
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 vs :: [Name]
vs [] err :: SC
err = SC -> CaseBuilder SC
forall (m :: * -> *) a. Monad m => a -> m a
return SC
err
mixture vs :: [Name]
vs (Cons ms :: [([Pat], (Term, Term))]
ms : ps :: [Partition]
ps) err :: SC
err = do SC
fallthrough <- [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture [Name]
vs [Partition]
ps SC
err
[Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
conRule [Name]
vs [([Pat], (Term, Term))]
ms SC
fallthrough
mixture vs :: [Name]
vs (Vars ms :: [([Pat], (Term, Term))]
ms : ps :: [Partition]
ps) err :: SC
err = do SC
fallthrough <- [Name] -> [Partition] -> SC -> CaseBuilder SC
mixture [Name]
vs [Partition]
ps SC
err
[Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
varRule [Name]
vs [([Pat], (Term, Term))]
ms SC
fallthrough
inaccessibleArgs :: Name -> CaseBuilder [Int]
inaccessibleArgs :: Name -> CaseBuilder [Int]
inaccessibleArgs n :: Name
n = do
ErasureInfo
getInaccessiblePositions <- ReaderT ErasureInfo (State CS) ErasureInfo
forall r (m :: * -> *). MonadReader r m => m r
ask
[Int] -> CaseBuilder [Int]
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
showList :: [ConType] -> ShowS
$cshowList :: [ConType] -> ShowS
show :: ConType -> String
$cshow :: ConType -> String
showsPrec :: Int -> ConType -> ShowS
$cshowsPrec :: Int -> ConType -> ShowS
Show, ConType -> ConType -> Bool
(ConType -> ConType -> Bool)
-> (ConType -> ConType -> Bool) -> Eq ConType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConType -> ConType -> Bool
$c/= :: ConType -> ConType -> Bool
== :: ConType -> ConType -> Bool
$c== :: ConType -> ConType -> Bool
Eq)
data Group = ConGroup Bool
ConType
[([Pat], Clause)]
deriving Int -> Group -> ShowS
[Group] -> ShowS
Group -> String
(Int -> Group -> ShowS)
-> (Group -> String) -> ([Group] -> ShowS) -> Show Group
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Group] -> ShowS
$cshowList :: [Group] -> ShowS
show :: Group -> String
$cshow :: Group -> String
showsPrec :: Int -> Group -> ShowS
$cshowsPrec :: Int -> Group -> ShowS
Show
conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
conRule :: [Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
conRule (v :: Name
v:vs :: [Name]
vs) cs :: [([Pat], (Term, Term))]
cs err :: SC
err = do [Group]
groups <- [([Pat], (Term, Term))] -> CaseBuilder [Group]
groupCons [([Pat], (Term, Term))]
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 (v :: Name
v:vs :: [Name]
vs) gs :: [Group]
gs err :: SC
err = do [CaseAlt' Term]
g <- [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [Group]
gs
SC -> CaseBuilder SC
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 True _ _ : _) = CaseType
Updatable
getShared _ = CaseType
Shared
altGroups :: [Group] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
altGroups [] = [CaseAlt' Term] -> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
forall (m :: * -> *) a. Monad m => a -> m a
return [SC -> CaseAlt' Term
forall t. SC' t -> CaseAlt' t
DefaultCase SC
err]
altGroups (ConGroup _ (CName n :: Name
n i :: Int
i) args :: [([Pat], ([Pat], (Term, Term)))]
args : cs :: [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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altGroup Name
n Int
i [([Pat], ([Pat], (Term, Term)))]
args ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
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 _ (CFn n :: Name
n) args :: [([Pat], ([Pat], (Term, Term)))]
args : cs :: [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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altFnGroup Name
n [([Pat], ([Pat], (Term, Term)))]
args ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
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 _ CSuc args :: [([Pat], ([Pat], (Term, Term)))]
args : cs :: [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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altSucGroup [([Pat], ([Pat], (Term, Term)))]
args ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
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 _ (CConst c :: Const
c) args :: [([Pat], ([Pat], (Term, Term)))]
args : cs :: [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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altConstGroup Const
c [([Pat], ([Pat], (Term, Term)))]
args ReaderT ErasureInfo (State CS) ([CaseAlt' Term] -> [CaseAlt' Term])
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
-> ReaderT ErasureInfo (State CS) [CaseAlt' Term]
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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altGroup n :: Name
n i :: Int
i args :: [([Pat], ([Pat], (Term, Term)))]
args
= do [Int]
inacc <- Name -> CaseBuilder [Int]
inaccessibleArgs Name
n
~(newVars :: [Name]
newVars, accVars :: [Name]
accVars, inaccVars :: [Name]
inaccVars, nextCs :: [([Pat], (Term, Term))]
nextCs) <- [Int]
-> [([Pat], ([Pat], (Term, Term)))]
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
argsToAlt [Int]
inacc [([Pat], ([Pat], (Term, Term)))]
args
SC
matchCs <- [Name] -> [([Pat], (Term, Term))] -> 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) [([Pat], (Term, Term))]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altFnGroup n :: Name
n args :: [([Pat], ([Pat], (Term, Term)))]
args = do ~(newVars :: [Name]
newVars, _, [], nextCs :: [([Pat], (Term, Term))]
nextCs) <- [Int]
-> [([Pat], ([Pat], (Term, Term)))]
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
argsToAlt [] [([Pat], ([Pat], (Term, Term)))]
args
SC
matchCs <- [Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
match ([Name]
newVars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
vs) [([Pat], (Term, Term))]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altSucGroup args :: [([Pat], ([Pat], (Term, Term)))]
args = do ~([newVar :: Name
newVar], _, [], nextCs :: [([Pat], (Term, Term))]
nextCs) <- [Int]
-> [([Pat], ([Pat], (Term, Term)))]
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
argsToAlt [] [([Pat], ([Pat], (Term, Term)))]
args
SC
matchCs <- [Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
match (Name
newVarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
vs) [([Pat], (Term, Term))]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
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], ([Pat], (Term, Term)))]
-> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
altConstGroup n :: Const
n args :: [([Pat], ([Pat], (Term, Term)))]
args = do ~(_, _, [], nextCs :: [([Pat], (Term, Term))]
nextCs) <- [Int]
-> [([Pat], ([Pat], (Term, Term)))]
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
argsToAlt [] [([Pat], ([Pat], (Term, Term)))]
args
SC
matchCs <- [Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
match [Name]
vs [([Pat], (Term, Term))]
nextCs SC
err
CaseAlt' Term -> ReaderT ErasureInfo (State CS) (CaseAlt' Term)
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], ([Pat], (Term, Term)))]
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
argsToAlt _ [] = ([Name], [Name], [Name], [([Pat], (Term, Term))])
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], [], [])
argsToAlt inacc :: [Int]
inacc rs :: [([Pat], ([Pat], (Term, Term)))]
rs@((r :: [Pat]
r, m :: ([Pat], (Term, Term))
m) : rest :: [([Pat], ([Pat], (Term, Term)))]
rest) = do
[Name]
newVars <- [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
r
let (accVars :: [Name]
accVars, inaccVars :: [Name]
inaccVars) = [Name] -> ([Name], [Name])
forall a. [a] -> ([a], [a])
partitionAcc [Name]
newVars
([Name], [Name], [Name], [([Pat], (Term, Term))])
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
newVars, [Name]
accVars, [Name]
inaccVars, [([Pat], ([Pat], (Term, Term)))] -> [([Pat], (Term, Term))]
forall a b. [([a], ([a], b))] -> [([a], b)]
addRs [([Pat], ([Pat], (Term, Term)))]
rs)
where
getNewVars :: [Pat] -> CaseBuilder [Name]
getNewVars :: [Pat] -> CaseBuilder [Name]
getNewVars [] = [Name] -> CaseBuilder [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return []
getNewVars ((PV n :: Name
n t :: Term
t) : ns :: [Pat]
ns) = do Name
v <- String -> CaseBuilder Name
getVar "e"
[Name]
nsv <- [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
(cs :: [Term]
cs, i :: Int
i, ntys :: [(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 (m :: * -> *) a. Monad m => a -> m a
return (Name
v Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
nsv)
getNewVars (PAny : ns :: [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 "i" ReaderT ErasureInfo (State CS) ([Name] -> [Name])
-> CaseBuilder [Name] -> CaseBuilder [Name]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
getNewVars (PTyPat : ns :: [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 "t" ReaderT ErasureInfo (State CS) ([Name] -> [Name])
-> CaseBuilder [Name] -> CaseBuilder [Name]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
getNewVars (_ : ns :: [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 "e" ReaderT ErasureInfo (State CS) ([Name] -> [Name])
-> CaseBuilder [Name] -> CaseBuilder [Name]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns
partitionAcc :: [a] -> ([a], [a])
partitionAcc xs :: [a]
xs =
( [a
x | (i :: Int
i,x :: a
x) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [a]
xs, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
inacc]
, [a
x | (i :: Int
i,x :: a
x) <- [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [a]
xs, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
inacc]
)
addRs :: [([a], ([a], b))] -> [([a], b)]
addRs [] = []
addRs ((r :: [a]
r, (ps :: [a]
ps, res :: b
res)) : rs :: [([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
(acc :: [a]
acc, inacc :: [a]
inacc) = [a] -> ([a], [a])
forall a. [a] -> ([a], [a])
partitionAcc [a]
r
getVar :: String -> CaseBuilder Name
getVar :: String -> CaseBuilder Name
getVar b :: String
b = do (t :: [Term]
t, v :: Int
v, ntys :: [(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
+1, [(Name, Term)]
ntys); Name -> CaseBuilder Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> String -> Name
sMN Int
v String
b)
groupCons :: [Clause] -> CaseBuilder [Group]
groupCons :: [([Pat], (Term, Term))] -> CaseBuilder [Group]
groupCons cs :: [([Pat], (Term, Term))]
cs = [Group] -> [([Pat], (Term, Term))] -> CaseBuilder [Group]
forall (m :: * -> *).
Monad m =>
[Group] -> [([Pat], (Term, Term))] -> m [Group]
gc [] [([Pat], (Term, Term))]
cs
where
gc :: [Group] -> [([Pat], (Term, Term))] -> m [Group]
gc acc :: [Group]
acc [] = [Group] -> m [Group]
forall (m :: * -> *) a. Monad m => a -> m a
return [Group]
acc
gc acc :: [Group]
acc ((p :: Pat
p : ps :: [Pat]
ps, res :: (Term, Term)
res) : cs :: [([Pat], (Term, Term))]
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] -> [([Pat], (Term, Term))] -> m [Group]
gc [Group]
acc' [([Pat], (Term, Term))]
cs
addGroup :: Pat -> [Pat] -> (Term, Term) -> [Group] -> m [Group]
addGroup p :: Pat
p ps :: [Pat]
ps res :: (Term, Term)
res acc :: [Group]
acc = case Pat
p of
PCon uniq :: Bool
uniq con :: Name
con i :: Int
i args :: [Pat]
args -> [Group] -> m [Group]
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] -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addg Bool
uniq (Name -> Int -> ConType
CName Name
con Int
i) [Pat]
args ([Pat]
ps, (Term, Term)
res) [Group]
acc
PConst cval :: Const
cval -> [Group] -> m [Group]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Group] -> m [Group]) -> [Group] -> m [Group]
forall a b. (a -> b) -> a -> b
$ Const -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addConG Const
cval ([Pat]
ps, (Term, Term)
res) [Group]
acc
PSuc n :: Pat
n -> [Group] -> m [Group]
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] -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addg Bool
False ConType
CSuc [Pat
n] ([Pat]
ps, (Term, Term)
res) [Group]
acc
PReflected fn :: Name
fn args :: [Pat]
args -> [Group] -> m [Group]
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] -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addg Bool
False (Name -> ConType
CFn Name
fn) [Pat]
args ([Pat]
ps, (Term, Term)
res) [Group]
acc
pat :: 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]
++ " is not a constructor or constant (can't happen)"
addg :: Bool
-> ConType -> [Pat] -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addg uniq :: Bool
uniq c :: ConType
c conargs :: [Pat]
conargs res :: ([Pat], (Term, Term))
res []
= [Bool -> ConType -> [([Pat], ([Pat], (Term, Term)))] -> Group
ConGroup Bool
uniq ConType
c [([Pat]
conargs, ([Pat], (Term, Term))
res)]]
addg uniq :: Bool
uniq c :: ConType
c conargs :: [Pat]
conargs res :: ([Pat], (Term, Term))
res (g :: Group
g@(ConGroup _ c' :: ConType
c' cs :: [([Pat], ([Pat], (Term, Term)))]
cs):gs :: [Group]
gs)
| ConType
c ConType -> ConType -> Bool
forall a. Eq a => a -> a -> Bool
== ConType
c' = Bool -> ConType -> [([Pat], ([Pat], (Term, Term)))] -> Group
ConGroup Bool
uniq ConType
c ([([Pat], ([Pat], (Term, Term)))]
cs [([Pat], ([Pat], (Term, Term)))]
-> [([Pat], ([Pat], (Term, Term)))]
-> [([Pat], ([Pat], (Term, Term)))]
forall a. [a] -> [a] -> [a]
++ [([Pat]
conargs, ([Pat], (Term, Term))
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] -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addg Bool
uniq ConType
c [Pat]
conargs ([Pat], (Term, Term))
res [Group]
gs
addConG :: Const -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addConG con :: Const
con res :: ([Pat], (Term, Term))
res [] = [Bool -> ConType -> [([Pat], ([Pat], (Term, Term)))] -> Group
ConGroup Bool
False (Const -> ConType
CConst Const
con) [([], ([Pat], (Term, Term))
res)]]
addConG con :: Const
con res :: ([Pat], (Term, Term))
res (g :: Group
g@(ConGroup False (CConst n :: Const
n) cs :: [([Pat], ([Pat], (Term, Term)))]
cs) : gs :: [Group]
gs)
| Const
con Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
n = Bool -> ConType -> [([Pat], ([Pat], (Term, Term)))] -> Group
ConGroup Bool
False (Const -> ConType
CConst Const
n) ([([Pat], ([Pat], (Term, Term)))]
cs [([Pat], ([Pat], (Term, Term)))]
-> [([Pat], ([Pat], (Term, Term)))]
-> [([Pat], ([Pat], (Term, Term)))]
forall a. [a] -> [a] -> [a]
++ [([], ([Pat], (Term, Term))
res)]) Group -> [Group] -> [Group]
forall a. a -> [a] -> [a]
: [Group]
gs
addConG con :: Const
con res :: ([Pat], (Term, Term))
res (g :: Group
g : gs :: [Group]
gs) = Group
g Group -> [Group] -> [Group]
forall a. a -> [a] -> [a]
: Const -> ([Pat], (Term, Term)) -> [Group] -> [Group]
addConG Const
con ([Pat], (Term, Term))
res [Group]
gs
varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
varRule :: [Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
varRule (v :: Name
v : vs :: [Name]
vs) alts :: [([Pat], (Term, Term))]
alts err :: SC
err =
do [([Pat], (Term, Term))]
alts' <- (([Pat], (Term, Term))
-> ReaderT ErasureInfo (State CS) ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))]
-> ReaderT ErasureInfo (State CS) [([Pat], (Term, Term))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> ([Pat], (Term, Term))
-> ReaderT ErasureInfo (State CS) ([Pat], (Term, Term))
forall (m :: * -> *) a b a.
MonadState (a, b, [(Name, Term)]) m =>
Name -> ([Pat], (a, Term)) -> m ([Pat], (a, Term))
repVar Name
v) [([Pat], (Term, Term))]
alts
[Name] -> [([Pat], (Term, Term))] -> SC -> CaseBuilder SC
match [Name]
vs [([Pat], (Term, Term))]
alts' SC
err
where
repVar :: Name -> ([Pat], (a, Term)) -> m ([Pat], (a, Term))
repVar v :: Name
v (PV p :: Name
p ty :: Term
ty : ps :: [Pat]
ps , (lhs :: a
lhs, res :: Term
res))
= do (cs :: a
cs, i :: b
i, ntys :: [(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 (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 v :: Name
v (PAny : ps :: [Pat]
ps , res :: (a, Term)
res) = ([Pat], (a, Term)) -> m ([Pat], (a, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a, Term)
res)
repVar v :: Name
v (PTyPat : ps :: [Pat]
ps , res :: (a, Term)
res) = ([Pat], (a, Term)) -> m ([Pat], (a, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
ps, (a, Term)
res)
depatt :: [Name] -> SC -> SC
depatt :: [Name] -> SC -> SC
depatt ns :: [Name]
ns tm :: SC
tm = [(Name, (Name, [Name]))] -> SC -> SC
dp [] SC
tm
where
dp :: [(Name, (Name, [Name]))] -> SC -> SC
dp ms :: [(Name, (Name, [Name]))]
ms (STerm tm :: Term
tm) = Term -> SC
forall t. t -> SC' t
STerm ([(Name, (Name, [Name]))] -> Term -> Term
forall n. Eq n => [(n, (n, [n]))] -> TT n -> TT n
applyMaps [(Name, (Name, [Name]))]
ms Term
tm)
dp ms :: [(Name, (Name, [Name]))]
ms (Case up :: CaseType
up x :: Name
x alts :: [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 ms :: [(Name, (Name, [Name]))]
ms sc :: SC
sc = SC
sc
dpa :: [(Name, (Name, [Name]))] -> Name -> CaseAlt' Term -> CaseAlt' Term
dpa ms :: [(Name, (Name, [Name]))]
ms x :: Name
x (ConCase n :: Name
n i :: Int
i args :: [Name]
args sc :: 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 ms :: [(Name, (Name, [Name]))]
ms x :: Name
x (FnCase n :: Name
n args :: [Name]
args sc :: 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 ms :: [(Name, (Name, [Name]))]
ms x :: Name
x (ConstCase c :: Const
c sc :: 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 ms :: [(Name, (Name, [Name]))]
ms x :: Name
x (SucCase n :: Name
n sc :: 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 ms :: [(Name, (Name, [Name]))]
ms x :: Name
x (DefaultCase sc :: 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 :: [(n, (n, [n]))] -> TT n -> TT n
applyMaps ms :: [(n, (n, [n]))]
ms f :: TT n
f@(App _ _ _)
| (P nt :: NameType
nt cn :: n
cn pty :: TT n
pty, args :: [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
f
= let args' :: [TT n]
args' = (TT n -> TT n) -> [TT n] -> [TT n]
forall a b. (a -> b) -> [a] -> [b]
map ([(n, (n, [n]))] -> TT n -> TT n
applyMaps [(n, (n, [n]))]
ms) [TT n]
args in
[(n, (n, [n]))] -> NameType -> n -> TT n -> [TT n] -> TT n
forall t.
Eq t =>
[(t, (t, [t]))] -> NameType -> t -> TT t -> [TT t] -> TT t
applyMap [(n, (n, [n]))]
ms NameType
nt n
cn TT n
pty [TT n]
args'
where
applyMap :: [(t, (t, [t]))] -> NameType -> t -> TT t -> [TT t] -> TT t
applyMap [] nt :: NameType
nt cn :: t
cn pty :: TT t
pty args' :: [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 ((x :: t
x, (n :: t
n, args :: [t]
args)) : ms :: [(t, (t, [t]))]
ms) nt :: NameType
nt cn :: t
cn pty :: TT t
pty args' :: [TT t]
args'
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (([t] -> 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 (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 n :: a
n (P _ n' :: a
n' _) = a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n'
same _ _ = Bool
False
applyMaps ms :: [(n, (n, [n]))]
ms (App s :: AppStatus n
s f :: TT n
f a :: TT n
a) = AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
s ([(n, (n, [n]))] -> TT n -> TT n
applyMaps [(n, (n, [n]))]
ms TT n
f) ([(n, (n, [n]))] -> TT n -> TT n
applyMaps [(n, (n, [n]))]
ms TT n
a)
applyMaps ms :: [(n, (n, [n]))]
ms t :: TT n
t = TT n
t
prune :: Bool
-> SC -> SC
prune :: Bool -> SC -> SC
prune proj :: Bool
proj (Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' Term]
alts) = case [CaseAlt' Term]
alts' of
[] -> SC
forall t. SC' t
ImpossibleCase
as :: [CaseAlt' Term]
as@[ConCase cn :: Name
cn i :: Int
i args :: [Name]
args sc :: 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 cn :: Name
cn sc :: SC
sc]
| Bool
proj
-> Name -> Name -> Int -> SC -> SC
projRep Name
cn Name
n (-1) (SC -> SC) -> SC -> SC
forall a b. (a -> b) -> a -> b
$ Bool -> SC -> SC
prune Bool
proj SC
sc
[ConstCase _ sc :: SC
sc]
-> Bool -> SC -> SC
prune Bool
proj SC
sc
[s :: CaseAlt' Term
s@(SucCase _ _), DefaultCase dc :: 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 0) SC
dc, CaseAlt' Term
s]
as :: [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 cn :: Name
cn i :: Int
i ns :: [Name]
ns sc :: 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 cn :: Name
cn ns :: [Name]
ns sc :: 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 c :: Const
c sc :: 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 n :: Name
n sc :: 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) = 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 Erased)) = Bool
True
erased (DefaultCase ImpossibleCase) = Bool
True
erased _ = Bool
False
projRep :: Name -> Name -> Int -> SC -> SC
projRep :: Name -> Name -> Int -> SC -> SC
projRep arg :: Name
arg n :: Name
n i :: Int
i (Case up :: CaseType
up x :: Name
x alts :: [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 arg :: Name
arg n :: Name
n i :: Int
i (Case up :: CaseType
up x :: Name
x alts :: [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 arg :: Name
arg n :: Name
n i :: Int
i (ProjCase t :: Term
t alts :: [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 arg :: Name
arg n :: Name
n i :: Int
i (STerm t :: 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 arg :: Name
arg n :: Name
n i :: Int
i c :: SC
c = SC
c
projRepAlt :: Name -> Name -> Int -> CaseAlt' Term -> CaseAlt' Term
projRepAlt arg :: Name
arg n :: Name
n i :: Int
i (ConCase cn :: Name
cn t :: Int
t args :: [Name]
args rhs :: 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 arg :: Name
arg n :: Name
n i :: Int
i (FnCase cn :: Name
cn args :: [Name]
args rhs :: 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 arg :: Name
arg n :: Name
n i :: Int
i (ConstCase t :: Const
t rhs :: 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 arg :: Name
arg n :: Name
n i :: Int
i (SucCase sn :: Name
sn rhs :: 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 arg :: Name
arg n :: Name
n i :: Int
i (DefaultCase rhs :: 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 arg :: n
arg n :: n
n i :: Int
i t :: 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 _ t :: SC
t = SC
t
removeUnreachable :: SC -> SC
removeUnreachable :: SC -> SC
removeUnreachable sc :: SC
sc = [(Name, Int)] -> SC -> SC
ru [] SC
sc
where
ru :: [(Name, Int)] -> SC -> SC
ru :: [(Name, Int)] -> SC -> SC
ru checked :: [(Name, Int)]
checked (Case t :: CaseType
t n :: Name
n alts :: [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 checked :: [(Name, Int)]
checked t :: SC
t = SC
t
dropImpossible :: Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible Nothing alts :: [CaseAlt' t]
alts = [CaseAlt' t]
alts
dropImpossible (Just t :: Int
t) [] = []
dropImpossible (Just t :: Int
t) (ConCase con :: Name
con tag :: Int
tag args :: [Name]
args sc :: SC' t
sc : rest :: [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 t :: Int
t) (c :: CaseAlt' t
c : rest :: [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 checked :: [(Name, Int)]
checked var :: Name
var (ConCase con :: Name
con tag :: Int
tag args :: [Name]
args sc :: 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 checked :: [(Name, Int)]
checked var :: Name
var (FnCase n :: Name
n args :: [Name]
args sc :: 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 checked :: [(Name, Int)]
checked var :: Name
var (ConstCase c :: Const
c sc :: 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 checked :: [(Name, Int)]
checked var :: Name
var (SucCase n :: Name
n sc :: 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 checked :: [(Name, Int)]
checked var :: Name
var (DefaultCase sc :: 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 n :: Name
n i :: Int
i checked :: [(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 (\x :: (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 ns :: [Name]
ns checked :: [(Name, Int)]
checked = ((Name, Int) -> Bool) -> [(Name, Int)] -> [(Name, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\x :: (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 ns :: [Name]
ns (STerm (Bind x :: Name
x (Lam _ _) sc :: Term
sc)) tm :: [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 x :: CaseDef
x = CaseDef
x
substSC :: Name -> Name -> SC -> SC
substSC :: Name -> Name -> SC -> SC
substSC n :: Name
n repl :: Name
repl (Case up :: CaseType
up n' :: Name
n' alts :: [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 n :: Name
n repl :: Name
repl (STerm t :: 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 n :: Name
n repl :: Name
repl (UnmatchedCase errmsg :: String
errmsg) = String -> SC
forall t. String -> SC' t
UnmatchedCase String
errmsg
substSC n :: Name
n repl :: Name
repl ImpossibleCase = SC
forall t. SC' t
ImpossibleCase
substSC n :: Name
n repl :: Name
repl sc :: SC
sc = String -> SC
forall a. HasCallStack => String -> a
error (String -> SC) -> String -> SC
forall a b. (a -> b) -> a -> b
$ "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 n :: Name
n repl :: Name
repl (ConCase cn :: Name
cn a :: Int
a ns :: [Name]
ns sc :: 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 n :: Name
n repl :: Name
repl (FnCase fn :: Name
fn ns :: [Name]
ns sc :: 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 n :: Name
n repl :: Name
repl (ConstCase c :: Const
c sc :: 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 n :: Name
n repl :: Name
repl (SucCase n' :: Name
n' sc :: 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 n :: Name
n repl :: Name
repl (DefaultCase sc :: 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 n :: Name
n arg :: Name
arg (Case up :: CaseType
up x :: Name
x alts :: [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 n :: Name
n arg :: Name
arg (Case up :: CaseType
up x :: Name
x alts :: [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 n :: Name
n arg :: Name
arg (ProjCase t :: t
t alts :: [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 n :: Name
n arg :: Name
arg c :: SC' t
c = SC' t
c
mkForceAlt :: Name -> Name -> CaseAlt' t -> CaseAlt' t
mkForceAlt n :: Name
n arg :: Name
arg (ConCase cn :: Name
cn t :: Int
t args :: [Name]
args rhs :: 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 n :: Name
n arg :: Name
arg (FnCase cn :: Name
cn args :: [Name]
args rhs :: 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 n :: Name
n arg :: Name
arg (ConstCase t :: Const
t rhs :: 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 n :: Name
n arg :: Name
arg (SucCase sn :: Name
sn rhs :: 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 n :: Name
n arg :: Name
arg (DefaultCase rhs :: 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)