git.iko.soy/Idris-dev
on master help sign in
Restrict PE for class dictionaries
f2edb7dEdwin Brady
src/Idris/Core/Evaluate.hs+27−10
compare with master
unifiedsplit
@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
13 mapDefCtxt,
13 mapDefCtxt,
14− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
14+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
16 isUniverse) where
16 isUniverse) where
17
17
@@ -25,7 +25,8 @@ import Idris.Core.TT
25import Idris.Core.CaseTree
25import Idris.Core.CaseTree
26
26
27data EvalState = ES { limited :: [(Name, Int)],
27data EvalState = ES { limited :: [(Name, Int)],
28− nexthole :: Int }
28+ nexthole :: Int,
29+ blocking :: Bool }
29 deriving Show
30 deriving Show
30
31
31type Eval a = State EvalState a
32type Eval a = State EvalState a
@@ -37,7 +38,7 @@ data EvalOpt = Spec
37 | RunTT
38 | RunTT
38 deriving (Show, Eq)
39 deriving (Show, Eq)
39
40
40−initEval = ES [] 0
41+initEval = ES [] 0 False
41
42
42-- VALUES (as HOAS) ---------------------------------------------------------
43-- VALUES (as HOAS) ---------------------------------------------------------
43-- | A HOAS representation of values
44-- | A HOAS representation of values
@@ -161,11 +162,12 @@ usable :: Bool -- specialising
161-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
162-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
162usable False n [] = return (True, [])
163usable False n [] = return (True, [])
163usable True n ns
164usable True n ns
164− = do ES ls num <- get
165+ = do ES ls num b <- get
166+ if b then return (False, ns)
165− case lookup n ls of
167+ else case lookup n ls of
166− Just 0 -> return (False, ns)
168+ Just 0 -> return (False, ns)
167− Just i -> return (True, ns)
169+ Just i -> return (True, ns)
168− _ -> return (False, ns)
170+ _ -> return (False, ns)
169usable False n ns
171usable False n ns
170 = case lookup n ns of
172 = case lookup n ns of
171 Just 0 -> return (False, ns)
173 Just 0 -> return (False, ns)
@@ -175,12 +177,16 @@ usable False n ns
175
177
176fnCount :: Int -> Name -> Eval ()
178fnCount :: Int -> Name -> Eval ()
177fnCount inc n
179fnCount inc n
178− = do ES ls num <- get
180+ = do ES ls num b <- get
179 case lookup n ls of
181 case lookup n ls of
180 Just i -> do put $ ES ((n, (i - inc)) :
182 Just i -> do put $ ES ((n, (i - inc)) :
181− filter (\ (n', _) -> n/=n') ls) num
183+ filter (\ (n', _) -> n/=n') ls) num b
182 _ -> return ()
184 _ -> return ()
183
185
186+setBlock :: Bool -> Eval ()
187+setBlock b = do ES ls num _ <- get
188+ put (ES ls num b)
189+
184deduct = fnCount 1
190deduct = fnCount 1
185reinstate = fnCount (-1)
191reinstate = fnCount (-1)
186
192
@@ -284,10 +290,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
284 let ntimes' = case f of
290 let ntimes' = case f of
285 P _ fn _ -> (fn, 0) : ntimes
291 P _ fn _ -> (fn, 0) : ntimes
286 _ -> ntimes
292 _ -> ntimes
293+ when spec $ setBlock True
287 d' <- ev ntimes' stk False env d
294 d' <- ev ntimes' stk False env d
288 l' <- ev ntimes' stk False env l
295 l' <- ev ntimes' stk False env l
289 t' <- ev ntimes' stk False env t
296 t' <- ev ntimes' stk False env t
290 arg' <- ev ntimes' stk False env arg
297 arg' <- ev ntimes' stk False env arg
298+ when spec $ setBlock False
291 evApply ntimes' stk top env [l',t',arg'] d'
299 evApply ntimes' stk top env [l',t',arg'] d'
292 -- Treat "assert_total" specially, as long as it's defined!
300 -- Treat "assert_total" specially, as long as it's defined!
293 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
301 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
@@ -959,6 +967,15 @@ isFnName n ctxt
959 Just (CaseOp _ _ _ _ _ _, _, _, _) -> True
967 Just (CaseOp _ _ _ _ _ _, _, _, _) -> True
960 _ -> False
968 _ -> False
961
969
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+
962lookupP :: Name -> Context -> [Term]
979lookupP :: Name -> Context -> [Term]
963lookupP n ctxt
980lookupP n ctxt
964 = do def <- lookupCtxt n (definitions ctxt)
981 = do def <- lookupCtxt n (definitions ctxt)
src/Idris/PartialEval.hs+2
@@ -66,6 +66,8 @@ partial_eval ctxt ns_in tms = mapM peClause tms where
66 do when (length tms == 1) $ checkProgress ns reductions
66 do when (length tms == 1) $ checkProgress ns reductions
67 return (Right (lhs, rhs'))
67 return (Right (lhs, rhs'))
68
68
69+ -- TMP HACK until I do PE by WHNF rather than using main evaluator
70+ toLimit (n, Nothing) | isTCDict n ctxt = (n, 2)
69 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
71 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
70 toLimit (n, Just l) = (n, l)
72 toLimit (n, Just l) = (n, l)
71
73