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