f1c6e39 · Idris-dev · git.iko.soy

.gitignore+1

compare with master

unifiedsplit

@@ -2,6 +2,7 @@ dist

2cabal-dev/

3.cabal-sandbox

4cabal.sandbox.config

5+cabal.config

5.hsenv

6.hsenv

6*.ibc

7*.ibc

7*.o

8*.o

CHANGELOG+2

@@ -1,5 +1,6 @@

1New in 0.9.18:

2--------------

3+* Add support for bundled toolchains.

3* Strings are now UTF8 encoded in the default back end

4* Strings are now UTF8 encoded in the default back end

4* Idris source files are now assumed to be in UTF8, regardless of locale

5* Idris source files are now assumed to be in UTF8, regardless of locale

5 settings.

6 settings.

@@ -26,6 +27,7 @@ New in 0.9.18:

26* The default Semigroup and Monoid instances for Maybe are now prioritised

27* The default Semigroup and Monoid instances for Maybe are now prioritised

27 choice, keeping the first success as Alternative does. The version that

28 choice, keeping the first success as Alternative does. The version that

28 collects successes is now a named instance.

29 collects successes is now a named instance.

30+* :exec REPL command now takes an optional expression to compile and run/show

29

31

30New in 0.9.17:

32New in 0.9.17:

31--------------

33--------------

CONTRIBUTORS+1

@@ -32,6 +32,7 @@ Adam Sandberg Eriksson

32Seo Sanghyeon

33Benjamin Saunders

34Alexander Shabalin

35+JP Smith

35startling

36startling

36Chetan T

37Chetan T

37Matúš Tejiščák

38Matúš Tejiščák

Setup.hs+24−7

@@ -62,7 +62,7 @@ execOnly flags =

62 case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of

63 Just True -> True

64 Just False -> False

65− Nothing -> True

65+ Nothing -> False

66

67isRelease :: S.ConfigFlags -> Bool

68isRelease flags =

@@ -137,17 +137,33 @@ generateTargetModule verbosity dir targetDir = do

137 ++ " dir <- getDataDir\n"

138 ++ " return (dir ++ \"/\" ++ name)"

139

140+-- a module that has info about existence and location of a bundled toolchain

141+generateToolchainModule verbosity srcDir toolDir = do

142+ let commonContent = "module Tools_idris where\n\n"

143+ let toolContent = case toolDir of

144+ Just dir -> "hasBundledToolchain = True\n" ++

145+ "getToolchainDir = \"" ++ dir ++ "\"\n"

146+ Nothing -> "hasBundledToolchain = False\n" ++

147+ "getToolchainDir = \"\""

148+ let toolPath = srcDir </> "Tools_idris" Px.<.> "hs"

149+ createDirectoryIfMissingVerbose verbosity True srcDir

150+ rewriteFile toolPath (commonContent ++ toolContent)

140

151

141idrisConfigure _ flags _ local = do

152idrisConfigure _ flags _ local = do

142− configureRTS

153+ configureRTS

143− generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))

154+ generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))

144− when (isFreestanding $ configFlags local) (do

155+ if (isFreestanding $ configFlags local)

156+ then (do

157+ toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"

158+ generateToolchainModule verbosity (autogenModulesDir local) toolDir

145− targetDir <- lookupEnv "IDRIS_INSTALL_DIR"

159+ targetDir <- lookupEnv "IDRIS_LIB_DIR"

146 case targetDir of

160 case targetDir of

147 Just d -> generateTargetModule verbosity (autogenModulesDir local) d

161 Just d -> generateTargetModule verbosity (autogenModulesDir local) d

148 Nothing -> error $ "Trying to build freestanding without a target directory."

162 Nothing -> error $ "Trying to build freestanding without a target directory."

149− ++ " Set it by defining IDRIS_INSTALL_DIR.")

163+ ++ " Set it by defining IDRIS_LIB_DIR.")

164+ else

165+ generateToolchainModule verbosity (autogenModulesDir local) Nothing

150− where

166+ where

151 verbosity = S.fromFlag $ S.configVerbosity flags

167 verbosity = S.fromFlag $ S.configVerbosity flags

152 version = pkgVersion . package $ localPkgDescr local

168 version = pkgVersion . package $ localPkgDescr local

153

169

@@ -162,6 +178,7 @@ idrisPreSDist args flags = do

162 let verb = S.fromFlag (S.sDistVerbosity flags)

178 let verb = S.fromFlag (S.sDistVerbosity flags)

163 generateVersionModule verb ("src") True

179 generateVersionModule verb ("src") True

164 generateTargetModule verb "src" "./libs"

180 generateTargetModule verb "src" "./libs"

181+ generateToolchainModule verb "src" Nothing

165 preSDist simpleUserHooks args flags

182 preSDist simpleUserHooks args flags

166

183

167idrisPostSDist args flags desc lbi = do

184idrisPostSDist args flags desc lbi = do

codegen/idris-c/Main.hs+4−1

@@ -14,6 +14,8 @@ import Control.Monad

14

15import Paths_idris

16

17+import Util.System

18+

17data Opts = Opts { inputs :: [FilePath],

19data Opts = Opts { inputs :: [FilePath],

18 interface :: Bool,

20 interface :: Bool,

19 output :: FilePath }

21 output :: FilePath }

@@ -31,7 +33,8 @@ getOpts = do xs <- getArgs

31 process opts [] = opts

33 process opts [] = opts

32

34

33c_main :: Opts -> Idris ()

35c_main :: Opts -> Idris ()

36+c_main opts = do runIO setupBundledCC

34−c_main opts = do elabPrims

37+ elabPrims

35 loadInputs (inputs opts) Nothing

38 loadInputs (inputs opts) Nothing

36 mainProg <- if interface opts

39 mainProg <- if interface opts

37 then liftM Just elabMain

40 then liftM Just elabMain

docs/effects/introduction.rst+1−1

@@ -66,7 +66,7 @@ library:

66 import Effects

67 import Effect.StdIO

68

69− hello : [STDIO] Eff ()

69+ hello : {[STDIO]} Eff ()

70 hello = putStrLn “Hello world!”

71

72 main : IO ()

docs/faq/faq.rst+15

@@ -131,6 +131,21 @@ choice by the developers of Idris, Idris uses the C style convention.

131That is, the names ``Float`` and ``Double`` are used to describe

132single and double precision numbers.

133

134+What is -ffreestanding?

135+=======================

136+

137+The freestanding flag is used to build Idris binaries which have their

138+libs and compiler in a relative path. This is useful for building binaries

139+where the install directory is unknown at build time. When passing this

140+flag, the IDRIS_LIB_DIR environment variable needs to be set to the path

141+where the Idris libs reside relative to the idris executable. The

142+IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,

143+Idris will use that path to find the C compiler.

144+

145+Example:

146+.. code-block::

147+ IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make

148+

134What does the name ‘Idris’ mean?

149What does the name ‘Idris’ mean?

135================================

150================================

136

151

idris.cabal+5

@@ -373,6 +373,10 @@ Extra-source-files:

373 test/effects003/*.idr

374 test/effects003/expected

375 test/effects003/input

376+ test/effects004/run

377+ test/effects004/*.idr

378+ test/effects004/expected

379+ test/effects004/input

376

380

377 test/error001/run

381 test/error001/run

378 test/error001/*.idr

382 test/error001/*.idr

@@ -806,6 +810,7 @@ Library

806 -- Auto Generated

810 -- Auto Generated

807 , Paths_idris

811 , Paths_idris

808 , Version_idris

812 , Version_idris

813+ , Tools_idris

809

814

810 Build-depends: base >=4 && <5

815 Build-depends: base >=4 && <5

811 , annotated-wl-pprint >= 0.5.3 && < 0.6

816 , annotated-wl-pprint >= 0.5.3 && < 0.6

libs/effects/Effect/Exception.idr+4−15

@@ -4,8 +4,8 @@ import Effects

4import System

5import Control.IOExcept

6

7−data Exception : Type -> Effect where

7+data Exception : Type -> Effect where

8− Raise : a -> { () } Exception a b

8+ Raise : a -> sig (Exception a) b

9

10instance Handler (Exception a) Maybe where

11 handle _ (Raise e) k = Nothing

@@ -14,7 +14,7 @@ instance Handler (Exception a) List where

14 handle _ (Raise e) k = []

15

16instance Show a => Handler (Exception a) IO where

17− handle _ (Raise e) k = do printLn e

17+ handle _ (Raise e) k = do print e

18 believe_me (exit 1)

19

20instance Handler (Exception a) (IOExcept a) where

@@ -26,16 +26,5 @@ instance Handler (Exception a) (Either a) where

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

29−raise : a -> { [EXCEPTION a ] } Eff b

29+raise : a -> Eff b [EXCEPTION a]

30raise err = call $ Raise err

31−

32−

33−

34−

35−

36−

37−-- TODO: Catching exceptions mid program?

38−-- probably need to invoke a new interpreter

39−

40−-- possibly add a 'handle' to the Eff language so that an alternative

41−-- handler can be introduced mid interpretation?

libs/effects/Effect/File.idr+16−16

@@ -46,29 +46,29 @@ data FileIO : Effect where

46 ||| @ m The file mode.

47 Open : (fname: String)

48 -> (m : Mode)

49− -> {() ==> {res} if res

49+ -> sig FileIO Bool () (\res => case res of

50− then OpenFile m

50+ True => OpenFile m

51− else ()} FileIO Bool

51+ False => ())

52

53 ||| Close a file.

54 |||

55 ||| Closing a file moves the state from Open to closed.

56− Close : {OpenFile m ==> ()} FileIO ()

56+ Close : sig FileIO () (OpenFile m) ()

57

58 ||| Read a line from the file.

59 |||

60 ||| Only files that are open for reading can be read.

61− ReadLine : {OpenFile Read} FileIO String

61+ ReadLine : sig FileIO String (OpenFile Read)

62

63 ||| Write a string to a file.

64 |||

65 ||| Only file that are open for writing can be written to.

66− WriteString : String -> {OpenFile Write} FileIO ()

66+ WriteString : String -> sig FileIO () (OpenFile Write)

67

68 ||| End of file?

69 |||

70 ||| Only files open for reading can be tested for EOF

71− EOF : {OpenFile Read} FileIO Bool

71+ EOF : sig FileIO Bool (OpenFile Read)

72

73-- ------------------------------------------------------------ [ The Handlers ]

74

@@ -117,31 +117,31 @@ FILE_IO t = MkEff t FileIO

117||| @ m The file mode.

118open : (fname : String)

119 -> (m : Mode)

120− -> { [FILE_IO ()] ==> {result}

121− [FILE_IO (if result

122− then OpenFile m

123− else ())] } Eff Bool

120+ -> Eff Bool [FILE_IO ()]

121+ (\res => [FILE_IO (case res of

122+ True => OpenFile m

123+ False => ())])

124open f m = call $ Open f m

125

126

127||| Close a file.

128−close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()

128+close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]

129close = call $ Close

130

131||| Read a line from the file.

132−readLine : { [FILE_IO (OpenFile Read)] } Eff String

132+readLine : Eff String [FILE_IO (OpenFile Read)]

133readLine = call $ ReadLine

134

135||| Write a string to a file.

136−writeString : String -> { [FILE_IO (OpenFile Write)] } Eff ()

136+writeString : String -> Eff () [FILE_IO (OpenFile Write)]

137writeString str = call $ WriteString str

138

139||| Write a line to a file.

140−writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()

140+writeLine : String -> Eff () [FILE_IO (OpenFile Write)]

141writeLine str = call $ WriteString (str ++ "\n")

142

143||| End of file?

144−eof : { [FILE_IO (OpenFile Read)] } Eff Bool

144+eof : Eff Bool [FILE_IO (OpenFile Read)]

145eof = call $ EOF

146

147-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Random.idr+12−13

@@ -5,28 +5,27 @@ import Data.Vect

5import Data.Fin

6

7data Random : Effect where

8− getRandom : { Integer } Random Integer

8+ getRandom : sig Random Integer Integer

9− setSeed : Integer -> { Integer } Random ()

9+ setSeed : Integer -> sig Random () Integer

10

11−using (m : Type -> Type)

12− instance Handler Random m where

11+instance Handler Random m where

13− handle seed getRandom k

12+ handle seed getRandom k

14− = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

13+ = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

15− k seed' seed'

14+ k seed' seed'

16− handle seed (setSeed n) k = k () n

15+ handle seed (setSeed n) k = k () n

17

16

18RND : EFFECT

17RND : EFFECT

19RND = MkEff Integer Random

18RND = MkEff Integer Random

20

19

21||| Generates a random Integer in a given range

20||| Generates a random Integer in a given range

22−rndInt : Integer -> Integer -> { [RND] } Eff Integer

21+rndInt : Integer -> Integer -> Eff Integer [RND]

23rndInt lower upper = do v <- call $ getRandom

22rndInt lower upper = do v <- call $ getRandom

24 return ((v `prim__sremBigInt` (upper - lower)) + lower)

23 return ((v `prim__sremBigInt` (upper - lower)) + lower)

25

24

26||| Generate a random number in Fin (S `k`)

25||| Generate a random number in Fin (S `k`)

27|||

26|||

28||| Note that rndFin k takes values 0, 1, ..., k.

27||| Note that rndFin k takes values 0, 1, ..., k.

29−rndFin : (k : Nat) -> { [RND] } Eff (Fin (S k))

28+rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]

30rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

29rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

31 return (toFin v)

30 return (toFin v)

32 where toFin : Integer -> Fin (S k)

31 where toFin : Integer -> Fin (S k)

@@ -35,15 +34,15 @@ rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast

35 Nothing => toFin (assert_smaller x (x - cast (S k)))

34 Nothing => toFin (assert_smaller x (x - cast (S k)))

36

35

37||| Select a random element from a vector

36||| Select a random element from a vector

38−rndSelect' : Vect (S k) a -> { [RND] } Eff a

37+rndSelect' : Vect (S k) a -> Eff a [RND]

39rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

38rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

40

39

41||| Select a random element from a list, or Nothing if the list is empty

40||| Select a random element from a list, or Nothing if the list is empty

42−rndSelect : List a -> { [RND] } Eff (Maybe a)

41+rndSelect : List a -> Eff (Maybe a) [RND]

43rndSelect [] = return Nothing

42rndSelect [] = return Nothing

44rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

45

44

46||| Sets the random seed

45||| Sets the random seed

47−srand : Integer -> { [RND] } Eff ()

46+srand : Integer -> Eff () [RND]

48srand n = call $ setSeed n

47srand n = call $ setSeed n

49

48

libs/effects/Effect/Select.idr+2−2

@@ -3,7 +3,7 @@ module Effect.Select

3import Effects

4

5data Selection : Effect where

6− Select : List a -> { () } Selection a

6+ Select : List a -> sig Selection a ()

7

8instance Handler Selection Maybe where

9 handle _ (Select xs) k = tryAll xs where

@@ -18,6 +18,6 @@ instance Handler Selection List where

18SELECT : EFFECT

19SELECT = MkEff () Selection

20

21−select : List a -> { [SELECT] } Eff a

21+select : List a -> Eff a [SELECT]

22select xs = call $ Select xs

23

libs/effects/Effect/State.idr+8−8

@@ -5,8 +5,8 @@ import Effects

5%access public

6

7data State : Effect where

8− Get : { a } State a

8+ Get : sig State a a

9− Put : b -> { a ==> b } State ()

9+ Put : b -> sig State () a b

10

11-- using (m : Type -> Type)

12instance Handler State m where

@@ -16,22 +16,22 @@ instance Handler State m where

16STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19−get : { [STATE x] } Eff x

19+get : Eff x [STATE x]

20get = call $ Get

21

22−put : x -> { [STATE x] } Eff ()

22+put : x -> Eff () [STATE x]

23put val = call $ Put val

24

25−putM : y -> { [STATE x] ==> [STATE y] } Eff ()

25+putM : y -> Eff () [STATE x] [STATE y]

26putM val = call $ Put val

27

28−update : (x -> x) -> { [STATE x] } Eff ()

28+update : (x -> x) -> Eff () [STATE x]

29update f = put (f !get)

30

31−updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff ()

31+updateM : (x -> y) -> Eff () [STATE x] [STATE y]

32updateM f = putM (f !get)

33

34−locally : x -> ({ [STATE x] } Eff t) -> { [STATE y] } Eff t

34+locally : x -> (Eff t [STATE x]) -> Eff t [STATE y]

35locally newst prog = do st <- get

36 putM newst

37 val <- prog

libs/effects/Effect/StdIO.idr+13−24

@@ -9,10 +9,10 @@ import Control.IOExcept

9

10||| The internal representation of StdIO effects

11data StdIO : Effect where

12− PutStr : String -> { () } StdIO ()

12+ PutStr : String -> sig StdIO ()

13− GetStr : { () } StdIO String

13+ GetStr : sig StdIO String

14− PutCh : Char -> { () } StdIO ()

14+ PutCh : Char -> sig StdIO ()

15− GetCh : { () } StdIO Char

15+ GetCh : sig StdIO Char

16

17

18-------------------------------------------------------------

@@ -22,13 +22,13 @@ data StdIO : Effect where

22instance Handler StdIO IO where

23 handle () (PutStr s) k = do putStr s; k () ()

24 handle () GetStr k = do x <- getLine; k x ()

25− handle () (PutCh c) k = do putChar c; k () ()

25+ handle () (PutCh c) k = do putChar c; k () ()

26 handle () GetCh k = do x <- getChar; k x ()

27

28instance Handler StdIO (IOExcept a) where

29 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

30 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

31− handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

31+ handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()

33

34-------------------------------------------------------------

@@ -39,33 +39,22 @@ STDIO : EFFECT

39STDIO = MkEff () StdIO

40

41||| Write a string to standard output.

42−putStr : String -> { [STDIO] } Eff ()

42+putStr : String -> Eff () [STDIO]

43putStr s = call $ PutStr s

44

45−||| Write a string to standard output, terminating with a newline.

46−putStrLn : String -> { [STDIO] } Eff ()

47−putStrLn s = putStr (s ++ "\n")

48−

49||| Write a character to standard output.

45||| Write a character to standard output.

50−putChar : Char -> { [STDIO] } Eff ()

46+putChar : Char -> Eff () [STDIO]

51putChar c = call $ PutCh c

47putChar c = call $ PutCh c

52

48

53−||| Write a character to standard output, terminating with a newline.

49+||| Write a string to standard output, terminating with a newline.

54−putCharLn : Char -> { [STDIO] } Eff ()

50+putStrLn : String -> Eff () [STDIO]

55−putCharLn c = putStrLn (singleton c)

51+putStrLn s = putStr (s ++ "\n")

56

52

57||| Read a string from standard input.

53||| Read a string from standard input.

58−getStr : { [STDIO] } Eff String

54+getStr : Eff String [STDIO]

59getStr = call $ GetStr

55getStr = call $ GetStr

60

56

61||| Read a character from standard input.

57||| Read a character from standard input.

62−getChar : { [STDIO] } Eff Char

58+getChar : Eff Char [STDIO]

63getChar = call $ GetCh

59getChar = call $ GetCh

64

60

65−||| Given a parameter `a` 'show' `a` to standard output.

66−print : Show a => a -> { [STDIO] } Eff ()

67−print a = putStr (show a)

68−

69−||| Given a parameter `a` 'show' `a` to a standard output, terminating with a newline

70−printLn : Show a => a -> { [STDIO] } Eff ()

71−printLn a = putStrLn (show a)

libs/effects/Effect/System.idr+8−8

@@ -8,10 +8,10 @@ import System

8import Control.IOExcept

9

10data System : Effect where

11− Args : { () } System (List String)

11+ Args : sig System (List String)

12− Time : { () } System Int

12+ Time : sig System Int

13− GetEnv : String -> { () } System (Maybe String)

13+ GetEnv : String -> sig System (Maybe String)

14− CSystem : String -> { () } System Int

14+ CSystem : String -> sig System Int

15

16instance Handler System IO where

17 handle () Args k = do x <- getArgs; k x ()

@@ -30,14 +30,14 @@ instance Handler System (IOExcept a) where

30SYSTEM : EFFECT

31SYSTEM = MkEff () System

32

33−getArgs : { [SYSTEM] } Eff (List String)

33+getArgs : Eff (List String) [SYSTEM]

34getArgs = call Args

35

36−time : { [SYSTEM] } Eff Int

36+time : Eff Int [SYSTEM]

37time = call Time

38

39−getEnv : String -> { [SYSTEM] } Eff (Maybe String)

39+getEnv : String -> Eff (Maybe String) [SYSTEM]

40getEnv s = call $ GetEnv s

41

42−system : String -> { [SYSTEM] } Eff Int

42+system : String -> Eff Int [SYSTEM]

43system s = call $ CSystem s

libs/effects/Effects.idr+93−33

@@ -24,6 +24,28 @@ Effect = (x : Type) -> Type -> (x -> Type) -> Type

24data EFFECT : Type where

25 MkEff : Type -> Effect -> EFFECT

26

27+-- 'sig' gives the signature for an effect. There are four versions

28+-- depending on whether there is no resource needed,

29+-- no state change, a non-dependent change,

30+-- or a dependent change. These are easily disambiguated by type.

31+

32+namespace NoResourceEffect

33+ sig : Effect -> Type -> Type

34+ sig e r = e r () (\v => ())

35+

36+namespace NoUpdateEffect

37+ sig : Effect -> (ret : Type) -> (resource : Type) -> Type

38+ sig e r e_in = e r e_in (\v => e_in)

39+

40+namespace UpdateEffect

41+ sig : Effect -> (ret : Type) -> (res_in : Type) -> (res_out : Type) -> Type

42+ sig e r e_in e_out = e r e_in (\v => e_out)

43+

44+namespace DepUpdateEffect

45+ sig : Effect ->

46+ (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type

47+ sig e r e_in e_out = e r e_in e_out

48+

27||| Handler classes describe how an effect `e` is translated to the

49||| Handler classes describe how an effect `e` is translated to the

28||| underlying computation context `m` for execution.

50||| underlying computation context `m` for execution.

29class Handler (e : Effect) (m : Type -> Type) where

51class Handler (e : Effect) (m : Type -> Type) where

@@ -60,6 +82,7 @@ data SubList : List a -> List a -> Type where

60 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

82 Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)

61 Drop : SubList xs ys -> SubList xs (x :: ys)

83 Drop : SubList xs ys -> SubList xs (x :: ys)

62

84

85+%hint

63subListId : SubList xs xs

86subListId : SubList xs xs

64subListId {xs = Nil} = SubNil

87subListId {xs = Nil} = SubNil

65subListId {xs = x :: xs} = Keep subListId

88subListId {xs = x :: xs} = Keep subListId

@@ -133,26 +156,61 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs

133||| @ x The return type of the result.

156||| @ x The return type of the result.

134||| @ es The list of allowed side-effects.

157||| @ es The list of allowed side-effects.

135||| @ ce Function to compute a new list of allowed side-effects.

158||| @ ce Function to compute a new list of allowed side-effects.

136−data Eff : (x : Type)

159+data EffM : (m : Type -> Type) -> (x : Type)

137− -> (es : List EFFECT)

160+ -> (es : List EFFECT)

138− -> (ce : x -> List EFFECT) -> Type where

161+ -> (ce : x -> List EFFECT) -> Type where

139− value : (val : a) -> Eff a (xs val) xs

162+ value : (val : a) -> EffM m a (xs val) xs

140− ebind : Eff a xs xs' ->

163+ ebind : EffM m a xs xs' ->

141− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

164+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''

142 callP : (prf : EffElem e a xs) ->

165 callP : (prf : EffElem e a xs) ->

143 (eff : e t a b) ->

166 (eff : e t a b) ->

144− Eff t xs (\v => updateResTy v xs prf eff)

167+ EffM m t xs (\v => updateResTy v xs prf eff)

145

168

146 liftP : (prf : SubList ys xs) ->

169 liftP : (prf : SubList ys xs) ->

147− Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)

170+ EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)

171+

172+ new : Handler e' m => (e : EFFECT) -> resTy ->

173+ {auto prf : e = MkEff resTy e'} ->

174+ EffM m t (e :: es) (\v => e :: es) ->

175+ EffM m t es (\v => es)

148

176

149 (:-) : (l : ty) ->

177 (:-) : (l : ty) ->

150− Eff t [x] xs' -> -- [x] (\v => xs) ->

178+ EffM m t [x] xs' -> -- [x] (\v => xs) ->

151− Eff t [l ::: x] (\v => map (l :::) (xs' v))

179+ EffM m t [l ::: x] (\v => map (l :::) (xs' v))

180+

181+-- Some type synonyms, so we don't always have to write EffM in full

182+

183+namespace SimpleEff

184+ -- Simple effects, no updates

185+ Eff : (x : Type) -> (es : List EFFECT) -> Type

186+ Eff x es = {m : Type -> Type} -> EffM m x es (\v => es)

187+

188+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT) -> Type

189+ EffT m x es = EffM m x es (\v => es)

190+

191+namespace TransEff

192+ -- Dependent effects, updates not dependent on result

193+ Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type

194+ Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)

195+

196+ EffT : (m : Type -> Type) ->

197+ (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type

198+ EffT m x es ce = EffM m x es (\_ => ce)

199+

200+namespace DepEff

201+ -- Dependent effects, updates dependent on result

202+ Eff : (x : Type) -> (es : List EFFECT)

203+ -> (ce : x -> List EFFECT) -> Type

204+ Eff x es ce = {m : Type -> Type} -> EffM m x es ce

205+

206+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)

207+ -> (ce : x -> List EFFECT) -> Type

208+ EffT m x es ce = EffM m x es ce

209+

152

210

153%no_implicit

211%no_implicit

154−(>>=) : Eff a xs xs' ->

212+(>>=) : EffM m a xs xs' ->

155− ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

213+ ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''

156(>>=) = ebind

214(>>=) = ebind

157

215

158-- namespace SimpleBind

216-- namespace SimpleBind

@@ -161,29 +219,29 @@ data Eff : (x : Type)

161-- (>>=) = ebind

219-- (>>=) = ebind

162

220

163||| Run a subprogram which results in an effect state the same as the input.

221||| Run a subprogram which results in an effect state the same as the input.

164−staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)

222+staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)

165staticEff = id

223staticEff = id

166

224

167||| Explicitly give the expected set of result effects for an effectful

225||| Explicitly give the expected set of result effects for an effectful

168||| operation.

226||| operation.

169−toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')

227+toEff : .(xs' : List EFFECT) -> EffM m a xs (\v => xs') -> EffM m a xs (\v => xs')

170toEff xs' = id

228toEff xs' = id

171

229

172−return : a -> Eff a xs (\v => xs)

230+return : a -> EffM m a xs (\v => xs)

173return x = value x

231return x = value x

174

232

175-- ------------------------------------------------------ [ for idiom brackets ]

233-- ------------------------------------------------------ [ for idiom brackets ]

176

234

177infixl 2 <*>

235infixl 2 <*>

178

236

179−pure : a -> Eff a xs (\v => xs)

237+pure : a -> EffM m a xs (\v => xs)

180pure = value

238pure = value

181

239

182−pureM : (val : a) -> Eff a (xs val) xs

240+pureM : (val : a) -> EffM m a (xs val) xs

183pureM = value

241pureM = value

184

242

185−(<*>) : Eff (a -> b) xs (\v => xs) ->

243+(<*>) : EffM m (a -> b) xs (\v => xs) ->

186− Eff a xs (\v => xs) -> Eff b xs (\v => xs)

244+ EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)

187(<*>) prog v = do fn <- prog

245(<*>) prog v = do fn <- prog

188 arg <- v

246 arg <- v

189 return (fn arg)

247 return (fn arg)

@@ -203,7 +261,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

203-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

261-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

204-- updates can be propagated even through failing computations?

262-- updates can be propagated even through failing computations?

205

263

206−eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

264+eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

207eff env (value x) k = k x env

265eff env (value x) k = k x env

208eff env (prog `ebind` c) k

266eff env (prog `ebind` c) k

209 = eff env prog (\p', env' => eff env' (c p') k)

267 = eff env prog (\p', env' => eff env' (c p') k)

@@ -211,6 +269,8 @@ eff env (callP prf effP) k = execEff env prf effP k

211eff env (liftP prf effP) k

269eff env (liftP prf effP) k

212 = let env' = dropEnv env prf in

270 = let env' = dropEnv env prf in

213 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

271 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

272+eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k

273+ = eff (res :: env) effP (\p', (val :: envk) => k p' envk)

214-- FIXME:

274-- FIXME:

215-- xs is needed explicitly because otherwise the pattern binding for

275-- xs is needed explicitly because otherwise the pattern binding for

216-- 'l' appears too late. Solution seems to be to reorder patterns at the

276-- 'l' appears too late. Solution seems to be to reorder patterns at the

@@ -235,14 +295,14 @@ call : {a, b: _} -> {e : Effect} ->

235 (eff : e t a b) ->

295 (eff : e t a b) ->

236 {default tactics { search 100; }

296 {default tactics { search 100; }

237 prf : EffElem e a xs} ->

297 prf : EffElem e a xs} ->

238− Eff t xs (\v => updateResTy v xs prf eff)

298+ EffM m t xs (\v => updateResTy v xs prf eff)

239call e {prf} = callP prf e

299call e {prf} = callP prf e

240

300

241implicit

301implicit

242−lift : Eff t ys ys' ->

302+lift : EffM m t ys ys' ->

243 {default tactics { search 100; }

303 {default tactics { search 100; }

244 prf : SubList ys xs} ->

304 prf : SubList ys xs} ->

245− Eff t xs (\v => updateWith (ys' v) xs prf)

305+ EffM m t xs (\v => updateWith (ys' v) xs prf)

246lift e {prf} = liftP prf e

306lift e {prf} = liftP prf e

247

307

248

308

@@ -255,7 +315,7 @@ lift e {prf} = liftP prf e

255|||

315|||

256||| @prog The effectful program to run.

316||| @prog The effectful program to run.

257run : Applicative m => {default MkDefaultEnv env : Env m xs}

317run : Applicative m => {default MkDefaultEnv env : Env m xs}

258− -> (prog : Eff a xs xs') -> m a

318+ -> (prog : EffM m a xs xs') -> m a

259run {env} prog = eff env prog (\r, env => pure r)

319run {env} prog = eff env prog (\r, env => pure r)

260

320

261||| Run an effectful program in the identity context.

321||| Run an effectful program in the identity context.

@@ -264,7 +324,7 @@ run {env} prog = eff env prog (\r, env => pure r)

264||| The `env` argument is implicit and initialised automatically.

324||| The `env` argument is implicit and initialised automatically.

265|||

325|||

266||| @prog The effectful program to run.

326||| @prog The effectful program to run.

267−runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff a xs xs') -> a

327+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : EffM id a xs xs') -> a

268runPure {env} prog = eff env prog (\r, env => r)

328runPure {env} prog = eff env prog (\r, env => r)

269

329

270||| Run an effectful program in a given context `m` with a default value for the environment.

330||| Run an effectful program in a given context `m` with a default value for the environment.

@@ -273,7 +333,7 @@ runPure {env} prog = eff env prog (\r, env => r)

273|||

333|||

274||| @env The environment to use.

334||| @env The environment to use.

275||| @prog The effectful program to run.

335||| @prog The effectful program to run.

276−runInit : Applicative m => (env : Env m xs) -> (prog : Eff a xs xs') -> m a

336+runInit : Applicative m => (env : Env m xs) -> (prog : EffM m a xs xs') -> m a

277runInit env prog = eff env prog (\r, env => pure r)

337runInit env prog = eff env prog (\r, env => pure r)

278

338

279||| Run an effectful program with a given default value for the environment.

339||| Run an effectful program with a given default value for the environment.

@@ -282,31 +342,31 @@ runInit env prog = eff env prog (\r, env => pure r)

282|||

342|||

283||| @env The environment to use.

343||| @env The environment to use.

284||| @prog The effectful program to run.

344||| @prog The effectful program to run.

285−runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a

345+runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a

286runPureInit env prog = eff env prog (\r, env => r)

346runPureInit env prog = eff env prog (\r, env => r)

287

347

288−runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a

348+runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a

289runWith inj env prog = eff env prog (\r, env => inj r)

349runWith inj env prog = eff env prog (\r, env => inj r)

290

350

291−runEnv : Applicative m => Env m xs -> Eff a xs xs' ->

351+runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->

292 m (x : a ** Env m (xs' x))

352 m (x : a ** Env m (xs' x))

293runEnv env prog = eff env prog (\r, env => pure (r ** env))

353runEnv env prog = eff env prog (\r, env => pure (r ** env))

294

354

295-- ----------------------------------------------- [ some higher order things ]

355-- ----------------------------------------------- [ some higher order things ]

296

356

297−mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)

357+mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)

298mapE f [] = pure []

358mapE f [] = pure []

299mapE f (x :: xs) = [| f x :: mapE f xs |]

359mapE f (x :: xs) = [| f x :: mapE f xs |]

300

360

301

361

302−mapVE : (a -> {xs} Eff b) ->

362+mapVE : (a -> {xs} EffM m b) ->

303 Vect n a ->

363 Vect n a ->

304− {xs} Eff (Vect n b)

364+ {xs} EffM m (Vect n b)

305mapVE f [] = pure []

365mapVE f [] = pure []

306mapVE f (x :: xs) = [| f x :: mapVE f xs |]

366mapVE f (x :: xs) = [| f x :: mapVE f xs |]

307

367

308

368

309−when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()

369+when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()

310when True e = Force e

370when True e = Force e

311when False e = pure ()

371when False e = pure ()

312

372

libs/prelude/IO.idr+3−1

@@ -152,13 +152,15 @@ FFI_C = MkFFI C_Types String String

152IO : Type -> Type

153IO = IO' FFI_C

154

155+-- Cannot be relaxed as is used by type providers and they expect IO a

156+-- in the first argument.

155run__provider : IO a -> PrimIO a

157run__provider : IO a -> PrimIO a

156run__provider (MkIO f) = f (TheWorld prim__TheWorld)

158run__provider (MkIO f) = f (TheWorld prim__TheWorld)

157

159

158prim_fork : PrimIO () -> PrimIO Ptr

160prim_fork : PrimIO () -> PrimIO Ptr

159prim_fork x = prim_io_return prim__vm -- compiled specially

161prim_fork x = prim_io_return prim__vm -- compiled specially

160

162

161−fork : IO () -> IO Ptr

163+fork : IO' l () -> IO' l Ptr

162fork (MkIO f) = MkIO (\w => prim_io_bind

164fork (MkIO f) = MkIO (\w => prim_io_bind

163 (prim_fork (prim_io_bind (f w)

165 (prim_fork (prim_io_bind (f w)

164 (\ x => prim_io_return x)))

166 (\ x => prim_io_return x)))

libs/prelude/Prelude.idr+1−1

@@ -526,7 +526,7 @@ validFile (FHandle h) = do x <- nullPtr h

526||| @ test the condition of the loop

527||| @ body the loop body

528partial -- obviously

529−while : (test : IO Bool) -> (body : IO ()) -> IO ()

529+while : (test : IO' l Bool) -> (body : IO' l ()) -> IO' l ()

530while t b = do v <- t

531 if v then do b

532 while t b

main/Main.hs+2

@@ -29,6 +29,7 @@ import Idris.CmdOptions

29import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )

30

31import Util.DynamicLinker

32+import Util.System

32

33

33import Pkg.Package

34import Pkg.Package

34

35

@@ -43,6 +44,7 @@ main = do opts <- runArgParser

43

44

44runIdris :: [Opt] -> Idris ()

45runIdris :: [Opt] -> Idris ()

45runIdris opts = do

46runIdris opts = do

47+ runIO setupBundledCC

46 when (ShowIncs `elem` opts) $ runIO showIncs

48 when (ShowIncs `elem` opts) $ runIO showIncs

47 when (ShowLibs `elem` opts) $ runIO showLibs

49 when (ShowLibs `elem` opts) $ runIO showLibs

48 when (ShowLibdir `elem` opts) $ runIO showLibdir

50 when (ShowLibdir `elem` opts) $ runIO showLibdir

src/IRTS/Compiler.hs+5−1

@@ -51,8 +51,12 @@ compile codegen f mtm

51 = do checkMVs -- check for undefined metavariables

52 checkTotality -- refuse to compile if there are totality problems

53 exports <- findExports

54+ let rootNames = case mtm of

55+ Nothing -> []

56+ Just t -> freeNames t

54

57

55− reachableNames <- performUsageAnalysis (getExpNames exports)

58+ reachableNames <- performUsageAnalysis

59+ (rootNames ++ getExpNames exports)

56 maindef <- case mtm of

60 maindef <- case mtm of

57 Nothing -> return []

61 Nothing -> return []

58 Just tm -> do md <- irMain tm

62 Just tm -> do md <- irMain tm

src/IRTS/Lang.hs+1−1

@@ -132,7 +132,7 @@ data LiftState = LS Name Int [(Name, LDecl)]

132

133lname (NS n x) i = NS (lname n i) x

134lname (UN n) i = MN i n

135−lname x i = sMN i (show x)

135+lname x i = sMN i (show x ++ "_lam")

136

137liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]

138liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs

src/Idris/AbsSyntaxTree.hs+29−23

@@ -369,7 +369,7 @@ data Command = Quit

369 | ModImport String

370 | Edit

371 | Compile Codegen String

372− | Execute

372+ | Execute PTerm

373 | ExecVal PTerm

374 | Metavars

375 | Prove Name

@@ -1633,6 +1633,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1633 basename (NS n _) = basename n

1634 basename n = n

1635

1636+ slist' _ _ e

1637+ | containsHole e = Nothing

1636 slist' p bnd (PApp _ (PRef _ nil) _)

1638 slist' p bnd (PApp _ (PRef _ nil) _)

1637 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1639 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1638 slist' p bnd (PRef _ nil)

1640 slist' p bnd (PRef _ nil)

@@ -1902,31 +1904,35 @@ allNamesIn tm = nub $ ni [] tm

1902 niTacImp env (TacImp _ _ scr) = ni env scr

1904 niTacImp env (TacImp _ _ scr) = ni env scr

1903 niTacImp _ _ = []

1905 niTacImp _ _ = []

1904

1906

1907+

1905-- Return all names defined in binders in the given term

1908-- Return all names defined in binders in the given term

1906boundNamesIn :: PTerm -> [Name]

1909boundNamesIn :: PTerm -> [Name]

1907−boundNamesIn tm = nub $ ni tm

1910+boundNamesIn tm = S.toList (ni S.empty tm)

1908 where -- TODO THINK Added niTacImp, but is it right?

1911 where -- TODO THINK Added niTacImp, but is it right?

1909− ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

1912+ ni set (PApp _ f as) = niTms (ni set f) (map getTm as)

1910− ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

1913+ ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)

1911− ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

1914+ ni set (PCase _ c os) = niTms (ni set c) (map snd os)

1912− ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)

1915+ ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc

1913− ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1916+ ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

1914− ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1917+ ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

1915− ni (PEq _ _ _ l r) = ni l ++ ni r

1918+ ni set (PEq _ _ _ l r) = ni (ni set l) r

1916− ni (PRewrite _ l r _) = ni l ++ ni r

1919+ ni set (PRewrite _ l r _) = ni (ni set l) r

1917− ni (PTyped l r) = ni l ++ ni r

1920+ ni set (PTyped l r) = ni (ni set l) r

1918− ni (PPair _ _ l r) = ni l ++ ni r

1921+ ni set (PPair _ _ l r) = ni (ni set l) r

1919− ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r

1922+ ni set (PDPair _ _ (PRef _ n) t r) = ni (ni set t) r

1920− ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r

1923+ ni set (PDPair _ _ l t r) = ni (ni (ni set l) t) r

1921− ni (PAlternative a as) = concatMap (ni) as

1924+ ni set (PAlternative a as) = niTms set as

1922− ni (PHidden tm) = ni tm

1925+ ni set (PHidden tm) = ni set tm

1923− ni (PUnifyLog tm) = ni tm

1926+ ni set (PUnifyLog tm) = ni set tm

1924− ni (PDisamb _ tm) = ni tm

1927+ ni set (PDisamb _ tm) = ni set tm

1925− ni (PNoImplicits tm) = ni tm

1928+ ni set (PNoImplicits tm) = ni set tm

1926− ni _ = []

1929+ ni set _ = set

1927−

1930+

1931+ niTms set [] = set

1932+ niTms set (x : xs) = niTms (ni set x) xs

1933+

1928− niTacImp (TacImp _ _ scr) = ni scr

1934+ niTacImp set (TacImp _ _ scr) = ni set scr

1929− niTacImp _ = []

1935+ niTacImp set _ = set

1930

1936

1931-- Return names which are valid implicits in the given term (type).

1937-- Return names which are valid implicits in the given term (type).

1932implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

1938implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

src/Idris/Core/Elaborate.hs+1

@@ -759,6 +759,7 @@ try' t1 t2 proofSearch

759 = do s <- get

760 ps <- get_probs

761 ulog <- getUnifyLog

762+ ivs <- get_instances

762 case prunStateT 999999 False ps t1 s of

763 case prunStateT 999999 False ps t1 s of

763 OK ((v, _, _), s') -> do put s'

764 OK ((v, _, _), s') -> do put s'

764 return $! v

765 return $! v

src/Idris/Core/ProofTerm.hs+1−1

@@ -112,7 +112,7 @@ refocus' (Just n) pt@(PT path env tm ups)

112 -- First look for the hole in the proof term as-is

113 | Just (p', env', tm') <- findHole n env tm

114 = PT (replaceTop p' path) env' tm' ups

115− -- Next apply the updates, and look for the hole in the resulting term

115+ -- If it's not there, rebuild and look from the top

116 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))

117 = PT p' env' tm' []

118 | otherwise = pt

src/Idris/Core/TT.hs+1

@@ -426,6 +426,7 @@ showCG (SN s) = showCG' s

426 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

427 showCG' (CaseN c) = showCG c ++ "_case"

428 showCG' (ElimN sn) = showCG sn ++ "_elim"

429+ showCG' (InstanceCtorN n) = showCG n ++ "_ictor"

429showCG NErased = "_"

430showCG NErased = "_"

430

431

432

src/Idris/Elab/Class.hs+14−5

@@ -175,8 +175,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

175 let lhs = PApp fc (PRef fc cfn) [pconst capp]

176 let rhs = PResolveTC (fileFC "HACK")

177 let ty = PPi constraint cnm c con

178− iLOG (showTmImpls ty)

178+ logLvl 2 ("Dictionary constraint: " ++ showTmImpls ty)

179− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

179+ logLvl 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

180 i <- getIState

181 let conn = case con of

182 PRef _ n -> n

@@ -193,16 +193,16 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

193 -- Generate a top level function which looks up a method in a given

194 -- dictionary (this is inlinable, always)

195 tfun cn c syn all (m, (doc, o, ty))

196− = do let ty' = insertConstraint c ty

196+ = do let ty' = expandMethNS syn (insertConstraint c ty)

197 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

198 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

199 let margs = getMArgs ty

200 let anames = map (\x -> sMN x "arg") [0..]

201 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

203− iLOG (showTmImpls ty')

203+ logLvl 2 ("Top level type: " ++ showTmImpls ty')

204 iLOG (show (m, ty', capp, margs))

205− iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

205+ logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

206 return [PTy doc [] syn fc o m ty',

207 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

208

@@ -236,6 +236,15 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

236 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

237 toExp ns e sc = sc

238

239+-- In a top level type for a method, expand all the method names namespaces

240+-- so that we don't have to disambiguate later

241+expandMethNS :: SyntaxInfo

242+ -> PTerm -> PTerm

243+expandMethNS syn = mapPT expand

244+ where

245+ expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n

246+ expand t = t

247+

239findDets :: Name -> [Name] -> Idris [Int]

248findDets :: Name -> [Name] -> Idris [Int]

240findDets n ns =

249findDets n ns =

241 do i <- getIState

250 do i <- getIState

src/Idris/Elab/Value.hs+16−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

3+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms, elabExec) where

4

5import Idris.AbsSyntax

6import Idris.ASTUtils

@@ -114,3 +114,18 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

114 then Example tm

115 else Checked tm

116 | otherwise = Unchecked

117+

118+-- Try running the term directly (as IO ()), then printing it as an Integer

119+-- (as a default numeric tye), then printing it as any Showable thing

120+elabExec :: FC -> PTerm -> PTerm

121+elabExec fc tm = runtm (PAlternative False

122+ [printtm (PApp fc (PRef fc (sUN "the"))

123+ [pexp (PConstant (AType (ATInt ITBig))), pexp tm]),

124+ tm,

125+ printtm tm

126+ ])

127+ where

128+ runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

129+ printtm t = PApp fc (PRef fc (sUN "printLn"))

130+ [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]

131+

src/Idris/Erasure.hs+3−16

@@ -66,13 +66,11 @@ type Vars = Map Name VarInfo

66-- Perform usage analysis, write the relevant information in the internal

67-- structures, returning the list of reachable names.

68performUsageAnalysis :: [Name] -> Idris [Name]

69−performUsageAnalysis roots = do

69+performUsageAnalysis startNames = do

70 ctx <- tt_ctxt <$> getIState

71− startNames <- getStartNames <$> getIState

72−

73 case startNames of

71 case startNames of

74− Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

72+ [] -> return [] -- no main -> not compiling -> reachability irrelevant

75− Right main -> do

73+ main -> do

76 ci <- idris_classes <$> getIState

74 ci <- idris_classes <$> getIState

77 cg <- idris_callgraph <$> getIState

75 cg <- idris_callgraph <$> getIState

78 opt <- idris_optimisation <$> getIState

76 opt <- idris_optimisation <$> getIState

@@ -107,17 +105,6 @@ performUsageAnalysis roots = do

107

105

108 return $ S.toList reachableNames

106 return $ S.toList reachableNames

109 where

107 where

110− getStartNames :: IState -> Either Err [Name]

111− getStartNames ist

112− = case lookupCtxtName n (idris_implicits ist) of

113− [(n', _)] -> Right (n' : roots)

114− [] -> if null roots

115− then Left (NoSuchVariable n)

116− else Right roots

117− more -> Left (CantResolveAlts (map fst more))

118− where

119− n = sNS (sUN "main") ["Main"]

120−

121 indent = (" " ++)

108 indent = (" " ++)

122

109

123 fmtItem :: (Cond, DepSet) -> String

110 fmtItem :: (Cond, DepSet) -> String

src/Idris/IdrisDoc.hs+2−2

@@ -420,7 +420,7 @@ createIndex nss out =

420 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

421 H.h1 $ "Namespaces"

422 H.ul ! class_ "names" $ do

423− let path ns = "docs" </> genRelNsPath ns "html"

423+ let path ns = "docs" ++ "/" ++ genRelNsPath ns "html"

424 item ns = do let n = toHtml $ nsName2Str ns

425 link = toValue $ path ns

426 H.li $ H.a ! href link ! class_ "code" $ n

@@ -663,7 +663,7 @@ existingNamespaces :: FilePath -- ^ The base directory containing the

663 -- namespace pages

664 -> IO (S.Set NsName)

665existingNamespaces out = do

666− let docs = out </> "docs"

666+ let docs = out ++ "/" ++ "docs"

667 str2Ns s | s == rootNsStr = []

668 str2Ns s = reverse $ T.splitOn (T.singleton '.') (txt s)

669 toNs fp = do isFile <- doesFileExist $ docs </> fp

src/Idris/ParseExpr.hs+58−41

@@ -1,5 +1,4 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2−{-# OPTIONS_GHC -O0 #-}

3module Idris.ParseExpr where

2module Idris.ParseExpr where

4

3

5import Prelude hiding (pi)

4import Prelude hiding (pi)

@@ -869,49 +868,67 @@ bindsymbol opts st syn

869 = do symbol "->"

868 = do symbol "->"

870 return (Exp opts st False)

869 return (Exp opts st False)

871

870

871+explicitPi opts st syn

872+ = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

873+ binder <- bindsymbol opts st syn

874+ sc <- expr syn

875+ return (bindList (PPi binder) xt sc)

876+

877+autoImplicit opts st syn

878+ = do reserved "auto"

879+ when (st == Static) $ fail "auto implicits can not be static"

880+ xt <- typeDeclList syn

881+ lchar '}'

882+ symbol "->"

883+ sc <- expr syn

884+ return (bindList (PPi

885+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)

886+

887+defaultImplicit opts st syn = do

888+ reserved "default"

889+ when (st == Static) $ fail "default implicits can not be static"

890+ ist <- get

891+ script' <- simpleExpr syn

892+ let script = debindApp syn . desugar syn ist $ script'

893+ xt <- typeDeclList syn

894+ lchar '}'

895+ symbol "->"

896+ sc <- expr syn

897+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

898+

899+normalImplicit opts st syn = do

900+ xt <- typeDeclList syn <* lchar '}'

901+ symbol "->"

902+ cs <- constraintList syn

903+ sc <- expr syn

904+ let (im,cl)

905+ = if implicitAllowed syn

906+ then (Imp opts st False Nothing,

907+ constraint)

908+ else (Imp opts st False (Just (Impl False)),

909+ Imp opts st False (Just (Impl True)))

910+ return (bindList (PPi im) xt

911+ (bindList (PPi cl) cs sc))

912+

913+implicitPi opts st syn =

914+ autoImplicit opts st syn

915+ <|> defaultImplicit opts st syn

916+ <|> normalImplicit opts st syn

917+

918+unboundPi opts st syn = do

919+ x <- opExpr syn

920+ (do binder <- bindsymbol opts st syn

921+ sc <- expr syn

922+ return (PPi binder (sUN "__pi_arg") x sc))

923+ <|> return x

924+

872pi :: SyntaxInfo -> IdrisParser PTerm

925pi :: SyntaxInfo -> IdrisParser PTerm

873pi syn =

926pi syn =

874 do opts <- piOpts syn

927 do opts <- piOpts syn

875 st <- static

928 st <- static

876− (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

877− binder <- bindsymbol opts st syn

929+ explicitPi opts st syn

878− sc <- expr syn

930+ <|> try (do lchar '{'; implicitPi opts st syn)

879− return (bindList (PPi binder) xt sc)) <|> (do

931+ <|> unboundPi opts st syn

880− (do try (lchar '{' *> reserved "auto")

881− when (st == Static) $ fail "auto type constraints can not be static"

882− xt <- typeDeclList syn

883− lchar '}'

884− symbol "->"

885− sc <- expr syn

886− return (bindList (PPi

887− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

888− try (lchar '{' *> reserved "default")

889− when (st == Static) $ fail "default tactic constraints can not be static"

890− ist <- get

891− script' <- simpleExpr syn

892− let script = debindApp syn . desugar syn ist $ script'

893− xt <- typeDeclList syn

894− lchar '}'

895− symbol "->"

896− sc <- expr syn

897− return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

898− <|> (do xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')

899− symbol "->"

900− cs <- constraintList syn

901− sc <- expr syn

902− let (im,cl)

903− = if implicitAllowed syn

904− then (Imp opts st False Nothing,

905− constraint)

906− else (Imp opts st False (Just (Impl False)),

907− Imp opts st False (Just (Impl True)))

908− return (bindList (PPi im) xt

909− (bindList (PPi cl) cs sc))))

910− <|> (do x <- opExpr syn

911− (do binder <- bindsymbol opts st syn

912− sc <- expr syn

913− return (PPi binder (sUN "__pi_arg") x sc))

914− <|> return x)

915 <?> "dependent type signature"

932 <?> "dependent type signature"

916

933

917{- | Parses Possible Options for Pi Expressions

934{- | Parses Possible Options for Pi Expressions

@@ -944,7 +961,7 @@ constraintList1 syn = try (do lchar '('

944 lchar ')'

961 lchar ')'

945 reservedOp "=>"

962 reservedOp "=>"

946 return tys)

963 return tys)

947− <|> try (do t <- expr (disallowImp syn)

964+ <|> try (do t <- opExpr (disallowImp syn)

948 reservedOp "=>"

965 reservedOp "=>"

949 return [(defname, t)])

966 return [(defname, t)])

950 <?> "type constraint list"

967 <?> "type constraint list"

src/Idris/Parser.hs+1−1

@@ -1365,7 +1365,7 @@ loadSource lidr f toline

1365 -- process and check module aliases

1366 let modAliases = M.fromList

1367 [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports]

1368− prep = map T.pack . reverse . Spl.splitOn "/"

1368+ prep = map T.pack . reverse . Spl.splitOn [pathSeparator]

1369 aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports]

1370 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames

1371 case map head . filter ((/= 1) . length) $ histogram of

src/Idris/ProofSearch.hs+36−23

@@ -15,6 +15,7 @@ import Idris.Error

15import Control.Applicative ((<$>))

16import Control.Monad

17import Control.Monad.State.Strict

18+import qualified Data.Set as S

18import Data.List

19import Data.List

19import Debug.Trace

20import Debug.Trace

20

21

@@ -91,7 +92,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

91 if ambigok || argsok then

92 if ambigok || argsok then

92 case lookupCtxt nroot (idris_tyinfodata ist) of

93 case lookupCtxt nroot (idris_tyinfodata ist) of

93 [TISolution ts] -> findInferredTy ts

94 [TISolution ts] -> findInferredTy ts

94− _ -> psRec rec maxDepth []

95+ _ -> psRec rec maxDepth [] S.empty

95 else autoArg (sUN "auto") -- not enough info in the type yet

96 else autoArg (sUN "auto") -- not enough info in the type yet

96 where

97 where

97 findInferredTy (t : _) = elab (delab ist (toUN t))

98 findInferredTy (t : _) = elab (delab ist (toUN t))

@@ -134,13 +135,21 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

134 -- (so we don't try a pointless application of something to itself,

135 -- (so we don't try a pointless application of something to itself,

135 -- which obviously won't work anyway but might lead us on a wild

136 -- which obviously won't work anyway but might lead us on a wild

136 -- goose chase...)

137 -- goose chase...)

138+ -- Also keep track of the types we've proved so far in this branch

139+ -- (if we get back to one we've been to before, we're just in a cycle and

140+ -- that's no use)

141+ psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()

137− psRec _ 0 locs | fromProver = cantSolveGoal

142+ psRec _ 0 locs tys | fromProver = cantSolveGoal

138− psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"

143+ psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"

139− psRec False d locs = tryCons d locs hints

144+ psRec False d locs tys = tryCons d locs tys hints

140− psRec True d locs

145+ psRec True d locs tys

141 = do compute

146 = do compute

147+ ty <- goal

148+ when (S.member ty tys) $ fail "Been here before"

149+ let tys' = S.insert ty tys

142 try' (trivial elab ist)

150 try' (trivial elab ist)

143− (try' (try' (resolveByCon (d - 1) locs) (resolveByLocals (d - 1) locs)

151+ (try' (try' (resolveByCon (d - 1) locs tys')

152+ (resolveByLocals (d - 1) locs tys')

144 True)

153 True)

145 -- if all else fails, make a new metavariable

154 -- if all else fails, make a new metavariable

146 (if fromProver

155 (if fromProver

@@ -151,7 +160,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

151 getFn d (Just f) | d < maxDepth-1 = [f]

160 getFn d (Just f) | d < maxDepth-1 = [f]

152 | otherwise = []

161 | otherwise = []

153

162

154− resolveByCon d locs

163+ resolveByCon d locs tys

155 = do t <- goal

164 = do t <- goal

156 let (f, _) = unApply t

165 let (f, _) = unApply t

157 case f of

166 case f of

@@ -160,7 +169,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

160 Nothing -> []

169 Nothing -> []

161 Just hs -> hs

170 Just hs -> hs

162 case lookupCtxtExact n (idris_datatypes ist) of

171 case lookupCtxtExact n (idris_datatypes ist) of

163− Just t -> tryCons d locs (hints ++

172+ Just t -> tryCons d locs tys

173+ (hints ++

164 con_names t ++

174 con_names t ++

165 autohints ++

175 autohints ++

166 getFn d fn)

176 getFn d fn)

@@ -169,28 +179,31 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

169

179

170 -- if there are local variables which have a function type, try

180 -- if there are local variables which have a function type, try

171 -- applying them too

181 -- applying them too

172− resolveByLocals d locs

182+ resolveByLocals d locs tys

173 = do env <- get_env

183 = do env <- get_env

174− tryLocals d locs env

184+ tryLocals d locs tys env

175

185

176− tryLocals d locs [] = fail "Locals failed"

186+ tryLocals d locs tys [] = fail "Locals failed"

177− tryLocals d locs ((x, t) : xs)

187+ tryLocals d locs tys ((x, t) : xs)

178− | x `elem` locs = tryLocals d locs xs

188+ | x `elem` locs = tryLocals d locs tys xs

179− | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True

189+ | otherwise = try' (tryLocal d (x : locs) tys x t)

190+ (tryLocals d locs tys xs) True

180

191

181− tryCons d locs [] = fail "Constructors failed"

192+ tryCons d locs tys [] = fail "Constructors failed"

193+ tryCons d locs tys (c : cs)

182− tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True

194+ = try' (tryCon d locs tys c) (tryCons d locs tys cs) True

183

195

184− tryLocal d locs n t

196+ tryLocal d locs tys n t

185 = do let a = getPArity (delab ist (binderTy t))

197 = do let a = getPArity (delab ist (binderTy t))

186− tryLocalArg d locs n a

198+ tryLocalArg d locs tys n a

187

199

188− tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)

200+ tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)

201+ tryLocalArg d locs tys n i

189− tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))

202+ = simple_app False (tryLocalArg d locs tys n (i - 1))

190− (psRec True d locs) "proof search local apply"

203+ (psRec True d locs tys) "proof search local apply"

191

204

192 -- Like type class resolution, but searching with constructors

205 -- Like type class resolution, but searching with constructors

193− tryCon d locs n =

206+ tryCon d locs tys n =

194 do ty <- goal

207 do ty <- goal

195 let imps = case lookupCtxtExact n (idris_implicits ist) of

208 let imps = case lookupCtxtExact n (idris_implicits ist) of

196 Nothing -> []

209 Nothing -> []

@@ -204,7 +217,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

204 when (length ps < length ps') $ fail "Can't apply constructor"

217 when (length ps < length ps') $ fail "Can't apply constructor"

205 mapM_ (\ (_, h) -> do focus h

218 mapM_ (\ (_, h) -> do focus h

206 aty <- goal

219 aty <- goal

207− psRec True d locs)

220+ psRec True d locs tys)

208 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

221 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

209 solve

222 solve

210

223

src/Idris/REPL.hs+9−11

@@ -582,8 +582,8 @@ idemodeProcess fn (HNF t) = process fn (HNF t)

582--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!

583idemodeProcess fn (TestInline t) = process fn (TestInline t)

584

585−idemodeProcess fn Execute = do process fn Execute

585+idemodeProcess fn (Execute t) = do process fn (Execute t)

586− iPrintResult ""

586+ iPrintResult ""

587idemodeProcess fn (Compile codegen f) = do process fn (Compile codegen f)

588 iPrintResult ""

589idemodeProcess fn (LogLvl i) = do process fn (LogLvl i)

@@ -1115,13 +1115,10 @@ process fn (TestInline t)

1115 let tm' = inlineTerm ist tm

1116 c <- colourise

1117 iPrintResult (showTm ist (delab ist tm'))

1118−process fn Execute

1118+process fn (Execute tm)

1119 = idrisCatch

1120 (do ist <- getIState

1121− (m, _) <- elabVal recinfo ERHS

1121+ (m, _) <- elabVal recinfo ERHS (elabExec fc tm)

1122− (PApp fc

1123− (PRef fc (sUN "run__IO"))

1124− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1125 (tmpn, tmph) <- runIO tempfile

1122 (tmpn, tmph) <- runIO tempfile

1126 runIO $ hClose tmph

1123 runIO $ hClose tmph

1127 t <- codegen

1124 t <- codegen

@@ -1232,10 +1229,11 @@ process fn (Apropos pkgs a) =

1232 delabTy ist n,

1229 delabTy ist n,

1233 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1230 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1234 | n <- sort names, isUN n ]

1231 | n <- sort names, isUN n ]

1232+ if (not (null mods)) || (not (null aproposInfo))

1235− iRenderResult $ vsep (map (\(m, d) -> text "Module" <+> text m <$>

1233+ then iRenderResult $ vsep (map (\(m, d) -> text "Module" <+> text m <$>

1236− ppD ist d <> line) mods) <$>

1234+ ppD ist d <> line) mods) <$>

1237− vsep (map (prettyDocumentedIst ist) aproposInfo)

1235+ vsep (map (prettyDocumentedIst ist) aproposInfo)

1238− putIState orig

1236+ else iRenderError $ text "No results found"

1239 where isUN (UN _) = True

1237 where isUN (UN _) = True

1240 isUN (NS n _) = isUN n

1238 isUN (NS n _) = isUN n

1241 isUN _ = False

1239 isUN _ = False

src/Idris/REPLParser.hs+9−1

@@ -71,7 +71,7 @@ parserCommandsForHelp =

71 , noArgCmd ["proofs"] Proofs "Show available proofs"

72 , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter"

73 , (["c", "compile"], FileArg, "Compile to an executable [codegen] <filename>", cmd_compile)

74− , noArgCmd ["exec", "execute"] Execute "Compile to an executable and run"

74+ , (["exec", "execute"], OptionalArg ExprArg, "Compile to an executable and run", cmd_execute)

75 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

76 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

77 , noArgCmd ["?", "h", "help"] Help "Display this help text"

@@ -276,6 +276,14 @@ cmd_consolewidth name = do

276 <|> do discard (P.symbol "infinite"); return InfinitelyWide

277 <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

278

279+cmd_execute :: String -> P.IdrisParser (Either String Command)

280+cmd_execute name = do

281+ tm <- option maintm (P.fullExpr defaultSyntax)

282+ return (Right (Execute tm))

283+ where

284+ maintm = PRef (fileFC "(repl)") (sNS (sUN "main") ["Main"])

285+

286+

279cmd_dynamic :: String -> P.IdrisParser (Either String Command)

287cmd_dynamic :: String -> P.IdrisParser (Either String Command)

280cmd_dynamic name = do

288cmd_dynamic name = do

281 let emptyArgs = noArgs ListDynamic name

289 let emptyArgs = noArgs ListDynamic name

src/Idris/TypeSearch.hs+7−5

@@ -30,7 +30,7 @@ import Idris.Core.Unify (match_unify)

30import Idris.Delaborate (delabTy)

31import Idris.Docstrings (noDocs, overview)

32import Idris.Elab.Type (elabType)

33−import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderResult, prettyDocumentedIst)

33+import Idris.Output (iputStrLn, iRenderOutput, iPrintResult, iRenderError, iRenderResult, prettyDocumentedIst)

34import Idris.IBC

35

36import Prelude hiding (pred)

@@ -54,10 +54,12 @@ searchByType pkgs pterm = do

54 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

55 displayScore theScore <> char ' ' <> prettyDocumentedIst i docInfo

56 | (n, theScore) <- names']

57+ if (not (null docs))

57− case idris_outputmode i of

58+ then case idris_outputmode i of

58− RawOutput _ -> do mapM_ iRenderOutput docs

59+ RawOutput _ -> do mapM_ iRenderOutput docs

59− iPrintResult ""

60+ iPrintResult ""

60− IdeMode _ _ -> iRenderResult (vsep docs)

61+ IdeMode _ _ -> iRenderResult (vsep docs)

62+ else iRenderError $ text "No results found"

61 putIState i -- don't actually make any changes

63 putIState i -- don't actually make any changes

62 where

64 where

63 numLimit = 50

65 numLimit = 50

src/Util/System.hs+30−2

@@ -1,5 +1,6 @@

1+{-# LANGUAGE CPP #-}

1module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,

2module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows,

2− readSource, writeSource) where

3+ writeSource, readSource, setupBundledCC) where

3

4

4-- System helper functions.

5-- System helper functions.

5import Control.Monad (when)

6import Control.Monad (when)

@@ -7,13 +8,19 @@ import System.Directory (getTemporaryDirectory

7 , removeFile

8 , removeFile

8 , removeDirectoryRecursive

9 , removeDirectoryRecursive

9 , createDirectoryIfMissing

10 , createDirectoryIfMissing

11+ , doesDirectoryExist

10 )

12 )

11−import System.FilePath ((</>), normalise)

13+import System.FilePath ((</>), normalise, isAbsolute, dropFileName)

12import System.IO

14import System.IO

13import System.Info

15import System.Info

14import System.IO.Error

16import System.IO.Error

15import Control.Exception as CE

17import Control.Exception as CE

16

18

19+#ifdef FREESTANDING

20+import Tools_idris

21+import System.Environment (getEnv, setEnv, getExecutablePath)

22+#endif

23+

17catchIO :: IO a -> (IOError -> IO a) -> IO a

24catchIO :: IO a -> (IOError -> IO a) -> IO a

18catchIO = CE.catch

25catchIO = CE.catch

19

26

@@ -54,3 +61,24 @@ rmFile f = do putStrLn $ "Removing " ++ f

54 catchIO (removeFile f)

61 catchIO (removeFile f)

55 (\ioerr -> putStrLn $ "WARNING: Cannot remove file "

62 (\ioerr -> putStrLn $ "WARNING: Cannot remove file "

56 ++ f ++ ", Error msg:" ++ show ioerr)

63 ++ f ++ ", Error msg:" ++ show ioerr)

64+

65+setupBundledCC :: IO()

66+#ifdef FREESTANDING

67+setupBundledCC = when hasBundledToolchain

68+ $ do

69+ exePath <- getExecutablePath

70+ path <- getEnv "PATH"

71+ tcDir <- return getToolchainDir

72+ absolute <- return $ isAbsolute tcDir

73+ target <- return $

74+ if absolute

75+ then tcDir

76+ else dropFileName exePath ++ tcDir

77+ let pathSep = if isWindows then ";" else ":"

78+ present <- doesDirectoryExist target

79+ when present

80+ $ do newPath <- return $ target ++ pathSep ++ path

81+ setEnv "PATH" newPath

82+#else

83+setupBundledCC = return ()

84+#endif

test/Makefile+1−1

@@ -8,7 +8,7 @@ test: $(TESTS)

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

9

10test_js:

11− @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 ffi006 --codegen node

11+ @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 effects004 buffer001 basic007 basic011 primitives004 ffi006 --codegen node

12

13update:

14 /usr/bin/env perl ./runtest.pl all -u

test/basic010/Main.idr+1−1

@@ -38,6 +38,6 @@ fmt (axiom n) = "axiom " ++ show n

38

39main : IO ()

40main = do

41− n <- map (const 10000) (putStrLn "*oink*")

41+ n <- map (const (the Nat 10000)) (putStrLn "*oink*")

42 putStrLn . show $ getWitness (f 4 n)

43 putStrLn . fmt $ getProof (g 4 n)

test/basic010/run+31−25

@@ -1,28 +1,5 @@

1#!/usr/bin/env bash

2

3−# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4−# Here copied from reg039.

5−#

6−# Executes command with a timeout

7−# Params:

8−# $1 timeout in seconds

9−# $2 command

10−# Returns 1 if timed out 0 otherwise

11−timeout() {

12−

13− time=$1

14−

15− # start the command in a subshell to avoid problem with pipes

16− # (spawn accepts one command)

17− command="/bin/sh -c \"$2\""

18−

19− expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

20−

21− if [ $? = 1 ] ; then

22− echo "Timeout after ${time} seconds"

23− fi

24−

25−}

26

3

27declare -a extraargs

4declare -a extraargs

28for arg in "$@"

5for arg in "$@"

@@ -30,6 +7,35 @@ do

30 extraargs=("${extraargs[@]}" "'$arg'")

7 extraargs=("${extraargs[@]}" "'$arg'")

31done

8done

32

9

10+if (which timeout&>/dev/null); then

11+ timeout 10 idris $@ Main.idr --nocolour --check --warnreach -o basic010

12+ timeout 5 ./basic010

13+else

14+ # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

15+ # Here copied from reg039.

16+ #

17+ # Executes command with a timeout

18+ # Params:

19+ # $1 timeout in seconds

20+ # $2 command

21+ # Returns 1 if timed out 0 otherwise

22+ timeout() {

23+

24+ time=$1

25+

26+ # start the command in a subshell to avoid problem with pipes

27+ # (spawn accepts one command)

28+ command="/bin/sh -c \"$2\""

29+

30+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

31+

32+ if [ $? = 1 ] ; then

33+ echo "Timeout after ${time} seconds"

34+ fi

35+

36+ }

37+

33−timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"

38+ timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"

34−timeout 5 "./basic010"

39+ timeout 5 "./basic010"

40+fi

35rm -f *.ibc basic010

41rm -f *.ibc basic010

test/effects001/test021.idr+1−2

@@ -9,8 +9,7 @@ import Control.IOExcept

9data Count : Type where

10

11FileIO : Type -> Type -> Type

12−FileIO st t

13− = { [FILE_IO st, STDIO, Count ::: STATE Int] } Eff t

12+FileIO st t = Eff t [FILE_IO st, STDIO, Count ::: STATE Int]

14

13

15readFile : FileIO (OpenFile Read) (List String)

14readFile : FileIO (OpenFile Read) (List String)

16readFile = readAcc [] where

15readFile = readAcc [] where

test/effects001/test021a.idr+1−1

@@ -18,7 +18,7 @@ Env = List (String, Integer)

18-- Evaluator t

19-- = Eff m [EXCEPTION String, RND, STATE Env] t

20

21−eval : Expr -> { [EXCEPTION String, STDIO, RND, STATE Env] } Eff Integer

21+eval : Expr -> Eff Integer [EXCEPTION String, STDIO, RND, STATE Env]

22eval (Var x) = do vs <- get

23 case lookup x vs of

24 Nothing => raise ("No such variable " ++ x)

test/effects002/test025.idr+2−2

@@ -6,8 +6,8 @@ import Control.IOExcept

6import Data.Vect

7

8MemoryIO : Type -> Type -> Type -> Type

9−MemoryIO td ts r = { [ Dst ::: RAW_MEMORY td

9+MemoryIO td ts r = Eff r [Dst ::: RAW_MEMORY td,

10− , Src ::: RAW_MEMORY ts ] } Eff r

10+ Src ::: RAW_MEMORY ts]

11

12inpVect : Vect 5 Bits8

13inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

test/effects003/hangman.idr+28−26

@@ -74,55 +74,59 @@ data HangmanRules : Effect where

74-- the number of missing letters, if not, reduce the number of guesses left

75

76 Guess : (x : Char) ->

77+ sig HangmanRules Bool

77− { Hangman (Running (S g) (S w)) ==>

78+ (Hangman (Running (S g) (S w)))

79+ (\inword =>

78− {inword} (case inword of

80+ case inword of

79 True => Hangman (Running (S g) w)

81 True => Hangman (Running (S g) w)

80− False => Hangman (Running g (S w))) }

82+ False => Hangman (Running g (S w)))

81− HangmanRules Bool

82

83

83-- The 'Won' operation requires that there are no missing letters

84-- The 'Won' operation requires that there are no missing letters

84

85

86+ Won : sig HangmanRules ()

87+ (Hangman (Running g 0))

85− Won : { Hangman (Running g 0) ==> Hangman NotRunning } HangmanRules ()

88+ (Hangman NotRunning)

86

89

87-- The 'Lost' operation requires that there are no guesses left

90-- The 'Lost' operation requires that there are no guesses left

88

91

92+ Lost : sig HangmanRules ()

93+ (Hangman (Running 0 g))

89− Lost : { Hangman (Running 0 g) ==> Hangman NotRunning } HangmanRules ()

94+ (Hangman NotRunning)

90

95

91-- Set up a new game, initialised with 6 guesses and the missing letters in

96-- Set up a new game, initialised with 6 guesses and the missing letters in

92-- the given word. Note that if there are no letters in the word, we won't

97-- the given word. Note that if there are no letters in the word, we won't

93-- be able to run 'Guess'!

98-- be able to run 'Guess'!

94

99

95 NewWord : (w : String) ->

100 NewWord : (w : String) ->

96− { h ==> Hangman (Running 6 (length (letters w))) } HangmanRules ()

101+ sig HangmanRules () h (Hangman (Running 6 (length (letters w))))

97

102

98-- Finally, allow us to get the current game state

103-- Finally, allow us to get the current game state

99

104

100− Get : { h } HangmanRules h

105+ Get : sig HangmanRules h h

101

106

102HANGMAN : HState -> EFFECT

107HANGMAN : HState -> EFFECT

103HANGMAN h = MkEff (Hangman h) HangmanRules

108HANGMAN h = MkEff (Hangman h) HangmanRules

104

109

105-- Promote explicit effecst to Eff programs

110-- Promote explicit effecst to Eff programs

106

111

107−guess : Char ->

112+guess : Char -> Eff Bool

108− { [HANGMAN (Running (S g) (S w))] ==>

113+ [HANGMAN (Running (S g) (S w))]

109− {inword} [HANGMAN (case inword of

114+ (\inword => [HANGMAN (case inword of

110− True => Running (S g) w

115+ True => Running (S g) w

111− False => Running g (S w))] } Eff Bool

116+ False => Running g (S w))])

112guess c = call (Main.Guess c)

117guess c = call (Main.Guess c)

113

118

114−won : { [HANGMAN (Running g 0)] ==> [HANGMAN NotRunning]} Eff ()

119+won : Eff () [HANGMAN (Running g 0)] [HANGMAN NotRunning]

115won = call Won

120won = call Won

116

121

117−lost : { [HANGMAN (Running 0 g)] ==> [HANGMAN NotRunning]} Eff ()

122+lost : Eff () [HANGMAN (Running 0 g)] [HANGMAN NotRunning]

118lost = call Lost

123lost = call Lost

119

124

120−new_word : (w : String) ->

125+new_word : (w : String) -> Eff () [HANGMAN h]

121− { [HANGMAN h] ==>

122− [HANGMAN (Running 6 (length (letters w)))]} Eff ()

126+ [HANGMAN (Running 6 (length (letters w)))]

123new_word w = call (NewWord w)

127new_word w = call (NewWord w)

124

128

125−get : { [HANGMAN h] } Eff (Hangman h)

129+get : Eff (Hangman h) [HANGMAN h]

126get = call Get

130get = call Get

127

131

128-----------------------------------------------------------------------

132-----------------------------------------------------------------------

@@ -163,8 +167,8 @@ were valid letters in it!

163soRefl : So x -> (x = True)

167soRefl : So x -> (x = True)

164soRefl Oh = Refl

168soRefl Oh = Refl

165

169

166−game : { [HANGMAN (Running (S g) w), STDIO] ==>

170+game : Eff () [HANGMAN (Running (S g) w), STDIO]

167− [HANGMAN NotRunning, STDIO] } Eff ()

171+ [HANGMAN NotRunning, STDIO]

168game {w=Z} = won

172game {w=Z} = won

169game {w=S _}

173game {w=S _}

170 = do putStrLn (show !get)

174 = do putStrLn (show !get)

@@ -175,10 +179,8 @@ game {w=S _}

175 (Right p) => do putStrLn "Invalid input!"

179 (Right p) => do putStrLn "Invalid input!"

176 game

180 game

177 where

181 where

178− processGuess : -- {g,w:_} ->

179− Char -> { [HANGMAN (Running (S g) (S w)), STDIO] ==>

182+ processGuess : Char -> Eff () [HANGMAN (Running (S g) (S w)), STDIO]

180− [HANGMAN NotRunning, STDIO] }

183+ [HANGMAN NotRunning, STDIO]

181− Eff ()

182 processGuess {g} c {w}

184 processGuess {g} c {w}

183 = case !(guess c) of

185 = case !(guess c) of

184 True => do putStrLn "Good guess!"

186 True => do putStrLn "Good guess!"

@@ -203,7 +205,7 @@ wlen = proof search

203

205

204{- It typechecks! Ship it! -}

206{- It typechecks! Ship it! -}

205

207

206−runGame : { [HANGMAN NotRunning, RND, STDIO] } Eff ()

208+runGame : Eff () [HANGMAN NotRunning, RND, STDIO]

207runGame = do srand 1234567890

209runGame = do srand 1234567890

208 let w = index !(rndFin _) words

210 let w = index !(rndFin _) words

209 new_word w

211 new_word w

test/effects004/effects004.idrnew file+19

@@ -0,0 +1,19 @@

1+import Effects

2+import Effect.StdIO

3+import Effect.State

4+

5+counter : Eff () [STATE Int, STDIO]

6+counter = do putStrLn $ "Counter at " ++ show !get

7+ x <- getStr

8+ if trim x /= "" then pure ()

9+ else do put (!get + 1)

10+ counter

11+

12+startCounter : Eff () [STDIO]

13+startCounter = do putStrLn "Off we go!"

14+ new (STATE Int) 0 counter

15+ putStrLn "Finished!"

16+

17+main : IO ()

18+main = run startCounter

19+

test/effects004/expectednew file+11

@@ -0,0 +1,11 @@

1+Off we go!

2+Counter at 0

3+Counter at 1

4+Counter at 2

5+Counter at 3

6+Counter at 4

7+Counter at 5

8+Counter at 6

9+Counter at 7

10+Counter at 8

11+Finished!

test/effects004/inputnew file+10

@@ -0,0 +1,10 @@

1+

2+

3+

4+

5+

6+

7+

8+

9+done

10+

test/effects004/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ effects004.idr -o effects004 -p effects

3+./effects004 < input

4+rm -f effects004 *.ibc

test/ffi006/run+1−1

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

2idris $@ ffi006.idr --interface -o ffi006.o

3−cc ffi006.c ffi006.o `idris --include` `idris --link` -o ffi006

3+${CC:=cc} ffi006.c ffi006.o `idris --include` `idris --link` -o ffi006

4./ffi006

5rm -f ffi006 *.ibc *.o *.h

test/interactive007/expected.msysnew file+1

@@ -0,0 +1 @@

1+Idris> *Data\ZZ> *Data\ZZ> *Data\ZZ> *Data\ZZ> Bye bye

test/reg039/run+27−24

@@ -1,32 +1,35 @@

1#!/usr/bin/env bash

2

3−# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4−# Executes command with a timeout

5−# Params:

6−# $1 timeout in seconds

7−# $2 command

8−# Returns 1 if timed out 0 otherwise

9−timeout() {

10−

11− time=$1

12−

13− # start the command in a subshell to avoid problem with pipes

14− # (spawn accepts one command)

15− command="/bin/sh -c \"$2\""

16−

17− expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

18−

19− if [ $? = 1 ] ; then

20− echo "Timeout after ${time} seconds"

21− fi

22−

23−}

24

3

25declare -a extraargs

4declare -a extraargs

26for arg in "$@"

5for arg in "$@"

27do

6do

28 extraargs=("${extraargs[@]}" "'$arg'")

7 extraargs=("${extraargs[@]}" "'$arg'")

29done

8done

30−

9+if (which timeout&>/dev/null); then

10+ timeout 60 idris $@ --nocolour reg039.idr --exec go

11+else

12+ # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

13+ # Executes command with a timeout

14+ # Params:

15+ # $1 timeout in seconds

16+ # $2 command

17+ # Returns 1 if timed out 0 otherwise

18+ timeout() {

19+

20+ time=$1

21+

22+ # start the command in a subshell to avoid problem with pipes

23+ # (spawn accepts one command)

24+ command="/bin/sh -c \"$2\""

25+

26+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

27+

28+ if [ $? = 1 ] ; then

29+ echo "Timeout after ${time} seconds"

30+ fi

31+

32+ }

31−timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"

33+ timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"

34+ fi

32−rm -f reg039 *.ibc

35+ rm -f reg039 *.ibc

test/runtest.pl+8

@@ -30,6 +30,14 @@ sub runtest {

30 my $got = `$sandbox ./run @idrOpts`;

31 my $exp = `cat expected`;

32

33+ # Allow for variant expected output for tests by overriding expected

34+ # when there is an expected.<os> file in the test.

35+ # This should be the exception but there are sometimes valid reasons

36+ # for os-dependent output.

37+ # The endings are msys for windows, darwin for osx and linux for linux

38+ if ( -e "expected.$^O") {

39+ $exp = `cat expected.$^O`;

40+ }

33 open my $out, '>', 'output';

41 open my $out, '>', 'output';

34 print $out $got;

42 print $out $got;

35 close $out;

43 close $out;

win-release.shnew file+2

@@ -0,0 +1,2 @@

1+

2+IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make