{-# LANGUAGE UndecidableInstances #-}

module Agda.Auto.CaseSplit where

import Data.IORef
import Data.Tuple (swap)
import Data.List (findIndex)
import Data.Monoid ((<>), Sum(..))
import Data.Foldable (foldMap)
import qualified Data.Set    as Set
import qualified Data.IntMap as IntMap
import Control.Monad.State as St hiding (lift)
import Control.Monad.Reader as Rd hiding (lift)
import qualified Control.Monad.State as St
import Data.Function

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

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

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

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

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

data HI a = HI Hiding a

drophid :: [HI a] -> [a]
drophid :: [HI a] -> [a]
drophid = (HI a -> a) -> [HI a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (\(HI _ x :: a
x) -> a
x)

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

data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]
              | CSPatVar Nat
              | CSPatExp (MExp o)
              | CSWith (MExp o) -- always an App
              | CSAbsurd

              | CSOmittedArg
type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]

caseSplitSearch ::
  forall o . IORef Int -> Int -> [ConstRef o] ->
  Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o ->
  CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch :: IORef Int
-> Int
-> [ConstRef o]
-> Maybe (EqReasoningConsts o)
-> Int
-> Cost
-> ConstRef o
-> CSCtx o
-> MExp o
-> [CSPat o]
-> IO [Sol o]
caseSplitSearch ticks :: IORef Int
ticks nsolwanted :: Int
nsolwanted chints :: [ConstRef o]
chints meqr :: Maybe (EqReasoningConsts o)
meqr depthinterval :: Int
depthinterval depth :: Cost
depth recdef :: ConstRef o
recdef ctx :: CSCtx o
ctx tt :: MExp o
tt pats :: [CSPat o]
pats = do
 let branchsearch :: Cost -> CSCtx o -> MExp o ->
                     ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
     branchsearch :: Cost
-> CSCtx o -> MExp o -> ([Int], Int, [Int]) -> IO (Maybe (MExp o))
branchsearch depth :: Cost
depth ctx :: CSCtx o
ctx tt :: MExp o
tt termcheckenv :: ([Int], Int, [Int])
termcheckenv = do

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

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

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

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


             [Sol o]
sols <- Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc (Cost
depth Cost -> Cost -> Cost
forall a. Num a => a -> a -> a
- Cost
cost) (CSCtx o -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length CSCtx o
ctx Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
scrut) CSCtx o
ctx2 MExp o
tt2 [CSPat o]
pats2
             case [Sol o]
sols of
              [] -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return []
              _ -> 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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Sol o -> [Sol o]) -> [Sol o] -> [[Sol o]]
forall a b. (a -> b) -> [a] -> [b]
map (\sol :: Sol o
sol -> (Sol o -> Sol o) -> [Sol o] -> [Sol o]
forall a b. (a -> b) -> [a] -> [b]
map (\sol2 :: 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)
       _ -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"
     _ -> [Sol o] -> IO [Sol o]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- split failed "scrut type is not datatype"

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

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

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

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

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

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

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


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

concatargs :: MArgList o -> MArgList o -> MArgList o
concatargs :: MArgList o -> MArgList o -> MArgList o
concatargs xs :: MArgList o
xs ys :: 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
  ALNil -> MArgList o
ys

  ALCons hid :: Hiding
hid x :: MExp o
x xs :: 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 as :: MArgList o
as -> ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM (ArgList o -> MArgList o) -> ArgList o -> MArgList o
forall a b. (a -> b) -> a -> b
$ MArgList o -> ArgList o
forall o. MArgList o -> ArgList o
ALConPar (MArgList o -> MArgList o -> MArgList o
forall o. MArgList o -> MArgList o -> MArgList o
concatargs MArgList o
xs MArgList o
ys)

replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep :: Int -> Int -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep sv :: Int
sv nnew :: Int
nnew rp :: CSPatI o
rp re :: MExp o
re = CSPat o -> CSPat o
r
 where
  r :: CSPat o -> CSPat o
  r :: CSPat o -> CSPat o
r (HI hid :: Hiding
hid (CSPatConApp c :: ConstRef o
c ps :: [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 hid :: Hiding
hid (CSPatVar v :: Int
v)) = if Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sv then
                    Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid CSPatI o
rp
                   else
                    if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
sv then
                     Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid (Int -> CSPatI o
forall o. Int -> CSPatI o
CSPatVar (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nnew Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1))
                    else
                     Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid (Int -> CSPatI o
forall o. Int -> CSPatI o
CSPatVar Int
v)
  r (HI hid :: Hiding
hid (CSPatExp e :: MExp o
e)) = Hiding -> CSPatI o -> CSPat o
forall a. Hiding -> a -> HI a
HI Hiding
hid (MExp o -> CSPatI o
forall o. MExp o -> CSPatI o
CSPatExp (MExp o -> CSPatI o) -> MExp o -> CSPatI o
forall a b. (a -> b) -> a -> b
$ Int -> Int -> MExp o -> MExp o -> MExp o
forall o t u. Replace o t u => Int -> Int -> MExp o -> t -> u
replace Int
sv Int
nnew MExp o
re MExp o
e)

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

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



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

type Assignments o = [(Nat, Exp o)]

class Unify o t | t -> o where
  unify'    :: t -> t -> StateT (Assignments o) Maybe ()
  notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool

unify :: Unify o t => t -> t -> Maybe (Assignments o)
unify :: t -> t -> Maybe (Assignments o)
unify t :: t
t u :: t
u = t -> t -> StateT (Assignments o) Maybe ()
forall o t. Unify o t => t -> t -> StateT (Assignments o) Maybe ()
unify' t
t t
u StateT (Assignments o) Maybe ()
-> Assignments o -> Maybe (Assignments o)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
`execStateT` []

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

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

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

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

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

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

instance Unify o (Exp o) where
  unify' :: Exp o -> Exp o -> StateT (Assignments o) Maybe ()
unify' e1 :: Exp o
e1 e2 :: Exp o
e2 = case (Exp o
e1, Exp o
e2) of
   (App _ _ elr1 :: Elr o
elr1 args1 :: MArgList o
args1, App _ _ elr2 :: Elr o
elr2 args2 :: 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 o) Maybe ()
forall o t. Unify o t => t -> t -> StateT (Assignments o) Maybe ()
unify' MArgList o
args1 MArgList o
args2
   (Lam hid1 :: Hiding
hid1 b1 :: Abs (MExp o)
b1, Lam hid2 :: Hiding
hid2 b2 :: 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 o) Maybe ()
forall o t. Unify o t => t -> t -> StateT (Assignments o) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
   (Pi _ hid1 :: Hiding
hid1 _ a1 :: MExp o
a1 b1 :: Abs (MExp o)
b1, Pi _ hid2 :: Hiding
hid2 _ a2 :: MExp o
a2 b2 :: Abs (MExp o)
b2)   | Hiding
hid1 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> MExp o -> MExp o -> StateT (Assignments o) Maybe ()
forall o t. Unify o t => t -> t -> StateT (Assignments o) 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 o) Maybe ()
forall o t. Unify o t => t -> t -> StateT (Assignments o) Maybe ()
unify' Abs (MExp o)
b1 Abs (MExp o)
b2
   (Sort _, Sort _) -> () -> StateT (Assignments o) Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- a bit sloppy
   (App _ _ (Var v :: Int
v) (NotM ALNil), _)
     | Int
v Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` (Exp o -> Set Int
forall t. FreeVars t => t -> Set Int
freeVars Exp o
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
   (_, App _ _ (Var v :: Int
v) (NotM ALNil))
     | Int
v Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` (Exp o -> Set Int
forall t. FreeVars t => t -> Set Int
freeVars Exp o
e1) -> Maybe () -> StateT (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 _ _ (Var v :: Int
v) (NotM ALNil), _) -> Int -> Exp o -> StateT (Assignments o) Maybe ()
forall o. Int -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Int
v Exp o
e2
   (_, App _ _ (Var v :: Int
v) (NotM ALNil)) -> Int -> Exp o -> StateT (Assignments o) Maybe ()
forall o. Int -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar Int
v 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

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

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

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

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

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

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

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

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

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

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


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

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


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

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

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

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

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

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

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

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

instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where
  sizeAndBoundVars :: HI a -> (Sum Int, [Int])
sizeAndBoundVars (HI _ p :: a
p) = a -> (Sum Int, [Int])
forall a. LocalTerminationEnv a => a -> (Sum Int, [Int])
sizeAndBoundVars a
p

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

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

instance LocalTerminationEnv (MExp o) where
--  sizeAndBoundVars e = case rm __IMPOSSIBLE__ e of
-- GA: 2017 06 27: Not actually impossible! (cf. #2620)
  sizeAndBoundVars :: MExp o -> (Sum Int, [Int])
sizeAndBoundVars Meta{} = (0, [])
-- Does this default behaviour even make sense? The catchall in the
-- following match seems to suggest it does
  sizeAndBoundVars (NotM e :: Exp o
e) = case Exp o
e of
    App _ _ (Var v :: Int
v) _      -> (0, [Int
v])
    App _ _ (Const _) args :: MArgList o
args -> (1, []) (Sum Int, [Int]) -> (Sum Int, [Int]) -> (Sum Int, [Int])
forall a. Semigroup a => a -> a -> a
<> MArgList o -> (Sum Int, [Int])
forall a. LocalTerminationEnv a => a -> (Sum Int, [Int])
sizeAndBoundVars MArgList o
args
    _                      -> (0, [])

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

instance LocalTerminationEnv (MArgList o) where
  sizeAndBoundVars :: MArgList o -> (Sum Int, [Int])
sizeAndBoundVars as :: 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
    ALNil         -> (0, [])
    ALCons _ a :: MExp o
a as :: MArgList o
as -> (MExp o, MArgList o) -> (Sum Int, [Int])
forall a. LocalTerminationEnv a => a -> (Sum Int, [Int])
sizeAndBoundVars (MExp o
a, MArgList o
as)
    ALProj{}      -> (Sum Int, [Int])
forall a. HasCallStack => a
__IMPOSSIBLE__
    ALConPar as :: MArgList o
as   -> MArgList o -> (Sum Int, [Int])
forall a. LocalTerminationEnv a => a -> (Sum Int, [Int])
sizeAndBoundVars MArgList o
as


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

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

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

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

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


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

      ALProj eas :: MArgList o
eas _ _ as :: MArgList o
as -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (MArgList o -> EE (MyPB o)
oks MArgList o
eas) (MArgList o -> EE (MyPB o)
oks MArgList o
as)


      ALConPar as :: MArgList o
as -> MArgList o -> EE (MyPB o)
oks MArgList o
as

     okcall :: Int -> t -> [Int] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall i :: Int
i size :: t
size vars :: [Int]
vars as :: 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
$ \as :: ArgList o
as -> case ArgList o
as of
      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 _ a :: MExp o
a as :: MArgList o
as | Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is ->
       Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (Maybe (t, [Int])) (RefInfo o))
-> (Maybe (t, [Int]) -> 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 (t -> [Int] -> MExp o -> MetaEnv (MB (Maybe (t, [Int])) (RefInfo o))
forall a o.
(Eq a, Num a) =>
a
-> [Int]
-> MM (Exp o) (RefInfo o)
-> MetaEnv (MB (Maybe (a, [Int])) (RefInfo o))
he t
size [Int]
vars MExp o
a) ((Maybe (t, [Int]) -> MetaEnv (PB (RefInfo o)))
 -> MetaEnv (PB (RefInfo o)))
-> (Maybe (t, [Int]) -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \x :: Maybe (t, [Int])
x -> case Maybe (t, [Int])
x of
        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 "localTerminationSidecond: reccall not ok"
        Just (size' :: t
size', vars' :: [Int]
vars') -> Int -> t -> [Int] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) t
size' [Int]
vars' MArgList o
as
      ALCons _ a :: MExp o
a as :: MArgList o
as -> Int -> t -> [Int] -> MArgList o -> MetaEnv (PB (RefInfo o))
okcall (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) t
size [Int]
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 as :: MArgList o
as -> MetaEnv (PB (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__

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

      ALProj{} -> MetaEnv (MB (Maybe (a, [Int])) (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__


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

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

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


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