git.iko.soy/Idris-dev
on master help sign in
Add assert_total function
6eee6c8Edwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -22,6 +22,8 @@ New in 0.9.11:
22 a pattern for use in totality checking.
22 a pattern for use in totality checking.
23 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
23 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
24 structurally smaller than "(x :: xs)"
24 structurally smaller than "(x :: xs)"
25+* assert_total internal function, which marks a subexpression as assumed to
26+ be total, e.g "assert_total (tail (x :: xs))".
25
27
26Internal changes
28Internal changes
27
29
libs/prelude/Builtins.idr+7
@@ -39,9 +39,16 @@ malloc size x = x -- compiled specially
39trace_malloc : a -> a
39trace_malloc : a -> a
40trace_malloc x = x -- compiled specially
40trace_malloc x = x -- compiled specially
41
41
42+-- Assert to the totality checker than y is always structureally smaller than
43+-- x (which is typically a pattern argument)
42assert_smaller : a -> a -> a
44assert_smaller : a -> a -> a
43assert_smaller x y = y
45assert_smaller x y = y
44
46
47+-- Assert to the totality checker than the given expression will always
48+-- terminate.
49+assert_total : a -> a
50+assert_total x = x
51+
45abstract %assert_total -- need to pretend
52abstract %assert_total -- need to pretend
46believe_me : a -> b -- compiled specially as id, use with care!
53believe_me : a -> b -- compiled specially as id, use with care!
47believe_me x = prim__believe_me _ _ x
54believe_me x = prim__believe_me _ _ x
src/IRTS/Compiler.hs+3
@@ -185,6 +185,9 @@ instance ToIR (TT Name) where
185 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
185 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
186 a == txt "assert_smaller"
186 a == txt "assert_smaller"
187 = ir' env arg
187 = ir' env arg
188+ | (P _ (UN a) _, [_, arg]) <- unApply tm,
189+ a == txt "assert_total"
190+ = ir' env arg
188 | (P _ (UN p) _, [_, arg]) <- unApply tm,
191 | (P _ (UN p) _, [_, arg]) <- unApply tm,
189 p == txt "par"
192 p == txt "par"
190 = do arg' <- ir' env arg
193 = do arg' <- ir' env arg
src/Idris/Core/Evaluate.hs+9−3
@@ -101,6 +101,7 @@ simplify :: Context -> Env -> TT Name -> TT Name
101simplify ctxt env t
101simplify ctxt env t
102 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
102 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
103 (sUN "assert_smaller", 0),
103 (sUN "assert_smaller", 0),
104+ (sUN "assert_total", 0),
104 (sUN "par", 0),
105 (sUN "par", 0),
105 (sUN "prim__syntactic_eq", 0),
106 (sUN "prim__syntactic_eq", 0),
106 (sUN "fork", 0)]
107 (sUN "fork", 0)]
@@ -112,7 +113,6 @@ simplify ctxt env t
112rt_simplify :: Context -> Env -> TT Name -> TT Name
113rt_simplify :: Context -> Env -> TT Name -> TT Name
113rt_simplify ctxt env t
114rt_simplify ctxt env t
114 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
115 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
115− (sUN "assert_smaller", 0),
116 (sUN "par", 0),
116 (sUN "par", 0),
117 (sUN "prim__syntactic_eq", 0),
117 (sUN "prim__syntactic_eq", 0),
118 (sUN "prim_fork", 0)]
118 (sUN "prim_fork", 0)]
@@ -206,6 +206,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
206 if u then
206 if u then
207 do let val = lookupDefAcc n (spec || atRepl) ctxt
207 do let val = lookupDefAcc n (spec || atRepl) ctxt
208 case val of
208 case val of
209+ [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->
210+ ev ntimes (n:stk) True env tm
209 [(Function _ tm, Public)] ->
211 [(Function _ tm, Public)] ->
210 ev ntimes (n:stk) True env tm
212 ev ntimes (n:stk) True env tm
211 [(Function _ tm, Hidden)] ->
213 [(Function _ tm, Hidden)] ->
@@ -213,7 +215,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
213 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
215 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
214 return $ VP nt n vty
216 return $ VP nt n vty
215 [(CaseOp ci _ _ _ _ cd, acc)]
217 [(CaseOp ci _ _ _ _ cd, acc)]
216− | (acc /= Frozen) &&
218+ | (acc /= Frozen || sUN "assert_total" `elem` stk) &&
217 null (fst (cases_totcheck cd)) -> -- unoptimised version
219 null (fst (cases_totcheck cd)) -> -- unoptimised version
218 let (ns, tree) = getCases cd in
220 let (ns, tree) = getCases cd in
219 if blockSimplify ci n stk
221 if blockSimplify ci n stk
@@ -260,6 +262,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
260-- stk top env (finalise tm)) t
262-- stk top env (finalise tm)) t
261-- | otherwise
263-- | otherwise
262 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
264 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
265+ ev ntimes stk top env (App (App (P _ (UN at) _) _) arg)
266+ | at == txt "assert_total" && not simpl
267+ = ev ntimes (UN at : stk) top env arg
263 ev ntimes stk top env (App f a)
268 ev ntimes stk top env (App f a)
264 = do f' <- ev ntimes stk False env f
269 = do f' <- ev ntimes stk False env f
265 a' <- ev ntimes stk False env a
270 a' <- ev ntimes stk False env a
@@ -313,7 +318,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
313 do let val = lookupDefAcc n (spec || atRepl) ctxt
318 do let val = lookupDefAcc n (spec || atRepl) ctxt
314 case val of
319 case val of
315 [(CaseOp ci _ _ _ _ cd, acc)]
320 [(CaseOp ci _ _ _ _ cd, acc)]
321+ | acc /= Frozen || sUN "assert_total" `elem` stk ->
316− | acc /= Frozen -> -- unoptimised version
322+ -- unoptimised version
317 let (ns, tree) = getCases cd in
323 let (ns, tree) = getCases cd in
318 if blockSimplify ci n stk
324 if blockSimplify ci n stk
319 then return $ unload env (VP Ref n ty) args
325 then return $ unload env (VP Ref n ty) args
src/Idris/Coverage.hs+24−9
@@ -333,16 +333,17 @@ checkTotality path fc n
333 else calcTotality path fc n pats
333 else calcTotality path fc n pats
334 setTotality n t'
334 setTotality n t'
335 addIBC (IBCTotal n t')
335 addIBC (IBCTotal n t')
336+ return t'
336 -- if it's not total, it can't reduce, to keep
337 -- if it's not total, it can't reduce, to keep
337 -- typechecking decidable
338 -- typechecking decidable
338− case t' of
339+-- case t' of
339− p@(Partial _) ->
340+-- p@(Partial _) ->
340− do setAccessibility n Frozen
341+-- do setAccessibility n Frozen
341− addIBC (IBCAccess n Frozen)
342+-- addIBC (IBCAccess n Frozen)
342− logLvl 5 $ "HIDDEN: "
343+-- logLvl 5 $ "HIDDEN: "
343− ++ show n ++ show p
344+-- ++ show n ++ show p
344− _ -> return ()
345+-- _ -> return ()
345− return t'
346+-- return t'
346 _ -> return $ Total []
347 _ -> return $ Total []
347 x -> return x
348 x -> return x
348 case t' of
349 case t' of
@@ -373,7 +374,17 @@ checkDeclTotality (fc, n)
373-- buildSCG (fc, n)
374-- buildSCG (fc, n)
374-- logLvl 2 $ "Built SCG"
375-- logLvl 2 $ "Built SCG"
375 i <- getIState
376 i <- getIState
376− checkTotality [] fc n
377+ t <- checkTotality [] fc n
378+ case t of
379+ -- if it's not total, it can't reduce, to keep
380+ -- typechecking decidable
381+ p@(Partial _) -> do setAccessibility n Frozen
382+ addIBC (IBCAccess n Frozen)
383+ logLvl 5 $ "HIDDEN: "
384+ ++ show n ++ show p
385+ _ -> return ()
386+ return t
387+
377
388
378-- Calculate the size change graph for this definition
389-- Calculate the size change graph for this definition
379
390
@@ -410,6 +421,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
410 | (P _ (UN l) _, [_, arg]) <- unApply ap,
421 | (P _ (UN l) _, [_, arg]) <- unApply ap,
411 l == txt "lazy"
422 l == txt "lazy"
412 = findCalls arg pvs pargs
423 = findCalls arg pvs pargs
424+ -- under a call to "assert_total", don't do any checking, just believe
425+ -- that it is total.
426+ | (P _ (UN at) _, [_, _]) <- unApply ap,
427+ at == txt "assert_total" = []
413 | (P _ n _, args) <- unApply ap
428 | (P _ n _, args) <- unApply ap
414 = mkChange n args pargs ++
429 = mkChange n args pargs ++
415 concatMap (\x -> findCalls x pvs pargs) args
430 concatMap (\x -> findCalls x pvs pargs) args