{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.Auto.Typecheck where

import Prelude hiding ((!!))

import Data.IORef

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

import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.Maybe

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

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

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


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

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

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

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

   Sort Sort
UnknownSort -> forall a. HasCallStack => a
__IMPOSSIBLE__

   Sort Sort
Type -> forall a. HasCallStack => a
__IMPOSSIBLE__

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


  where
   t :: Clos (MExp o) o -> CExp o
t = 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 :: forall o.
ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
getDatatype ICExp o
t =
 forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
t) forall a b. (a -> b) -> a -> b
$ \HNExp o
hnt -> case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnt of
  HNApp (Const ConstRef o
c) ICArgList o
args -> do
   ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
   case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
    Datatype [ConstRef o]
cons [ConstRef o]
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (ICArgList o
args, [ConstRef o]
cons) -- ?? check that lenth args corresponds to type of datatype
    DeclCont o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
  HNExp' o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing

constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)
constructorImpossible :: forall o. ICArgList o -> ConstRef o -> EE (MyPB o)
constructorImpossible ICArgList o
args ConstRef o
c = do
 ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
 forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda forall a. Maybe a
Nothing (forall o. Nat -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi (-Nat
1) (forall a o. [CAction o] -> a -> Clos a o
Clos [] forall a b. (a -> b) -> a -> b
$ forall o. ConstDef o -> MExp o
cdtype ConstDef o
cd)) forall a b. (a -> b) -> a -> b
$ \HNExp o
hnot ->
  case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnot of
   HNApp Elr o
_ ICArgList o
args2 -> 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)]
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error String
"not unequal") []
   HNExp' o
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ 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 :: 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 =
 forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda forall a. Maybe a
Nothing (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
es1) forall a b. (a -> b) -> a -> b
$ \HNArgList o
hnes1 ->
 forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda forall a. Maybe a
Nothing (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
es2) 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) -> 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 (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) -> 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 :: 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 [(Nat, HNExp o)] -> EE (MyPB o)
cont [(Nat, HNExp o)]
unifier2 =
 forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda forall a. Maybe a
Nothing (forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
e1) forall a b. (a -> b) -> a -> b
$ \HNExp o
hne1 ->
 forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda forall a. Maybe a
Nothing (forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
e2) forall a b. (a -> b) -> a -> b
$ \HNExp o
hne2 ->
  case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne2 of
   HNApp (Var Nat
v2) ICArgList o
es2 | Nat
v2 forall a. Ord a => a -> a -> Bool
< Nat
0 ->
    forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioAbsurdLambda forall a. Maybe a
Nothing (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
es2) forall a b. (a -> b) -> a -> b
$ \HNArgList o
hnes2 -> case HNArgList o
hnes2 of
     HNArgList o
HNALNil ->
      case 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) 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{} -> 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 (forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne1, 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 <- forall a. IORef a -> IO a
readIORef ConstRef o
c1
    ConstDef o
cd2 <- forall a. IORef a -> IO a
readIORef ConstRef o
c2
    case (forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd1, forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd2) of
     (Constructor{}, Constructor{}) ->
      if ConstRef o
c1 forall a. Eq a => a -> a -> Bool
== ConstRef o
c2 then
       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
       forall blk. Prop blk -> MetaEnv (PB blk)
mpret 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 :: forall o. Nat -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi Nat
v ICExp o
t =
 forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
t) forall a b. (a -> b) -> a -> b
$ \HNExp o
hnt ->
 case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hnt of
  HNPi Hiding
_ Bool
_ ICExp o
_ (Abs MId
_ ICExp o
ot) -> forall o. Nat -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi (Nat
v forall a. Num a => a -> a -> a
- Nat
1) forall a b. (a -> b) -> a -> b
$ forall o. MExp o -> ICExp o -> ICExp o
subi (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Nat -> Elr o
Var Nat
v) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) ICExp o
ot
  HNExp' 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 :: 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 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 = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
True, Prio
prioTypecheckArgList, (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall o. Bool -> RefInfo o
RICheckElim forall a b. (a -> b) -> a -> b
$ Bool
isdep Bool -> Bool -> Bool
|| Bool
isconstructor)) MArgList o
args 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 ->
  forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioInferredTypeUnknown (forall a. a -> Maybe a
Just forall o. RefInfo o
RIInferredTypeUnknown) (forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
iityp) forall a b. (a -> b) -> a -> b
$ \HNExp o
hnityp -> case 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 forall a. Ord a => a -> a -> Bool
> Nat
0 Bool -> Bool -> Bool
|| forall o. MExp o -> Bool
copyarg MExp o
a Bool -> Bool -> Bool
|| Hiding
hid forall a. Eq a => a -> a -> Bool
== Hiding
hid2 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$
    forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And (forall a. a -> Maybe a
Just ([forall blk a. TravWith a blk => a -> Term blk
Term MExp o
a | Bool
possdep] forall a. [a] -> [a] -> [a]
++ [forall blk a. TravWith a blk => a -> Term blk
Term Ctx o
ctx, forall blk a. TravWith a blk => a -> Term blk
Term [MExp o]
ityptrs]))
        (if Nat
ndfv forall a. Ord a => a -> a -> Bool
> Nat
0 then forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK else 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)
        (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 forall a. Num a => a -> a -> a
- Nat
1) Bool
isdep Ctx o
ctx (forall o. MExp o -> CExp o -> CExp o
sub MExp o
a (ICExp o -> CExp o
t ICExp o
ot)) MArgList o
as (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
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error String
"tcargs, inf type should be fun or pi (and same hid)"


 ALProj{} | Nat
ndfv forall a. Ord a => a -> a -> Bool
> Nat
0 -> forall a. HasCallStack => a
__IMPOSSIBLE__

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


 ALConPar MArgList o
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

 where
  t :: ICExp o -> CExp o
t = 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 :: forall o blk. 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)) = forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ 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)             = forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp o
a (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. ArgList o
ALNil)
   f (NotM (ALCons Hiding
hid MExp o
a MArgList o
as)) = forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp o
a (MArgList o -> MArgList o
f MArgList o
as)
   f MArgList o
_                        = forall a. HasCallStack => a
__IMPOSSIBLE__
addend Hiding
_ MExp o
_ MM (Exp o) blk
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

type HNNBlks o = [HNExp o]

noblks :: HNNBlks o
noblks :: forall o. HNNBlks o
noblks = []

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

hnn :: ICExp o -> EE (MyMB (HNExp o) o)
hnn :: forall o. ICExp o -> EE (MyMB (HNExp o) o)
hnn ICExp o
e = forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
e) forall a b. (a -> b) -> a -> b
$ \(HNExp o
hne, HNNBlks 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 :: forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
e = forall o.
ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' ICExp o
e forall o. ICArgList o
CALNil

hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)
hnn_checkstep :: forall o. ICExp o -> EE (MyMB (HNExp o, Bool) o)
hnn_checkstep ICExp o
e =
 forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb ICExp o
e forall o. ICArgList o
CALNil) forall a b. (a -> b) -> a -> b
$ \HNExp o
hne ->
  forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne) 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
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret (HNExp o
hne, Bool
False)
   Left (ICExp o
e, ICArgList o
as) ->
    forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' ICExp o
e ICArgList o
as) forall a b. (a -> b) -> a -> b
$ \(HNExp o
hne, HNNBlks 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' :: forall o.
ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' ICExp o
e ICArgList o
as =
 forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb ICExp o
e ICArgList o
as) forall a b. (a -> b) -> a -> b
$ \HNExp o
hne ->
  forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne) 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 -> forall a blk. a -> MetaEnv (MB a blk)
mbret (HNExp o
hne, HNNBlks o
blks)
   Left (ICExp o
e, ICArgList o
as) -> 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 :: forall o. ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb ICExp o
e ICArgList o
as = forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
False ICExp o
e ICArgList o
as []) forall a b. (a -> b) -> a -> b
$ \HNRes o
res -> case HNRes o
res of
            HNDone Maybe (Metavar (Exp o) (RefInfo o))
_ HNExp o
hne -> forall a blk. a -> MetaEnv (MB a blk)
mbret HNExp o
hne
            HNMeta{} -> 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 :: forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
haltmeta = ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop
 where
  loop :: ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop ce :: ICExp o
ce@(Clos [CAction o]
cl MM (Exp o) (RefInfo o)
e) ICArgList o
cargs [Maybe (UId o)]
seenuids =
   (if Bool
haltmeta then 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 (forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall o. ICExp o -> ICArgList o -> [Maybe (UId o)] -> HNRes o
HNMeta ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids) else 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) 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 = forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat (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 forall o. [CAction o] -> Nat -> Either Nat (ICExp o)
doclos [CAction o]
cl Nat
v of
       Left Nat
v' -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
                        forall a b. (a -> b) -> a -> b
$ forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (Maybe (UId o)
uid forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
                        forall a b. (a -> b) -> a -> b
$ forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (forall o. Nat -> Elr o
Var Nat
v') ICArgList o
ncargs
       Right ICExp o
f -> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop ICExp o
f ICArgList o
ncargs (Maybe (UId o)
uid forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
      Const ConstRef o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
                       forall a b. (a -> b) -> a -> b
$ forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (Maybe (UId o)
uid forall a. a -> [a] -> [a]
: [Maybe (UId o)]
seenuids)
                       forall a b. (a -> b) -> a -> b
$ 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) ->
     forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
cargs) forall a b. (a -> b) -> a -> b
$ \HNArgList o
hncargs -> case HNArgList o
hncargs of
      HNArgList o
HNALNil -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall o. Maybe (UId o) -> HNExp o -> HNRes o
HNDone Maybe (UId o)
expmeta
                       forall a b. (a -> b) -> a -> b
$ forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds [Maybe (UId o)]
seenuids
                       forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> Abs (ICExp o) -> HNExp' o
HNLam Hiding
hid (forall a. MId -> a -> Abs a
Abs MId
id (forall a o. [CAction o] -> a -> Clos a o
Clos (forall o. CAction o
Skip 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)]
-> MetaEnv (MB (HNRes o) (RefInfo o))
loop (forall a o. [CAction o] -> a -> Clos a o
Clos (forall o. ICExp o -> CAction o
Sub ICExp o
arg forall a. a -> [a] -> [a]
: [CAction o]
cl) MM (Exp o) (RefInfo o)
b) ICArgList o
cargs' [Maybe (UId o)]
seenuids

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

    AbsurdLambda{} -> 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 -> forall a. a -> Maybe a
Just UId o
m; NotM Exp 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 =
   forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
cargs) 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{} -> forall a blk. String -> MetaEnv (MB a blk)
mbfailed String
"hnc: there should be no args"

    HNALConPar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__


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

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


    ALConPar MArgList o
args -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall o. ICArgList o -> HNArgList o
HNALConPar (forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat (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 :: forall o.
Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs Nat
0 ICArgList o
args = forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([], ICArgList o
args)
getNArgs Nat
narg ICArgList o
args =
 forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args) forall a b. (a -> b) -> a -> b
$ \HNArgList o
hnargs -> case HNArgList o
hnargs of
  HNArgList o
HNALNil -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
  HNALCons Hiding
_ ICExp o
arg ICArgList o
args' ->
   forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs (Nat
narg forall a. Num a => a -> a -> a
- Nat
1) ICArgList o
args') 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 -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a. Maybe a
Nothing
    Just ([ICExp o]
pargs, ICArgList o
rargs) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (ICExp o
arg forall a. a -> [a] -> [a]
: [ICExp o]
pargs, ICArgList o
rargs)

  HNALConPar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__


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

  HNALConPar ICArgList o
args2 ->
   forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
args2) forall a b. (a -> b) -> a -> b
$ \[ICExp o]
args3 -> forall a blk. a -> MetaEnv (MB a blk)
mbret (forall a. HasCallStack => a
__IMPOSSIBLE__ 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 :: forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
smartcheck HNExp o
e = case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
e of
 HNApp (Const ConstRef o
c) ICArgList o
args -> do
  ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
  case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
   Def Nat
narg [Clause o]
cls Maybe Nat
_ Maybe Nat
_ ->
    forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs Nat
narg ICArgList o
args) 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 -> forall a blk. a -> MetaEnv (MB a blk)
mbret (forall a b. b -> Either a b
Right forall o. HNNBlks o
noblks)
     Just ([ICExp o]
pargs, ICArgList o
rargs) ->
      forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
[Clause o]
-> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
dorules [Clause o]
cls (forall a b. (a -> b) -> [a] -> [b]
map forall o. ICExp o -> PEval o
PENo [ICExp o]
pargs)) 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 -> forall a blk. a -> MetaEnv (MB a blk)
mbret (forall a b. b -> Either a b
Right HNNBlks o
blks)
       Left ICExp o
rhs -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (ICExp o
rhs, ICArgList o
rargs)
   DeclCont o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall o. HNNBlks o
noblks
 HNExp' o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall o. HNNBlks o
noblks
 where
 dorules :: [Clause o] -> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
 dorules :: forall o.
[Clause o]
-> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
dorules [] [PEval o]
_ = forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall o. HNNBlks o
noblks
 dorules (Clause o
rule:[Clause o]
rules') [PEval o]
as =
  forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Clause o
-> [PEval o]
-> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
dorule Clause o
rule [PEval o]
as) 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') -> 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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret (forall a b. b -> Either a b
Right HNNBlks o
blks)
   Right ICExp o
rhs -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ 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 :: forall o.
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 =
  forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (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) 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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (forall a o. [CAction o] -> a -> Clos a o
Clos (forall a b. (a -> b) -> [a] -> [b]
map forall o. ICExp o -> CAction o
Sub [ICExp o]
ss) MExp o
rhs)
   Left Either [PEval o] (HNNBlks o)
hnas -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ 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 :: forall o.
[Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [] [] = forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ([], [])
 dopats (Pat o
p:[Pat o]
ps') (PEval o
a:[PEval o]
as') =
  forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (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) 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) ->
    forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (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') 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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (PEval o
hna forall a. a -> [a] -> [a]
: [PEval o]
hnas, [ICExp o]
ss2 forall a. [a] -> [a] -> [a]
++ [ICExp o]
ss)
     Left (Right HNNBlks o
blks) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right HNNBlks o
blks)
     Left (Left [PEval o]
hnas) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (PEval o
hna forall a. a -> [a] -> [a]
: [PEval o]
hnas)
   Left (Right HNNBlks o
blks) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right HNNBlks o
blks)
   Left (Left PEval o
hna) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (PEval o
hna forall a. a -> [a] -> [a]
: [PEval o]
as')
 dopats [Pat o]
_ [PEval 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 :: forall o.
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
     forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor ICExp o
a) forall a b. (a -> b) -> a -> b
$ \Bool
notcon -> if Bool
notcon then forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right 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 =
      forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
a) forall a b. (a -> b) -> a -> b
$ \(HNExp o
hna, HNNBlks o
blks) -> case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hna of
       HNApp (Const ConstRef o
c') ICArgList o
as ->
        if ConstRef o
c forall a. Eq a => a -> a -> Bool
== ConstRef o
c' then
         forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
as) forall a b. (a -> b) -> a -> b
$ \[ICExp o]
as' ->
          if forall (t :: * -> *) a. Foldable t => t a -> Nat
length [ICExp o]
as' forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Pat o]
pas then
           forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
[Pat o]
-> [PEval o]
-> EE
     (MyMB
        (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [Pat o]
pas (forall a b. (a -> b) -> [a] -> [b]
map forall o. ICExp o -> PEval o
PENo [ICExp o]
as')) 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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right HNNBlks o
blks)
            Left (Left [PEval o]
hnas) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' [PEval o]
hnas)
          else
           forall a blk. String -> MetaEnv (MB a blk)
mbfailed String
"dopat: wrong amount of args"
        else do
         ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c'
         case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
          Constructor{} -> forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
as) forall a b. (a -> b) -> a -> b
$ \[ICExp o]
as' ->
           forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left (forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' (forall a b. (a -> b) -> [a] -> [b]
map forall o. ICExp o -> PEval o
PENo [ICExp o]
as')))
          DeclCont o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right (forall o. HNExp o -> HNNBlks o -> HNNBlks o
addblk HNExp o
hna HNNBlks o
blks))
       HNExp' o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right (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 forall a. Eq a => a -> a -> Bool
== ConstRef o
c' then
     if forall (t :: * -> *) a. Foldable t => t a -> Nat
length [PEval o]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Pat o]
pas then
      forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (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) 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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right HNNBlks o
blks)
       Left (Left [PEval o]
hnas) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' [PEval o]
hnas)
     else
      forall a blk. String -> MetaEnv (MB a blk)
mbfailed String
"dopat: wrong amount of args"
    else
     forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left PEval o
aa)
 dopat (PatProj ConstRef o
cs) PEval o
a =
  case PEval o
a of
   PENo ICExp o
a ->
    if Bool
smartcheck then
     forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor ICExp o
a) forall a b. (a -> b) -> a -> b
$ \Bool
notcon -> if Bool
notcon then forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right 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 =
      forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks ICExp o
a) forall a b. (a -> b) -> a -> b
$ \(HNExp o
hna, HNNBlks o
blks) -> case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hna of
       HNApp (Const ConstRef o
c') ICArgList o
as ->
        do
         ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c'
         case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
          Constructor{} -> forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o. ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs ICArgList o
as) forall a b. (a -> b) -> a -> b
$ \[ICExp o]
as' ->
           forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left (forall o. ICExp o -> ConstRef o -> [PEval o] -> PEval o
PEConApp ICExp o
a ConstRef o
c' (forall a b. (a -> b) -> [a] -> [b]
map forall o. ICExp o -> PEval o
PENo [ICExp o]
as')))
          DeclCont o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right (forall o. HNExp o -> HNNBlks o -> HNNBlks o
addblk HNExp o
hna HNNBlks o
blks))
       HNExp' o
_ -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right (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) -> forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left PEval o
aa)
 dopat PatVar{} a :: PEval o
a@(PENo ICExp o
a') = forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ 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]
_) = forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (PEval o
a, [ICExp o
a'])
 dopat Pat o
PatExp PEval o
a = forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (PEval o
a, [])

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

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

noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)
noiotastep_term :: forall o. ConstRef o -> MArgList o -> EE (MyPB o)
noiotastep_term ConstRef o
c MArgList o
args = do
  ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
  case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
    Def Nat
_ [([Pat o]
pats, MExp o
_)] Maybe Nat
_ Maybe Nat
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
      -- all (\pat -> case pat of {PatConApp{} -> False; _ -> True}) pats
    DeclCont o
_ -> forall o. HNExp o -> EE (MyPB o)
noiotastep forall a b. (a -> b) -> a -> b
$ forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds []
                    forall a b. (a -> b) -> a -> b
$ forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (forall o. ConstRef o -> Elr o
Const ConstRef o
c) forall a b. (a -> b) -> a -> b
$ forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat (forall a o. [CAction o] -> a -> Clos a o
Clos [] MArgList o
args) 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' :: forall o. 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 forall o. ICArgList o
CALNil [] 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 forall o. ICArgList o
CALNil [] 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 =
     forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBeta forall a. Maybe a
Nothing (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) 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 forall a b. (a -> b) -> a -> b
$ forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MExp o
m (forall o. ICExp o -> ICArgList o -> [Maybe (UId o)] -> CMFlex o
CMFFlex ICExp o
ce ICArgList o
cargs [Maybe (UId o)]
seenuids)
         else
          forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBetaStructured forall a. Maybe a
Nothing (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) 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 forall a b. (a -> b) -> a -> b
$ forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MExp o
m (forall o. Maybe (UId o) -> HNExp o -> CMFlex o
CMFBlocked Maybe (UId o)
mexpmeta HNExp o
hne)
            HNMeta{} -> 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 =
     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 (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 (forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MM b (RefInfo o)
m (forall o. Maybe (UId o) -> HNExp o -> CMFlex o
CMFSemi Maybe (UId o)
mexpmeta HNExp o
hne))
         else
          CMode o -> EE (MyPB o)
cont (forall o b.
Refinable b (RefInfo o) =>
MM b (RefInfo o) -> CMFlex o -> CMode o
CMFlex MM b (RefInfo o)
m (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 (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 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 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) -> 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 forall a b. (a -> b) -> a -> b
$ CMFlex o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
fcm CMFlex o
fl1 forall a b. (a -> b) -> a -> b
$ \CMode o
res1 -> CMFlex o -> (CMode o -> EE (MyPB o)) -> EE (MyPB o)
fcm CMFlex o
fl2 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) = 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 =
     forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk.
Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Or Prio
prioCompChoice
      (forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And (forall a. a -> Maybe a
Just [forall blk a. TravWith a blk => a -> Term blk
Term CExp o
lhs, forall blk a. TravWith a blk => a -> Term blk
Term CExp o
rhs])
       (forall o. HNExp o -> EE (MyPB o)
noiotastep HNExp o
hne)
       (CMode o -> EE (MyPB o)
cont (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 =
     forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompIota (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall o. Bool -> RefInfo o
RIIotaStep Bool
semif) (forall o.
Bool
-> HNExp o
-> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)
iotastep Bool
True HNExp o
hne) 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
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ 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 (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 (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 <- forall o. ICExp o -> ICArgList o -> IO Bool
iotapossmeta ICExp o
ce ICArgList o
cargs
       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 ->
        (forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBeta (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall o. Bool -> RefInfo o
RIIotaStep Bool
False) (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) 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{} -> 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 =
         forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioCompUnif, forall a. a -> Maybe a
Just (forall o. [CAction o] -> HNExp o -> RefInfo o
RIUnifInfo [CAction o]
cl HNExp o
opphne)) MExp o
m forall a b. (a -> b) -> a -> b
$ \Exp o
_ ->
         forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompBeta forall a. Maybe a
Nothing (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) forall a b. (a -> b) -> a -> b
$ \HNRes o
res -> case HNRes o
res of
          HNDone Maybe (UId o)
mexpmeta HNExp o
hne ->
           forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And (forall a. a -> Maybe a
Just [forall blk a. TravWith a blk => a -> Term blk
Term CExp o
lhs, forall blk a. TravWith a blk => a -> Term blk
Term CExp o
rhs])
            (forall o. HNExp o -> EE (MyPB o)
noiotastep HNExp o
hne)
            (CMode o -> EE (MyPB o)
iter (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 ->
       forall a. HasCallStack => a
__IMPOSSIBLE__ -- CMFSemi disabled, if used should be: stp True hne iter
      CMFBlocked{} -> 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 (forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne1, 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 forall a. Eq a => a -> a -> Bool
== Nat
v2 then forall a. Maybe a
Nothing
                     else forall a. a -> Maybe a
Just String
"comphn, elr, vars not equal"
                 (Const ConstRef o
c1, Const ConstRef o
c2) ->
                    if ConstRef o
c1 forall a. Eq a => a -> a -> Bool
== ConstRef o
c2 then forall a. Maybe a
Nothing
                    else forall a. a -> Maybe a
Just String
"comphn, elr, consts not equal"
                 (Elr o
_, Elr o
_) -> 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 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ 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 forall o. ICArgList o
CALNil (forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne1) 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 (forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne2) forall a b. (a -> b) -> a -> b
$ forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (forall t. Weakening t => Nat -> t -> t
weak Nat
1 Elr o
elr2) (forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs (forall a o. [CAction o] -> a -> Clos a o
Clos [] forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
NotHidden{- arbitrary -} (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Nat -> Elr o
Var Nat
0) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) (forall t. Weakening t => Nat -> t -> t
weak Nat
1 ICArgList o
args2))) 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 (forall a o. [Maybe (UId o)] -> a -> WithSeenUIds a o
WithSeenUIds (forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne1) forall a b. (a -> b) -> a -> b
$ forall o. Elr o -> ICArgList o -> HNExp' o
HNApp (forall t. Weakening t => Nat -> t -> t
weak Nat
1 Elr o
elr1) (forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs (forall a o. [CAction o] -> a -> Clos a o
Clos [] forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
NotHidden{- arbitrary -} (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Nat -> Elr o
Var Nat
0) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)) (forall t. Weakening t => Nat -> t -> t
weak Nat
1 ICArgList o
args1))) 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 forall o. ICArgList o
CALNil (forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne2) 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)) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$
       forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And (forall a. a -> Maybe a
Just [forall blk a. TravWith a blk => a -> Term blk
Term [MExp o]
trs1, 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) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$
       case (Sort
s1, Sort
s2) of
        (Set Nat
i1, Set Nat
i2) -> if Nat
i1 forall a. Eq a => a -> a -> Bool
== Nat
i2 Bool -> Bool -> Bool
|| Bool
ineq Bool -> Bool -> Bool
&& Nat
i1 forall a. Ord a => a -> a -> Bool
> Nat
i2 then forall blk. Prop blk
OK else forall blk. String -> Prop blk
Error String
"comphn, set levels not matching"
        (Set Nat
_, Sort
UnknownSort) -> forall blk. Prop blk
OK
        (Sort
UnknownSort, Set Nat
_) -> forall blk. Prop blk
OK
        (Sort
UnknownSort, Sort
UnknownSort) -> forall blk. Prop blk
OK
        (Sort
Type, Set Nat
_) | Bool
ineq -> forall blk. Prop blk
OK
        (Sort
Type, Sort
UnknownSort) | Bool
ineq -> forall blk. Prop blk
OK
        (Sort, Sort)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      (HNApp (Const ConstRef o
c1) ICArgList o
_, HNExp' o
_) -> case Maybe (UId o)
mexpmeta2 of
       Maybe (UId o)
Nothing -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error String
"comphn, not equal (2)"
       Just UId o
m2 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk a. String -> Metavar a blk -> Move' blk a -> Prop blk
AddExtraRef String
"comphn: not equal, adding extra ref"
                          UId o
m2 (forall o. UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref UId o
m2 (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 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error String
"comphn, not equal (3)"
       Just UId o
m1 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk a. String -> Metavar a blk -> Move' blk a -> Prop blk
AddExtraRef String
"comphn: not equal, adding extra ref"
                          UId o
m1 (forall o. UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref UId o
m1 (forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne2) ConstRef o
c2)
      (HNExp' o
_, HNExp' o
_) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ 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 =
     forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompareArgList forall a. Maybe a
Nothing (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args1) forall a b. (a -> b) -> a -> b
$ \HNArgList o
hnargs1 ->
     forall blk a.
Prio
-> Maybe blk
-> MetaEnv (MB a blk)
-> (a -> MetaEnv (PB blk))
-> MetaEnv (PB blk)
mbpcase Prio
prioCompareArgList forall a. Maybe a
Nothing (forall o. ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist ICArgList o
args2) forall a b. (a -> b) -> a -> b
$ \HNArgList o
hnargs2 ->
     case (HNArgList o
hnargs1, HNArgList o
hnargs2) of
      (HNArgList o
HNALNil, HNArgList o
HNALNil) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
      (HNALCons Hiding
hid1 ICExp o
arg1 ICArgList o
args1b, HNALCons Hiding
hid2 ICExp o
arg2 ICArgList o
args2b) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$
       forall blk.
Maybe [Term blk]
-> MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
And (forall a. a -> Maybe a
Just [forall blk a. TravWith a blk => a -> Term blk
Term [MExp o]
trs1, 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
_) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. String -> Prop blk
Error 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 <- 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 <- forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MArgList o
as
        case MArgList o
as of
         Meta{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
         NotM ArgList o
as -> case ArgList o
as of
          ArgList o
ALNil -> case forall o. [CAction o] -> Nat -> Either Nat (ICExp o)
doclos [CAction o]
cl Nat
v of
           Left Nat
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
           Right ICExp o
e -> ICExp o -> IO Bool
boringExp ICExp o
e
          ALCons{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          ALProj{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          ALConPar{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

       Exp o
_ -> 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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
           f (Weak Nat
_) = 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 = 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
     forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MArgList o
as
       case MArgList o
as of
        Meta{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        NotM ArgList o
as -> case ArgList o
as of
         ArgList o
ALNil -> 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 (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
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
b1 Bool -> Bool -> Bool
&& Bool
b2

         ALProj{} -> 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 :: forall o. MExp o -> EE (MyPB o)
checkeliminand = 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 =
   forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. a -> Maybe a
Just (forall o. [UId o] -> [Elr o] -> RefInfo o
RIUsedVars [UId o]
uids [Elr o]
used)) MExp o
e 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 (forall {a}. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (Elr o
elr 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 <- forall a. IORef a -> IO a
readIORef ConstRef o
c
     case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
      Def Nat
_ [Clause o]
_ (Just Nat
i) Maybe Nat
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition ([UId o] -> [Elr o] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs (forall {a}. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (Elr o
elr forall a. a -> [a] -> [a]
: [Elr o]
used) MArgList o
args) (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 = forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
                  ArgList o
ALNil -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
                  ALCons Hiding
_ MExp o
a MArgList o
as -> case a
i of
                   a
0 -> forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. a -> Maybe a
Just forall o. RefInfo o
RINotConstructor) MExp o
a forall a b. (a -> b) -> a -> b
$ \Exp o
_ ->
                         forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
                   a
_ -> a -> MArgList o -> MetaEnv (PB (RefInfo o))
g (a
i 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 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK


                  ALConPar MArgList o
as -> case a
i of
                   a
0 -> forall a. HasCallStack => a
__IMPOSSIBLE__
                   a
_ -> a -> MArgList o -> MetaEnv (PB (RefInfo o))
g (a
i 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 (forall {a}. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (Elr o
elr 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 (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) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition ([UId o] -> [Elr o] -> MExp o -> MetaEnv (PB (RefInfo o))
f (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 (forall {a}. Maybe a -> [a] -> [a]
adduid Maybe (UId o)
uid [UId o]
uids) (forall {o}. [Elr o] -> [Elr o]
w [Elr o]
used) MExp o
e2)
    Sort Sort
_ -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK

    AbsurdLambda{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret 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 =
   forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
as forall a b. (a -> b) -> a -> b
$ \ArgList o
as -> case ArgList o
as of
    ArgList o
ALNil -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
    ALCons Hiding
_ MExp o
a MArgList o
as -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ 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 -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\Elr o
x -> case Elr o
x of {Var Nat
v -> forall o. Nat -> Elr o
Var (Nat
v 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 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 :: forall o.
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 :: forall o. ICExp o -> ICArgList o -> IO Bool
iotapossmeta ce :: ICExp o
ce@(Clos [CAction o]
cl MExp o
_) ICArgList o
cargs = do
 [Bool]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {o}. CAction o -> IO Bool
ncaction [CAction o]
cl
 Bool
y <- forall {o}. ICArgList o -> IO Bool
nccargs ICArgList o
cargs
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (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) = forall o. ICExp o -> IO Bool
nonconstructor ICExp o
ce
  ncaction CAction o
Skip = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ncaction (Weak{}) = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  nccargs :: ICArgList o -> IO Bool
nccargs ICArgList o
CALNil = 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 <- 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
   forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall a. IORef a -> IO a
readIORef (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 -> 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 = 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 <- forall o. ICExp o -> IO Bool
nonconstructor (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
   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
x Bool -> Bool -> Bool
&& Bool
y

  ncargs [CAction o]
_ (ALProj{}) = 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 :: forall o. ICExp o -> IO Bool
nonconstructor ICExp o
ce = do
   MyMB (HNRes o) o
res <- forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
True ICExp o
ce forall o. ICArgList o
CALNil []
   case MyMB (HNRes o) o
res of
    Blocked{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Failed{} -> 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 <- forall a blk. Metavar a blk -> IO [blk]
extractblkinfos UId o
m
      if 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
        forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       else
        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 <- 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 forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne of
        HNApp (Const ConstRef o
c) ICArgList o
_ -> do
         ConstDef o
cd <- forall a. IORef a -> IO a
readIORef ConstRef o
c
         case forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
          Constructor{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          DeclCont o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        HNExp' o
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Blocked Metavar b (RefInfo o)
m MetaEnv (MyMB (HNExp o) o)
_ -> 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor :: forall o. ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor ICExp o
a =
 forall a blk b.
MetaEnv (MB a blk)
-> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbcase (forall o.
Bool
-> ICExp o
-> ICArgList o
-> [Maybe (UId o)]
-> EE (MyMB (HNRes o) o)
hnc Bool
True ICExp o
a forall o. ICArgList o
CALNil []) 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 <- forall a blk. Metavar a blk -> IO [blk]
extractblkinfos UId o
m
    if 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 <- forall o. ICExp o -> ICArgList o -> IO Bool
iotapossmeta ICExp o
ce forall o. ICArgList o
CALNil
      forall a blk. a -> MetaEnv (MB a blk)
mbret forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b
     else
      forall a blk. a -> MetaEnv (MB a blk)
mbret Bool
False
  HNDone{} -> forall a blk. a -> MetaEnv (MB a blk)
mbret Bool
False

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

calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState :: forall o. EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState EqReasoningConsts o
cs = EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
EqRSNone
 where
  f :: EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
s MExp o
e =
   forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. a -> Maybe a
Just (forall o. EqReasoningState -> RefInfo o
RIEqRState EqReasoningState
s)) MExp o
e 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 forall a. Eq a => a -> a -> Bool
== forall o. EqReasoningConsts o -> ConstRef o
eqrcBegin EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSChain] MArgList o
args
     ()
_ | ConstRef o
c forall a. Eq a => a -> a -> Bool
== forall o. EqReasoningConsts o -> ConstRef o
eqrcStep EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSPrf1, EqReasoningState
EqRSChain] MArgList o
args
     ()
_ | ConstRef o
c forall a. Eq a => a -> a -> Bool
== forall o. EqReasoningConsts o -> ConstRef o
eqrcSym EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSPrf2] MArgList o
args
     ()
_ | ConstRef o
c forall a. Eq a => a -> a -> Bool
== forall o. EqReasoningConsts o -> ConstRef o
eqrcCong EqReasoningConsts o
cs -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSNone, EqReasoningState
EqRSPrf3] MArgList o
args
     ()
_ -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [] MArgList o
args
    App Maybe (UId o)
_ OKHandle (RefInfo o)
_ (Var{}) MArgList o
args -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [] MArgList o
args
    Lam Hiding
_ (Abs MId
_ MExp o
b) -> EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
EqRSNone MExp o
b
    Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ MExp o
ot) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
EqRSNone MExp o
it) (EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
EqRSNone MExp o
ot)
    Sort{} -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK

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


  fs :: [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState]
ss MArgList o
args =
   forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
False, Prio
prioNo, forall a. Maybe a
Nothing) MArgList o
args forall a b. (a -> b) -> a -> b
$ \ArgList o
args -> case ([EqReasoningState]
ss, ArgList o
args) of
    ([EqReasoningState]
_, ArgList o
ALNil) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall blk. Prop blk
OK
    (EqReasoningState
s : [EqReasoningState]
ss, ALCons Hiding
_ MExp o
a MArgList o
args) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
s MExp o
a) ([EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState]
ss MArgList o
args)
    ([], ALCons Hiding
_ MExp o
a MArgList o
args) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (EqReasoningState -> MExp o -> MetaEnv (PB (RefInfo o))
f EqReasoningState
EqRSNone MExp o
a) ([EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [] MArgList o
args)

    ([EqReasoningState]
_, ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ MArgList o
as) -> forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition ([EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo o))
fs [] MArgList o
eas) ([EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo 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 -> MetaEnv (PB (RefInfo o))
fs [EqReasoningState]
ss MArgList o
args
    ([], ALConPar MArgList o
args) -> [EqReasoningState] -> MArgList o -> MetaEnv (PB (RefInfo 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 :: forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch Bool
isdep Ctx o
ctx CExp o
typ MExp o
trm = forall blk. Prop blk -> MetaEnv (PB blk)
mpret forall a b. (a -> b) -> a -> b
$ forall blk. MetaEnv (PB blk) -> MetaEnv (PB blk) -> Prop blk
Sidecondition (forall o. MExp o -> EE (MyPB o)
checkeliminand MExp o
trm)
                              (forall o. Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp Bool
isdep Ctx o
ctx CExp o
typ MExp o
trm)

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