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 (on)
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 = (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]
              | 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 <- Nat -> IO (IORef Nat)
forall a. a -> IO (IORef a)
newIORef Nat
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
                    (([Nat], Nat, [Nat])
-> ConstRef o -> MExp o -> MetaEnv (PB (RefInfo o))
forall o.
([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond ([Nat], Nat, [Nat])
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 a b. (a -> b) -> (MId, a) -> (MId, b)
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 { 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 :: Nat
rieDefFreeVars = ConstDef o -> Nat
forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
recdefd
                      , rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
rieEqReasoningConsts = Maybe (EqReasoningConsts o)
meqr
                      }
      Bool
depreached <- IORef Nat
-> IORef Nat
-> IO ()
-> RefInfo o
-> MetaEnv (PB (RefInfo o))
-> Cost
-> Cost
-> IO Bool
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 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' = Nat -> CSCtx o -> CSCtx o
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) = Hiding -> (a, b) -> HI (a, b)
forall a. Hiding -> a -> HI a
HI Hiding
hid (a
id, Nat -> b -> b
forall t. Lift t => Nat -> t -> t
lift Nat
n b
t) HI (a, b) -> [HI (a, b)] -> [HI (a, b)]
forall a. a -> [a] -> [a]
: Nat -> [HI (a, b)] -> [HI (a, b)]
ff (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [HI (a, b)]
ctx
 (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]
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 <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
recdef
  Cost -> Nat -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc Cost
depth (ConstDef o -> Nat
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 Cost -> Cost -> Bool
forall a. Ord a => a -> a -> Bool
< Cost
0 = [Sol o] -> IO [Sol o]
forall a. a -> IO a
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 <- MExp o -> IO [Nat]
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]
_) -> [Sol o] -> IO [Sol o]
forall a. a -> IO a
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 [] = [Sol o] -> IO [Sol o]
forall a. a -> IO a
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]
_) -> [Sol o] -> IO [Sol o]
forall a. a -> IO a
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 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
x | Nat
x <- [Nat
0..Nat
nv]] -- [0..length ctx - 1 - nscrutavoid]
    where nv :: Nat
nv = CSCtx o -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
   dobody :: IO [Sol o]
   dobody :: IO [Sol o]
dobody = do
    case [MExp o] -> Maybe [Nat]
forall o. [MExp o] -> Maybe [Nat]
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 [Nat]
perm -> do
      let (CSCtx o
ctx', MExp o
tt', [CSPat o]
pats') = [Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
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' ([CSPat o] -> ([Nat], Nat, [Nat])
forall o. [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv [CSPat o]
pats')
      [Sol o] -> IO [Sol o]
forall a. a -> IO a
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 [Nat]
Nothing -> IO [Sol o]
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 = CSCtx o -> Nat -> MExp o
forall o. CSCtx o -> Nat -> MExp o
infertypevar CSCtx o
ctx Nat
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 a. a -> IO a
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 [Nat]
forall o. [MExp o] -> Maybe [Nat]
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 [Nat]
perm ->
             let HI Hiding
scrhid(MId
_, MExp o
scrt) = CSCtx o
ctx CSCtx o -> Nat -> HI (MId, MExp o)
forall a. HasCallStack => [a] -> Nat -> a
!! Nat
scrut
                 ctx1 :: CSCtx o
ctx1 = Nat -> CSCtx o -> CSCtx o
forall a. Nat -> [a] -> [a]
take Nat
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]
: Nat -> CSCtx o -> CSCtx o
forall a. Nat -> [a] -> [a]
drop (Nat
scrut Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) CSCtx o
ctx
                 (CSCtx o
ctx', MExp o
_, [CSPat o]
pats') = [Nat]
-> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o])
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', Maybe (MExp o)
forall a. Maybe a
Nothing)]
            Maybe [Nat]
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 a. a -> IO a
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, Nat), 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, 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 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ [((Hiding, Nat), MId, MExp o)] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
xs), MId
id, Nat -> MExp o -> MExp o
forall t. Lift t => Nat -> t -> t
lift (Nat
scrut Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ [((Hiding, Nat), MId, MExp o)] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), MId, MExp o)]
xs Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) MExp o
it) ((Hiding, Nat), MId, MExp o)
-> [((Hiding, Nat), MId, MExp o)] -> [((Hiding, Nat), MId, MExp o)]
forall a. a -> [a] -> [a]
: [((Hiding, Nat), MId, MExp o)]
xs, MExp o
inft)
                        Exp o
_ -> ([], Nat -> MExp o -> MExp 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 (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, Nat), MId, MExp o) -> MArgList o)
-> MArgList o -> [((Hiding, Nat), MId, MExp o)] -> MArgList o
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\MArgList o
xs ((Hiding
h, Nat
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) (Nat -> Elr o
forall o. Nat -> Elr o
Var Nat
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, Nat), MId, MExp o)] -> [((Hiding, Nat), MId, MExp o)]
forall a. [a] -> [a]
reverse [((Hiding, Nat), 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, Nat), MId, MExp o) -> CSPat o)
-> [((Hiding, Nat), MId, MExp o)] -> [CSPat o]
forall a b. (a -> b) -> [a] -> [b]
map (\((Hiding
hid, Nat
v), MId
_, MExp o
_) -> Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid (Nat -> CSPatI o
forall o. Nat -> CSPatI o
CSPatVar Nat
v)) [((Hiding, Nat), MId, MExp o)]
newvars)
              thesub :: MExp o -> MExp o
thesub = Nat
-> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
scrut ([((Hiding, Nat), MId, MExp o)] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [((Hiding, Nat), 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)] -> Nat -> (MId, MExp o)
forall a. HasCallStack => [a] -> Nat -> a
!! Nat
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)) (Nat -> CSCtx o -> CSCtx o
forall a. Nat -> [a] -> [a]
take Nat
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, Nat), MId, MExp o) -> Integer -> HI (MId, MExp o))
-> [((Hiding, Nat), MId, MExp o)] -> [Integer] -> CSCtx o
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\((Hiding
hid, Nat
_), 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, Nat), 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)) (Nat -> CSCtx o -> CSCtx o
forall a. Nat -> [a] -> [a]
drop (Nat
scrut Nat -> Nat -> Nat
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' = (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
forall a b. (a -> b) -> [a] -> [b]
map (Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
scrut ([((Hiding, Nat), MId, MExp o)] -> Nat
forall a. [a] -> Nat
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 MExp o -> MExp o -> Maybe [(Nat, MExp o)]
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 <- Nat -> Nat -> MExp o -> MExp o -> IO Bool
forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal Nat
scrut ([((Hiding, Nat), MId, MExp o)] -> Nat
forall a. [a] -> Nat
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
              [Sol o] -> IO [Sol o]
forall a. a -> IO a
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) = CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
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
                   | [Nat] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar Bool -> Bool -> Bool
&& Nat
scrut Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< CSCtx o -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
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
*
                                                                  Nat -> Cost
Cost (Nat -> [CSPat o] -> Nat
forall o. Nat -> [CSPat o] -> Nat
depthofvar Nat
scrut [CSPat o]
pats)
                   | [Nat] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar                               = Cost
costCaseSplitVeryHigh
                   | Nat
scrut Nat -> [Nat] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Nat]
mblkvar                       = Cost
costCaseSplitLow
                   | Nat
scrut Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< CSCtx o -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx Nat -> Nat -> Nat
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 CSCtx o -> Nat -> HI (MId, MExp o)
forall a. HasCallStack => [a] -> Nat -> a
!! Nat
scrut
                          in Hiding
hid Hiding -> Hiding -> Bool
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 Cost -> Cost -> Cost
forall a. Num a => a -> a -> a
- Cost
cost) (CSCtx o -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length CSCtx o
ctx Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
scrut) CSCtx o
ctx2 MExp o
tt2 [CSPat o]
pats2
             case [Sol o]
sols of
              [] -> [Sol o] -> IO [Sol o]
forall a. a -> IO a
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 a. a -> IO a
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"
     Exp o
_ -> [Sol o] -> IO [Sol o]
forall a. a -> IO a
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 = (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)] -> Nat -> (MId, MExp o)
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 = Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
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 Reader (Nat, Nat) u -> (Nat, Nat) -> u
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) = MId -> u -> Abs u
forall a. MId -> a -> Abs a
Abs MId
mid (u -> Abs u)
-> ReaderT (Nat, Nat) Identity u -> Reader (Nat, Nat) (Abs u)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> MExp (ReplaceWith t u) -> t -> ReaderT (Nat, Nat) Identity u
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
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' :: 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         <- ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM (ArgList o -> MArgList o)
-> ReaderT (Nat, Nat) Identity (ArgList o)
-> ReaderT (Nat, Nat) Identity (MArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> ReaderT (Nat, Nat) Identity (ArgList o)
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MArgList o) (ArgList o))
MExp (ReplaceWith (Exp o) (MExp o))
re MArgList o
args
      (Nat
sv, Nat
nnew) <- ReaderT (Nat, Nat) Identity (Nat, Nat)
forall r (m :: * -> *). MonadReader r m => m r
ask
      MExp o -> Reader (Nat, Nat) (MExp o)
forall a. a -> ReaderT (Nat, Nat) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp o -> Reader (Nat, Nat) (MExp o))
-> MExp o -> Reader (Nat, Nat) (MExp o)
forall a b. (a -> b) -> a -> b
$
        if Nat
v Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
n
        then if Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
sv
             then MExp o -> MArgList o -> MExp o
forall o. MExp o -> MArgList o -> MExp o
betareduce (Nat -> MExp o -> MExp o
forall t. Lift t => Nat -> t -> t
lift Nat
n MExp o
MExp (ReplaceWith (Exp o) (MExp o))
re) MArgList o
ih
             else if Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
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 (Nat -> Elr o
forall o. Nat -> Elr o
Var (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
nnew Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
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 (Nat, Nat) Identity (ArgList o)
-> Reader (Nat, Nat) (MExp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> ReaderT (Nat, Nat) Identity (ArgList o)
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
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 (Nat, Nat) Identity (Abs (MExp o))
-> Reader (Nat, Nat) (MExp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
-> Abs (MExp o)
-> ReaderT (Nat, Nat) Identity (Abs (MExp o))
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
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 (Nat, Nat) Identity (Exp o)
-> Reader (Nat, Nat) (MExp o)
forall a b.
(a -> b)
-> ReaderT (Nat, Nat) Identity a -> ReaderT (Nat, Nat) Identity b
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 (Nat, Nat) Identity (Exp o) -> Reader (Nat, Nat) (MExp o))
-> ReaderT (Nat, Nat) Identity (Exp o)
-> Reader (Nat, Nat) (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 (Nat, Nat) (MExp o)
-> ReaderT (Nat, Nat) Identity (Abs (MExp o) -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (MExp o) (MExp o))
-> MExp o
-> Reader (Nat, Nat) (MExp o)
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MExp o) (MExp o))
MExp (ReplaceWith (Exp o) (MExp o))
re MExp o
it ReaderT (Nat, Nat) Identity (Abs (MExp o) -> Exp o)
-> ReaderT (Nat, Nat) Identity (Abs (MExp o))
-> ReaderT (Nat, Nat) Identity (Exp o)
forall a b.
ReaderT (Nat, Nat) Identity (a -> b)
-> ReaderT (Nat, Nat) Identity a -> ReaderT (Nat, Nat) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Nat
-> MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
-> Abs (MExp o)
-> ReaderT (Nat, Nat) Identity (Abs (MExp o))
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))
MExp (ReplaceWith (Abs (MExp o)) (Abs (MExp o)))
re Abs (MExp o)
b
    e :: Exp o
e@Sort{} -> MExp o -> Reader (Nat, Nat) (MExp o)
forall a. a -> ReaderT (Nat, Nat) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp o -> Reader (Nat, Nat) (MExp o))
-> MExp o -> Reader (Nat, Nat) (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 (Nat, Nat) (MExp o)
forall a. a -> ReaderT (Nat, Nat) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp o -> Reader (Nat, Nat) (MExp o))
-> MExp o -> Reader (Nat, Nat) (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' :: 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 = Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith t u)
MExp (ReplaceWith (MM t (RefInfo o)) u)
re (t -> Reader (Nat, Nat) u)
-> (MM t (RefInfo o) -> t)
-> MM t (RefInfo o)
-> Reader (Nat, Nat) 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' :: 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           -> ArgList o -> Reader (Nat, Nat) (ArgList o)
forall a. a -> ReaderT (Nat, Nat) Identity a
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 (Nat, Nat) Identity (MExp o)
-> ReaderT (Nat, Nat) Identity (MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (MExp o) (MExp o))
-> MExp o
-> ReaderT (Nat, Nat) Identity (MExp o)
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MExp o) (MExp o))
MExp (ReplaceWith (ArgList o) (ArgList o))
re MExp o
a ReaderT (Nat, Nat) Identity (MArgList o -> ArgList o)
-> ReaderT (Nat, Nat) Identity (MArgList o)
-> Reader (Nat, Nat) (ArgList o)
forall a b.
ReaderT (Nat, Nat) Identity (a -> b)
-> ReaderT (Nat, Nat) Identity a -> ReaderT (Nat, Nat) Identity b
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 (Nat, Nat) (ArgList o)
-> ReaderT (Nat, Nat) Identity (MArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> Reader (Nat, Nat) (ArgList o)
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
n MExp (ReplaceWith (MArgList o) (ArgList o))
MExp (ReplaceWith (ArgList o) (ArgList o))
re MArgList o
as)
    ALProj{}        -> Reader (Nat, Nat) (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 (Nat, Nat) (ArgList o) -> Reader (Nat, Nat) (ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> MExp (ReplaceWith (MArgList o) (ArgList o))
-> MArgList o
-> Reader (Nat, Nat) (ArgList o)
forall t u.
Replace t u =>
Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u
replace' Nat
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 :: forall o. 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 (Nat
-> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
0 Nat
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 :: forall o. 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 :: 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)) = 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 Nat
v)) | Nat
v Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
sv   = Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid CSPatI o
rp
                          | Nat
v Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
sv    = Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid (Nat -> CSPatI o
forall o. Nat -> CSPatI o
CSPatVar (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
nnew Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1))
                          | Bool
otherwise = Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid (Nat -> CSPatI o
forall o. Nat -> CSPatI o
CSPatVar Nat
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
$ Nat
-> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
sv Nat
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 :: forall t. Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))
unify t
t t
u = t -> t -> StateT [(Nat, Exp (UnifiesTo t))] Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' t
t t
u StateT [(Nat, Exp (UnifiesTo t))] Maybe ()
-> [(Nat, Exp (UnifiesTo t))] -> Maybe [(Nat, Exp (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 :: forall t. Unify t => Nat -> Nat -> t -> t -> IO Bool
notequal Nat
fstnew Nat
nbnew t
t1 t
t2 = t
-> t
-> ReaderT (Nat, Nat) (StateT [(Nat, Exp (UnifiesTo t))] IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' t
t1 t
t2 ReaderT (Nat, Nat) (StateT [(Nat, Exp (UnifiesTo t))] IO) Bool
-> (Nat, Nat) -> StateT [(Nat, Exp (UnifiesTo t))] IO Bool
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (Nat
fstnew, Nat
nbnew)
                                              StateT [(Nat, Exp (UnifiesTo t))] IO Bool
-> [(Nat, Exp (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 [(Nat, Exp o)] Maybe ()
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
forall t.
Unify t =>
t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
unify' (t -> t -> StateT [(Nat, Exp o)] Maybe ())
-> (MM t (RefInfo o) -> t)
-> MM t (RefInfo o)
-> MM t (RefInfo o)
-> StateT [(Nat, 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
     (Nat, Nat)
     (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO)
     Bool
notequal' = t -> t -> ReaderT (Nat, Nat) (StateT [(Nat, Exp o)] IO) Bool
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' (t -> t -> ReaderT (Nat, Nat) (StateT [(Nat, Exp o)] IO) Bool)
-> (MM t (RefInfo o) -> t)
-> MM t (RefInfo o)
-> MM t (RefInfo o)
-> ReaderT (Nat, Nat) (StateT [(Nat, 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 :: forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e = do
  Assignments o
unif <- StateT (Assignments o) Maybe (Assignments o)
forall s (m :: * -> *). MonadState s m => m s
get
  case Nat -> Assignments o -> Maybe (Exp o)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
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 ((Nat
v, Exp o
e) (Nat, 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
     (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool
notequal' (Abs MId
_ t
b1) (Abs MId
_ t
b2) = t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
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 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 (Assignments o) Maybe ()
-> StateT (Assignments o) Maybe ()
-> StateT (Assignments o) Maybe ()
forall a b.
StateT (Assignments o) Maybe a
-> StateT (Assignments o) Maybe b -> StateT (Assignments o) Maybe b
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 (Assignments o) Maybe ()
forall a. a -> StateT (Assignments o) Maybe a
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 Nat -> Set Nat -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` (Exp o -> Set Nat
forall t. FreeVars t => t -> Set Nat
freeVars Exp o
e2) -> Maybe () -> StateT (Assignments o) Maybe ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Assignments o) m a
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 Nat
v) (NotM ArgList o
ALNil))
     | Nat
v Nat -> Set Nat -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` (Exp o -> Set Nat
forall t. FreeVars t => t -> Set Nat
freeVars Exp o
e1) -> Maybe () -> StateT (Assignments o) Maybe ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Assignments o) m a
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 Nat
v) (NotM ArgList o
ALNil), Exp o
_) -> Nat -> Exp o -> StateT (Assignments o) Maybe ()
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)) -> Nat -> Exp o -> StateT (Assignments o) Maybe ()
forall o. Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Nat
v Exp o
e1
   (Exp o, Exp o)
_ -> Maybe () -> StateT (Assignments o) Maybe ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Assignments o) m a
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
     (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
notequal' Exp o
e1 Exp o
e2 = do
    (Nat
fstnew, Nat
nbnew) <- ReaderT (Nat, Nat) (StateT (Assignments o) IO) (Nat, Nat)
forall r (m :: * -> *). MonadReader r m => m r
ask
    Assignments o
unifier         <- ReaderT (Nat, Nat) (StateT (Assignments o) IO) (Assignments 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
     (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
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 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
v2 Bool -> Bool -> Bool
&& Nat
v2 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
fstnew Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
nbnew ->
        case Nat -> Assignments o -> Maybe (Exp o)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
v2 Assignments o
unifier of
          Maybe (Exp o)
Nothing  -> (Assignments o -> Assignments o)
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Nat
v2, Exp o
e1)(Nat, Exp o) -> Assignments o -> Assignments o
forall a. a -> [a] -> [a]
:) ReaderT (Nat, Nat) (StateT (Assignments o) IO) ()
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall a b.
ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) b
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall a. a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Just Exp o
e2' -> Exp o
-> Exp o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool
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 <- IO (ConstDef o)
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
forall a. IO a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef o)
 -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o))
-> IO (ConstDef o)
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
forall a b. (a -> b) -> a -> b
$ ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c1
        ConstDef o
cd2 <- IO (ConstDef o)
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
forall a. IO a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef o)
 -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o))
-> IO (ConstDef o)
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) (ConstDef o)
forall a b. (a -> b) -> a -> b
$ ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c2
        case (ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd1, ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd2) of
          (Constructor{}, Constructor{}) -> if ConstRef o
c1 ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== ConstRef o
c2 then MArgList o
-> MArgList o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MArgList o
es1 MArgList o
es2
                                            else Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall a. a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          (DeclCont o, DeclCont o)
_ -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall a. a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
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 (Nat, Nat) (StateT (Assignments o) IO) Bool
forall a. a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
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 a. a -> StateT (Assignments o) Maybe a
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 a b.
StateT (Assignments o) Maybe a
-> StateT (Assignments o) Maybe b -> StateT (Assignments o) Maybe b
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 (m :: * -> *) a.
Monad m =>
m a -> StateT (Assignments o) m a
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
     (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) -> MExp o
-> MExp o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (MExp o))) IO) Bool
forall t.
Unify t =>
t
-> t
-> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool
notequal' MExp o
e MExp o
f ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
-> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` MArgList o
-> MArgList o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
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)   -> MArgList o
-> MArgList o
-> ReaderT
     (Nat, Nat) (StateT (Assignments (UnifiesTo (MArgList o))) IO) Bool
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)
_                              -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall a. a -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) a
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 = ((Nat, Exp o) -> (Nat, MExp o))
-> [(Nat, Exp o)] -> [(Nat, MExp o)]
forall a b. (a -> b) -> [a] -> [b]
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) -> (Nat, Exp o) -> (Nat, MExp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([(Nat, Exp o)] -> [(Nat, MExp o)])
-> Maybe [(Nat, Exp o)] -> Maybe [(Nat, 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 :: forall t. Lift t => Nat -> t -> t
lift Nat
0 = t -> t
forall a. a -> a
id
lift Nat
n = Nat -> Nat -> t -> t
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) = MId -> t -> Abs t
forall a. MId -> a -> Abs a
Abs MId
mid (Nat -> Nat -> t -> t
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n (Nat
j Nat -> Nat -> Nat
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 = 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
. Nat -> Nat -> t -> t
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
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' :: 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 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
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 (Nat -> Elr o
forall o. Nat -> Elr o
Var (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n)) (Nat -> Nat -> MArgList o -> MArgList o
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
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 (Nat -> Nat -> MArgList o -> MArgList o
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
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 (Nat -> Nat -> Abs (MExp o) -> Abs (MExp o)
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 -> 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 (Nat -> Nat -> MExp o -> MExp o
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MExp o
it) (Nat -> Nat -> Abs (MExp o) -> Abs (MExp o)
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           -> 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 (Nat -> Nat -> MExp o -> MExp o
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
j MExp o
a) (Nat -> Nat -> MArgList o -> MArgList o
forall t. Lift t => Nat -> Nat -> t -> t
lift' Nat
n Nat
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 (Nat -> Nat -> MArgList o -> MArgList o
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 = Nat
-> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
v Nat
0 MExp o
MExp (ReplaceWith (MExp o) (MExp o))
forall a. HasCallStack => a
__IMPOSSIBLE__ {- occurs check failed -} MExp o
e
  thesub :: MExp o -> MExp o
thesub = Nat
-> Nat -> MExp (ReplaceWith (MExp o) (MExp o)) -> MExp o -> MExp o
forall t u.
Replace t u =>
Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u
replace Nat
v Nat
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)) (Nat -> CSCtx o -> CSCtx o
forall a. Nat -> [a] -> [a]
take Nat
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)) (Nat -> CSCtx o -> CSCtx o
forall a. Nat -> [a] -> [a]
drop (Nat
v Nat -> Nat -> Nat
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' = (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
forall a b. (a -> b) -> [a] -> [b]
map (Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep Nat
v Nat
0 (MExp o -> CSPatI o
forall o. MExp o -> CSPatI o
CSPatExp MExp o
e2) MExp o
e2) [CSPat o]
pats
  unif' :: [(Nat, MExp o)]
unif' = ((Nat, MExp o) -> (Nat, MExp o))
-> [(Nat, MExp o)] -> [(Nat, MExp o)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Nat
uv, MExp o
ue) -> (if Nat
uv Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
v then Nat
uv Nat -> Nat -> Nat
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
  CSCtx o
-> MExp o
-> [CSPat o]
-> [(Nat, MExp o)]
-> (CSCtx o, MExp o, [CSPat o])
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 = (MExp o -> [Nat]) -> [MExp o] -> [[Nat]]
forall a b. (a -> b) -> [a] -> [b]
map MExp o -> [Nat]
forall t. FreeVars t => t -> [Nat]
freevars [MExp o]
ts
  m :: IntMap Nat
m = [(Nat, Nat)] -> IntMap Nat
forall a. [(Nat, a)] -> IntMap a
IntMap.fromList ([(Nat, Nat)] -> IntMap Nat) -> [(Nat, Nat)] -> IntMap Nat
forall a b. (a -> b) -> a -> b
$
      (Nat -> (Nat, Nat)) -> [Nat] -> [(Nat, Nat)]
forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> (Nat
i, [[Nat]] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length (([Nat] -> Bool) -> [[Nat]] -> [[Nat]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Nat -> [Nat] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Nat
i) [[Nat]]
frees)))
          [Nat
0..[MExp o] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [MExp o]
ts Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
  r :: IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r IntMap Nat
_ [Nat]
perm Nat
0 = [Nat] -> Maybe [Nat]
forall a. a -> Maybe a
Just ([Nat] -> Maybe [Nat]) -> [Nat] -> Maybe [Nat]
forall a b. (a -> b) -> a -> b
$ [Nat] -> [Nat]
forall a. [a] -> [a]
reverse [Nat]
perm
  r IntMap Nat
m [Nat]
perm Nat
n =
   case Nat -> [(Nat, Nat)] -> Maybe Nat
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
0 (((Nat, Nat) -> (Nat, Nat)) -> [(Nat, Nat)] -> [(Nat, Nat)]
forall a b. (a -> b) -> [a] -> [b]
map (Nat, Nat) -> (Nat, Nat)
forall a b. (a, b) -> (b, a)
swap (IntMap Nat -> [(Nat, Nat)]
forall a. IntMap a -> [(Nat, a)]
IntMap.toList IntMap Nat
m)) of
    Maybe Nat
Nothing -> Maybe [Nat]
forall a. Maybe a
Nothing
    Just Nat
i -> IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r ((IntMap Nat -> Nat -> IntMap Nat)
-> IntMap Nat -> [Nat] -> IntMap Nat
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Nat -> IntMap Nat -> IntMap Nat)
-> IntMap Nat -> Nat -> IntMap Nat
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Nat -> IntMap Nat -> IntMap Nat)
 -> IntMap Nat -> Nat -> IntMap Nat)
-> (Nat -> IntMap Nat -> IntMap Nat)
-> IntMap Nat
-> Nat
-> IntMap Nat
forall a b. (a -> b) -> a -> b
$ (Nat -> Nat) -> Nat -> IntMap Nat -> IntMap Nat
forall a. (a -> a) -> Nat -> IntMap a -> IntMap a
IntMap.adjust (Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
subtract Nat
1))
                       (Nat -> Nat -> IntMap Nat -> IntMap Nat
forall a. Nat -> a -> IntMap a -> IntMap a
IntMap.insert Nat
i (-Nat
1) IntMap Nat
m)
                       ([[Nat]]
frees [[Nat]] -> Nat -> [Nat]
forall a. HasCallStack => [a] -> Nat -> a
!! Nat
i))
                 (Nat
i Nat -> [Nat] -> [Nat]
forall a. a -> [a] -> [a]
: [Nat]
perm) (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
 in IntMap Nat -> [Nat] -> Nat -> Maybe [Nat]
r IntMap Nat
m [] ([MExp o] -> Nat
forall a. [a] -> Nat
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 = Set Nat -> [Nat]
forall a. Set a -> [a]
Set.toList (Set Nat -> [Nat]) -> (t -> Set Nat) -> t -> [Nat]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Set Nat
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 = (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, (Nat -> Nat) -> MExp o -> MExp o
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 = (Nat -> HI (MId, MExp o)) -> [Nat] -> CSCtx o
forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> CSCtx o
ctx1 CSCtx o -> Nat -> HI (MId, MExp o)
forall a. HasCallStack => [a] -> Nat -> a
!! Nat
i) [Nat]
perm
     ctx3 :: CSCtx o
ctx3 = CSCtx o -> CSCtx o
forall o. CSCtx o -> CSCtx o
seqctx CSCtx o
ctx2
     tt' :: MExp o
tt' = (Nat -> Nat) -> MExp o -> MExp o
forall t. Renaming t => (Nat -> Nat) -> t -> t
rename ([Nat] -> Nat -> Nat
ren [Nat]
perm) MExp o
tt
     pats' :: [CSPat o]
pats' = (CSPat o -> CSPat o) -> [CSPat o] -> [CSPat o]
forall a b. (a -> b) -> [a] -> [b]
map ((Nat -> Nat) -> CSPat o -> CSPat o
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 = Nat -> [Nat] -> Maybe Nat
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) = 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
$ Nat -> (Nat -> Nat) -> t -> t
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 -> 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 (Nat -> (Nat -> Nat) -> CSPat o -> CSPat o
forall t. Renaming t => Nat -> (Nat -> Nat) -> t -> t
renameOffset Nat
j Nat -> Nat
ren) [CSPat o]
pats
    CSPatVar Nat
i         -> Nat -> CSPatI o
forall o. Nat -> CSPatI o
CSPatVar (Nat -> CSPatI o) -> Nat -> CSPatI o
forall a b. (a -> b) -> a -> b
$ Nat
j Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat -> Nat
ren Nat
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
$ Nat -> (Nat -> Nat) -> MExp o -> MExp o
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
_                  -> CSPatI o
forall a. HasCallStack => a
__IMPOSSIBLE__

seqctx :: CSCtx o -> CSCtx o
seqctx :: forall o. CSCtx o -> CSCtx o
seqctx = Nat -> [HI (MId, MExp o)] -> [HI (MId, MExp o)]
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) = Hiding -> (a, b) -> HI (a, b)
forall a. Hiding -> a -> HI a
HI Hiding
hid (a
id, Nat -> b -> b
forall t. Lift t => Nat -> t -> t
lift Nat
n b
t) HI (a, b) -> [HI (a, b)] -> [HI (a, b)]
forall a. a -> [a] -> [a]
: Nat -> [HI (a, b)] -> [HI (a, b)]
r (Nat
n Nat -> Nat -> Nat
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] = (CSPatI o -> [Nat]) -> [CSPatI o] -> [Nat]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Nat -> CSPatI o -> [Nat]
f Nat
0) ([CSPat o] -> [CSPatI o]
forall a. [HI a] -> [a]
drophid [CSPat o]
pats)
     f :: Nat -> CSPatI o -> [Nat]
f Nat
d (CSPatConApp ConstRef o
_ [CSPat o]
pats) = (CSPatI o -> [Nat]) -> [CSPatI o] -> [Nat]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Nat -> CSPatI o -> [Nat]
f (Nat
d Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)) ([CSPat o] -> [CSPatI o]
forall a. [HI a] -> [a]
drophid [CSPat o]
pats)
     f Nat
d (CSPatVar Nat
v') = [Nat
d | Nat
v Nat -> Nat -> Bool
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) = a -> (Sum Nat, [Nat])
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, []) (Sum Nat, [Nat]) -> (Sum Nat, [Nat]) -> (Sum Nat, [Nat])
forall a. Semigroup a => a -> a -> a
<> [CSPat o] -> (Sum Nat, [Nat])
forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars [CSPat o]
ps
    CSPatVar Nat
n       -> (Sum Nat
0, [Nat
n])
    CSPatExp MExp o
e       -> MExp o -> (Sum Nat, [Nat])
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 = (a -> (Sum Nat, [Nat])) -> [a] -> (Sum Nat, [Nat])
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> (Sum Nat, [Nat])
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, []) (Sum Nat, [Nat]) -> (Sum Nat, [Nat]) -> (Sum Nat, [Nat])
forall a. Semigroup a => a -> a -> a
<> MArgList o -> (Sum Nat, [Nat])
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) = a -> (Sum Nat, [Nat])
forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars a
a (Sum Nat, [Nat]) -> (Sum Nat, [Nat]) -> (Sum Nat, [Nat])
forall a. Semigroup a => a -> a -> a
<> b -> (Sum Nat, [Nat])
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 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 Nat
0, [])
    ALCons Hiding
_ MExp o
a MArgList o
as -> (MExp o, MArgList o) -> (Sum Nat, [Nat])
forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars (MExp o
a, MArgList o
as)
    ALProj{}      -> (Sum Nat, [Nat])
forall a. HasCallStack => a
__IMPOSSIBLE__
    ALConPar MArgList o
as   -> MArgList o -> (Sum Nat, [Nat])
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, Sum Nat -> Nat
forall a. Sum a -> a
getSum Sum Nat
s, [Nat]
vs) where

  ([Nat]
is , Sum Nat
s , [Nat]
vs) = Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
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) = CSPat o -> (Sum Nat, [Nat])
forall a. LocalTerminationEnv a => a -> (Sum Nat, [Nat])
sizeAndBoundVars CSPat o
hp
                     in ([Nat
i], Sum Nat
size, [Nat]
vars) ([Nat], Sum Nat, [Nat])
-> ([Nat], Sum Nat, [Nat]) -> ([Nat], Sum Nat, [Nat])
forall a. Semigroup a => a -> a -> a
<> Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [CSPat o]
ps
    CSPatI o
_ -> Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
forall o. Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g (Nat
i Nat -> Nat -> Nat
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 = BlkInfo (RefInfo o)
-> MExp o
-> (Exp o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, Maybe (RefInfo o)
forall a. Maybe a
Nothing) MExp o
e ((Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o)))
-> (Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo 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) -> 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
       (MArgList o -> MetaEnv (PB (RefInfo 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 Nat
size Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0 then Prop (RefInfo o) -> MetaEnv (PB (RefInfo 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 Nat -> Nat -> [Nat] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall Nat
0 Nat
size [Nat]
vars MArgList o
args
          Elr o
_ -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo 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 -> MetaEnv (PB (RefInfo o))
ok MExp o
e
      Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ MExp o
ot) -> 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
       (MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
it)
       (MExp o -> MetaEnv (PB (RefInfo o))
ok MExp o
ot)
      Sort{} -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK

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


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

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


      ALConPar MArgList o
as -> MetaEnv (PB (RefInfo o))
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 = MM (Exp o) (RefInfo o)
-> (Exp o -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> MetaEnv (MB (Maybe (t, [Nat])) (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 (t, [Nat])) (RefInfo o)))
 -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> (Exp o -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> MetaEnv (MB (Maybe (t, [Nat])) (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 Nat
v) MArgList o
_ ->
       case Nat -> [Nat] -> Maybe [Nat]
forall {t}. Eq t => t -> [t] -> Maybe [t]
remove Nat
v [Nat]
vars of
        Maybe [Nat]
Nothing -> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (t, [Nat])
forall a. Maybe a
Nothing
        Just [Nat]
vars' -> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ (t, [Nat]) -> Maybe (t, [Nat])
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 <- 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 t
size t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
1 then
          Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (t, [Nat])
forall a. Maybe a
Nothing
         else
          t
-> [Nat]
-> MArgList o
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
hes (t
size t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [Nat]
vars MArgList o
args
        DeclCont o
_ -> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (t, [Nat])
forall a. Maybe a
Nothing
      Exp o
_ -> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (t, [Nat])
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 = MArgList o
-> (ArgList o -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> MetaEnv (MB (Maybe (t, [Nat])) (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 (t, [Nat])) (RefInfo o)))
 -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> (ArgList o -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
      ArgList o
ALNil -> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ (t, [Nat]) -> Maybe (t, [Nat])
forall a. a -> Maybe a
Just (t
size, [Nat]
vars)
      ALCons Hiding
_ MM (Exp o) (RefInfo o)
a MArgList o
as ->
       MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
-> (Maybe (t, [Nat])
    -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
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) ((Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
 -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> (Maybe (t, [Nat])
    -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o)))
-> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \Maybe (t, [Nat])
x -> case Maybe (t, [Nat])
x of
        Maybe (t, [Nat])
Nothing -> Maybe (t, [Nat]) -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (t, [Nat])
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{} -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__


      ALConPar MArgList o
as -> MetaEnv (MB (Maybe (t, [Nat])) (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__

     remove :: t -> [t] -> Maybe [t]
remove t
_ [] = Maybe [t]
forall a. Maybe a
Nothing
     remove t
x (t
y : [t]
ys) | t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y = [t] -> Maybe [t]
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 -> Maybe [t]
forall a. Maybe a
Nothing; Just [t]
ys' -> [t] -> Maybe [t]
forall a. a -> Maybe a
Just (t
y t -> [t] -> [t]
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) <- 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 Nat
forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f HNNBlks o
blks of
  Just Nat
v -> [Nat] -> IO [Nat]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Nat
v]
  Maybe Nat
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{} -> [Nat] -> ICArgList o -> IO [Nat]
forall {o}. [Nat] -> ICArgList o -> IO [Nat]
g [] ICArgList o
args
     DeclCont o
_ -> [Nat] -> IO [Nat]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
   HNExp' o
_ -> [Nat] -> IO [Nat]
forall a. a -> IO a
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 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 Nat
v) ICArgList o
_ -> Nat -> Maybe Nat
forall a. a -> Maybe a
Just Nat
v
              HNExp' o
_ -> Maybe Nat
forall a. Maybe a
Nothing
             [WithSeenUIds (HNExp' o) o]
_ -> Maybe Nat
forall a. Maybe a
Nothing
  g :: [Nat] -> ICArgList o -> IO [Nat]
g [Nat]
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' :: [Nat]
vs' = case HNNBlks o -> Maybe Nat
forall {o} {o}. [WithSeenUIds (HNExp' o) o] -> Maybe Nat
f HNNBlks o
blks of
                Just Nat
v | Nat
v Nat -> [Nat] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Nat]
vs -> Nat
v Nat -> [Nat] -> [Nat]
forall a. a -> [a] -> [a]
: [Nat]
vs
                Maybe Nat
_ -> [Nat]
vs
     [Nat] -> ICArgList o -> IO [Nat]
g [Nat]
vs' ICArgList o
as
    HNArgList o
_ -> [Nat] -> IO [Nat]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Nat]
vs
-- ---------------------------