module Agda.Auto.CaseSplit where
import Control.Monad.State as St hiding (lift)
import Control.Monad.Reader as Rd hiding (lift)
import qualified Control.Monad.State as St
import Control.Monad.IO.Class ( MonadIO(..) )
import Data.Function
import Data.IORef
import Data.Tuple (swap)
import Data.List (elemIndex)
import Data.Monoid ((<>), Sum(..))
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
import Agda.Syntax.Common (Hiding(..))
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Auto.SearchControl
import Agda.Auto.Typecheck
import Agda.Utils.Impossible
import Agda.Utils.Monad (or2M)
import Agda.Utils.List (last1)
abspatvarname :: String
abspatvarname :: String
abspatvarname = String
"\0absurdPattern"
costCaseSplitVeryHigh, costCaseSplitHigh, costCaseSplitLow, costAddVarDepth
:: Cost
costCaseSplitVeryHigh :: Cost
costCaseSplitVeryHigh = Cost
10000
costCaseSplitHigh :: Cost
costCaseSplitHigh = Cost
5000
costCaseSplitLow :: Cost
costCaseSplitLow = Cost
2000
costAddVarDepth :: Cost
costAddVarDepth = Cost
1000
data HI a = HI Hiding a
drophid :: [HI a] -> [a]
drophid :: forall a. [HI a] -> [a]
drophid = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
_ a
x) -> a
x)
type CSPat o = HI (CSPatI o)
type CSCtx o = [HI (MId, MExp o)]
data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]
| CSPatVar Nat
| CSPatExp (MExp o)
| CSWith (MExp o)
| CSAbsurd
| CSOmittedArg
type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]
caseSplitSearch ::
forall o . IORef Int -> Int -> [ConstRef o] ->
Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o ->
CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch :: forall o.
IORef Nat
-> Nat
-> [ConstRef o]
-> Maybe (EqReasoningConsts o)
-> Nat
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch IORef Nat
ticks Nat
nsolwanted [ConstRef o]
chints Maybe (EqReasoningConsts o)
meqr Nat
depthinterval Cost
depth ConstRef o
recdef CSCtx o
ctx MExp o
tt [CSPat o]
pats = do
let branchsearch :: Cost -> CSCtx o -> MExp o ->
([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch :: Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Cost
depth CSCtx o
ctx MExp o
tt ([Nat], Nat, [Nat])
termcheckenv = do
IORef Nat
nsol <- forall a. a -> IO (IORef a)
newIORef Nat
1
Metavar (Exp o) (RefInfo o)
m <- forall a blk. IO (Metavar a blk)
initMeta
IORef (Maybe (MExp o))
sol <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
let trm :: MExp o
trm = forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp o) (RefInfo o)
m
hsol :: IO ()
hsol = do MExp o
trm' <- forall t. ExpandMetas t => t -> IO t
expandMetas MExp o
trm
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe (MExp o))
sol (forall a. a -> Maybe a
Just MExp o
trm')
initcon :: MetaEnv (PB (RefInfo o))
initcon = forall blk. Prop blk -> MetaEnv (PB blk)
mpret
forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
(forall o.
([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond ([Nat], Nat, [Nat])
termcheckenv ConstRef o
recdef MExp o
trm)
forall a b. (a -> b) -> a -> b
$ (case Maybe (EqReasoningConsts o)
meqr of
Maybe (EqReasoningConsts o)
Nothing -> forall a. a -> a
id
Just EqReasoningConsts o
eqr -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (forall o. EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState EqReasoningConsts o
eqr MExp o
trm)
) forall a b. (a -> b) -> a -> b
$ forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch Bool
False (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall o. MExp o -> CExp o
closify) (forall a. [HI a] -> [a]
drophid CSCtx o
ctx))
(forall o. MExp o -> CExp o
closify MExp o
tt) MExp o
trm
ConstDef o
recdefd <- forall a. IORef a -> IO a
readIORef ConstRef o
recdef
let env :: RefInfo o
env = RIEnv { rieHints :: [(ConstRef o, HintMode)]
rieHints = (ConstRef o
recdef, HintMode
HMRecCall) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (, HintMode
HMNormal) [ConstRef o]
chints
, rieDefFreeVars :: Nat
rieDefFreeVars = forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
recdefd
, rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
rieEqReasoningConsts = Maybe (EqReasoningConsts o)
meqr
}
Bool
depreached <- forall blk.
IORef Nat
-> IORef Nat
-> IO ()
-> blk
-> MetaEnv (PB blk)
-> Cost
-> Cost
-> IO Bool
topSearch IORef Nat
ticks IORef Nat
nsol IO ()
hsol RefInfo o
env MetaEnv (PB (RefInfo o))
initcon Cost
depth (Cost
depth forall a. Num a => a -> a -> a
+ Cost
1)
forall a. IORef a -> IO a
readIORef IORef (Maybe (MExp o))
sol
ctx' :: CSCtx o
ctx' = forall {b} {a}. Lift b => Nat -> [HI (a, b)] -> [HI (a, b)]
ff Nat
1 CSCtx o
ctx
ff :: Nat -> [HI (a, b)] -> [HI (a, b)]
ff Nat
_ [] = []
ff Nat
n (HI Hiding
hid (a
id, b
t) : [HI (a, b)]
ctx) = forall a. Hiding -> a -> HI a
HI Hiding
hid (a
id, forall t. Lift t => Nat -> t -> t
lift Nat
n b
t) forall a. a -> [a] -> [a]
: Nat -> [HI (a, b)] -> [HI (a, b)]
ff (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) [HI (a, b)]
ctx
forall o.
(Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
-> Nat
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch' Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Nat
depthinterval Cost
depth ConstRef o
recdef CSCtx o
ctx' MExp o
tt [CSPat o]
pats
caseSplitSearch' :: forall o .
(Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) ->
Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch' :: forall o.
(Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
-> Nat
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch' Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Nat
depthinterval Cost
depth ConstRef o
recdef CSCtx o
ctx MExp o
tt [CSPat o]
pats = do
ConstDef o
recdefd <- forall a. IORef a -> IO a
readIORef ConstRef o
recdef
Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc Cost
depth (forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
recdefd) CSCtx o
ctx MExp o
tt [CSPat o]
pats
where
rc :: Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc :: Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc Cost
depth Nat
_ CSCtx o
_ MExp o
_ [CSPat o]
_ | Cost
depth forall a. Ord a => a -> a -> Bool
< Cost
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
rc Cost
depth Nat
nscrutavoid CSCtx o
ctx MExp o
tt [CSPat o]
pats = do
[Nat]
mblkvar <- forall o. MExp o -> IO [Nat]
getblks MExp o
tt
[Nat] -> IO [Sol o]
fork
[Nat]
mblkvar
where
fork :: [Nat] -> IO [Sol o]
fork :: [Nat] -> IO [Sol o]
fork [Nat]
mblkvar = do
[Sol o]
sols1 <- IO [Sol o]
dobody
case [Sol o]
sols1 of
(Sol o
_:[Sol o]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return [Sol o]
sols1
[] -> do
let r :: [Nat] -> IO [Sol o]
r :: [Nat] -> IO [Sol o]
r [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
r (Nat
v:[Nat]
vs) = do
[Sol o]
sols2 <- [Nat] -> Nat -> IO [Sol o]
splitvar [Nat]
mblkvar Nat
v
case [Sol o]
sols2 of
(Sol o
_:[Sol o]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return [Sol o]
sols2
[] -> [Nat] -> IO [Sol o]
r [Nat]
vs
[Nat] -> IO [Sol o]
r [Nat
nv forall a. Num a => a -> a -> a
- Nat
x | Nat
x <- [Nat
0..Nat
nv]]
where nv :: Nat
nv = forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
1
dobody :: IO [Sol o]
dobody :: IO [Sol o]
dobody = do
case forall o. [MExp o] -> Maybe [Nat]
findperm (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a. [HI a] -> [a]
drophid CSCtx o
ctx)) of
Just [Nat]
perm -> do
let (CSCtx o
ctx', MExp o
tt', [CSPat o]
pats') = forall o.
[Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
applyperm [Nat]
perm CSCtx o
ctx MExp o
tt [CSPat o]
pats
Maybe (MExp o)
res <- Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Cost
depth CSCtx o
ctx' MExp o
tt' (forall o. [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv [CSPat o]
pats')
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Maybe (MExp o)
res of
Just MExp o
trm -> [[(CSCtx o
ctx', [CSPat o]
pats', forall a. a -> Maybe a
Just MExp o
trm)]]
Maybe (MExp o)
Nothing -> []
Maybe [Nat]
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__
splitvar :: [Nat] -> Nat -> IO [Sol o]
splitvar :: [Nat] -> Nat -> IO [Sol o]
splitvar [Nat]
mblkvar Nat
scrut = do
let scruttype :: MExp o
scruttype = forall o. CSCtx o -> Nat -> MExp o
infertypevar CSCtx o
ctx Nat
scrut
case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
scruttype of
App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) MArgList o
_ -> do
ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
Datatype [ConstRef o]
cons [ConstRef o]
_ -> do
[Sol o]
sols <- [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Sol o
sol -> case Sol o
sol of
[] ->
case forall o. [MExp o] -> Maybe [Nat]
findperm (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a. [HI a] -> [a]
drophid CSCtx o
ctx)) of
Just [Nat]
perm ->
let HI Hiding
scrhid(MId
_, MExp o
scrt) = CSCtx o
ctx forall a. [a] -> Nat -> a
!! Nat
scrut
ctx1 :: CSCtx o
ctx1 = forall a. Nat -> [a] -> [a]
take Nat
scrut CSCtx o
ctx forall a. [a] -> [a] -> [a]
++ (forall a. Hiding -> a -> HI a
HI Hiding
scrhid (String -> MId
Id String
abspatvarname, MExp o
scrt)) forall a. a -> [a] -> [a]
: forall a. Nat -> [a] -> [a]
drop (Nat
scrut forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx
(CSCtx o
ctx', MExp o
_, [CSPat o]
pats') = forall o.
[Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
applyperm [Nat]
perm CSCtx o
ctx1 MExp o
tt ([CSPat o]
pats)
in [(CSCtx o
ctx', [CSPat o]
pats', forall a. Maybe a
Nothing)]
Maybe [Nat]
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__
Sol o
_ -> Sol o
sol
) [Sol o]
sols
where
dobranches :: [ConstRef o] -> IO [Sol o]
dobranches :: [ConstRef o] -> IO [Sol o]
dobranches [] = forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
dobranches (ConstRef o
con : [ConstRef o]
cons) = do
ConstDef o
cond <- forall a. IORef a -> IO a
readIORef ConstRef o
con
let ff :: MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
ff MExp o
t = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
t of
Pi Maybe (UId o)
_ Hiding
h Bool
_ MExp o
it (Abs MId
id MExp o
ot) ->
let ([((Hiding, Nat), MId, MExp o)]
xs, MExp o
inft) = MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
ff MExp o
ot
in (((Hiding
h, Nat
scrut forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
xs), MId
id, forall t. Lift t => Nat -> t -> t
lift (Nat
scrut forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
xs forall a. Num a => a -> a -> a
+ Nat
1) MExp o
it) forall a. a -> [a] -> [a]
: [((Hiding, Nat), MId, MExp o)]
xs, MExp o
inft)
Exp o
_ -> ([], forall t. Lift t => Nat -> t -> t
lift Nat
scrut MExp o
t)
([((Hiding, Nat), MId, MExp o)]
newvars, MExp o
inftype) = MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
ff (forall o. ConstDef o -> MExp o
cdtype ConstDef o
cond)
constrapp :: MExp o
constrapp = forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. ConstRef o -> Elr o
Const ConstRef o
con) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\MArgList o
xs ((Hiding
h, Nat
v), MId
_, MExp o
_) -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
h (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Nat -> Elr o
Var Nat
v) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) MArgList o
xs) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil) (forall a. [a] -> [a]
reverse [((Hiding, Nat), MId, MExp o)]
newvars))
pconstrapp :: CSPatI o
pconstrapp = forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef o
con (forall a b. (a -> b) -> [a] -> [b]
map (\((Hiding
hid, Nat
v), MId
_, MExp o
_) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Nat -> CSPatI o
CSPatVar Nat
v)) [((Hiding, Nat), MId, MExp o)]
newvars)
thesub :: MExp o -> MExp o
thesub = forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
scrut (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
newvars) MExp o
constrapp
Id String
newvarprefix = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ (forall a. [HI a] -> [a]
drophid CSCtx o
ctx) forall a. [a] -> Nat -> a
!! Nat
scrut
ctx1 :: CSCtx o
ctx1 = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
take Nat
scrut CSCtx o
ctx) forall a. [a] -> [a] -> [a]
++
forall a. [a] -> [a]
reverse (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\((Hiding
hid, Nat
_), MId
id, MExp o
t) Integer
i ->
forall a. Hiding -> a -> HI a
HI Hiding
hid (String -> MId
Id (case MId
id of {MId
NoId -> String
newvarprefix; Id String
id -> String
id}), MExp o
t)
) [((Hiding, Nat), MId, MExp o)]
newvars [Integer
0..]) forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
drop (Nat
scrut forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx)
tt' :: MExp o
tt' = MExp o -> MExp o
thesub MExp o
tt
pats' :: [CSPat o]
pats' = forall a b. (a -> b) -> [a] -> [b]
map (forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
scrut (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
newvars) CSPatI o
pconstrapp MExp o
constrapp) [CSPat o]
pats
scruttype' :: MExp o
scruttype' = MExp o -> MExp o
thesub MExp o
scruttype
case forall o. MExp o -> MExp o -> Maybe [(Nat, MExp o)]
unifyexp MExp o
inftype MExp o
scruttype' of
Maybe [(Nat, MExp o)]
Nothing -> do
Bool
res <- forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal Nat
scrut (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
newvars) MExp o
scruttype' MExp o
inftype
if Bool
res then
[ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
else
forall (m :: * -> *) a. Monad m => a -> m a
return []
Just [(Nat, MExp o)]
unif ->
do
let (CSCtx o
ctx2, MExp o
tt2, [CSPat o]
pats2) = forall o.
CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
removevar CSCtx o
ctx1 MExp o
tt' [CSPat o]
pats' [(Nat, MExp o)]
unif
cost :: Cost
cost
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar Bool -> Bool -> Bool
&& Nat
scrut forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
nscrutavoid Bool -> Bool -> Bool
&& Bool
nothid
= Cost
costCaseSplitLow forall a. Num a => a -> a -> a
+
Cost
costAddVarDepth forall a. Num a => a -> a -> a
*
Nat -> Cost
Cost (forall o. Nat -> [CSPat o] -> Nat
depthofvar Nat
scrut [CSPat o]
pats)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar = Cost
costCaseSplitVeryHigh
| Nat
scrut forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Nat]
mblkvar = Cost
costCaseSplitLow
| Nat
scrut forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
nscrutavoid Bool -> Bool -> Bool
&& Bool
nothid = Cost
costCaseSplitHigh
| Bool
otherwise = Cost
costCaseSplitVeryHigh
nothid :: Bool
nothid = let HI Hiding
hid (MId, MExp o)
_ = CSCtx o
ctx forall a. [a] -> Nat -> a
!! Nat
scrut
in Hiding
hid forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden
[Sol o]
sols <- Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc (Cost
depth forall a. Num a => a -> a -> a
- Cost
cost) (forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
scrut) CSCtx o
ctx2 MExp o
tt2 [CSPat o]
pats2
case [Sol o]
sols of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return []
[Sol o]
_ -> do
[Sol o]
sols2 <- [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Sol o
sol -> forall a b. (a -> b) -> [a] -> [b]
map (\Sol o
sol2 -> Sol o
sol forall a. [a] -> [a] -> [a]
++ Sol o
sol2) [Sol o]
sols2) [Sol o]
sols
DeclCont o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
Exp o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
infertypevar :: CSCtx o -> Nat -> MExp o
infertypevar :: forall o. CSCtx o -> Nat -> MExp o
infertypevar CSCtx o
ctx Nat
v = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ (forall a. [HI a] -> [a]
drophid CSCtx o
ctx) forall a. [a] -> Nat -> a
!! Nat
v
class Replace t u where
type ReplaceWith t u
replace' :: Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace :: Replace t u => Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace :: forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
sv Nat
nnew MExp (ReplaceWith t u)
e t
t = forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
0 MExp (ReplaceWith t u)
e t
t forall r a. Reader r a -> r -> a
`runReader` (Nat
sv, Nat
nnew)
instance Replace t u => Replace (Abs t) (Abs u) where
type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u
replace' :: Nat
-> MExp (ReplaceWith (Abs t) (Abs u))
-> Abs t
-> Reader (Nat, Nat) (Abs u)
replace' Nat
n MExp (ReplaceWith (Abs t) (Abs u))
re (Abs MId
mid t
b) = forall a. MId -> a -> Abs a
Abs MId
mid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) MExp (ReplaceWith (Abs t) (Abs u))
re t
b
instance Replace (Exp o) (MExp o) where
type ReplaceWith (Exp o) (MExp o) = o
replace' :: Nat
-> MExp (ReplaceWith (Exp o) (MExp o))
-> Exp o
-> Reader (Nat, Nat) (MExp o)
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re = \case
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok elr :: Elr o
elr@(Var Nat
v) MArgList o
args -> do
MArgList o
ih <- forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
(Nat
sv, Nat
nnew) <- forall r (m :: * -> *). MonadReader r m => m r
ask
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
if Nat
v forall a. Ord a => a -> a -> Bool
>= Nat
n
then if Nat
v forall a. Num a => a -> a -> a
- Nat
n forall a. Eq a => a -> a -> Bool
== Nat
sv
then forall o. MExp o -> MArgList o -> MExp o
betareduce (forall t. Lift t => Nat -> t -> t
lift Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re) MArgList o
ih
else if Nat
v forall a. Num a => a -> a -> a
- Nat
n forall a. Ord a => a -> a -> Bool
> Nat
sv
then forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok (forall o. Nat -> Elr o
Var (Nat
v forall a. Num a => a -> a -> a
+ Nat
nnew forall a. Num a => a -> a -> a
- Nat
1)) MArgList o
ih
else forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
ih
else forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
ih
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok elr :: Elr o
elr@Const{} MArgList o
args ->
forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
Lam Hiding
hid Abs (MExp o)
b -> forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) MExp (ReplaceWith (Exp o) (MExp o))
re Abs (MExp o)
b
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it Abs (MExp o)
b ->
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re MExp o
it forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re Abs (MExp o)
b
e :: Exp o
e@Sort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM Exp o
e
e :: Exp o
e@AbsurdLambda{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM Exp o
e
instance Replace t u => Replace (MM t (RefInfo o)) u where
type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u
replace' :: Nat
-> MExp (ReplaceWith (MM t (RefInfo o)) u)
-> MM t (RefInfo o)
-> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MM t (RefInfo o)) u)
re = forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MM t (RefInfo o)) u)
re forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__
instance Replace (ArgList o) (ArgList o) where
type ReplaceWith (ArgList o) (ArgList o) = o
replace' :: Nat
-> MExp (ReplaceWith (ArgList o) (ArgList o))
-> ArgList o
-> Reader (Nat, Nat) (ArgList o)
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re ArgList o
args = case ArgList o
args of
ArgList o
ALNil -> forall (m :: * -> *) a. Monad m => a -> m a
return forall o. ArgList o
ALNil
ALCons Hiding
hid MExp o
a MArgList o
as ->
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re MExp o
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as)
ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar MArgList o
as -> forall o. MArgList o -> ArgList o
ALConPar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as
betareduce :: MExp o -> MArgList o -> MExp o
betareduce :: forall o. MExp o -> MArgList o -> MExp o
betareduce MExp o
e MArgList o
args = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MArgList o
args of
ArgList o
ALNil -> MExp o
e
ALCons Hiding
_ MExp o
a MArgList o
rargs -> case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
e of
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
eargs -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr (forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
eargs MArgList o
args)
Lam Hiding
_ (Abs MId
_ MExp o
b) -> forall o. MExp o -> MArgList o -> MExp o
betareduce (forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
0 Nat
0 MExp o
a MExp o
b) MArgList o
rargs
Exp o
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar MArgList o
as -> forall a. HasCallStack => a
__IMPOSSIBLE__
concatargs :: MArgList o -> MArgList o -> MArgList o
concatargs :: forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MArgList o
xs of
ArgList o
ALNil -> MArgList o
ys
ALCons Hiding
hid MExp o
x MArgList o
xs -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp o
x (forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys)
ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar MArgList o
as -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. MArgList o -> ArgList o
ALConPar (forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys)
replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
sv Nat
nnew CSPatI o
rp MExp o
re = CSPat o -> CSPat o
r
where
r :: CSPat o -> CSPat o
r :: CSPat o -> CSPat o
r (HI Hiding
hid (CSPatConApp ConstRef o
c [CSPat o]
ps)) = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef o
c (forall a b. (a -> b) -> [a] -> [b]
map CSPat o -> CSPat o
r [CSPat o]
ps))
r (HI Hiding
hid (CSPatVar Nat
v)) | Nat
v forall a. Eq a => a -> a -> Bool
== Nat
sv = forall a. Hiding -> a -> HI a
HI Hiding
hid CSPatI o
rp
| Nat
v forall a. Ord a => a -> a -> Bool
> Nat
sv = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Nat -> CSPatI o
CSPatVar (Nat
v forall a. Num a => a -> a -> a
+ Nat
nnew forall a. Num a => a -> a -> a
- Nat
1))
| Bool
otherwise = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Nat -> CSPatI o
CSPatVar Nat
v)
r (HI Hiding
hid (CSPatExp MExp o
e)) = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. MExp o -> CSPatI o
CSPatExp forall a b. (a -> b) -> a -> b
$ forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
sv Nat
nnew MExp o
re MExp o
e)
r p :: CSPat o
p@(HI Hiding
_ CSPatI o
CSOmittedArg) = CSPat o
p
r CSPat o
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
type Assignments o = [(Nat, Exp o)]
class Unify t where
type UnifiesTo t
unify' :: t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
unify :: Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
unify :: forall t. Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
unify t
t t
u = forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' t
t t
u forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
`execStateT` []
notequal :: Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal :: forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal Nat
fstnew Nat
nbnew t
t1 t
t2 = forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' t
t1 t
t2 forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (Nat
fstnew, Nat
nbnew)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` []
instance (Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) where
type UnifiesTo (MM t (RefInfo o)) = o
unify' :: MM t (RefInfo o)
-> MM t (RefInfo o)
-> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()
unify' = forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__
notequal' :: MM t (RefInfo o)
-> MM t (RefInfo o)
-> ReaderT
(Nat, Nat)
(StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO)
Bool
notequal' = forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__
unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar :: forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e = do
Assignments o
unif <- forall s (m :: * -> *). MonadState s m => m s
get
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
v Assignments o
unif of
Maybe (Exp o)
Nothing -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Nat
v, Exp o
e) forall a. a -> [a] -> [a]
:)
Just Exp o
e' -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Exp o
e Exp o
e'
instance Unify t => Unify (Abs t) where
type UnifiesTo (Abs t) = UnifiesTo t
unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe ()
unify' (Abs MId
_ t
b1) (Abs MId
_ t
b2) = forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' t
b1 t
b2
notequal' :: Abs t
-> Abs t
-> ReaderT
(Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool
notequal' (Abs MId
_ t
b1) (Abs MId
_ t
b2) = forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' t
b1 t
b2
instance Unify (Exp o) where
type UnifiesTo (Exp o) = o
unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()
unify' Exp o
e1 Exp o
e2 = case (Exp o
e1, Exp o
e2) of
(App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr1 MArgList o
args1, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr2 MArgList o
args2) | Elr o
elr1 forall a. Eq a => a -> a -> Bool
== Elr o
elr2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
args1 MArgList o
args2
(Lam Hiding
hid1 Abs (MExp o)
b1, Lam Hiding
hid2 Abs (MExp o)
b2) | Hiding
hid1 forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
(Pi Maybe (UId o)
_ Hiding
hid1 Bool
_ MExp o
a1 Abs (MExp o)
b1, Pi Maybe (UId o)
_ Hiding
hid2 Bool
_ MExp o
a2 Abs (MExp o)
b2) | Hiding
hid1 forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MExp o
a1 MExp o
a2
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
(Sort Sort
_, Sort Sort
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
(App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil), Exp o
_)
| Nat
v forall a. Ord a => a -> Set a -> Bool
`Set.member` (forall t. FreeVars t => t -> Set Nat
freeVars Exp o
e2) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing
(Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil))
| Nat
v forall a. Ord a => a -> Set a -> Bool
`Set.member` (forall t. FreeVars t => t -> Set Nat
freeVars Exp o
e1) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing
(App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil), Exp o
_) -> forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e2
(Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil)) -> forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e1
(Exp o, Exp o)
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing
notequal' :: Exp o
-> Exp o
-> ReaderT
(Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
notequal' Exp o
e1 Exp o
e2 = do
(Nat
fstnew, Nat
nbnew) <- forall r (m :: * -> *). MonadReader r m => m r
ask
Assignments o
unifier <- forall s (m :: * -> *). MonadState s m => m s
get
case (Exp o
e1, Exp o
e2) of
(App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr1 MArgList o
es1, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr2 MArgList o
es2) | Elr o
elr1 forall a. Eq a => a -> a -> Bool
== Elr o
elr2 -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
(Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v2) (NotM ArgList o
ALNil))
| Nat
fstnew forall a. Ord a => a -> a -> Bool
<= Nat
v2 Bool -> Bool -> Bool
&& Nat
v2 forall a. Ord a => a -> a -> Bool
< Nat
fstnew forall a. Num a => a -> a -> a
+ Nat
nbnew ->
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
v2 Assignments o
unifier of
Maybe (Exp o)
Nothing -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Nat
v2, Exp o
e1)forall a. a -> [a] -> [a]
:) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just Exp o
e2' -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' Exp o
e1 Exp o
e2'
(App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c1) MArgList o
es1, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c2) MArgList o
es2) -> do
ConstDef o
cd1 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef o
c1
ConstDef o
cd2 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef o
c2
case (forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd1, forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd2) of
(Constructor{}, Constructor{}) -> if ConstRef o
c1 forall a. Eq a => a -> a -> Bool
== ConstRef o
c2 then forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
else forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
(DeclCont o, DeclCont o)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
(Exp o, Exp o)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
instance Unify (ArgList o) where
type UnifiesTo (ArgList o) = o
unify' :: ArgList o
-> ArgList o
-> StateT (Assignments (UnifiesTo (ArgList o))) Maybe ()
unify' ArgList o
args1 ArgList o
args2 = case (ArgList o
args1, ArgList o
args2) of
(ArgList o
ALNil, ArgList o
ALNil) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
(ALCons Hiding
hid1 MExp o
a1 MArgList o
as1, ALCons Hiding
hid2 MExp o
a2 MArgList o
as2) | Hiding
hid1 forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MExp o
a1 MExp o
a2
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
(ALConPar MArgList o
as1, ALCons Hiding
_ MExp o
_ MArgList o
as2) -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
(ALCons Hiding
_ MExp o
_ MArgList o
as1, ALConPar MArgList o
as2) -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
(ALConPar MArgList o
as1, ALConPar MArgList o
as2) -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
(ArgList o, ArgList o)
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing
notequal' :: ArgList o
-> ArgList o
-> ReaderT
(Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool
notequal' ArgList o
args1 ArgList o
args2 = case (ArgList o
args1, ArgList o
args2) of
(ALCons Hiding
_ MExp o
e MArgList o
es, ALCons Hiding
_ MExp o
f MArgList o
fs) -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MExp o
e MExp o
f forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es MArgList o
fs
(ALConPar MArgList o
es1, ALConPar MArgList o
es2) -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
(ArgList o, ArgList o)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
unifyexp :: forall o. MExp o -> MExp o -> Maybe [(Nat, MExp o)]
unifyexp MExp o
e1 MExp o
e2 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
unify MExp o
e1 MExp o
e2
class Lift t where
lift' :: Nat -> Nat -> t -> t
lift :: Lift t => Nat -> t -> t
lift :: forall t. Lift t => Nat -> t -> t
lift Nat
0 = forall a. a -> a
id
lift Nat
n = forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
0
instance Lift t => Lift (Abs t) where
lift' :: Nat -> Nat -> Abs t -> Abs t
lift' Nat
n Nat
j (Abs MId
mid t
b) = forall a. MId -> a -> Abs a
Abs MId
mid (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n (Nat
j forall a. Num a => a -> a -> a
+ Nat
1) t
b)
instance Lift t => Lift (MM t r) where
lift' :: Nat -> Nat -> MM t r -> MM t r
lift' Nat
n Nat
j = forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__
instance Lift (Exp o) where
lift' :: Nat -> Nat -> Exp o -> Exp o
lift' Nat
n Nat
j = \case
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
args -> case Elr o
elr of
Var Nat
v | Nat
v forall a. Ord a => a -> a -> Bool
>= Nat
j -> forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok (forall o. Nat -> Elr o
Var (Nat
v forall a. Num a => a -> a -> a
+ Nat
n)) (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
args)
Elr o
_ -> forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
args)
Lam Hiding
hid Abs (MExp o)
b -> forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j Abs (MExp o)
b)
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it Abs (MExp o)
b -> forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MExp o
it) (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j Abs (MExp o)
b)
e :: Exp o
e@Sort{} -> Exp o
e
e :: Exp o
e@AbsurdLambda{} -> Exp o
e
instance Lift (ArgList o) where
lift' :: Nat -> Nat -> ArgList o -> ArgList o
lift' Nat
n Nat
j ArgList o
args = case ArgList o
args of
ArgList o
ALNil -> forall o. ArgList o
ALNil
ALCons Hiding
hid MExp o
a MArgList o
as -> forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MExp o
a) (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
as)
ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar MArgList o
as -> forall o. MArgList o -> ArgList o
ALConPar (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
as)
removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])
removevar :: forall o.
CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
removevar CSCtx o
ctx MExp o
tt [CSPat o]
pats [] = (CSCtx o
ctx, MExp o
tt, [CSPat o]
pats)
removevar CSCtx o
ctx MExp o
tt [CSPat o]
pats ((Nat
v, MExp o
e) : [(Nat, MExp o)]
unif) =
let
e2 :: MExp o
e2 = forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
v Nat
0 forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
e
thesub :: MExp o -> MExp o
thesub = forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
v Nat
0 MExp o
e2
ctx1 :: CSCtx o
ctx1 = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
take Nat
v CSCtx o
ctx) forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
drop (Nat
v forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx)
tt' :: MExp o
tt' = MExp o -> MExp o
thesub MExp o
tt
pats' :: [CSPat o]
pats' = forall a b. (a -> b) -> [a] -> [b]
map (forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
v Nat
0 (forall o. MExp o -> CSPatI o
CSPatExp MExp o
e2) MExp o
e2) [CSPat o]
pats
unif' :: [(Nat, MExp o)]
unif' = forall a b. (a -> b) -> [a] -> [b]
map (\(Nat
uv, MExp o
ue) -> (if Nat
uv forall a. Ord a => a -> a -> Bool
> Nat
v then Nat
uv forall a. Num a => a -> a -> a
- Nat
1 else Nat
uv, MExp o -> MExp o
thesub MExp o
ue)) [(Nat, MExp o)]
unif
in
forall o.
CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
removevar CSCtx o
ctx1 MExp o
tt' [CSPat o]
pats' [(Nat, MExp o)]
unif'
findperm :: [MExp o] -> Maybe [Nat]
findperm :: forall o. [MExp o] -> Maybe [Nat]
findperm [MExp o]
ts =
let
frees :: [[Nat]]
frees = forall a b. (a -> b) -> [a] -> [b]
map forall t. FreeVars t => t -> [Nat]
freevars [MExp o]
ts
m :: IntMap Nat
m = forall a. [(Nat, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> (Nat
i, forall (t :: * -> *) a. Foldable t => t a -> Nat
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Nat
i) [[Nat]]
frees)))
[Nat
0..forall (t :: * -> *) a. Foldable t => t a -> Nat
length [MExp o]
ts forall a. Num a => a -> a -> a
- Nat
1]
r :: IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r IntMap Nat
_ [Nat]
perm Nat
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Nat]
perm
r IntMap Nat
m [Nat]
perm Nat
n =
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
0 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> (b, a)
swap (forall a. IntMap a -> [(Nat, a)]
IntMap.toList IntMap Nat
m)) of
Maybe Nat
Nothing -> forall a. Maybe a
Nothing
Just Nat
i -> IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> Nat -> IntMap a -> IntMap a
IntMap.adjust (forall a. Num a => a -> a -> a
subtract Nat
1))
(forall a. Nat -> a -> IntMap a -> IntMap a
IntMap.insert Nat
i (-Nat
1) IntMap Nat
m)
([[Nat]]
frees forall a. [a] -> Nat -> a
!! Nat
i))
(Nat
i forall a. a -> [a] -> [a]
: [Nat]
perm) (Nat
n forall a. Num a => a -> a -> a
- Nat
1)
in IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r IntMap Nat
m [] (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [MExp o]
ts)
freevars :: FreeVars t => t -> [Nat]
freevars :: forall t. FreeVars t => t -> [Nat]
freevars = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FreeVars t => t -> Set Nat
freeVars
applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] ->
(CSCtx o, MExp o, [CSPat o])
applyperm :: forall o.
[Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
applyperm [Nat]
perm CSCtx o
ctx MExp o
tt [CSPat o]
pats =
let ctx1 :: CSCtx o
ctx1 = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm) MExp o
t)) CSCtx o
ctx
ctx2 :: CSCtx o
ctx2 = forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> CSCtx o
ctx1 forall a. [a] -> Nat -> a
!! Nat
i) [Nat]
perm
ctx3 :: CSCtx o
ctx3 = forall o. CSCtx o -> CSCtx o
seqctx CSCtx o
ctx2
tt' :: MExp o
tt' = forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm) MExp o
tt
pats' :: [CSPat o]
pats' = forall a b. (a -> b) -> [a] -> [b]
map (forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm)) [CSPat o]
pats
in (CSCtx o
ctx3, MExp o
tt', [CSPat o]
pats')
ren :: [Nat] -> Nat -> Int
ren :: [Nat] -> Nat -> Nat
ren [Nat]
n Nat
i = let Just Nat
j = forall a. Eq a => a -> [a] -> Maybe Nat
elemIndex Nat
i [Nat]
n in Nat
j
instance Renaming t => Renaming (HI t) where
renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t
renameOffset Nat
j Nat -> Nat
ren (HI Hiding
hid t
t) = forall a. Hiding -> a -> HI a
HI Hiding
hid forall a b. (a -> b) -> a -> b
$ forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren t
t
instance Renaming (CSPatI o) where
renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o
renameOffset Nat
j Nat -> Nat
ren = \case
CSPatConApp ConstRef o
c [CSPat o]
pats -> forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef o
c forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren) [CSPat o]
pats
CSPatVar Nat
i -> forall o. Nat -> CSPatI o
CSPatVar forall a b. (a -> b) -> a -> b
$ Nat
j forall a. Num a => a -> a -> a
+ Nat -> Nat
ren Nat
i
CSPatExp MExp o
e -> forall o. MExp o -> CSPatI o
CSPatExp forall a b. (a -> b) -> a -> b
$ forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren MExp o
e
e :: CSPatI o
e@CSPatI o
CSOmittedArg -> CSPatI o
e
CSPatI o
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
seqctx :: CSCtx o -> CSCtx o
seqctx :: forall o. CSCtx o -> CSCtx o
seqctx = forall {b} {a}. Lift b => Nat -> [HI (a, b)] -> [HI (a, b)]
r (-Nat
1)
where
r :: Nat -> [HI (a, b)] -> [HI (a, b)]
r Nat
_ [] = []
r Nat
n (HI Hiding
hid (a
id, b
t) : [HI (a, b)]
ctx) = forall a. Hiding -> a -> HI a
HI Hiding
hid (a
id, forall t. Lift t => Nat -> t -> t
lift Nat
n b
t) forall a. a -> [a] -> [a]
: Nat -> [HI (a, b)] -> [HI (a, b)]
r (Nat
n forall a. Num a => a -> a -> a
- Nat
1) [HI (a, b)]
ctx
depthofvar :: Nat -> [CSPat o] -> Nat
depthofvar :: forall o. Nat -> [CSPat o] -> Nat
depthofvar Nat
v [CSPat o]
pats =
let [Nat
depth] = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Nat -> CSPatI o -> [Nat]
f Nat
0) (forall a. [HI a] -> [a]
drophid [CSPat o]
pats)
f :: Nat -> CSPatI o -> [Nat]
f Nat
d (CSPatConApp ConstRef o
_ [CSPat o]
pats) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Nat -> CSPatI o -> [Nat]
f (Nat
d forall a. Num a => a -> a -> a
+ Nat
1)) (forall a. [HI a] -> [a]
drophid [CSPat o]
pats)
f Nat
d (CSPatVar Nat
v') = [Nat
d | Nat
v forall a. Eq a => a -> a -> Bool
== Nat
v']
f Nat
_ CSPatI o
_ = []
in Nat
depth
class LocalTerminationEnv a where
sizeAndBoundVars :: a -> (Sum Nat, [Nat])
instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where
sizeAndBoundVars :: HI a -> (Sum Nat, [Nat])
sizeAndBoundVars (HI Hiding
_ a
p) = forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars a
p
instance LocalTerminationEnv (CSPatI o) where
sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat])
sizeAndBoundVars = \case
CSPatConApp ConstRef o
_ [CSPat o]
ps -> (Sum Nat
1, []) forall a. Semigroup a => a -> a -> a
<> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars [CSPat o]
ps
CSPatVar Nat
n -> (Sum Nat
0, [Nat
n])
CSPatExp MExp o
e -> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars MExp o
e
CSPatI o
_ -> (Sum Nat
0, [])
instance LocalTerminationEnv a => LocalTerminationEnv [a] where
sizeAndBoundVars :: [a] -> (Sum Nat, [Nat])
sizeAndBoundVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars
instance LocalTerminationEnv (MExp o) where
sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])
sizeAndBoundVars Meta{} = (Sum Nat
0, [])
sizeAndBoundVars (NotM Exp o
e) = case Exp o
e of
App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) MArgList o
_ -> (Sum Nat
0, [Nat
v])
App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
_) MArgList o
args -> (Sum Nat
1, []) forall a. Semigroup a => a -> a -> a
<> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars MArgList o
args
Exp o
_ -> (Sum Nat
0, [])
instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where
sizeAndBoundVars :: (a, b) -> (Sum Nat, [Nat])
sizeAndBoundVars (a
a, b
b) = forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars a
a forall a. Semigroup a => a -> a -> a
<> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars b
b
instance LocalTerminationEnv (MArgList o) where
sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])
sizeAndBoundVars MArgList o
as = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MArgList o
as of
ArgList o
ALNil -> (Sum Nat
0, [])
ALCons Hiding
_ MExp o
a MArgList o
as -> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars (MExp o
a, MArgList o
as)
ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar MArgList o
as -> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars MArgList o
as
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv :: forall o. [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv [CSPat o]
pats = ([Nat]
is, forall a. Sum a -> a
getSum Sum Nat
s, [Nat]
vs) where
([Nat]
is , Sum Nat
s , [Nat]
vs) = forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g Nat
0 [CSPat o]
pats
g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g :: forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g Nat
_ [] = ([], Sum Nat
0, [])
g Nat
i (hp :: CSPat o
hp@(HI Hiding
_ CSPatI o
p) : [CSPat o]
ps) = case CSPatI o
p of
CSPatConApp{} -> let (Sum Nat
size, [Nat]
vars) = forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars CSPat o
hp
in ([Nat
i], Sum Nat
size, [Nat]
vars) forall a. Semigroup a => a -> a -> a
<> forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) [CSPat o]
ps
CSPatI o
_ -> forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) [CSPat o]
ps
localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond :: forall o.
([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond ([Nat]
is, Nat
size, [Nat]
vars) ConstRef o
reccallc MExp o
b =
MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
b
where
ok :: MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
e = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MExp o
e forall a b. (a -> b) -> a -> b
$ \Exp o
e -> case Exp o
e of
App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr MArgList o
args -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
(MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
args)
(case Elr o
elr of
Const ConstRef o
c | ConstRef o
c forall a. Eq a => a -> a -> Bool
== ConstRef o
reccallc -> if Nat
size forall a. Eq a => a -> a -> Bool
== Nat
0 then forall blk. Prop blk -> MetaEnv (PB blk)
mpret (forall blk. String -> Prop blk
Error String
"localTerminationSidecond: no size to decrement") else Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall Nat
0 Nat
size [Nat]
vars MArgList o
args
Elr o
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
)
Lam Hiding
_ (Abs MId
_ MExp o
e) -> MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
e
Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ MExp o
ot) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
(MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
it)
(MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
ot)
Sort{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
AbsurdLambda{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
oks :: MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
ArgList o
ALNil -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
ALCons Hiding
_ MExp o
a MArgList o
as -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
(MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
a)
(MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as)
ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ MArgList o
as -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
eas) (MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as)
ALConPar MArgList o
as -> MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as
okcall :: Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall Nat
i Nat
size [Nat]
vars MArgList o
as = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
ArgList o
ALNil -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
ALCons Hiding
_ MExp o
a MArgList o
as | Nat
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Nat]
is ->
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioNo forall a. Maybe a
Nothing (forall {t} {o}.
(Eq t, Num t) =>
t
-> [Nat]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
he Nat
size [Nat]
vars MExp o
a) forall a b. (a -> b) -> a -> b
$ \Maybe (Nat, [Nat])
x -> case Maybe (Nat, [Nat])
x of
Maybe (Nat, [Nat])
Nothing -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error String
"localTerminationSidecond: reccall not ok"
Just (Nat
size', [Nat]
vars') -> Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) Nat
size' [Nat]
vars' MArgList o
as
ALCons Hiding
_ MExp o
a MArgList o
as -> Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) Nat
size [Nat]
vars MArgList o
as
ALProj{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
ALConPar MArgList o
as -> forall a. HasCallStack => a
__IMPOSSIBLE__
he :: t
-> [Nat]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
he t
size [Nat]
vars MM (Exp o) (RefInfo o)
e = forall a blk b.
Refinable a blk =>
MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmcase MM (Exp o) (RefInfo o)
e forall a b. (a -> b) -> a -> b
$ \Exp o
e -> case Exp o
e of
App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) MArgList o
_ ->
case forall {t}. Eq t => t -> [t] -> Maybe [t]
remove Nat
v [Nat]
vars of
Maybe [Nat]
Nothing -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
Just [Nat]
vars' -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (t
size, [Nat]
vars')
App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) MArgList o
args -> do
ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
Constructor{} ->
if t
size forall a. Eq a => a -> a -> Bool
== t
1 then
forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
else
t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes (t
size forall a. Num a => a -> a -> a
- t
1) [Nat]
vars MArgList o
args
DeclCont o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
Exp o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
hes :: t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes t
size [Nat]
vars MArgList o
as = forall a blk b.
Refinable a blk =>
MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmcase MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
ArgList o
ALNil -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (t
size, [Nat]
vars)
ALCons Hiding
_ MM (Exp o) (RefInfo o)
a MArgList o
as ->
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (t
-> [Nat]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
he t
size [Nat]
vars MM (Exp o) (RefInfo o)
a) forall a b. (a -> b) -> a -> b
$ \Maybe (t, [Nat])
x -> case Maybe (t, [Nat])
x of
Maybe (t, [Nat])
Nothing -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
Just (t
size', [Nat]
vars') -> t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes t
size' [Nat]
vars' MArgList o
as
ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar MArgList o
as -> forall a. HasCallStack => a
__IMPOSSIBLE__
remove :: t -> [t] -> Maybe [t]
remove t
_ [] = forall a. Maybe a
Nothing
remove t
x (t
y : [t]
ys) | t
x forall a. Eq a => a -> a -> Bool
== t
y = forall a. a -> Maybe a
Just [t]
ys
remove t
x (t
y : [t]
ys) = case t -> [t] -> Maybe [t]
remove t
x [t]
ys of {Maybe [t]
Nothing -> forall a. Maybe a
Nothing; Just [t]
ys' -> forall a. a -> Maybe a
Just (t
y forall a. a -> [a] -> [a]
: [t]
ys')}
getblks :: MExp o -> IO [Nat]
getblks :: forall o. MExp o -> IO [Nat]
getblks MExp o
tt = do
NotB (HNExp o
hntt, HNNBlks o
blks) <- forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks (forall a o. [CAction o] -> a -> Clos a o
Clos [] MExp o
tt)
case forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f HNNBlks o
blks of
Just Nat
v -> forall (m :: * -> *) a. Monad m => a -> m a
return [Nat
v]
Maybe Nat
Nothing -> case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntt of
HNApp (Const ConstRef o
c) ICArgList o
args -> do
ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
Datatype{} -> forall {o}. [Nat] -> ICArgList o -> IO [Nat]
g [] ICArgList o
args
DeclCont o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
HNExp' o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
where
f :: [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f [WithSeenUIds (HNExp' o) o]
blks = case [WithSeenUIds (HNExp' o) o]
blks of
(WithSeenUIds (HNExp' o) o
b : [WithSeenUIds (HNExp' o) o]
bs) -> case forall a o. WithSeenUIds a o -> a
rawValue (forall a. a -> [a] -> a
last1 WithSeenUIds (HNExp' o) o
b [WithSeenUIds (HNExp' o) o]
bs) of
HNApp (Var Nat
v) ICArgList o
_ -> forall a. a -> Maybe a
Just Nat
v
HNExp' o
_ -> forall a. Maybe a
Nothing
[WithSeenUIds (HNExp' o) o]
_ -> forall a. Maybe a
Nothing
g :: [Nat] -> ICArgList o -> IO [Nat]
g [Nat]
vs ICArgList o
args = do
NotB HNArgList o
hnargs <- forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args
case HNArgList o
hnargs of
HNALCons Hiding
_ ICExp o
a ICArgList o
as -> do
NotB (HNExp o
_, HNNBlks o
blks) <- forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
a
let vs' :: [Nat]
vs' = case forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f HNNBlks o
blks of
Just Nat
v | Nat
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Nat]
vs -> Nat
v forall a. a -> [a] -> [a]
: [Nat]
vs
Maybe Nat
_ -> [Nat]
vs
[Nat] -> ICArgList o -> IO [Nat]
g [Nat]
vs' ICArgList o
as
HNArgList o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [Nat]
vs