module Agda.Auto.CaseSplit where

import Data.IORef
import Data.Tuple (swap)
import Data.List (elemIndex)
-- Import of <> needed for 8.2.2, but redundant in 8.8.3
import Data.Monoid ((<>), Sum(..))
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)
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 :: [HI a] -> [a]
drophid = (HI a -> a) -> [HI a] -> [a]
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) -- always an App
              | 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 IORef Int
ticks Int
nsolwanted [ConstRef o]
chints Maybe (EqReasoningConsts o)
meqr Int
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 -> ([Int], Int, [Int]) -> IO (Maybe (MExp o))
branchsearch Cost
depth CSCtx o
ctx MExp o
tt ([Int], Int, [Int])
termcheckenv = do

      IORef Int
nsol <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
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
                        Maybe (EqReasoningConsts o)
Nothing  -> MetaEnv (PB (RefInfo o)) -> MetaEnv (PB (RefInfo o))
forall a. a -> a
id
                        Just 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
+ Cost
1)
      IORef (Maybe (MExp o)) -> IO (Maybe (MExp o))
forall a. IORef a -> IO a
readIORef IORef (Maybe (MExp o))
sol
     ctx' :: CSCtx o
ctx' = Int -> CSCtx o -> CSCtx o
forall b a. Lift b => Int -> [HI (a, b)] -> [HI (a, b)]
ff Int
1 CSCtx o
ctx
     ff :: Int -> [HI (a, b)] -> [HI (a, b)]
ff Int
_ [] = []
     ff Int
n (HI Hiding
hid (a
id, b
t) : [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
+ Int
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' 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 = do
  ConstDef o
recdefd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
recdef
  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
 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 Cost
depth Int
_ CSCtx o
_ MExp o
_ [CSPat o]
_ | Cost
depth Cost -> Cost -> Bool
forall a. Ord a => a -> a -> Bool
< Cost
0 = [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  rc Cost
depth Int
nscrutavoid CSCtx o
ctx MExp o
tt [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 [Int]
mblkvar = do
    [Sol o]
sols1 <- IO [Sol o]
dobody
    case [Sol o]
sols1 of
     (Sol o
_:[Sol o]
_) -> [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 (Int
v:[Int]
vs) = do
           [Sol o]
sols2 <- [Int] -> Int -> IO [Sol o]
splitvar [Int]
mblkvar Int
v
           case [Sol o]
sols2 of
            (Sol o
_:[Sol o]
_) -> [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 <- [Int
0..Int
nv]] -- [0..length ctx - 1 - nscrutavoid]
    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
- Int
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 [Int]
perm -> do
      let (CSCtx o
ctx', MExp o
tt', [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 MExp o
trm -> [[(CSCtx o
ctx', [CSPat o]
pats', MExp o -> Maybe (MExp o)
forall a. a -> Maybe a
Just MExp o
trm)]]
       Maybe (MExp o)
Nothing -> []
     Maybe [Int]
Nothing -> IO [Sol o]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- no permutation found
   splitvar :: [Nat] -> Nat -> IO [Sol o]
   splitvar :: [Int] -> Int -> IO [Sol o]
splitvar [Int]
mblkvar 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 Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) MArgList o
_ -> 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 [ConstRef o]
cons [ConstRef o]
_ -> 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 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 [Int]
perm ->
             let HI Hiding
scrhid(MId
_, 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
+ Int
1) CSCtx o
ctx
                 (CSCtx o
ctx', MExp o
_, [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 ({-map (replacep scrut 1 CSAbsurd __IMPOSSIBLE__) -}[CSPat o]
pats)
             in [(CSCtx o
ctx', [CSPat o]
pats', Maybe (MExp o)
forall a. Maybe a
Nothing)]
            Maybe [Int]
Nothing -> Sol o
forall a. HasCallStack => a
__IMPOSSIBLE__ -- no permutation found
          Sol o
_ -> 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 (ConstRef o
con : [ConstRef o]
cons) = do
          ConstDef o
cond <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
con
          let ff :: MExp o -> ([((Hiding, Int), MId, MExp o)], MExp o)
ff MExp o
t = case Empty -> MExp o -> Exp o
forall a b. Empty -> MM a b -> a
rm Empty
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, Int), MId, MExp o)]
xs, MExp o
inft) = MExp o -> ([((Hiding, Int), MId, MExp o)], MExp o)
ff MExp o
ot
                         in (((Hiding
h, Int
scrut Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [((Hiding, Int), MId, MExp o)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Hiding, Int), MId, MExp o)]
xs), MId
id, Int -> MExp o -> MExp o
forall t. Lift t => Int -> t -> t
lift (Int
scrut Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [((Hiding, Int), MId, MExp o)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Hiding, Int), MId, MExp o)]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) MExp o
it) ((Hiding, Int), MId, MExp o)
-> [((Hiding, Int), MId, MExp o)] -> [((Hiding, Int), MId, MExp o)]
forall a. a -> [a] -> [a]
: [((Hiding, Int), MId, MExp o)]
xs, MExp o
inft)
                        Exp o
_ -> ([], Int -> MExp o -> MExp o
forall t. Lift t => Int -> t -> t
lift Int
scrut MExp o
t)
              ([((Hiding, Int), MId, MExp o)]
newvars, MExp o
inftype) = MExp o -> ([((Hiding, Int), MId, MExp o)], MExp o)
ff (ConstDef o -> MExp o
forall o. ConstDef o -> MExp o
cdtype ConstDef o
cond)
              constrapp :: MExp o
constrapp = 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) (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 (\MArgList o
xs ((Hiding
h, Int
v), MId
_, MExp o
_) -> 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 (\((Hiding
hid, Int
v), MId
_, MExp o
_) -> 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 (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Int -> Int -> MExp (ReplaceWith t u) -> 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
MExp (ReplaceWith (MExp o) (MExp o))
constrapp
              Id 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 Hiding
hid (MId
id, 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 c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\((Hiding
hid, Int
_), MId
id, MExp o
t) 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 {MId
NoId -> String
newvarprefix{- ++ show i-}; Id String
id -> String
id}), MExp o
t)
                      ) [((Hiding, Int), MId, MExp o)]
newvars [Integer
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 Hiding
hid (MId
id, 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
+ Int
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
constrapp) [CSPat o]
pats
              scruttype' :: MExp o
scruttype' = MExp o -> MExp o
thesub MExp o
scruttype  -- scruttype shouldn't really refer to scrutvar so lift is enough, but what if circular ref has been created and this is not detected until case split is done
          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
           Maybe [(Int, MExp o)]
Nothing -> do
            Bool
res <- Int -> Int -> MExp o -> MExp o -> IO Bool
forall t. Unify 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 -- branch absurd
              [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
             else -- branch dont know
              [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           Just [(Int, MExp o)]
unif ->
            do
             let (CSCtx o
ctx2, MExp o
tt2, [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 = if elem scrut mblkvar then costCaseSplit - (costCaseSplit - costCaseSplitFollow) `div` (length mblkvar) else costCaseSplit
                 cost :: Cost
cost
                   | [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
mblkvar Bool -> Bool -> Bool
&& 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
                                                                = 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)
                   | [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
mblkvar                               = Cost
costCaseSplitVeryHigh
                   | Int
scrut Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
mblkvar                       = Cost
costCaseSplitLow
                   | 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 = Cost
costCaseSplitHigh
                   | Bool
otherwise                                  = Cost
costCaseSplitVeryHigh

                 nothid :: Bool
nothid = let HI Hiding
hid (MId, MExp o)
_ = 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
- Int
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 []
              [Sol o]
_ -> 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]) -> [Sol o] -> [Sol o]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Sol o
sol -> (Sol o -> Sol o) -> [Sol o] -> [Sol o]
forall a b. (a -> b) -> [a] -> [b]
map (\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
       DeclCont o
_ -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"
     Exp o
_ -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"

infertypevar :: CSCtx o -> Nat -> MExp o
infertypevar :: CSCtx o -> Int -> MExp o
infertypevar CSCtx o
ctx 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 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 :: Int -> Int -> MExp (ReplaceWith t u) -> t -> u
replace Int
sv Int
nnew MExp (ReplaceWith t u)
e t
t = Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
0 MExp (ReplaceWith t u)
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 t u => Replace (Abs t) (Abs u) where
  type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u
  replace' :: Int
-> MExp (ReplaceWith (Abs t) (Abs u))
-> Abs t
-> Reader (Int, Int) (Abs u)
replace' Int
n MExp (ReplaceWith (Abs t) (Abs u))
re (Abs MId
mid 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 (ReplaceWith t u) -> t -> ReaderT (Int, Int) Identity u
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) MExp (ReplaceWith t u)
MExp (ReplaceWith (Abs t) (Abs u))
re t
b

instance Replace (Exp o) (MExp o) where
  type ReplaceWith (Exp o) (MExp o) = o
  replace' :: Int
-> MExp (ReplaceWith (Exp o) (MExp o))
-> Exp o
-> Reader (Int, Int) (MExp o)
replace' Int
n MExp (ReplaceWith (Exp o) (MExp o))
re = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
ok elr :: Elr o
elr@(Var Int
v) 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 (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> ReaderT (Int, Int) Identity (ArgList o)
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MArgList o) (ArgList o))
MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
      (Int
sv, 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
MExp (ReplaceWith (Exp o) (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
- Int
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 Maybe (UId o)
uid OKHandle (RefInfo o)
ok elr :: Elr o
elr@Const{} 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 (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> ReaderT (Int, Int) Identity (ArgList o)
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MArgList o) (ArgList o))
MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
    Lam Hiding
hid 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 (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
-> Abs (MExp o)
-> ReaderT (Int, Int) Identity (Abs (MExp o))
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) MExp (ReplaceWith (Exp o) (MExp o))
MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
re Abs (MExp o)
b
    Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it 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 (ReplaceWith (MExp o) (MExp o))
-> MExp o
-> Reader (Int, Int) (MExp o)
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MExp o) (MExp o))
MExp (ReplaceWith (Exp o) (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 (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
-> Abs (MExp o)
-> ReaderT (Int, Int) Identity (Abs (MExp o))
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (Exp o) (MExp o))
MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
re Abs (MExp o)
b
    e :: Exp o
e@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
    e :: 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 t u => Replace (MM t (RefInfo o)) u where
  type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u
  replace' :: Int
-> MExp (ReplaceWith (MM t (RefInfo o)) u)
-> MM t (RefInfo o)
-> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MM t (RefInfo o)) u)
re = Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith t u)
MExp (ReplaceWith (MM t (RefInfo o)) u)
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 (ArgList o) (ArgList o) where
  type ReplaceWith (ArgList o) (ArgList o) = o
  replace' :: Int
-> MExp (ReplaceWith (ArgList o) (ArgList o))
-> ArgList o
-> Reader (Int, Int) (ArgList o)
replace' Int
n MExp (ReplaceWith (ArgList o) (ArgList o))
re ArgList o
args = case ArgList o
args of
    ArgList o
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 Hiding
hid MExp o
a 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 (ReplaceWith (MExp o) (MExp o))
-> MExp o
-> ReaderT (Int, Int) Identity (MExp o)
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MExp o) (MExp o))
MExp (ReplaceWith (ArgList o) (ArgList 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 (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> Reader (Int, Int) (ArgList o)
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MArgList o) (ArgList o))
MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as)
    ALProj{}        -> Reader (Int, Int) (ArgList o)
forall a. HasCallStack => a
__IMPOSSIBLE__
    ALConPar 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 (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> Reader (Int, Int) (ArgList o)
forall t u.
Replace t u =>
Int -> MExp (ReplaceWith t u) -> t -> Reader (Int, Int) u
replace' Int
n MExp (ReplaceWith (MArgList o) (ArgList o))
MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as


betareduce :: MExp o -> MArgList o -> MExp o
betareduce :: MExp o -> MArgList o -> MExp o
betareduce MExp o
e 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
 ArgList o
ALNil -> MExp o
e
 ALCons Hiding
_ MExp o
a 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 Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr 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 Hiding
_ (Abs MId
_ MExp o
b) -> MExp o -> MArgList o -> MExp o
forall o. MExp o -> MArgList o -> MExp o
betareduce (Int
-> Int -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Int -> Int -> MExp (ReplaceWith t u) -> t -> u
replace Int
0 Int
0 MExp o
MExp (ReplaceWith (MExp o) (MExp o))
a MExp o
b) MArgList o
rargs
  Exp o
_ -> MExp o
forall a. HasCallStack => a
__IMPOSSIBLE__ -- not type correct if this happens
 ALProj{} -> MExp o
forall a. HasCallStack => a
__IMPOSSIBLE__
 ALConPar 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 MArgList o
xs 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
  ArgList o
ALNil -> MArgList o
ys

  ALCons Hiding
hid MExp o
x 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 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 Int
sv Int
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)) = 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 Hiding
hid (CSPatVar Int
v)) | Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sv   = Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid CSPatI o
rp
                          | Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
sv    = 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
- Int
1))
                          | Bool
otherwise = 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 Hiding
hid (CSPatExp 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 (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Int -> Int -> MExp (ReplaceWith t u) -> t -> u
replace Int
sv Int
nnew MExp o
MExp (ReplaceWith (MExp o) (MExp o))
re MExp o
e)

  r p :: CSPat o
p@(HI Hiding
_ CSPatI o
CSOmittedArg) = CSPat o
p

  r CSPat o
_ = CSPat o
forall a. HasCallStack => a
__IMPOSSIBLE__ -- other constructors dont appear in indata Pats



-- Unification takes two values of the same type and generates a list
-- of assignments making the two terms equal.

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 :: t -> t -> Maybe (Assignments (UnifiesTo t))
unify t
t t
u = t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' t
t t
u StateT (Assignments (UnifiesTo t)) Maybe ()
-> Assignments (UnifiesTo t) -> Maybe (Assignments (UnifiesTo t))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
`execStateT` []

notequal :: Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal :: Int -> Int -> t -> t -> IO Bool
notequal Int
fstnew Int
nbnew t
t1 t
t2 = t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' t
t1 t
t2 ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
-> (Int, Int) -> StateT (Assignments (UnifiesTo t)) IO Bool
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (Int
fstnew, Int
nbnew)
                                              StateT (Assignments (UnifiesTo t)) IO Bool
-> Assignments (UnifiesTo t) -> IO Bool
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' = t -> t -> StateT [(Int, Exp o)] Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' (t -> t -> StateT [(Int, Exp o)] Maybe ())
-> (MM t (RefInfo o) -> t)
-> MM t (RefInfo o)
-> MM t (RefInfo o)
-> StateT [(Int, Exp 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 (UnifiesTo (MM t (RefInfo o)))) IO)
     Bool
notequal' = t -> t -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' (t -> t -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool)
-> (MM t (RefInfo o) -> t)
-> MM t (RefInfo o)
-> MM t (RefInfo o)
-> ReaderT (Int, Int) (StateT [(Int, Exp 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 Int
v 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
    Maybe (Exp o)
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 Exp o
e' -> Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()
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) = t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' t
b1 t
b2

  notequal' :: Abs t
-> Abs t
-> ReaderT
     (Int, Int) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool
notequal' (Abs MId
_ t
b1) (Abs MId
_ t
b2) = t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (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 Elr o -> Elr o -> Bool
forall a. Eq a => a -> a -> Bool
== Elr o
elr2 -> MArgList o
-> MArgList o
-> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
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 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> Abs (MExp o)
-> Abs (MExp o)
-> StateT (Assignments (UnifiesTo (Abs (MExp o)))) Maybe ()
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 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> MExp o
-> MExp o -> StateT (Assignments (UnifiesTo (MExp o))) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MExp o
a1 MExp o
a2
                                                           StateT [(Int, Exp o)] Maybe ()
-> StateT [(Int, Exp o)] Maybe () -> StateT [(Int, Exp o)] Maybe ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Abs (MExp o)
-> Abs (MExp o)
-> StateT (Assignments (UnifiesTo (Abs (MExp o)))) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
   (Sort Sort
_, Sort Sort
_) -> () -> StateT [(Int, Exp o)] Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- a bit sloppy
   (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v) (NotM ArgList o
ALNil), Exp o
_)
     | 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 [(Int, Exp o)] Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift Maybe ()
forall a. Maybe a
Nothing -- Occurs check
   (Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v) (NotM ArgList o
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 [(Int, Exp o)] Maybe ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift Maybe ()
forall a. Maybe a
Nothing -- Occurs check
   (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v) (NotM ArgList o
ALNil), Exp o
_) -> Int -> Exp o -> StateT [(Int, Exp o)] Maybe ()
forall o. Int -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Int
v Exp o
e2
   (Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v) (NotM ArgList o
ALNil)) -> Int -> Exp o -> StateT [(Int, Exp o)] Maybe ()
forall o. Int -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Int
v Exp o
e1
   (Exp o, Exp o)
_ -> Maybe () -> StateT [(Int, Exp 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 (UnifiesTo (Exp o))) IO) Bool
notequal' Exp o
e1 Exp o
e2 = do
    (Int
fstnew, Int
nbnew) <- ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) (Int, Int)
forall r (m :: * -> *). MonadReader r m => m r
ask
    [(Int, Exp o)]
unifier         <- ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) [(Int, Exp o)]
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 Elr o -> Elr o -> Bool
forall a. Eq a => a -> a -> Bool
== Elr o
elr2 -> MArgList o
-> MArgList o
-> ReaderT
     (Int, Int) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
      (Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v2) (NotM ArgList o
ALNil)) -- why is this not symmetric?!
        | 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 -> [(Int, Exp o)] -> Maybe (Exp o)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
v2 [(Int, Exp o)]
unifier of
          Maybe (Exp o)
Nothing  -> ([(Int, Exp o)] -> [(Int, Exp o)])
-> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Int
v2, Exp o
e1)(Int, Exp o) -> [(Int, Exp o)] -> [(Int, Exp o)]
forall a. a -> [a] -> [a]
:) ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) ()
-> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
-> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Just Exp o
e2' -> Exp o
-> Exp o
-> ReaderT
     (Int, Int) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' Exp o
e1 Exp o
e2'
{-
  GA: Skipped these: Not sure why we'd claim they're impossible
      (_, App _ _ (Var v2) (NotM ALProj{})) -> __IMPOSSIBLE__
      (_, App _ _ (Var v2) (NotM ALConPar{})) -> __IMPOSSIBLE__
-}
      (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 <- IO (ConstDef o)
-> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) (ConstDef o)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef o)
 -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) (ConstDef o))
-> IO (ConstDef o)
-> ReaderT (Int, Int) (StateT [(Int, Exp 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 [(Int, Exp o)] IO) (ConstDef o)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef o)
 -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) (ConstDef o))
-> IO (ConstDef o)
-> ReaderT (Int, Int) (StateT [(Int, Exp 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 (UnifiesTo (MArgList o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
                                            else Bool -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          (DeclCont o, DeclCont o)
_ -> Bool -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
{- GA: Why don't we have a case for distinct heads after all these
       unification cases for vars with no spines & metas that can
       be looked up?
      (App _ _ elr1 _, App _ _ elr2 _) | elr1 <> elr2 -> return True
-}
      (Exp o, Exp o)
_ -> Bool -> ReaderT (Int, Int) (StateT [(Int, Exp o)] IO) Bool
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) -> () -> StateT (Assignments o) Maybe ()
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 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> MExp o
-> MExp o -> StateT (Assignments (UnifiesTo (MExp o))) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) 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 (UnifiesTo (MArgList o))) Maybe ()
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) -> MArgList o
-> MArgList o
-> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
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) -> MArgList o
-> MArgList o
-> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
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)   -> MArgList o
-> MArgList o
-> StateT (Assignments (UnifiesTo (MArgList o))) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
   (ArgList o, ArgList o)
_ -> 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 (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) -> MExp o
-> MExp o
-> ReaderT
     (Int, Int) (StateT (Assignments (UnifiesTo (MExp o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) 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 (UnifiesTo (MArgList o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es MArgList o
fs
    (ALConPar MArgList o
es1, ALConPar MArgList o
es2)   -> MArgList o
-> MArgList o
-> ReaderT
     (Int, Int) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Int, Int) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
    (ArgList o, ArgList o)
_                              -> Bool -> ReaderT (Int, Int) (StateT (Assignments o) IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- This definition is only here to respect the previous interface.
unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
unifyexp :: MExp o -> MExp o -> Maybe [(Int, MExp o)]
unifyexp MExp o
e1 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 (Assignments (UnifiesTo (MExp o)))
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 :: Int -> t -> t
lift Int
0 = t -> t
forall a. a -> a
id
lift Int
n = Int -> Int -> t -> t
forall t. Lift t => Int -> Int -> t -> t
lift' Int
n Int
0

instance Lift t => Lift (Abs t) where
  lift' :: Int -> Int -> Abs t -> Abs t
lift' Int
n Int
j (Abs MId
mid 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
+ Int
1) t
b)

instance Lift t => Lift (MM t r) where
  lift' :: Int -> Int -> MM t r -> MM t r
lift' Int
n 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' Int
n Int
j = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
args -> case Elr o
elr of
      Var 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)
      Elr o
_ -> 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 Hiding
hid 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 Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it 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)
    e :: Exp o
e@Sort{} -> Exp o
e
    e :: Exp o
e@AbsurdLambda{} -> Exp o
e

instance Lift (ArgList o) where
  lift' :: Int -> Int -> ArgList o -> ArgList o
lift' Int
n Int
j ArgList o
args = case ArgList o
args of
    ArgList o
ALNil           -> ArgList o
forall o. ArgList o
ALNil
    ALCons Hiding
hid MExp o
a 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 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 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 ((Int
v, MExp o
e) : [(Int, MExp o)]
unif) =
 let
  e2 :: MExp o
e2 = Int
-> Int -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Int -> Int -> MExp (ReplaceWith t u) -> t -> u
replace Int
v Int
0 MExp (ReplaceWith (MExp o) (MExp o))
forall a. HasCallStack => a
__IMPOSSIBLE__ {- occurs check failed -} MExp o
e
  thesub :: MExp o -> MExp o
thesub = Int
-> Int -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Int -> Int -> MExp (ReplaceWith t u) -> t -> u
replace Int
v Int
0 MExp o
MExp (ReplaceWith (MExp o) (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 Hiding
hid (MId
id, 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 Hiding
hid (MId
id, 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
+ Int
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 Int
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 (\(Int
uv, 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
- Int
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 [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 (\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)))
          [Int
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
- Int
1]
  r :: IntMap Int -> [Int] -> Int -> Maybe [Int]
r IntMap Int
_ [Int]
perm Int
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 IntMap Int
m [Int]
perm Int
n =
   case Int -> [(Int, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
0 (((Int, Int) -> (Int, Int)) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> (Int, Int)
forall a b. (a, b) -> (b, a)
swap (IntMap Int -> [(Int, Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Int
m)) of
    Maybe Int
Nothing -> Maybe [Int]
forall a. Maybe a
Nothing
    Just Int
i -> IntMap Int -> [Int] -> Int -> Maybe [Int]
r ((IntMap Int -> Int -> IntMap Int)
-> IntMap Int -> [Int] -> IntMap Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Int -> IntMap Int -> IntMap Int)
-> IntMap Int -> Int -> IntMap Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Int -> IntMap Int -> IntMap Int)
 -> IntMap Int -> Int -> IntMap Int)
-> (Int -> IntMap Int -> IntMap Int)
-> IntMap Int
-> Int
-> IntMap Int
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Int -> IntMap Int -> IntMap Int
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1))
                       (Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (-Int
1) IntMap Int
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) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
 in IntMap Int -> [Int] -> Int -> 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 [Int]
perm CSCtx o
ctx MExp o
tt [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 Hiding
hid (MId
id, 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 (\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 [Int]
n Int
i = let Just Int
j = Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Int
i [Int]
n in Int
j

instance Renaming t => Renaming (HI t) where
  renameOffset :: Int -> (Int -> Int) -> HI t -> HI t
renameOffset Int
j Int -> Int
ren (HI Hiding
hid 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 Int
j Int -> Int
ren = \case
    CSPatConApp ConstRef o
c [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 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 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
    e :: CSPatI o
e@CSPatI o
CSOmittedArg     -> CSPatI o
e
    CSPatI o
_                  -> 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 (-Int
1)
 where
  r :: Int -> [HI (a, b)] -> [HI (a, b)]
r Int
_ [] = []
  r Int
n (HI Hiding
hid (a
id, b
t) : [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
- Int
1) [HI (a, b)]
ctx
-- --------------------

depthofvar :: Nat -> [CSPat o] -> Nat
depthofvar :: Int -> [CSPat o] -> Int
depthofvar Int
v [CSPat o]
pats =
 let [Int
depth] = (CSPatI o -> [Int]) -> [CSPatI o] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> CSPatI o -> [Int]
f Int
0) ([CSPat o] -> [CSPatI o]
forall a. [HI a] -> [a]
drophid [CSPat o]
pats)
     f :: Int -> CSPatI o -> [Int]
f Int
d (CSPatConApp ConstRef o
_ [CSPat o]
pats) = (CSPatI o -> [Int]) -> [CSPatI o] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> CSPatI o -> [Int]
f (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) ([CSPat o] -> [CSPatI o]
forall a. [HI a] -> [a]
drophid [CSPat o]
pats)
     f Int
d (CSPatVar Int
v') = [Int
d | Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v']
     f Int
_ CSPatI o
_ = []
 in Int
depth

-- --------------------
-- | Speculation: Type class computing the size (?) of a pattern
--   and collecting the vars it introduces
class LocalTerminationEnv a where
  sizeAndBoundVars :: a -> (Sum Nat, [Nat])

instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where
  sizeAndBoundVars :: HI a -> (Sum Int, [Int])
sizeAndBoundVars (HI Hiding
_ 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 = \case
    CSPatConApp ConstRef o
_ [CSPat o]
ps -> (Sum Int
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 Int
n       -> (Sum Int
0, [Int
n])
    CSPatExp MExp o
e       -> MExp o -> (Sum Int, [Int])
forall a. LocalTerminationEnv a => a -> (Sum Int, [Int])
sizeAndBoundVars MExp o
e
    CSPatI o
_                -> (Sum Int
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 e = case rm __IMPOSSIBLE__ e of
-- GA: 2017 06 27: Not actually impossible! (cf. #2620)
  sizeAndBoundVars :: MExp o -> (Sum Int, [Int])
sizeAndBoundVars Meta{} = (Sum Int
0, [])
-- Does this default behaviour even make sense? The catchall in the
-- following match seems to suggest it does
  sizeAndBoundVars (NotM Exp o
e) = case Exp o
e of
    App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v) MArgList o
_      -> (Sum Int
0, [Int
v])
    App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
_) MArgList o
args -> (Sum Int
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
    Exp o
_                      -> (Sum Int
0, [])

instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where
  sizeAndBoundVars :: (a, b) -> (Sum Int, [Int])
sizeAndBoundVars (a
a, 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 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
    ArgList o
ALNil         -> (Sum Int
0, [])
    ALCons Hiding
_ MExp o
a 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 MArgList o
as   -> MArgList o -> (Sum Int, [Int])
forall a. LocalTerminationEnv a => a -> (Sum Int, [Int])
sizeAndBoundVars MArgList o
as


-- | Take a list of patterns and returns (is, size, vars) where (speculation):
---  * the is are the pattern indices the vars are contained in
--   * size is total number of constructors removed (?) to access vars
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv :: [CSPat o] -> ([Int], Int, [Int])
localTerminationEnv [CSPat o]
pats = ([Int]
is, Sum Int -> Int
forall a. Sum a -> a
getSum Sum Int
s, [Int]
vs) where

  ([Int]
is , Sum Int
s , [Int]
vs) = Int -> [CSPat o] -> ([Int], Sum Int, [Int])
forall o. Int -> [CSPat o] -> ([Int], Sum Int, [Int])
g Int
0 [CSPat o]
pats

  g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
  g :: Int -> [CSPat o] -> ([Int], Sum Int, [Int])
g Int
_ [] = ([], Sum Int
0, [])
  g Int
i (hp :: CSPat o
hp@(HI Hiding
_ CSPatI o
p) : [CSPat o]
ps) = case CSPatI o
p of
    CSPatConApp{} -> let (Sum Int
size, [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
+ Int
1) [CSPat o]
ps
    CSPatI o
_ -> 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
+ Int
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 ([Int]
is, Int
size, [Int]
vars) ConstRef o
reccallc MExp o
b =
  MExp o -> EE (MyPB o)
ok MExp o
b
 where
     ok :: MExp o -> EE (MyPB o)
ok 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
$ \Exp o
e -> case Exp o
e of
      App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr 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 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
== Int
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 String
"localTerminationSidecond: no size to decrement") else Int -> Int -> [Int] -> MArgList o -> EE (MyPB o)
okcall Int
0 Int
size [Int]
vars MArgList o
args
          Elr o
_ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
       )
      Lam Hiding
_ (Abs MId
_ MExp o
e) -> MExp o -> EE (MyPB o)
ok MExp o
e
      Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ 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 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
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
ALNil -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
      ALCons Hiding
_ MExp o
a 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 MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ 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 MArgList o
as -> MArgList o -> EE (MyPB o)
oks MArgList o
as

     okcall :: Int -> Int -> [Int] -> MArgList o -> EE (MyPB o)
okcall Int
i Int
size [Int]
vars 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
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
ALNil -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
      ALCons Hiding
_ MExp o
a 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 (Int, [Int])) (RefInfo o))
-> (Maybe (Int, [Int]) -> EE (MyPB o))
-> EE (MyPB 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 (Int
-> [Int] -> MExp o -> MetaEnv (MB (Maybe (Int, [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 Int
size [Int]
vars MExp o
a) ((Maybe (Int, [Int]) -> EE (MyPB o)) -> EE (MyPB o))
-> (Maybe (Int, [Int]) -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \Maybe (Int, [Int])
x -> case Maybe (Int, [Int])
x of
        Maybe (Int, [Int])
Nothing -> 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
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error String
"localTerminationSidecond: reccall not ok"
        Just (Int
size', [Int]
vars') -> Int -> Int -> [Int] -> MArgList o -> EE (MyPB o)
okcall (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size' [Int]
vars' MArgList o
as
      ALCons Hiding
_ MExp o
a MArgList o
as -> Int -> Int -> [Int] -> MArgList o -> EE (MyPB o)
okcall (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size [Int]
vars MArgList o
as

      ALProj{} -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK


      ALConPar MArgList o
as -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__

     he :: a
-> [Int]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (a, [Int])) (RefInfo o))
he a
size [Int]
vars 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
$ \Exp o
e -> case Exp o
e of
      App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Int
v) MArgList o
_ ->
       case Int -> [Int] -> Maybe [Int]
forall a. Eq a => a -> [a] -> Maybe [a]
remove Int
v [Int]
vars of
        Maybe [Int]
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 [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 Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) 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
== a
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
- a
1) [Int]
vars MArgList o
args
        DeclCont o
_ -> 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
      Exp o
_ -> 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 a
size [Int]
vars 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
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
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 Hiding
_ MM (Exp o) (RefInfo o)
a 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
$ \Maybe (a, [Int])
x -> case Maybe (a, [Int])
x of
        Maybe (a, [Int])
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 (a
size', [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 MArgList o
as -> MetaEnv (MB (Maybe (a, [Int])) (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__

     remove :: a -> [a] -> Maybe [a]
remove a
_ [] = Maybe [a]
forall a. Maybe a
Nothing
     remove a
x (a
y : [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 a
x (a
y : [a]
ys) = case a -> [a] -> Maybe [a]
remove a
x [a]
ys of {Maybe [a]
Nothing -> Maybe [a]
forall a. Maybe a
Nothing; Just [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 MExp o
tt = do
 NotB (HNExp o
hntt, 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 Int
v -> [Int] -> IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int
v]
  Maybe Int
Nothing -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntt of
   HNApp (Const ConstRef o
c) 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
     DeclCont o
_ -> [Int] -> IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
   HNExp' o
_ -> [Int] -> IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
 where
  f :: [WithSeenUIds (HNExp' o) o] -> Maybe Int
f [WithSeenUIds (HNExp' o) o]
blks = case [WithSeenUIds (HNExp' o) o]
blks of
             (WithSeenUIds (HNExp' o) o
b : [WithSeenUIds (HNExp' o) o]
bs) -> case WithSeenUIds (HNExp' o) o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue (WithSeenUIds (HNExp' o) o
-> [WithSeenUIds (HNExp' o) o] -> WithSeenUIds (HNExp' o) o
forall a. a -> [a] -> a
last1 WithSeenUIds (HNExp' o) o
b [WithSeenUIds (HNExp' o) o]
bs) of
              HNApp (Var Int
v) ICArgList o
_ -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
v
              HNExp' o
_ -> Maybe Int
forall a. Maybe a
Nothing
             [WithSeenUIds (HNExp' o) o]
_ -> Maybe Int
forall a. Maybe a
Nothing
  g :: [Int] -> ICArgList o -> IO [Int]
g [Int]
vs ICArgList o
args = do
   NotB 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 Hiding
_ ICExp o
a ICArgList o
as -> do
     NotB (HNExp o
_, 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 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
                Maybe Int
_ -> [Int]
vs
     [Int] -> ICArgList o -> IO [Int]
g [Int]
vs' ICArgList o
as
    HNArgList o
_ -> [Int] -> IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
vs
-- ---------------------------