@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
1212 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
1313 mapDefCtxt,
14− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
14+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,
1515 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
1616 isUniverse) where
1717
@@ -25,7 +25,8 @@ import Idris.Core.TT
2525import Idris.Core.CaseTree
2626
2727data EvalState = ES { limited :: [(Name, Int)],
28− nexthole :: Int }
28+ nexthole :: Int,
29+ blocking :: Bool }
2930 deriving Show
3031
3132type Eval a = State EvalState a
@@ -37,7 +38,7 @@ data EvalOpt = Spec
3738 | RunTT
3839 deriving (Show, Eq)
3940
40−initEval = ES [] 0
41+initEval = ES [] 0 False
4142
4243-- VALUES (as HOAS) ---------------------------------------------------------
4344-- | A HOAS representation of values
@@ -161,11 +162,12 @@ usable :: Bool -- specialising
161162-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
162163usable False n [] = return (True, [])
163164usable True n ns
164− = do ES ls num <- get
165− case lookup n ls of
166− Just 0 -> return (False, ns)
167− Just i -> return (True, ns)
168− _ -> return (False, ns)
165+ = do ES ls num b <- get
166+ if b then return (False, ns)
167+ else case lookup n ls of
168+ Just 0 -> return (False, ns)
169+ Just i -> return (True, ns)
170+ _ -> return (False, ns)
169171usable False n ns
170172 = case lookup n ns of
171173 Just 0 -> return (False, ns)
@@ -175,12 +177,16 @@ usable False n ns
175177
176178fnCount :: Int -> Name -> Eval ()
177179fnCount inc n
178− = do ES ls num <- get
180+ = do ES ls num b <- get
179181 case lookup n ls of
180182 Just i -> do put $ ES ((n, (i - inc)) :
181− filter (\ (n', _) -> n/=n') ls) num
183+ filter (\ (n', _) -> n/=n') ls) num b
182184 _ -> return ()
183185
186+setBlock :: Bool -> Eval ()
187+setBlock b = do ES ls num _ <- get
188+ put (ES ls num b)
189+
184190deduct = fnCount 1
185191reinstate = fnCount (-1)
186192
@@ -284,10 +290,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
284290 let ntimes' = case f of
285291 P _ fn _ -> (fn, 0) : ntimes
286292 _ -> ntimes
293+ when spec $ setBlock True
287294 d' <- ev ntimes' stk False env d
288295 l' <- ev ntimes' stk False env l
289296 t' <- ev ntimes' stk False env t
290297 arg' <- ev ntimes' stk False env arg
298+ when spec $ setBlock False
291299 evApply ntimes' stk top env [l',t',arg'] d'
292300 -- Treat "assert_total" specially, as long as it's defined!
293301 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
@@ -959,6 +967,15 @@ isFnName n ctxt
959967 Just (CaseOp _ _ _ _ _ _, _, _, _) -> True
960968 _ -> False
961969
970+isTCDict :: Name -> Context -> Bool
971+isTCDict n ctxt
972+ = let def = lookupCtxtExact n (definitions ctxt) in
973+ case def of
974+ Just (Function _ _, _, _, _) -> False
975+ Just (Operator _ _ _, _, _, _) -> False
976+ Just (CaseOp ci _ _ _ _ _, _, _, _) -> tc_dictionary ci
977+ _ -> False
978+
962979lookupP :: Name -> Context -> [Term]
963980lookupP n ctxt
964981 = do def <- lookupCtxt n (definitions ctxt)