0ca1715 · 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/Language/Reflection/Elab.idrnew file+149

@@ -0,0 +1,149 @@

1+module Language.Reflection.Elab

2+

3+import Builtins

4+import Prelude.Applicative

5+import Prelude.Functor

6+import Prelude.List

7+import Prelude.Maybe

8+import Prelude.Monad

9+import Language.Reflection

10+

11+data Arg : Type where

12+ Explicit : TTName -> Raw -> Arg

13+ Implicit : TTName -> Raw -> Arg

14+ Constraint : TTName -> Raw -> Arg

15+

16+data TyDecl : Type where

17+ Declare : TTName -> List Arg -> Raw -> TyDecl

18+

19+data FunClause : Type where

20+ MkFunClause : (lhs, rhs : Raw) -> FunClause

21+ MkImpossibleClause : (lhs : Raw) -> FunClause

22+

23+data FunDefn : Type where

24+ DefineFun : TTName -> List FunClause -> FunDefn

25+

26+abstract

27+data Elab : Type -> Type where

28+ -- obligatory control stuff

29+ prim__PureElab : a -> Elab a

30+ prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b

31+

32+ prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a

33+ prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a

34+

35+ prim__Env : Elab (List (TTName, Binder TT))

36+ prim__Goal : Elab (TTName, TT)

37+ prim__Holes : Elab (List TTName)

38+ prim__Guess : Elab (Maybe TT)

39+

40+ prim__SourceLocation : Elab SourceLocation

41+

42+ prim__Forget : TT -> Elab Raw

43+

44+ prim__Gensym : String -> Elab TTName

45+

46+ prim__Solve : Elab ()

47+ prim__Fill : Raw -> Elab ()

48+ prim__Focus : TTName -> Elab ()

49+ prim__Unfocus : TTName -> Elab ()

50+ prim__Attack : Elab ()

51+

52+ prim__Rewrite : Raw -> Elab ()

53+

54+ prim__Claim : TTName -> Raw -> Elab ()

55+ prim__Intro : Maybe TTName -> Elab ()

56+

57+ prim__DeclareType : TyDecl -> Elab ()

58+ prim__DefineFunction : FunDefn -> Elab ()

59+

60+ prim__Debug : {a : Type} -> Maybe String -> Elab a

61+

62+

63+-------------

64+-- Public API

65+-------------

66+%access public

67+

68+instance Functor Elab where

69+ map f t = prim__BindElab t (\x => prim__PureElab (f x))

70+

71+instance Applicative Elab where

72+ pure x = prim__PureElab x

73+ f <*> x = prim__BindElab f $ \g =>

74+ prim__BindElab x $ \y =>

75+ prim__PureElab $ g y

76+

77+instance Alternative Elab where

78+ empty = prim__Fail [TextPart "empty"]

79+ x <|> y = prim__Try x y

80+

81+instance Monad Elab where

82+ x >>= f = prim__BindElab x f

83+

84+fail : List ErrorReportPart -> Elab a

85+fail err = prim__Fail err

86+

87+getEnv : Elab (List (TTName, Binder TT))

88+getEnv = prim__Env

89+

90+getGoal : Elab (TTName, TT)

91+getGoal = prim__Goal

92+

93+getHoles : Elab (List TTName)

94+getHoles = prim__Holes

95+

96+getGuess : Elab (Maybe TT)

97+getGuess = prim__Guess

98+

99+forgetTypes : TT -> Elab Raw

100+forgetTypes tt = prim__Forget tt

101+

102+gensym : (hint : String) -> Elab TTName

103+gensym hint = prim__Gensym hint

104+

105+solve : Elab ()

106+solve = prim__Solve

107+

108+fill : Raw -> Elab ()

109+fill tm = prim__Fill tm

110+

111+focus : (hole : TTName) -> Elab ()

112+focus hole = prim__Focus hole

113+

114+unfocus : TTName -> Elab ()

115+unfocus hole = prim__Unfocus hole

116+

117+attack : Elab ()

118+attack = prim__Attack

119+

120+claim : TTName -> Raw -> Elab ()

121+claim n ty = prim__Claim n ty

122+

123+intro : Maybe TTName -> Elab ()

124+intro n = prim__Intro n

125+

126+||| Find out the present source context for the tactic script

127+getSourceLocation : Elab SourceLocation

128+getSourceLocation = prim__SourceLocation

129+

130+||| Attempt to solve the current goal with the source code location

131+sourceLocation : Elab ()

132+sourceLocation = do loc <- getSourceLocation

133+ fill (quote loc)

134+ solve

135+

136+rewriteWith : Raw -> Elab ()

137+rewriteWith rule = prim__Rewrite rule

138+

139+declareType : TyDecl -> Elab ()

140+declareType decl = prim__DeclareType decl

141+

142+defineFunction : FunDefn -> Elab ()

143+defineFunction defun = prim__DefineFunction defun

144+

145+debug : Elab a

146+debug = prim__Debug Nothing

147+

148+debugMessage : String -> Elab a

149+debugMessage msg = prim__Debug (Just msg)

libs/prelude/Language/Reflection/Tactical.idrdeleted−148

@@ -1,148 +0,0 @@

1−module Language.Reflection.Tactical

2−

3−import Builtins

4−import Prelude.Applicative

5−import Prelude.Functor

6−import Prelude.List

7−import Prelude.Maybe

8−import Prelude.Monad

9−import Language.Reflection

10−

11−data Arg : Type where

12− Explicit : TTName -> Raw -> Arg

13− Implicit : TTName -> Raw -> Arg

14− Constraint : TTName -> Raw -> Arg

15−

16−data TyDecl : Type where

17− Declare : TTName -> List Arg -> Raw -> TyDecl

18−

19−data FunClause : Type where

20− MkFunClause : (lhs, rhs : Raw) -> FunClause

21−

22−data FunDefn : Type where

23− DefineFun : TTName -> List FunClause -> FunDefn

24−

25−abstract

26−data Tactical : Type -> Type where

27− -- obligatory control stuff

28− prim__PureTactical : a -> Tactical a

29− prim__BindTactical : {a, b : Type} -> Tactical a -> (a -> Tactical b) -> Tactical b

30−

31− prim__Try : {a : Type} -> Tactical a -> Tactical a -> Tactical a

32− prim__Fail : {a : Type} -> List ErrorReportPart -> Tactical a

33−

34− prim__Env : Tactical (List (TTName, Binder TT))

35− prim__Goal : Tactical (TTName, TT)

36− prim__Holes : Tactical (List TTName)

37− prim__Guess : Tactical (Maybe TT)

38−

39− prim__SourceLocation : Tactical SourceLocation

40−

41− prim__Forget : TT -> Tactical Raw

42−

43− prim__Gensym : String -> Tactical TTName

44−

45− prim__Solve : Tactical ()

46− prim__Fill : Raw -> Tactical ()

47− prim__Focus : TTName -> Tactical ()

48− prim__Unfocus : TTName -> Tactical ()

49− prim__Attack : Tactical ()

50−

51− prim__Rewrite : Raw -> Tactical ()

52−

53− prim__Claim : TTName -> Raw -> Tactical ()

54− prim__Intro : Maybe TTName -> Tactical ()

55−

56− prim__DeclareType : TyDecl -> Tactical ()

57− prim__DefineFunction : FunDefn -> Tactical ()

58−

59− prim__Debug : {a : Type} -> Maybe String -> Tactical a

60−

61−

62−-------------

63−-- Public API

64−-------------

65−%access public

66−

67−instance Functor Tactical where

68− map f t = prim__BindTactical t (\x => prim__PureTactical (f x))

69−

70−instance Applicative Tactical where

71− pure x = prim__PureTactical x

72− f <*> x = prim__BindTactical f $ \g =>

73− prim__BindTactical x $ \y =>

74− prim__PureTactical $ g y

75−

76−instance Alternative Tactical where

77− empty = prim__Fail [TextPart "empty"]

78− x <|> y = prim__Try x y

79−

80−instance Monad Tactical where

81− x >>= f = prim__BindTactical x f

82−

83−fail : List ErrorReportPart -> Tactical a

84−fail err = prim__Fail err

85−

86−getEnv : Tactical (List (TTName, Binder TT))

87−getEnv = prim__Env

88−

89−getGoal : Tactical (TTName, TT)

90−getGoal = prim__Goal

91−

92−getHoles : Tactical (List TTName)

93−getHoles = prim__Holes

94−

95−getGuess : Tactical (Maybe TT)

96−getGuess = prim__Guess

97−

98−forgetTypes : TT -> Tactical Raw

99−forgetTypes tt = prim__Forget tt

100−

101−gensym : (hint : String) -> Tactical TTName

102−gensym hint = prim__Gensym hint

103−

104−solve : Tactical ()

105−solve = prim__Solve

106−

107−fill : Raw -> Tactical ()

108−fill tm = prim__Fill tm

109−

110−focus : (hole : TTName) -> Tactical ()

111−focus hole = prim__Focus hole

112−

113−unfocus : TTName -> Tactical ()

114−unfocus hole = prim__Unfocus hole

115−

116−attack : Tactical ()

117−attack = prim__Attack

118−

119−claim : TTName -> Raw -> Tactical ()

120−claim n ty = prim__Claim n ty

121−

122−intro : Maybe TTName -> Tactical ()

123−intro n = prim__Intro n

124−

125−||| Find out the present source context for the tactic script

126−getSourceLocation : Tactical SourceLocation

127−getSourceLocation = prim__SourceLocation

128−

129−||| Attempt to solve the current goal with the source code location

130−sourceLocation : Tactical ()

131−sourceLocation = do loc <- getSourceLocation

132− fill (quote loc)

133− solve

134−

135−rewriteWith : Raw -> Tactical ()

136−rewriteWith rule = prim__Rewrite rule

137−

138−declareType : TyDecl -> Tactical ()

139−declareType decl = prim__DeclareType decl

140−

141−defineFunction : FunDefn -> Tactical ()

142−defineFunction defun = prim__DefineFunction defun

143−

144−debug : Tactical a

145−debug = prim__Debug Nothing

146−

147−debugMessage : String -> Tactical a

148−debugMessage msg = prim__Debug (Just msg)

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

libs/prelude/prelude.ipkg+1−1

@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

12

13− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,

13+ Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

14

15 Decidable.Equality

16

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/AbsSyntax.hs+4−4

@@ -1011,7 +1011,7 @@ expandParams dec ps ns infs tm = en tm

1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1014− en (PRunTactics fc tm) = PRunTactics fc (en tm)

1014+ en (PRunElab fc tm) = PRunElab fc (en tm)

1015 en t = t

1016

1017 nselem x [] = False

@@ -1485,7 +1485,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1485 imps top env (PHidden tm) = imps False env tm

1486 imps top env (PUnifyLog tm) = imps False env tm

1487 imps top env (PNoImplicits tm) = imps False env tm

1488− imps top env (PRunTactics fc tm) = imps False env tm

1488+ imps top env (PRunElab fc tm) = imps False env tm

1489 imps top env _ = return ()

1490

1491 pibind using [] sc = sc

@@ -1612,7 +1612,7 @@ addImpl' inpat env infns imp_meths ist ptm

1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1613 (fmap (ai True env ds) g)

1614 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1615− ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)

1615+ ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)

1616 ai qq env ds tm = tm

1617

1618 handleErr (Left err) = PElabError err

@@ -2149,5 +2149,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2149 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

2150 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2151 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2152− mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)

2152+ mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)

2153 mkUniq t = return t

src/Idris/AbsSyntaxTree.hs+43−28

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

@@ -648,6 +648,7 @@ deriving instance NFData PDecl'

648-- | A set of instructions for things that need to happen in IState

649-- after a term elaboration when there's been reflected elaboration.

650data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

651+ | RClausesInstrs Name [([Name], Term, Term)]

651

652

652-- | For elaborator state

653-- | For elaborator state

653data EState = EState {

654data EState = EState {

@@ -825,7 +826,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

825 | PNoImplicits PTerm -- ^ never run implicit converions on the term

826 | PNoImplicits PTerm -- ^ never run implicit converions on the term

826 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

827 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

827 | PUnquote PTerm -- ^ ~Term

828 | PUnquote PTerm -- ^ ~Term

828− | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script

829+ | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

829 deriving (Eq, Data, Typeable)

830 deriving (Eq, Data, Typeable)

830

831

832

@@ -1432,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1432 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1433 prettySe p bnd (PLam fc n ty sc) =

1434 prettySe p bnd (PLam fc n ty sc) =

1434 bracket p startPrec . group . align . hang 2 $

1435 bracket p startPrec . group . align . hang 2 $

1435− text "\\" <> bindingOf n False <+> text "=>" <$>

1436+ text "\\" <> prettyBindingOf n False <+> text "=>" <$>

1436 prettySe startPrec ((n, False):bnd) sc

1437 prettySe startPrec ((n, False):bnd) sc

1437 prettySe p bnd (PLet fc n ty v sc) =

1438 prettySe p bnd (PLet fc n ty v sc) =

1438 bracket p startPrec . group . align $

1439 bracket p startPrec . group . align $

1439− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

1440+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

1440 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

1441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

1441 prettySe p bnd (PPi (Exp l s _) n ty sc)

1442 prettySe p bnd (PPi (Exp l s _) n ty sc)

1442 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1443 bracket p startPrec . group $

1444 bracket p startPrec . group $

1444− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

1445+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

1445 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc

1446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc

1446 | otherwise =

1447 | otherwise =

1447 bracket p startPrec . group $

1448 bracket p startPrec . group $

@@ -1454,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1454 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

1455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

1455 | ppopt_impl ppo =

1456 | ppopt_impl ppo =

1456 bracket p startPrec $

1457 bracket p startPrec $

1457− lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1458+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1458 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc

1459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc

1459 | otherwise = prettySe startPrec ((n, True):bnd) sc

1460 | otherwise = prettySe startPrec ((n, True):bnd) sc

1460 where

1461 where

@@ -1611,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1611

1612

1612 prettySe p bnd _ = text "missing pretty-printer for term"

1613 prettySe p bnd _ = text "missing pretty-printer for term"

1613

1614

1615+ prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation

1616+ prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))

1617+ where display (UN n) = T.unpack n

1618+ display (MN _ n) = T.unpack n

1619+ -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings

1620+ display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n

1621+ display n = show n

1622+

1614 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1623 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1615 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm

1624 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm

1616 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1625 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

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

1632 basename (NS n _) = basename n

1641 basename (NS n _) = basename n

1633 basename n = n

1642 basename n = n

1634

1643

1644+ slist' _ _ e

1645+ | containsHole e = Nothing

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

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

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

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

1637 slist' p bnd (PRef _ nil)

1648 slist' p bnd (PRef _ nil)

@@ -1901,31 +1912,35 @@ allNamesIn tm = nub $ ni [] tm

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

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

1902 niTacImp _ _ = []

1913 niTacImp _ _ = []

1903

1914

1915+

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

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

1905boundNamesIn :: PTerm -> [Name]

1917boundNamesIn :: PTerm -> [Name]

1906−boundNamesIn tm = nub $ ni tm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1921− ni (PHidden tm) = ni tm

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

1922− ni (PUnifyLog tm) = ni tm

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

1923− ni (PDisamb _ tm) = ni tm

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

1924− ni (PNoImplicits tm) = ni tm

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

1925− ni _ = []

1937+ ni set _ = set

1926−

1938+

1939+ niTms set [] = set

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

1941+

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

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

1928− niTacImp _ = []

1943+ niTacImp set _ = set

1929

1944

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

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

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

1946implicitNamesIn :: [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/DSL.hs+2−2

@@ -108,7 +108,7 @@ expandDo dsl (PDoBlock ds)

108 block b _ = PElabError (Msg "Invalid statement in do block")

109

110expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

111−expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm

111+expandDo dsl (PRunElab fc tm) = PRunElab fc $ expandDo dsl tm

112expandDo dsl t = t

113

114-- | Replace DSL-bound variable in a term

@@ -195,7 +195,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

195 db' (PDPair fc p l t r) = do l' <- db' l

196 r' <- db' r

197 return (PDPair fc p l' t r')

198− db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)

198+ db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)

199 db' t = return t

200

201 dbArg a = do t' <- db' (getTm a)

src/Idris/DeepSeq.hs+1−1

@@ -243,7 +243,7 @@ instance NFData PTerm where

243 rnf (PNoImplicits x1) = rnf x1 `seq` ()

244 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

245 rnf (PUnquote x1) = rnf x1 `seq` ()

246− rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

246+ rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

247

248instance (NFData t) => NFData (PTactic' t) where

249 rnf (Intro x1) = rnf x1 `seq` ()

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/ElabQuasiquote.hs+2−2

@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)

170 return (PRef (fileFC "(unquote)") n, [(n, tm)])

171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

172 extractUnquotes (n-1) tm

173−extractUnquotes n (PRunTactics fc tm)

173+extractUnquotes n (PRunElab fc tm)

174− = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm

174+ = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm

175extractUnquotes n x = return (x, []) -- no subterms!

176

177

src/Idris/ElabTerm.hs+38−16

@@ -62,6 +62,11 @@ processTacticDecls info =

62 addIBC (IBCDef n)

63 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

64 addDeferred ds'

65+ RClausesInstrs n cs ->

66+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n

67+ solveDeferred n

68+ updateIState $ \i -> i { idris_patdefs = addDef n (cs, []) $ idris_patdefs i } -- TODO: missing clauses

69+ addIBC (IBCDef n)

65

70

66-- Using the elaborator, convert a term in raw syntax to a fully

71-- Using the elaborator, convert a term in raw syntax to a fully

67-- elaborated, typechecked term.

72-- elaborated, typechecked term.

@@ -215,7 +220,7 @@ goal_polymorphic =

215

220

216-- | Returns the set of declarations we need to add to complete the

221-- | Returns the set of declarations we need to add to complete the

217-- definition (most likely case blocks to elaborate) as well as

222-- definition (most likely case blocks to elaborate) as well as

218−-- declarations resulting from user tactic scripts (%runTactics)

223+-- declarations resulting from user tactic scripts (%runElab)

219elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

224elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

220 ElabD ()

225 ElabD ()

221elab ist info emode opts fn tm

226elab ist info emode opts fn tm

@@ -1102,11 +1107,11 @@ elab ist info emode opts fn tm

1102 delayElab $ do focus h

1107 delayElab $ do focus h

1103 dotterm

1108 dotterm

1104 elab' ina fc t

1109 elab' ina fc t

1105− elab' ina fc (PRunTactics fc' tm) =

1110+ elab' ina fc (PRunElab fc' tm) =

1106 do attack

1111 do attack

1107 n <- getNameFrom (sMN 0 "tacticScript")

1112 n <- getNameFrom (sMN 0 "tacticScript")

1108 n' <- getNameFrom (sMN 0 "tacticExpr")

1113 n' <- getNameFrom (sMN 0 "tacticExpr")

1109− let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)

1114+ let scriptTy = RApp (Var (sNS (sUN "Elab") ["Elab", "Reflection", "Language"])) (Var unitTy)

1110 claim n scriptTy

1115 claim n scriptTy

1111 movelast n

1116 movelast n

1112 letbind n' scriptTy (Var n)

1117 letbind n' scriptTy (Var n)

@@ -1585,7 +1590,7 @@ case_ ind autoSolve ist fn tm = do

1585 when autoSolve solveAll

1590 when autoSolve solveAll

1586

1591

1587tacN :: String -> Name

1592tacN :: String -> Name

1588−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1593+tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]

1589

1594

1590runTactical :: FC -> Env -> Term -> ElabD ()

1595runTactical :: FC -> Env -> Term -> ElabD ()

1591runTactical fc env tm = do tm' <- eval tm

1596runTactical fc env tm = do tm' <- eval tm

@@ -1597,28 +1602,43 @@ runTactical fc env tm = do tm' <- eval tm

1597

1602

1598 returnUnit = fmap fst $ get_type_val (Var unitCon)

1603 returnUnit = fmap fst $ get_type_val (Var unitCon)

1599

1604

1605+ patvars :: [Name] -> Term -> ([Name], Term)

1606+ patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)

1607+ patvars ns tm = (ns, tm)

1608+

1609+ pullVars :: (Term, Term) -> ([Name], Term, Term)

1610+ pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1611+

1600 defineFunction :: RFunDefn -> ElabD ()

1612 defineFunction :: RFunDefn -> ElabD ()

1601 defineFunction (RDefineFun n clauses) =

1613 defineFunction (RDefineFun n clauses) =

1602 do ctxt <- get_context

1614 do ctxt <- get_context

1603 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt

1615 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt

1604 let info = CaseInfo True True False -- TODO document and figure out

1616 let info = CaseInfo True True False -- TODO document and figure out

1617+ clauses' <- forM clauses (\case

1605− clauses' <- forM clauses (\(RMkFunClause lhs rhs) ->

1618+ RMkFunClause lhs rhs ->

1606− do lhs' <- lift $ check ctxt [] lhs

1619+ do lhs' <- fmap fst . lift $ check ctxt [] lhs

1607− rhs' <- lift $ check ctxt [] rhs

1620+ rhs' <- fmap fst . lift $ check ctxt [] rhs

1608− return (fst lhs', fst rhs'))

1621+ return $ Right (lhs', rhs')

1622+ RMkImpossibleClause lhs ->

1623+ do lhs' <- fmap fst . lift $ check ctxt [] lhs

1624+ return $ Left lhs')

1625+ let clauses'' = map (\case Right c -> pullVars c

1626+ Left lhs -> let (ns, lhs') = patvars [] lhs'

1627+ in (ns, lhs', Impossible))

1609− trace (show clauses') $ return ()

1628+ clauses'

1610 set_context $

1629 set_context $

1611 addCasedef n (const [])

1630 addCasedef n (const [])

1612 info False (STerm Erased)

1631 info False (STerm Erased)

1613 True False -- TODO what are these?

1632 True False -- TODO what are these?

1614 [] [] -- TODO argument types, inaccessible types

1633 [] [] -- TODO argument types, inaccessible types

1615− (map Right clauses')

1634+ clauses'

1616− (map (\(l,r) -> ([], l, r)) clauses')

1635+ clauses''

1617− (map (\(l,r) -> ([], l, r)) clauses')

1636+ clauses''

1618− (map (\(l,r) -> ([], l, r)) clauses')

1637+ clauses''

1619− (map (\(l,r) -> ([], l, r)) clauses')

1638+ clauses''

1620 ty

1639 ty

1621 ctxt

1640 ctxt

1641+ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1622 return ()

1642 return ()

1623

1643

1624 -- | Do a step in the reflected elaborator monad. The input is the

1644 -- | Do a step in the reflected elaborator monad. The input is the

@@ -1659,9 +1679,9 @@ runTactical fc env tm = do tm' <- eval tm

1659 = do errs' <- eval errs

1679 = do errs' <- eval errs

1660 parts <- reifyReportParts errs'

1680 parts <- reifyReportParts errs'

1661 lift . tfail $ ReflectionError [parts] (Msg "")

1681 lift . tfail $ ReflectionError [parts] (Msg "")

1662− | n == tacN "prim__PureTactical", [_a, tm] <- args

1682+ | n == tacN "prim__PureElab", [_a, tm] <- args

1663 = return tm

1683 = return tm

1664− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1684+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args

1665 = do first' <- eval first

1685 = do first' <- eval first

1666 res <- runTacTm first'

1686 res <- runTacTm first'

1667 next <- eval (App andThen res)

1687 next <- eval (App andThen res)

@@ -2916,6 +2936,8 @@ reifyFunDefn (App (App (P _ n _) fnN) clauses)

2916 | n == tacN "MkFunClause" = liftM2 RMkFunClause

2936 | n == tacN "MkFunClause" = liftM2 RMkFunClause

2917 (reifyRaw lhs)

2937 (reifyRaw lhs)

2918 (reifyRaw rhs)

2938 (reifyRaw rhs)

2939+ reifyC (App (P (DCon _ _ _) n _) lhs)

2940+ | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs

2919 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

2941 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

2920reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

2942reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

2921

2943

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/Error.hs+1−1

@@ -148,4 +148,4 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>

148warnDisamb ist (PUnquote tm) = warnDisamb ist tm

149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

151−warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm

151+warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm

src/Idris/IBC.hs+4−4

@@ -1674,9 +1674,9 @@ instance Binary PTerm where

1674 put x2

1675 PUniverse x1 -> do putWord8 38

1676 put x1

1677− PRunTactics x1 x2 -> do putWord8 39

1677+ PRunElab x1 x2 -> do putWord8 39

1678− put x1

1678+ put x1

1679− put x2

1679+ put x2

1680 PAs x1 x2 x3 -> do putWord8 40

1681 put x1

1682 put x2

@@ -1809,7 +1809,7 @@ instance Binary PTerm where

1809 return (PUniverse x1)

1810 39 -> do x1 <- get

1811 x2 <- get

1812− return (PRunTactics x1 x2)

1812+ return (PRunElab x1 x2)

1813 40 -> do x1 <- get

1814 x2 <- get

1815 x3 <- get

src/Idris/IdrisDoc.hs+3−3

@@ -321,7 +321,7 @@ extractPTermNames (PCoerced p) = extract p

321extractPTermNames (PDisamb _ p) = extract p

322extractPTermNames (PUnifyLog p) = extract p

323extractPTermNames (PNoImplicits p) = extract p

324−extractPTermNames (PRunTactics _ p) = extract p

324+extractPTermNames (PRunElab _ p) = extract p

325extractPTermNames _ = []

326

327-- | Shorter name for extractPTermNames

@@ -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+67−50

@@ -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)

@@ -221,7 +220,7 @@ InternalExpr ::=

221internalExpr :: SyntaxInfo -> IdrisParser PTerm

220internalExpr :: SyntaxInfo -> IdrisParser PTerm

222internalExpr syn =

221internalExpr syn =

223 unifyLog syn

222 unifyLog syn

224− <|> runTactics syn

223+ <|> runElab syn

225 <|> disamb syn

224 <|> disamb syn

226 <|> noImplicits syn

225 <|> noImplicits syn

227 <|> recordType syn

226 <|> recordType syn

@@ -498,16 +497,16 @@ unifyLog syn = do try (lchar '%' *> reserved "unifyLog")

498

497

499{- | Parses a new-style tactics expression

498{- | Parses a new-style tactics expression

500RunTactics ::=

499RunTactics ::=

501− '%' 'runTactics' SimpleExpr

500+ '%' 'runElab' SimpleExpr

502 ;

501 ;

503-}

502-}

504−runTactics :: SyntaxInfo -> IdrisParser PTerm

503+runElab :: SyntaxInfo -> IdrisParser PTerm

505−runTactics syn = do try (lchar '%' *> reserved "runTactics")

504+runElab syn = do try (lchar '%' *> reserved "runElab")

506− fc <- getFC

505+ fc <- getFC

507− tm <- simpleExpr syn

506+ tm <- simpleExpr syn

508− i <- get

507+ i <- get

509− return $ PRunTactics fc tm

508+ return $ PRunElab fc tm

510− <?> "new-style tactics expression"

509+ <?> "new-style tactics expression"

511

510

512{- | Parses a disambiguation expression

511{- | Parses a disambiguation expression

513Disamb ::=

512Disamb ::=

@@ -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/Reflection.hs+3−1

@@ -17,6 +17,8 @@ rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

19

20−data RFunClause = RMkFunClause Raw Raw deriving Show

20+data RFunClause = RMkFunClause Raw Raw

21+ | RMkImpossibleClause Raw

22+ deriving Show

21

23

22data RFunDefn = RDefineFun Name [RFunClause] deriving Show

24data RFunDefn = RDefineFun Name [RFunClause] deriving Show

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;

test/tactics001/Tactics.idr+4−4

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

1module Tactics

2

3−import Language.Reflection.Tactical

3+import Language.Reflection.Elab

4

5import Data.Vect

6

@@ -18,21 +18,21 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x

18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n

19plusZeroRightNeutralNew Z = Refl

20plusZeroRightNeutralNew (S k) =

21− %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))

21+ %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))

22 fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))

23 solve)

24

25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)

26plusSuccRightSuccNew Z k = Refl

27plusSuccRightSuccNew (S j) k =

28− %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

28+ %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

29 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

30 solve)

31

32-- Test that side effects in new tactics work

33

34mkDecl : ()

35−mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

35+mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

36 [Implicit (UN "z") `(Nat)]

37 `(Vect ~(Var (UN "z")) ())

38 fill `(() : ())

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