git.iko.soy/Idris-dev
on master help sign in
Add assert_total function

This marks its argument as total, meaning that smaller subexpressions can now be asserted to be total, rather than entire functions. A combination of assert_smaller and assert_total should be used to help the totality checker, rather than %assert_total to mark an entire function as total. The %assert_total option will be removed later.

commit6eee6c8350d806be1d79473278873f9f3a3cb71e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 2 Feb 2014, 01:04 (13 years ago) parent5775f84
5 files changed+45−12
compare with master
unifiedsplit
CHANGELOG+2 libs/prelude/Builtins.idr+7 src/IRTS/Compiler.hs+3 src/Idris/Core/Evaluate.hs+9−3 src/Idris/Coverage.hs+24−9
CHANGELOG+2
@@ -22,6 +22,8 @@ New in 0.9.11:
2222 a pattern for use in totality checking.
2323 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
2424 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))".
2527
2628Internal changes
2729
libs/prelude/Builtins.idr+7
@@ -39,9 +39,16 @@ malloc size x = x -- compiled specially
3939trace_malloc : a -> a
4040trace_malloc x = x -- compiled specially
4141
42+-- Assert to the totality checker than y is always structureally smaller than
43+-- x (which is typically a pattern argument)
4244assert_smaller : a -> a -> a
4345assert_smaller x y = y
4446
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+
4552abstract %assert_total -- need to pretend
4653believe_me : a -> b -- compiled specially as id, use with care!
4754believe_me x = prim__believe_me _ _ x
src/IRTS/Compiler.hs+3
@@ -185,6 +185,9 @@ instance ToIR (TT Name) where
185185 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
186186 a == txt "assert_smaller"
187187 = ir' env arg
188+ | (P _ (UN a) _, [_, arg]) <- unApply tm,
189+ a == txt "assert_total"
190+ = ir' env arg
188191 | (P _ (UN p) _, [_, arg]) <- unApply tm,
189192 p == txt "par"
190193 = do arg' <- ir' env arg
src/Idris/Core/Evaluate.hs+9−3
@@ -101,6 +101,7 @@ simplify :: Context -> Env -> TT Name -> TT Name
101101simplify ctxt env t
102102 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
103103 (sUN "assert_smaller", 0),
104+ (sUN "assert_total", 0),
104105 (sUN "par", 0),
105106 (sUN "prim__syntactic_eq", 0),
106107 (sUN "fork", 0)]
@@ -112,7 +113,6 @@ simplify ctxt env t
112113rt_simplify :: Context -> Env -> TT Name -> TT Name
113114rt_simplify ctxt env t
114115 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
115− (sUN "assert_smaller", 0),
116116 (sUN "par", 0),
117117 (sUN "prim__syntactic_eq", 0),
118118 (sUN "prim_fork", 0)]
@@ -206,6 +206,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
206206 if u then
207207 do let val = lookupDefAcc n (spec || atRepl) ctxt
208208 case val of
209+ [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->
210+ ev ntimes (n:stk) True env tm
209211 [(Function _ tm, Public)] ->
210212 ev ntimes (n:stk) True env tm
211213 [(Function _ tm, Hidden)] ->
@@ -213,7 +215,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
213215 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
214216 return $ VP nt n vty
215217 [(CaseOp ci _ _ _ _ cd, acc)]
216− | (acc /= Frozen) &&
218+ | (acc /= Frozen || sUN "assert_total" `elem` stk) &&
217219 null (fst (cases_totcheck cd)) -> -- unoptimised version
218220 let (ns, tree) = getCases cd in
219221 if blockSimplify ci n stk
@@ -260,6 +262,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
260262-- stk top env (finalise tm)) t
261263-- | otherwise
262264 = 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
263268 ev ntimes stk top env (App f a)
264269 = do f' <- ev ntimes stk False env f
265270 a' <- ev ntimes stk False env a
@@ -313,7 +318,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
313318 do let val = lookupDefAcc n (spec || atRepl) ctxt
314319 case val of
315320 [(CaseOp ci _ _ _ _ cd, acc)]
316− | acc /= Frozen -> -- unoptimised version
321+ | acc /= Frozen || sUN "assert_total" `elem` stk ->
322+ -- unoptimised version
317323 let (ns, tree) = getCases cd in
318324 if blockSimplify ci n stk
319325 then return $ unload env (VP Ref n ty) args
src/Idris/Coverage.hs+24−9
@@ -333,16 +333,17 @@ checkTotality path fc n
333333 else calcTotality path fc n pats
334334 setTotality n t'
335335 addIBC (IBCTotal n t')
336+ return t'
336337 -- if it's not total, it can't reduce, to keep
337338 -- typechecking decidable
338− case t' of
339− p@(Partial _) ->
340− do setAccessibility n Frozen
341− addIBC (IBCAccess n Frozen)
342− logLvl 5 $ "HIDDEN: "
343− ++ show n ++ show p
344− _ -> return ()
345− return t'
339+-- case t' of
340+-- p@(Partial _) ->
341+-- do setAccessibility n Frozen
342+-- addIBC (IBCAccess n Frozen)
343+-- logLvl 5 $ "HIDDEN: "
344+-- ++ show n ++ show p
345+-- _ -> return ()
346+-- return t'
346347 _ -> return $ Total []
347348 x -> return x
348349 case t' of
@@ -373,7 +374,17 @@ checkDeclTotality (fc, n)
373374-- buildSCG (fc, n)
374375-- logLvl 2 $ "Built SCG"
375376 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+
377388
378389-- Calculate the size change graph for this definition
379390
@@ -410,6 +421,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
410421 | (P _ (UN l) _, [_, arg]) <- unApply ap,
411422 l == txt "lazy"
412423 = 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" = []
413428 | (P _ n _, args) <- unApply ap
414429 = mkChange n args pargs ++
415430 concatMap (\x -> findCalls x pvs pargs) args