module Agda.Auto.Typecheck where
import Data.IORef
import Control.Monad (liftM)
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Auto.SearchControl
#include "../undefined.h"
import Agda.Utils.Impossible
tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcExp isdep ctx typ@(TrBr typtrs ityp@(Clos _ itypexp)) trm =
mbpcase prioTypeUnknown Nothing (hnn_checkstep ityp) $ \(hntyp, iotastepdone) ->
mmpcase (True, prioTypecheck isdep, Just (RIMainInfo (length ctx) hntyp iotastepdone)) trm $ \trm -> case trm of
App _ okh elr args -> case hntyp of
HNPi{} | isdep -> mpret $ Error "tcExp, dep terms should be eta-long"
_ -> do
(ityp, sc) <- case elr of
Var v ->
return (weak (v + 1) (snd $ ctx !! v), id)
Const c -> do
cdef <- readIORef c
return (closify (cdtype cdef), \x -> mpret $ And (Just [Term args]) (noiotastep_term c args) x)
ndfv <- case elr of
Var{} -> return 0
Const c -> readIORef c >>= \cd -> return (cddeffreevars cd)
isconstructor <- case elr of
Var{} -> return False
Const c -> do
cdef <- readIORef c
return $ case cdcont cdef of {Constructor{} -> True; _ -> False}
sc $ tcargs ndfv isdep ctx ityp args (NotM $ App Nothing (NotM OKVal) elr (NotM ALNil)) isconstructor $ \ityp _ -> mpret $ ConnectHandle okh (comp' True typ ityp)
Lam hid (Abs id1 b) -> case hntyp of
HNPi _ hid2 _ it (Abs id2 ot) | hid == hid2 ->
tcExp isdep ((pickid id1 id2, t it) : ctx) (t ot) b
_ -> mpret $ Error "tcExp, type of lam should be fun or pi (and same hid)"
Pi _ _ _ it (Abs id ot) -> case hntyp of
HNSort s ->
mpret $ And (Just [Term ctx, Term it])
(tcExp True ctx (closify (NotM $ Sort s)) it)
(tcExp isdep ((id, closify it) : ctx) (closify (NotM $ Sort s)) ot)
_ -> mpret $ Error "tcExp, type of pi should be set"
Sort (Set i) -> case hntyp of
HNSort s2 -> case s2 of
Set j -> mpret $ if i < j then OK else Error "tcExp, type of set should be larger set"
UnknownSort -> mpret OK
Type -> mpret OK
_ -> mpret $ Error "tcExp, type of set should be set"
Sort UnknownSort -> __IMPOSSIBLE__
Sort Type -> __IMPOSSIBLE__
AbsurdLambda hid -> case hntyp of
HNPi _ hid2 _ it _ | hid == hid2 ->
mbpcase prioAbsurdLambda Nothing (getDatatype it) $ \res -> case res of
Just (indeces, cons) ->
foldl (\p con -> mpret $ And Nothing p (
constructorImpossible indeces con
)) (mpret OK) cons
Nothing -> mpret $ Error "tcExp, absurd lambda, datatype needed"
_ -> mpret $ Error "tcExp, type of absurd lam should be fun or pi (and same hid)"
where
t = TrBr typtrs
getDatatype :: ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)
getDatatype t =
mbcase (hnn t) $ \hnt -> case hnt of
HNApp _ (Const c) args -> do
cd <- readIORef c
case cdcont cd of
Datatype cons _ -> mbret $ Just (args, cons)
_ -> mbret Nothing
_ -> mbret Nothing
constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)
constructorImpossible args c = do
cd <- readIORef c
mbpcase prioAbsurdLambda Nothing (traversePi (1) (Clos [] $ cdtype cd)) $ \hnot ->
case hnot of
HNApp _ _ args2 -> unequals args args2 (\_ -> mpret $ Error "not unequal") []
_ -> mpret $ Error "constructorImpossible 1"
unequals :: ICArgList o -> ICArgList o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)
unequals es1 es2 cont unifier2 =
mbpcase prioAbsurdLambda Nothing (hnarglist es1) $ \hnes1 ->
mbpcase prioAbsurdLambda Nothing (hnarglist es2) $ \hnes2 ->
case (hnes1, hnes2) of
(HNALCons _ e1 es1, HNALCons _ e2 es2) -> unequal e1 e2 (unequals es1 es2 cont) unifier2
(HNALConPar es1, HNALConPar es2) -> unequals es1 es2 cont unifier2
_ -> cont unifier2
unequal :: ICExp o -> ICExp o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)
unequal e1 e2 cont unifier2 =
mbpcase prioAbsurdLambda Nothing (hnn e1) $ \hne1 ->
mbpcase prioAbsurdLambda Nothing (hnn e2) $ \hne2 ->
case hne2 of
HNApp _ (Var v2) es2 | v2 < 0 ->
mbpcase prioAbsurdLambda Nothing (hnarglist es2) $ \hnes2 -> case hnes2 of
HNALNil ->
case lookup v2 unifier2 of
Nothing -> cont ((v2, hne1) : unifier2)
Just hne2' -> cc hne1 hne2'
HNALCons{} -> cont unifier2
HNALConPar{} -> __IMPOSSIBLE__
_ -> cc hne1 hne2
where
cc hne1 hne2 = case (hne1, hne2) of
(HNApp _ (Const c1) es1, HNApp _ (Const c2) es2) -> do
cd1 <- readIORef c1
cd2 <- readIORef c2
case (cdcont cd1, cdcont cd2) of
(Constructor{}, Constructor{}) ->
if c1 == c2 then
unequals es1 es2 cont unifier2
else
mpret OK
_ -> cont unifier2
_ -> cont unifier2
traversePi :: Int -> ICExp o -> EE (MyMB (HNExp o) o)
traversePi v t =
mbcase (hnn t) $ \hnt ->
case hnt of
HNPi _ _ _ _ (Abs _ ot) -> traversePi (v 1) (subi (NotM $ App Nothing (NotM OKVal) (Var v) (NotM ALNil)) ot)
_ -> mbret hnt
tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool -> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)
tcargs ndfv isdep ctx ityp@(TrBr ityptrs iityp) args elimtrm isconstructor cont = mmpcase (True, prioTypecheckArgList, (Just $ RICheckElim $ isdep || isconstructor)) args $ \args' -> case args' of
ALNil -> cont ityp elimtrm
ALCons hid a as ->
mbpcase prioInferredTypeUnknown (Just RIInferredTypeUnknown) (hnn iityp) $ \hnityp -> case hnityp of
HNPi _ hid2 possdep it (Abs _ ot) | ndfv > 0 || copyarg a || hid == hid2 -> mpret $
And (Just ((if possdep then [Term a] else []) ++ [Term ctx, Term ityptrs]))
(if ndfv > 0 then mpret OK else (tcExp (isdep || possdep) ctx (t it) a))
(tcargs (ndfv 1) isdep ctx (sub a (t ot)) as (addend hid a elimtrm) isconstructor cont)
_ -> mpret $ Error "tcargs, inf type should be fun or pi (and same hid)"
ALProj{} | ndfv > 0 -> __IMPOSSIBLE__
ALProj preas projidx hid as ->
mbpcase prioInferredTypeUnknown (Just RIInferredTypeUnknown) (hnn iityp) $ \hnityp -> case hnityp of
HNApp _ (Const dd) _ -> do
dddef <- readIORef dd
case cdcont dddef of
Datatype _ projs ->
mmpcase (True, prioProjIndex, Just (RICheckProjIndex projs)) projidx $
\projidx -> do
projd <- readIORef projidx
tcargs (cddeffreevars projd) isdep ctx (closify $ cdtype projd) preas (NotM $ App Nothing (NotM OKVal) (Const projidx) (NotM ALNil)) True $
\ityp2@(TrBr ityp2trs iityp2) elimtrm2 ->
case iityp2 of
Clos _ (NotM (Pi _ _ _ (NotM (App _ _ (Const dd2) _)) _)) | dd2 == dd ->
mbpcase prioInferredTypeUnknown (Just RIInferredTypeUnknown) (hnn iityp2) $ \hnityp2 -> case hnityp2 of
HNPi _ hid2 possdep it (Abs _ ot) | hid == hid2 -> mpret $
And Nothing
(comp' True (TrBr ityp2trs it) ityp)
(tcargs 0 isdep ctx (sub elimtrm (t ot)) as (addend hid elimtrm elimtrm2) isconstructor cont)
_ -> mpret $ Error "proj function type is not a Pi"
_ -> mpret $ Error "proj function type is not correct"
_ -> mpret $ Error "proj, not a datatype"
_ -> mpret $ Error "proj, not a const app"
ALConPar _ -> __IMPOSSIBLE__
where
t = TrBr ityptrs
addend hid a (NotM (App uid okh elr as)) = NotM $ App uid okh elr (f as)
where f (NotM ALNil) = NotM $ ALCons hid a (NotM $ ALNil)
f (NotM (ALCons hid a as)) = NotM $ ALCons hid a (f as)
f _ = __IMPOSSIBLE__
addend _ _ _ = __IMPOSSIBLE__
copyarg _ = False
type HNNBlks o = [HNExp o]
noblks = []
addblk = (:)
hnn :: ICExp o -> EE (MyMB (HNExp o) o)
hnn e = mbcase (hnn_blks e) $ \(hne, _) -> mbret hne
hnn_blks :: ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn_blks e = hnn' e CALNil
hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)
hnn_checkstep e =
mbcase (hnb e CALNil) $ \hne ->
mbcase (iotastep True hne) $ \res -> case res of
Right _ -> mbret (hne, False)
Left (e, as) ->
mbcase (hnn' e as) $ \(hne, _) -> mbret (hne, True)
hnn' :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)
hnn' e as =
mbcase (hnb e as) $ \hne ->
mbcase (iotastep True hne) $ \res -> case res of
Right blks -> mbret (hne, blks)
Left (e, as) -> hnn' e as
hnb :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)
hnb e as = mbcase (hnc False e as []) $ \res -> case res of
HNDone _ hne -> mbret hne
HNMeta{} -> __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 haltmeta = loop
where
loop ce@(Clos cl e) cargs seenuids =
(if haltmeta then mmmcase e (mbret $ HNMeta ce cargs seenuids) else mmcase e) $
\ee -> case ee of
App uid okh elr args ->
let ncargs = CALConcat (Clos cl args) cargs
in case elr of
Var v -> case doclos cl v of
Left v' -> mbret $ HNDone expmeta (HNApp (uid : seenuids) (Var v') ncargs)
Right f -> loop f ncargs (uid : seenuids)
Const _ -> mbret $ HNDone expmeta (HNApp (uid : seenuids) elr ncargs)
Lam hid (Abs id b) ->
mbcase (hnarglist cargs) $ \hncargs -> case hncargs of
HNALNil -> mbret $ HNDone expmeta (HNLam seenuids hid (Abs id (Clos (Skip : cl) b)))
HNALCons _ arg cargs' -> loop (Clos (Sub arg : cl) b) cargs' seenuids
HNALConPar{} -> __IMPOSSIBLE__
Pi uid hid possdep it (Abs id ot) -> checkNoArgs cargs $ mbret $ HNDone expmeta (HNPi (uid : seenuids) hid possdep (Clos cl it) (Abs id (Clos (Skip : cl) ot)))
Sort s -> checkNoArgs cargs $ mbret $ HNDone expmeta (HNSort s)
AbsurdLambda{} -> mbfailed "hnc: encountered absurdlambda"
where expmeta = case e of {Meta m -> Just m; NotM _ -> Nothing}
checkNoArgs cargs c =
mbcase (hnarglist cargs) $ \hncargs -> case hncargs of
HNALNil -> c
HNALCons{} -> mbfailed "hnc: there should be no args"
HNALConPar{} -> __IMPOSSIBLE__
hnarglist :: ICArgList o -> EE (MyMB (HNArgList o) o)
hnarglist args =
case args of
CALNil -> mbret HNALNil
CALConcat (Clos cl args) args2 ->
mmcase args $ \args -> case args of
ALNil -> hnarglist args2
ALCons hid arg argsb -> mbret $ HNALCons hid (Clos cl arg) (CALConcat (Clos cl argsb) args2)
ALProj{} -> mbret HNALNil
ALConPar args -> mbret $ HNALConPar (CALConcat (Clos cl args) args2)
getNArgs :: Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)
getNArgs 0 args = mbret $ Just ([], args)
getNArgs narg args =
mbcase (hnarglist args) $ \hnargs -> case hnargs of
HNALNil -> mbret Nothing
HNALCons _ arg args' ->
mbcase (getNArgs (narg 1) args') $ \res -> case res of
Nothing -> mbret Nothing
Just (pargs, rargs) -> mbret $ Just (arg : pargs, rargs)
HNALConPar{} -> __IMPOSSIBLE__
getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)
getAllArgs args =
mbcase (hnarglist args) $ \hnargs -> case hnargs of
HNALNil -> mbret []
HNALCons _ arg args' ->
mbcase (getAllArgs args') $ \args'' ->
mbret (arg : args'')
HNALConPar args2 ->
mbcase (getAllArgs args2) $ \args3 -> mbret (__IMPOSSIBLE__ : 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 smartcheck e = case e of
HNApp _ (Const c) args -> do
cd <- readIORef c
case cdcont cd of
Def narg cls _ _ ->
mbcase (getNArgs narg args) $ \res -> case res of
Nothing -> mbret (Right noblks)
Just (pargs, rargs) ->
mbcase (dorules cls (map PENo pargs)) $ \res -> case res of
Right blks -> mbret (Right blks)
Left rhs -> mbret $ Left (rhs, rargs)
_ -> mbret $ Right noblks
_ -> mbret $ Right noblks
where
dorules :: [Clause o] -> [PEval o] -> EE (MyMB (Either (ICExp o) (HNNBlks o)) o)
dorules [] _ = mbret $ Right noblks
dorules (rule:rules') as =
mbcase (dorule rule as) $ \x -> case x of
Left (Left as') -> dorules rules' as'
Left (Right blks) -> mbret (Right blks)
Right rhs -> mbret $ Left rhs
dorule :: Clause o -> [PEval o] -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) (ICExp o)) o)
dorule (pats, rhs) as =
mbcase (dopats pats as) $ \x -> case x of
Right (_, ss) -> mbret $ Right (Clos (map Sub ss) rhs)
Left hnas -> mbret $ Left hnas
dopats :: [Pat o] -> [PEval o] -> EE (MyMB (Either (Either [PEval o] (HNNBlks o)) ([PEval o], [ICExp o])) o)
dopats [] [] = mbret $ Right ([], [])
dopats (p:ps') (a:as') =
mbcase (dopat p a) $ \x -> case x of
Right (hna, ss) ->
mbcase (dopats ps' as') $ \x -> case x of
Right (hnas, ss2) -> mbret $ Right (hna : hnas, ss2 ++ ss)
Left (Right blks) -> mbret $ Left (Right blks)
Left (Left hnas) -> mbret $ Left $ Left (hna : hnas)
Left (Right blks) -> mbret $ Left (Right blks)
Left (Left hna) -> mbret $ Left $ Left (hna : as')
dopats _ _ = __IMPOSSIBLE__
dopat :: Pat o -> PEval o -> EE (MyMB (Either (Either (PEval o) (HNNBlks o)) (PEval o, [ICExp o])) o)
dopat (PatConApp c pas) a =
case a of
PENo a ->
if smartcheck then
mbcase (meta_not_constructor a) $ \notcon -> if notcon then mbret $ Left $ Right noblks else qq
else
qq
where
qq =
mbcase (hnn_blks a) $ \(hna, blks) -> case hna of
HNApp _ (Const c') as ->
if c == c' then
mbcase (getAllArgs as) $ \as' ->
if length as' == length pas then
mbcase (dopats pas (map PENo as')) $ \x -> case x of
Right (hnas, ss) -> mbret $ Right (PEConApp a c' hnas, ss)
Left (Right blks) -> mbret $ Left (Right blks)
Left (Left hnas) -> mbret $ Left $ Left (PEConApp a c' hnas)
else
mbfailed "dopat: wrong amount of args"
else do
cd <- readIORef c'
case cdcont cd of
Constructor{} -> mbcase (getAllArgs as) $ \as' ->
mbret $ Left (Left (PEConApp a c' (map PENo as')))
_ -> mbret $ Left (Right (addblk hna blks))
_ -> mbret $ Left (Right (addblk hna blks))
aa@(PEConApp a c' as) ->
if c == c' then
if length as == length pas then
mbcase (dopats pas as) $ \x -> case x of
Right (hnas, ss) -> mbret $ Right (PEConApp a c' hnas, ss)
Left (Right blks) -> mbret $ Left (Right blks)
Left (Left hnas) -> mbret $ Left $ Left (PEConApp a c' hnas)
else
mbfailed "dopat: wrong amount of args"
else
mbret $ Left (Left aa)
dopat PatVar{} a@(PENo a') = mbret $ Right (a, [a'])
dopat PatVar{} a@(PEConApp a' _ _) = mbret $ Right (a, [a'])
dopat PatExp a = mbret $ Right (a, [])
noiotastep :: HNExp o -> EE (MyPB o)
noiotastep hne =
mbpcase prioNoIota Nothing (iotastep False hne) $ \res -> case res of
Left _ -> mpret $ Error "iota step possible contrary to assumed"
Right _ -> mpret OK
noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)
noiotastep_term c args = f (HNApp [] (Const c) (CALConcat (Clos [] args) CALNil))
where
f hne@(HNApp _ (Const c) _) = do
cd <- readIORef c
let isshorthand =
case cdcont cd of
Def _ [(pats, _)] _ _ -> True
_ -> False
if isshorthand then
mpret OK
else
noiotastep hne
f _ = __IMPOSSIBLE__
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' ineq lhs@(TrBr trs1 e1) rhs@(TrBr trs2 e2) = comp ineq e1 e2
where
comp :: Bool -> ICExp o -> ICExp o -> EE (MyPB o)
comp ineq e1 e2 =
proc e1 e2
where
proc e1 e2 = f True e1 CALNil [] $ \res1 -> f True e2 CALNil [] $ \res2 -> g res1 res2
f semifok e as seenuids cont =
mbpcase prioCompBeta Nothing (hnc True e as seenuids) $ \res ->
case res of
HNDone mexpmeta hne -> fhn semifok mexpmeta hne cont
HNMeta ce@(Clos cl m) cargs seenuids -> do
b1 <- boringClos cl
b2 <- boringArgs cargs
if b1 && b2 then
cont $ CMFlex m (CMFFlex ce cargs seenuids)
else
mbpcase prioCompBetaStructured Nothing (hnc False ce cargs seenuids) $ \res ->
case res of
HNDone mexpmeta hne -> cont $ CMFlex m (CMFBlocked mexpmeta hne)
HNMeta{} -> __IMPOSSIBLE__
fhn semifok mexpmeta hne cont =
mmbpcase (iotastep True hne)
(\m -> do
sf <- return False
if semifok && sf then
cont (CMFlex m (CMFSemi mexpmeta hne))
else
cont (CMFlex m (CMFBlocked mexpmeta hne))
)
(\res -> case res of
Right _ -> cont (CMRigid mexpmeta hne)
Left (e, as) -> f semifok e as [] cont
)
g res1 res2 =
case (res1, res2) of
(CMRigid mexpmeta1 hne1, CMRigid mexpmeta2 hne2) -> comphn ineq mexpmeta1 hne1 mexpmeta2 hne2
(CMFlex m1 (CMFBlocked mexpmeta1 hne1), _) -> mstp False mexpmeta1 hne1 $ \res1 -> g res1 res2
(_, CMFlex m2 (CMFBlocked mexpmeta2 hne2)) -> mstp False mexpmeta2 hne2 $ \res2 -> g res1 res2
(CMRigid mexpmeta1 hne1, CMFlex _ fl2) -> unif True mexpmeta1 hne1 fl2
(CMFlex _ fl1, CMRigid mexpmeta2 hne2) -> unif False mexpmeta2 hne2 fl1
(CMFlex m1 fl1, CMFlex m2 fl2) -> doubleblock m1 m2 $ fcm fl1 $ \res1 -> fcm fl2 $ \res2 -> g res1 res2
fcm (CMFFlex ce cargs seenuids) = f True ce cargs seenuids
fcm (CMFSemi mexpmeta hne) = fhn True mexpmeta hne
fcm (CMFBlocked _ hne) = __IMPOSSIBLE__
mstp semif mexpmeta hne cont =
mpret $ Or prioCompChoice
(mpret $ And (Just [Term lhs, Term rhs])
(noiotastep hne)
(cont (CMRigid mexpmeta hne))
)
(stp semif hne cont)
stp semif hne cont =
mbpcase prioCompIota (Just $ RIIotaStep semif) (iotastep True hne) $ \res -> case res of
Right _ -> mpret $ Error "no iota step possible, contrary to assumed"
Left (e, as) -> f semif e as [] cont
unif oppis1 oppmexpmeta opphne res =
let iter res = if oppis1 then
g (CMRigid oppmexpmeta opphne) res
else
g res (CMRigid oppmexpmeta opphne)
in case res of
CMFFlex ce cargs seenuids -> do
poss <- iotapossmeta ce cargs
maybeor poss prioCompChoice
(loop ce cargs seenuids)
(mbpcase prioCompBeta (Just $ RIIotaStep False) (hnc False ce cargs seenuids) $ \res ->
case res of
HNDone mexpmeta hne -> stp False hne iter
HNMeta{} -> __IMPOSSIBLE__
)
where
loop ce@(Clos cl m) cargs seenuids =
mmpcase (False, prioCompUnif, Just (RIUnifInfo cl opphne)) m $ \_ ->
mbpcase prioCompBeta Nothing (hnc True ce cargs seenuids) $ \res -> case res of
HNDone mexpmeta hne ->
mpret $ And (Just [Term lhs, Term rhs])
(noiotastep hne)
(iter (CMRigid mexpmeta hne))
HNMeta ce cargs seenuids -> loop ce cargs seenuids
CMFSemi _ hne ->
__IMPOSSIBLE__
CMFBlocked{} -> __IMPOSSIBLE__
comphn :: Bool -> Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> Maybe (Metavar (Exp o) (RefInfo o)) -> HNExp o -> EE (MyPB o)
comphn ineq mexpmeta1 hne1 mexpmeta2 hne2 =
case (hne1, hne2) of
(HNApp _ elr1 args1, HNApp _ elr2 args2) ->
let ce = case (elr1, elr2) of
(Var v1, Var v2) -> if v1 == v2 then Nothing else Just "comphn, elr, vars not equal"
(Const c1, Const c2) -> if c1 == c2 then Nothing else Just "comphn, elr, consts not equal"
(_, _) -> Just "comphn, elrs not equal"
in case ce of
Nothing -> compargs args1 args2
Just msg -> mpret $ Error msg
(HNLam _ hid1 (Abs id1 b1), HNLam _ hid2 (Abs id2 b2)) -> comp False b1 b2
(HNLam seenuids _ (Abs _ b1), HNApp uid2 elr2 args2) ->
f True b1 CALNil seenuids $ \res1 -> fhn True mexpmeta2 (HNApp uid2 (weakelr 1 elr2) (addtrailingargs (Clos [] $ NotM $ ALCons NotHidden (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)) (NotM ALNil)) (weakarglist 1 args2))) $ \res2 -> g res1 res2
(HNApp uid1 elr1 args1, HNLam seenuids _ (Abs _ b2)) ->
fhn True mexpmeta1 (HNApp uid1 (weakelr 1 elr1) (addtrailingargs (Clos [] $ NotM $ ALCons NotHidden (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)) (NotM ALNil)) (weakarglist 1 args1))) $ \res1 -> f True b2 CALNil seenuids $ \res2 -> g res1 res2
(HNPi _ hid1 _ it1 (Abs id1 ot1), HNPi _ hid2 _ it2 (Abs id2 ot2)) -> mpret $
And (Just [Term trs1, Term trs2]) (comp False it1 it2) (comp ineq ot1 ot2)
(HNSort s1, HNSort s2) -> mpret $
case (s1, s2) of
(Set i1, Set i2) -> if i1 == i2 || ineq && i1 > i2 then OK else Error "comphn, set levels not matching"
(Set _, UnknownSort) -> OK
(UnknownSort, Set _) -> OK
(UnknownSort, UnknownSort) -> OK
(Type, Set _) | ineq -> OK
(Type, UnknownSort) | ineq -> OK
_ -> __IMPOSSIBLE__
(HNApp uid1 (Const c1) _, _) -> case mexpmeta2 of
Nothing -> mpret $ Error "comphn, not equal (2)"
Just m2 -> mpret $ AddExtraRef "comphn: not equal, adding extra ref" m2 (extraref m2 uid1 c1)
(_, HNApp uid2 (Const c2) _) -> case mexpmeta1 of
Nothing -> mpret $ Error "comphn, not equal (3)"
Just m1 -> mpret $ AddExtraRef "comphn: not equal, adding extra ref" m1 (extraref m1 uid2 c2)
(_, _) -> mpret $ Error "comphn, not equal"
compargs :: ICArgList o -> ICArgList o -> EE (MyPB o)
compargs args1 args2 =
mbpcase prioCompareArgList Nothing (hnarglist args1) $ \hnargs1 ->
mbpcase prioCompareArgList Nothing (hnarglist args2) $ \hnargs2 ->
case (hnargs1, hnargs2) of
(HNALNil, HNALNil) -> mpret OK
(HNALCons hid1 arg1 args1b, HNALCons hid2 arg2 args2b) -> mpret $
And (Just [Term trs1, Term trs2]) (comp False arg1 arg2) (compargs args1b args2b)
(HNALConPar args1b, HNALCons _ _ args2b) -> compargs args1b args2b
(HNALCons _ _ args1b, HNALConPar args2b) -> compargs args1b args2b
(HNALConPar args1', HNALConPar args2') -> compargs args1' args2'
(_, _) -> mpret $ Error $ "comphnargs, not equal"
boringExp :: ICExp o -> EE Bool
boringExp (Clos cl e) = do
e <- expandbind e
case e of
Meta{} -> boringClos cl
NotM e -> case e of
App _ _ (Var v) as -> do
as <- expandbind as
case as of
Meta{} -> return False
NotM as -> case as of
ALNil -> case doclos cl v of
Left _ -> return True
Right e -> boringExp e
ALCons{} -> return False
ALProj{} -> return False
ALConPar{} -> return False
_ -> return False
boringClos :: [CAction o] -> EE Bool
boringClos cl = liftM (all id) $ mapM f cl
where f (Sub e) = boringExp e
f Skip = return True
f (Weak _) = return True
boringArgs :: ICArgList o -> EE Bool
boringArgs CALNil = return True
boringArgs (CALConcat (Clos cl as) as2) = do
b1 <- f cl as
b2 <- boringArgs as2
return $ b1 && b2
where
f cl as = do
as <- expandbind as
case as of
Meta{} -> return False
NotM as -> case as of
ALNil -> return True
ALCons _ a as -> do
b1 <- boringExp (Clos cl a)
b2 <- f cl as
return $ b1 && b2
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> f cl as
checkeliminand :: MExp o -> EE (MyPB o)
checkeliminand = f [] []
where
f uids used e =
mmpcase (False, prioNo, Just (RIUsedVars uids used)) e $ \e -> case e of
App uid _ elr@(Var{}) args -> fs (adduid uid uids) (elr : used) args
App uid _ elr@(Const c) args -> do
cd <- readIORef c
case cdcont cd of
Def _ _ (Just i) _ -> mpret $ Sidecondition (fs (adduid uid uids) (elr : used) args) (g i args)
where
g i as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of
ALNil -> mpret OK
ALCons _ a as -> case i of
0 -> mmpcase (False, prioNo, Just RINotConstructor) a $ \_ ->
mpret OK
_ -> g (i 1) as
ALProj eas _ _ as -> mpret OK
ALConPar as -> case i of
0 -> __IMPOSSIBLE__
_ -> g (i 1) as
_ -> fs (adduid uid uids) (elr : used) args
Lam _ (Abs _ e) -> f uids (w used) e
Pi uid _ _ e1 (Abs _ e2) -> mpret $ Sidecondition (f (adduid uid uids) used e1) (f (adduid uid uids) (w used) e2)
Sort _ -> mpret OK
AbsurdLambda{} -> mpret OK
fs uids used as =
mmpcase (False, prioNo, Nothing) as $ \as -> case as of
ALNil -> mpret OK
ALCons _ a as -> mpret $ Sidecondition (f uids used a) (fs uids used as)
ALProj eas _ _ as -> mpret $ Sidecondition (fs uids used eas) (fs uids used as)
ALConPar as -> fs uids used as
w = map (\x -> case x of {Var v -> Var (v + 1); Const{} -> x})
adduid (Just uid) uids = uid : uids
adduid Nothing uids = uids
maybeor _ _ mainalt _ = mainalt
iotapossmeta :: ICExp o -> ICArgList o -> EE Bool
iotapossmeta ce@(Clos cl _) cargs = do
xs <- mapM ncaction cl
y <- nccargs cargs
return $ not (all id xs && y)
where
ncaction (Sub ce) = nonconstructor ce
ncaction Skip = return True
ncaction (Weak{}) = return True
nccargs CALNil = return True
nccargs (CALConcat (Clos cl margs) cargs) = do
x <- ncmargs cl margs
y <- nccargs cargs
return $ x && y
ncmargs cl (Meta m) = do
mb <- readIORef (mbind m)
case mb of
Nothing -> return False
Just x -> ncargs cl x
ncmargs cl (NotM args) = ncargs cl args
ncargs cl ALNil = return True
ncargs cl (ALCons _ a args) = do
x <- nonconstructor (Clos cl a)
y <- ncmargs cl args
return $ x && y
ncargs _ (ALProj{}) = __IMPOSSIBLE__
ncargs cl (ALConPar args) = ncmargs cl args
nonconstructor :: ICExp o -> EE Bool
nonconstructor ce = do
res <- hnc True ce CALNil []
case res of
Blocked{} -> return False
Failed{} -> return False
NotB res -> case res of
HNMeta ce _ _ -> do
let (Clos _ (Meta m)) = ce
infos <- extractblkinfos m
if any (\info -> case info of {RINotConstructor -> True; _ -> False}) infos then do
return True
else
return False
HNDone{} -> do
res <- hnn ce
case res of
NotB hne -> case hne of
HNApp _ (Const c) _ -> do
cd <- readIORef c
case cdcont cd of
Constructor{} -> return False
_ -> return True
_ -> return True
Blocked m _ -> return False
Failed _ -> return False
meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))
meta_not_constructor a =
mbcase (hnc True a CALNil []) $ \res -> case res of
HNMeta ce _ _ -> do
let (Clos _ (Meta m)) = ce
infos <- extractblkinfos m
if any (\info -> case info of {RINotConstructor -> True; _ -> False}) infos then do
b <- iotapossmeta ce CALNil
mbret $ not b
else
mbret False
HNDone{} -> mbret False
calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)
calcEqRState cs = f EqRSNone
where
f s e =
mmpcase (False, prioNo, Just (RIEqRState s)) e $ \e -> case e of
App _ _ (Const c) args -> case () of
_ | c == eqrcBegin cs -> fs [EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSChain] args
_ | c == eqrcStep cs -> fs [EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSPrf1, EqRSChain] args
_ | c == eqrcSym cs -> fs [EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSPrf2] args
_ | c == eqrcCong cs -> fs [EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSNone, EqRSPrf3] args
_ -> fs [] args
App _ _ (Var{}) args -> fs [] args
Lam _ (Abs _ b) -> f EqRSNone b
Pi _ _ _ it (Abs _ ot) -> mpret $ Sidecondition (f EqRSNone it) (f EqRSNone ot)
Sort{} -> mpret OK
AbsurdLambda{} -> mpret OK
fs ss args =
mmpcase (False, prioNo, Nothing) args $ \args -> case (ss, args) of
(_, ALNil) -> mpret OK
(s : ss, ALCons _ a args) -> mpret $ Sidecondition (f s a) (fs ss args)
([], ALCons _ a args) -> mpret $ Sidecondition (f EqRSNone a) (fs [] args)
(_, ALProj eas _ _ as) -> mpret $ Sidecondition (fs [] eas) (fs [] as)
(_ : ss, ALConPar args) -> fs ss args
([], ALConPar args) -> fs [] args
pickid :: MId -> MId -> MId
pickid mid1@(Id _) _ = mid1
pickid _ mid2 = mid2
tcSearch :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
tcSearch isdep ctx typ trm = mpret $ Sidecondition (checkeliminand trm)
(tcExp isdep ctx typ trm)