git.iko.soy/Idris-dev
on master help sign in
Lazy elaboration tweaks

Firstly, never add a Delay to a pattern variable on the lhs, since evaluation isn't forced until it is deconstructed. Secondly, "try" is supposed to return the first error if there's a failure, but this wasn't happening in some cases. In particular, this can make errors from Lazy elaboration surprising, so this is fixed. Fixes #3105

commitd662e2652dfad40f59bae603499a56ea4382d627 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 Apr 2016, 18:51 (11 years ago) parent7688c8d
8 files changed+68−5
compare with master
unifiedsplit
idris.cabal+6 libs/prelude/Language/Reflection/Elab.idr+1 libs/prelude/Prelude/List.idr+1−1 libs/prelude/Prelude/Maybe.idr+1−1 src/Idris/Elab/Term.hs+12−3 test/error007/error007.idr+29 test/error007/expected+15 test/error007/run+3
idris.cabal+6
@@ -467,6 +467,12 @@ Extra-source-files:
467467 test/error005/run
468468 test/error005/*.idr
469469 test/error005/expected
470+ test/error006/run
471+ test/error006/*.idr
472+ test/error006/expected
473+ test/error007/run
474+ test/error007/*.idr
475+ test/error007/expected
470476
471477 test/ffi001/run
472478 test/ffi001/*.idr
libs/prelude/Language/Reflection/Elab.idr+1
@@ -10,6 +10,7 @@ import Prelude.Applicative
1010import Prelude.Basics
1111import Prelude.Bool
1212import Prelude.Functor
13+import Prelude.Interfaces
1314import Prelude.List
1415import Prelude.Maybe
1516import Prelude.Monad
libs/prelude/Prelude/List.idr+1−1
@@ -230,7 +230,7 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
230230||| @ xs the list to recurse over
231231list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b
232232list nil cons [] = nil
233−list nil cons (x::xs) = (Force cons) x xs
233+list nil cons (x::xs) = cons x xs
234234
235235--------------------------------------------------------------------------------
236236-- Building (bigger) lists
libs/prelude/Prelude/Maybe.idr+1−1
@@ -44,7 +44,7 @@ data IsJust : Maybe a -> Type where
4444
4545maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
4646maybe n j Nothing = n
47−maybe n j (Just x) = (Force j) x
47+maybe n j (Just x) = j x
4848
4949||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
5050||| in the case that the `Maybe` value is `Nothing`.
src/Idris/Elab/Term.hs+12−3
@@ -499,8 +499,10 @@ elab ist info emode opts fn tm
499499 trySeq [] = fail "Nothing to try in sequence"
500500 trySeq' deferr [] = proofFail deferr
501501 trySeq' deferr (x : xs)
502− = try' (do elab' ina fc x
503− solveAutos ist fn False) (trySeq' deferr xs) True
502+ = try' (tryCatch (do elab' ina fc x
503+ solveAutos ist fn False)
504+ (\_ -> deferr))
505+ (trySeq' deferr xs) True
504506 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
505507 env <- get_env
506508 compute
@@ -1377,15 +1379,22 @@ elab ist info emode opts fn tm
13771379 fullyElaborated (Proj t _) = fullyElaborated t
13781380 fullyElaborated _ = return ()
13791381
1382+ -- If the goal type is a "Lazy", then try elaborating via 'Delay'
1383+ -- first. We need to do this brute force approach, rather than anything
1384+ -- more precise, since there may be various other ambiguities to resolve
1385+ -- first.
13801386 insertLazy :: PTerm -> ElabD PTerm
13811387 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
13821388 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
13831389 insertLazy (PCoerced t) = return t
1390+ -- Don't add a delay to pattern variables, since they can be forced
1391+ -- on the rhs
1392+ insertLazy t@(PPatvar _ _) | pattern = return t
13841393 insertLazy t =
13851394 do ty <- goal
13861395 env <- get_env
13871396 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
1388− let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]
1397+ let tries = [mkDelay env t, t]
13891398 case tyh of
13901399 P _ (UN l) _ | l == txt "Lazy'"
13911400 -> return (PAlternative [] FirstSuccess tries)
test/error007/error007.idrnew file+29
@@ -0,0 +1,29 @@
1+module Main
2+
3+import CFFI
4+
5+string_from_c : Ptr -> IO String
6+string_from_c str = foreign FFI_C "make_string_2" (Ptr -> IO String) str
7+
8+connection_information_struct : Composite
9+connection_information_struct = STRUCT [I8, PTR, PTR, PTR, I32]
10+
11+send_page : (conn : Ptr) -> (text : String) -> (code : Int) -> IO Int
12+send_page conn page code = pure (the Int 1)
13+
14+-- Error here was using the error from the 'do' block without 'Delay' applied,
15+-- which ended up looking very strange... elaborator should take the first
16+-- error (from the delayed block) when elaborating arguments which may or may
17+-- not need a delay
18+answer_to_connection : Ptr -> Ptr -> IO Int
19+answer_to_connection conn conn_info = do
20+ code_fld <- pure $ (connection_information_struct#4) conn_info
21+ code <- peek I32 code_fld
22+ answer_fld <- pure $ (connection_information_struct#1) conn_info
23+ answer <- peek PTR answer_fld
24+ if answer /= null then do
25+ str <- string_from_c answer
26+ send_page conn str code -- (prim__zextB32_Int code)
27+ else do
28+ send_page conn str (prim__zextB32_Int code)
29+
test/error007/expectednew file+15
@@ -0,0 +1,15 @@
1+error007.idr:26:17:
2+When checking right hand side of answer_to_connection with expected type
3+ IO Int
4+
5+When checking argument code to function Main.send_page:
6+ Type mismatch between
7+ translate I32 (Type of code)
8+ and
9+ Int (Expected type)
10+
11+ Specifically:
12+ Type mismatch between
13+ Bits32
14+ and
15+ Int
test/error007/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --check --nocolour error007.idr -p contrib
3+rm -f *.ibc