module Agda.Auto.CaseSplit where

import Control.Monad.State as St hiding (lift)
import Control.Monad.Reader as Rd hiding (lift)
import qualified Control.Monad.State as St
import Control.Monad.IO.Class ( MonadIO(..) )

import Data.Function
import Data.IORef
import Data.Tuple (swap)
import Data.List (elemIndex)
-- Import 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 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
-- ---------------------------