d662e26 · Idris-dev · git.iko.soy

idris.cabal+6

compare with master

unifiedsplit

@@ -467,6 +467,12 @@ Extra-source-files:

467 test/error005/run

468 test/error005/*.idr

469 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

470

476

471 test/ffi001/run

477 test/ffi001/run

472 test/ffi001/*.idr

478 test/ffi001/*.idr

libs/prelude/Language/Reflection/Elab.idr+1

@@ -10,6 +10,7 @@ import Prelude.Applicative

10import Prelude.Basics

11import Prelude.Bool

12import Prelude.Functor

13+import Prelude.Interfaces

13import Prelude.List

14import Prelude.List

14import Prelude.Maybe

15import Prelude.Maybe

15import Prelude.Monad

16import 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

230||| @ xs the list to recurse over

231list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b

232list nil cons [] = nil

233−list nil cons (x::xs) = (Force cons) x xs

233+list nil cons (x::xs) = cons x xs

234

235--------------------------------------------------------------------------------

236-- Building (bigger) lists

libs/prelude/Prelude/Maybe.idr+1−1

@@ -44,7 +44,7 @@ data IsJust : Maybe a -> Type where

44

45maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

46maybe n j Nothing = n

47−maybe n j (Just x) = (Force j) x

47+maybe n j (Just x) = j x

48

49||| Convert a `Maybe a` value to an `a` value by providing a default `a` value

50||| 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

499 trySeq [] = fail "Nothing to try in sequence"

500 trySeq' deferr [] = proofFail deferr

501 trySeq' deferr (x : xs)

502− = try' (do elab' ina fc x

502+ = try' (tryCatch (do elab' ina fc x

503− solveAutos ist fn False) (trySeq' deferr xs) True

503+ solveAutos ist fn False)

504+ (\_ -> deferr))

505+ (trySeq' deferr xs) True

504 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

506 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

505 env <- get_env

507 env <- get_env

506 compute

508 compute

@@ -1377,15 +1379,22 @@ elab ist info emode opts fn tm

1377 fullyElaborated (Proj t _) = fullyElaborated t

1379 fullyElaborated (Proj t _) = fullyElaborated t

1378 fullyElaborated _ = return ()

1380 fullyElaborated _ = return ()

1379

1381

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.

1380 insertLazy :: PTerm -> ElabD PTerm

1386 insertLazy :: PTerm -> ElabD PTerm

1381 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1387 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1382 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1388 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1383 insertLazy (PCoerced t) = return t

1389 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

1384 insertLazy t =

1393 insertLazy t =

1385 do ty <- goal

1394 do ty <- goal

1386 env <- get_env

1395 env <- get_env

1387 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

1396 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]

1389 case tyh of

1398 case tyh of

1390 P _ (UN l) _ | l == txt "Lazy'"

1399 P _ (UN l) _ | l == txt "Lazy'"

1391 -> return (PAlternative [] FirstSuccess tries)

1400 -> 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