module Agda.Auto.CaseSplit where

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

import Data.Function
import Data.IORef
import Data.Tuple (swap)
import Data.List (elemIndex)
-- Import of <> needed for 8.2.2, but redundant in 8.8.3
import Data.Monoid ((<>), Sum(..))
import qualified Data.Set    as Set
import qualified Data.IntMap as IntMap

import Agda.Syntax.Common (Hiding(..))
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax

import Agda.Auto.SearchControl
import Agda.Auto.Typecheck

import Agda.Utils.Impossible
import Agda.Utils.Monad (or2M)
import Agda.Utils.List (last1)

abspatvarname :: String
abspatvarname :: String
abspatvarname = String
"\0absurdPattern"

costCaseSplitVeryHigh, costCaseSplitHigh, costCaseSplitLow, costAddVarDepth
  :: Cost
costCaseSplitVeryHigh :: Cost
costCaseSplitVeryHigh = Cost
10000
costCaseSplitHigh :: Cost
costCaseSplitHigh     = Cost
5000
costCaseSplitLow :: Cost
costCaseSplitLow      = Cost
2000
costAddVarDepth :: Cost
costAddVarDepth       = Cost
1000

data HI a = HI Hiding a

drophid :: [HI a] -> [a]
drophid :: 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]
              | 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 (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 (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 (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 (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 (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 (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 (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 (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. [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 (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 (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 (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 (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 (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. [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 (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 (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 (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 (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 (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 (t :: * -> *) a. Foldable t => t a -> Bool
null [Nat]
mblkvar                               = Cost
costCaseSplitVeryHigh
                   | Nat
scrut Nat -> [Nat] -> 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 (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. [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 (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 (m :: * -> *) a. Monad m => a -> m a
return []
              [Sol o]
_ -> do
               [Sol o]
sols2 <- [ConstRef o] -> IO [Sol o]
dobranches [ConstRef o]
cons
               [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Sol o] -> IO [Sol o]) -> [Sol o] -> IO [Sol o]
forall a b. (a -> b) -> a -> b
$ (Sol o -> [Sol o]) -> [Sol o] -> [Sol o]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Sol o
sol -> (Sol o -> Sol o) -> [Sol o] -> [Sol o]
forall a b. (a -> b) -> [a] -> [b]
map (\Sol o
sol2 -> Sol o
sol Sol o -> Sol o -> Sol o
forall a. [a] -> [a] -> [a]
++ Sol o
sol2) [Sol o]
sols2) [Sol o]
sols
       DeclCont o
_ -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"
     Exp o
_ -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"

infertypevar :: CSCtx o -> Nat -> MExp o
infertypevar :: 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. [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 (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 (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 (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 (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 (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 (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 (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 (Assignments (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 (Assignments (UnifiesTo t)) IO) Bool
-> (Nat, Nat) -> StateT (Assignments (UnifiesTo t)) IO Bool
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (Nat
fstnew, Nat
nbnew)
                                              StateT (Assignments (UnifiesTo t)) IO Bool
-> Assignments (UnifiesTo t) -> IO Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` []

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

  unify' :: MM t (RefInfo o)
-> MM t (RefInfo o)
-> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()
unify' = t -> t -> StateT [(Nat, Exp o)] 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
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 (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 (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 (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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          (DeclCont o, DeclCont o)
_ -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
{- GA: Why don't we have a case for distinct heads after all these
       unification cases for vars with no spines & metas that can
       be looked up?
      (App _ _ elr1 _, App _ _ elr2 _) | elr1 <> elr2 -> return True
-}
      (Exp o, Exp o)
_ -> Bool -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

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

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

  notequal' :: ArgList o
-> ArgList o
-> ReaderT
     (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 (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 (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 (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 (t :: * -> *) a. Foldable t => t a -> Nat
length (([Nat] -> Bool) -> [[Nat]] -> [[Nat]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Nat -> [Nat] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Nat
i) [[Nat]]
frees)))
          [Nat
0..[MExp o] -> 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 (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. [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 (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. [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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return []
   HNExp' o
_ -> [Nat] -> IO [Nat]
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 (m :: * -> *) a. Monad m => a -> m a
return [Nat]
vs
-- ---------------------------