{-|
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
showList :: [CaseDef] -> ShowS
$cshowList :: [CaseDef] -> ShowS
show :: CaseDef -> String
$cshow :: CaseDef -> String
showsPrec :: Int -> CaseDef -> ShowS
$cshowsPrec :: Int -> CaseDef -> ShowS
Show

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

type SC = SC' Term

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

type CaseAlt = CaseAlt' Term

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

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

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


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

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

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

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

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

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

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

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

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

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

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

-- 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 _ n :: Name
n _) = [Name
n]
directUse (Bind n :: Name
n (Let _ t :: Term
t v :: Term
v) sc :: Term
sc) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
v [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Term -> [Name]
directUse Term
sc [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n])
                                        [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
t
directUse (Bind n :: Name
n b :: Binder Term
b sc :: Term
sc) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Term -> [Name]
directUse Term
sc [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n])
directUse fn :: Term
fn@(App _ f :: Term
f a :: Term
a)
    | (P Ref (UN pfk :: Text
pfk) _, [App _ e :: Term
e w :: Term
w]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn,
         Text
pfk Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "prim_fork"
             = Term -> [Name]
directUse Term
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
directUse Term
w -- HACK so that fork works
    | (P Ref (UN fce :: Text
fce) _, [_, _, a :: Term
a]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
fn,
         Text
fce Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Force"
             = Term -> [Name]
directUse Term
a -- forcing a value counts as a use
    | (P Ref n :: Name
n _, args :: [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 _ _) n :: Name
n _, args :: [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 x :: Term
x i :: Int
i) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
directUse Term
x
directUse _ = []

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

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

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

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

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

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

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

type ErasureInfo = Name -> [Int]  -- 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 :: ErasureInfo -> CaseBuilder a -> CS -> (a, CS)
runCaseBuilder ei :: ErasureInfo
ei bld :: CaseBuilder a
bld = State CS a -> CS -> (a, CS)
forall s a. State s a -> s -> (a, s)
runState (State CS a -> CS -> (a, CS)) -> State CS a -> CS -> (a, CS)
forall a b. (a -> b) -> a -> b
$ CaseBuilder a -> ErasureInfo -> State CS a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CaseBuilder a
bld ErasureInfo
ei

data Phase = CoverageCheck [Int] -- 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
showList :: [Phase] -> ShowS
$cshowList :: [Phase] -> ShowS
show :: Phase -> String
$cshow :: Phase -> String
showsPrec :: Int -> Phase -> ShowS
$cshowsPrec :: Int -> Phase -> ShowS
Show, Phase -> Phase -> Bool
(Phase -> Phase -> Bool) -> (Phase -> Phase -> Bool) -> Eq Phase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Phase -> Phase -> Bool
$c/= :: Phase -> Phase -> Bool
== :: Phase -> Phase -> Bool
$c== :: Phase -> Phase -> Bool
Eq)

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

          -- 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 (avs :: t Name
avs, l :: [Pat]
l, c :: b
c)
               | Phase
phase Phase -> Phase -> Bool
forall a. Eq a => a -> a -> Bool
/= Phase
CompileTime Bool -> Bool -> Bool
|| Bool
reflect = ([Pat], b) -> TC ([Pat], b)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)
               | Bool
otherwise = do (Name -> TC ()) -> t Name -> TC ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Pat] -> Name -> TC ()
acc [Pat]
l) t Name
avs
                                ([Pat], b) -> TC ([Pat], b)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Pat]
l, b
c)

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

data Pat = PCon Bool Name Int [Pat]
         | PConst Const
         | PInferred Pat
         | PV Name Type
         | PSuc Pat -- 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
showList :: [Pat] -> ShowS
$cshowList :: [Pat] -> ShowS
show :: Pat -> String
$cshow :: Pat -> String
showsPrec :: Int -> Pat -> ShowS
$cshowsPrec :: Int -> Pat -> ShowS
Show

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

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

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

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

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

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

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

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

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

    toPat' _ t :: Term
t = Pat
PAny

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

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

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

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

-- 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)]
-> [([Pat], (Term, Term))]
-> [Bool]
-> ([Name], [([Pat], (Term, Term))])
order _ []  cs :: [([Pat], (Term, Term))]
cs cans :: [Bool]
cans = ([], [([Pat], (Term, Term))]
cs)
order _ ns' :: [(Name, Bool)]
ns' [] cans :: [Bool]
cans = (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
ns', [])
order (CoverageCheck pos :: [Int]
pos) ns' :: [(Name, Bool)]
ns' cs :: [([Pat], (Term, Term))]
cs cans :: [Bool]
cans
    = let ns_out :: [Name]
ns_out = Int -> [Name] -> [Name] -> [Name]
forall a. Int -> [a] -> [a] -> [a]
pick 0 [] (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
ns')
          cs_out :: [([Pat], (Term, Term))]
cs_out = (([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))] -> [([Pat], (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
forall a b. ([a], b) -> ([a], b)
pickClause [([Pat], (Term, Term))]
cs in
          ([Name]
ns_out, [([Pat], (Term, Term))]
cs_out)
  where
    pickClause :: ([a], b) -> ([a], b)
pickClause (pats :: [a]
pats, def :: b
def) = (Int -> [a] -> [a] -> [a]
forall a. Int -> [a] -> [a] -> [a]
pick 0 [] [a]
pats, b
def)

    -- 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 i :: Int
i skipped :: [a]
skipped [] = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
skipped
    pick i :: Int
i skipped :: [a]
skipped (x :: a
x : xs :: [a]
xs)
         | Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
pos = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a] -> [a]
pick (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [a]
skipped [a]
xs
         | Bool
otherwise    = Int -> [a] -> [a] -> [a]
pick (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
skipped) [a]
xs

order phase :: Phase
phase ns' :: [(Name, Bool)]
ns' cs :: [([Pat], (Term, Term))]
cs cans :: [Bool]
cans
    = let patnames :: [[((Name, Bool), (Bool, Pat))]]
patnames = [[((Name, Bool), (Bool, Pat))]] -> [[((Name, Bool), (Bool, Pat))]]
forall a. [[a]] -> [[a]]
transpose (([(Bool, Pat)] -> [((Name, Bool), (Bool, Pat))])
-> [[(Bool, Pat)]] -> [[((Name, Bool), (Bool, Pat))]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Bool)] -> [(Bool, Pat)] -> [((Name, Bool), (Bool, Pat))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Name, Bool)]
ns') (([Pat] -> [(Bool, Pat)]) -> [[Pat]] -> [[(Bool, Pat)]]
forall a b. (a -> b) -> [a] -> [b]
map ([Bool] -> [Pat] -> [(Bool, Pat)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
cans) ((([Pat], (Term, Term)) -> [Pat])
-> [([Pat], (Term, Term))] -> [[Pat]]
forall a b. (a -> b) -> [a] -> [b]
map ([Pat], (Term, Term)) -> [Pat]
forall a b. (a, b) -> a
fst [([Pat], (Term, Term))]
cs)))
          -- 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
          (patnames_ord :: [[((Name, Bool), (Bool, Pat))]]
patnames_ord, patnames_rest :: [[((Name, Bool), (Bool, Pat))]]
patnames_rest)
                = ([((Name, Bool), (Bool, Pat))] -> Bool)
-> [[((Name, Bool), (Bool, Pat))]]
-> ([[((Name, Bool), (Bool, Pat))]],
    [[((Name, Bool), (Bool, Pat))]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
Data.List.partition ([(Bool, Pat)] -> Bool
noClash ([(Bool, Pat)] -> Bool)
-> ([((Name, Bool), (Bool, Pat))] -> [(Bool, Pat)])
-> [((Name, Bool), (Bool, Pat))]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Name, Bool), (Bool, Pat)) -> (Bool, Pat))
-> [((Name, Bool), (Bool, Pat))] -> [(Bool, Pat)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Bool), (Bool, Pat)) -> (Bool, Pat)
forall a b. (a, b) -> b
snd) [[((Name, Bool), (Bool, Pat))]]
patnames
          patnames_ord' :: [[((Name, Bool), (Bool, Pat))]]
patnames_ord' = case Phase
phase of
                               CompileTime -> [[((Name, Bool), (Bool, Pat))]]
patnames_ord
                               -- reversing tends to make better case trees
                               -- and helps erasure
                               RunTime -> [[((Name, Bool), (Bool, Pat))]] -> [[((Name, Bool), (Bool, Pat))]]
forall a. [a] -> [a]
reverse [[((Name, Bool), (Bool, Pat))]]
patnames_ord
          pats' :: [[((Name, Bool), (Bool, Pat))]]
pats' = [[((Name, Bool), (Bool, Pat))]] -> [[((Name, Bool), (Bool, Pat))]]
forall a. [[a]] -> [[a]]
transpose (([((Name, Bool), (Bool, Pat))]
 -> [((Name, Bool), (Bool, Pat))] -> Ordering)
-> [[((Name, Bool), (Bool, Pat))]]
-> [[((Name, Bool), (Bool, Pat))]]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy [((Name, Bool), (Bool, Pat))]
-> [((Name, Bool), (Bool, Pat))] -> Ordering
forall a a a a a.
Ord a =>
[((a, a), (a, Pat))] -> [((a, a), (a, Pat))] -> Ordering
moreDistinct [[((Name, Bool), (Bool, Pat))]]
patnames_ord'
                                       [[((Name, Bool), (Bool, Pat))]]
-> [[((Name, Bool), (Bool, Pat))]]
-> [[((Name, Bool), (Bool, Pat))]]
forall a. [a] -> [a] -> [a]
++ [[((Name, Bool), (Bool, Pat))]]
patnames_rest) in
          ([[((Name, Bool), (Bool, Pat))]] -> [Name]
forall b b b. [[((b, b), b)]] -> [b]
getNOrder [[((Name, Bool), (Bool, Pat))]]
pats', ([((Name, Bool), (Bool, Pat))]
 -> ([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [[((Name, Bool), (Bool, Pat))]]
-> [([Pat], (Term, Term))]
-> [([Pat], (Term, Term))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [((Name, Bool), (Bool, Pat))]
-> ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
forall a a b a b. [(a, (a, b))] -> (a, b) -> ([b], b)
rebuild [[((Name, Bool), (Bool, Pat))]]
pats' [([Pat], (Term, Term))]
cs)
  where
    getNOrder :: [[((b, b), b)]] -> [b]
getNOrder [] = String -> [b]
forall a. HasCallStack => String -> a
error (String -> [b]) -> String -> [b]
forall a b. (a -> b) -> a -> b
$ "Failed order on " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Name], [([Pat], (Term, Term))]) -> String
forall a. Show a => a -> String
show (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
ns', [([Pat], (Term, Term))]
cs)
    getNOrder (c :: [((b, b), b)]
c : _) = (((b, b), b) -> b) -> [((b, b), b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((b, b) -> b
forall a b. (a, b) -> a
fst ((b, b) -> b) -> (((b, b), b) -> (b, b)) -> ((b, b), b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b), b) -> (b, b)
forall a b. (a, b) -> a
fst) [((b, b), b)]
c

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

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

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

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

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

-- 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]
-> [([Pat], (Term, Term))] -> ([Name], [([Pat], (Term, Term))])
orderByInf vs :: [Name]
vs cs :: [([Pat], (Term, Term))]
cs = let alwaysInf :: [Int]
alwaysInf = [([Pat], (Term, Term))] -> [Int]
forall a b. (Num a, Eq a) => [([Pat], b)] -> [a]
getInf [([Pat], (Term, Term))]
cs in
                       ([Int] -> [Name] -> [Name]
forall a. [Int] -> [a] -> [a]
selectInf [Int]
alwaysInf [Name]
vs,
                        (([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))] -> [([Pat], (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
forall b. ([Pat], b) -> ([Pat], b)
deInf ((([Pat], (Term, Term)) -> ([Pat], (Term, Term)))
-> [([Pat], (Term, Term))] -> [([Pat], (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> ([Pat], (Term, Term)) -> ([Pat], (Term, Term))
selectExp [Int]
alwaysInf) [([Pat], (Term, Term))]
cs))
  where
    getInf :: [([Pat], b)] -> [a]
getInf [] = []
    getInf [(pats :: [Pat]
pats, def :: b
def)] = a -> [Pat] -> [a]
forall a. Num a => a -> [Pat] -> [a]
infPos 0 [Pat]
pats
    getInf ((pats :: [Pat]
pats, def :: b
def) : cs :: [([Pat], b)]
cs) = a -> [Pat] -> [a]
forall a. Num a => a -> [Pat] -> [a]
infPos 0 [Pat]
pats [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [([Pat], b)] -> [a]
getInf [([Pat], b)]
cs

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

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

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

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

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

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

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

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

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

data ConType = CName Name Int -- 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
showList :: [ConType] -> ShowS
$cshowList :: [ConType] -> ShowS
show :: ConType -> String
$cshow :: ConType -> String
showsPrec :: Int -> ConType -> ShowS
$cshowsPrec :: Int -> ConType -> ShowS
Show, ConType -> ConType -> Bool
(ConType -> ConType -> Bool)
-> (ConType -> ConType -> Bool) -> Eq ConType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConType -> ConType -> Bool
$c/= :: ConType -> ConType -> Bool
== :: ConType -> ConType -> Bool
$c== :: ConType -> ConType -> Bool
Eq)

data Group = ConGroup Bool -- 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
showList :: [Group] -> ShowS
$cshowList :: [Group] -> ShowS
show :: Group -> String
$cshow :: Group -> String
showsPrec :: Int -> Group -> ShowS
$cshowsPrec :: Int -> Group -> ShowS
Show

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

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

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

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

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

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

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

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

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

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

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

-- 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], ([Pat], (Term, Term)))]
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
argsToAlt _ [] = ([Name], [Name], [Name], [([Pat], (Term, Term))])
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], [], [])
argsToAlt inacc :: [Int]
inacc rs :: [([Pat], ([Pat], (Term, Term)))]
rs@((r :: [Pat]
r, m :: ([Pat], (Term, Term))
m) : rest :: [([Pat], ([Pat], (Term, Term)))]
rest) = do
    [Name]
newVars <- [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
r
    let (accVars :: [Name]
accVars, inaccVars :: [Name]
inaccVars) = [Name] -> ([Name], [Name])
forall a. [a] -> ([a], [a])
partitionAcc [Name]
newVars
    ([Name], [Name], [Name], [([Pat], (Term, Term))])
-> CaseBuilder ([Name], [Name], [Name], [([Pat], (Term, Term))])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
newVars, [Name]
accVars, [Name]
inaccVars, [([Pat], ([Pat], (Term, Term)))] -> [([Pat], (Term, Term))]
forall a b. [([a], ([a], b))] -> [([a], b)]
addRs [([Pat], ([Pat], (Term, Term)))]
rs)
  where
    -- Create names for new variables arising from the given patterns.
    getNewVars :: [Pat] -> CaseBuilder [Name]
    getNewVars :: [Pat] -> CaseBuilder [Name]
getNewVars [] = [Name] -> CaseBuilder [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    getNewVars ((PV n :: Name
n t :: Term
t) : ns :: [Pat]
ns) = do Name
v <- String -> CaseBuilder Name
getVar "e"
                                    [Name]
nsv <- [Pat] -> CaseBuilder [Name]
getNewVars [Pat]
ns

                                    -- 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.
                                    (cs :: [Term]
cs, i :: Int
i, ntys :: [(Name, Term)]
ntys) <- ReaderT ErasureInfo (State CS) CS
forall s (m :: * -> *). MonadState s m => m s
get
                                    CS -> ReaderT ErasureInfo (State CS) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Term]
cs, Int
i, (Name
v, Term
t) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
ntys)

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

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

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

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

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

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

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

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

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

-- 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 ns :: [Name]
ns tm :: SC
tm = [(Name, (Name, [Name]))] -> SC -> SC
dp [] SC
tm
  where
    dp :: [(Name, (Name, [Name]))] -> SC -> SC
dp ms :: [(Name, (Name, [Name]))]
ms (STerm tm :: Term
tm) = Term -> SC
forall t. t -> SC' t
STerm ([(Name, (Name, [Name]))] -> Term -> Term
forall n. Eq n => [(n, (n, [n]))] -> TT n -> TT n
applyMaps [(Name, (Name, [Name]))]
ms Term
tm)
    dp ms :: [(Name, (Name, [Name]))]
ms (Case up :: CaseType
up x :: Name
x alts :: [CaseAlt' Term]
alts) = CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
x ((CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, (Name, [Name]))] -> Name -> CaseAlt' Term -> CaseAlt' Term
dpa [(Name, (Name, [Name]))]
ms Name
x) [CaseAlt' Term]
alts)
    dp ms :: [(Name, (Name, [Name]))]
ms sc :: SC
sc = SC
sc

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

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

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

-- 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 proj :: Bool
proj (Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' Term]
alts) = case [CaseAlt' Term]
alts' of
    [] -> SC
forall t. SC' t
ImpossibleCase

    -- 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 cn :: Name
cn i :: Int
i args :: [Name]
args sc :: SC
sc]
        | Bool
proj -> let sc' :: SC
sc' = Bool -> SC -> SC
prune Bool
proj SC
sc in
                      if (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SC -> Name -> Bool
isUsed SC
sc') [Name]
args
                         then CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
i [Name]
args SC
sc']
                         else SC
sc'

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

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

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

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

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

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

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

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

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

prune _ t :: SC
t = SC
t

-- Remove any branches we can't reach because of variables we've already
-- tested
removeUnreachable :: SC -> SC
removeUnreachable :: SC -> SC
removeUnreachable sc :: 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 checked :: [(Name, Int)]
checked (Case t :: CaseType
t n :: Name
n alts :: [CaseAlt' Term]
alts)
        = let alts' :: [CaseAlt' Term]
alts' = (CaseAlt' Term -> CaseAlt' Term)
-> [CaseAlt' Term] -> [CaseAlt' Term]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Int)] -> Name -> CaseAlt' Term -> CaseAlt' Term
ruAlt [(Name, Int)]
checked Name
n) (Maybe Int -> [CaseAlt' Term] -> [CaseAlt' Term]
forall t. Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
checked) [CaseAlt' Term]
alts) in
              CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
t Name
n [CaseAlt' Term]
alts'
    ru checked :: [(Name, Int)]
checked t :: SC
t = SC
t

    dropImpossible :: Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible Nothing alts :: [CaseAlt' t]
alts = [CaseAlt' t]
alts
    dropImpossible (Just t :: Int
t) [] = []
    dropImpossible (Just t :: Int
t) (ConCase con :: Name
con tag :: Int
tag args :: [Name]
args sc :: SC' t
sc : rest :: [CaseAlt' t]
rest)
        | Int
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tag = [Name -> Int -> [Name] -> SC' t -> CaseAlt' t
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
con Int
tag [Name]
args SC' t
sc] -- 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 t :: Int
t) (c :: CaseAlt' t
c : rest :: [CaseAlt' t]
rest)
        = CaseAlt' t
c CaseAlt' t -> [CaseAlt' t] -> [CaseAlt' t]
forall a. a -> [a] -> [a]
: Maybe Int -> [CaseAlt' t] -> [CaseAlt' t]
dropImpossible (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
t) [CaseAlt' t]
rest

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

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

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

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

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

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

-- mkForce 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 n :: Name
n arg :: Name
arg (Case up :: CaseType
up x :: Name
x alts :: [CaseAlt' t]
alts) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
arg
        = CaseType -> Name -> [CaseAlt' t] -> SC' t
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n ([CaseAlt' t] -> SC' t) -> [CaseAlt' t] -> SC' t
forall a b. (a -> b) -> a -> b
$ (CaseAlt' t -> CaseAlt' t) -> [CaseAlt' t] -> [CaseAlt' t]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> CaseAlt' t -> CaseAlt' t
mkForceAlt Name
n Name
arg) [CaseAlt' t]
alts

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

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

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

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