idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Evaluate with tcinline under Delay

Browse Source 
If we never evaluate under Delay at all, we won't inline interface
methods, which means productive things defined in an interface can never
be today. So, make sure to set the tcinline flag before quoting the
Delayed closure.
This commit is contained in:
Edwin Brady 2020-05-22 13:28:07 +01:00
parent d0af73a295
commit 6d946fed7f
3 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
CHANGELOG.md
View File

@ -17,8 +17,9 @@ Compiler updates:
* 0-multiplicity constructor arguments are now properly erased, not just * 0-multiplicity constructor arguments are now properly erased, not just
given a placeholder null value. given a placeholder null value.
Language extensions: Language changes:
* `total`, `covering` and `partial` flags on functions now have an effect.
* %transform directive, for declaring transformation rules on runtime * %transform directive, for declaring transformation rules on runtime
expressions. Transformation rules are automatically added for top level expressions. Transformation rules are automatically added for top level
implementations of interfaces. implementations of interfaces.

6
src/Core/Normalise.idr
View File

@ -595,8 +595,10 @@ mutual
pure (TDelay fc r tyQ argQ) pure (TDelay fc r tyQ argQ)
where where
toHolesOnly : Closure vs -> Closure vs toHolesOnly : Closure vs -> Closure vs
toHolesOnly (MkClosure _ locs env tm) toHolesOnly (MkClosure opts locs env tm)
= MkClosure withHoles locs env tm = MkClosure (record { holesOnly = True,
argHolesOnly = True } opts)
locs env tm
toHolesOnly c = c toHolesOnly c = c
quoteGenNF q defs bound env (NForce fc r arg args) quoteGenNF q defs bound env (NForce fc r arg args)
= do args' <- quoteArgs q defs bound env args = do args' <- quoteArgs q defs bound env args

2
tests/idris2/total006/expected
View File

@ -1,6 +1,6 @@
1/1: Building Total (Total.idr) 1/1: Building Total (Total.idr)
Main> Main.count is total Main> Main.count is total
Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:1010:1--1015:1 -> Prelude.map Main> Main.badCount is possibly not terminating due to recursive path Main.badCount
Main> Main.process is total Main> Main.process is total
Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
Main> Main.doubleInt is total Main> Main.doubleInt is total