module Agda.Auto.CaseSplit where

import Prelude hiding ((!!))

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 :: forall a. [HI a] -> [a]
drophid = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
_ a
x) -> a
x)

type CSPat o = HI (CSPatI o)
type CSCtx o = [HI (MId, MExp o)]

data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]
              | CSPatProj (ConstRef 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 :: forall o.
IORef Nat
-> Nat
-> [ConstRef o]
-> Maybe (EqReasoningConsts o)
-> Nat
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch IORef Nat
ticks Nat
nsolwanted [ConstRef o]
chints Maybe (EqReasoningConsts o)
meqr Nat
depthinterval Cost
depth ConstRef o
recdef CSCtx o
ctx MExp o
tt [CSPat o]
pats = do
 let branchsearch :: Cost -> CSCtx o -> MExp o ->
                     ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
     branchsearch :: Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Cost
depth CSCtx o
ctx MExp o
tt ([Nat], Nat, [Nat])
termcheckenv = do

      IORef Nat
nsol <- forall a. a -> IO (IORef a)
newIORef Nat
1
      Metavar (Exp o) (RefInfo o)
m <- forall a blk. IO (Metavar a blk)
initMeta
      IORef (Maybe (MExp o))
sol <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
      let trm :: MExp o
trm = forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp o) (RefInfo o)
m
          hsol :: IO ()
hsol = do MExp o
trm' <- forall t. ExpandMetas t => t -> IO t
expandMetas MExp o
trm
                    forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe (MExp o))
sol (forall a. a -> Maybe a
Just MExp o
trm')
          initcon :: MetaEnv (PB (RefInfo o))
initcon = forall blk. Prop blk -> MetaEnv (PB blk)
mpret
                  forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
                    (forall o.
([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond ([Nat], Nat, [Nat])
termcheckenv ConstRef o
recdef MExp o
trm)
                  forall a b. (a -> b) -> a -> b
$ (case Maybe (EqReasoningConsts o)
meqr of
                        Maybe (EqReasoningConsts o)
Nothing  -> forall a. a -> a
id
                        Just EqReasoningConsts o
eqr -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (forall o. EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState EqReasoningConsts o
eqr MExp o
trm)
                     ) forall a b. (a -> b) -> a -> b
$ forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch Bool
False (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall o. MExp o -> CExp o
closify) (forall a. [HI a] -> [a]
drophid CSCtx o
ctx))
                         (forall o. MExp o -> CExp o
closify MExp o
tt) MExp o
trm
      ConstDef o
recdefd <- forall a. IORef a -> IO a
readIORef ConstRef o
recdef
      let env :: RefInfo o
env = RIEnv { rieHints :: [(ConstRef o, HintMode)]
rieHints = (ConstRef o
recdef, HintMode
HMRecCall) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (, HintMode
HMNormal) [ConstRef o]
chints
                      , rieDefFreeVars :: Nat
rieDefFreeVars = forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
recdefd
                      , rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
rieEqReasoningConsts = Maybe (EqReasoningConsts o)
meqr
                      }
      Bool
depreached <- forall blk.
IORef Nat
-> IORef Nat
-> IO ()
-> blk
-> MetaEnv (PB blk)
-> Cost
-> Cost
-> IO Bool
topSearch IORef Nat
ticks IORef Nat
nsol IO ()
hsol RefInfo o
env MetaEnv (PB (RefInfo o))
initcon Cost
depth (Cost
depth forall a. Num a => a -> a -> a
+ Cost
1)
      forall a. IORef a -> IO a
readIORef IORef (Maybe (MExp o))
sol
     ctx' :: CSCtx o
ctx' = forall {b} {a}. Lift b => Nat -> [HI (a, b)] -> [HI (a, b)]
ff Nat
1 CSCtx o
ctx
     ff :: Nat -> [HI (a, b)] -> [HI (a, b)]
ff Nat
_ [] = []
     ff Nat
n (HI Hiding
hid (a
id, b
t) : [HI (a, b)]
ctx) = forall a. Hiding -> a -> HI a
HI Hiding
hid (a
id, forall t. Lift t => Nat -> t -> t
lift Nat
n b
t) forall a. a -> [a] -> [a]
: Nat -> [HI (a, b)] -> [HI (a, b)]
ff (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) [HI (a, b)]
ctx
 forall o.
(Cost
 -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
-> Nat
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch' Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Nat
depthinterval Cost
depth ConstRef o
recdef CSCtx o
ctx' MExp o
tt [CSPat o]
pats

caseSplitSearch' :: forall o .
  (Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) ->
  Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch' :: forall o.
(Cost
 -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o)))
-> Nat
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch' Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Nat
depthinterval Cost
depth ConstRef o
recdef CSCtx o
ctx MExp o
tt [CSPat o]
pats = do
  ConstDef o
recdefd <- forall a. IORef a -> IO a
readIORef ConstRef o
recdef
  Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc Cost
depth (forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
recdefd) CSCtx o
ctx MExp o
tt [CSPat o]
pats
 where
  rc :: Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
  rc :: Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc Cost
depth Nat
_ CSCtx o
_ MExp o
_ [CSPat o]
_ | Cost
depth forall a. Ord a => a -> a -> Bool
< Cost
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
  rc Cost
depth Nat
nscrutavoid CSCtx o
ctx MExp o
tt [CSPat o]
pats = do

    [Nat]
mblkvar <- forall o. MExp o -> IO [Nat]
getblks MExp o
tt
    [Nat] -> IO [Sol o]
fork
     [Nat]
mblkvar
   where
   fork :: [Nat] -> IO [Sol o]
   fork :: [Nat] -> IO [Sol o]
fork [Nat]
mblkvar = do
    [Sol o]
sols1 <- IO [Sol o]
dobody
    case [Sol o]
sols1 of
     (Sol o
_:[Sol o]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return [Sol o]
sols1
     [] -> do
      let r :: [Nat] -> IO [Sol o]
          r :: [Nat] -> IO [Sol o]
r [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
          r (Nat
v:[Nat]
vs) = do
           [Sol o]
sols2 <- [Nat] -> Nat -> IO [Sol o]
splitvar [Nat]
mblkvar Nat
v
           case [Sol o]
sols2 of
            (Sol o
_:[Sol o]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return [Sol o]
sols2
            [] -> [Nat] -> IO [Sol o]
r [Nat]
vs
      [Nat] -> IO [Sol o]
r [Nat
nv forall a. Num a => a -> a -> a
- Nat
x | Nat
x <- [Nat
0..Nat
nv]] -- [0..length ctx - 1 - nscrutavoid]
    where nv :: Nat
nv = forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
1
   dobody :: IO [Sol o]
   dobody :: IO [Sol o]
dobody = do
    case forall o. [MExp o] -> Maybe [Nat]
findperm (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a. [HI a] -> [a]
drophid CSCtx o
ctx)) of
     Just [Nat]
perm -> do
      let (CSCtx o
ctx', MExp o
tt', [CSPat o]
pats') = forall o.
[Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
applyperm [Nat]
perm CSCtx o
ctx MExp o
tt [CSPat o]
pats
      Maybe (MExp o)
res <- Cost
-> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch Cost
depth CSCtx o
ctx' MExp o
tt' (forall o. [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv [CSPat o]
pats')
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Maybe (MExp o)
res of
       Just MExp o
trm -> [[(CSCtx o
ctx', [CSPat o]
pats', forall a. a -> Maybe a
Just MExp o
trm)]]
       Maybe (MExp o)
Nothing -> []
     Maybe [Nat]
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- no permutation found
   splitvar :: [Nat] -> Nat -> IO [Sol o]
   splitvar :: [Nat] -> Nat -> IO [Sol o]
splitvar [Nat]
mblkvar Nat
scrut = do
    let scruttype :: MExp o
scruttype = forall o. CSCtx o -> Nat -> MExp o
infertypevar CSCtx o
ctx Nat
scrut
    case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
scruttype of
     App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) MArgList o
_ -> do
      ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
      case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
       Datatype [ConstRef o]
cons [ConstRef o]
_ -> do
         [Sol o]
sols <- [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Sol o
sol -> case Sol o
sol of
          [] ->
           case forall o. [MExp o] -> Maybe [Nat]
findperm (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a. [HI a] -> [a]
drophid CSCtx o
ctx)) of
            Just [Nat]
perm ->
             let HI Hiding
scrhid(MId
_, MExp o
scrt) = CSCtx o
ctx forall a. HasCallStack => [a] -> Nat -> a
!! Nat
scrut
                 ctx1 :: CSCtx o
ctx1 = forall a. Nat -> [a] -> [a]
take Nat
scrut CSCtx o
ctx forall a. [a] -> [a] -> [a]
++ (forall a. Hiding -> a -> HI a
HI Hiding
scrhid (String -> MId
Id String
abspatvarname, MExp o
scrt)) forall a. a -> [a] -> [a]
: forall a. Nat -> [a] -> [a]
drop (Nat
scrut forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx
                 (CSCtx o
ctx', MExp o
_, [CSPat o]
pats') = forall o.
[Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
applyperm [Nat]
perm CSCtx o
ctx1 MExp o
tt ({-map (replacep scrut 1 CSAbsurd __IMPOSSIBLE__) -}[CSPat o]
pats)
             in [(CSCtx o
ctx', [CSPat o]
pats', forall a. Maybe a
Nothing)]
            Maybe [Nat]
Nothing -> 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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
         dobranches (ConstRef o
con : [ConstRef o]
cons) = do
          ConstDef o
cond <- forall a. IORef a -> IO a
readIORef ConstRef o
con
          let ff :: MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
ff MExp o
t = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
t of
                        Pi Maybe (UId o)
_ Hiding
h Bool
_ MExp o
it (Abs MId
id MExp o
ot) ->
                         let ([((Hiding, Nat), MId, MExp o)]
xs, MExp o
inft) = MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
ff MExp o
ot
                         in (((Hiding
h, Nat
scrut forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
xs), MId
id, forall t. Lift t => Nat -> t -> t
lift (Nat
scrut forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
xs forall a. Num a => a -> a -> a
+ Nat
1) MExp o
it) forall a. a -> [a] -> [a]
: [((Hiding, Nat), MId, MExp o)]
xs, MExp o
inft)
                        Exp o
_ -> ([], forall t. Lift t => Nat -> t -> t
lift Nat
scrut MExp o
t)
              ([((Hiding, Nat), MId, MExp o)]
newvars, MExp o
inftype) = MExp o -> ([((Hiding, Nat), MId, MExp o)], MExp o)
ff (forall o. ConstDef o -> MExp o
cdtype ConstDef o
cond)
              constrapp :: MExp o
constrapp = forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. ConstRef o -> Elr o
Const ConstRef o
con) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\MArgList o
xs ((Hiding
h, Nat
v), MId
_, MExp o
_) -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
h (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Nat -> Elr o
Var Nat
v) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) MArgList o
xs) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil) (forall a. [a] -> [a]
reverse [((Hiding, Nat), MId, MExp o)]
newvars))
              pconstrapp :: CSPatI o
pconstrapp = forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef o
con (forall a b. (a -> b) -> [a] -> [b]
map (\((Hiding
hid, Nat
v), MId
_, MExp o
_) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Nat -> CSPatI o
CSPatVar Nat
v)) [((Hiding, Nat), MId, MExp o)]
newvars)
              thesub :: MExp o -> MExp o
thesub = forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
scrut (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
newvars) MExp o
constrapp
              Id String
newvarprefix = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ (forall a. [HI a] -> [a]
drophid CSCtx o
ctx) forall a. HasCallStack => [a] -> Nat -> a
!! Nat
scrut
              ctx1 :: CSCtx o
ctx1 = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
take Nat
scrut CSCtx o
ctx) forall a. [a] -> [a] -> [a]
++
                     forall a. [a] -> [a]
reverse (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\((Hiding
hid, Nat
_), MId
id, MExp o
t) Integer
i ->
                       forall a. Hiding -> a -> HI a
HI Hiding
hid (String -> MId
Id (case MId
id of {MId
NoId -> String
newvarprefix{- ++ show i-}; Id String
id -> String
id}), MExp o
t)
                      ) [((Hiding, Nat), MId, MExp o)]
newvars [Integer
0..]) forall a. [a] -> [a] -> [a]
++
                     forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
drop (Nat
scrut forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx)
              tt' :: MExp o
tt' = MExp o -> MExp o
thesub MExp o
tt
              pats' :: [CSPat o]
pats' = forall a b. (a -> b) -> [a] -> [b]
map (forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
scrut (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
newvars) CSPatI o
pconstrapp MExp o
constrapp) [CSPat o]
pats
              scruttype' :: MExp o
scruttype' = MExp o -> MExp o
thesub MExp o
scruttype  -- 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 forall o. MExp o -> MExp o -> Maybe [(Nat, MExp o)]
unifyexp MExp o
inftype MExp o
scruttype' of
           Maybe [(Nat, MExp o)]
Nothing -> do
            Bool
res <- forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal Nat
scrut (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
newvars) MExp o
scruttype' MExp o
inftype
            if Bool
res then -- branch absurd
              [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
             else -- branch dont know
              forall (m :: * -> *) a. Monad m => a -> m a
return []
           Just [(Nat, MExp o)]
unif ->
            do
             let (CSCtx o
ctx2, MExp o
tt2, [CSPat o]
pats2) = forall o.
CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
removevar CSCtx o
ctx1 MExp o
tt' [CSPat o]
pats' [(Nat, MExp o)]
unif
                 --cost = if elem scrut mblkvar then costCaseSplit - (costCaseSplit - costCaseSplitFollow) `div` (length mblkvar) else costCaseSplit
                 cost :: Cost
cost
                   | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar Bool -> Bool -> Bool
&& Nat
scrut forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
nscrutavoid Bool -> Bool -> Bool
&& Bool
nothid
                                                                = Cost
costCaseSplitLow forall a. Num a => a -> a -> a
+
                                                                  Cost
costAddVarDepth forall a. Num a => a -> a -> a
*
                                                                  Nat -> Cost
Cost (forall o. Nat -> [CSPat o] -> Nat
depthofvar Nat
scrut [CSPat o]
pats)
                   | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar                               = Cost
costCaseSplitVeryHigh
                   | Nat
scrut forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Nat]
mblkvar                       = Cost
costCaseSplitLow
                   | Nat
scrut forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
nscrutavoid Bool -> Bool -> Bool
&& Bool
nothid = Cost
costCaseSplitHigh
                   | Bool
otherwise                                  = Cost
costCaseSplitVeryHigh

                 nothid :: Bool
nothid = let HI Hiding
hid (MId, MExp o)
_ = CSCtx o
ctx forall a. HasCallStack => [a] -> Nat -> a
!! Nat
scrut
                          in Hiding
hid forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden


             [Sol o]
sols <- Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc (Cost
depth forall a. Num a => a -> a -> a
- Cost
cost) (forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
scrut) CSCtx o
ctx2 MExp o
tt2 [CSPat o]
pats2
             case [Sol o]
sols of
              [] -> forall (m :: * -> *) a. Monad m => a -> m a
return []
              [Sol o]
_ -> do
               [Sol o]
sols2 <- [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Sol o
sol -> forall a b. (a -> b) -> [a] -> [b]
map (\Sol o
sol2 -> Sol o
sol forall a. [a] -> [a] -> [a]
++ Sol o
sol2) [Sol o]
sols2) [Sol o]
sols
       DeclCont o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"
     Exp o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"

infertypevar :: CSCtx o -> Nat -> MExp o
infertypevar :: forall o. CSCtx o -> Nat -> MExp o
infertypevar CSCtx o
ctx Nat
v = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ (forall a. [HI a] -> [a]
drophid CSCtx o
ctx) forall a. HasCallStack => [a] -> Nat -> a
!! Nat
v

class Replace t u where
  type ReplaceWith t u
  replace' :: Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u

replace :: Replace t u => Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace :: forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
sv Nat
nnew MExp (ReplaceWith t u)
e t
t = forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
0 MExp (ReplaceWith t u)
e t
t forall r a. Reader r a -> r -> a
`runReader` (Nat
sv, Nat
nnew)

instance Replace t u => Replace (Abs t) (Abs u) where
  type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u
  replace' :: Nat
-> MExp (ReplaceWith (Abs t) (Abs u))
-> Abs t
-> Reader (Nat, Nat) (Abs u)
replace' Nat
n MExp (ReplaceWith (Abs t) (Abs u))
re (Abs MId
mid t
b) = forall a. MId -> a -> Abs a
Abs MId
mid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) MExp (ReplaceWith (Abs t) (Abs u))
re t
b

instance Replace (Exp o) (MExp o) where
  type ReplaceWith (Exp o) (MExp o) = o
  replace' :: Nat
-> MExp (ReplaceWith (Exp o) (MExp o))
-> Exp o
-> Reader (Nat, Nat) (MExp o)
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
ok elr :: Elr o
elr@(Var Nat
v) MArgList o
args -> do
      MArgList o
ih         <- forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
      (Nat
sv, Nat
nnew) <- forall r (m :: * -> *). MonadReader r m => m r
ask
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        if Nat
v forall a. Ord a => a -> a -> Bool
>= Nat
n
        then if Nat
v forall a. Num a => a -> a -> a
- Nat
n forall a. Eq a => a -> a -> Bool
== Nat
sv
             then forall o. MExp o -> MArgList o -> MExp o
betareduce (forall t. Lift t => Nat -> t -> t
lift Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re) MArgList o
ih
             else if Nat
v forall a. Num a => a -> a -> a
- Nat
n forall a. Ord a => a -> a -> Bool
> Nat
sv
                  then forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok (forall o. Nat -> Elr o
Var (Nat
v forall a. Num a => a -> a -> a
+ Nat
nnew forall a. Num a => a -> a -> a
- Nat
1)) MArgList o
ih
                  else forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
ih
        else forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
ih
    App Maybe (UId o)
uid OKHandle (RefInfo o)
ok elr :: Elr o
elr@Const{} MArgList o
args ->
      forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
    Lam Hiding
hid Abs (MExp o)
b -> forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) MExp (ReplaceWith (Exp o) (MExp o))
re Abs (MExp o)
b
    Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it Abs (MExp o)
b ->
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re MExp o
it forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (Exp o) (MExp o))
re Abs (MExp o)
b
    e :: Exp o
e@Sort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM Exp o
e
    e :: Exp o
e@AbsurdLambda{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM Exp o
e

instance Replace t u => Replace (MM t (RefInfo o)) u where
  type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u
  replace' :: Nat
-> MExp (ReplaceWith (MM t (RefInfo o)) u)
-> MM t (RefInfo o)
-> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MM t (RefInfo o)) u)
re = forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MM t (RefInfo o)) u)
re forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__

instance Replace (ArgList o) (ArgList o) where
  type ReplaceWith (ArgList o) (ArgList o) = o
  replace' :: Nat
-> MExp (ReplaceWith (ArgList o) (ArgList o))
-> ArgList o
-> Reader (Nat, Nat) (ArgList o)
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re ArgList o
args = case ArgList o
args of
    ArgList o
ALNil           -> forall (m :: * -> *) a. Monad m => a -> m a
return forall o. ArgList o
ALNil
    ALCons Hiding
hid MExp o
a MArgList o
as ->
      forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re MExp o
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as)
    ALProj{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
    ALConPar MArgList o
as     -> forall o. MArgList o -> ArgList o
ALConPar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as


betareduce :: MExp o -> MArgList o -> MExp o
betareduce :: forall o. MExp o -> MArgList o -> MExp o
betareduce MExp o
e MArgList o
args = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MArgList o
args of
 ArgList o
ALNil -> MExp o
e
 ALCons Hiding
_ MExp o
a MArgList o
rargs -> case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MExp o
e of
  App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
eargs -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr (forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
eargs MArgList o
args)
  Lam Hiding
_ (Abs MId
_ MExp o
b) -> forall o. MExp o -> MArgList o -> MExp o
betareduce (forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
0 Nat
0 MExp o
a MExp o
b) MArgList o
rargs
  Exp o
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- not type correct if this happens
 ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
 ALConPar MArgList o
as -> forall a. HasCallStack => a
__IMPOSSIBLE__

concatargs :: MArgList o -> MArgList o -> MArgList o
concatargs :: forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MArgList o
xs of
  ArgList o
ALNil -> MArgList o
ys

  ALCons Hiding
hid MExp o
x MArgList o
xs -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp o
x (forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys)

  ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

  ALConPar MArgList o
as -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. MArgList o -> ArgList o
ALConPar (forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys)

replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
sv Nat
nnew CSPatI o
rp MExp o
re = CSPat o -> CSPat o
r
 where
  r :: CSPat o -> CSPat o
  r :: CSPat o -> CSPat o
r (HI Hiding
hid (CSPatConApp ConstRef o
c [CSPat o]
ps)) = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef o
c (forall a b. (a -> b) -> [a] -> [b]
map CSPat o -> CSPat o
r [CSPat o]
ps))
  r (HI Hiding
hid (CSPatVar Nat
v)) | Nat
v forall a. Eq a => a -> a -> Bool
== Nat
sv   = forall a. Hiding -> a -> HI a
HI Hiding
hid CSPatI o
rp
                          | Nat
v forall a. Ord a => a -> a -> Bool
> Nat
sv    = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Nat -> CSPatI o
CSPatVar (Nat
v forall a. Num a => a -> a -> a
+ Nat
nnew forall a. Num a => a -> a -> a
- Nat
1))
                          | Bool
otherwise = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Nat -> CSPatI o
CSPatVar Nat
v)
  r (HI Hiding
hid (CSPatExp MExp o
e)) = forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. MExp o -> CSPatI o
CSPatExp forall a b. (a -> b) -> a -> b
$ forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
sv Nat
nnew MExp o
re MExp o
e)

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

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

notequal :: Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal :: forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal Nat
fstnew Nat
nbnew t
t1 t
t2 = forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' t
t1 t
t2 forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (Nat
fstnew, Nat
nbnew)
                                              forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` []

instance (Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) where
  type UnifiesTo (MM t (RefInfo o)) = o

  unify' :: MM t (RefInfo o)
-> MM t (RefInfo o)
-> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()
unify' = forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__

  notequal' :: MM t (RefInfo o)
-> MM t (RefInfo o)
-> ReaderT
     (Nat, Nat)
     (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO)
     Bool
notequal' = forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__

unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar :: forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e = do
  Assignments o
unif <- forall s (m :: * -> *). MonadState s m => m s
get
  case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
v Assignments o
unif of
    Maybe (Exp o)
Nothing -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Nat
v, Exp o
e) forall a. a -> [a] -> [a]
:)
    Just Exp o
e' -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Exp o
e Exp o
e'

instance Unify t => Unify (Abs t) where
  type UnifiesTo (Abs t) = UnifiesTo t
  unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe ()
unify' (Abs MId
_ t
b1) (Abs MId
_ t
b2) = forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' t
b1 t
b2

  notequal' :: Abs t
-> Abs t
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool
notequal' (Abs MId
_ t
b1) (Abs MId
_ t
b2) = forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' t
b1 t
b2

instance Unify (Exp o) where
  type UnifiesTo (Exp o) = o

  unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()
unify' Exp o
e1 Exp o
e2 = case (Exp o
e1, Exp o
e2) of
   (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr1 MArgList o
args1, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr2 MArgList o
args2) | Elr o
elr1 forall a. Eq a => a -> a -> Bool
== Elr o
elr2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
args1 MArgList o
args2
   (Lam Hiding
hid1 Abs (MExp o)
b1, Lam Hiding
hid2 Abs (MExp o)
b2)               | Hiding
hid1 forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
   (Pi Maybe (UId o)
_ Hiding
hid1 Bool
_ MExp o
a1 Abs (MExp o)
b1, Pi Maybe (UId o)
_ Hiding
hid2 Bool
_ MExp o
a2 Abs (MExp o)
b2)   | Hiding
hid1 forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MExp o
a1 MExp o
a2
                                                           forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
   (Sort Sort
_, Sort Sort
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return () -- a bit sloppy
   (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil), Exp o
_)
     | Nat
v forall a. Ord a => a -> Set a -> Bool
`Set.member` (forall t. FreeVars t => t -> Set Nat
freeVars Exp o
e2) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing -- Occurs check
   (Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil))
     | Nat
v forall a. Ord a => a -> Set a -> Bool
`Set.member` (forall t. FreeVars t => t -> Set Nat
freeVars Exp o
e1) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing -- Occurs check
   (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil), Exp o
_) -> forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e2
   (Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) (NotM ArgList o
ALNil)) -> forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e1
   (Exp o, Exp o)
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing

  notequal' :: Exp o
-> Exp o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
notequal' Exp o
e1 Exp o
e2 = do
    (Nat
fstnew, Nat
nbnew) <- forall r (m :: * -> *). MonadReader r m => m r
ask
    Assignments o
unifier         <- forall s (m :: * -> *). MonadState s m => m s
get
    case (Exp o
e1, Exp o
e2) of
      (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr1 MArgList o
es1, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr2 MArgList o
es2) | Elr o
elr1 forall a. Eq a => a -> a -> Bool
== Elr o
elr2 -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
      (Exp o
_, App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v2) (NotM ArgList o
ALNil)) -- why is this not symmetric?!
        | Nat
fstnew forall a. Ord a => a -> a -> Bool
<= Nat
v2 Bool -> Bool -> Bool
&& Nat
v2 forall a. Ord a => a -> a -> Bool
< Nat
fstnew forall a. Num a => a -> a -> a
+ Nat
nbnew ->
        case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
v2 Assignments o
unifier of
          Maybe (Exp o)
Nothing  -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Nat
v2, Exp o
e1)forall a. a -> [a] -> [a]
:) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Just Exp o
e2' -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' Exp o
e1 Exp o
e2'
{-
  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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef o
c1
        ConstDef o
cd2 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef o
c2
        case (forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd1, forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd2) of
          (Constructor{}, Constructor{}) -> if ConstRef o
c1 forall a. Eq a => a -> a -> Bool
== ConstRef o
c2 then forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
                                            else forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          (DeclCont o, DeclCont o)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
{- 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)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

instance Unify (ArgList o) where
  type UnifiesTo (ArgList o) = o

  unify' :: ArgList o
-> ArgList o
-> StateT (Assignments (UnifiesTo (ArgList o))) Maybe ()
unify' ArgList o
args1 ArgList o
args2 = case (ArgList o
args1, ArgList o
args2) of
   (ArgList o
ALNil, ArgList o
ALNil) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
   (ALCons Hiding
hid1 MExp o
a1 MArgList o
as1, ALCons Hiding
hid2 MExp o
a2 MArgList o
as2) | Hiding
hid1 forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MExp o
a1 MExp o
a2
                                                           forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
   (ALConPar MArgList o
as1, ALCons Hiding
_ MExp o
_ MArgList o
as2) -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
   (ALCons Hiding
_ MExp o
_ MArgList o
as1, ALConPar MArgList o
as2) -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
   (ALConPar MArgList o
as1, ALConPar MArgList o
as2)   -> forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' MArgList o
as1 MArgList o
as2
   (ArgList o, ArgList o)
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
St.lift forall a. Maybe a
Nothing

  notequal' :: ArgList o
-> ArgList o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool
notequal' ArgList o
args1 ArgList o
args2 = case (ArgList o
args1, ArgList o
args2) of
    (ALCons Hiding
_ MExp o
e MArgList o
es, ALCons Hiding
_ MExp o
f MArgList o
fs) -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MExp o
e MExp o
f forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es MArgList o
fs
    (ALConPar MArgList o
es1, ALConPar MArgList o
es2)   -> forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
    (ArgList o, ArgList o)
_                              -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- This definition is only here to respect the previous interface.
unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
unifyexp :: forall o. MExp o -> MExp o -> Maybe [(Nat, MExp o)]
unifyexp MExp o
e1 MExp o
e2 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a blk. a -> MM a blk
NotM forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
unify MExp o
e1 MExp o
e2

class Lift t where
  lift' :: Nat -> Nat -> t -> t

lift :: Lift t => Nat -> t -> t
lift :: forall t. Lift t => Nat -> t -> t
lift Nat
0 = forall a. a -> a
id
lift Nat
n = forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
0

instance Lift t => Lift (Abs t) where
  lift' :: Nat -> Nat -> Abs t -> Abs t
lift' Nat
n Nat
j (Abs MId
mid t
b) = forall a. MId -> a -> Abs a
Abs MId
mid (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n (Nat
j forall a. Num a => a -> a -> a
+ Nat
1) t
b)

instance Lift t => Lift (MM t r) where
  lift' :: Nat -> Nat -> MM t r -> MM t r
lift' Nat
n Nat
j = forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__

instance Lift (Exp o) where
  lift' :: Nat -> Nat -> Exp o -> Exp o
lift' Nat
n Nat
j = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
args -> case Elr o
elr of
      Var Nat
v | Nat
v forall a. Ord a => a -> a -> Bool
>= Nat
j -> forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok (forall o. Nat -> Elr o
Var (Nat
v forall a. Num a => a -> a -> a
+ Nat
n)) (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
args)
      Elr o
_ -> forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
args)
    Lam Hiding
hid Abs (MExp o)
b -> forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j Abs (MExp o)
b)
    Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it Abs (MExp o)
b -> forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MExp o
it) (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j Abs (MExp o)
b)
    e :: Exp o
e@Sort{} -> Exp o
e
    e :: Exp o
e@AbsurdLambda{} -> Exp o
e

instance Lift (ArgList o) where
  lift' :: Nat -> Nat -> ArgList o -> ArgList o
lift' Nat
n Nat
j ArgList o
args = case ArgList o
args of
    ArgList o
ALNil           -> forall o. ArgList o
ALNil
    ALCons Hiding
hid MExp o
a MArgList o
as -> forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MExp o
a) (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
as)
    ALProj{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
    ALConPar MArgList o
as     -> forall o. MArgList o -> ArgList o
ALConPar (forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MArgList o
as)


removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])
removevar :: forall o.
CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
removevar CSCtx o
ctx MExp o
tt [CSPat o]
pats [] = (CSCtx o
ctx, MExp o
tt, [CSPat o]
pats)
removevar CSCtx o
ctx MExp o
tt [CSPat o]
pats ((Nat
v, MExp o
e) : [(Nat, MExp o)]
unif) =
 let
  e2 :: MExp o
e2 = forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
v Nat
0 forall a. HasCallStack => a
__IMPOSSIBLE__ {- occurs check failed -} MExp o
e
  thesub :: MExp o -> MExp o
thesub = forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
v Nat
0 MExp o
e2
  ctx1 :: CSCtx o
ctx1 = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
take Nat
v CSCtx o
ctx) forall a. [a] -> [a] -> [a]
++
         forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, MExp o -> MExp o
thesub MExp o
t)) (forall a. Nat -> [a] -> [a]
drop (Nat
v forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx)
  tt' :: MExp o
tt' = MExp o -> MExp o
thesub MExp o
tt
  pats' :: [CSPat o]
pats' = forall a b. (a -> b) -> [a] -> [b]
map (forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
v Nat
0 (forall o. MExp o -> CSPatI o
CSPatExp MExp o
e2) MExp o
e2) [CSPat o]
pats
  unif' :: [(Nat, MExp o)]
unif' = forall a b. (a -> b) -> [a] -> [b]
map (\(Nat
uv, MExp o
ue) -> (if Nat
uv forall a. Ord a => a -> a -> Bool
> Nat
v then Nat
uv forall a. Num a => a -> a -> a
- Nat
1 else Nat
uv, MExp o -> MExp o
thesub MExp o
ue)) [(Nat, MExp o)]
unif
 in
  forall o.
CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
removevar CSCtx o
ctx1 MExp o
tt' [CSPat o]
pats' [(Nat, MExp o)]
unif'

findperm :: [MExp o] -> Maybe [Nat]
findperm :: forall o. [MExp o] -> Maybe [Nat]
findperm [MExp o]
ts =
 let
  frees :: [[Nat]]
frees = forall a b. (a -> b) -> [a] -> [b]
map forall t. FreeVars t => t -> [Nat]
freevars [MExp o]
ts
  m :: IntMap Nat
m = forall a. [(Nat, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> (Nat
i, forall (t :: * -> *) a. Foldable t => t a -> Nat
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Nat
i) [[Nat]]
frees)))
          [Nat
0..forall (t :: * -> *) a. Foldable t => t a -> Nat
length [MExp o]
ts forall a. Num a => a -> a -> a
- Nat
1]
  r :: IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r IntMap Nat
_ [Nat]
perm Nat
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Nat]
perm
  r IntMap Nat
m [Nat]
perm Nat
n =
   case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
0 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> (b, a)
swap (forall a. IntMap a -> [(Nat, a)]
IntMap.toList IntMap Nat
m)) of
    Maybe Nat
Nothing -> forall a. Maybe a
Nothing
    Just Nat
i -> IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> Nat -> IntMap a -> IntMap a
IntMap.adjust (forall a. Num a => a -> a -> a
subtract Nat
1))
                       (forall a. Nat -> a -> IntMap a -> IntMap a
IntMap.insert Nat
i (-Nat
1) IntMap Nat
m)
                       ([[Nat]]
frees forall a. HasCallStack => [a] -> Nat -> a
!! Nat
i))
                 (Nat
i forall a. a -> [a] -> [a]
: [Nat]
perm) (Nat
n forall a. Num a => a -> a -> a
- Nat
1)
 in IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r IntMap Nat
m [] (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [MExp o]
ts)


freevars :: FreeVars t => t -> [Nat]
freevars :: forall t. FreeVars t => t -> [Nat]
freevars = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FreeVars t => t -> Set Nat
freeVars

applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] ->
             (CSCtx o, MExp o, [CSPat o])
applyperm :: forall o.
[Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
applyperm [Nat]
perm CSCtx o
ctx MExp o
tt [CSPat o]
pats =
 let ctx1 :: CSCtx o
ctx1 = forall a b. (a -> b) -> [a] -> [b]
map (\(HI Hiding
hid (MId
id, MExp o
t)) -> forall a. Hiding -> a -> HI a
HI Hiding
hid (MId
id, forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm) MExp o
t)) CSCtx o
ctx
     ctx2 :: CSCtx o
ctx2 = forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> CSCtx o
ctx1 forall a. HasCallStack => [a] -> Nat -> a
!! Nat
i) [Nat]
perm
     ctx3 :: CSCtx o
ctx3 = forall o. CSCtx o -> CSCtx o
seqctx CSCtx o
ctx2
     tt' :: MExp o
tt' = forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm) MExp o
tt
     pats' :: [CSPat o]
pats' = forall a b. (a -> b) -> [a] -> [b]
map (forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm)) [CSPat o]
pats
 in (CSCtx o
ctx3, MExp o
tt', [CSPat o]
pats')

ren :: [Nat] -> Nat -> Int
ren :: [Nat] -> Nat -> Nat
ren [Nat]
n Nat
i = let Just Nat
j = forall a. Eq a => a -> [a] -> Maybe Nat
elemIndex Nat
i [Nat]
n in Nat
j

instance Renaming t => Renaming (HI t) where
  renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t
renameOffset Nat
j Nat -> Nat
ren (HI Hiding
hid t
t) = forall a. Hiding -> a -> HI a
HI Hiding
hid forall a b. (a -> b) -> a -> b
$ forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren t
t

instance Renaming (CSPatI o) where
  renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o
renameOffset Nat
j Nat -> Nat
ren = \case
    CSPatConApp ConstRef o
c [CSPat o]
pats -> forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef o
c forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren) [CSPat o]
pats
    CSPatVar Nat
i         -> forall o. Nat -> CSPatI o
CSPatVar forall a b. (a -> b) -> a -> b
$ Nat
j forall a. Num a => a -> a -> a
+ Nat -> Nat
ren Nat
i
    CSPatExp MExp o
e         -> forall o. MExp o -> CSPatI o
CSPatExp forall a b. (a -> b) -> a -> b
$ forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren MExp o
e
    e :: CSPatI o
e@CSPatI o
CSOmittedArg     -> CSPatI o
e
    CSPatI o
_                  -> forall a. HasCallStack => a
__IMPOSSIBLE__

seqctx :: CSCtx o -> CSCtx o
seqctx :: forall o. CSCtx o -> CSCtx o
seqctx = forall {b} {a}. Lift b => Nat -> [HI (a, b)] -> [HI (a, b)]
r (-Nat
1)
 where
  r :: Nat -> [HI (a, b)] -> [HI (a, b)]
r Nat
_ [] = []
  r Nat
n (HI Hiding
hid (a
id, b
t) : [HI (a, b)]
ctx) = forall a. Hiding -> a -> HI a
HI Hiding
hid (a
id, forall t. Lift t => Nat -> t -> t
lift Nat
n b
t) forall a. a -> [a] -> [a]
: Nat -> [HI (a, b)] -> [HI (a, b)]
r (Nat
n forall a. Num a => a -> a -> a
- Nat
1) [HI (a, b)]
ctx
-- --------------------

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

-- --------------------
-- | 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 Nat, [Nat])
sizeAndBoundVars (HI Hiding
_ a
p) = forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars a
p

instance LocalTerminationEnv (CSPatI o) where
  sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat])
sizeAndBoundVars = \case
    CSPatConApp ConstRef o
_ [CSPat o]
ps -> (Sum Nat
1, []) forall a. Semigroup a => a -> a -> a
<> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars [CSPat o]
ps
    CSPatVar Nat
n       -> (Sum Nat
0, [Nat
n])
    CSPatExp MExp o
e       -> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars MExp o
e
    CSPatI o
_                -> (Sum Nat
0, [])

instance LocalTerminationEnv a => LocalTerminationEnv [a] where
  sizeAndBoundVars :: [a] -> (Sum Nat, [Nat])
sizeAndBoundVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars

instance LocalTerminationEnv (MExp o) where
--  sizeAndBoundVars e = case rm __IMPOSSIBLE__ e of
-- GA: 2017 06 27: Not actually impossible! (cf. #2620)
  sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])
sizeAndBoundVars Meta{} = (Sum Nat
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 Nat
v) MArgList o
_      -> (Sum Nat
0, [Nat
v])
    App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
_) MArgList o
args -> (Sum Nat
1, []) forall a. Semigroup a => a -> a -> a
<> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars MArgList o
args
    Exp o
_                      -> (Sum Nat
0, [])

instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where
  sizeAndBoundVars :: (a, b) -> (Sum Nat, [Nat])
sizeAndBoundVars (a
a, b
b) = forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars a
a forall a. Semigroup a => a -> a -> a
<> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars b
b

instance LocalTerminationEnv (MArgList o) where
  sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])
sizeAndBoundVars MArgList o
as = case forall a b. Empty -> MM a b -> a
rm forall a. HasCallStack => a
__IMPOSSIBLE__ MArgList o
as of
    ArgList o
ALNil         -> (Sum Nat
0, [])
    ALCons Hiding
_ MExp o
a MArgList o
as -> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars (MExp o
a, MArgList o
as)
    ALProj{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    ALConPar MArgList o
as   -> forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars MArgList o
as


-- | 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 :: forall o. [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv [CSPat o]
pats = ([Nat]
is, forall a. Sum a -> a
getSum Sum Nat
s, [Nat]
vs) where

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

  g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
  g :: forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g Nat
_ [] = ([], Sum Nat
0, [])
  g Nat
i (hp :: CSPat o
hp@(HI Hiding
_ CSPatI o
p) : [CSPat o]
ps) = case CSPatI o
p of
    CSPatConApp{} -> let (Sum Nat
size, [Nat]
vars) = forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars CSPat o
hp
                     in ([Nat
i], Sum Nat
size, [Nat]
vars) forall a. Semigroup a => a -> a -> a
<> forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) [CSPat o]
ps
    CSPatI o
_ -> forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) [CSPat o]
ps

localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond :: forall o.
([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond ([Nat]
is, Nat
size, [Nat]
vars) ConstRef o
reccallc MExp o
b =
  MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
b
 where
     ok :: MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
e = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MExp o
e forall a b. (a -> b) -> a -> b
$ \Exp o
e -> case Exp o
e of
      App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr MArgList o
args -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
       (MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
args)
       (case Elr o
elr of
          Const ConstRef o
c | ConstRef o
c forall a. Eq a => a -> a -> Bool
== ConstRef o
reccallc -> if Nat
size forall a. Eq a => a -> a -> Bool
== Nat
0 then forall blk. Prop blk -> MetaEnv (PB blk)
mpret (forall blk. String -> Prop blk
Error String
"localTerminationSidecond: no size to decrement") else Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall Nat
0 Nat
size [Nat]
vars MArgList o
args
          Elr o
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
       )
      Lam Hiding
_ (Abs MId
_ MExp o
e) -> MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
e
      Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ MExp o
ot) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
       (MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
it)
       (MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
ot)
      Sort{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK

      AbsurdLambda{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK


     oks :: MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
ALNil -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
      ALCons Hiding
_ MExp o
a MArgList o
as -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition
       (MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
a)
       (MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as)

      ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ MArgList o
as -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
eas) (MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as)


      ALConPar MArgList o
as -> MArgList o -> MetaEnv (PB (RefInfo o))
oks MArgList o
as

     okcall :: Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall Nat
i Nat
size [Nat]
vars MArgList o
as = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
ALNil -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
      ALCons Hiding
_ MExp o
a MArgList o
as | Nat
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Nat]
is ->
       forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioNo forall a. Maybe a
Nothing (forall {t} {o}.
(Eq t, Num t) =>
t
-> [Nat]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
he Nat
size [Nat]
vars MExp o
a) forall a b. (a -> b) -> a -> b
$ \Maybe (Nat, [Nat])
x -> case Maybe (Nat, [Nat])
x of
        Maybe (Nat, [Nat])
Nothing -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error String
"localTerminationSidecond: reccall not ok"
        Just (Nat
size', [Nat]
vars') -> Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) Nat
size' [Nat]
vars' MArgList o
as
      ALCons Hiding
_ MExp o
a MArgList o
as -> Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) Nat
size [Nat]
vars MArgList o
as

      ALProj{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK


      ALConPar MArgList o
as -> forall a. HasCallStack => a
__IMPOSSIBLE__

     he :: t
-> [Nat]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
he t
size [Nat]
vars MM (Exp o) (RefInfo o)
e = forall a blk b.
Refinable a blk =>
MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmcase MM (Exp o) (RefInfo o)
e forall a b. (a -> b) -> a -> b
$ \Exp o
e -> case Exp o
e of
      App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) MArgList o
_ ->
       case forall {t}. Eq t => t -> [t] -> Maybe [t]
remove Nat
v [Nat]
vars of
        Maybe [Nat]
Nothing -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
        Just [Nat]
vars' -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (t
size, [Nat]
vars')
      App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) MArgList o
args -> do
       ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
       case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
        Constructor{} ->
         if t
size forall a. Eq a => a -> a -> Bool
== t
1 then
          forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
         else
          t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes (t
size forall a. Num a => a -> a -> a
- t
1) [Nat]
vars MArgList o
args
        DeclCont o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
      Exp o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
     hes :: t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes t
size [Nat]
vars MArgList o
as = forall a blk b.
Refinable a blk =>
MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmcase MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
ALNil -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (t
size, [Nat]
vars)
      ALCons Hiding
_ MM (Exp o) (RefInfo o)
a MArgList o
as ->
       forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (t
-> [Nat]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
he t
size [Nat]
vars MM (Exp o) (RefInfo o)
a) forall a b. (a -> b) -> a -> b
$ \Maybe (t, [Nat])
x -> case Maybe (t, [Nat])
x of
        Maybe (t, [Nat])
Nothing -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
        Just (t
size', [Nat]
vars') -> t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes t
size' [Nat]
vars' MArgList o
as

      ALProj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__


      ALConPar MArgList o
as -> forall a. HasCallStack => a
__IMPOSSIBLE__

     remove :: t -> [t] -> Maybe [t]
remove t
_ [] = forall a. Maybe a
Nothing
     remove t
x (t
y : [t]
ys) | t
x forall a. Eq a => a -> a -> Bool
== t
y = forall a. a -> Maybe a
Just [t]
ys
     remove t
x (t
y : [t]
ys) = case t -> [t] -> Maybe [t]
remove t
x [t]
ys of {Maybe [t]
Nothing -> forall a. Maybe a
Nothing; Just [t]
ys' -> forall a. a -> Maybe a
Just (t
y forall a. a -> [a] -> [a]
: [t]
ys')}

-- ---------------------------


getblks :: MExp o -> IO [Nat]
getblks :: forall o. MExp o -> IO [Nat]
getblks MExp o
tt = do
 NotB (HNExp o
hntt, HNNBlks o
blks) <- forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks (forall a o. [CAction o] -> a -> Clos a o
Clos [] MExp o
tt)
 case forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f HNNBlks o
blks of
  Just Nat
v -> forall (m :: * -> *) a. Monad m => a -> m a
return [Nat
v]
  Maybe Nat
Nothing -> case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntt of
   HNApp (Const ConstRef o
c) ICArgList o
args -> do
    ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
    case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
     Datatype{} -> forall {o}. [Nat] -> ICArgList o -> IO [Nat]
g [] ICArgList o
args
     DeclCont o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
   HNExp' o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
 where
  f :: [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f [WithSeenUIds (HNExp' o) o]
blks = case [WithSeenUIds (HNExp' o) o]
blks of
             (WithSeenUIds (HNExp' o) o
b : [WithSeenUIds (HNExp' o) o]
bs) -> case forall a o. WithSeenUIds a o -> a
rawValue (forall a. a -> [a] -> a
last1 WithSeenUIds (HNExp' o) o
b [WithSeenUIds (HNExp' o) o]
bs) of
              HNApp (Var Nat
v) ICArgList o
_ -> forall a. a -> Maybe a
Just Nat
v
              HNExp' o
_ -> forall a. Maybe a
Nothing
             [WithSeenUIds (HNExp' o) o]
_ -> forall a. Maybe a
Nothing
  g :: [Nat] -> ICArgList o -> IO [Nat]
g [Nat]
vs ICArgList o
args = do
   NotB HNArgList o
hnargs <- forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args
   case HNArgList o
hnargs of
    HNALCons Hiding
_ ICExp o
a ICArgList o
as -> do
     NotB (HNExp o
_, HNNBlks o
blks) <- forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
a
     let vs' :: [Nat]
vs' = case forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f HNNBlks o
blks of
                Just Nat
v | Nat
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Nat]
vs -> Nat
v forall a. a -> [a] -> [a]
: [Nat]
vs
                Maybe Nat
_ -> [Nat]
vs
     [Nat] -> ICArgList o -> IO [Nat]
g [Nat]
vs' ICArgList o
as
    HNArgList o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [Nat]
vs
-- ---------------------------