module Agda.Auto.Typecheck where

import Data.IORef

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 Bool
isdep Ctx o
ctx typ :: CExp o
typ@(TrBr [MExp o]
typtrs ityp :: ICExp o
ityp@(Clos [CAction o]
_ MExp o
itypexp)) 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
$ \(HNExp o
hntyp, 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
$ \Exp o
trm -> case Exp o
trm of
   App Maybe (UId o)
_ OKHandle (RefInfo o)
okh Elr o
elr 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 String
"tcExp, dep terms should be eta-long"
    HNExp' o
_ -> do
     (CExp o
ityp, EE (MyPB o) -> EE (MyPB o)
sc) <- case Elr o
elr of
              Var 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
+ Nat
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 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), \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. TravWith 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 Nat
0
              Const 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
>>= \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 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; DeclCont o
_ -> 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
$ \CExp o
ityp MExp o
_ -> 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 Hiding
hid (Abs MId
id1 MExp o
b) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNPi Hiding
hid2 Bool
_ ICExp o
it (Abs MId
id2 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
t ICExp o
it) (MId, CExp o) -> Ctx o -> Ctx o
forall a. a -> [a] -> [a]
: Ctx o
ctx) (ICExp o -> CExp o
t ICExp o
ot) MExp o
b
    HNExp' o
_ -> 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
"tcExp, type of lam should be fun or pi (and same hid)"
   Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
id MExp o
ot) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNSort 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. TravWith a blk => a -> Term blk
Term Ctx o
ctx, MExp o -> Term (RefInfo o)
forall blk a. TravWith 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)
    HNExp' o
_ -> 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
"tcExp, type of pi should be set"
   Sort (Set Nat
i) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNSort Sort
s2 -> case Sort
s2 of
     Set 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 String
"tcExp, type of set should be larger set"

     Sort
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__)

     Sort
Type -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
    HNExp' o
_ -> 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
"tcExp, type of set should be set"

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

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

   AbsurdLambda Hiding
hid -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hntyp of
    HNPi Hiding
hid2 Bool
_ ICExp o
it Abs (ICExp o)
_ | 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
$ \Maybe (ICArgList o, [ConstRef o])
res -> case Maybe (ICArgList o, [ConstRef o])
res of
      Just (ICArgList o
indeces, [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 (\EE (MyPB o)
p 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
      Maybe (ICArgList o, [ConstRef o])
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 String
"tcExp, absurd lambda, datatype needed"
    HNExp' o
_ -> 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
"tcExp, type of absurd lam should be fun or pi (and same hid)"


  where
   t :: ICExp o -> CExp o
t = [MExp o] -> ICExp o -> CExp 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 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
$ \HNExp o
hnt -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnt of
  HNApp (Const ConstRef o
c) ICArgList o
args -> do
   ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
   case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
    Datatype [ConstRef o]
cons [ConstRef o]
_ -> 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
    DeclCont o
_ -> 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
  HNExp' o
_ -> 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 ICArgList o
args 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 (-Nat
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
$ \HNExp o
hnot ->
  case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnot of
   HNApp Elr o
_ 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 (\[(Nat, HNExp o)]
_ -> 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
"not unequal") []
   HNExp' o
_ -> 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
"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 ICArgList o
es1 ICArgList o
es2 [(Nat, HNExp o)] -> EE (MyPB o)
cont [(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
$ \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
$ \HNArgList o
hnes2 ->
 case (HNArgList o
hnes1, HNArgList o
hnes2) of
  (HNALCons Hiding
_ ICExp o
e1 ICArgList o
es1, HNALCons Hiding
_ ICExp o
e2 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 ICArgList o
es1, HNALConPar 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

  (HNArgList o, HNArgList o)
_ -> [(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 ICExp o
e1 ICExp o
e2 [(Nat, HNExp o)] -> EE (MyPB o)
cont [(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
$ \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
$ \HNExp o
hne2 ->
  case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne2 of
   HNApp (Var Nat
v2) ICArgList o
es2 | Nat
v2 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
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
$ \HNArgList o
hnes2 -> case HNArgList o
hnes2 of
     HNArgList o
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
       Maybe (HNExp o)
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 HNExp o
hne2' -> HNExp o -> HNExp 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 -> HNExp o -> EE (MyPB o)
cc HNExp o
hne1 HNExp o
hne2
 where
  cc :: HNExp o -> HNExp o -> EE (MyPB o)
cc HNExp o
hne1 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 (Const ConstRef o
c1) ICArgList o
es1, HNApp (Const ConstRef o
c2) 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
     (DeclCont o, DeclCont o)
_ -> [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2
   (HNExp' o, HNExp' o)
_ -> [(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 Nat
v 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
$ \HNExp o
hnt ->
 case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnt of
  HNPi Hiding
_ Bool
_ ICExp o
_ (Abs MId
_ 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
- Nat
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
_ -> 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 Nat
ndfv Bool
isdep Ctx o
ctx ityp :: CExp o
ityp@(TrBr [MExp o]
ityptrs ICExp o
iityp) MArgList o
args MExp o
elimtrm Bool
isconstructor 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
$ \ArgList o
args' -> case ArgList o
args' of
 ArgList o
ALNil -> CExp o -> MExp o -> EE (MyPB o)
cont CExp o
ityp MExp o
elimtrm
 ALCons Hiding
hid MExp o
a 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
$ \HNExp o
hnityp -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnityp of
   HNPi Hiding
hid2 Bool
possdep ICExp o
it (Abs MId
_ ICExp o
ot)
     | Nat
ndfv Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
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 ([MExp o -> Term (RefInfo o)
forall blk a. TravWith a blk => a -> Term blk
Term MExp o
a | Bool
possdep] [Term (RefInfo o)] -> [Term (RefInfo o)] -> [Term (RefInfo o)]
forall a. [a] -> [a] -> [a]
++ [Ctx o -> Term (RefInfo o)
forall blk a. TravWith a blk => a -> Term blk
Term Ctx o
ctx, [MExp o] -> Term (RefInfo o)
forall blk a. TravWith a blk => a -> Term blk
Term [MExp o]
ityptrs]))
        (if Nat
ndfv Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
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
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
- Nat
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
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)
   HNExp' o
_ -> 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
"tcargs, inf type should be fun or pi (and same hid)"


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

 ALProj MArgList o
preas MM (ConstRef o) (RefInfo o)
projidx Hiding
hid 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
$ \HNExp o
hnityp -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnityp of
   HNApp (Const ConstRef o
dd) ICArgList o
_ -> 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 [ConstRef o]
_ [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
$
      \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 [MExp o]
ityp2trs ICExp o
iityp2) MExp o
elimtrm2 ->
         case ICExp o
iityp2 of
          Clos [CAction o]
_ (NotM (Pi Maybe (UId o)
_ Hiding
_ Bool
_ (NotM (App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
dd2) MArgList o
_)) Abs (MExp o)
_)) | 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
$ \HNExp o
hnityp2 -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnityp2 of
            HNPi Hiding
hid2 Bool
possdep ICExp o
it (Abs MId
_ 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 Nat
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
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)
            HNExp' o
_ -> 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
"proj function type is not a Pi"
          ICExp o
_ -> 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
"proj function type is not correct"
     DeclCont o
_ -> 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
"proj, not a datatype"
   HNExp' o
_ -> 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
"proj, not a const app"


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

 where
  t :: ICExp o -> CExp o
t = [MExp o] -> ICExp o -> CExp 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 Hiding
hid MExp o
a (NotM (App Maybe (UId o)
uid OKHandle (RefInfo o)
okh Elr o
elr 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 ArgList o
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 Hiding
hid MExp o
a 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
_                        = MArgList o
forall a. HasCallStack => a
__IMPOSSIBLE__
addend Hiding
_ MExp o
_ MM (Exp o) blk
_ = MM (Exp o) blk
forall a. HasCallStack => a
__IMPOSSIBLE__

copyarg :: MExp o -> Bool
copyarg :: MExp o -> Bool
copyarg MExp o
_ = 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 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
$ \(HNExp o
hne, HNNBlks o
_) -> 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 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 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
$ \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
$ \Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
   Right HNNBlks o
_ -> (HNExp o, Bool) -> EE (MyMB (HNExp o, Bool) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNExp o
hne, Bool
False)
   Left (ICExp o
e, 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
$ \(HNExp o
hne, HNNBlks o
_) -> (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' ICExp o
e 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
$ \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
$ \Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
   Right 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 (ICExp o
e, 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 ICExp o
e 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
$ \HNRes o
res -> case HNRes o
res of
            HNDone Maybe (UId o)
_ 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 Bool
haltmeta = ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)
loop
 where
  loop :: ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)
loop ce :: ICExp o
ce@(Clos [CAction o]
cl MM (Exp o) (RefInfo o)
e) ICArgList o
cargs [Maybe (UId o)]
seenuids =
   (if Bool
haltmeta then MM (Exp o) (RefInfo o)
-> EE (MyMB (HNRes o) o)
-> (Exp o -> EE (MyMB (HNRes o) o))
-> EE (MyMB (HNRes o) 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 -> EE (MyMB (HNRes o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> EE (MyMB (HNRes o) o))
-> HNRes o -> EE (MyMB (HNRes o) 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 -> EE (MyMB (HNRes o) o)) -> EE (MyMB (HNRes o) 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 -> EE (MyMB (HNRes o) o)) -> EE (MyMB (HNRes o) o))
-> (Exp o -> EE (MyMB (HNRes o) o)) -> EE (MyMB (HNRes o) o)
forall a b. (a -> b) -> a -> b
$
   \Exp o
ee -> case Exp o
ee of
    App Maybe (UId o)
uid OKHandle (RefInfo o)
okh Elr o
elr 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 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 Nat
v' -> HNRes o -> EE (MyMB (HNRes o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> EE (MyMB (HNRes o) o))
-> HNRes o -> EE (MyMB (HNRes o) 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 ICExp o
f -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) 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 ConstRef o
_ -> HNRes o -> EE (MyMB (HNRes o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> EE (MyMB (HNRes o) o))
-> HNRes o -> EE (MyMB (HNRes o) 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 Hiding
hid (Abs MId
id MM (Exp o) (RefInfo o)
b) ->
     MetaEnv (MB (HNArgList o) (RefInfo o))
-> (HNArgList o -> EE (MyMB (HNRes o) o)) -> EE (MyMB (HNRes 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
cargs) ((HNArgList o -> EE (MyMB (HNRes o) o)) -> EE (MyMB (HNRes o) o))
-> (HNArgList o -> EE (MyMB (HNRes o) o)) -> EE (MyMB (HNRes o) o)
forall a b. (a -> b) -> a -> b
$ \HNArgList o
hncargs -> case HNArgList o
hncargs of
      HNArgList o
HNALNil -> HNRes o -> EE (MyMB (HNRes o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> EE (MyMB (HNRes o) o))
-> HNRes o -> EE (MyMB (HNRes o) 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 Hiding
_ ICExp o
arg ICArgList o
cargs' -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) 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{} -> EE (MyMB (HNRes o) o)
forall a. HasCallStack => a
__IMPOSSIBLE__

    Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MM (Exp o) (RefInfo o)
it (Abs MId
id MM (Exp o) (RefInfo o)
ot) ->
       ICArgList o -> EE (MyMB (HNRes o) o) -> EE (MyMB (HNRes o) o)
forall o b.
ICArgList o
-> MetaEnv (MB b (RefInfo o)) -> MetaEnv (MB b (RefInfo o))
checkNoArgs ICArgList o
cargs (EE (MyMB (HNRes o) o) -> EE (MyMB (HNRes o) o))
-> EE (MyMB (HNRes o) o) -> EE (MyMB (HNRes o) o)
forall a b. (a -> b) -> a -> b
$ HNRes o -> EE (MyMB (HNRes o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret (HNRes o -> EE (MyMB (HNRes o) o))
-> HNRes o -> EE (MyMB (HNRes o) 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 Sort
s -> ICArgList o -> EE (MyMB (HNRes o) o) -> EE (MyMB (HNRes o) o)
forall o b.
ICArgList o
-> MetaEnv (MB b (RefInfo o)) -> MetaEnv (MB b (RefInfo o))
checkNoArgs ICArgList o
cargs (EE (MyMB (HNRes o) o) -> EE (MyMB (HNRes o) o))
-> EE (MyMB (HNRes o) o) -> EE (MyMB (HNRes o) o)
forall a b. (a -> b) -> a -> b
$ HNRes o -> EE (MyMB (HNRes o) o)
forall a blk. a -> MetaEnv (MB a blk)
mbret
            (HNRes o -> EE (MyMB (HNRes o) o))
-> HNRes o -> EE (MyMB (HNRes o) 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 -> EE (MyMB (HNRes o) o)
forall a blk. String -> MetaEnv (MB a blk)
mbfailed String
"hnc: encountered absurdlambda"


   where expmeta :: Maybe (UId o)
expmeta = case MM (Exp o) (RefInfo o)
e of {Meta UId o
m -> UId o -> Maybe (UId o)
forall a. a -> Maybe a
Just UId o
m; NotM Exp o
_ -> Maybe (UId o)
forall a. Maybe a
Nothing}
  checkNoArgs :: ICArgList o
-> MetaEnv (MB b (RefInfo o)) -> MetaEnv (MB b (RefInfo o))
checkNoArgs ICArgList o
cargs 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
$ \HNArgList o
hncargs -> case HNArgList o
hncargs of
    HNArgList o
HNALNil -> MetaEnv (MB b (RefInfo o))
c
    HNALCons{} -> String -> MetaEnv (MB b (RefInfo o))
forall a blk. String -> MetaEnv (MB a blk)
mbfailed String
"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 ICArgList o
args =
 case ICArgList o
args of
  ICArgList o
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 [CAction o]
cl MArgList o
args) 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
$ \ArgList o
args -> case ArgList o
args of
    ArgList o
ALNil -> ICArgList o -> EE (MyMB (HNArgList o) o)
forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args2
    ALCons Hiding
hid MExp o
arg 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 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 Nat
0 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 Nat
narg 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
$ \HNArgList o
hnargs -> case HNArgList o
hnargs of
  HNArgList o
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 Hiding
_ ICExp o
arg 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
- Nat
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
$ \Maybe ([ICExp o], ICArgList o)
res -> case Maybe ([ICExp o], ICArgList o)
res of
    Maybe ([ICExp o], ICArgList o)
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 ([ICExp o]
pargs, 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 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
$ \HNArgList o
hnargs -> case HNArgList o
hnargs of
  HNArgList o
HNALNil -> [ICExp o] -> EE (MyMB [ICExp o] o)
forall a blk. a -> MetaEnv (MB a blk)
mbret []
  HNALCons Hiding
_ ICExp o
arg 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
$ \[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 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
$ \[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 Bool
smartcheck HNExp o
e = case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
e of
 HNApp (Const ConstRef o
c) ICArgList o
args -> do
  ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
  case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
   Def Nat
narg [Clause o]
cls Maybe Nat
_ Maybe Nat
_ ->
    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
$ \Maybe ([ICExp o], ICArgList o)
res -> case Maybe ([ICExp o], ICArgList o)
res of
     Maybe ([ICExp o], ICArgList o)
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 ([ICExp o]
pargs, 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
$ \Either (ICExp o) (HNNBlks o)
res -> case Either (ICExp o) (HNNBlks o)
res of
       Right 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 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)
   DeclCont o
_ -> 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
 HNExp' o
_ -> 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 [] [PEval o]
_ = 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 (Clause o
rule:[Clause o]
rules') [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
$ \Either (Either [PEval o] (HNNBlks o)) (ICExp o)
x -> case Either (Either [PEval o] (HNNBlks o)) (ICExp o)
x of
   Left (Left [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 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 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 ([Pat o]
pats, MExp o
rhs) [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
$ \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 ([PEval o]
_, [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 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 (Pat o
p:[Pat o]
ps') (PEval o
a:[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
$ \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 (PEval o
hna, [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
$ \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 ([PEval o]
hnas, [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 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 [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 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 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 [Pat o]
_ [PEval o]
_ = String
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
forall a blk. String -> MetaEnv (MB a blk)
mbfailed String
"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 ConstRef o
c [Pat o]
pas) PEval o
a =
  case PEval o
a of
   PENo 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
$ \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
$ \(HNExp o
hna, HNNBlks o
blks) -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hna of
       HNApp (Const ConstRef o
c') 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
$ \[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
$ \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 ([PEval o]
hnas, [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 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 [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 String
"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
$ \[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')))
          DeclCont 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 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))
       HNExp' 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 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 ICExp o
a ConstRef o
c' [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
$ \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 ([PEval o]
hnas, [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 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 [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 String
"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 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 ICExp o
a' ConstRef o
_ [PEval 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 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 Pat o
PatExp 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 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
$ \Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
  Left (ICExp o, ICArgList o)
_ -> 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
"iota step possible contrary to assumed"
  Right HNNBlks o
_ -> 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 ConstRef o
c MArgList o
args = do
  ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
  case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
    Def Nat
_ [([Pat o]
pats, MExp o
_)] Maybe Nat
_ Maybe Nat
_ -> 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
    DeclCont o
_ -> 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' Bool
ineq lhs :: CExp o
lhs@(TrBr [MExp o]
trs1 ICExp o
e1) rhs :: CExp o
rhs@(TrBr [MExp o]
trs2 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 Bool
ineq ICExp o
e1 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 ICExp o
e1 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
$ \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
$ \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 Bool
semifok ICExp o
e ICArgList o
as [Maybe (UId o)]
seenuids 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
$ \HNRes o
res ->
      case HNRes o
res of
       HNDone Maybe (UId o)
mexpmeta 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 [CAction o]
cl MExp o
m) ICArgList o
cargs [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
$ \HNRes o
res ->
           case HNRes o
res of
            HNDone Maybe (UId o)
mexpmeta 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 Bool
semifok Maybe (UId o)
mexpmeta HNExp o
hne 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)
      (\MM b (RefInfo o)
m -> do
        let sf :: Bool
sf = 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))
      )
      (\Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
        Right HNNBlks o
_ -> 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 (ICExp o
e, 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 CMode o
res1 CMode o
res2 =
     case (CMode o
res1, CMode o
res2) of
      (CMRigid Maybe (UId o)
mexpmeta1 HNExp o
hne1, CMRigid Maybe (UId o)
mexpmeta2 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 MM b (RefInfo o)
m1 (CMFBlocked Maybe (UId o)
mexpmeta1 HNExp o
hne1), CMode o
_) -> 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
$ \CMode o
res1 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
      (CMode o
_, CMFlex MM b (RefInfo o)
m2 (CMFBlocked Maybe (UId o)
mexpmeta2 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
$ \CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
      (CMRigid Maybe (UId o)
mexpmeta1 HNExp o
hne1, CMFlex MM b (RefInfo o)
_ 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 MM b (RefInfo o)
_ CMFlex o
fl1, CMRigid Maybe (UId o)
mexpmeta2 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 MM b (RefInfo o)
m1 CMFlex o
fl1, CMFlex MM b (RefInfo o)
m2 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
$ \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
$ \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 ICExp o
ce ICArgList o
cargs [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 Maybe (UId o)
mexpmeta 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 Maybe (UId o)
_ 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 Bool
semif Maybe (UId o)
mexpmeta HNExp o
hne 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. TravWith a blk => a -> Term blk
Term CExp o
lhs, CExp o -> Term (RefInfo o)
forall blk a. TravWith 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 Bool
semif HNExp o
hne 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
$ \Either (ICExp o, ICArgList o) (HNNBlks o)
res -> case Either (ICExp o, ICArgList o) (HNNBlks o)
res of
      Right HNNBlks o
_ -> 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
"no iota step possible, contrary to assumed"
      Left (ICExp o
e, 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 Bool
oppis1 Maybe (UId o)
oppmexpmeta HNExp o
opphne CMFlex o
res =
     let iter :: CMode o -> EE (MyPB o)
iter 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 ICExp o
ce ICArgList o
cargs [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
$ \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 Maybe (UId o)
mexpmeta 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 [CAction o]
cl MExp o
m) ICArgList o
cargs [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
$ \Exp o
_ ->
         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
$ \HNRes o
res -> case HNRes o
res of
          HNDone Maybe (UId o)
mexpmeta 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. TravWith a blk => a -> Term blk
Term CExp o
lhs, CExp o -> Term (RefInfo o)
forall blk a. TravWith 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 ICExp o
ce ICArgList o
cargs [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 Maybe (UId o)
_ 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 Bool
ineq Maybe (UId o)
mexpmeta1 HNExp o
hne1 Maybe (UId o)
mexpmeta2 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 Elr o
elr1 ICArgList o
args1, HNApp Elr o
elr2 ICArgList o
args2) ->
       let ce :: Maybe String
ce = case (Elr o
elr1, Elr o
elr2) of
                 (Var Nat
v1, Var 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 String
"comphn, elr, vars not equal"
                 (Const ConstRef o
c1, Const 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 String
"comphn, elr, consts not equal"
                 (Elr o
_, Elr o
_) -> String -> Maybe String
forall a. a -> Maybe a
Just String
"comphn, elrs not equal"
       in case Maybe String
ce of
            Maybe String
Nothing -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1 ICArgList o
args2
            Just 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 Hiding
hid1 (Abs MId
id1 ICExp o
b1), HNLam Hiding
hid2 (Abs MId
id2 ICExp o
b2)) -> Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp Bool
False ICExp o
b1 ICExp o
b2
      (HNLam Hiding
_ (Abs MId
_ ICExp o
b1), HNApp Elr o
elr2 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
$ \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 Nat
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 Nat
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 Nat
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
$ \CMode o
res2 -> CMode o -> CMode o -> EE (MyPB o)
g CMode o
res1 CMode o
res2
      (HNApp Elr o
elr1 ICArgList o
args1, HNLam Hiding
_ (Abs MId
_ 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 Nat
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 Nat
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 Nat
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
$ \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
$ \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 Hiding
hid1 Bool
_ ICExp o
it1 (Abs MId
id1 ICExp o
ot1), HNPi Hiding
hid2 Bool
_ ICExp o
it2 (Abs MId
id2 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. TravWith a blk => a -> Term blk
Term [MExp o]
trs1, [MExp o] -> Term (RefInfo o)
forall blk a. TravWith 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 Sort
s1, HNSort 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 Nat
i1, Set 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 String
"comphn, set levels not matching"
        (Set Nat
_, Sort
UnknownSort) -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Sort
UnknownSort, Set Nat
_) -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Sort
UnknownSort, Sort
UnknownSort) -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Sort
Type, Set Nat
_) | Bool
ineq -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Sort
Type, Sort
UnknownSort) | Bool
ineq -> Prop (RefInfo o)
forall blk. Prop blk
OK
        (Sort, Sort)
_ -> Prop (RefInfo o)
forall a. HasCallStack => a
__IMPOSSIBLE__
      (HNApp (Const ConstRef o
c1) ICArgList o
_, HNExp' o
_) -> case Maybe (UId o)
mexpmeta2 of
       Maybe (UId o)
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 String
"comphn, not equal (2)"
       Just 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 String
"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)
      (HNExp' o
_, HNApp (Const ConstRef o
c2) ICArgList o
_) -> case Maybe (UId o)
mexpmeta1 of
       Maybe (UId o)
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 String
"comphn, not equal (3)"
       Just 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 String
"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)
      (HNExp' o
_, HNExp' o
_) -> 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
"comphn, not equal"

    compargs :: ICArgList o -> ICArgList o -> EE (MyPB o)
    compargs :: ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1 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
$ \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
$ \HNArgList o
hnargs2 ->
     case (HNArgList o
hnargs1, HNArgList o
hnargs2) of
      (HNArgList o
HNALNil, HNArgList o
HNALNil) -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
      (HNALCons Hiding
hid1 ICExp o
arg1 ICArgList o
args1b, HNALCons Hiding
hid2 ICExp o
arg2 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. TravWith a blk => a -> Term blk
Term [MExp o]
trs1, [MExp o] -> Term (RefInfo o)
forall blk a. TravWith 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 ICArgList o
args1b, HNALCons Hiding
_ ICExp o
_ ICArgList o
args2b) -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1b ICArgList o
args2b
      (HNALCons Hiding
_ ICExp o
_ ICArgList o
args1b, HNALConPar ICArgList o
args2b) -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1b ICArgList o
args2b
      (HNALConPar ICArgList o
args1', HNALConPar ICArgList o
args2') -> ICArgList o -> ICArgList o -> EE (MyPB o)
compargs ICArgList o
args1' ICArgList o
args2'

      (HNArgList o
_, HNArgList o
_) -> 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
$ String
"comphnargs, not equal"


    boringExp :: ICExp o -> EE Bool
    boringExp :: ICExp o -> IO Bool
boringExp (Clos [CAction o]
cl 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 Exp o
e -> case Exp o
e of
       App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var Nat
v) 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 ArgList o
as -> case ArgList o
as of
          ArgList o
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 Nat
_ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
           Right 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

       Exp o
_ -> 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 [CAction o]
cl = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> IO [Bool] -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 ICExp o
e) = ICExp o -> IO Bool
boringExp ICExp o
e
           f CAction o
Skip = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
           f (Weak Nat
_) = 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 ICArgList o
CALNil = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    boringArgs (CALConcat (Clos [CAction o]
cl MArgList o
as) 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 [CAction o]
cl 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 ArgList o
as -> case ArgList o
as of
         ArgList o
ALNil -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
         ALCons Hiding
_ MExp o
a 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 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 [UId o]
uids [Elr o]
used 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
$ \Exp o
e -> case Exp o
e of
    App Maybe (UId o)
uid OKHandle (RefInfo o)
_ elr :: Elr o
elr@(Var{}) 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 Maybe (UId o)
uid OKHandle (RefInfo o)
_ elr :: Elr o
elr@(Const ConstRef o
c) MArgList o
args -> do
     ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
     case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
      Def Nat
_ [Clause o]
_ (Just Nat
i) Maybe Nat
_ -> 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 a
i MArgList o
as = BlkInfo (RefInfo o)
-> MArgList o
-> (ArgList o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, Maybe (RefInfo o)
forall a. Maybe a
Nothing) MArgList o
as ((ArgList o -> MetaEnv (PB (RefInfo o)))
 -> MetaEnv (PB (RefInfo o)))
-> (ArgList o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
                  ArgList o
ALNil -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
                  ALCons Hiding
_ MExp o
a MArgList o
as -> case a
i of
                   a
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
$ \Exp o
_ ->
                         Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
                   a
_ -> a -> MArgList o -> MetaEnv (PB (RefInfo o))
g (a
i a -> a -> a
forall a. Num a => a -> a -> a
- a
1) MArgList o
as

                  ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ MArgList o
as -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK


                  ALConPar MArgList o
as -> case a
i of
                   a
0 -> MetaEnv (PB (RefInfo o))
forall a. HasCallStack => a
__IMPOSSIBLE__
                   a
_ -> a -> MArgList o -> MetaEnv (PB (RefInfo o))
g (a
i a -> a -> a
forall a. Num a => a -> a -> a
- a
1) MArgList o
as

      DeclCont o
_ -> [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 Hiding
_ (Abs MId
_ 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 Maybe (UId o)
uid Hiding
_ Bool
_ MExp o
e1 (Abs MId
_ 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 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 [UId o]
uids [Elr o]
used MArgList o
as =
   BlkInfo (RefInfo o)
-> MArgList o
-> (ArgList o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, Maybe (RefInfo o)
forall a. Maybe a
Nothing) MArgList o
as ((ArgList o -> MetaEnv (PB (RefInfo o)))
 -> MetaEnv (PB (RefInfo o)))
-> (ArgList o -> MetaEnv (PB (RefInfo o)))
-> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
    ArgList o
ALNil -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
    ALCons Hiding
_ MExp o
a MArgList o
as -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
-> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ MetaEnv (PB (RefInfo o))
-> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition ([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 MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ MArgList o
as -> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall blk. Prop blk -> MetaEnv (PB blk)
mpret (Prop (RefInfo o) -> MetaEnv (PB (RefInfo o)))
-> Prop (RefInfo o) -> MetaEnv (PB (RefInfo o))
forall a b. (a -> b) -> a -> b
$ MetaEnv (PB (RefInfo o))
-> MetaEnv (PB (RefInfo o)) -> Prop (RefInfo o)
forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition ([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 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 (\Elr o
x -> case Elr o
x of {Var Nat
v -> Nat -> Elr o
forall o. Nat -> Elr o
Var (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1); Const{} -> Elr o
x})
  adduid :: Maybe a -> [a] -> [a]
adduid (Just a
uid) [a]
uids = a
uid a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
uids
  adduid Maybe a
Nothing [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 Bool
_ Prio
_ IO (PB (RefInfo o))
mainalt IO (PB (RefInfo o))
_ = 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 [CAction o]
cl MExp o
_) 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
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
xs Bool -> Bool -> Bool
&& Bool
y)
 where
  ncaction :: CAction o -> IO Bool
ncaction (Sub ICExp o
ce) = ICExp o -> IO Bool
forall o. ICExp o -> IO Bool
nonconstructor ICExp o
ce
  ncaction CAction o
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 ICArgList o
CALNil = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  nccargs (CALConcat (Clos [CAction o]
cl MArgList o
margs) 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 [CAction o]
cl (Meta 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
    Maybe (ArgList o)
Nothing -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just ArgList o
x -> [CAction o] -> ArgList o -> IO Bool
ncargs [CAction o]
cl ArgList o
x
  ncmargs [CAction o]
cl (NotM ArgList o
args) = [CAction o] -> ArgList o -> IO Bool
ncargs [CAction o]
cl ArgList o
args
  ncargs :: [CAction o] -> ArgList o -> IO Bool
ncargs [CAction o]
cl ArgList o
ALNil = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ncargs [CAction o]
cl (ALCons Hiding
_ MExp o
a 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 [CAction o]
_ (ALProj{}) = IO Bool
forall a. HasCallStack => a
__IMPOSSIBLE__


  ncargs [CAction o]
cl (ALConPar 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 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 HNRes o
res -> case HNRes o
res of
     HNMeta ICExp o
ce ICArgList o
_ [Maybe (UId o)]
_ -> do
      let (Clos [CAction o]
_ (Meta 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 (\RefInfo o
info -> case RefInfo o
info of {RefInfo o
RINotConstructor -> Bool
True; RefInfo o
_ -> 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 HNExp o
hne -> case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne of
        HNApp (Const ConstRef o
c) ICArgList o
_ -> do
         ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
         case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
          Constructor{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          DeclCont o
_ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        HNExp' o
_ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Blocked Metavar b (RefInfo o)
m EE (MyMB (HNExp o) o)
_ -> 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 String
_ -> 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 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
$ \HNRes o
res -> case HNRes o
res of
  HNMeta ICExp o
ce ICArgList o
_ [Maybe (UId o)]
_ -> do
    let (Clos [CAction o]
_ (Meta 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 (\RefInfo o
info -> case RefInfo o
info of {RefInfo o
RINotConstructor -> Bool
True; RefInfo o
_ -> 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 EqReasoningConsts o
cs = EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone
 where
  f :: EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
s 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
$ \Exp o
e -> case Exp o
e of
    App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Const ConstRef o
c) 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 Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var{}) MArgList o
args -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [] MArgList o
args
    Lam Hiding
_ (Abs MId
_ MExp o
b) -> EqReasoningState -> MExp o -> EE (MyPB o)
f EqReasoningState
EqRSNone MExp o
b
    Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ 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 [EqReasoningState]
ss 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
$ \ArgList o
args -> case ([EqReasoningState]
ss, ArgList o
args) of
    ([EqReasoningState]
_, ArgList o
ALNil) -> Prop (RefInfo o) -> EE (MyPB o)
forall blk. Prop blk -> MetaEnv (PB blk)
mpret Prop (RefInfo o)
forall blk. Prop blk
OK
    (EqReasoningState
s : [EqReasoningState]
ss, ALCons Hiding
_ MExp o
a 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 Hiding
_ MExp o
a 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)

    ([EqReasoningState]
_, ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ 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


    (EqReasoningState
_ : [EqReasoningState]
ss, ALConPar MArgList o
args) -> [EqReasoningState] -> MArgList o -> EE (MyPB o)
fs [EqReasoningState]
ss MArgList o
args
    ([], ALConPar 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 String
_) MId
_ = MId
mid1
pickid MId
_ 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 Bool
isdep Ctx o
ctx CExp o
typ 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)

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