4297666 · Idris-dev · git.iko.soy

CHANGELOG+8−1

compare with master

unifiedsplit

@@ -32,7 +32,14 @@ New in 0.9.17:

32* New REPL command ":core TM" that shows the elaborated form of TM along with

33 its elaborated type using the syntax of TT. IDE mode has a corresponding

34 command :elaborate-term for serialized terms.

35−

35+* Effectful and IO function names for sending data to STDOUT have been

36+ aligned, semantically.

37+ + `print` is now for putting showable things to STDOUT.

38+ + `printLn` is for putting showable things to STDOUT with a new line

39+ + `putCharLn` for putting a single character to STDOUT, with a new line.

40+* Classes can now be annotated with 'determining parameters' to say which

41+ must be available before resolving instances. Only determining parameters

42+ are checked when checking for overlapping instances.

36

43

37New in 0.9.16:

44New in 0.9.16:

38--------------

45--------------

Setup.hs+9−2

@@ -57,6 +57,13 @@ usesGMP flags =

57 Just False -> False

58 Nothing -> True

59

60+execOnly :: S.ConfigFlags -> Bool

61+execOnly flags =

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

63+ Just True -> True

64+ Just False -> False

65+ Nothing -> True

66+

60isRelease :: S.ConfigFlags -> Bool

67isRelease :: S.ConfigFlags -> Bool

61isRelease flags =

68isRelease flags =

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

69 case lookup (FlagName "release") (S.configConfigurationsFlags flags) of

@@ -176,7 +183,7 @@ getVersion args flags = do

176 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

183 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

177 return (Just buildinfo, [])

184 return (Just buildinfo, [])

178

185

179−idrisBuild _ flags _ local = do

186+idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do

180 buildStdLib

187 buildStdLib

181 buildRTS

188 buildRTS

182 where

189 where

@@ -199,7 +206,7 @@ idrisBuild _ flags _ local = do

199-- -----------------------------------------------------------------------------

206-- -----------------------------------------------------------------------------

200-- Copy/Install

207-- Copy/Install

201

208

202−idrisInstall verbosity copy pkg local = do

209+idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do

203 installStdLib

210 installStdLib

204 installRTS

211 installRTS

205 where

212 where

benchmarks/quasigroups/Main.idr+2−2

@@ -14,11 +14,11 @@ main = do

14 Left err => putStrLn err

15 Right (_ ** (board ** legal)) => do

16 putStrLn "Got board:"

17− print board

17+ printLn board

18 putStrLn "Solving..."

19 case fillBoard board legal of

20 Nothing => putStrLn "No solution found"

21 Just (solved ** _) => do

22 putStrLn "Solution found:"

23− print solved

23+ printLn solved

24 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

benchmarks/trivial/sortvec.idr+2−3

@@ -13,7 +13,7 @@ vsort [] = []

13vsort (x :: xs) = insert x (vsort xs)

14

15mkSortVec : (n : Nat) -> Eff m [RND] (Vect n Int)

16−mkSortVec Z = return []

16+mkSortVec Z = return []

17mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

18

19main : IO ()

@@ -21,5 +21,4 @@ main = do (_ :: arg :: _) <- getArgs

21-- let arg = "2000"

22 let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))

23 putStrLn "Made vector"

24− print (vsort vec)

24+ printLn (vsort vec)

25−

contribs/lib/SQLite3/testunit.idr+14−14

@@ -7,12 +7,12 @@ testexpr = do db <- open_db "somedb.db"

7 let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (OR (AND (MkCond (Equals (VCol "data")(VStr "data0"))) (MkCond (Equals (VCol "num")(VInt 1))) ) (MkCond (Equals (VCol "num")(VInt 2))))))

8 let x = (fst sql) -- get the string

9 let list = (snd sql) -- list of vals

10− liftIO(print x) -- use liftIO to turn this into DB type

10+ liftIO(printLn x) -- use liftIO to turn this into DB type

11 stmt <- (prepare_db db x) -- prepare the statement

12 bindMulti stmt list -- bind the values in the list

13 exec_db_v2 stmt -- execute the prepared query

14 res <- toList_v1 db -- toList_v1 to get the result

15− liftIO(print res) -- print the result

15+ liftIO(printLn res) -- print the result

16 finalize_db stmt -- Statment pointer must be finalized in the end

17 close_db db -- close the datbase

18 return ()

@@ -22,7 +22,7 @@ testupdate = do db <- open_db "somedb.db"

22 let sql = (evalSQL [] (UPDATE (TBL ["tbl1"]) (WHERE (SET (MkCond (Equals(VCol "data") (VStr "data600"))) ) (MkCond (Equals (VCol "num") (VInt 2))) ) ))

23 let x = (fst sql)

24 let list = (snd sql)

25− liftIO(print x)

25+ liftIO(printLn x)

26 stmt <- (prepare_db db x)

27 bindMulti stmt list

28 exec_db_v2 stmt

@@ -35,7 +35,7 @@ testInsert = do db <- open_db "somedb.db"

35 let sql = (evalSQL [] (INSERT (TBL ["tbl1"]) [(VInt 3),(VStr "ham")]))

36 let x = (fst sql)

37 let list = (snd sql)

38− liftIO(print x)

38+ liftIO(printLn x)

39 stmt <- (prepare_db db x)

40 bindMulti stmt list

41 exec_db_v2 stmt

@@ -48,12 +48,12 @@ testNull = do db <- open_db "somedb.db"

48 let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data")))))

49 let x = (fst sql)

50 let list = (snd sql)

51− liftIO(print x)

51+ liftIO(printLn x)

52 stmt <- (prepare_db db x)

53 bindMulti stmt list

54 exec_db_v2 stmt

55 res <- toList_v1 db

56− liftIO(print res)

56+ liftIO(printLn res)

57 finalize_db stmt

58 close_db db

59 return ()

@@ -64,7 +64,7 @@ testInsertWithCond = do db <- open_db "somedb.db"

64 let sql = (evalSQL [] (INSERTC (TBL ["tbl1"]) [(VCol "data"),(VCol "num")] [(VInt 30),(VStr "inserthere")]))

65 let x = (fst sql)

66 let list = (snd sql)

67− liftIO(print x)

67+ liftIO(printLn x)

68 stmt <- (prepare_db db x)

69 bindMulti stmt list

70 exec_db_v2 stmt

@@ -78,12 +78,12 @@ testNestedSel1 = do db <- open_db "somedb.db"

78 let sql = (evalSQL [] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (MkGT (VCol "num")(VInt 2))))Empty))

79 let x = (fst sql)

80 let list = (snd sql)

81− liftIO(print x)

81+ liftIO(printLn x)

82 stmt <- (prepare_db db x)

83 bindMulti stmt list

84 exec_db_v2 stmt

85 res <- toList_v1 db

86− liftIO(print res)

86+ liftIO(printLn res)

87 finalize_db stmt

88 close_db db

89 return ()

@@ -94,7 +94,7 @@ testCreateTable = do db <- open_db "somedb.db"

94 let sql = (evalSQL [] (CREATE (TBL ["mynewtbl"]) [ ((VCol "col"),(CInt "int"),(None)) ] ) )

95 let x = (fst sql)

96 let list = (snd sql)

97− liftIO(print x)

97+ liftIO(printLn x)

98 stmt <- (prepare_db db x)

99 bindMulti stmt list

100 exec_db_v2 stmt

@@ -108,12 +108,12 @@ testMultiTable = do db <- open_db "somedb.db"

108 let sql = (evalSQL [] ((SELECT ALL )(TBL ["mytable","tbl1"]) (Empty) ) )

109 let x = (fst sql)

110 let list = (snd sql)

111− liftIO(print x)

111+ liftIO(printLn x)

112 stmt <- (prepare_db db x)

113 bindMulti stmt list

114 exec_db_v2 stmt

115 res <- toList_v1 db

116− liftIO(print res)

116+ liftIO(printLn res)

117 finalize_db stmt

118 close_db db

119 return ()

@@ -123,12 +123,12 @@ testSelAll = do db <- open_db "somedb.db"

123 let sql = (evalSQL [] ((SELECT ALL )(TBL ["tbl1"]) (Empty) ) )

124 let x = (fst sql)

125 let list = (snd sql)

126− liftIO(print x)

126+ liftIO(printLn x)

127 stmt <- (prepare_db db x)

128 bindMulti stmt list

129 exec_db_v2 stmt

130 res <- toList_v1 db

131− liftIO(print res)

131+ liftIO(printLn res)

132 finalize_db stmt

133 close_db db

134 return ()

idris.cabal+6

@@ -658,6 +658,11 @@ Flag CI

658 Default: False

659 manual: True

660

661+Flag execonly

662+ Description: Build executables only, skip the libraries and RTS

663+ Default: False

664+ manual: True

665+

661Library

666Library

662 hs-source-dirs: src

667 hs-source-dirs: src

663 Exposed-modules:

668 Exposed-modules:

@@ -725,6 +730,7 @@ Library

725 , Idris.ProofSearch

730 , Idris.ProofSearch

726 , Idris.Prover

731 , Idris.Prover

727 , Idris.Providers

732 , Idris.Providers

733+ , Idris.Reflection

728 , Idris.REPL

734 , Idris.REPL

729 , Idris.REPLParser

735 , Idris.REPLParser

730 , Idris.Transforms

736 , Idris.Transforms

libs/base/Control/Monad/State.idr+1−1

@@ -6,7 +6,7 @@ import Control.Monad.Trans

6%access public

7

8||| A computation which runs in a context and produces an output

9−class Monad m => MonadState s (m : Type -> Type) where

9+class Monad m => MonadState s (m : Type -> Type) | m where

10 ||| Get the context

11 get : m s

12 ||| Write a new context/output

libs/base/Control/Monad/Writer.idr+2−1

@@ -51,7 +51,8 @@ instance Monoid w => MonadTrans (WriterT w) where

51

52||| Run an action in the Writer monad and transform the written output

53listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)

54−listens f m = listens' f (listen m) where

54+listens {m} f act = listens' f (listen act) where

55+ listens' : (w -> b) -> m (a, w) -> m (a, b)

55 listens' f' ma = do (a, w) <- ma

56 listens' f' ma = do (a, w) <- ma

56 return (a, f' w)

57 return (a, f' w)

57

58

libs/base/Data/Fin.idr+1−1

@@ -179,7 +179,7 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m))

179 , TextPart "is less than", TermPart (getNat m)

180 , TextPart "because", TermPart (P Bound n t)

181 , TextPart "is a bound variable instead of a constant"

182− , TermPart (TConst (AType (ATInt ITBig)))

182+ , TermPart `(Integer : Type)

183 ]

184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)

185 = mkFinIntegerErr n m

libs/base/Data/Heap.idr+4−4

@@ -146,7 +146,7 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h =

146isEmptySizeZero Empty p = Refl

147isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd

148

149−total emptyHeapValid : Ord a => isValidHeap empty = True

149+total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True

150emptyHeapValid = Refl

151

152total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

@@ -182,8 +182,8 @@ isEmptySizeZeroNodeAbsurd = proof {

182 does seem to work correctly!

183main : IO ()

184main = do

185− _ <- print $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]

185+ _ <- printLn $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]

186− _ <- print $ main.sort ["orange", "apple", "pear", "lime", "durian"]

186+ _ <- printLn $ main.sort ["orange", "apple", "pear", "lime", "durian"]

187− _ <- print $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]

187+ _ <- printLn $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]

188 return ()

189-}

libs/base/Decidable/Order.idr+4−4

@@ -36,12 +36,12 @@ class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) wher

36 eq (f a) (f b)

37

38minimum : (Ordered t to) => t -> t -> t

39−minimum x y with (order x y)

39+minimum {to} x y with (order {to} x y)

40 | Left _ = x

41 | Right _ = y

42

43maximum : (Ordered t to) => t -> t -> t

44−maximum x y with (order x y)

44+maximum {to} x y with (order {to} x y)

45 | Left _ = y

46 | Right _ = x

47

@@ -103,7 +103,7 @@ total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)

103decideLTE Z y = Yes LTEZero

104decideLTE (S x) Z = No zeroNeverGreater

105decideLTE (S x) (S y) with (decEq (S x) (S y))

106− | Yes eq = rewrite eq in Yes (reflexive x)

106+ | Yes eq = rewrite eq in Yes (reflexive (S y))

107 | No _ with (decideLTE x y)

108 | Yes nLTEm = Yes (LTESucc nLTEm)

109 | No nGTm = No (ltesuccinjective nGTm)

@@ -122,7 +122,7 @@ shift m n mLTEn = LTESucc mLTEn

122instance Ordered Nat LTE where

123 order Z n = Left LTEZero

124 order m Z = Right LTEZero

125− order (S k) (S j) with (order k j)

125+ order (S k) (S j) with (order {to=LTE} k j)

126 order (S k) (S j) | Left prf = Left (shift k j prf)

127 order (S k) (S j) | Right prf = Right (shift j k prf)

128

libs/base/Language/Reflection/Utils.idr+1

@@ -272,6 +272,7 @@ instance Show Err where

272 show (CantResolve tm) = "CantResolve " ++ show tm

273 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

274 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

275+ show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

275 show UniverseError = "UniverseError"

276 show UniverseError = "UniverseError"

276 show ProgramLineComment = "ProgramLineComment"

277 show ProgramLineComment = "ProgramLineComment"

277 show (Inaccessible n) = "Inaccessible " ++ show n

278 show (Inaccessible n) = "Inaccessible " ++ show n

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

@@ -4,7 +4,7 @@ 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

9

10instance Handler (Exception a) Maybe where

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

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

18 believe_me (exit 1)

19

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

@@ -26,7 +26,7 @@ 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 -> { [EXCEPTION a ] } Eff b

30raise err = call $ Raise err

31

32

@@ -39,4 +39,3 @@ raise err = call $ Raise err

39

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

41-- handler can be introduced mid interpretation?

42−

libs/effects/Effect/StdIO.idr+7−3

@@ -42,13 +42,17 @@ STDIO = MkEff () StdIO

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

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+

45||| Write a character to standard output.

49||| Write a character to standard output.

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

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

47putChar c = call $ PutCh c

51putChar c = call $ PutCh c

48

52

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

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

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

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

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

55+putCharLn c = putStrLn (singleton c)

52

56

53||| Read a string from standard input.

57||| Read a string from standard input.

54getStr : { [STDIO] } Eff String

58getStr : { [STDIO] } Eff String

libs/oldeffects/Effect/Exception.idr+3−4

@@ -4,7 +4,7 @@ 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

9

10instance Handler (Exception a) Maybe where

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

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

18 believe_me (exit 1)

19

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

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

26EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

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

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

30raise err = call $ Raise err

31

32

@@ -39,4 +39,3 @@ raise err = call $ Raise err

39

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

41-- handler can be introduced mid interpretation?

42−

libs/prelude/Language/Reflection.idr+6−6

@@ -416,14 +416,14 @@ instance Quotable NameType Raw where

416 quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))

417

418instance Quotable a TT => Quotable (List a) TT where

419− quotedTy = `(List ~(quotedTy {a=a}))

419+ quotedTy = `(List ~(quotedTy {a}))

420− quote [] = `(List.Nil {a=~quotedTy})

420+ quote [] = `(List.Nil {a=~(quotedTy {a})})

421− quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))

421+ quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))

422

423instance Quotable a Raw => Quotable (List a) Raw where

424− quotedTy = `(List ~(quotedTy {a=a}))

424+ quotedTy = `(List ~(quotedTy {a}))

425− quote [] = `(List.Nil {a=~quotedTy})

425+ quote [] = `(List.Nil {a=~(quotedTy {a})})

426− quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))

426+ quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))

427

428instance Quotable TTName TT where

429 quotedTy = `(TTName)

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

@@ -31,6 +31,7 @@ data Err = Msg String

31 | CantResolve TT

32 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34+ | NoEliminator String TT

34 | UniverseError

35 | UniverseError

35 | ProgramLineComment

36 | ProgramLineComment

36 | Inaccessible TTName

37 | Inaccessible TTName

libs/prelude/Language/Reflection/Tactical.idr+14

@@ -8,6 +8,14 @@ import Prelude.Maybe

8import Prelude.Monad

9import 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+

11abstract

19abstract

12data Tactical : Type -> Type where

20data Tactical : Type -> Type where

13 -- obligatory control stuff

21 -- obligatory control stuff

@@ -39,8 +47,11 @@ data Tactical : Type -> Type where

39 prim__Claim : TTName -> Raw -> Tactical ()

47 prim__Claim : TTName -> Raw -> Tactical ()

40 prim__Intro : Maybe TTName -> Tactical ()

48 prim__Intro : Maybe TTName -> Tactical ()

41

49

50+ prim__DeclareType : TyDecl -> Tactical ()

51+

42 prim__Debug : {a : Type} -> Maybe String -> Tactical a

52 prim__Debug : {a : Type} -> Maybe String -> Tactical a

43

53

54+

44-------------

55-------------

45-- Public API

56-- Public API

46-------------

57-------------

@@ -117,6 +128,9 @@ sourceLocation = do loc <- getSourceLocation

117rewriteWith : Raw -> Tactical ()

128rewriteWith : Raw -> Tactical ()

118rewriteWith rule = prim__Rewrite rule

129rewriteWith rule = prim__Rewrite rule

119

130

131+declareType : TyDecl -> Tactical ()

132+declareType decl = prim__DeclareType decl

133+

120debug : Tactical a

134debug : Tactical a

121debug = prim__Debug Nothing

135debug = prim__Debug Nothing

122

136

libs/prelude/Prelude.idr+15−5

@@ -442,20 +442,30 @@ putStr x = do prim_write x

442putStrLn : String -> IO' ffi ()

443putStrLn x = putStr (x ++ "\n")

444

445−||| Output something showable to stdout, with a trailing newline

445+||| Output something showable to stdout, without a trailing newline

446partial

447print : Show a => a -> IO' ffi ()

448+print x = putStr (show x)

449+

450+||| Output something showable to stdout, with a trailing newline

451+partial

452+printLn : Show a => a -> IO' ffi ()

448−print x = putStrLn (show x)

453+printLn x = putStrLn (show x)

449

454

450||| Read one line of input from stdin

455||| Read one line of input from stdin

451partial

456partial

452getLine : IO' ffi String

457getLine : IO' ffi String

453−getLine = prim_read

458+getLine = prim_read

454

459

455||| Write a single character to stdout

460||| Write a single character to stdout

456partial

461partial

457putChar : Char -> IO ()

462putChar : Char -> IO ()

458−putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

463+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)

464+

465+||| Write a singel character to stdout, with a trailing newline

466+partial

467+putCharLn : Char -> IO ()

468+putCharLn c = putStrLn (singleton c)

459

469

460||| Read a single character from stdin

470||| Read a single character from stdin

461partial

471partial

@@ -484,7 +494,7 @@ stderr = FHandle prim__stderr

484do_fopen : String -> String -> IO Ptr

494do_fopen : String -> String -> IO Ptr

485do_fopen f m

495do_fopen f m

486 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

496 = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

487−

497+

488||| Open a file

498||| Open a file

489||| @ f the filename

499||| @ f the filename

490||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

500||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)

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

@@ -316,7 +316,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where

316

317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

318 total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

319− total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v

319+ total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v

320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

322

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

@@ -31,7 +31,7 @@ infixl 9 .

31

32||| Function composition

33(.) : (b -> c) -> (a -> b) -> a -> c

34−(.) f g x = f (g x)

34+(.) f g = \x => f (g x)

35

36||| Takes in the first two arguments in reverse order.

37||| @ f the function to flip

samples/binary.idr+1−2

@@ -41,7 +41,7 @@ adc (numx # bx) (numy # by) carry

41main : IO ()

42main = do let n1 = zero # b1 # b0 # b1 # b0

43 let n2 = zero # b1 # b1 # b1 # b0

44− print (adc n1 n2 b0)

44+ printLn (adc n1 n2 b0)

45

46

47

@@ -92,4 +92,3 @@ main.adc_lemma_1 = proof {

92 rewrite sym (plusZeroRightNeutral c) ;

93 trivial;

94}

95−

samples/interp-alt.idr+2−2

@@ -77,5 +77,5 @@ testFac : Int

77testFac = interp [] eFac 4

78

79main : IO ()

80−main = do print test

80+main = do printLn test

81− print testFac

81+ printLn testFac

samples/interp.idr+1−2

@@ -88,5 +88,4 @@ testFac : Int

88testFac = interp [] eFac 4

89

90main : IO ()

91−main = print testFac

91+main = printLn testFac

92−

samples/javaffi.idr+1−1

@@ -9,4 +9,4 @@ binom n k = mkForeign (FFun "IntMath.binomial" [FInt, FInt] FInt) n k

9main : IO ()

10main = do print "The number of possibilities in lotto is 49 choose 6:"

11 res <- binom 49 6

12− print res

12+ printLn res

src/Idris/AbsSyntax.hs+19−5

@@ -360,10 +360,10 @@ addInstance :: Bool -> Name -> Name -> Idris ()

360addInstance int n i

361 = do ist <- getIState

362 case lookupCtxt n (idris_classes ist) of

363− [CI a b c d e ins] ->

363+ [CI a b c d e ins fds] ->

364− do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)

364+ do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)

365 putIState $ ist { idris_classes = cs }

366− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)

366+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i] []) (idris_classes ist)

367 putIState $ ist { idris_classes = cs }

368 where addI i ins | int = i : ins

369 | chaser n = ins ++ [i]

@@ -455,6 +455,10 @@ getIState = get

455putIState :: IState -> Idris ()

456putIState = put

457

458+updateIState :: (IState -> IState) -> Idris ()

459+updateIState f = do i <- getIState

460+ putIState $ f i

461+

458withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b

462withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b

459withContext ctx name dflt action = do

463withContext ctx name dflt action = do

460 ist <- getIState

464 ist <- getIState

@@ -547,7 +551,16 @@ addConstraints fc (v, cs)

547addDeferred = addDeferred' Ref

551addDeferred = addDeferred' Ref

548addDeferredTyCon = addDeferred' (TCon 0 0)

552addDeferredTyCon = addDeferred' (TCon 0 0)

549

553

554+-- | Save information about a name that is not yet defined

555+addDeferred' :: NameType

550−addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

556+ -> [(Name, (Int, Maybe Name, Type, Bool))]

557+ -- ^ The Name is the name being made into a metavar,

558+ -- the Int is the number of vars that are part of a

559+ -- putative proof context, the Maybe Name is the

560+ -- top-level function containing the new metavariable,

561+ -- the Type is its type, and the Bool is whether :p is

562+ -- allowed

563+ -> Idris ()

551addDeferred' nt ns

564addDeferred' nt ns

552 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

565 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

553 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

566 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

@@ -1075,12 +1088,13 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

1075-- (map (expandParamsD ist dec ps ns) pds)

1088-- (map (expandParamsD ist dec ps ns) pds)

1076expandParamsD rhs ist dec ps ns (PMutual f pds)

1089expandParamsD rhs ist dec ps ns (PMutual f pds)

1077 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1090 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1078−expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

1091+expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)

1079 = PClass doc info f

1092 = PClass doc info f

1080 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1093 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1081 n

1094 n

1082 (map (mapsnd (expandParams dec ps ns [])) params)

1095 (map (mapsnd (expandParams dec ps ns [])) params)

1083 pDocs

1096 pDocs

1097+ fds

1084 (map (expandParamsD rhs ist dec ps ns) decls)

1098 (map (expandParamsD rhs ist dec ps ns) decls)

1085expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1099expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1086 = PInstance doc argDocs info f

1100 = PInstance doc argDocs info f

src/Idris/AbsSyntaxTree.hs+16−8

@@ -184,7 +184,11 @@ data IState = IState {

184 idris_name :: Int,

185 idris_lineapps :: [((FilePath, Int), PTerm)],

186 -- ^ Full application LHS on source line

187+ idris_metavars :: [(Name, (Maybe Name, Int, Bool))],

187− idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

188+ -- ^ The currently defined but not proven metavariables. The Int

189+ -- is the number of vars to display as a context, the Maybe Name

190+ -- is its top-level function, and the Bool is whether :p is

191+ -- allowed

188 idris_coercions :: [Name],

192 idris_coercions :: [Name],

189 idris_errRev :: [(Term, Term)],

193 idris_errRev :: [(Term, Term)],

190 syntax_rules :: SyntaxRules,

194 syntax_rules :: SyntaxRules,

@@ -599,6 +603,7 @@ data PDecl' t

599 Name

603 Name

600 [(Name, t)] -- parameters

604 [(Name, t)] -- parameters

601 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

605 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

606+ [Name] -- determining parameters

602 [PDecl' t] -- declarations

607 [PDecl' t] -- declarations

603 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

608 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

604 -- class name, parameters, method declarations

609 -- class name, parameters, method declarations

@@ -631,10 +636,12 @@ deriving instance NFData PDecl'

631-- For elaborator state

636-- For elaborator state

632data EState = EState {

637data EState = EState {

633 case_decls :: [PDecl],

638 case_decls :: [PDecl],

634− delayed_elab :: [Elab' EState ()]

639+ delayed_elab :: [Elab' EState ()],

640+ new_tyDecls :: [(Name, FC, [PArg], Type)]

635 }

641 }

636

642

637−initEState = EState [] []

643+initEState :: EState

644+initEState = EState [] [] []

638

645

639type ElabD a = Elab' EState a

646type ElabD a = Elab' EState a

640

647

@@ -693,7 +700,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

693declared (PParams _ _ ds) = concatMap declared ds

700declared (PParams _ _ ds) = concatMap declared ds

694declared (PNamespace _ ds) = concatMap declared ds

701declared (PNamespace _ ds) = concatMap declared ds

695declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

702declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

696−declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

703+declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms

697declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

704declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

698declared (PDSL n _) = [n]

705declared (PDSL n _) = [n]

699declared (PSyntax _ _) = []

706declared (PSyntax _ _) = []

@@ -712,7 +719,7 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

712tldeclared (PParams _ _ ds) = []

719tldeclared (PParams _ _ ds) = []

713tldeclared (PMutual _ ds) = concatMap tldeclared ds

720tldeclared (PMutual _ ds) = concatMap tldeclared ds

714tldeclared (PNamespace _ ds) = concatMap tldeclared ds

721tldeclared (PNamespace _ ds) = concatMap tldeclared ds

715−tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

722+tldeclared (PClass _ _ _ _ n _ _ _ ms) = concatMap tldeclared ms

716tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

723tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

717tldeclared _ = []

724tldeclared _ = []

718

725

@@ -728,7 +735,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

728defined (PParams _ _ ds) = concatMap defined ds

735defined (PParams _ _ ds) = concatMap defined ds

729defined (PNamespace _ ds) = concatMap defined ds

736defined (PNamespace _ ds) = concatMap defined ds

730defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

737defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

731−defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

738+defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms

732defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

739defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

733defined (PDSL n _) = [n]

740defined (PDSL n _) = [n]

734defined (PSyntax _ _) = []

741defined (PSyntax _ _) = []

@@ -1029,7 +1036,8 @@ data ClassInfo = CI { instanceName :: Name,

1029 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

1036 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

1030 class_default_superclasses :: [PDecl],

1037 class_default_superclasses :: [PDecl],

1031 class_params :: [Name],

1038 class_params :: [Name],

1032− class_instances :: [Name] }

1039+ class_instances :: [Name],

1040+ class_determiners :: [Int] }

1033 deriving Show

1041 deriving Show

1034{-!

1042{-!

1035deriving instance Binary ClassInfo

1043deriving instance Binary ClassInfo

@@ -1727,7 +1735,7 @@ showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

1727showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1735showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1728showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

1736showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

1729showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1737showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1730−showDeclImp o (PClass _ _ _ cs n ps _ ds)

1738+showDeclImp o (PClass _ _ _ cs n ps _ _ ds)

1731 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1739 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1732showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1740showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1733 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1741 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

src/Idris/Core/Binary.hs+13−3

@@ -29,6 +29,8 @@ instance Binary Provenance where

29 put t

30 put InferredVal = putWord8 2

31 put GivenVal = putWord8 3

32+ put (TooManyArgs t) = do putWord8 4

33+ put t

32

34

33 get = do i <- getWord8

35 get = do i <- getWord8

34 case i of

36 case i of

@@ -37,6 +39,8 @@ instance Binary Provenance where

37 return (SourceTerm x1)

39 return (SourceTerm x1)

38 2 -> return InferredVal

40 2 -> return InferredVal

39 3 -> return GivenVal

41 3 -> return GivenVal

42+ 4 -> do x1 <- get

43+ return (TooManyArgs x1)

40 _ -> error "Corrupted binary data for Provenance"

44 _ -> error "Corrupted binary data for Provenance"

41

45

42instance Binary a => Binary (Err' a) where

46instance Binary a => Binary (Err' a) where

@@ -87,8 +91,8 @@ instance Binary a => Binary (Err' a) where

87 put x

91 put x

88 put y

92 put y

89 put z

93 put z

90− put (CantResolve t) = do putWord8 15

94+ put (CantResolve _ t) = do putWord8 15

91− put t

95+ put t

92 put (CantResolveAlts ns) = do putWord8 16

96 put (CantResolveAlts ns) = do putWord8 16

93 put ns

97 put ns

94 put (IncompleteTerm t) = do putWord8 17

98 put (IncompleteTerm t) = do putWord8 17

@@ -142,6 +146,9 @@ instance Binary a => Binary (Err' a) where

142 put x1

146 put x1

143 put x2

147 put x2

144 put x3

148 put x3

149+ put (NoEliminator s t) = do putWord8 37

150+ put s

151+ put t

145

152

146 get = do i <- getWord8

153 get = do i <- getWord8

147 case i of

154 case i of

@@ -168,7 +175,7 @@ instance Binary a => Binary (Err' a) where

168 13 -> fmap NoTypeDecl get

175 13 -> fmap NoTypeDecl get

169 14 -> do x <- get ; y <- get ; z <- get

176 14 -> do x <- get ; y <- get ; z <- get

170 return $ NotInjective x y z

177 return $ NotInjective x y z

171− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

172 16 -> fmap CantResolveAlts get

179 16 -> fmap CantResolveAlts get

173 17 -> fmap IncompleteTerm get

180 17 -> fmap IncompleteTerm get

174 18 -> return UniverseError

181 18 -> return UniverseError

@@ -201,6 +208,9 @@ instance Binary a => Binary (Err' a) where

201 x2 <- get

208 x2 <- get

202 x3 <- get

209 x3 <- get

203 return (ElabDebug x1 x2 x3)

210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

204 _ -> error "Corrupted binary data for Err'"

214 _ -> error "Corrupted binary data for Err'"

205----- Generated by 'derive'

215----- Generated by 'derive'

206

216

src/Idris/Core/DeepSeq.hs+3−1

@@ -48,6 +48,7 @@ instance NFData Provenance where

48 rnf InferredVal = ()

49 rnf GivenVal = ()

50 rnf (SourceTerm x1) = rnf x1 `seq` ()

51+ rnf (TooManyArgs x1) = rnf x1 `seq` ()

51

52

52instance NFData Err where

53instance NFData Err where

53 rnf (Msg x1) = rnf x1 `seq` ()

54 rnf (Msg x1) = rnf x1 `seq` ()

@@ -79,9 +80,10 @@ instance NFData Err where

79 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

80 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

80 rnf (NotInjective x1 x2 x3)

81 rnf (NotInjective x1 x2 x3)

81 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

82 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

82− rnf (CantResolve x1) = rnf x1 `seq` ()

83+ rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

83 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

84 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

84 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

85 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

86+ rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

85 rnf UniverseError = ()

87 rnf UniverseError = ()

86 rnf ProgramLineComment = ()

88 rnf ProgramLineComment = ()

87 rnf (Inaccessible x1) = rnf x1 `seq` ()

89 rnf (Inaccessible x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+30−14

@@ -756,20 +756,20 @@ handleError p t1 t2 proofSearch

756

757try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

758try' t1 t2 proofSearch

759− = do s <- get

759+ = do s <- get

760− ps <- get_probs

760+ ps <- get_probs

761− ulog <- getUnifyLog

761+ ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

762+ case prunStateT 999999 False ps t1 s of

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

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

764− return $! v

764+ return $! v

765− Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

765+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766− if recoverableErr e1 then

766+ if recoverableErr e1 then

767− do case runStateT t2 s of

767+ do case runStateT t2 s of

768− OK (v, s') -> do put s'; return $! v

768+ OK (v, s') -> do put s'; return $! v

769− Error e2 -> if score e1 >= score e2

769+ Error e2 -> if score e1 >= score e2

770− then lift (tfail e1)

770+ then lift (tfail e1)

771− else lift (tfail e2)

771+ else lift (tfail e2)

772− else lift (tfail e1)

772+ else lift (tfail e1)

773 where recoverableErr err@(CantUnify r x y _ _ _)

774 = -- traceWhen r (show err) $

775 r || proofSearch

@@ -782,6 +782,22 @@ try' t1 t2 proofSearch

782 recoverableErr (ElabDebug _ _ _) = False

783 recoverableErr _ = True

784

785+tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

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

792+ return $! v

793+ Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

794+ case runStateT (t2 e1) s of

795+ OK (v, s') -> do put s'

796+ return $! v

797+ Error e2 -> if score e1 >= score e2

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

785tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

801tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

786tryWhen True a b = try a b

802tryWhen True a b = try a b

787tryWhen False a b = a

803tryWhen False a b = a

src/Idris/Core/ProofState.hs+17−7

@@ -478,12 +478,19 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

478-- let valtyn = normalise ctxt env valty

479-- let tyn = normalise ctxt env ty

480 ns <- unify' ctxt env (valty, Just $ SourceTerm val)

481− (ty, Just ExpectedType)

481+ (ty, Just (chkPurpose val ty))

482 ps <- get

483 let (uh, uns) = unified ps

484-- put (ps { unified = (uh, uns ++ ns) })

485-- addLog (show (uh, uns ++ ns))

486 return $ Bind x (Guess ty val) sc

487+ where

488+ -- some expected types show up commonly in errors and indicate a

489+ -- specific problem.

490+ -- argTy -> retTy suggests a function applied to too many arguments

491+ chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))

492+ = TooManyArgs val

493+ chkPurpose _ _ = ExpectedType

487fill _ _ _ _ = fail "Can't fill here."

494fill _ _ _ _ = fail "Can't fill here."

488

495

489-- As fill, but attempts to solve other goals by matching

496-- As fill, but attempts to solve other goals by matching

@@ -674,8 +681,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

674 (tmv, tmt) <- lift $ check ctxt env tm

681 (tmv, tmt) <- lift $ check ctxt env tm

675 let tmt' = normalise ctxt env tmt

682 let tmt' = normalise ctxt env tmt

676 let (tacn, tacstr, tactt) = if induction

683 let (tacn, tacstr, tactt) = if induction

677− then (ElimN, "an eliminator", "Induction")

684+ then (ElimN, "eliminator", "Induction")

678− else (CaseN, "a case function", "Case analysis")

685+ else (CaseN, "case analysis", "Case analysis")

679 case unApply tmt' of

686 case unApply tmt' of

680 (P _ tnm _, tyargs) -> do

687 (P _ tnm _, tyargs) -> do

681 case lookupTy (SN (tacn tnm)) ctxt of

688 case lookupTy (SN (tacn tnm)) ctxt of

@@ -710,9 +717,10 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

710 (scv, sct) <- lift $ check ctxt env res'

717 (scv, sct) <- lift $ check ctxt env res'

711 let (scv', _) = specialise ctxt env [] scv

718 let (scv', _) = specialise ctxt env [] scv

712 return scv'

719 return scv'

713− [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

720+ [] -> lift $ tfail $ NoEliminator tacstr tmt'

714 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

721 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

715− _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

722+ _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")

723+ tmt'

716 where scname = sMN 0 "scarg"

724 where scname = sMN 0 "scarg"

717 makeConsArg (nm, ty) = P Bound nm ty

725 makeConsArg (nm, ty) = P Bound nm ty

718 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

726 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

@@ -871,6 +879,7 @@ updateProblems ps updates probs = up updates probs where

871 ctxt = context ps

879 ctxt = context ps

872 ulog = unifylog ps

880 ulog = unifylog ps

873 usupp = map fst (notunified ps)

881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

874

883

875 up ns [] = (ns, [])

884 up ns [] = (ns, [])

876 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

885 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

@@ -882,8 +891,9 @@ updateProblems ps updates probs = up updates probs where

882 if newx || newy || ready ||

891 if newx || newy || ready ||

883 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

892 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

884 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of

893 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of

885− OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

894+ OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $

895+ let v' = filter (\(n, _) -> n `notElem` dont) v in

886− up (ns ++ v) ps

896+ up (ns ++ v') ps

887 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

897 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

888 let (ns', ps') = up ns ps in

898 let (ns', ps') = up ns ps in

889 (ns', (x',y', False, env',err', while, um) : ps')

899 (ns', (x',y', False, env',err', while, um) : ps')

src/Idris/Core/ProofTerm.hs+3

@@ -172,6 +172,9 @@ updateSolvedTerm' xs x = updateSolved' xs x where

172 else (t, False)

173 updateSolved' xs t@(P _ n@(MN _ _) _)

174 | Just v <- lookup n xs = (v, True)

175+ updateSolved' xs t@(P nt n ty)

176+ = let (ty', ut) = updateSolved' xs ty in

177+ if ut then (P nt n ty', True) else (t, False)

175 updateSolved' xs t = (t, False)

178 updateSolved' xs t = (t, False)

176

179

177 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

180 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

src/Idris/Core/TT.hs+12−4

@@ -121,6 +121,7 @@ data ErrorReportPart = TextPart String

121-- Language.Reflection.Errors.Err in the stdlib!

122

123data Provenance = ExpectedType

124+ | TooManyArgs Term

124 | InferredVal

125 | InferredVal

125 | GivenVal

126 | GivenVal

126 | SourceTerm Term

127 | SourceTerm Term

@@ -154,9 +155,11 @@ data Err' t

154 | WithFnType t

155 | WithFnType t

155 | NoTypeDecl Name

156 | NoTypeDecl Name

156 | NotInjective t t t

157 | NotInjective t t t

157− | CantResolve t

158+ | CantResolve Bool -- True if postponed, False if fatal

159+ t

158 | CantResolveAlts [Name]

160 | CantResolveAlts [Name]

159 | IncompleteTerm t

161 | IncompleteTerm t

162+ | NoEliminator String t

160 | UniverseError

163 | UniverseError

161 | UniqueError Universe Name

164 | UniqueError Universe Name

162 | UniqueKindError Universe Name

165 | UniqueKindError Universe Name

@@ -230,7 +233,7 @@ instance Sized Err where

230 size (NoSuchVariable name) = size name

233 size (NoSuchVariable name) = size name

231 size (NoTypeDecl name) = size name

234 size (NoTypeDecl name) = size name

232 size (NotInjective l c r) = size l + size c + size r

235 size (NotInjective l c r) = size l + size c + size r

233− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

234 size (NoRewriting trm) = size trm

237 size (NoRewriting trm) = size trm

235 size (CantResolveAlts _) = 1

238 size (CantResolveAlts _) = 1

236 size (IncompleteTerm trm) = size trm

239 size (IncompleteTerm trm) = size trm

@@ -245,7 +248,7 @@ instance Sized Err where

245

248

246score :: Err -> Int

249score :: Err -> Int

247score (CantUnify _ _ _ m _ s) = s + score m

250score (CantUnify _ _ _ m _ s) = s + score m

248−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

249score (NoSuchVariable _) = 1000

252score (NoSuchVariable _) = 1000

250score (ProofSearchFail e) = score e

253score (ProofSearchFail e) = score e

251score (CantSolveGoal _ _) = 100000

254score (CantSolveGoal _ _) = 100000

@@ -506,7 +509,7 @@ toAlist :: Ctxt a -> [(Name, a)]

506toAlist ctxt = let allns = map snd (Map.toList ctxt) in

509toAlist ctxt = let allns = map snd (Map.toList ctxt) in

507 concatMap (Map.toList) allns

510 concatMap (Map.toList) allns

508

511

509−addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a

512+addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a

510addAlist [] ctxt = ctxt

513addAlist [] ctxt = ctxt

511addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

514addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

512

515

@@ -933,6 +936,7 @@ vinstances i t = 0

933-- | Replace the outermost (index 0) de Bruijn variable with the given term

936-- | Replace the outermost (index 0) de Bruijn variable with the given term

934instantiate :: TT n -> TT n -> TT n

937instantiate :: TT n -> TT n -> TT n

935instantiate e = subst 0 where

938instantiate e = subst 0 where

939+ subst i (P nt x ty) = P nt x (subst i ty)

936 subst i (V x) | i == x = e

940 subst i (V x) | i == x = e

937 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

941 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

938 subst i (App f a) = App (subst i f) (subst i a)

942 subst i (App f a) = App (subst i f) (subst i a)

@@ -944,6 +948,7 @@ instantiate e = subst 0 where

944-- that has been substituted.

948-- that has been substituted.

945substV :: TT n -> TT n -> TT n

949substV :: TT n -> TT n -> TT n

946substV x tm = dropV 0 (instantiate x tm) where

950substV x tm = dropV 0 (instantiate x tm) where

951+ subst i (P nt x ty) = P nt x (subst i ty)

947 dropV i (V x) | x > i = V (x - 1)

952 dropV i (V x) | x > i = V (x - 1)

948 | otherwise = V x

953 | otherwise = V x

949 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

954 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

@@ -1037,6 +1042,9 @@ subst n v tm = fst $ subst' 0 tm

1037 -- substitution happens...)

1042 -- substitution happens...)

1038 subst' i (V x) | i == x = (v, True)

1043 subst' i (V x) | i == x = (v, True)

1039 subst' i (P _ x _) | n == x = (v, True)

1044 subst' i (P _ x _) | n == x = (v, True)

1045+ subst' i t@(P nt x ty)

1046+ = let (ty', ut) = subst' i ty in

1047+ if ut then (P nt x ty', True) else (t, False)

1040 subst' i t@(Bind x b sc) | x /= n

1048 subst' i t@(Bind x b sc) | x /= n

1041 = let (b', ub) = substB' i b

1049 = let (b', ub) = substB' i b

1042 (sc', usc) = subst' (i+1) sc in

1050 (sc', usc) = subst' (i+1) sc in

src/Idris/Core/Unify.hs+2−2

@@ -100,7 +100,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

100 | (P (TCon _ _) _ _, _) <- unApply x,

101 holeIn env f || f `elem` holes

102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

103− checkCycle names (f, Bind n' (Lam t) x)

103+ checkCycle names (f, Bind n' (Lam t) x)

104 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

105 | (P (TCon _ _) _ _, _) <- unApply x,

106 holeIn env f || f `elem` holes

@@ -110,7 +110,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

110 | (P (DCon _ _ _) _ _, _) <- unApply x,

111 holeIn env f || f `elem` holes

112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

113− checkCycle names (f, Bind n' (Lam t) x)

113+ checkCycle names (f, Bind n' (Lam t) x)

114 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

115 | (P (DCon _ _ _) _ _, _) <- unApply x,

116 holeIn env f || f `elem` holes

src/Idris/DeepSeq.hs+4−4

@@ -149,10 +149,10 @@ instance (NFData t) => NFData (PDecl' t) where

149 rnf x2 `seq`

150 rnf x3 `seq`

151 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

152− rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7)

152+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)

153 = rnf x1 `seq`

154 rnf x2 `seq`

155− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

155+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

156 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

157 = rnf x1 `seq`

158 rnf x2 `seq`

@@ -313,9 +313,9 @@ instance (NFData t) => NFData (PArg' t) where

313 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

314

315instance NFData ClassInfo where

316− rnf (CI x1 x2 x3 x4 x5 x6)

316+ rnf (CI x1 x2 x3 x4 x5 x6 x7)

317 = rnf x1 `seq`

318− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

318+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

319

320instance NFData OptInfo where

321 rnf (Optimise x1 x2)

src/Idris/Delaborate.hs+12−1

@@ -202,6 +202,11 @@ pprintProv i e (SourceTerm tm)

202 = text "Type of " <>

203 annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

204 (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))

205+pprintProv i e (TooManyArgs tm)

206+ = text "Is " <>

207+ annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

208+ (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))

209+ <> text " applied to too many arguments?"

205

210

206pprintErr :: IState -> Err -> Doc OutputAnnotation

211pprintErr :: IState -> Err -> Doc OutputAnnotation

207pprintErr i err = pprintErr' i (fmap (errReverse i) err)

212pprintErr i err = pprintErr' i (fmap (errReverse i) err)

@@ -284,7 +289,7 @@ pprintErr' i (NotInjective p x y) =

284 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

289 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

285 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

286 annTm y (pprintTerm i (delab i y))

291 annTm y (pprintTerm i (delab i y))

287−pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

292+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

288pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

293pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

289 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

294 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

290pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

295pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

@@ -294,6 +299,12 @@ pprintErr' i (WithFnType ty) =

294pprintErr' i (CantMatch t) =

299pprintErr' i (CantMatch t) =

295 text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

300 text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

296pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

301pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

302+pprintErr' i (NoEliminator s t)

303+ = text "No " <> text s <> text " for type " <+>

304+ annTm t (pprintTerm i (delab i t)) <$>

305+ text "Please note that 'induction' is experimental." <$>

306+ text "Only types declared with '%elim' can be used." <$>

307+ text "Consider writing a pattern matching definition instead."

297pprintErr' i UniverseError = text "Universe inconsistency"

308pprintErr' i UniverseError = text "Universe inconsistency"

298pprintErr' i (UniqueError NullType n)

309pprintErr' i (UniqueError NullType n)

299 = text "Borrowed name" <+> annName' n (showbasic n)

310 = text "Borrowed name" <+> annName' n (showbasic n)

src/Idris/Elab/Class.hs+28−10

@@ -50,12 +50,13 @@ import Data.List.Split (splitOn)

50

51import Util.Pretty(pretty, text)

52

53−data MArgTy = IA | EA | CA deriving Show

53+data MArgTy = IA Name | EA Name | CA deriving Show

54

55elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

56 FC -> [(Name, PTerm)] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [PDecl] -> Idris ()

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58+ [Name] -> [PDecl] -> Idris ()

58−elabClass info syn_in doc fc constraints tn ps pDocs ds

59+elabClass info syn_in doc fc constraints tn ps pDocs fds ds

59 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

60 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

60 let tty = pibind ps PType

61 let tty = pibind ps PType

61 let constraint = PApp fc (PRef fc tn)

62 let constraint = PApp fc (PRef fc tn)

@@ -75,7 +76,6 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

75 let (methods, imethods)

76 let (methods, imethods)

76 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

77 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

77 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

78 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

78− addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])

79 -- build instance constructor type

80 -- decorate names of functions to ensure they can't be referred

81 -- to elsewhere in the class declaration

@@ -86,6 +86,9 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

86 let ddecl = PDatadecl tn tty cons

87 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

88 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

89+

90+ dets <- findDets cn fds

91+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

89 -- for each constraint, build a top level function to chase it

92 -- for each constraint, build a top level function to chase it

90 logLvl 5 $ "Building functions"

93 logLvl 5 $ "Building functions"

91-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

94-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -94,6 +97,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

94 mapM_ (rec_elabDecl info EAll info) (concat fns)

97 mapM_ (rec_elabDecl info EAll info) (concat fns)

95 -- for each method, build a top level function

98 -- for each method, build a top level function

96 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

99 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

100+ logLvl 5 $ "Functions " ++ show fns

97 mapM_ (rec_elabDecl info EAll info) (concat fns)

101 mapM_ (rec_elabDecl info EAll info) (concat fns)

98 -- add the default definitions

102 -- add the default definitions

99 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

103 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

@@ -201,21 +205,21 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

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

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

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

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

203

207

204− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

208+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA n : getMArgs sc

205− getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

209+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA n : getMArgs sc

206 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

210 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

207 getMArgs _ = []

211 getMArgs _ = []

208

212

209 getMeth (m:ms) (a:as) x | x == a = PRef fc m

213 getMeth (m:ms) (a:as) x | x == a = PRef fc m

210 | otherwise = getMeth ms as x

214 | otherwise = getMeth ms as x

211

215

212− lhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns

216+ lhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns

213− lhsArgs (IA : xs) ns = lhsArgs xs ns

217+ lhsArgs (IA n : xs) ns = pimp n (PRef fc n) False : lhsArgs xs ns

214 lhsArgs (CA : xs) ns = lhsArgs xs ns

218 lhsArgs (CA : xs) ns = lhsArgs xs ns

215 lhsArgs [] _ = []

219 lhsArgs [] _ = []

216

220

217− rhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns

221+ rhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns

218− rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns

222+ rhsArgs (IA n : xs) ns = pexp (PRef fc n) : rhsArgs xs ns

219 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

223 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

220 rhsArgs [] _ = []

224 rhsArgs [] _ = []

221

225

@@ -230,3 +234,17 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

234 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

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

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

232 toExp ns e sc = sc

236 toExp ns e sc = sc

237+

238+findDets :: Name -> [Name] -> Idris [Int]

239+findDets n ns =

240+ do i <- getIState

241+ return $ case lookupTyExact n (tt_ctxt i) of

242+ Just ty -> getDetPos 0 ns ty

243+ Nothing -> []

244+ where

245+ getDetPos i ns (Bind n (Pi _ _ _) sc)

246+ | n `elem` ns = i : getDetPos (i + 1) ns sc

247+ | otherwise = getDetPos (i + 1) ns sc

248+ getDetPos _ _ _ = []

249+

250+

src/Idris/Elab/Clause.hs+34−22

@@ -455,8 +455,10 @@ checkPossible info fc tcgen fname lhs_in

455 -- if the LHS type checks, it is possible

456 case elaborate ctxt (sMN 0 "patLHS") infP initEState

457 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

458− OK ((lhs', _, _), _) ->

458+ OK (ElabResult lhs' _ _ ctxt' newDecls, _) ->

459+ do setContext ctxt'

460+ processTacticDecls newDecls

459− do let lhs_tm = orderPats (getInferTerm lhs')

461+ let lhs_tm = orderPats (getInferTerm lhs')

460 case recheck ctxt [] (forget lhs_tm) lhs_tm of

462 case recheck ctxt [] (forget lhs_tm) lhs_tm of

461 OK _ -> return True

463 OK _ -> return True

462 err -> return False

464 err -> return False

@@ -579,14 +581,15 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

579 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

581 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

580 "\n" ++ show (fn_ty, fn_is))

582 "\n" ++ show (fn_ty, fn_is))

581

583

582− (((lhs', dlhs, []), probs, inj), _) <-

584+ ((ElabResult lhs' dlhs [] ctxt' newDecls, probs, inj), _) <-

583− tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

585+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

584− (do res <- errAt "left hand side of " fname

586+ (do res <- errAt "left hand side of " fname

585− (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

587+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

586− probs <- get_probs

588+ probs <- get_probs

587− inj <- get_inj

589+ inj <- get_inj

588− return (res, probs, inj))

590+ return (res, probs, inj))

589−

591+ setContext ctxt'

592+ processTacticDecls newDecls

590 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

593 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

591

594

592 let lhs_tm = orderPats (getInferTerm lhs')

595 let lhs_tm = orderPats (getInferTerm lhs')

@@ -653,13 +656,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

653 logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

656 logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

654 ctxt <- getContext -- new context with where block added

657 ctxt <- getContext -- new context with where block added

655 logLvl 5 "STARTING CHECK"

658 logLvl 5 "STARTING CHECK"

656− ((rhs', defer, is, probs), _) <-

659+ ((rhs', defer, is, probs, ctxt', newDecls), _) <-

657 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty initEState

660 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty initEState

658 (do pbinds ist lhs_tm

661 (do pbinds ist lhs_tm

659 mapM_ setinj (nub (params ++ inj))

662 mapM_ setinj (nub (params ++ inj))

660 setNextName

663 setNextName

664+ (ElabResult _ _ is ctxt' newDecls) <-

661− (_, _, is) <- errAt "right hand side of " fname

665+ errAt "right hand side of " fname

662− (erun fc (build i winfo ERHS opts fname rhs))

666+ (erun fc (build i winfo ERHS opts fname rhs))

663 errAt "right hand side of " fname

667 errAt "right hand side of " fname

664 (erun fc $ psolve lhs_tm)

668 (erun fc $ psolve lhs_tm)

665 hs <- get_holes

669 hs <- get_holes

@@ -668,8 +672,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

668 tt <- get_term

672 tt <- get_term

669 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

673 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

670 probs <- get_probs

674 probs <- get_probs

671− return (tm, ds, is, probs))

675+ return (tm, ds, is, probs, ctxt', newDecls))

672−

676+ setContext ctxt'

677+ processTacticDecls newDecls

673 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

678 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

674

679

675 logLvl 5 "DONE CHECK"

680 logLvl 5 "DONE CHECK"

@@ -812,10 +817,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

812 let params = getParamsInType i [] fn_is fn_ty

817 let params = getParamsInType i [] fn_is fn_ty

813 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

818 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

814 logLvl 2 ("LHS: " ++ show lhs)

819 logLvl 2 ("LHS: " ++ show lhs)

815− ((lhs', dlhs, []), _) <-

820+ (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

816 tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

821 tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

817 (errAt "left hand side of with in " fname

822 (errAt "left hand side of with in " fname

818 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

823 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

824+ setContext ctxt'

825+ processTacticDecls newDecls

819 let lhs_tm = orderPats (getInferTerm lhs')

826 let lhs_tm = orderPats (getInferTerm lhs')

820 let lhs_ty = getInferType lhs'

827 let lhs_ty = getInferType lhs'

821 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

828 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

@@ -827,17 +834,19 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

827 let wval = addImplBound i (map fst bargs) wval_in

834 let wval = addImplBound i (map fst bargs) wval_in

828 logLvl 5 ("Checking " ++ showTmImpls wval)

835 logLvl 5 ("Checking " ++ showTmImpls wval)

829 -- Elaborate wval in this context

836 -- Elaborate wval in this context

830− ((wval', defer, is), _) <-

837+ ((wval', defer, is, ctxt', newDecls), _) <-

831 tclift $ elaborate ctxt (sMN 0 "withRHS")

838 tclift $ elaborate ctxt (sMN 0 "withRHS")

832 (bindTyArgs PVTy bargs infP) initEState

839 (bindTyArgs PVTy bargs infP) initEState

833 (do pbinds i lhs_tm

840 (do pbinds i lhs_tm

834 setNextName

841 setNextName

835 -- TODO: may want where here - see winfo abpve

842 -- TODO: may want where here - see winfo abpve

836− (_', d, is) <- errAt "with value in " fname

843+ (ElabResult _ d is ctxt' newDecls) <- errAt "with value in " fname

837 (erun fc (build i info ERHS opts fname (infTerm wval)))

844 (erun fc (build i info ERHS opts fname (infTerm wval)))

838 erun fc $ psolve lhs_tm

845 erun fc $ psolve lhs_tm

839 tt <- get_term

846 tt <- get_term

840− return (tt, d, is))

847+ return (tt, d, is, ctxt', newDecls))

848+ setContext ctxt'

849+ processTacticDecls newDecls

841 def' <- checkDef fc defer

850 def' <- checkDef fc defer

842 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

851 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

843 addDeferred def''

852 addDeferred def''

@@ -923,14 +932,17 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

923 logLvl 5 ("New RHS " ++ showTmImpls rhs)

932 logLvl 5 ("New RHS " ++ showTmImpls rhs)

924 ctxt <- getContext -- New context with block added

933 ctxt <- getContext -- New context with block added

925 i <- getIState

934 i <- getIState

926− ((rhs', defer, is), _) <-

935+ ((rhs', defer, is, ctxt', newDecls), _) <-

927 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty initEState

936 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty initEState

928 (do pbinds i lhs_tm

937 (do pbinds i lhs_tm

929 setNextName

938 setNextName

930− (_, d, is) <- erun fc (build i info ERHS opts fname rhs)

939+ (ElabResult _ d is ctxt' newDecls) <- erun fc (build i info ERHS opts fname rhs)

931 psolve lhs_tm

940 psolve lhs_tm

932 tt <- get_term

941 tt <- get_term

933− return (tt, d, is))

942+ return (tt, d, is, ctxt', newDecls))

943+ setContext ctxt'

944+ processTacticDecls newDecls

945+

934 def' <- checkDef fc defer

946 def' <- checkDef fc defer

935 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

947 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

936 addDeferred def''

948 addDeferred def''

src/Idris/Elab/Instance.hs+23−11

@@ -75,7 +75,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

75 -- if the instance type matches any of the instances we have already,

76 -- and it's not a named instance, then it's overlapping, so report an error

77 case expn of

78− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))

78+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (class_determiners ci) (delab i nty))

79 (class_instances ci)

80 addInstance intInst n iname

81 Just _ -> addInstance intInst n iname

@@ -169,31 +169,43 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

169 ty' <- implicit info syn iname ty'

170 let ty = addImpl i ty'

171 ctxt <- getContext

172− ((tyT, _, _), _) <-

172+ (ElabResult tyT _ _ ctxt' newDecls, _) <-

173− tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

173+ tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

174− (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

174+ (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

175+ setContext ctxt'

176+ processTacticDecls newDecls

175 ctxt <- getContext

177 ctxt <- getContext

176 (cty, _) <- recheckC fc [] tyT

178 (cty, _) <- recheckC fc [] tyT

177 let nty = normalise ctxt [] cty

179 let nty = normalise ctxt [] cty

178− return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)

180+ return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)

179

181

180− findOverlapping i t n

182+ findOverlapping i dets t n

181 | take 2 (show n) == "@@" = Nothing

183 | take 2 (show n) == "@@" = Nothing

182 | otherwise

184 | otherwise

183 = case lookupTy n (tt_ctxt i) of

185 = case lookupTy n (tt_ctxt i) of

184 [t'] -> let tret = getRetType t

186 [t'] -> let tret = getRetType t

185 tret' = getRetType (delab i t') in

187 tret' = getRetType (delab i t') in

186− case matchClause i tret' tret of

188+ case matchArgs i dets tret' tret of

187− Right ms -> Just tret'

189+ Right _ -> Just tret'

188− Left _ -> case matchClause i tret tret' of

190+ Left _ -> case matchArgs i dets tret tret' of

189− Right ms -> Just tret'

191+ Right _ -> Just tret'

190− Left _ -> Nothing

192+ Left _ -> Nothing

191 _ -> Nothing

193 _ -> Nothing

192 overlapping t' = tclift $ tfail (At fc (Msg $

194 overlapping t' = tclift $ tfail (At fc (Msg $

193 "Overlapping instance: " ++ show t' ++ " already defined"))

195 "Overlapping instance: " ++ show t' ++ " already defined"))

194 getRetType (PPi _ _ _ sc) = getRetType sc

196 getRetType (PPi _ _ _ sc) = getRetType sc

195 getRetType t = t

197 getRetType t = t

196

198

199+ matchArgs i dets x y =

200+ let x' = keepDets dets x

201+ y' = keepDets dets y in

202+ matchClause i x' y'

203+

204+ keepDets dets (PApp fc f args)

205+ = PApp fc f $ let a' = zip [0..] args in

206+ map snd (filter (\(i, _) -> i `elem` dets) a')

207+ keepDets dets t = t

208+

197 mkMethApp (n, _, _, ty)

209 mkMethApp (n, _, _, ty)

198 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

210 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

199 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

211 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

src/Idris/Elab/Transform.hs+10−4

@@ -53,10 +53,12 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56− ((lhs', dlhs, []), _) <-

56+ (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

57 tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState

58 (erun fc (buildTC i info ELHS [] (sUN "transform")

59 (infTerm lhs)))

60+ setContext ctxt'

61+ processTacticDecls newDecls

60 let lhs_tm = orderPats (getInferTerm lhs')

62 let lhs_tm = orderPats (getInferTerm lhs')

61 let lhs_ty = getInferType lhs'

63 let lhs_ty = getInferType lhs'

62 let newargs = pvars i lhs_tm

64 let newargs = pvars i lhs_tm

@@ -66,14 +68,18 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

66 logLvl 3 ("Transform LHS " ++ show clhs_tm)

68 logLvl 3 ("Transform LHS " ++ show clhs_tm)

67

69

68 let rhs = addImplBound i (map fst newargs) rhs_in

70 let rhs = addImplBound i (map fst newargs) rhs_in

69− ((rhs', defer), _) <-

71+ ((rhs', defer, ctxt', newDecls), _) <-

70 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

72 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

71 (do pbinds i lhs_tm

73 (do pbinds i lhs_tm

72 setNextName

74 setNextName

73− erun fc (build i info ERHS [] (sUN "transform") rhs)

75+ (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

74 erun fc $ psolve lhs_tm

76 erun fc $ psolve lhs_tm

75 tt <- get_term

77 tt <- get_term

76− return (runState (collectDeferred Nothing tt) []))

78+ let (rhs', defer) = runState (collectDeferred Nothing tt) []

79+ return (rhs', defer, ctxt', newDecls))

80+ setContext ctxt'

81+ processTacticDecls newDecls

82+

77 (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

83 (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

78 let crhs_tm = renamepats pnames crhs_tm_in

84 let crhs_tm = renamepats pnames crhs_tm_in

79 logLvl 3 ("Transform RHS " ++ show crhs_tm)

85 logLvl 3 ("Transform RHS " ++ show crhs_tm)

src/Idris/Elab/Type.hs+10−6

@@ -65,9 +65,11 @@ buildType info syn fc opts n ty' = do

65 logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66 logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

67

68− ((tyT', defer, is), log) <-

68+ (ElabResult tyT' defer is ctxt' newDecls, log) <-

69− tclift $ elaborate ctxt n (TType (UVal 0)) initEState

69+ tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

70+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

71+ setContext ctxt'

72+ processTacticDecls newDecls

71

73

72 let tyT = patToImp tyT'

74 let tyT = patToImp tyT'

73

75

@@ -114,12 +116,14 @@ buildType info syn fc opts n ty' = do

114 param_pos i ns t = []

116 param_pos i ns t = []

115

117

116-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

118-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

119+elabType :: ElabInfo -> SyntaxInfo

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

120+ -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

118− FC -> FnOpts -> Name -> PTerm -> Idris Type

121+ -> FC -> FnOpts -> Name -> PTerm -> Idris Type

119elabType = elabType' False

122elabType = elabType' False

120

123

121elabType' :: Bool -> -- normalise it

124elabType' :: Bool -> -- normalise it

125+ ElabInfo -> SyntaxInfo ->

122− ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

126+ Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

123 FC -> FnOpts -> Name -> PTerm -> Idris Type

127 FC -> FnOpts -> Name -> PTerm -> Idris Type

124elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

128elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125 n = liftname info n_in in -}

129 n = liftname info n_in in -}

src/Idris/Elab/Utils.hs+10−8

@@ -22,7 +22,7 @@ import Debug.Trace

22

23import qualified Data.Map as Map

24

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

26

27recheckC_borrowing uniq_check bs fc env t

28 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

@@ -34,9 +34,13 @@ recheckC_borrowing uniq_check bs fc env t

34 addConstraints fc cs

35 return (tm, ty)

36

37−

37+checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]

38+ -> Idris [(Name, (Int, Maybe Name, Type))]

38checkDef fc ns = checkAddDef False True fc ns

39checkDef fc ns = checkAddDef False True fc ns

39

40

41+checkAddDef :: Bool -> Bool -> FC

42+ -> [(Name, (Int, Maybe Name, Type))]

43+ -> Idris [(Name, (Int, Maybe Name, Type))]

40checkAddDef add toplvl fc [] = return []

44checkAddDef add toplvl fc [] = return []

41checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

45checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

42 = do ctxt <- getContext

46 = do ctxt <- getContext

@@ -46,7 +50,7 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

46 ns' <- checkAddDef add toplvl fc ns

50 ns' <- checkAddDef add toplvl fc ns

47 return ((n, (i, top, t')) : ns')

51 return ((n, (i, top, t')) : ns')

48

52

49−-- Get the list of (index, name) of inaccessible arguments from an elaborated

53+-- | Get the list of (index, name) of inaccessible arguments from an elaborated

50-- type

54-- type

51inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

55inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

52inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

56inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

@@ -54,7 +58,7 @@ inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

54 | otherwise = inaccessibleImps (i + 1) sc ins

58 | otherwise = inaccessibleImps (i + 1) sc ins

55inaccessibleImps _ _ _ = []

59inaccessibleImps _ _ _ = []

56

60

57−-- Get the list of (index, name) of inaccessible arguments from the type.

61+-- | Get the list of (index, name) of inaccessible arguments from the type.

58inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

62inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

59inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

63inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

60 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

64 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

@@ -74,10 +78,9 @@ elabCaseBlock info opts d@(PClauses f o n ps)

74 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

78 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

75 rec_elabDecl info EAll info (PClauses f opts' n ps )

79 rec_elabDecl info EAll info (PClauses f opts' n ps )

76

80

77−-- Check that the result of type checking matches what the programmer wrote

81+-- | Check that the result of type checking matches what the programmer wrote

78-- (i.e. - if we inferred any arguments that the user provided, make sure

82-- (i.e. - if we inferred any arguments that the user provided, make sure

79-- they are the same!)

83-- they are the same!)

80−

81checkInferred :: FC -> PTerm -> PTerm -> Idris ()

84checkInferred :: FC -> PTerm -> PTerm -> Idris ()

82checkInferred fc inf user =

85checkInferred fc inf user =

83 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

86 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

@@ -92,9 +95,8 @@ checkInferred fc inf user =

92 logLvl 10 $ "Checked match"

95 logLvl 10 $ "Checked match"

93-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

96-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

94

97

95−-- Return whether inferred term is different from given term

98+-- | Return whether inferred term is different from given term

96-- (as above, but return a Bool)

99-- (as above, but return a Bool)

97−

98inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

100inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

99inferredDiff fc inf user =

101inferredDiff fc inf user =

100 do i <- getIState

102 do i <- getIState

src/Idris/Elab/Value.hs+8−3

@@ -63,9 +63,14 @@ elabValBind info aspat norm tm_in

63 -- * elaboration as a Type

64 -- * elaboration as a function a -> b

65

66− ((tm', defer, is), _) <-

66+ (ElabResult tm' defer is ctxt' newDecls, _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP initEState

67+ tclift (elaborate ctxt (sMN 0 "val") infP initEState

68− (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

68+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

69+

70+ -- Extend the context with new definitions created

71+ setContext ctxt'

72+ processTacticDecls newDecls

73+

69 let vtm = orderPats (getInferTerm tm')

74 let vtm = orderPats (getInferTerm tm')

70

75

71 def' <- checkDef (fileFC "(input)") defer

76 def' <- checkDef (fileFC "(input)") defer

src/Idris/ElabDecls.hs+2−2

@@ -229,10 +229,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

229 ninfo = case namespace info of

230 Nothing -> info { namespace = Just [n] }

231 Just ns -> info { namespace = Just (n:ns) }

232−elabDecl' what info (PClass doc s f cs n ps pdocs ds)

232+elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)

233 | what /= EDefns

234 = do iLOG $ "Elaborating class " ++ show n

235− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

235+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds

236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237 = do iLOG $ "Elaborating instance " ++ show n

238 elabInstance info s doc argDocs what f cs n ps t expn ds

src/Idris/ElabTerm.hs+210−81

@@ -18,6 +18,7 @@ import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20import Idris.Elab.Utils

21+import Idris.Reflection

21import qualified Util.Pretty as U

22import qualified Util.Pretty as U

22

23

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

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

@@ -36,6 +37,32 @@ import Debug.Trace

36data ElabMode = ETyDecl | ELHS | ERHS

37data ElabMode = ETyDecl | ELHS | ERHS

37 deriving Eq

38 deriving Eq

38

39

40+data ElabResult =

41+ ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

42+ , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

43+ -- ^ Information about new metavariables

44+ , resultCaseDecls :: [PDecl]

45+ -- ^ Deferred declarations as the meaning of case blocks

46+ , resultContext :: Context

47+ -- ^ The potentially extended context from new definitions

48+ , resultTyDecls :: [(Name, FC, [PArg], Type)]

49+ -- ^ Meta-info about the new type declarations

50+ }

51+

52+processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()

53+processTacticDecls info =

54+ forM_ info $ \(n, fc, impls, ty) ->

55+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

56+ logLvl 3 $ " It has impls " ++ show impls

57+ updateIState $ \i -> i { idris_implicits =

58+ addDef n impls (idris_implicits i) }

59+ addIBC (IBCImp n)

60+ ds <- checkDef fc [(n, (-1, Nothing, ty))]

61+ addIBC (IBCDef n)

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

63+ addDeferred ds'

64+

65+

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

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

40-- elaborated, typechecked term.

67-- elaborated, typechecked term.

41--

68--

@@ -45,7 +72,7 @@ data ElabMode = ETyDecl | ELHS | ERHS

45-- Also find deferred names in the term and their types

72-- Also find deferred names in the term and their types

46

73

47build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

74build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

48− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

75+ ElabD ElabResult

49build ist info emode opts fn tm

76build ist info emode opts fn tm

50 = do elab ist info emode opts fn tm

77 = do elab ist info emode opts fn tm

51 let tmIn = tm

78 let tmIn = tm

@@ -64,7 +91,7 @@ build ist info emode opts fn tm

64 mapM_ (\n -> when (n `elem` hs) $

91 mapM_ (\n -> when (n `elem` hs) $

65 do focus n

92 do focus n

66 g <- goal

93 g <- goal

67− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

68 (movelast n)) ivs

95 (movelast n)) ivs

69 ivs <- get_instances

96 ivs <- get_instances

70 hs <- get_holes

97 hs <- get_holes

@@ -72,7 +99,8 @@ build ist info emode opts fn tm

72 mapM_ (\n -> when (n `elem` hs) $

99 mapM_ (\n -> when (n `elem` hs) $

73 do focus n

100 do focus n

74 g <- goal

101 g <- goal

102+ ptm <- get_term

75− resolveTC True 7 g fn ist) ivs

103+ resolveTC True True 7 g fn ist) ivs

76 tm <- get_term

104 tm <- get_term

77 ctxt <- get_context

105 ctxt <- get_context

78 probs <- get_probs

106 probs <- get_probs

@@ -94,12 +122,13 @@ build ist info emode opts fn tm

94 when tydecl (do update_term orderPats

122 when tydecl (do update_term orderPats

95 mkPat)

123 mkPat)

96-- update_term liftPats)

124-- update_term liftPats)

97− EState is _ <- getAux

125+ EState is _ impls <- getAux

98 tt <- get_term

126 tt <- get_term

99 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

100 log <- getLog

128 log <- getLog

129+ ctxt <- get_context

101− if (log /= "") then trace log $ return (tm, ds, is)

130+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

102− else return (tm, ds, is)

131+ else return (ElabResult tm ds is ctxt impls)

103 where pattern = emode == ELHS

132 where pattern = emode == ELHS

104 tydecl = emode == ETyDecl

133 tydecl = emode == ETyDecl

105

134

@@ -114,7 +143,7 @@ build ist info emode opts fn tm

114-- know about yet on the LHS of a pattern def)

143-- know about yet on the LHS of a pattern def)

115

144

116buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

145buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

117− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

146+ ElabD ElabResult

118buildTC ist info emode opts fn tm

147buildTC ist info emode opts fn tm

119 = do -- set name supply to begin after highest index in tm

148 = do -- set name supply to begin after highest index in tm

120 let ns = allNamesIn tm

149 let ns = allNamesIn tm

@@ -135,12 +164,13 @@ buildTC ist info emode opts fn tm

135 -- unification

164 -- unification

136 when (not (null dots)) $

165 when (not (null dots)) $

137 lift (Error (CantMatch (getInferTerm tm)))

166 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

167+ EState is _ impls <- getAux

139 tt <- get_term

168 tt <- get_term

140 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

169 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

141 log <- getLog

170 log <- getLog

171+ ctxt <- get_context

142− if (log /= "") then trace log $ return (tm, ds, is)

172+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

143− else return (tm, ds, is)

173+ else return (ElabResult tm ds is ctxt impls)

144 where pattern = emode == ELHS

174 where pattern = emode == ELHS

145

175

146-- return whether arguments of the given constructor name can be

176-- return whether arguments of the given constructor name can be

@@ -183,9 +213,9 @@ goal_polymorphic =

183 _ -> return True

213 _ -> return True

184 _ -> return False

214 _ -> return False

185

215

186−-- Returns the set of declarations we need to add to complete the definition

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

187−-- (most likely case blocks to elaborate)

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

188−

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

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

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

190 ElabD ()

220 ElabD ()

191elab ist info emode opts fn tm

221elab ist info emode opts fn tm

@@ -321,7 +351,7 @@ elab ist info emode opts fn tm

321 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

351 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322 _ -> elab' ina (Just fc) (PRef fc unitCon)

352 _ -> elab' ina (Just fc) (PRef fc unitCon)

323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

353 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

324− = do g <- goal; resolveTC False 5 g fn ist

354+ = do g <- goal; resolveTC False False 5 g fn ist

325 elab' ina fc (PResolveTC fc')

355 elab' ina fc (PResolveTC fc')

326 = do c <- getNameFrom (sMN 0 "class")

356 = do c <- getNameFrom (sMN 0 "class")

327 instanceArg c

357 instanceArg c

@@ -540,7 +570,7 @@ elab ist info emode opts fn tm

540 g <- goal

570 g <- goal

541 hs <- get_holes

571 hs <- get_holes

542 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

572 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

543− then try (resolveTC True 7 g fn ist)

573+ then try (resolveTC True False 7 g fn ist)

544 (movelast n)

574 (movelast n)

545 else movelast n)

575 else movelast n)

546 (ivs' \\ ivs)

576 (ivs' \\ ivs)

@@ -700,7 +730,7 @@ elab ist info emode opts fn tm

700 env <- get_env

730 env <- get_env

701 hs <- get_holes

731 hs <- get_holes

702 if all (\n -> not (n `elem` hs)) (freeNames g)

732 if all (\n -> not (n `elem` hs)) (freeNames g)

703− then try (resolveTC False 7 g fn ist)

733+ then try (resolveTC False False 7 g fn ist)

704 (movelast n)

734 (movelast n)

705 else movelast n)

735 else movelast n)

706 (ivs' \\ ivs)

736 (ivs' \\ ivs)

@@ -965,17 +995,14 @@ elab ist info emode opts fn tm

965 elab' ina fc (PUnifyLog t) = do unifyLog True

995 elab' ina fc (PUnifyLog t) = do unifyLog True

966 elab' ina fc t

996 elab' ina fc t

967 unifyLog False

997 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

969 = do -- First extract the unquoted subterms, replacing them with fresh

999 = do -- First extract the unquoted subterms, replacing them with fresh

970 -- names in the quasiquoted term. Claim their reflections to be

1000 -- names in the quasiquoted term. Claim their reflections to be

971 -- an inferred type (to support polytypic quasiquotes).

1001 -- an inferred type (to support polytypic quasiquotes).

1002+ finalTy <- goal

972 (t, unq) <- extractUnquotes 0 t

1003 (t, unq) <- extractUnquotes 0 t

973 let unquoteNames = map fst unq

1004 let unquoteNames = map fst unq

974− mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")

975− claim uqh RType

976− movelast uqh

977− claim uqn (Var uqh)) unquoteNames

1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames

978−

979

1006

980 -- Save the old state - we need a fresh proof state to avoid

1007 -- Save the old state - we need a fresh proof state to avoid

981 -- capturing lexically available variables in the quoted term.

1008 -- capturing lexically available variables in the quoted term.

@@ -1010,7 +1037,7 @@ elab ist info emode opts fn tm

1010 letbind nTm (Var qTy) (Var qTm)

1037 letbind nTm (Var qTy) (Var qTm)

1011

1038

1012 -- Fill out the goal type, if relevant

1039 -- Fill out the goal type, if relevant

1013− case goal of

1040+ case goalt of

1014 Nothing -> return ()

1041 Nothing -> return ()

1015 Just gTy -> do focus qTy

1042 Just gTy -> do focus qTy

1016 elabE (ina { e_qq = True }) fc gTy

1043 elabE (ina { e_qq = True }) fc gTy

@@ -1025,18 +1052,20 @@ elab ist info emode opts fn tm

1025 env <- get_env

1052 env <- get_env

1026 loadState

1053 loadState

1027 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1054 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1028−

1055+ isRaw = case unApply (normaliseAll ctxt env finalTy) of

1056+ (P _ n _, []) | n == reflm "Raw" -> True

1057+ _ -> False

1029 case quoted of

1058 case quoted of

1030 Just q -> do ctxt <- get_context

1059 Just q -> do ctxt <- get_context

1031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1032 if pattern

1061 if pattern

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1033− then do try' (reflectTTQuotePattern unquoteNames q')

1064+ else reflectTTQuotePattern unquoteNames q'

1034− (reflectRawQuotePattern unquoteNames (forget q'))

1065+ else do if isRaw

1035− True

1036− else do try' (fill $ reflectTTQuote unquoteNames q')

1037− -- we forget q' instead of using q to ensure rechecking

1066+ then -- we forget q' instead of using q to ensure rechecking

1038− (fill $ reflectRawQuote unquoteNames (forget q'))

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1039− True -- ignore errors like proof search does

1068+ else fill $ reflectTTQuote unquoteNames q'

1040 solve

1069 solve

1041

1070

1042 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

1071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

@@ -1077,8 +1106,8 @@ elab ist info emode opts fn tm

1077 focus n

1106 focus n

1078 elab' ina (Just fc') tm

1107 elab' ina (Just fc') tm

1079 env <- get_env

1108 env <- get_env

1080− ctxt <- get_context

1081− runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)

1109+ runTactical (maybe fc' id fc) env (P Bound n' Erased)

1110+ EState _ _ todo <- getAux

1082 solve

1111 solve

1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1084

1113

@@ -1346,7 +1375,7 @@ findInstances :: IState -> Term -> [Name]

1346findInstances ist t

1375findInstances ist t

1347 | (P _ n _, _) <- unApply t

1376 | (P _ n _, _) <- unApply t

1348 = case lookupCtxt n (idris_classes ist) of

1377 = case lookupCtxt n (idris_classes ist) of

1349− [CI _ _ _ _ _ ins] -> ins

1378+ [CI _ _ _ _ _ ins _] -> ins

1350 _ -> []

1379 _ -> []

1351 | otherwise = []

1380 | otherwise = []

1352

1381

@@ -1376,14 +1405,26 @@ proofSearch' ist rec ambigok depth prv top n hints

1376-- Resolve type classes. This will only pick up 'normal' instances, never

1405-- Resolve type classes. This will only pick up 'normal' instances, never

1377-- named instances (hence using 'tcname' to check it's a generated instance

1406-- named instances (hence using 'tcname' to check it's a generated instance

1378-- name).

1407-- name).

1408+resolveTC :: Bool -- using default Int

1409+ -> Bool -- allow metavariables in the goal

1410+ -> Int -- depth

1411+ -> Term -- top level goal

1412+ -> Name -- top level function name

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1413+ -> IState -> ElabD ()

1380−resolveTC = resTC' []

1414+resolveTC def mvok depth top fn ist

1381−

1415+ = do hs <- get_holes

1416+ resTC' [] def hs depth top fn ist

1417+

1382−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1418+resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1383−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1419+resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1384−resTC' tcs defaultOn depth topg fn ist

1420+resTC' tcs defaultOn topholes depth topg fn ist

1385− = do compute

1421+ = do compute

1386− g <- goal

1422+ g <- goal

1423+ let argsok = tcArgsOK g topholes

1424+-- trace (show (g,hs,argsok,topholes)) $

1425+ if not argsok -- && not mvok)

1426+ then lift $ tfail $ CantResolve True topg

1427+ else do

1387 ptm <- get_term

1428 ptm <- get_term

1388 ulog <- getUnifyLog

1429 ulog <- getUnifyLog

1389 hs <- get_holes

1430 hs <- get_holes

@@ -1400,6 +1441,31 @@ resTC' tcs defaultOn depth topg fn ist

1400 let depth' = if scopeOnly then 2 else depth

1441 let depth' = if scopeOnly then 2 else depth

1401 blunderbuss t depth' stk (stk ++ insts)) True

1442 blunderbuss t depth' stk (stk ++ insts)) True

1402 where

1443 where

1444+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1445+ = True

1446+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1447+ = let (f, as) = unApply ty in

1448+ case f of

1449+ P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1450+ Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1451+ Nothing -> not $ any (isMeta hs) as

1452+ _ -> not $ any (isMeta hs) as

1453+

1454+ tcDetArgsOK i ds hs (x : xs)

1455+ | i `elem` ds = not (isMeta hs x) && tcDetArgsOK (i + 1) ds hs xs

1456+ | otherwise = tcDetArgsOK (i + 1) ds hs xs

1457+ tcDetArgsOK _ _ _ [] = True

1458+

1459+ isMeta :: [Name] -> Term -> Bool

1460+ isMeta ns (P _ n _) = n `elem` ns

1461+ isMeta _ _ = False

1462+

1463+ notHole hs (P _ n _, c)

1464+ | (P _ cn _, _) <- unApply c,

1465+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1466+ | Constant _ <- c = not (n `elem` hs)

1467+ notHole _ _ = True

1468+

1403 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1469 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1404 | otherwise = (fail "Can't resolve", show n)

1470 | otherwise = (fail "Can't resolve", show n)

1405

1471

@@ -1427,10 +1493,13 @@ resTC' tcs defaultOn depth topg fn ist

1427

1493

1428 blunderbuss t d stk [] = do -- c <- get_env

1494 blunderbuss t d stk [] = do -- c <- get_env

1429 -- ps <- get_probs

1495 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1496+ lift $ tfail $ CantResolve False topg

1431 blunderbuss t d stk (n:ns)

1497 blunderbuss t d stk (n:ns)

1432 | n /= fn && (n `elem` stk || tcname n)

1498 | n /= fn && (n `elem` stk || tcname n)

1499+ = tryCatch (resolve n d)

1500+ (\e -> case e of

1501+ CantResolve True _ -> lift $ tfail e

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1502+ _ -> blunderbuss t d stk ns)

1434 | otherwise = blunderbuss t d stk ns

1503 | otherwise = blunderbuss t d stk ns

1435

1504

1436 resolve n depth

1505 resolve n depth

@@ -1459,7 +1528,7 @@ resTC' tcs defaultOn depth topg fn ist

1459 let got = fst (unApply t)

1528 let got = fst (unApply t)

1460 let depth' = if tc' `elem` tcs

1529 let depth' = if tc' `elem` tcs

1461 then depth - 1 else depth

1530 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1531+ resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

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

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

1464 -- if there's any arguments left, we've failed to resolve

1533 -- if there's any arguments left, we've failed to resolve

1465 hs <- get_holes

1534 hs <- get_holes

@@ -1505,11 +1574,17 @@ case_ ind autoSolve ist fn tm = do

1505 else casetac (forget val)

1574 else casetac (forget val)

1506 when autoSolve solveAll

1575 when autoSolve solveAll

1507

1576

1577+tacN :: String -> Name

1578+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1579+

1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1580+runTactical :: FC -> Env -> Term -> ElabD ()

1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1581+runTactical fc env tm = do tm' <- eval tm

1582+ runTacTm tm'

1583+ return ()

1510 where

1584 where

1585+ eval tm = do ctxt <- get_context

1511− eval = normaliseAll ctxt env . finalise

1586+ return $ normaliseAll ctxt env (finalise tm)

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

1587+

1513 returnUnit = fmap fst $ get_type_val (Var unitCon)

1588 returnUnit = fmap fst $ get_type_val (Var unitCon)

1514

1589

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

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

@@ -1547,26 +1622,31 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1547 = do env <- get_env

1622 = do env <- get_env

1548 fmap fst . get_type_val $ reflectEnv env

1623 fmap fst . get_type_val $ reflectEnv env

1549 | n == tacN "prim__Fail", [_a, errs] <- args

1624 | n == tacN "prim__Fail", [_a, errs] <- args

1625+ = do errs' <- eval errs

1550− = do parts <- reifyReportParts (eval errs)

1626+ parts <- reifyReportParts errs'

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

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

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

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

1553 = return tm

1629 = return tm

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

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

1555− = do let first' = eval first

1631+ = do first' <- eval first

1556 res <- runTacTm first'

1632 res <- runTacTm first'

1557− let next = eval (App andThen res)

1633+ next <- eval (App andThen res)

1558 runTacTm next

1634 runTacTm next

1559 | n == tacN "prim__Try", [_a, first, alt] <- args

1635 | n == tacN "prim__Try", [_a, first, alt] <- args

1560− = do let first' = eval first

1636+ = do first' <- eval first

1561− let alt' = eval alt

1637+ alt' <- eval alt

1562 try' (runTacTm first') (runTacTm alt') True

1638 try' (runTacTm first') (runTacTm alt') True

1563 | n == tacN "prim__Fill", [raw] <- args

1639 | n == tacN "prim__Fill", [raw] <- args

1564 = do raw' <- reifyRaw raw

1640 = do raw' <- reifyRaw raw

1565 apply raw' []

1641 apply raw' []

1566 returnUnit

1642 returnUnit

1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

1643+ | n == tacN "prim__Gensym", [hint] <- args

1644+ = do hintStr <- eval hint

1645+ case hintStr of

1646+ Constant (Str h) -> do

1568− = do n <- getNameFrom (sMN 0 hint)

1647+ n <- getNameFrom (sMN 0 h)

1569− fmap fst $ get_type_val (reflectName n)

1648+ fmap fst $ get_type_val (reflectName n)

1649+ _ -> fail "no hint"

1570 | n == tacN "prim__Claim", [n, ty] <- args

1650 | n == tacN "prim__Claim", [n, ty] <- args

1571 = do n' <- reifyTTName n

1651 = do n' <- reifyTTName n

1572 ty' <- reifyRaw ty

1652 ty' <- reifyRaw ty

@@ -1596,6 +1676,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1596 Just name -> fmap Just $ reifyTTName name

1676 Just name -> fmap Just $ reifyTTName name

1597 intro n

1677 intro n

1598 returnUnit

1678 returnUnit

1679+ | n == tacN "prim__DeclareType", [decl] <- args

1680+ = do (RDeclare n args res) <- reifyTyDecl decl

1681+ ctxt <- get_context

1682+ let mkPi arg res = RBind (argName arg)

1683+ (Pi Nothing (argTy arg) (RUType AllTypes))

1684+ res

1685+ rty = foldr mkPi res args

1686+ (checked, ty') <- lift $ check ctxt [] rty

1687+ case normaliseAll ctxt [] (finalise ty') of

1688+ TType _ -> lift . tfail . InternalMsg $

1689+ show checked ++ " is not a type: it's " ++ show ty'

1690+ _ -> return ()

1691+ case lookupDefExact n ctxt of

1692+ Just _ -> lift . tfail . InternalMsg $

1693+ show n ++ " is already defined."

1694+ Nothing -> return ()

1695+ let decl = TyDecl Ref checked

1696+ ctxt' = addCtxtDef n decl ctxt

1697+ set_context ctxt'

1698+ updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :

1699+ new_tyDecls e }

1700+ aux <- getAux

1701+ returnUnit

1599 | n == tacN "prim__Debug", [ty, msg] <- args

1702 | n == tacN "prim__Debug", [ty, msg] <- args

1600 = do let msg' = fromTTMaybe msg

1703 = do let msg' = fromTTMaybe msg

1601 case msg' of

1704 case msg' of

@@ -1850,6 +1953,7 @@ runTac autoSolve ist perhapsFC fn tac

1850 Just fc ->

1953 Just fc ->

1851 do fill $ reflectFC fc

1954 do fill $ reflectFC fc

1852 solve

1955 solve

1956+ runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

1853 runT x = fail $ "Not implemented " ++ show x

1957 runT x = fail $ "Not implemented " ++ show x

1854

1958

1855 runReflected t = do t' <- reify ist t

1959 runReflected t = do t' <- reify ist t

@@ -2361,7 +2465,7 @@ reflectTTQuote unq (P nt n t)

2361reflectTTQuote unq (V n)

2465reflectTTQuote unq (V n)

2362 = reflCall "V" [RConstant (I n)]

2466 = reflCall "V" [RConstant (I n)]

2363reflectTTQuote unq (Bind n b x)

2467reflectTTQuote unq (Bind n b x)

2364− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]

2468+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2365reflectTTQuote unq (App f x)

2469reflectTTQuote unq (App f x)

2366 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2367reflectTTQuote unq (Constant c)

2471reflectTTQuote unq (Constant c)

@@ -2378,7 +2482,7 @@ reflectRawQuote unq (Var n)

2378 | n `elem` unq = Var n

2482 | n `elem` unq = Var n

2379 | otherwise = reflCall "Var" [reflectName n]

2483 | otherwise = reflCall "Var" [reflectName n]

2380reflectRawQuote unq (RBind n b r) =

2484reflectRawQuote unq (RBind n b r) =

2381− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]

2485+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2382reflectRawQuote unq (RApp f x) =

2486reflectRawQuote unq (RApp f x) =

2383 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2384reflectRawQuote unq RType = Var (reflm "RType")

2488reflectRawQuote unq RType = Var (reflm "RType")

@@ -2436,27 +2540,27 @@ reflectNameQuotePattern _ -- for all other names, match any

2436 solve

2540 solve

2437

2541

2438reflectBinder :: Binder Term -> Raw

2542reflectBinder :: Binder Term -> Raw

2439−reflectBinder = reflectBinderQuote reflectTTQuote []

2543+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2440−

2544+

2441−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2545+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2442−reflectBinderQuote q unq (Lam t)

2546+reflectBinderQuote q ty unq (Lam t)

2443− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2547+ = reflCall "Lam" [Var ty, q unq t]

2444−reflectBinderQuote q unq (Pi _ t k)

2548+reflectBinderQuote q ty unq (Pi _ t k)

2445− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2549+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2446−reflectBinderQuote q unq (Let x y)

2550+reflectBinderQuote q ty unq (Let x y)

2447− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2551+ = reflCall "Let" [Var ty, q unq x, q unq y]

2448−reflectBinderQuote q unq (NLet x y)

2552+reflectBinderQuote q ty unq (NLet x y)

2449− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2450−reflectBinderQuote q unq (Hole t)

2554+reflectBinderQuote q ty unq (Hole t)

2451− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2555+ = reflCall "Hole" [Var ty, q unq t]

2452−reflectBinderQuote q unq (GHole _ t)

2556+reflectBinderQuote q ty unq (GHole _ t)

2453− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2557+ = reflCall "GHole" [Var ty, q unq t]

2454−reflectBinderQuote q unq (Guess x y)

2558+reflectBinderQuote q ty unq (Guess x y)

2455− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2456−reflectBinderQuote q unq (PVar t)

2560+reflectBinderQuote q ty unq (PVar t)

2457− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2561+ = reflCall "PVar" [Var ty, q unq t]

2458−reflectBinderQuote q unq (PVTy t)

2562+reflectBinderQuote q ty unq (PVTy t)

2459− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2563+ = reflCall "PVTy" [Var ty, q unq t]

2460

2564

2461mkList :: Raw -> [Raw] -> Raw

2565mkList :: Raw -> [Raw] -> Raw

2462mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2603,11 +2707,14 @@ reflectErr (NotInjective t1 t2 t3) =

2603 , reflect t2

2707 , reflect t2

2604 , reflect t3

2708 , reflect t3

2605 ]

2709 ]

2606−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2710+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2607reflectErr (CantResolveAlts ss) =

2711reflectErr (CantResolveAlts ss) =

2608 raw_apply (Var $ reflErrName "CantResolveAlts")

2712 raw_apply (Var $ reflErrName "CantResolveAlts")

2609 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2713 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2610reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2714reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2715+reflectErr (NoEliminator str t)

2716+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2717+ reflect t]

2611reflectErr UniverseError = Var $ reflErrName "UniverseError"

2718reflectErr UniverseError = Var $ reflErrName "UniverseError"

2612reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2719reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2613reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2720reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2748,6 +2855,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

2748 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2855 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2749reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2856reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2750

2857

2858+reifyTyDecl :: Term -> ElabD RTyDecl

2859+reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2860+ | n == tacN "Declare" =

2861+ do tyN' <- reifyTTName tyN

2862+ args' <- case unList args of

2863+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2864+ Just xs -> mapM reifyRArg xs

2865+ ret' <- reifyRaw ret

2866+ return $ RDeclare tyN' args' ret'

2867+ where reifyRArg :: Term -> ElabD RArg

2868+ reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2869+ | n == tacN "Explicit" = liftM2 RExplicit

2870+ (reifyTTName argN)

2871+ (reifyRaw argTy)

2872+ | n == tacN "Implicit" = liftM2 RImplicit

2873+ (reifyTTName argN)

2874+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2875+ (reifyTTName argN)

2876+ (reifyRaw argTy)

2877+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2878+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2879+

2751envTupleType :: Raw

2880envTupleType :: Raw

2752envTupleType

2881envTupleType

2753 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2882 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/IBC.hs+10−6

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

@@ -365,7 +365,7 @@ pClasses cs = mapM_ (\ (n, c) ->

365 -- Don't lose instances from previous IBCs, which

366 -- could have loaded in any order

367 let is = case lookupCtxtExact n (idris_classes i) of

368− Just (CI _ _ _ _ _ ins) -> ins

368+ Just (CI _ _ _ _ _ ins _) -> ins

369 _ -> []

370 let c' = c { class_instances =

371 class_instances c ++ is }

@@ -1238,7 +1238,7 @@ instance (Binary t) => Binary (PDecl' t) where

1238 put x7

1239 put x8

1240 put x9

1241− PClass x1 x2 x3 x4 x5 x6 x7 x8

1241+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

1242 -> do putWord8 7

1243 put x1

1244 put x2

@@ -1248,6 +1248,7 @@ instance (Binary t) => Binary (PDecl' t) where

1248 put x6

1249 put x7

1250 put x8

1251+ put x9

1251 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252 do putWord8 8

1253 do putWord8 8

1253 put x1

1254 put x1

@@ -1346,7 +1347,8 @@ instance (Binary t) => Binary (PDecl' t) where

1346 x6 <- get

1347 x6 <- get

1347 x7 <- get

1348 x7 <- get

1348 x8 <- get

1349 x8 <- get

1350+ x9 <- get

1349− return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1351+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

1350 8 -> do x1 <- get

1352 8 -> do x1 <- get

1351 x2 <- get

1353 x2 <- get

1352 x3 <- get

1354 x3 <- get

@@ -2071,19 +2073,21 @@ instance (Binary t) => Binary (PArg' t) where

2071

2073

2072

2074

2073instance Binary ClassInfo where

2075instance Binary ClassInfo where

2074− put (CI x1 x2 x3 x4 x5 _)

2076+ put (CI x1 x2 x3 x4 x5 _ x6)

2075 = do put x1

2077 = do put x1

2076 put x2

2078 put x2

2077 put x3

2079 put x3

2078 put x4

2080 put x4

2079 put x5

2081 put x5

2082+ put x6

2080 get

2083 get

2081 = do x1 <- get

2084 = do x1 <- get

2082 x2 <- get

2085 x2 <- get

2083 x3 <- get

2086 x3 <- get

2084 x4 <- get

2087 x4 <- get

2085 x5 <- get

2088 x5 <- get

2089+ x6 <- get

2086− return (CI x1 x2 x3 x4 x5 [])

2090+ return (CI x1 x2 x3 x4 x5 [] x6)

2087

2091

2088instance Binary OptInfo where

2092instance Binary OptInfo where

2089 put (Optimise x1 x2)

2093 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

@@ -585,8 +585,8 @@ collect (c@(PClauses _ o _ _) : ds)

585collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

586collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588−collect (PClass doc f s cs n ps pdocs ds : ds')

588+collect (PClass doc f s cs n ps pdocs fds ds : ds')

589− = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

589+ = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

590collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592collect (d : ds) = d : collect ds

src/Idris/Parser.hs+5−1

@@ -612,11 +612,15 @@ class_ syn = do (doc, argDocs, acc)

612 n_in <- fnName

613 let n = expandNS syn n_in

614 cs <- many carg

615+ fds <- option (map fst cs) fundeps

615 ds <- option [] (classBlock syn)

616 ds <- option [] (classBlock syn)

616 accData acc n (concatMap declared ds)

617 accData acc n (concatMap declared ds)

617− return [PClass doc syn fc cons n cs argDocs ds]

618+ return [PClass doc syn fc cons n cs argDocs fds ds]

618 <?> "type-class declaration"

619 <?> "type-class declaration"

619 where

620 where

621+ fundeps :: IdrisParser [Name]

622+ fundeps = do lchar '|'; sepBy name (lchar ',')

623+

620 carg :: IdrisParser (Name, PTerm)

624 carg :: IdrisParser (Name, PTerm)

621 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

625 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

622 return (i, ty)

626 return (i, ty)

src/Idris/REPL.hs+1−1

@@ -773,7 +773,7 @@ process fn (NewDefn decls) = do

773 getName (PTy docs argdocs syn fc opts name ty) = Just name

774 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

775 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

776− getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name

776+ getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

777 getName _ = Nothing

778 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

779 getClauseName (PClause fc name whole with rhs whereBlock) = name

src/Idris/Reflection.hsnew file+18

@@ -0,0 +1,18 @@

1+{-|

2+Handy tools for doing reflection.

3+-}

4+module Idris.Reflection where

5+

6+import Idris.Core.TT

7+import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))

8+

9+data RArg = RExplicit { argName :: Name, argTy :: Raw }

10+ | RImplicit { argName :: Name, argTy :: Raw }

11+ | RConstraint { argName :: Name, argTy :: Raw }

12+

13+data RTyDecl = RDeclare Name [RArg] Raw

14+

15+rArgToPArg :: RArg -> PArg

16+rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

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

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

test/basic002/test006.idr+1−1

@@ -18,7 +18,7 @@ natToBin k with (parity k)

18 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

19

20main : IO ()

21−main = do print (natToBin 42)

21+main = do printLn (natToBin 42)

22

23---------- Proofs ----------

24

test/basic003/test027.idr+3−3

@@ -19,7 +19,7 @@ using (Ord a, Num n)

19 mprod (x :: xs) = x * mprod xs

20

21main : IO ()

22−main = do print $ isort [1,5,3,5,1,9,8]

22+main = do printLn $ isort [1,5,3,5,1,9,8]

23− print $ msum [1..10]

23+ printLn $ msum [1..10]

24− print $ mprod [1..10]

24+ printLn $ mprod [1..10]

25

test/basic004/test016.idr+1−1

@@ -13,5 +13,5 @@ take (S n) (x :: xs) = x :: take n xs

13take n [] = []

14

15main : IO ()

16−main = do print (take 10 (Main.countFrom 10))

16+main = do printLn (take 10 (Main.countFrom 10))

17

test/basic005/test019.lidr+1−1

@@ -14,5 +14,5 @@

14> | False = ifFalse x

15

16> main : IO ()

17−> main = print (test ((S 4) ==) 5 Oh)

17+> main = printLn (test ((S 4) ==) 5 Oh)

18

test/basic006/test020.idr+2−2

@@ -21,7 +21,7 @@ test : Integer -> String

21test x = "Number " ++ x

22

23main : IO ()

24−main = do print (foo [1,2,3])

24+main = do printLn (foo [1,2,3])

25− print (test 42)

25+ printLn (test 42)

26

27

test/basic006/test020a.idr+1−1

@@ -16,5 +16,5 @@ foo : Vect n a -> List a

16foo xs = reverse xs

17

18main : IO ()

19−main = print (foo [1,2,3])

19+main = printLn (foo [1,2,3])

20

test/basic007/test033.idr+1−1

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

1module Main

2

3main : IO ()

4−main = nullPtr null >>= print

4+main = nullPtr null >>= printLn

test/basic011/basic011.idr+10−10

@@ -3,14 +3,14 @@ module Main

3import Data.Hash

4

5main : IO ()

6−main = do print $ hash (the Bits8 3)

6+main = do printLn $ hash (the Bits8 3)

7− print $ hash (the (List Bits8) [3])

7+ printLn $ hash (the (List Bits8) [3])

8− print $ hash "hello world"

8+ printLn $ hash "hello world"

9− print $ hash 'a'

9+ printLn $ hash 'a'

10− print $ hash (the Bits8 3)

10+ printLn $ hash (the Bits8 3)

11− print $ hash (the Bits16 3)

11+ printLn $ hash (the Bits16 3)

12− print $ hash (the Bits32 3)

12+ printLn $ hash (the Bits32 3)

13− print $ hash (the Bits64 3)

13+ printLn $ hash (the Bits64 3)

14− print $ hash (the Int 3)

14+ printLn $ hash (the Int 3)

15− print $ hash (the Integer 3)

15+ printLn $ hash (the Integer 3)

16

test/basic012/basic012.idr+5−4

@@ -1,7 +1,7 @@

1import Data.Vect

2import Control.Monad.State

3import Control.Monad.Identity

4−

4+

5VThing : Type

6VThing = {n : Nat} -> Vect n Int -> Int

7

@@ -31,7 +31,8 @@ testfoo3 xs = foo 42 xs (bar 10)

31AnyST : Type -> Type -> Type

32AnyST s a = {m : _} -> Monad m => StateT s m a

33

34−foost: AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

35foost = do x <- get

36foost = do x <- get

36 put x

37 put x

37

38

@@ -52,11 +53,11 @@ tupleId f (a, b) = (f a, f b)

52

53

53AppendType : Type

54AppendType : Type

54AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

55−

56+

56append : AppendType

57append : AppendType

57append [] ys = ys

58append [] ys = ys

58append (x :: xs) ys = x :: append xs ys

59append (x :: xs) ys = x :: append xs ys

59

60

60main : IO ()

61main : IO ()

61main = do putStrLn (baz 42)

62main = do putStrLn (baz 42)

62− print (append [1,2,3] [4,5,6])

63+ printLn (append [1,2,3] [4,5,6])

test/dsl001/test001.idr+2−2

@@ -96,8 +96,8 @@ testEnv : Int -> Env [TyInt,TyInt]

96testEnv x = [x,x]

97

98main : IO ()

99−main = do { print testFac

99+main = do { printLn testFac

100− print test }

100+ printLn test }

101

102

103

test/effects002/test025.idr+1−1

@@ -30,6 +30,6 @@ testMemory = do Src :- allocate 5

30

31main : IO ()

32main = ioe_run (runInit [Dst := (), Src := ()] testMemory)

33− (\err => print err) (\ok => print ok)

33+ (\err => printLn err) (\ok => printLn ok)

34

35

test/io002/test008.idr+1−1

@@ -22,7 +22,7 @@ main = do (a, b) <- ioVals

22 let x = "bar"

23 putStrLn (show (getVal x 7 testlist))

24 let ((y, z) :: _) = testlist

25− print z

25+ printLn z

26 case lookup x testlist of

27 Just v => putStrLn (show v)

28 Nothing => putStrLn "Not there!"

test/io003/test018a.idr+1−1

@@ -27,7 +27,7 @@ mainProc = do mainID <- myID

27

28repeatIO : Int -> IO ()

29repeatIO 0 = return ()

30−repeatIO n = do print n

30+repeatIO n = do printLn n

31 run mainProc

32 repeatIO (n - 1)

33

test/primitives001/test005.idr+6−6

@@ -7,9 +7,9 @@ tlist : List Int

7tlist = [1, 2, 3, 4, 5]

8

9main : IO ()

10−main = do print (abs (-8))

10+main = do printLn (abs (-8))

11− print (abs (S Z))

11+ printLn (abs (S Z))

12− print (span isAlpha tstr)

12+ printLn (span isAlpha tstr)

13− print (break isDigit tstr)

13+ printLn (break isDigit tstr)

14− print (span (\x => x < 3) tlist)

14+ printLn (span (\x => x < 3) tlist)

15− print (break (\x => x > 2) tlist)

15+ printLn (break (\x => x > 2) tlist)

test/proof003/test015.idr+3−3

@@ -72,10 +72,10 @@ readNum = do putStr "Enter a number:"

72

73main : IO ()

74main = do let Just bin1 = natToBin 8 42

75− print bin1

75+ printLn bin1

76 let Just bin2 = natToBin 8 89

77− print bin2

77+ printLn bin2

78− print (adc bin1 bin2 b0)

78+ printLn (adc bin1 bin2 b0)

79

80

81

test/records001/test011.idr+5−5

@@ -20,9 +20,9 @@ person = MkPerson "Fred" 30

20main : IO ()

21main = do let x = record { name = "foo",

22 more_things = reverse ["a","b"] } testFoo

23− print $ name x

23+ printLn $ name x

24− print $ name person

24+ printLn $ name person

25− print $ things x

25+ printLn $ things x

26− print $ more_things x

26+ printLn $ more_things x

27− print $ age (record { age = 25 } person)

27+ printLn $ age (record { age = 25 } person)

28

test/records003/records003.idr+6−6

@@ -38,10 +38,10 @@ test : Meeting 2015

38test = next_year idm_gbg

39

40main : IO ()

41−main = do print (record { event->organiser->name } test)

41+main = do printLn (record { event->organiser->name } test)

42− print (record { event->organiser->age } test)

42+ printLn (record { event->organiser->age } test)

43− print (record { event->organiser->age } idm_gbg)

43+ printLn (record { event->organiser->age } idm_gbg)

44− print (record { organiser->age } test)

44+ printLn (record { organiser->age } test)

45− print (record { organiser->age } idm_gbg)

45+ printLn (record { organiser->age } idm_gbg)

46− print (record { year } idm_gbg)

46+ printLn (record { year } idm_gbg)

47

test/reg002/reg012.idr+1−1

@@ -30,4 +30,4 @@ swap (x :: Nil) = x :: Nil

30swap (x :: y :: xs) = (y :: x :: (swap xs))

31

32main : IO ()

33−main = print (swap [1,2,3,4,5])

33+main = printLn (swap [1,2,3,4,5])

test/reg004/reg004.idr+1−1

@@ -13,4 +13,4 @@ h True = r2 where

13 r2 = r

14

15main : IO ()

16−main = do print (h True); print (h False)

16+main = do printLn (h True); printLn (h False)

test/reg013/reg013.idr+3−3

@@ -2,7 +2,7 @@ module Main

2

3main : IO ()

4main = do

5− print $ prim_lenString "hallo"

5+ printLn $ prim_lenString "hallo"

6− print $ prim_lenString "1"

6+ printLn $ prim_lenString "1"

7− print $ prim_lenString ""

7+ printLn $ prim_lenString ""

8

test/reg016/reg016.idr+6−6

@@ -1,11 +1,11 @@

1module Main

2

3main : IO ()

4−main = do print $ the Integer 429496729500000000000000

4+main = do printLn $ the Integer 429496729500000000000000

5−-- print $ the Integer 4294967296

5+-- printLn $ the Integer 4294967296

6−-- print $ the Integer 4294967297

6+-- printLn $ the Integer 4294967297

7−-- print $ the Int 4294967295

7+-- printLn $ the Int 4294967295

8−-- print $ the Int 4294967296

8+-- printLn $ the Int 4294967296

9−-- print $ the Int 4294967297

9+-- printLn $ the Int 4294967297

10

11

test/reg017/reg017.idr+1−1

@@ -10,4 +10,4 @@ foo : { t : Type } ->

10foo {t} a {prfA = p} b c {prfBC} = b

11

12main : IO ()

13−main = print $ foo 3 4 4

13+main = printLn $ foo 3 4 4

test/reg018/reg018d.idr+1−1

@@ -12,4 +12,4 @@ pull {n=S _} (FS n) (x :: xs) =

12 (v, x::vs)

13

14main : IO ()

15−main = print (pull FZ [0, 1, 2])

15+main = printLn (pull FZ [0, 1, 2])

test/reg027/reg027.idr+1−1

@@ -27,6 +27,6 @@ foo = do val <- dbl

27 \x => show val

28

29main : IO ()

30−main = do print dbl

30+main = do printLn dbl

31 putStrLn (foo 3)

32

test/reg029/reg029.idr+2−2

@@ -7,5 +7,5 @@ import System

7

8main : IO ()

9main = do

10− print !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

10+ printLn !(getEnv "IDRIS_REG029_NONEXISTENT_VAR")

11− print !(getEnv "IDRIS_REG029_EXISTENT_VAR")

11+ printLn !(getEnv "IDRIS_REG029_EXISTENT_VAR")

test/reg031/reg031.idr+1−1

@@ -1,7 +1,7 @@

1module Main

2

3main : IO ()

4−main = print . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

4+main = printLn . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

5 where

6 -- make the values positive if the backend has signed chars

7 val : Char -> Int

test/reg040/reg040.idr+1−1

@@ -4,4 +4,4 @@ io : IO Int

4io = return 42

5

6main : IO ()

7−main = print $ unsafePerformIO io

7+main = printLn $ unsafePerformIO io

test/reg042/reg042.idr+1−1

@@ -21,4 +21,4 @@ g (C x y z) = x + y

21-- Here, we'd apply the not-a-function to the erased argument 4,

22-- which would make the program go wrong.

23main : IO ()

24−main = print $ g (proj 3 f 4)

24+main = printLn $ g (proj 3 f 4)

test/reg045/reg045.idr+1−1

@@ -15,5 +15,5 @@ foo : ListZ Nat

15foo = (1 :: 2 :: 3 :: Nil)

16

17main : IO ()

18−main = print foo

18+main = printLn foo

19

test/reg052/reg052.idr+1−1

@@ -5,4 +5,4 @@ impure_int : IO Int

5impure_int = return 41

6

7main : IO ()

8−main = impure_int >>= impure_op . prim__zextInt_B64 >>= print

8+main = impure_int >>= impure_op . prim__zextInt_B64 >>= printLn

test/sourceLocation001/SourceLoc.idr+4−4

@@ -36,7 +36,7 @@ using (ctxt : Vect n Ty)

36 Var : (i : Fin n) -> Tm ctxt (index i ctxt)

37 Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

38 App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'

39− ||| A term that makes the program halt and print where it halted

39+ ||| A term that makes the program halt and printLn where it halted

40 Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

41

42 data Env : Vect n Ty -> Type where

@@ -83,11 +83,11 @@ testTerm4 = App testTerm3 MkU

83namespace Main

84 main : IO ()

85 main = do putStrLn "Testing using definition"

86− print fromRHS

86+ printLn fromRHS

87 putStrLn "Testing using inline tactics"

88− print fromProofScript

88+ printLn fromProofScript

89 putStrLn "Testing using metavariable with later definition"

90− print fromMetavar

90+ printLn fromMetavar

91 putStrLn "-----------------------"

92 sequence_ $ with List [ exec testTerm1

93 , exec testTerm2

test/sugar001/test007.idr+4−4

@@ -35,7 +35,7 @@ runEval env e with (eval e) {

35}

36

37main : IO ()

38−main = do print [| (\x => x *2) (Just 4) |]

38+main = do printLn [| (\x => x *2) (Just 4) |]

39− print [| plus (Just 4) (Just 5) |]

39+ printLn [| plus (Just 4) (Just 5) |]

40− print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

40+ printLn (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41− print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41+ printLn (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

test/sugar004/sugar004.idr+1−1

@@ -9,7 +9,7 @@ foo x = let Just x' = x | Nothing => 100 in x'

9main : IO ()

10main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

11 | (x :: y :: _) => putStrLn "Too many arguments!"

12− print (foo (Just (cast a)))

12+ printLn (foo (Just (cast a)))

13

14{-

15

test/sugar005/As.idr+9−9

@@ -24,13 +24,13 @@ same _ _ = Nothing

24

25namespace Main

26 main : IO ()

27− main = do print $ isS 0

27+ main = do printLn $ isS 0

28− print $ isS 1

28+ printLn $ isS 1

29− print $ hasS [0,0,0]

29+ printLn $ hasS [0,0,0]

30− print $ hasS [0,1,2]

30+ printLn $ hasS [0,1,2]

31− print $ isSS 5

31+ printLn $ isSS 5

32− print $ isSS 0

32+ printLn $ isSS 0

33− print $ same 1 1

33+ printLn $ same 1 1

34− print $ same 0 0

34+ printLn $ same 0 0

35− print $ same 1 0

35+ printLn $ same 1 0

36

test/tactics001/Tactics.idr+14

@@ -2,6 +2,9 @@ module Tactics

2

3import Language.Reflection.Tactical

4

5+import Data.Vect

6+

7+

5%default total

8%default total

6

9

7-- Test that basic proofs with new-style tactics work

10-- Test that basic proofs with new-style tactics work

@@ -25,3 +28,14 @@ plusSuccRightSuccNew (S j) k =

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

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

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

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

27 solve)

30 solve)

31+

32+-- Test that side effects in new tactics work

33+

34+mkDecl : ()

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

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

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

38+ fill `(() : ())

39+ solve)

40+

41+repUnit = pure ()

test/totality004/totality004.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

21countStream x = x :: countStream (x + 1)

22

23main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

25

test/totality004/totality004a.idr+1−1

@@ -21,5 +21,5 @@ countStream : Nat -> Stream Nat

21countStream x = x :: countStream (x + 1)

22

23main : IO ()

24−main = print (take 10 (process doubleInt (countStream 1)))

24+main = printLn (take 10 (process doubleInt (countStream 1)))

25

test/totality005/totality005.idr+1−1

@@ -7,4 +7,4 @@ fib : Stream Nat

7fib = 0 :: zipWithS (+) fib (1 :: fib)

8

9partial main : IO ()

10−main = print (take 15 fib)

10+main = printLn (take 15 fib)

test/tutorial002/tutorial002.idr+1−1

@@ -34,7 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

34main : IO ()

35main = do putStr "Enter a number: "

36 x <- getLine

37− print (natToBin (fromInteger (cast x)))

37+ printLn (natToBin (fromInteger (cast x)))

38

39---------- Proofs ----------

40