module Agda.Auto.Typecheck where

import Data.IORef
import Control.Monad (liftM)

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

import Agda.Utils.Impossible

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

-- | Typechecker drives the solution of metas.
tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp isdep :: Bool
isdep ctx :: Ctx o
ctx typ :: CExp o
typ@(TrBr typtrs :: [MExp o]
typtrs ityp :: ICExp o
ityp@(Clos _ itypexp :: MExp o
itypexp)) trm :: MExp o
trm =
  Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o, Bool) (RefInfo o))
-> ((HNExp o, Bool) -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioTypeUnknown Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICExp o -> MetaEnv (MB (HNExp o, Bool) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o, Bool) o)
hnn_checkstep ICExp o
ityp) (((HNExp o, Bool) -> EE (MyPB o)) -> EE (MyPB o))
-> ((HNExp o, Bool) -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \(hntyp :: HNExp o
hntyp, iotastepdone :: Bool
iotastepdone) ->
  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
True, Bool -> Prio
prioTypecheck Bool
isdep, RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just (Nat -> HNExp o -> Bool -> RefInfo o
forall o. Nat -> HNExp o -> Bool -> RefInfo o
RIMainInfo (Ctx o -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Ctx o
ctx) HNExp o
hntyp Bool
iotastepdone)) MExp o
trm ((Exp o -> EE (MyPB o)) -> EE (MyPB o))
-> (Exp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \trm :: Exp o
trm -> case Exp o
trm of
   App _ okh :: OKHandle (RefInfo o)
okh elr :: Elr o
elr args :: MArgList o
args -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNPi{} | Bool
isdep -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, dep terms should be eta-long"
    _ -> do
     (ityp :: CExp o
ityp, sc :: EE (MyPB o) -> EE (MyPB o)
sc) <- case Elr o
elr of
              Var v :: Nat
v -> -- assuming within scope
               (CExp o, EE (MyPB o) -> EE (MyPB o))
-> IO (CExp o, EE (MyPB o) -> EE (MyPB o))
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat -> CExp o -> CExp o
forall t. Weakening t => Nat -> t -> t
weak (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ 1) ((MId, CExp o) -> CExp o
forall a b. (a, b) -> b
snd ((MId, CExp o) -> CExp o) -> (MId, CExp o) -> CExp o
forall a b. (a -> b) -> a -> b
$ Ctx o
ctx Ctx o -> Nat -> (MId, CExp o)
forall a. [a] -> Nat -> a
!! Nat
v), EE (MyPB o) -> EE (MyPB o)
forall a. a -> a
id)
              Const c :: ConstRef o
c -> do
               ConstDef o
cdef <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
               (CExp o, EE (MyPB o) -> EE (MyPB o))
-> IO (CExp o, EE (MyPB o) -> EE (MyPB o))
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp o -> CExp o
forall o. MExp o -> CExp o
closify (ConstDef o -> MExp o
forall o. ConstDef o -> MExp o
cdtype ConstDef o
cdef), \x :: EE (MyPB o)
x -> 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
$ Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just [MArgList o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term MArgList o
args]) (ConstRef o -> MArgList o -> EE (MyPB o)
forall o. ConstRef o -> MArgList o -> EE (MyPB o)
noiotastep_term ConstRef o
c MArgList o
args) EE (MyPB o)
x)

     Nat
ndfv <- case Elr o
elr of
              Var{} -> Nat -> IO Nat
forall (m :: * -> *) a. Monad m => a -> m a
return 0
              Const c :: ConstRef o
c -> ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c IO (ConstDef o) -> (ConstDef o -> IO Nat) -> IO Nat
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \cd :: ConstDef o
cd -> Nat -> IO Nat
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstDef o -> Nat
forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
cd)


     Bool
isconstructor <- case Elr o
elr of
      Var{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Const c :: ConstRef o
c -> do
       ConstDef o
cdef <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
       Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cdef of {Constructor{} -> Bool
True; _ -> Bool
False}

     EE (MyPB o) -> EE (MyPB o)
sc (EE (MyPB o) -> EE (MyPB o)) -> EE (MyPB o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
forall o.
Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
tcargs Nat
ndfv Bool
isdep Ctx o
ctx CExp o
ityp MArgList o
args (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) Elr o
elr (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) Bool
isconstructor ((CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \ityp :: CExp o
ityp _ -> 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
$ OKHandle (RefInfo o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk. OKHandle blk -> MetaEnv (PB blk) -> Prop blk
ConnectHandle OKHandle (RefInfo o)
okh (Bool -> CExp o -> CExp o -> EE (MyPB o)
forall o. Bool -> CExp o -> CExp o -> EE (MyPB o)
comp' Bool
True CExp o
typ CExp o
ityp)
   Lam hid :: Hiding
hid (Abs id1 :: MId
id1 b :: MExp o
b) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNPi hid2 :: Hiding
hid2 _ it :: ICExp o
it (Abs id2 :: MId
id2 ot :: ICExp o
ot) | Hiding
hid Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 ->
     Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp Bool
isdep ((MId -> MId -> MId
pickid MId
id1 MId
id2, ICExp o -> CExp o
forall a. a -> TrBr a o
t ICExp o
it) (MId, CExp o) -> Ctx o -> Ctx o
forall a. a -> [a] -> [a]
: Ctx o
ctx) (ICExp o -> CExp o
forall a. a -> TrBr a o
t ICExp o
ot) MExp o
b
    _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, type of lam should be fun or pi (and same hid)"
   Pi _ _ _ it :: MExp o
it (Abs id :: MId
id ot :: MExp o
ot) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNSort s :: Sort
s ->
     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
$ Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just [Ctx o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term Ctx o
ctx, MExp o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term MExp o
it])
      (Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp Bool
True Ctx o
ctx (MExp o -> CExp o
forall o. MExp o -> CExp o
closify (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
$ Sort -> Exp o
forall o. Sort -> Exp o
Sort Sort
s)) MExp o
it)
      (Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp Bool
isdep ((MId
id, MExp o -> CExp o
forall o. MExp o -> CExp o
closify MExp o
it) (MId, CExp o) -> Ctx o -> Ctx o
forall a. a -> [a] -> [a]
: Ctx o
ctx) (MExp o -> CExp o
forall o. MExp o -> CExp o
closify (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
$ Sort -> Exp o
forall o. Sort -> Exp o
Sort Sort
s)) 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
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, type of pi should be set"
   Sort (Set i :: Nat
i) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNSort s2 :: Sort
s2 -> case Sort
s2 of
     Set j :: Nat
j -> 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
$ if Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
j then Prop (RefInfo o)
forall blk. Prop blk
OK else String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, type of set should be larger set"

     UnknownSort -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK -- mpret $ Error "tcExp, type of set i unknown sort" -- OK instead? (prev __IMPOSSIBLE__)

     Type -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
    _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, type of set should be set"

   Sort UnknownSort -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__

   Sort Type -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__

   AbsurdLambda hid :: Hiding
hid -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNPi hid2 :: Hiding
hid2 _ it :: ICExp o
it _ | Hiding
hid Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 ->
     Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (Maybe (ICArgList o, [ConstRef o])) (RefInfo o))
-> (Maybe (ICArgList o, [ConstRef o]) -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICExp o
-> MetaEnv (MB (Maybe (ICArgList o, [ConstRef o])) (RefInfo o))
forall o.
ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
getDatatype ICExp o
it) ((Maybe (ICArgList o, [ConstRef o]) -> EE (MyPB o)) -> EE (MyPB o))
-> (Maybe (ICArgList o, [ConstRef o]) -> EE (MyPB o))
-> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: Maybe (ICArgList o, [ConstRef o])
res -> case Maybe (ICArgList o, [ConstRef o])
res of
      Just (indeces :: ICArgList o
indeces, cons :: [ConstRef o]
cons) ->
       (EE (MyPB o) -> ConstRef o -> EE (MyPB o))
-> EE (MyPB o) -> [ConstRef o] -> EE (MyPB o)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\p :: EE (MyPB o)
p con :: ConstRef o
con -> 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
$ Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And Maybe [Term (RefInfo o)]
forall a. Maybe a
Nothing EE (MyPB o)
p (
        ICArgList o -> ConstRef o -> EE (MyPB o)
forall o. ICArgList o -> ConstRef o -> EE (MyPB o)
constructorImpossible ICArgList o
indeces ConstRef o
con
       )) (Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK) [ConstRef o]
cons
      Nothing -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, absurd lambda, datatype needed"
    _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcExp, type of absurd lam should be fun or pi (and same hid)"


  where
   t :: a -> TrBr a o
t = [MExp o] -> a -> TrBr a o
forall a o. [MExp o] -> a -> TrBr a o
TrBr [MExp o]
typtrs


getDatatype :: ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
getDatatype :: ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
getDatatype t :: ICExp o
t =
 MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o))
-> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
t) ((HNExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o))
 -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o))
-> (HNExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o))
-> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
forall a b. (a -> b) -> a -> b
$ \hnt :: HNExp o
hnt -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnt 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 cons :: [ConstRef o]
cons _ -> Maybe (ICArgList o, [ConstRef o])
-> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Maybe (ICArgList o, [ConstRef o])
 -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o))
-> Maybe (ICArgList o, [ConstRef o])
-> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
forall a b. (a -> b) -> a -> b
$ (ICArgList o, [ConstRef o]) -> Maybe (ICArgList o, [ConstRef o])
forall a. a -> Maybe a
Just (ICArgList o
args, [ConstRef o]
cons) -- ?? check that lenth args corresponds to type of datatype
    _ -> Maybe (ICArgList o, [ConstRef o])
-> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (ICArgList o, [ConstRef o])
forall a. Maybe a
Nothing
  _ -> Maybe (ICArgList o, [ConstRef o])
-> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe (ICArgList o, [ConstRef o])
forall a. Maybe a
Nothing

constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)
constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)
constructorImpossible args :: ICArgList o
args c :: ConstRef o
c = do
 ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
 Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (Nat -> ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. Nat -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi (-1) ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [] (MExp o -> ICExp o) -> MExp o -> ICExp o
forall a b. (a -> b) -> a -> b
$ ConstDef o -> MExp o
forall o. ConstDef o -> MExp o
cdtype ConstDef o
cd)) ((HNExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnot :: HNExp o
hnot ->
  case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnot of
   HNApp _ args2 :: ICArgList o
args2 -> ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
forall o.
ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequals ICArgList o
args ICArgList o
args2 (\_ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "not unequal") []
   _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "constructorImpossible 1"

unequals :: ICArgList o -> ICArgList o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)
unequals :: ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequals es1 :: ICArgList o
es1 es2 :: ICArgList o
es2 cont :: [(Nat, HNExp o)] -> EE (MyPB o)
cont unifier2 :: [(Nat, HNExp o)]
unifier2 =
 Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
es1) ((HNArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnes1 :: HNArgList o
hnes1 ->
 Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
es2) ((HNArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnes2 :: HNArgList o
hnes2 ->
 case (HNArgList o
hnes1, HNArgList o
hnes2) of
  (HNALCons _ e1 :: ICExp o
e1 es1 :: ICArgList o
es1, HNALCons _ e2 :: ICExp o
e2 es2 :: ICArgList o
es2) -> ICExp o
-> ICExp o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
forall o.
ICExp o
-> ICExp o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequal ICExp o
e1 ICExp o
e2 (ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
forall o.
ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequals ICArgList o
es1 ICArgList o
es2 [(Nat, HNExp o)] -> EE (MyPB o)
cont) [(Nat, HNExp o)]
unifier2

  (HNALConPar es1 :: ICArgList o
es1, HNALConPar es2 :: ICArgList o
es2) -> ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
forall o.
ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequals ICArgList o
es1 ICArgList o
es2 [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2

  _ -> [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2

unequal :: ICExp o -> ICExp o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)
unequal :: ICExp o
-> ICExp o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequal e1 :: ICExp o
e1 e2 :: ICExp o
e2 cont :: [(Nat, HNExp o)] -> EE (MyPB o)
cont unifier2 :: [(Nat, HNExp o)]
unifier2 =
 Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
e1) ((HNExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hne1 :: HNExp o
hne1 ->
 Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
e2) ((HNExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hne2 :: HNExp o
hne2 ->
  case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne2 of
   HNApp (Var v2 :: Nat
v2) es2 :: ICArgList o
es2 | Nat
v2 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< 0 ->
    Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
es2) ((HNArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnes2 :: HNArgList o
hnes2 -> case HNArgList o
hnes2 of
     HNALNil ->
      case Nat -> [(Nat, HNExp o)] -> Maybe (HNExp o)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Nat
v2 [(Nat, HNExp o)]
unifier2 of
       Nothing -> [(Nat, HNExp o)] -> EE (MyPB o)
cont ((Nat
v2, HNExp o
hne1) (Nat, HNExp o) -> [(Nat, HNExp o)] -> [(Nat, HNExp o)]
forall a. a -> [a] -> [a]
: [(Nat, HNExp o)]
unifier2)
       Just hne2' :: HNExp o
hne2' -> HNExp o -> HNExp o -> EE (MyPB o)
forall o o.
WithSeenUIds (HNExp' o) o
-> WithSeenUIds (HNExp' o) o -> EE (MyPB o)
cc HNExp o
hne1 HNExp o
hne2'
     HNALCons{} -> [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2

     HNALConPar{} -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__

   _ -> HNExp o -> HNExp o -> EE (MyPB o)
forall o o.
WithSeenUIds (HNExp' o) o
-> WithSeenUIds (HNExp' o) o -> EE (MyPB o)
cc HNExp o
hne1 HNExp o
hne2
 where
  cc :: WithSeenUIds (HNExp' o) o
-> WithSeenUIds (HNExp' o) o -> EE (MyPB o)
cc hne1 :: WithSeenUIds (HNExp' o) o
hne1 hne2 :: WithSeenUIds (HNExp' o) o
hne2 = case (WithSeenUIds (HNExp' o) o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue WithSeenUIds (HNExp' o) o
hne1, WithSeenUIds (HNExp' o) o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue WithSeenUIds (HNExp' o) o
hne2) of
   (HNApp (Const c1 :: ConstRef o
c1) es1 :: ICArgList o
es1, HNApp (Const c2 :: ConstRef o
c2) es2 :: ICArgList o
es2) -> do
    ConstDef o
cd1 <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c1
    ConstDef o
cd2 <- 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
       ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
forall o.
ICArgList o
-> ICArgList o
-> ([(Nat, HNExp o)] -> EE (MyPB o))
-> [(Nat, HNExp o)]
-> EE (MyPB o)
unequals ICArgList o
es1 ICArgList o
es2 [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2
      else
       Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
     _ -> [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2
   _ -> [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2

traversePi :: Int -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi :: Nat -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi v :: Nat
v t :: ICExp o
t =
 EE (MyMB (HNExp o) o)
-> (HNExp o -> EE (MyMB (HNExp o) o)) -> EE (MyMB (HNExp o) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> EE (MyMB (HNExp o) o)
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
t) ((HNExp o -> EE (MyMB (HNExp o) o)) -> EE (MyMB (HNExp o) o))
-> (HNExp o -> EE (MyMB (HNExp o) o)) -> EE (MyMB (HNExp o) o)
forall a b. (a -> b) -> a -> b
$ \hnt :: HNExp o
hnt ->
 case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnt of
  HNPi _ _ _ (Abs _ ot :: ICExp o
ot) -> Nat -> ICExp o -> EE (MyMB (HNExp o) o)
forall o. Nat -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- 1) (ICExp o -> EE (MyMB (HNExp o) o))
-> ICExp o -> EE (MyMB (HNExp o) o)
forall a b. (a -> b) -> a -> b
$ MExp o -> ICExp o -> ICExp o
forall o. MExp o -> ICExp o -> ICExp o
subi (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (Nat -> Elr o
forall o. Nat -> Elr o
Var Nat
v) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) ICExp o
ot
  _ -> HNExp o -> EE (MyMB (HNExp o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret HNExp o
hnt

tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool ->
          (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)
tcargs :: Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
tcargs ndfv :: Nat
ndfv isdep :: Bool
isdep ctx :: Ctx o
ctx ityp :: CExp o
ityp@(TrBr ityptrs :: [MExp o]
ityptrs iityp :: ICExp o
iityp) args :: MArgList o
args elimtrm :: MExp o
elimtrm isconstructor :: Bool
isconstructor cont :: CExp o -> MExp o -> EE (MyPB o)
cont = 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
True, Prio
prioTypecheckArgList, (RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just (RefInfo o -> Maybe (RefInfo o)) -> RefInfo o -> Maybe (RefInfo o)
forall a b. (a -> b) -> a -> b
$ Bool -> RefInfo o
forall o. Bool -> RefInfo o
RICheckElim (Bool -> RefInfo o) -> Bool -> RefInfo o
forall a b. (a -> b) -> a -> b
$ Bool
isdep Bool -> Bool -> Bool
|| Bool
isconstructor)) MArgList o
args ((ArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (ArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \args' :: ArgList o
args' -> case ArgList o
args' of
 ALNil -> CExp o -> MExp o -> EE (MyPB o)
cont CExp o
ityp MExp o
elimtrm
 ALCons hid :: Hiding
hid a :: MExp o
a as :: MArgList o
as ->
  Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioInferredTypeUnknown (RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just RefInfo o
forall o. RefInfo o
RIInferredTypeUnknown) (ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
iityp) ((HNExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnityp :: HNExp o
hnityp -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnityp of
   HNPi hid2 :: Hiding
hid2 possdep :: Bool
possdep it :: ICExp o
it (Abs _ ot :: ICExp o
ot)
     | Nat
ndfv Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
|| MExp o -> Bool
forall o. MExp o -> Bool
copyarg MExp o
a Bool -> Bool -> Bool
|| Hiding
hid Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> 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
$
    Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just ((if Bool
possdep then [MExp o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term MExp o
a] else []) [Term (RefInfo o)] -> [Term (RefInfo o)] -> [Term (RefInfo o)]
forall a. [a] -> [a] -> [a]
++ [Ctx o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term Ctx o
ctx, [MExp o] -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term [MExp o]
ityptrs]))
        (if Nat
ndfv Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK else (Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp (Bool
isdep Bool -> Bool -> Bool
|| Bool
possdep) Ctx o
ctx (ICExp o -> CExp o
forall a. a -> TrBr a o
t ICExp o
it) MExp o
a))
        (Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
forall o.
Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
tcargs (Nat
ndfv Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- 1) Bool
isdep Ctx o
ctx (MExp o -> CExp o -> CExp o
forall o. MExp o -> CExp o -> CExp o
sub MExp o
a (ICExp o -> CExp o
forall a. a -> TrBr a o
t ICExp o
ot)) MArgList o
as (Hiding -> MExp o -> MExp o -> MExp o
forall o blk. Hiding -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk
addend Hiding
hid MExp o
a MExp o
elimtrm) Bool
isconstructor CExp o -> MExp o -> EE (MyPB o)
cont)
   _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "tcargs, inf type should be fun or pi (and same hid)"


 ALProj{} | Nat
ndfv Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__

 ALProj preas :: MArgList o
preas projidx :: MM (ConstRef o) (RefInfo o)
projidx hid :: Hiding
hid as :: MArgList o
as ->
  Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioInferredTypeUnknown (RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just RefInfo o
forall o. RefInfo o
RIInferredTypeUnknown) (ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
iityp) ((HNExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnityp :: HNExp o
hnityp -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnityp of
   HNApp (Const dd :: ConstRef o
dd) _ -> do
    ConstDef o
dddef <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
dd
    case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
dddef of
     Datatype _ projs :: [ConstRef o]
projs ->
      BlkInfo (RefInfo o)
-> MM (ConstRef o) (RefInfo o)
-> (ConstRef 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
True, Prio
prioProjIndex, RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just ([ConstRef o] -> RefInfo o
forall o. [ConstRef o] -> RefInfo o
RICheckProjIndex [ConstRef o]
projs)) MM (ConstRef o) (RefInfo o)
projidx ((ConstRef o -> EE (MyPB o)) -> EE (MyPB o))
-> (ConstRef o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$
      \projidx :: ConstRef o
projidx -> do
       ConstDef o
projd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
projidx
       Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
forall o.
Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
tcargs (ConstDef o -> Nat
forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
projd) Bool
isdep Ctx o
ctx (MExp o -> CExp o
forall o. MExp o -> CExp o
closify (MExp o -> CExp o) -> MExp o -> CExp o
forall a b. (a -> b) -> a -> b
$ ConstDef o -> MExp o
forall o. ConstDef o -> MExp o
cdtype ConstDef o
projd) MArgList o
preas (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
projidx) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) Bool
True ((CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$
        \ityp2 :: CExp o
ityp2@(TrBr ityp2trs :: [MExp o]
ityp2trs iityp2 :: ICExp o
iityp2) elimtrm2 :: MExp o
elimtrm2 ->
         case ICExp o
iityp2 of
          Clos _ (NotM (Pi _ _ _ (NotM (App _ _ (Const dd2 :: ConstRef o
dd2) _)) _)) | ConstRef o
dd2 ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== ConstRef o
dd ->
           Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioInferredTypeUnknown (RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just RefInfo o
forall o. RefInfo o
RIInferredTypeUnknown) (ICExp o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
iityp2) ((HNExp o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNExp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnityp2 :: HNExp o
hnityp2 -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnityp2 of
            HNPi hid2 :: Hiding
hid2 possdep :: Bool
possdep it :: ICExp o
it (Abs _ ot :: ICExp o
ot) | Hiding
hid Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> 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
$
             Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And Maybe [Term (RefInfo o)]
forall a. Maybe a
Nothing
                 (Bool -> CExp o -> CExp o -> EE (MyPB o)
forall o. Bool -> CExp o -> CExp o -> EE (MyPB o)
comp' Bool
True ([MExp o] -> ICExp o -> CExp o
forall a o. [MExp o] -> a -> TrBr a o
TrBr [MExp o]
ityp2trs ICExp o
it) CExp o
ityp)
                 (Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
forall o.
Nat
-> Bool
-> Ctx o
-> CExp o
-> MArgList o
-> MExp o
-> Bool
-> (CExp o -> MExp o -> EE (MyPB o))
-> EE (MyPB o)
tcargs 0 Bool
isdep Ctx o
ctx (MExp o -> CExp o -> CExp o
forall o. MExp o -> CExp o -> CExp o
sub MExp o
elimtrm (ICExp o -> CExp o
forall a. a -> TrBr a o
t ICExp o
ot)) MArgList o
as (Hiding -> MExp o -> MExp o -> MExp o
forall o blk. Hiding -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk
addend Hiding
hid MExp o
elimtrm MExp o
elimtrm2) Bool
isconstructor CExp o -> MExp o -> EE (MyPB o)
cont)
            _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "proj function type is not a Pi"
          _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "proj function type is not correct"
     _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "proj, not a datatype"
   _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "proj, not a const app"


 ALConPar _ -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__

 where
  t :: a -> TrBr a o
t = [MExp o] -> a -> TrBr a o
forall a o. [MExp o] -> a -> TrBr a o
TrBr [MExp o]
ityptrs

addend :: Hiding -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk
addend :: Hiding -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk
addend hid :: Hiding
hid a :: MExp o
a (NotM (App uid :: Maybe (UId o)
uid okh :: OKHandle (RefInfo o)
okh elr :: Elr o
elr as :: MArgList o
as)) = 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)
uid OKHandle (RefInfo o)
okh Elr o
elr (MArgList o -> MArgList o
f MArgList o
as)
 where
   f :: MArgList o -> MArgList o
f (NotM ALNil)             = 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
a (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
$ ArgList o
forall o. ArgList o
ALNil)
   f (NotM (ALCons hid :: Hiding
hid a :: MExp o
a 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
$ Hiding -> MExp o -> MArgList o -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp o
a (MArgList o -> MArgList o
f MArgList o
as)
   f _                        = MArgList o
forall a. HasCallStack => a
__IMPOSSIBLE__
addend _ _ _ = MM (Exp o) blk
forall a. HasCallStack => a
__IMPOSSIBLE__

copyarg :: MExp o -> Bool
copyarg :: MExp o -> Bool
copyarg _ = Bool
False

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

type HNNBlks o = [HNExp o]

noblks :: HNNBlks o
noblks :: HNNBlks o
noblks = []

addblk :: HNExp o -> HNNBlks o -> HNNBlks o
addblk :: HNExp o -> HNNBlks o -> HNNBlks o
addblk = (:)

hnn :: ICExp o -> EE (MyMB (HNExp o) o)
hnn :: ICExp o -> EE (MyMB (HNExp o) o)
hnn e :: ICExp o
e = MetaEnv (MB (HNExp o, HNNBlks o) (RefInfo o))
-> ((HNExp o, HNNBlks o) -> EE (MyMB (HNExp o) o))
-> EE (MyMB (HNExp o) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> MetaEnv (MB (HNExp o, HNNBlks o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
e) (((HNExp o, HNNBlks o) -> EE (MyMB (HNExp o) o))
 -> EE (MyMB (HNExp o) o))
-> ((HNExp o, HNNBlks o) -> EE (MyMB (HNExp o) o))
-> EE (MyMB (HNExp o) o)
forall a b. (a -> b) -> a -> b
$ \(hne :: HNExp o
hne, _) -> HNExp o -> EE (MyMB (HNExp o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret HNExp o
hne

hnn_blks :: ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks :: ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks e :: ICExp o
e = ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
forall o.
ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' ICExp o
e ICArgList o
forall o. ICArgList o
CALNil

hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)
hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)
hnn_checkstep e :: ICExp o
e =
 MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyMB (HNExp o, Bool) o))
-> EE (MyMB (HNExp o, Bool) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> ICArgList o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb ICExp o
e ICArgList o
forall o. ICArgList o
CALNil) ((HNExp o -> EE (MyMB (HNExp o, Bool) o))
 -> EE (MyMB (HNExp o, Bool) o))
-> (HNExp o -> EE (MyMB (HNExp o, Bool) o))
-> EE (MyMB (HNExp o, Bool) o)
forall a b. (a -> b) -> a -> b
$ \hne :: HNExp o
hne ->
  MetaEnv
  (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o)
    -> EE (MyMB (HNExp o, Bool) o))
-> EE (MyMB (HNExp o, Bool) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Bool
-> HNExp o
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne) ((Either (ICExp o, ICArgList o) (HNNBlks o)
  -> EE (MyMB (HNExp o, Bool) o))
 -> EE (MyMB (HNExp o, Bool) o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o)
    -> EE (MyMB (HNExp o, Bool) o))
-> EE (MyMB (HNExp o, Bool) o)
forall a b. (a -> b) -> a -> b
$ \res :: Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
   Right _ -> (HNExp o, Bool) -> EE (MyMB (HNExp o, Bool) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNExp o
hne, Bool
False)
   Left (e :: ICExp o
e, as :: ICArgList o
as) ->
    MetaEnv (MB (HNExp o, HNNBlks o) (RefInfo o))
-> ((HNExp o, HNNBlks o) -> EE (MyMB (HNExp o, Bool) o))
-> EE (MyMB (HNExp o, Bool) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o
-> ICArgList o -> MetaEnv (MB (HNExp o, HNNBlks o) (RefInfo o))
forall o.
ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' ICExp o
e ICArgList o
as) (((HNExp o, HNNBlks o) -> EE (MyMB (HNExp o, Bool) o))
 -> EE (MyMB (HNExp o, Bool) o))
-> ((HNExp o, HNNBlks o) -> EE (MyMB (HNExp o, Bool) o))
-> EE (MyMB (HNExp o, Bool) o)
forall a b. (a -> b) -> a -> b
$ \(hne :: HNExp o
hne, _) -> (HNExp o, Bool) -> EE (MyMB (HNExp o, Bool) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNExp o
hne, Bool
True)


hnn' :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' e :: ICExp o
e as :: ICArgList o
as =
 MetaEnv (MB (HNExp o) (RefInfo o))
-> (HNExp o -> EE (MyMB (HNExp o, HNNBlks o) o))
-> EE (MyMB (HNExp o, HNNBlks o) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> ICArgList o -> MetaEnv (MB (HNExp o) (RefInfo o))
forall o. ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb ICExp o
e ICArgList o
as) ((HNExp o -> EE (MyMB (HNExp o, HNNBlks o) o))
 -> EE (MyMB (HNExp o, HNNBlks o) o))
-> (HNExp o -> EE (MyMB (HNExp o, HNNBlks o) o))
-> EE (MyMB (HNExp o, HNNBlks o) o)
forall a b. (a -> b) -> a -> b
$ \hne :: HNExp o
hne ->
  MetaEnv
  (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o)
    -> EE (MyMB (HNExp o, HNNBlks o) o))
-> EE (MyMB (HNExp o, HNNBlks o) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Bool
-> HNExp o
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne) ((Either (ICExp o, ICArgList o) (HNNBlks o)
  -> EE (MyMB (HNExp o, HNNBlks o) o))
 -> EE (MyMB (HNExp o, HNNBlks o) o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o)
    -> EE (MyMB (HNExp o, HNNBlks o) o))
-> EE (MyMB (HNExp o, HNNBlks o) o)
forall a b. (a -> b) -> a -> b
$ \res :: Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
   Right blks :: HNNBlks o
blks -> (HNExp o, HNNBlks o) -> EE (MyMB (HNExp o, HNNBlks o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNExp o
hne, HNNBlks o
blks)
   Left (e :: ICExp o
e, as :: ICArgList o
as) -> ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
forall o.
ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' ICExp o
e ICArgList o
as

hnb :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb e :: ICExp o
e as :: ICArgList o
as = MetaEnv (MB (HNRes o) (RefInfo o))
-> (HNRes o -> EE (MyMB (HNExp o) o)) -> EE (MyMB (HNExp o) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
False ICExp o
e ICArgList o
as []) ((HNRes o -> EE (MyMB (HNExp o) o)) -> EE (MyMB (HNExp o) o))
-> (HNRes o -> EE (MyMB (HNExp o) o)) -> EE (MyMB (HNExp o) o)
forall a b. (a -> b) -> a -> b
$ \res :: HNRes o
res -> case HNRes o
res of
            HNDone _ hne :: HNExp o
hne -> HNExp o -> EE (MyMB (HNExp o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret HNExp o
hne
            HNMeta{} -> EE (MyMB (HNExp o) o)
forall a. HasCallStack => a
__IMPOSSIBLE__

data HNRes o = HNDone (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
             | HNMeta (ICExp o) (ICArgList o) [Maybe (UId o)]

hnc :: Bool -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)
hnc :: Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc haltmeta :: Bool
haltmeta = ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)
forall o.
ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop
 where
  loop :: ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop ce :: ICExp o
ce@(Clos cl :: [CAction o]
cl e :: MM (Exp o) (RefInfo o)
e) cargs :: ICArgList o
cargs seenuids :: [Maybe (UId o)]
seenuids =
   (if Bool
haltmeta then MM (Exp o) (RefInfo o)
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> (Exp o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk b.
MM a blk
-> MetaEnv (MB b blk)
-> (a -> MetaEnv (MB b blk))
-> MetaEnv (MB b blk)
mmmcase MM (Exp o) (RefInfo o)
e (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ ICExp o -> ICArgList o -> [Maybe (UId o)] -> HNRes o
forall o. ICExp o -> ICArgList o -> [Maybe (UId o)] -> HNRes o
HNMeta ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids) else MM (Exp o) (RefInfo o)
-> (Exp o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (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 (HNRes o) (RefInfo o)))
 -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> (Exp o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$
   \ee :: Exp o
ee -> case Exp o
ee of
    App uid :: Maybe (UId o)
uid okh :: OKHandle (RefInfo o)
okh elr :: Elr o
elr args :: MArgList o
args ->
     let ncargs :: ICArgList o
ncargs = Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat ([CAction o] -> MArgList o -> Clos (MArgList o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MArgList o
args) ICArgList o
cargs
     in case Elr o
elr of
      Var v :: Nat
v -> case [CAction o] -> Nat -> Either Nat (ICExp o)
forall o. [CAction o] -> Nat -> Either Nat (ICExp o)
doclos [CAction o]
cl Nat
v of
       Left v' :: Nat
v' -> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> HNExp o -> HNRes o
forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
                        (HNExp o -> HNRes o) -> HNExp o -> HNRes o
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (Maybe (UId o)
uid Maybe (UId o) -> [Maybe (UId o)] -> [Maybe (UId o)]
forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
                        (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Elr o -> ICArgList o -> HNExp' o
forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (Nat -> Elr o
forall o. Nat -> Elr o
Var Nat
v') ICArgList o
ncargs
       Right f :: ICExp o
f -> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop ICExp o
f ICArgList o
ncargs (Maybe (UId o)
uid Maybe (UId o) -> [Maybe (UId o)] -> [Maybe (UId o)]
forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
      Const _ -> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> HNExp o -> HNRes o
forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
                       (HNExp o -> HNRes o) -> HNExp o -> HNRes o
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (Maybe (UId o)
uid Maybe (UId o) -> [Maybe (UId o)] -> [Maybe (UId o)]
forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
                       (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Elr o -> ICArgList o -> HNExp' o
forall o. Elr o -> ICArgList o -> HNExp' o
HNApp Elr o
elr ICArgList o
ncargs
    Lam hid :: Hiding
hid (Abs id :: MId
id b :: MM (Exp o) (RefInfo o)
b) ->
     MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
cargs) ((HNArgList o -> MetaEnv (MB (HNRes o) (RefInfo o)))
 -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> (HNArgList o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \hncargs :: HNArgList o
hncargs -> case HNArgList o
hncargs of
      HNALNil -> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> HNExp o -> HNRes o
forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
                       (HNExp o -> HNRes o) -> HNExp o -> HNRes o
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds [Maybe (UId o)]
seenuids
                       (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Hiding -> Abs (ICExp o) -> HNExp' o
forall o. Hiding -> Abs (ICExp o) -> HNExp' o
HNLam Hiding
hid (MId -> ICExp o -> Abs (ICExp o)
forall a. MId -> a -> Abs a
Abs MId
id ([CAction o] -> MM (Exp o) (RefInfo o) -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos (CAction o
forall o. CAction o
Skip CAction o -> [CAction o] -> [CAction o]
forall a. a -> [a] -> [a]
: [CAction o]
cl) MM (Exp o) (RefInfo o)
b))
      HNALCons _ arg :: ICExp o
arg cargs' :: ICArgList o
cargs' -> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop ([CAction o] -> MM (Exp o) (RefInfo o) -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos (ICExp o -> CAction o
forall o. ICExp o -> CAction o
Sub ICExp o
arg CAction o -> [CAction o] -> [CAction o]
forall a. a -> [a] -> [a]
: [CAction o]
cl) MM (Exp o) (RefInfo o)
b) ICArgList o
cargs' [Maybe (UId o)]
seenuids

      HNALConPar{} -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__

    Pi uid :: Maybe (UId o)
uid hid :: Hiding
hid possdep :: Bool
possdep it :: MM (Exp o) (RefInfo o)
it (Abs id :: MId
id ot :: MM (Exp o) (RefInfo o)
ot) ->
       ICArgList o
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o b.
ICArgList o
-> MetaEnv (MB b (RefInfo o)) -> MetaEnv (MB b (RefInfo o))
checkNoArgs ICArgList o
cargs (MetaEnv (MB (HNRes o) (RefInfo o))
 -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> HNExp o -> HNRes o
forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
         (HNExp o -> HNRes o) -> HNExp o -> HNRes o
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (Maybe (UId o)
uid Maybe (UId o) -> [Maybe (UId o)] -> [Maybe (UId o)]
forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
         (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Hiding -> Bool -> ICExp o -> Abs (ICExp o) -> HNExp' o
forall o. Hiding -> Bool -> ICExp o -> Abs (ICExp o) -> HNExp' o
HNPi Hiding
hid Bool
possdep ([CAction o] -> MM (Exp o) (RefInfo o) -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MM (Exp o) (RefInfo o)
it) (MId -> ICExp o -> Abs (ICExp o)
forall a. MId -> a -> Abs a
Abs MId
id ([CAction o] -> MM (Exp o) (RefInfo o) -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos (CAction o
forall o. CAction o
Skip CAction o -> [CAction o] -> [CAction o]
forall a. a -> [a] -> [a]
: [CAction o]
cl) MM (Exp o) (RefInfo o)
ot))
    Sort s :: Sort
s -> ICArgList o
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o b.
ICArgList o
-> MetaEnv (MB b (RefInfo o)) -> MetaEnv (MB b (RefInfo o))
checkNoArgs ICArgList o
cargs (MetaEnv (MB (HNRes o) (RefInfo o))
 -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret
            (HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o)))
-> HNRes o -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> HNExp o -> HNRes o
forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta (HNExp o -> HNRes o) -> HNExp o -> HNRes o
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds [] (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Sort -> HNExp' o
forall o. Sort -> HNExp' o
HNSort Sort
s

    AbsurdLambda{} -> String -> MetaEnv (MB (HNRes o) (RefInfo o))
forall a blk. String -> MetaEnv (MB a blk)
mbfailed "hnc: encountered absurdlambda"


   where expmeta :: Maybe (UId o)
expmeta = case MM (Exp o) (RefInfo o)
e of {Meta m -> UId o -> Maybe (UId o)
forall a. a -> Maybe a
Just UId o
m; NotM _ -> Maybe (UId o)
forall a. Maybe a
Nothing}
  checkNoArgs :: ICArgList o
-> MetaEnv (MB b (RefInfo o)) -> MetaEnv (MB b (RefInfo o))
checkNoArgs cargs :: ICArgList o
cargs c :: MetaEnv (MB b (RefInfo o))
c =
   MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> MetaEnv (MB b (RefInfo o)))
-> MetaEnv (MB b (RefInfo o))
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
cargs) ((HNArgList o -> MetaEnv (MB b (RefInfo o)))
 -> MetaEnv (MB b (RefInfo o)))
-> (HNArgList o -> MetaEnv (MB b (RefInfo o)))
-> MetaEnv (MB b (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \hncargs :: HNArgList o
hncargs -> case HNArgList o
hncargs of
    HNALNil -> MetaEnv (MB b (RefInfo o))
c
    HNALCons{} -> String -> MetaEnv (MB b (RefInfo o))
forall a blk. String -> MetaEnv (MB a blk)
mbfailed "hnc: there should be no args"

    HNALConPar{} -> MetaEnv (MB b (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__


hnarglist :: ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist :: ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist args :: ICArgList o
args =
 case ICArgList o
args of
  CALNil -> HNArgList o -> EE (MyMB (HNArgList o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret HNArgList o
forall o. HNArgList o
HNALNil
  CALConcat (Clos cl :: [CAction o]
cl args :: MArgList o
args) args2 :: ICArgList o
args2 ->
   MArgList o
-> (ArgList o -> EE (MyMB (HNArgList o) o))
-> EE (MyMB (HNArgList o) o)
forall a blk b.
Refinable a blk =>
MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmcase MArgList o
args ((ArgList o -> EE (MyMB (HNArgList o) o))
 -> EE (MyMB (HNArgList o) o))
-> (ArgList o -> EE (MyMB (HNArgList o) o))
-> EE (MyMB (HNArgList o) o)
forall a b. (a -> b) -> a -> b
$ \args :: ArgList o
args -> case ArgList o
args of
    ALNil -> ICArgList o -> EE (MyMB (HNArgList o) o)
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args2
    ALCons hid :: Hiding
hid arg :: MExp o
arg argsb :: MArgList o
argsb -> HNArgList o -> EE (MyMB (HNArgList o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNArgList o -> EE (MyMB (HNArgList o) o))
-> HNArgList o -> EE (MyMB (HNArgList o) o)
forall a b. (a -> b) -> a -> b
$ Hiding -> ICExp o -> ICArgList o -> HNArgList o
forall o. Hiding -> ICExp o -> ICArgList o -> HNArgList o
HNALCons Hiding
hid ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MExp o
arg) (Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat ([CAction o] -> MArgList o -> Clos (MArgList o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MArgList o
argsb) ICArgList o
args2)

    ALProj{} -> HNArgList o -> EE (MyMB (HNArgList o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret HNArgList o
forall o. HNArgList o
HNALNil -- dirty hack to make check of no-iota in term work


    ALConPar args :: MArgList o
args -> HNArgList o -> EE (MyMB (HNArgList o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNArgList o -> EE (MyMB (HNArgList o) o))
-> HNArgList o -> EE (MyMB (HNArgList o) o)
forall a b. (a -> b) -> a -> b
$ ICArgList o -> HNArgList o
forall o. ICArgList o -> HNArgList o
HNALConPar (Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat ([CAction o] -> MArgList o -> Clos (MArgList o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MArgList o
args) ICArgList o
args2)
-- -----------------------------

getNArgs :: Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs :: Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs 0 args :: ICArgList o
args = Maybe ([ICExp o], ICArgList o)
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Maybe ([ICExp o], ICArgList o)
 -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> Maybe ([ICExp o], ICArgList o)
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a b. (a -> b) -> a -> b
$ ([ICExp o], ICArgList o) -> Maybe ([ICExp o], ICArgList o)
forall a. a -> Maybe a
Just ([], ICArgList o
args)
getNArgs narg :: Nat
narg args :: ICArgList o
args =
 MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args) ((HNArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
 -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> (HNArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a b. (a -> b) -> a -> b
$ \hnargs :: HNArgList o
hnargs -> case HNArgList o
hnargs of
  HNALNil -> Maybe ([ICExp o], ICArgList o)
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe ([ICExp o], ICArgList o)
forall a. Maybe a
Nothing
  HNALCons _ arg :: ICExp o
arg args' :: ICArgList o
args' ->
   EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
-> (Maybe ([ICExp o], ICArgList o)
    -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall o.
Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs (Nat
narg Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- 1) ICArgList o
args') ((Maybe ([ICExp o], ICArgList o)
  -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
 -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> (Maybe ([ICExp o], ICArgList o)
    -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a b. (a -> b) -> a -> b
$ \res :: Maybe ([ICExp o], ICArgList o)
res -> case Maybe ([ICExp o], ICArgList o)
res of
    Nothing -> Maybe ([ICExp o], ICArgList o)
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret Maybe ([ICExp o], ICArgList o)
forall a. Maybe a
Nothing
    Just (pargs :: [ICExp o]
pargs, rargs :: ICArgList o
rargs) -> Maybe ([ICExp o], ICArgList o)
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Maybe ([ICExp o], ICArgList o)
 -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o))
-> Maybe ([ICExp o], ICArgList o)
-> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a b. (a -> b) -> a -> b
$ ([ICExp o], ICArgList o) -> Maybe ([ICExp o], ICArgList o)
forall a. a -> Maybe a
Just (ICExp o
arg ICExp o -> [ICExp o] -> [ICExp o]
forall a. a -> [a] -> [a]
: [ICExp o]
pargs, ICArgList o
rargs)

  HNALConPar{} -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
forall a. HasCallStack => a
__IMPOSSIBLE__


getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs args :: ICArgList o
args =
 MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args) ((HNArgList o -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o))
-> (HNArgList o -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o)
forall a b. (a -> b) -> a -> b
$ \hnargs :: HNArgList o
hnargs -> case HNArgList o
hnargs of
  HNALNil -> [ICExp o] -> EE (MyMB [ICExp o] o)
forall a blk. a -> MetaEnv (MB a blk)
mbret []
  HNALCons _ arg :: ICExp o
arg args' :: ICArgList o
args' ->
   EE (MyMB [ICExp o] o)
-> ([ICExp o] -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> EE (MyMB [ICExp o] o)
forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
args') (([ICExp o] -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o))
-> ([ICExp o] -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o)
forall a b. (a -> b) -> a -> b
$ \args'' :: [ICExp o]
args'' ->
    [ICExp o] -> EE (MyMB [ICExp o] o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (ICExp o
arg ICExp o -> [ICExp o] -> [ICExp o]
forall a. a -> [a] -> [a]
: [ICExp o]
args'')

  HNALConPar args2 :: ICArgList o
args2 ->
   EE (MyMB [ICExp o] o)
-> ([ICExp o] -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> EE (MyMB [ICExp o] o)
forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
args2) (([ICExp o] -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o))
-> ([ICExp o] -> EE (MyMB [ICExp o] o)) -> EE (MyMB [ICExp o] o)
forall a b. (a -> b) -> a -> b
$ \args3 :: [ICExp o]
args3 -> [ICExp o] -> EE (MyMB [ICExp o] o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (ICExp o
forall a. HasCallStack => a
__IMPOSSIBLE__ ICExp o -> [ICExp o] -> [ICExp o]
forall a. a -> [a] -> [a]
: [ICExp o]
args3)


data PEval o = PENo (ICExp o)
             | PEConApp (ICExp o) (ConstRef o) [PEval o]

iotastep :: Bool -> HNExp o -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep :: Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep smartcheck :: Bool
smartcheck e :: HNExp o
e = case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
e 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
   Def narg :: Nat
narg cls :: [Clause o]
cls _ _ ->
    MetaEnv (MB (Maybe ([ICExp o], ICArgList o)) (RefInfo o))
-> (Maybe ([ICExp o], ICArgList o)
    -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Nat
-> ICArgList o
-> MetaEnv (MB (Maybe ([ICExp o], ICArgList o)) (RefInfo o))
forall o.
Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs Nat
narg ICArgList o
args) ((Maybe ([ICExp o], ICArgList o)
  -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
 -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> (Maybe ([ICExp o], ICArgList o)
    -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ \res :: Maybe ([ICExp o], ICArgList o)
res -> case Maybe ([ICExp o], ICArgList o)
res of
     Nothing -> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNNBlks o -> Either (ICExp o, ICArgList o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
forall o. HNNBlks o
noblks)
     Just (pargs :: [ICExp o]
pargs, rargs :: ICArgList o
rargs) ->
      MetaEnv (MB (Either (ICExp o) (HNNBlks o)) (RefInfo o))
-> (Either (ICExp o) (HNNBlks o)
    -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase ([Clause o]
-> [PEval o]
-> MetaEnv (MB (Either (ICExp o) (HNNBlks o)) (RefInfo o))
forall o.
[Clause o]
-> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
dorules [Clause o]
cls ((ICExp o -> PEval o) -> [ICExp o] -> [PEval o]
forall a b. (a -> b) -> [a] -> [b]
map ICExp o -> PEval o
forall o. ICExp o -> PEval o
PENo [ICExp o]
pargs)) ((Either (ICExp o) (HNNBlks o)
  -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
 -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> (Either (ICExp o) (HNNBlks o)
    -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ \res :: Either (ICExp o) (HNNBlks o)
res -> case Either (ICExp o) (HNNBlks o)
res of
       Right blks :: HNNBlks o
blks -> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNNBlks o -> Either (ICExp o, ICArgList o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
blks)
       Left rhs :: ICExp o
rhs -> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (ICExp o, ICArgList o) (HNNBlks o)
 -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ (ICExp o, ICArgList o) -> Either (ICExp o, ICArgList o) (HNNBlks o)
forall a b. a -> Either a b
Left (ICExp o
rhs, ICArgList o
rargs)
   _ -> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (ICExp o, ICArgList o) (HNNBlks o)
 -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ HNNBlks o -> Either (ICExp o, ICArgList o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
forall o. HNNBlks o
noblks
 _ -> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (ICExp o, ICArgList o) (HNNBlks o)
 -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o))
-> Either (ICExp o, ICArgList o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ HNNBlks o -> Either (ICExp o, ICArgList o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
forall o. HNNBlks o
noblks
 where
 dorules :: [Clause o] -> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
 dorules :: [Clause o]
-> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
dorules [] _ = Either (ICExp o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (ICExp o) (HNNBlks o)
 -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o))
-> Either (ICExp o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ HNNBlks o -> Either (ICExp o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
forall o. HNNBlks o
noblks
 dorules (rule :: Clause o
rule:rules' :: [Clause o]
rules') as :: [PEval o]
as =
  MetaEnv
  (MB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) (RefInfo o))
-> (Either (Either [PEval o] (HNNBlks o)) (ICExp o)
    -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o))
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Clause o
-> [PEval o]
-> MetaEnv
     (MB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) (RefInfo o))
forall o.
Clause o
-> [PEval o]
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
dorule Clause o
rule [PEval o]
as) ((Either (Either [PEval o] (HNNBlks o)) (ICExp o)
  -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o))
 -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o))
-> (Either (Either [PEval o] (HNNBlks o)) (ICExp o)
    -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o))
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ \x :: Either (Either [PEval o] (HNNBlks o)) (ICExp o)
x -> case Either (Either [PEval o] (HNNBlks o)) (ICExp o)
x of
   Left (Left as' :: [PEval o]
as') -> [Clause o]
-> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall o.
[Clause o]
-> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
dorules [Clause o]
rules' [PEval o]
as'
   Left (Right blks :: HNNBlks o
blks) -> Either (ICExp o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNNBlks o -> Either (ICExp o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
blks)
   Right rhs :: ICExp o
rhs -> Either (ICExp o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (ICExp o) (HNNBlks o)
 -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o))
-> Either (ICExp o) (HNNBlks o)
-> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
forall a b. (a -> b) -> a -> b
$ ICExp o -> Either (ICExp o) (HNNBlks o)
forall a b. a -> Either a b
Left ICExp o
rhs

 dorule :: Clause o -> [PEval o] -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
 dorule :: Clause o
-> [PEval o]
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
dorule (pats :: [Pat o]
pats, rhs :: MExp o
rhs) as :: [PEval o]
as =
  MetaEnv
  (MB
     (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
     (RefInfo o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o))
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase ([Pat o]
-> [PEval o]
-> MetaEnv
     (MB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
        (RefInfo o))
forall o.
[Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [Pat o]
pats [PEval o]
as) ((Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
  -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o))
 -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o))
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
forall a b. (a -> b) -> a -> b
$ \x :: Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x -> case Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x of
   Right (_, ss :: [ICExp o]
ss) -> Either (Either [PEval o] (HNNBlks o)) (ICExp o)
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) (ICExp o)
 -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o))
-> Either (Either [PEval o] (HNNBlks o)) (ICExp o)
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
forall a b. (a -> b) -> a -> b
$ ICExp o -> Either (Either [PEval o] (HNNBlks o)) (ICExp o)
forall a b. b -> Either a b
Right ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos ((ICExp o -> CAction o) -> [ICExp o] -> [CAction o]
forall a b. (a -> b) -> [a] -> [b]
map ICExp o -> CAction o
forall o. ICExp o -> CAction o
Sub [ICExp o]
ss) MExp o
rhs)
   Left hnas :: Either [PEval o] (HNNBlks o)
hnas -> Either (Either [PEval o] (HNNBlks o)) (ICExp o)
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) (ICExp o)
 -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o))
-> Either (Either [PEval o] (HNNBlks o)) (ICExp o)
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
forall a b. (a -> b) -> a -> b
$ Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) (ICExp o)
forall a b. a -> Either a b
Left Either [PEval o] (HNNBlks o)
hnas

 dopats :: [Pat o] -> [PEval o] -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
 dopats :: [Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [] [] = Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ ([PEval o], [ICExp o])
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. b -> Either a b
Right ([], [])
 dopats (p :: Pat o
p:ps' :: [Pat o]
ps') (a :: PEval o
a:as' :: [PEval o]
as') =
  MetaEnv
  (MB
     (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o]))
     (RefInfo o))
-> (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
    -> EE
         (MyMB
            (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Pat o
-> PEval o
-> MetaEnv
     (MB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o]))
        (RefInfo o))
forall o.
Pat o
-> PEval o
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
dopat Pat o
p PEval o
a) ((Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
  -> EE
       (MyMB
          (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
    -> EE
         (MyMB
            (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \x :: Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
x -> case Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
x of
   Right (hna :: PEval o
hna, ss :: [ICExp o]
ss) ->
    EE
  (MyMB
     (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE
         (MyMB
            (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase ([Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall o.
[Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [Pat o]
ps' [PEval o]
as') ((Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
  -> EE
       (MyMB
          (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE
         (MyMB
            (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \x :: Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x -> case Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x of
     Right (hnas :: [PEval o]
hnas, ss2 :: [ICExp o]
ss2) -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ ([PEval o], [ICExp o])
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. b -> Either a b
Right (PEval o
hna PEval o -> [PEval o] -> [PEval o]
forall a. a -> [a] -> [a]
: [PEval o]
hnas, [ICExp o]
ss2 [ICExp o] -> [ICExp o] -> [ICExp o]
forall a. [a] -> [a] -> [a]
++ [ICExp o]
ss)
     Left (Right blks :: HNNBlks o
blks) -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. a -> Either a b
Left (HNNBlks o -> Either [PEval o] (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
blks)
     Left (Left hnas :: [PEval o]
hnas) -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. a -> Either a b
Left (Either [PEval o] (HNNBlks o)
 -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
-> Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. (a -> b) -> a -> b
$ [PEval o] -> Either [PEval o] (HNNBlks o)
forall a b. a -> Either a b
Left (PEval o
hna PEval o -> [PEval o] -> [PEval o]
forall a. a -> [a] -> [a]
: [PEval o]
hnas)
   Left (Right blks :: HNNBlks o
blks) -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. a -> Either a b
Left (HNNBlks o -> Either [PEval o] (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
blks)
   Left (Left hna :: PEval o
hna) -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
 -> EE
      (MyMB
         (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o))
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. a -> Either a b
Left (Either [PEval o] (HNNBlks o)
 -> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
-> Either [PEval o] (HNNBlks o)
-> Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
forall a b. (a -> b) -> a -> b
$ [PEval o] -> Either [PEval o] (HNNBlks o)
forall a b. a -> Either a b
Left (PEval o
hna PEval o -> [PEval o] -> [PEval o]
forall a. a -> [a] -> [a]
: [PEval o]
as')
 dopats _ _ = String
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. String -> MetaEnv (MB a blk)
mbfailed "bad patterns"

 dopat :: Pat o -> PEval o -> EE (MyMB (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
 dopat :: Pat o
-> PEval o
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
dopat (PatConApp c :: ConstRef o
c pas :: [Pat o]
pas) a :: PEval o
a =
  case PEval o
a of
   PENo a :: ICExp o
a ->
    if Bool
smartcheck then
     MetaEnv (MB Bool (RefInfo o))
-> (Bool
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> MetaEnv (MB Bool (RefInfo o))
forall o. ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor ICExp o
a) ((Bool
  -> EE
       (MyMB
          (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> (Bool
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \notcon :: Bool
notcon -> if Bool
notcon then Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (Either (PEval o) (HNNBlks o)
 -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o]))
-> Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. (a -> b) -> a -> b
$ HNNBlks o -> Either (PEval o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
forall o. HNNBlks o
noblks else EE
  (MyMB
     (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
qq -- to know more often if iota step is possible
    else
     EE
  (MyMB
     (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
qq
    where
     qq :: EE
  (MyMB
     (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
qq =
      MetaEnv (MB (HNExp o, HNNBlks o) (RefInfo o))
-> ((HNExp o, HNNBlks o)
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICExp o -> MetaEnv (MB (HNExp o, HNNBlks o) (RefInfo o))
forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
a) (((HNExp o, HNNBlks o)
  -> EE
       (MyMB
          (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> ((HNExp o, HNNBlks o)
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \(hna :: HNExp o
hna, blks :: HNNBlks o
blks) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hna of
       HNApp (Const c' :: ConstRef o
c') as :: ICArgList o
as ->
        if ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== ConstRef o
c' then
         MetaEnv (MB [ICExp o] (RefInfo o))
-> ([ICExp o]
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> MetaEnv (MB [ICExp o] (RefInfo o))
forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
as) (([ICExp o]
  -> EE
       (MyMB
          (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> ([ICExp o]
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \as' :: [ICExp o]
as' ->
          if [ICExp o] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [ICExp o]
as' Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== [Pat o] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Pat o]
pas then
           MetaEnv
  (MB
     (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
     (RefInfo o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase ([Pat o]
-> [PEval o]
-> MetaEnv
     (MB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
        (RefInfo o))
forall o.
[Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [Pat o]
pas ((ICExp o -> PEval o) -> [ICExp o] -> [PEval o]
forall a b. (a -> b) -> [a] -> [b]
map ICExp o -> PEval o
forall o. ICExp o -> PEval o
PENo [ICExp o]
as')) ((Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
  -> EE
       (MyMB
          (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \x :: Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x -> case Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x of
            Right (hnas :: [PEval o]
hnas, ss :: [ICExp o]
ss) -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ (PEval o, [ICExp o])
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. b -> Either a b
Right (ICExp o -> ConstRef o -> [PEval o] -> PEval o
forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' [PEval o]
hnas, [ICExp o]
ss)
            Left (Right blks :: HNNBlks o
blks) -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (HNNBlks o -> Either (PEval o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
blks)
            Left (Left hnas :: [PEval o]
hnas) -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (Either (PEval o) (HNNBlks o)
 -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o]))
-> Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. (a -> b) -> a -> b
$ PEval o -> Either (PEval o) (HNNBlks o)
forall a b. a -> Either a b
Left (ICExp o -> ConstRef o -> [PEval o] -> PEval o
forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' [PEval o]
hnas)
          else
           String
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. String -> MetaEnv (MB a blk)
mbfailed "dopat: wrong amount of args"
        else 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{} -> MetaEnv (MB [ICExp o] (RefInfo o))
-> ([ICExp o]
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (ICArgList o -> MetaEnv (MB [ICExp o] (RefInfo o))
forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
as) (([ICExp o]
  -> EE
       (MyMB
          (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> ([ICExp o]
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \as' :: [ICExp o]
as' ->
           Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (PEval o -> Either (PEval o) (HNNBlks o)
forall a b. a -> Either a b
Left (ICExp o -> ConstRef o -> [PEval o] -> PEval o
forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' ((ICExp o -> PEval o) -> [ICExp o] -> [PEval o]
forall a b. (a -> b) -> [a] -> [b]
map ICExp o -> PEval o
forall o. ICExp o -> PEval o
PENo [ICExp o]
as')))
          _ -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (HNNBlks o -> Either (PEval o) (HNNBlks o)
forall a b. b -> Either a b
Right (HNExp o -> HNNBlks o -> HNNBlks o
forall o. HNExp o -> HNNBlks o -> HNNBlks o
addblk HNExp o
hna HNNBlks o
blks))
       _ -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (HNNBlks o -> Either (PEval o) (HNNBlks o)
forall a b. b -> Either a b
Right (HNExp o -> HNNBlks o -> HNNBlks o
forall o. HNExp o -> HNNBlks o -> HNNBlks o
addblk HNExp o
hna HNNBlks o
blks))
   aa :: PEval o
aa@(PEConApp a :: ICExp o
a c' :: ConstRef o
c' as :: [PEval o]
as) ->
    if ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== ConstRef o
c' then
     if [PEval o] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [PEval o]
as Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== [Pat o] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Pat o]
pas then
      MetaEnv
  (MB
     (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
     (RefInfo o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase ([Pat o]
-> [PEval o]
-> MetaEnv
     (MB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o]))
        (RefInfo o))
forall o.
[Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [Pat o]
pas [PEval o]
as) ((Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
  -> EE
       (MyMB
          (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
    -> EE
         (MyMB
            (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ \x :: Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x -> case Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])
x of
       Right (hnas :: [PEval o]
hnas, ss :: [ICExp o]
ss) -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ (PEval o, [ICExp o])
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. b -> Either a b
Right (ICExp o -> ConstRef o -> [PEval o] -> PEval o
forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' [PEval o]
hnas, [ICExp o]
ss)
       Left (Right blks :: HNNBlks o
blks) -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (HNNBlks o -> Either (PEval o) (HNNBlks o)
forall a b. b -> Either a b
Right HNNBlks o
blks)
       Left (Left hnas :: [PEval o]
hnas) -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (Either (PEval o) (HNNBlks o)
 -> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o]))
-> Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. (a -> b) -> a -> b
$ PEval o -> Either (PEval o) (HNNBlks o)
forall a b. a -> Either a b
Left (ICExp o -> ConstRef o -> [PEval o] -> PEval o
forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' [PEval o]
hnas)
     else
      String
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. String -> MetaEnv (MB a blk)
mbfailed "dopat: wrong amount of args"
    else
     Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ Either (PEval o) (HNNBlks o)
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. a -> Either a b
Left (PEval o -> Either (PEval o) (HNNBlks o)
forall a b. a -> Either a b
Left PEval o
aa)
 dopat PatVar{} a :: PEval o
a@(PENo a' :: ICExp o
a') = Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ (PEval o, [ICExp o])
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. b -> Either a b
Right (PEval o
a, [ICExp o
a'])
 dopat PatVar{} a :: PEval o
a@(PEConApp a' :: ICExp o
a' _ _) = Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ (PEval o, [ICExp o])
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. b -> Either a b
Right (PEval o
a, [ICExp o
a'])
 dopat PatExp a :: PEval o
a = Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
 -> EE
      (MyMB
         (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o))
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
-> EE
     (MyMB
        (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
forall a b. (a -> b) -> a -> b
$ (PEval o, [ICExp o])
-> Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])
forall a b. b -> Either a b
Right (PEval o
a, [])

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

noiotastep :: HNExp o -> EE (MyPB o)
noiotastep :: HNExp o -> EE (MyPB o)
noiotastep hne :: HNExp o
hne =
 Prio
-> Maybe (RefInfo o)
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioNoIota Maybe (RefInfo o)
forall a. Maybe a
Nothing (Bool
-> HNExp o
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
False HNExp o
hne) ((Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
 -> EE (MyPB o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
-> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
  Left _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "iota step possible contrary to assumed"
  Right _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK

noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)
noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)
noiotastep_term 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
    Def _ [(pats :: [Pat o]
pats, _)] _ _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
      -- all (\pat -> case pat of {PatConApp{} -> False; _ -> True}) pats
    _ -> HNExp o -> EE (MyPB o)
forall o. HNExp o -> EE (MyPB o)
noiotastep (HNExp o -> EE (MyPB o)) -> HNExp o -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds []
                    (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Elr o -> ICArgList o -> HNExp' o
forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
c) (ICArgList o -> HNExp' o) -> ICArgList o -> HNExp' o
forall a b. (a -> b) -> a -> b
$ Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat ([CAction o] -> MArgList o -> Clos (MArgList o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [] MArgList o
args) ICArgList o
forall o. ICArgList o
CALNil

data CMode o = CMRigid (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
             | forall b . Refinable b (RefInfo o) => CMFlex (MM b (RefInfo o)) (CMFlex o)
data CMFlex o = CMFFlex (ICExp o) (ICArgList o) [Maybe (UId o)]
              | CMFSemi (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)
              | CMFBlocked (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)

comp' :: forall o . Bool -> CExp o -> CExp o -> EE (MyPB o)
comp' :: Bool -> CExp o -> CExp o -> EE (MyPB o)
comp' ineq :: Bool
ineq lhs :: CExp o
lhs@(TrBr trs1 :: [MExp o]
trs1 e1 :: ICExp o
e1) rhs :: CExp o
rhs@(TrBr trs2 :: [MExp o]
trs2 e2 :: ICExp o
e2) = Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp Bool
ineq ICExp o
e1 ICExp o
e2
 where
  comp :: Bool -> ICExp o -> ICExp o -> EE (MyPB o)
  comp :: Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp ineq :: Bool
ineq e1 :: ICExp o
e1 e2 :: ICExp o
e2 =
   ICExp o -> ICExp o -> EE (MyPB o)
proc ICExp o
e1 ICExp o
e2

   where
    proc :: ICExp o -> ICExp o -> EE (MyPB o)
proc e1 :: ICExp o
e1 e2 :: ICExp o
e2 = Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
True ICExp o
e1 ICArgList o
forall o. ICArgList o
CALNil [] ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res1 :: CMode o
res1 -> Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
True ICExp o
e2 ICArgList o
forall o. ICArgList o
CALNil [] ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res2 :: CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
    f :: Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f semifok :: Bool
semifok e :: ICExp o
e as :: ICArgList o
as seenuids :: [Maybe (UId o)]
seenuids cont :: CMode o -> EE (MyPB o)
cont =
     Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> (HNRes o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBeta Maybe (RefInfo o)
forall a. Maybe a
Nothing (Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
True ICExp o
e ICArgList o
as [Maybe (UId o)]
seenuids) ((HNRes o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNRes o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: HNRes o
res ->
      case HNRes o
res of
       HNDone mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne -> Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
fhn Bool
semifok Maybe (UId o)
mexpmeta HNExp o
hne CMode o -> EE (MyPB o)
cont

       HNMeta ce :: ICExp o
ce@(Clos cl :: [CAction o]
cl m :: MExp o
m) cargs :: ICArgList o
cargs seenuids :: [Maybe (UId o)]
seenuids -> do
        Bool
b1 <- [CAction o] -> IO Bool
boringClos [CAction o]
cl
        Bool
b2 <- ICArgList o -> IO Bool
boringArgs ICArgList o
cargs
        if Bool
b1 Bool -> Bool -> Bool
&& Bool
b2 then
          CMode o -> EE (MyPB o)
cont (CMode o -> EE (MyPB o)) -> CMode o -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ MExp o -> CMFlex o -> CMode o
forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MExp o
m (ICExp o -> ICArgList o -> [Maybe (UId o)] -> CMFlex o
forall o. ICExp o -> ICArgList o -> [Maybe (UId o)] -> CMFlex o
CMFFlex ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids)
         else
          Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> (HNRes o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBetaStructured Maybe (RefInfo o)
forall a. Maybe a
Nothing (Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
False ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids) ((HNRes o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNRes o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: HNRes o
res ->
           case HNRes o
res of
            HNDone mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne -> CMode o -> EE (MyPB o)
cont (CMode o -> EE (MyPB o)) -> CMode o -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ MExp o -> CMFlex o -> CMode o
forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MExp o
m (Maybe (UId o) -> HNExp o -> CMFlex o
forall o. Maybe (UId o) -> HNExp o -> CMFlex o
CMFBlocked Maybe (UId o)
mexpmeta HNExp o
hne)
            HNMeta{} -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__


    fhn :: Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
fhn semifok :: Bool
semifok mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne cont :: CMode o -> EE (MyPB o)
cont =
     MetaEnv
  (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
-> (forall b.
    Refinable b (RefInfo o) =>
    MM b (RefInfo o) -> EE (MyPB o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
-> EE (MyPB o)
forall a blk.
MetaEnv (MB a blk)
-> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk))
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mmbpcase (Bool
-> HNExp o
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne)
      (\m :: MM b (RefInfo o)
m -> do
        Bool
sf <- Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False {- semiflex hne -}
        if Bool
semifok Bool -> Bool -> Bool
&& Bool
sf then
          CMode o -> EE (MyPB o)
cont (MM b (RefInfo o) -> CMFlex o -> CMode o
forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MM b (RefInfo o)
m (Maybe (UId o) -> HNExp o -> CMFlex o
forall o. Maybe (UId o) -> HNExp o -> CMFlex o
CMFSemi Maybe (UId o)
mexpmeta HNExp o
hne))
         else
          CMode o -> EE (MyPB o)
cont (MM b (RefInfo o) -> CMFlex o -> CMode o
forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MM b (RefInfo o)
m (Maybe (UId o) -> HNExp o -> CMFlex o
forall o. Maybe (UId o) -> HNExp o -> CMFlex o
CMFBlocked Maybe (UId o)
mexpmeta HNExp o
hne))
      )
      (\res :: Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
        Right _ -> CMode o -> EE (MyPB o)
cont (Maybe (UId o) -> HNExp o -> CMode o
forall o. Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> CMode o
CMRigid Maybe (UId o)
mexpmeta HNExp o
hne)
        Left (e :: ICExp o
e, as :: ICArgList o
as) -> Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
semifok ICExp o
e ICArgList o
as [] CMode o -> EE (MyPB o)
cont
      )
    g :: CMode o -> CMode o -> EE (MyPB o)
g res1 :: CMode o
res1 res2 :: CMode o
res2 =
     case (CMode o
res1, CMode o
res2) of
      (CMRigid mexpmeta1 :: Maybe (UId o)
mexpmeta1 hne1 :: HNExp o
hne1, CMRigid mexpmeta2 :: Maybe (UId o)
mexpmeta2 hne2 :: HNExp o
hne2) -> Bool
-> Maybe (UId o)
-> HNExp o
-> Maybe (UId o)
-> HNExp o
-> EE (MyPB o)
comphn Bool
ineq Maybe (UId o)
mexpmeta1 HNExp o
hne1 Maybe (UId o)
mexpmeta2 HNExp o
hne2
      (CMFlex m1 :: MM b (RefInfo o)
m1 (CMFBlocked mexpmeta1 :: Maybe (UId o)
mexpmeta1 hne1 :: HNExp o
hne1), _) -> Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
mstp Bool
False Maybe (UId o)
mexpmeta1 HNExp o
hne1 ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res1 :: CMode o
res1 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
      (_, CMFlex m2 :: MM b (RefInfo o)
m2 (CMFBlocked mexpmeta2 :: Maybe (UId o)
mexpmeta2 hne2 :: HNExp o
hne2)) -> Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
mstp Bool
False Maybe (UId o)
mexpmeta2 HNExp o
hne2 ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res2 :: CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
      (CMRigid mexpmeta1 :: Maybe (UId o)
mexpmeta1 hne1 :: HNExp o
hne1, CMFlex _ fl2 :: CMFlex o
fl2) -> Bool -> Maybe (UId o) -> HNExp o -> CMFlex o -> EE (MyPB o)
unif Bool
True Maybe (UId o)
mexpmeta1 HNExp o
hne1 CMFlex o
fl2
      (CMFlex _ fl1 :: CMFlex o
fl1, CMRigid mexpmeta2 :: Maybe (UId o)
mexpmeta2 hne2 :: HNExp o
hne2) -> Bool -> Maybe (UId o) -> HNExp o -> CMFlex o -> EE (MyPB o)
unif Bool
False Maybe (UId o)
mexpmeta2 HNExp o
hne2 CMFlex o
fl1


      (CMFlex m1 :: MM b (RefInfo o)
m1 fl1 :: CMFlex o
fl1, CMFlex m2 :: MM b (RefInfo o)
m2 fl2 :: CMFlex o
fl2) -> MM b (RefInfo o) -> MM b (RefInfo o) -> EE (MyPB o) -> EE (MyPB o)
forall a blk b.
(Refinable a blk, Refinable b blk) =>
MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk)
doubleblock MM b (RefInfo o)
m1 MM b (RefInfo o)
m2 (EE (MyPB o) -> EE (MyPB o)) -> EE (MyPB o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ CMFlex o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
fcm CMFlex o
fl1 ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res1 :: CMode o
res1 -> CMFlex o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
fcm CMFlex o
fl2 ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res2 :: CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
    fcm :: CMFlex o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
fcm (CMFFlex ce :: ICExp o
ce cargs :: ICArgList o
cargs seenuids :: [Maybe (UId o)]
seenuids) = Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
True ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids
    fcm (CMFSemi mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne) = Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
fhn Bool
True Maybe (UId o)
mexpmeta HNExp o
hne
    fcm (CMFBlocked _ hne :: HNExp o
hne) = (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__ -- not used. if so should be: fhn False hne
    mstp :: Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
mstp semif :: Bool
semif mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne cont :: CMode o -> EE (MyPB o)
cont =
     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
$ Prio -> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Or Prio
prioCompChoice
      (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
$ Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just [CExp o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term CExp o
lhs, CExp o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term CExp o
rhs])
       (HNExp o -> EE (MyPB o)
forall o. HNExp o -> EE (MyPB o)
noiotastep HNExp o
hne)
       (CMode o -> EE (MyPB o)
cont (Maybe (UId o) -> HNExp o -> CMode o
forall o. Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> CMode o
CMRigid Maybe (UId o)
mexpmeta HNExp o
hne))
      )
      (Bool -> HNExp o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
stp Bool
semif HNExp o
hne CMode o -> EE (MyPB o)
cont)
    stp :: Bool -> HNExp o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
stp semif :: Bool
semif hne :: HNExp o
hne cont :: CMode o -> EE (MyPB o)
cont =
     Prio
-> Maybe (RefInfo o)
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompIota (RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just (RefInfo o -> Maybe (RefInfo o)) -> RefInfo o -> Maybe (RefInfo o)
forall a b. (a -> b) -> a -> b
$ Bool -> RefInfo o
forall o. Bool -> RefInfo o
RIIotaStep Bool
semif) (Bool
-> HNExp o
-> MetaEnv
     (MB (Either (ICExp o, ICArgList o) (HNNBlks o)) (RefInfo o))
forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne) ((Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
 -> EE (MyPB o))
-> (Either (ICExp o, ICArgList o) (HNNBlks o) -> EE (MyPB o))
-> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
      Right _ -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "no iota step possible, contrary to assumed"
      Left (e :: ICExp o
e, as :: ICArgList o
as) -> Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
semif ICExp o
e ICArgList o
as [] CMode o -> EE (MyPB o)
cont
    unif :: Bool -> Maybe (UId o) -> HNExp o -> CMFlex o -> EE (MyPB o)
unif oppis1 :: Bool
oppis1 oppmexpmeta :: Maybe (UId o)
oppmexpmeta opphne :: HNExp o
opphne res :: CMFlex o
res =
     let iter :: CMode o -> EE (MyPB o)
iter res :: CMode o
res = if Bool
oppis1 then
                     CMode o -> CMode o -> EE (MyPB o)
g (Maybe (UId o) -> HNExp o -> CMode o
forall o. Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> CMode o
CMRigid Maybe (UId o)
oppmexpmeta HNExp o
opphne) CMode o
res
                    else
                     CMode o -> CMode o -> EE (MyPB o)
g CMode o
res (Maybe (UId o) -> HNExp o -> CMode o
forall o. Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> CMode o
CMRigid Maybe (UId o)
oppmexpmeta HNExp o
opphne)
     in case CMFlex o
res of
      CMFFlex ce :: ICExp o
ce cargs :: ICArgList o
cargs seenuids :: [Maybe (UId o)]
seenuids -> do
       Bool
poss <- ICExp o -> ICArgList o -> IO Bool
forall o. ICExp o -> ICArgList o -> IO Bool
iotapossmeta ICExp o
ce ICArgList o
cargs
       Bool -> Prio -> EE (MyPB o) -> EE (MyPB o) -> EE (MyPB o)
forall o.
Bool
-> Prio
-> IO (PB (RefInfo o))
-> IO (PB (RefInfo o))
-> IO (PB (RefInfo o))
maybeor Bool
poss Prio
prioCompChoice
        (ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyPB o)
loop ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids)
-- (mbpcase prioCompBeta (Just $ RIIotaStep False) (hnb ce cargs) $ \hne ->
        (Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> (HNRes o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBeta (RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just (RefInfo o -> Maybe (RefInfo o)) -> RefInfo o -> Maybe (RefInfo o)
forall a b. (a -> b) -> a -> b
$ Bool -> RefInfo o
forall o. Bool -> RefInfo o
RIIotaStep Bool
False) (Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
False ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids) ((HNRes o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNRes o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: HNRes o
res ->
          -- RIIotaStep here on beta-norm to make cost high when guessing elim const in type par
          case HNRes o
res of
           HNDone mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne -> Bool -> HNExp o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
stp Bool
False HNExp o
hne CMode o -> EE (MyPB o)
iter
           HNMeta{} -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__
        )
       where
        loop :: ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyPB o)
loop ce :: ICExp o
ce@(Clos cl :: [CAction o]
cl m :: MExp o
m) cargs :: ICArgList o
cargs seenuids :: [Maybe (UId o)]
seenuids =
         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
prioCompUnif, RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just ([CAction o] -> HNExp o -> RefInfo o
forall o. [CAction o] -> HNExp o -> RefInfo o
RIUnifInfo [CAction o]
cl HNExp o
opphne)) MExp o
m ((Exp o -> EE (MyPB o)) -> EE (MyPB o))
-> (Exp o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \_ ->
         Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNRes o) (RefInfo o))
-> (HNRes o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBeta Maybe (RefInfo o)
forall a. Maybe a
Nothing (Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
True ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids) ((HNRes o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNRes o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res :: HNRes o
res -> case HNRes o
res of
          HNDone mexpmeta :: Maybe (UId o)
mexpmeta hne :: HNExp o
hne ->
           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
$ Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just [CExp o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term CExp o
lhs, CExp o -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term CExp o
rhs])
            (HNExp o -> EE (MyPB o)
forall o. HNExp o -> EE (MyPB o)
noiotastep HNExp o
hne)
            (CMode o -> EE (MyPB o)
iter (Maybe (UId o) -> HNExp o -> CMode o
forall o. Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> CMode o
CMRigid Maybe (UId o)
mexpmeta HNExp o
hne))
          HNMeta ce :: ICExp o
ce cargs :: ICArgList o
cargs seenuids :: [Maybe (UId o)]
seenuids -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyPB o)
loop ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids
      CMFSemi _ hne :: HNExp o
hne ->
       EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__ -- CMFSemi disabled, if used should be: stp True hne iter
      CMFBlocked{} -> EE (MyPB o)
forall a. HasCallStack => a
__IMPOSSIBLE__
    comphn :: Bool -> Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> EE (MyPB o)
    comphn :: Bool
-> Maybe (UId o)
-> HNExp o
-> Maybe (UId o)
-> HNExp o
-> EE (MyPB o)
comphn ineq :: Bool
ineq mexpmeta1 :: Maybe (UId o)
mexpmeta1 hne1 :: HNExp o
hne1 mexpmeta2 :: Maybe (UId o)
mexpmeta2 hne2 :: HNExp o
hne2 =
     case (HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne1, HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne2) of
      (HNApp elr1 :: Elr o
elr1 args1 :: ICArgList o
args1, HNApp elr2 :: Elr o
elr2 args2 :: ICArgList o
args2) ->
       let ce :: Maybe String
ce = case (Elr o
elr1, Elr o
elr2) of
                 (Var v1 :: Nat
v1, Var v2 :: Nat
v2) ->
                     if Nat
v1 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
v2 then Maybe String
forall a. Maybe a
Nothing
                     else String -> Maybe String
forall a. a -> Maybe a
Just "comphn, elr, vars not equal"
                 (Const c1 :: ConstRef o
c1, Const c2 :: ConstRef o
c2) ->
                    if ConstRef o
c1 ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== ConstRef o
c2 then Maybe String
forall a. Maybe a
Nothing
                    else String -> Maybe String
forall a. a -> Maybe a
Just "comphn, elr, consts not equal"
                 (_, _) -> String -> Maybe String
forall a. a -> Maybe a
Just "comphn, elrs not equal"
       in case Maybe String
ce of
            Nothing -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1 ICArgList o
args2
            Just msg :: String
msg -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error String
msg
      (HNLam hid1 :: Hiding
hid1 (Abs id1 :: MId
id1 b1 :: ICExp o
b1), HNLam hid2 :: Hiding
hid2 (Abs id2 :: MId
id2 b2 :: ICExp o
b2)) -> Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp Bool
False ICExp o
b1 ICExp o
b2
      (HNLam _ (Abs _ b1 :: ICExp o
b1), HNApp elr2 :: Elr o
elr2 args2 :: ICArgList o
args2) ->
       Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
True ICExp o
b1 ICArgList o
forall o. ICArgList o
CALNil (HNExp o -> [Maybe (UId o)]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne1) ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res1 :: CMode o
res1 ->
       Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
fhn Bool
True Maybe (UId o)
mexpmeta2 ([Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (HNExp o -> [Maybe (UId o)]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne2) (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Elr o -> ICArgList o -> HNExp' o
forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (Nat -> Elr o -> Elr o
forall t. Weakening t => Nat -> t -> t
weak 1 Elr o
elr2) (Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs ([CAction o] -> MArgList o -> Clos (MArgList o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [] (MArgList o -> Clos (MArgList o) o)
-> MArgList o -> Clos (MArgList o) o
forall a b. (a -> b) -> a -> b
$ 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
NotHidden{- arbitrary -} (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (Nat -> Elr o
forall o. Nat -> Elr o
Var 0) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) (Nat -> ICArgList o -> ICArgList o
forall t. Weakening t => Nat -> t -> t
weak 1 ICArgList o
args2))) ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res2 :: CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
      (HNApp elr1 :: Elr o
elr1 args1 :: ICArgList o
args1, HNLam _ (Abs _ b2 :: ICExp o
b2)) ->
       Bool
-> Maybe (UId o)
-> HNExp o
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
fhn Bool
True Maybe (UId o)
mexpmeta1 ([Maybe (UId o)] -> HNExp' o -> HNExp o
forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (HNExp o -> [Maybe (UId o)]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne1) (HNExp' o -> HNExp o) -> HNExp' o -> HNExp o
forall a b. (a -> b) -> a -> b
$ Elr o -> ICArgList o -> HNExp' o
forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (Nat -> Elr o -> Elr o
forall t. Weakening t => Nat -> t -> t
weak 1 Elr o
elr1) (Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs ([CAction o] -> MArgList o -> Clos (MArgList o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [] (MArgList o -> Clos (MArgList o) o)
-> MArgList o -> Clos (MArgList o) o
forall a b. (a -> b) -> a -> b
$ 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
NotHidden{- arbitrary -} (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (Nat -> Elr o
forall o. Nat -> Elr o
Var 0) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)) (Nat -> ICArgList o -> ICArgList o
forall t. Weakening t => Nat -> t -> t
weak 1 ICArgList o
args1))) ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res1 :: CMode o
res1 -> Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> (CMode o -> EE (MyPB o))
-> EE (MyPB o)
f Bool
True ICExp o
b2 ICArgList o
forall o. ICArgList o
CALNil (HNExp o -> [Maybe (UId o)]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne2) ((CMode o -> EE (MyPB o)) -> EE (MyPB o))
-> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \res2 :: CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
{-
      (HNLam _ (Abs _ b1), HNApp uid2 elr2 args2) ->
       f True b1 CALNil $ \res1 -> g res1
        (CMRigid mexpmeta2 (HNApp uid2 (weak 1 elr2) (addtrailingargs (Clos [] $ NotM $ ALCons NotHidden{- arbitrary -} (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)) (NotM ALNil)) (weak 1 args2))))
      (HNApp uid1 elr1 args1, HNLam _ (Abs _ b2)) ->
       f True b2 CALNil $ \res2 -> g
        (CMRigid mexpmeta1 (HNApp uid1 (weak 1 elr1) (addtrailingargs (Clos [] $ NotM $ ALCons NotHidden{- arbitrary -} (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)) (NotM ALNil)) (weak 1 args1))))
        res2
-}
      (HNPi hid1 :: Hiding
hid1 _ it1 :: ICExp o
it1 (Abs id1 :: MId
id1 ot1 :: ICExp o
ot1), HNPi hid2 :: Hiding
hid2 _ it2 :: ICExp o
it2 (Abs id2 :: MId
id2 ot2 :: ICExp o
ot2)) -> 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
$
       Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just [[MExp o] -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term [MExp o]
trs1, [MExp o] -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term [MExp o]
trs2]) (Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp Bool
False ICExp o
it1 ICExp o
it2) (Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp Bool
ineq ICExp o
ot1 ICExp o
ot2)
      (HNSort s1 :: Sort
s1, HNSort s2 :: Sort
s2) -> 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
$
       case (Sort
s1, Sort
s2) of
        (Set i1 :: Nat
i1, Set i2 :: Nat
i2) -> if Nat
i1 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
i2 Bool -> Bool -> Bool
|| Bool
ineq Bool -> Bool -> Bool
&& Nat
i1 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
i2 then Prop (RefInfo o)
forall blk. Prop blk
OK else String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "comphn, set levels not matching"
        (Set _, UnknownSort) -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (UnknownSort, Set _) -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (UnknownSort, UnknownSort) -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Type, Set _) | Bool
ineq -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Type, UnknownSort) | Bool
ineq -> Prop (RefInfo o)
forall blk. Prop blk
OK
        _ -> Prop (RefInfo o)
forall a. HasCallStack => a
__IMPOSSIBLE__
      (HNApp (Const c1 :: ConstRef o
c1) _, _) -> case Maybe (UId o)
mexpmeta2 of
       Nothing -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "comphn, not equal (2)"
       Just m2 :: UId o
m2 -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> UId o -> Move' (RefInfo o) (Exp o) -> Prop (RefInfo o)
forall blk a. String -> Metavar a blk -> Move' blk a -> Prop blk
AddExtraRef "comphn: not equal, adding extra ref"
                          UId o
m2 (UId o -> [Maybe (UId o)] -> ConstRef o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref UId o
m2 (HNExp o -> [Maybe (UId o)]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne1) ConstRef o
c1)
      (_, HNApp (Const c2 :: ConstRef o
c2) _) -> case Maybe (UId o)
mexpmeta1 of
       Nothing -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "comphn, not equal (3)"
       Just m1 :: UId o
m1 -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> UId o -> Move' (RefInfo o) (Exp o) -> Prop (RefInfo o)
forall blk a. String -> Metavar a blk -> Move' blk a -> Prop blk
AddExtraRef "comphn: not equal, adding extra ref"
                          UId o
m1 (UId o -> [Maybe (UId o)] -> ConstRef o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref UId o
m1 (HNExp o -> [Maybe (UId o)]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne2) ConstRef o
c2)
      (_, _) -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error "comphn, not equal"

    compargs :: ICArgList o -> ICArgList o -> EE (MyPB o)
    compargs :: ICArgList o -> ICArgList o -> EE (MyPB o)
compargs args1 :: ICArgList o
args1 args2 :: ICArgList o
args2 =
     Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompareArgList Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args1) ((HNArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnargs1 :: HNArgList o
hnargs1 ->
     Prio
-> Maybe (RefInfo o)
-> MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyPB o))
-> EE (MyPB o)
forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompareArgList Maybe (RefInfo o)
forall a. Maybe a
Nothing (ICArgList o -> MetaEnv (MB (HNArgList o) (RefInfo o))
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args2) ((HNArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (HNArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \hnargs2 :: HNArgList o
hnargs2 ->
     case (HNArgList o
hnargs1, HNArgList o
hnargs2) of
      (HNALNil, HNALNil) -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
      (HNALCons hid1 :: Hiding
hid1 arg1 :: ICExp o
arg1 args1b :: ICArgList o
args1b, HNALCons hid2 :: Hiding
hid2 arg2 :: ICExp o
arg2 args2b :: ICArgList o
args2b) -> 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
$
       Maybe [Term (RefInfo o)]
-> EE (MyPB o) -> EE (MyPB o) -> Prop (RefInfo o)
forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And ([Term (RefInfo o)] -> Maybe [Term (RefInfo o)]
forall a. a -> Maybe a
Just [[MExp o] -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term [MExp o]
trs1, [MExp o] -> Term (RefInfo o)
forall blk a. Trav a blk => a -> Term blk
Term [MExp o]
trs2]) (Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp Bool
False ICExp o
arg1 ICExp o
arg2) (ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1b ICArgList o
args2b)

      (HNALConPar args1b :: ICArgList o
args1b, HNALCons _ _ args2b :: ICArgList o
args2b) -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1b ICArgList o
args2b
      (HNALCons _ _ args1b :: ICArgList o
args1b, HNALConPar args2b :: ICArgList o
args2b) -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1b ICArgList o
args2b
      (HNALConPar args1' :: ICArgList o
args1', HNALConPar args2' :: ICArgList o
args2') -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1' ICArgList o
args2'

      (_, _) -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> EE (MyPB o))
-> Prop (RefInfo o) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ String -> Prop (RefInfo o)
forall blk. String -> Prop blk
Error (String -> Prop (RefInfo o)) -> String -> Prop (RefInfo o)
forall a b. (a -> b) -> a -> b
$ "comphnargs, not equal"


    boringExp :: ICExp o -> EE Bool
    boringExp :: ICExp o -> IO Bool
boringExp (Clos cl :: [CAction o]
cl e :: MExp o
e) = do
     MExp o
e <- MExp o -> MetaEnv (MExp o)
forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MExp o
e
     case MExp o
e of
      Meta{} -> [CAction o] -> IO Bool
boringClos [CAction o]
cl
      NotM e :: Exp o
e -> case Exp o
e of
       App _ _ (Var v :: Nat
v) as :: MArgList o
as -> do
        MArgList o
as <- MArgList o -> MetaEnv (MArgList o)
forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MArgList o
as
        case MArgList o
as of
         Meta{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
         NotM as :: ArgList o
as -> case ArgList o
as of
          ALNil -> case [CAction o] -> Nat -> Either Nat (ICExp o)
forall o. [CAction o] -> Nat -> Either Nat (ICExp o)
doclos [CAction o]
cl Nat
v of
           Left _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
           Right e :: ICExp o
e -> ICExp o -> IO Bool
boringExp ICExp o
e
          ALCons{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          ALProj{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          ALConPar{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

       _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    boringClos :: [CAction o] -> EE Bool
    boringClos :: [CAction o] -> IO Bool
boringClos cl :: [CAction o]
cl = ([Bool] -> Bool) -> IO [Bool] -> IO Bool
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bool -> Bool
forall a. a -> a
id) (IO [Bool] -> IO Bool) -> IO [Bool] -> IO Bool
forall a b. (a -> b) -> a -> b
$ (CAction o -> IO Bool) -> [CAction o] -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CAction o -> IO Bool
f [CAction o]
cl
     where f :: CAction o -> IO Bool
f (Sub e :: ICExp o
e) = ICExp o -> IO Bool
boringExp ICExp o
e
           f Skip = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
           f (Weak _) = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    boringArgs :: ICArgList o -> EE Bool
    boringArgs :: ICArgList o -> IO Bool
boringArgs CALNil = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    boringArgs (CALConcat (Clos cl :: [CAction o]
cl as :: MArgList o
as) as2 :: ICArgList o
as2) = do
     Bool
b1 <- [CAction o] -> MArgList o -> IO Bool
f [CAction o]
cl MArgList o
as
     Bool
b2 <- ICArgList o -> IO Bool
boringArgs ICArgList o
as2
     Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
b1 Bool -> Bool -> Bool
&& Bool
b2
     where
      f :: [CAction o] -> MArgList o -> IO Bool
f cl :: [CAction o]
cl as :: MArgList o
as = do
       MArgList o
as <- MArgList o -> MetaEnv (MArgList o)
forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MArgList o
as
       case MArgList o
as of
        Meta{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        NotM as :: ArgList o
as -> case ArgList o
as of
         ALNil -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
         ALCons _ a :: MExp o
a as :: MArgList o
as -> do
          Bool
b1 <- ICExp o -> IO Bool
boringExp ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MExp o
a)
          Bool
b2 <- [CAction o] -> MArgList o -> IO Bool
f [CAction o]
cl MArgList o
as
          Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
b1 Bool -> Bool -> Bool
&& Bool
b2

         ALProj{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False  -- Not impossible: #2966


         ALConPar as :: MArgList o
as -> [CAction o] -> MArgList o -> IO Bool
f [CAction o]
cl MArgList o
as
-- ---------------------------------

checkeliminand :: MExp o -> EE (MyPB o)
checkeliminand :: MExp o -> EE (MyPB o)
checkeliminand = [UId o] -> [Elr o] -> MExp o -> EE (MyPB o)
forall o. [UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f [] []
 where
  f :: [UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f uids :: [UId o]
uids used :: [Elr o]
used e :: MExp o
e =
   BlkInfo (RefInfo o)
-> MExp o
-> (Exp o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just ([UId o] -> [Elr o] -> RefInfo o
forall o. [UId o] -> [Elr o] -> RefInfo o
RIUsedVars [UId o]
uids [Elr o]
used)) MExp o
e ((Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o)))
-> (Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \e :: Exp o
e -> case Exp o
e of
    App uid :: Maybe (UId o)
uid _ elr :: Elr o
elr@(Var{}) args :: MArgList o
args -> [UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs (Maybe (UId o) -> [UId o] -> [UId o]
forall a. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (Elr o
elr Elr o -> [Elr o] -> [Elr o]
forall a. a -> [a] -> [a]
: [Elr o]
used) MArgList o
args
    App uid :: Maybe (UId o)
uid _ elr :: Elr o
elr@(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
      Def _ _ (Just i :: Nat
i) _ -> 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 ([UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs (Maybe (UId o) -> [UId o] -> [UId o]
forall a. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (Elr o
elr Elr o -> [Elr o] -> [Elr o]
forall a. a -> [a] -> [a]
: [Elr o]
used) MArgList o
args) (Nat -> MArgList o -> MetaEnv (PB (RefInfo o))
forall a o.
(Eq a, Num a) =>
a -> MArgList o -> MetaEnv (PB (RefInfo o))
g Nat
i MArgList o
args)
       where
        g :: a -> MArgList o -> MetaEnv (PB (RefInfo o))
g i :: a
i 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 -> case a
i of
                   0 -> BlkInfo (RefInfo o)
-> MExp o
-> (Exp o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just RefInfo o
forall o. RefInfo o
RINotConstructor) MExp o
a ((Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o)))
-> (Exp o -> MetaEnv (PB (RefInfo o))) -> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \_ ->
                         Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
                   _ -> a -> MArgList o -> MetaEnv (PB (RefInfo o))
g (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) MArgList o
as

                  ALProj eas :: MArgList o
eas _ _ as :: MArgList o
as -> 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 -> case a
i of
                   0 -> MetaEnv (PB (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__
                   _ -> a -> MArgList o -> MetaEnv (PB (RefInfo o))
g (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) MArgList o
as

      _ -> [UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs (Maybe (UId o) -> [UId o] -> [UId o]
forall a. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (Elr o
elr Elr o -> [Elr o] -> [Elr o]
forall a. a -> [a] -> [a]
: [Elr o]
used) MArgList o
args
    Lam _ (Abs _ e :: MExp o
e) -> [UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f [UId o]
uids ([Elr o] -> [Elr o]
forall o. [Elr o] -> [Elr o]
w [Elr o]
used) MExp o
e
    Pi uid :: Maybe (UId o)
uid _ _ e1 :: MExp o
e1 (Abs _ e2 :: MExp o
e2) -> 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 ([UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f (Maybe (UId o) -> [UId o] -> [UId o]
forall a. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) [Elr o]
used MExp o
e1) ([UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f (Maybe (UId o) -> [UId o] -> [UId o]
forall a. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) ([Elr o] -> [Elr o]
forall o. [Elr o] -> [Elr o]
w [Elr o]
used) MExp o
e2)
    Sort _ -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK

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


  fs :: [UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs uids :: [UId o]
uids used :: [Elr o]
used 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 -> 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 ([UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f [UId o]
uids [Elr o]
used MExp o
a) ([UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [UId o]
uids [Elr o]
used MArgList o
as)

    ALProj eas :: MArgList o
eas _ _ as :: MArgList o
as -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
-> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ MetaEnv (PB (RefInfo o))
-> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition ([UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [UId o]
uids [Elr o]
used MArgList o
eas) ([UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [UId o]
uids [Elr o]
used MArgList o
as)


    ALConPar as :: MArgList o
as -> [UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [UId o]
uids [Elr o]
used MArgList o
as

  w :: [Elr o] -> [Elr o]
w = (Elr o -> Elr o) -> [Elr o] -> [Elr o]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Elr o
x -> case Elr o
x of {Var v :: Nat
v -> Nat -> Elr o
forall o. Nat -> Elr o
Var (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ 1); Const{} -> Elr o
x})
  adduid :: Maybe a -> [a] -> [a]
adduid (Just uid :: a
uid) uids :: [a]
uids = a
uid a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
uids
  adduid Nothing uids :: [a]
uids = [a]
uids

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

maybeor :: Bool -> Prio -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) ->
           IO (PB (RefInfo o))
maybeor :: Bool
-> Prio
-> IO (PB (RefInfo o))
-> IO (PB (RefInfo o))
-> IO (PB (RefInfo o))
maybeor _ _ mainalt :: IO (PB (RefInfo o))
mainalt _ = IO (PB (RefInfo o))
mainalt

iotapossmeta :: ICExp o -> ICArgList o -> EE Bool
iotapossmeta :: ICExp o -> ICArgList o -> IO Bool
iotapossmeta ce :: ICExp o
ce@(Clos cl :: [CAction o]
cl _) cargs :: ICArgList o
cargs = do
 [Bool]
xs <- (CAction o -> IO Bool) -> [CAction o] -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CAction o -> IO Bool
forall o. CAction o -> IO Bool
ncaction [CAction o]
cl
 Bool
y <- ICArgList o -> IO Bool
forall o. ICArgList o -> IO Bool
nccargs ICArgList o
cargs
 Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not ((Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bool -> Bool
forall a. a -> a
id [Bool]
xs Bool -> Bool -> Bool
&& Bool
y)
 where
  ncaction :: CAction o -> IO Bool
ncaction (Sub ce :: ICExp o
ce) = ICExp o -> IO Bool
forall o. ICExp o -> IO Bool
nonconstructor ICExp o
ce
  ncaction Skip = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ncaction (Weak{}) = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  nccargs :: ICArgList o -> IO Bool
nccargs CALNil = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  nccargs (CALConcat (Clos cl :: [CAction o]
cl margs :: MArgList o
margs) cargs :: ICArgList o
cargs) = do
   Bool
x <- [CAction o] -> MArgList o -> IO Bool
forall o. [CAction o] -> MM (ArgList o) (RefInfo o) -> IO Bool
ncmargs [CAction o]
cl MArgList o
margs
   Bool
y <- ICArgList o -> IO Bool
nccargs ICArgList o
cargs
   Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
x Bool -> Bool -> Bool
&& Bool
y
  ncmargs :: [CAction o] -> MM (ArgList o) (RefInfo o) -> IO Bool
ncmargs cl :: [CAction o]
cl (Meta m :: Metavar (ArgList o) (RefInfo o)
m) = do
   Maybe (ArgList o)
mb <- IORef (Maybe (ArgList o)) -> IO (Maybe (ArgList o))
forall a. IORef a -> IO a
readIORef (Metavar (ArgList o) (RefInfo o) -> IORef (Maybe (ArgList o))
forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar (ArgList o) (RefInfo o)
m)
   case Maybe (ArgList o)
mb of
    Nothing -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just x :: ArgList o
x -> [CAction o] -> ArgList o -> IO Bool
ncargs [CAction o]
cl ArgList o
x
  ncmargs cl :: [CAction o]
cl (NotM args :: ArgList o
args) = [CAction o] -> ArgList o -> IO Bool
ncargs [CAction o]
cl ArgList o
args
  ncargs :: [CAction o] -> ArgList o -> IO Bool
ncargs cl :: [CAction o]
cl ALNil = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ncargs cl :: [CAction o]
cl (ALCons _ a :: MExp o
a args :: MM (ArgList o) (RefInfo o)
args) = do
   Bool
x <- ICExp o -> IO Bool
forall o. ICExp o -> IO Bool
nonconstructor ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [CAction o]
cl MExp o
a)
   Bool
y <- [CAction o] -> MM (ArgList o) (RefInfo o) -> IO Bool
ncmargs [CAction o]
cl MM (ArgList o) (RefInfo o)
args
   Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
x Bool -> Bool -> Bool
&& Bool
y

  ncargs _ (ALProj{}) = IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__


  ncargs cl :: [CAction o]
cl (ALConPar args :: MM (ArgList o) (RefInfo o)
args) = [CAction o] -> MM (ArgList o) (RefInfo o) -> IO Bool
ncmargs [CAction o]
cl MM (ArgList o) (RefInfo o)
args

  nonconstructor :: ICExp o -> EE Bool
  nonconstructor :: ICExp o -> IO Bool
nonconstructor ce :: ICExp o
ce = do
   MyMB (HNRes o) o
res <- Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
True ICExp o
ce ICArgList o
forall o. ICArgList o
CALNil []
   case MyMB (HNRes o) o
res of
    Blocked{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Failed{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    NotB res :: HNRes o
res -> case HNRes o
res of
     HNMeta ce :: ICExp o
ce _ _ -> do
      let (Clos _ (Meta m :: UId o
m)) = ICExp o
ce
      [RefInfo o]
infos <- UId o -> IO [RefInfo o]
forall a blk. Metavar a blk -> IO [blk]
extractblkinfos UId o
m
      if (RefInfo o -> Bool) -> [RefInfo o] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\info :: RefInfo o
info -> case RefInfo o
info of {RINotConstructor -> Bool
True; _ -> Bool
False}) [RefInfo o]
infos then do
        Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       else
        Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      -- return False -- return True -- ?? removes completeness - Yes, in DavidW1.additionRight
     HNDone{} -> do
      MyMB (HNExp o) o
res <- ICExp o -> EE (MyMB (HNExp o) o)
forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
ce
      case MyMB (HNExp o) o
res of
       NotB hne :: HNExp o
hne -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne of
        HNApp (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
          Constructor{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Blocked m :: Metavar b (RefInfo o)
m _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- not necessary to do check here because already done by hnn (!! if it's known that m stands for an eliminator then it cannot be constructor so True instead)
       Failed _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor a :: ICExp o
a =
 MetaEnv (MB (HNRes o) (RefInfo o))
-> (HNRes o -> EE (MB Bool (RefInfo o)))
-> EE (MB Bool (RefInfo o))
forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
True ICExp o
a ICArgList o
forall o. ICArgList o
CALNil []) ((HNRes o -> EE (MB Bool (RefInfo o))) -> EE (MB Bool (RefInfo o)))
-> (HNRes o -> EE (MB Bool (RefInfo o)))
-> EE (MB Bool (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \res :: HNRes o
res -> case HNRes o
res of
  HNMeta ce :: ICExp o
ce _ _ -> do
    let (Clos _ (Meta m :: UId o
m)) = ICExp o
ce
    [RefInfo o]
infos <- UId o -> IO [RefInfo o]
forall a blk. Metavar a blk -> IO [blk]
extractblkinfos UId o
m
    if (RefInfo o -> Bool) -> [RefInfo o] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\info :: RefInfo o
info -> case RefInfo o
info of {RINotConstructor -> Bool
True; _ -> Bool
False}) [RefInfo o]
infos then do
      Bool
b <- ICExp o -> ICArgList o -> IO Bool
forall o. ICExp o -> ICArgList o -> IO Bool
iotapossmeta ICExp o
ce ICArgList o
forall o. ICArgList o
CALNil
      Bool -> EE (MB Bool (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret (Bool -> EE (MB Bool (RefInfo o)))
-> Bool -> EE (MB Bool (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b
     else
      Bool -> EE (MB Bool (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Bool
False
  HNDone{} -> Bool -> EE (MB Bool (RefInfo o))
forall a blk. a -> MetaEnv (MB a blk)
mbret Bool
False

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

calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState cs :: EqReasoningConsts o
cs = EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone
 where
  f :: EqReasoningState -> MExp o -> EE (MyPB o)
f s :: EqReasoningState
s 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, RefInfo o -> Maybe (RefInfo o)
forall a. a -> Maybe a
Just (EqReasoningState -> RefInfo o
forall o. EqReasoningState -> RefInfo o
RIEqRState EqReasoningState
s)) 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 _ _ (Const c :: ConstRef o
c) args :: MArgList o
args -> case () of
     _ | ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcBegin EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSChain] MArgList o
args
     _ | ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcStep EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSPrf1, EqReasoningState
EqRSChain] MArgList o
args
     _ | ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcSym EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSPrf2] MArgList o
args
     _ | ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcCong EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSPrf3] MArgList o
args
     _ -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
args
    App _ _ (Var{}) args :: MArgList o
args -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
args
    Lam _ (Abs _ b :: MExp o
b) -> EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone MExp o
b
    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 (EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone MExp o
it) (EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone 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


  fs :: [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs ss :: [EqReasoningState]
ss args :: MArgList o
args =
   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
args ((ArgList o -> EE (MyPB o)) -> EE (MyPB o))
-> (ArgList o -> EE (MyPB o)) -> EE (MyPB o)
forall a b. (a -> b) -> a -> b
$ \args :: ArgList o
args -> case ([EqReasoningState]
ss, ArgList o
args) of
    (_, ALNil) -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
    (s :: EqReasoningState
s : ss :: [EqReasoningState]
ss, ALCons _ a :: MExp o
a 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 (EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
s MExp o
a) ([EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState]
ss MArgList o
args)
    ([], ALCons _ a :: MExp o
a 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 (EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone MExp o
a) ([EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
args)

    (_, 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 ([EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
eas) ([EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
as) -- when eqr-hint is given manually, ss can be non-empty here


    (_ : ss :: [EqReasoningState]
ss, ALConPar args :: MArgList o
args) -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState]
ss MArgList o
args
    ([], ALConPar args :: MArgList o
args) -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
args

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

pickid :: MId -> MId -> MId
pickid :: MId -> MId -> MId
pickid mid1 :: MId
mid1@(Id _) _ = MId
mid1
pickid _ mid2 :: MId
mid2 = MId
mid2

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

tcSearch :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch isdep :: Bool
isdep ctx :: Ctx o
ctx typ :: CExp o
typ trm :: MExp o
trm = 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)
forall o. MExp o -> EE (MyPB o)
checkeliminand MExp o
trm)
                              (Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp Bool
isdep Ctx o
ctx CExp o
typ MExp o
trm)

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