From 062a0846f2d8a53fb0f53b4154facbe6e7a57f56 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 27 Apr 2020 17:49:50 +0100 Subject: [PATCH] Fix getRelevantArg IORes is a newtype again, so the chez tests are working again now --- src/TTImp/ProcessData.idr | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 5b66517..df24efe 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -207,16 +207,15 @@ getRelevantArg defs i rel world (NBind fc _ (Pi rig _ val) sc) (NPrimVal _ WorldType) => getRelevantArg defs (1 + i) rel False !(sc defs (toClosure defaultOpts [] (Erased fc False))) - _ => pure Nothing) + _ => + -- if we haven't found a relevant argument yet, make + -- a note of this one and keep going. Otherwise, we + -- have more than one, so give up. + maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) + getRelevantArg defs (1 + i) (Just i) False sc') + (const (pure Nothing)) + rel) rig -getRelevantArg defs i rel world (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc) - = getRelevantArg defs (1 + i) rel False - !(sc defs (toClosure defaultOpts [] (Erased fc False))) -getRelevantArg defs i Nothing world (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg - = getRelevantArg defs (1 + i) (Just i) world - !(sc defs (toClosure defaultOpts [] (Erased fc False))) -getRelevantArg defs i (Just _) world (NBind _ _ (Pi _ _ _) sc) -- more than one relevant - = pure Nothing getRelevantArg defs i rel world tm = pure (maybe Nothing (\r => Just (world, r)) rel)