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

License     : BSD3
Maintainer  : The Idris Community.

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

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

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

-}

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

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

import Idris.Core.TT

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

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

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

data CaseType = Updatable | Shared
   deriving (CaseType -> CaseType -> Bool
(CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool) -> Eq CaseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CaseType -> CaseType -> Bool
== :: CaseType -> CaseType -> Bool
$c/= :: CaseType -> CaseType -> Bool
/= :: CaseType -> CaseType -> Bool
Eq, Eq CaseType
Eq CaseType =>
(CaseType -> CaseType -> Ordering)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> Bool)
-> (CaseType -> CaseType -> CaseType)
-> (CaseType -> CaseType -> CaseType)
-> Ord CaseType
CaseType -> CaseType -> Bool
CaseType -> CaseType -> Ordering
CaseType -> CaseType -> CaseType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CaseType -> CaseType -> Ordering
compare :: CaseType -> CaseType -> Ordering
$c< :: CaseType -> CaseType -> Bool
< :: CaseType -> CaseType -> Bool
$c<= :: CaseType -> CaseType -> Bool
<= :: CaseType -> CaseType -> Bool
$c> :: CaseType -> CaseType -> Bool
> :: CaseType -> CaseType -> Bool
$c>= :: CaseType -> CaseType -> Bool
>= :: CaseType -> CaseType -> Bool
$cmax :: CaseType -> CaseType -> CaseType
max :: CaseType -> CaseType -> CaseType
$cmin :: CaseType -> CaseType -> CaseType
min :: CaseType -> CaseType -> CaseType
Ord, Int -> CaseType -> ShowS
[CaseType] -> ShowS
CaseType -> String
(Int -> CaseType -> ShowS)
-> (CaseType -> String) -> ([CaseType] -> ShowS) -> Show CaseType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CaseType -> ShowS
showsPrec :: Int -> CaseType -> ShowS
$cshow :: CaseType -> String
show :: CaseType -> String
$cshowList :: [CaseType] -> ShowS
showList :: [CaseType] -> ShowS
Show, (forall x. CaseType -> Rep CaseType x)
-> (forall x. Rep CaseType x -> CaseType) -> Generic CaseType
forall x. Rep CaseType x -> CaseType
forall x. CaseType -> Rep CaseType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CaseType -> Rep CaseType x
from :: forall x. CaseType -> Rep CaseType x
$cto :: forall x. Rep CaseType x -> CaseType
to :: forall x. Rep CaseType x -> CaseType
Generic)

type SC = SC' Term

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

type CaseAlt = CaseAlt' Term

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
runCaseBuilder :: forall a. ErasureInfo -> CaseBuilder a -> CS -> (a, CS)
runCaseBuilder ErasureInfo
ei CaseBuilder a
bld = 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] -- list of positions explicitly given
           | CompileTime
           | RunTime
    deriving (Int -> Phase -> ShowS
[Phase] -> ShowS
Phase -> String
(Int -> Phase -> ShowS)
-> (Phase -> String) -> ([Phase] -> ShowS) -> Show Phase
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Phase -> ShowS
showsPrec :: Int -> Phase -> ShowS
$cshow :: Phase -> String
show :: Phase -> String
$cshowList :: [Phase] -> ShowS
showList :: [Phase] -> ShowS
Show, Phase -> Phase -> Bool
(Phase -> Phase -> Bool) -> (Phase -> Phase -> Bool) -> Eq Phase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Phase -> Phase -> Bool
== :: Phase -> Phase -> Bool
$c/= :: Phase -> Phase -> Bool
/= :: Phase -> Phase -> Bool
Eq)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    toPat' [Term]
_ Term
t = Pat
PAny

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                    [Name] -> CaseBuilder [Name]
forall a. a -> ReaderT ErasureInfo (State CS) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
v Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
nsv)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

prune Bool
_ SC
t = SC
t

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

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

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

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

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

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

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

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

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

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

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

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

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